SPARK

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