SPARK
From MaRDI portal
SPARK Q15656
Cited in
(67)- TraitCbC
- Panellist position statement: some industrial experience with program verification
- Automatic Generation of CSP || B Skeletons from xUML Models
- Inter-process buffers in separation logic with rely-guarantee
- Formal methods for components and objects. 4th international symposium, FMCO 2005, Amsterdam, The Netherlands, November 1--4, 2005. Revised lectures.
- Proving the correctness of mobile Java code
- SICStus Prolog -- the first 25 years
- Building high integrity applications with SPARK
- The safety-critical Java memory model formalised
- scientific article; zbMATH DE number 5652074 (Why is no real title available?)
- Precise and automated contract-based reasoning for verification and certification of information flow properties of programs with arrays
- FeatherTrait
- HOL-Boogie -- an interactive prover-backend for the verifying C compiler
- An engineering process for the verification of real-time systems
- Formalizing Single-Assignment Program Verification: An Adaptation-Complete Approach
- The verified software repository: a step towards the verifying compiler
- scientific article; zbMATH DE number 2080002 (Why is no real title available?)
- Generating good pseudo-random numbers
- SafeJML
- Are the logical foundations of verifying compiler prototypes matching user expectations?
- Programming language elements for proof construction
- Valigator
- Ada95
- LARCH
- JML
- JACK
- StateFlow
- Omnibus
- Cheddar
- Spec#
- CZT
- ArcAngelC
- SPARKSkein
- ESC/Java
- JUnit
- An integrated approach to high integrity software verification
- PolyPaver
- Flow Caml
- Alcoa
- Amphion
- LOOP
- GNATprove
- ProBE
- Implicit flows in malicious and nonmalicious code
- Investigating the usability of real-time scheduling theory with the Cheddar project
- Splint
- Houdini
- Jessie
- AstraVer
- Jass
- JSFlow
- ANNA
- Programming language elements for correctness proofs
- scientific article; zbMATH DE number 2217740 (Why is no real title available?)
- A Software Component Model and Its Preliminary Formalisation
- Specification and verification challenges for sequential object-oriented programs
- A verifying compiler for a multi-threaded object-oriented language
- Combining behavioural types with security analysis
- scientific article; zbMATH DE number 47171 (Why is no real title available?)
- scientific article; zbMATH DE number 2080006 (Why is no real title available?)
- Relational decomposition
- Deriving a Floyd-Hoare logic for non-local jumps from a formulæ-as-types notion of control
- Hoare type theory, polymorphism and separation
- Valigator: A Verification Tool with Bound and Invariant Generation
- Polynomial function intervals for floating-point software verification
- Software Verification and Analysis
- A mechanical analysis of program verification strategies
This page was built for software: SPARK
