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