swMATH3124MaRDI QIDQ15656FDOQ15656
Author name not available (Why is that?)
Official website: http://en.wikipedia.org/wiki/SPARK_%28programming_language%29
Cited In (65)
- TraitCbC
- Panellist position statement: some industrial experience with program verification
- Automatic Generation of CSP || B Skeletons from xUML Models
- Implicit flows in malicious and nonmalicious code
- Title not available (Why is that?)
- 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.
- FeatherTrait
- 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
- SafeJML
- Polynomial function intervals for floating-point software verification
- Building high integrity applications with SPARK
- Title not available (Why is that?)
- A verifying compiler for a multi-threaded object-oriented language
- Ada95
- JML
- JACK
- StateFlow
- Omnibus
- Cheddar
- Spec#
- CZT
- ArcAngelC
- SPARKSkein
- ESC/Java
- JUnit
- Title not available (Why is that?)
- PolyPaver
- Flow Caml
- Alcoa
- Amphion
- LOOP
- GNATprove
- ProBE
- Title not available (Why is that?)
- Programming language elements for correctness proofs
- 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
- Splint
- Houdini
- Jessie
- AstraVer
- Jass
- JSFlow
- Generating good pseudo-random numbers
- Valigator: A Verification Tool with Bound and Invariant Generation
- ANNA
- Formalizing Single-Assignment Program Verification: An Adaptation-Complete Approach
- The verified software repository: a step towards the verifying compiler
- Investigating the usability of real-time scheduling theory with the Cheddar project
- Relational decomposition
- Specification and verification challenges for sequential object-oriented programs
- A mechanical analysis of program verification strategies
- 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
- Precise and automated contract-based reasoning for verification and certification of information flow properties of programs with arrays
- Title not available (Why is that?)
- Hoare type theory, polymorphism and separation
- Proving the correctness of mobile Java code
This page was built for software: SPARK
