SPARK
From MaRDI portal
Software:15656
swMATH3124MaRDI QIDQ15656FDOQ15656
Author name not available (Why is that?)
Cited In (36)
- Implicit flows in malicious and nonmalicious code
- Title not available (Why is that?)
- Relational Decomposition
- 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.
- Title not available (Why is that?)
- Title not available (Why is that?)
- Precise and Automated Contract-Based Reasoning for Verification and Certification of Information Flow Properties of Programs with Arrays
- 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
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Panellist position statement: some industrial experience with program verification
- 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
- Generating good pseudo-random numbers
- Valigator: A Verification Tool with Bound and Invariant Generation
- Title not available (Why is that?)
- 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
- Automatic Generation of CSP || B Skeletons from xUML Models
- Building High Integrity Applications with SPARK
- Specification and verification challenges for sequential object-oriented programs
- A mechanical analysis of program verification strategies
- The safety-critical Java memory model formalised
- A Software Component Model and Its Preliminary Formalisation
- Software Verification and Analysis
- Title not available (Why is that?)
- Hoare type theory, polymorphism and separation
This page was built for software: SPARK