SPARK

swMATH3124MaRDI QIDQ15656

No author found.

Related Items (36)

Unnamed Item ⋮ SICStus Prolog—The first 25 years ⋮ Formal methods for components and objects. 4th international symposium, FMCO 2005, Amsterdam, The Netherlands, November 1--4, 2005. Revised lectures. ⋮ Panellist position statement: some industrial experience with program verification ⋮ Are the logical foundations of verifying compiler prototypes matching user expectations? ⋮ Specification and verification challenges for sequential object-oriented programs ⋮ An integrated approach to high integrity software verification ⋮ HOL-Boogie -- an interactive prover-backend for the verifying C compiler ⋮ Implicit flows in malicious and nonmalicious code ⋮ An engineering process for the verification of real-time systems ⋮ Inter-process buffers in separation logic with rely-guarantee ⋮ Building High Integrity Applications with SPARK ⋮ Combining behavioural types with security analysis ⋮ Unnamed Item ⋮ The safety-critical Java memory model formalised ⋮ Unnamed Item ⋮ Unnamed Item ⋮ The verified software repository: a step towards the verifying compiler ⋮ Deriving a Floyd-Hoare logic for non-local jumps from a formulæ-as-types notion of control ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Polynomial function intervals for floating-point software verification ⋮ A mechanical analysis of program verification strategies ⋮ Unnamed Item ⋮ Hoare type theory, polymorphism and separation ⋮ Precise and Automated Contract-Based Reasoning for Verification and Certification of Information Flow Properties of Programs with Arrays ⋮ A Software Component Model and Its Preliminary Formalisation ⋮ Unnamed Item ⋮ Formalizing Single-Assignment Program Verification: An Adaptation-Complete Approach ⋮ Generating good pseudo-random numbers ⋮ Relational Decomposition ⋮ Unnamed Item ⋮ Investigating the usability of real-time scheduling theory with the Cheddar project ⋮ Software Verification and Analysis ⋮ Valigator: A Verification Tool with Bound and Invariant Generation ⋮ Automatic Generation of CSP || B Skeletons from xUML Models

This page was built for software: SPARK