Automatically validating temporal safety properties of interfaces

DOI10.1007/3-540-45139-0_7MaRDI QIDQ4531754zbMATH OpenFDO

Authors Thomas Ball, Sriram K. Rajamani

Publication date 23 May 2002

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2057/20570103

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Computing methodologies and applications (68U99)

Recommendations

• ProMoVer: modular verification of temporal safety properties
• Temporal-safety proofs for systems code
• scientific article; zbMATH DE number 52748
• SAT-based induction for temporal safety properties
• Temporal property verification as a program analysis task
• Safe runtime verification of real-time properties
• Refining the Safety-Liveness Classification of Temporal Properties According to Realizability

Cited in

(23)

• Integration of verification methods for program systems
• Syntax-directed model checking of sequential programs
• Translating Xd-C programs to MSVL programs
• Specification and verification of concurrent programs through refinements
• Verification of SpecC using predicate abstraction
• Program verification with interacting analysis plugins
• Highly dependable concurrent programming using design for verification
• View-augmented abstractions
• LCTD: test-guided proofs for C programs on LLVM
• New Challenges in Model Checking
• Splitting the Control Flow with Boolean Flags
• Tutorial on Model Checking: Modelling and Verification in Computer Science
• Could We Have Chosen a Better Loop Invariant or Method Contract?
• Finding and fixing faults
• Verification of multi-linked heaps
• Establishing flight software reliability: testing, model checking, constraint-solving, monitoring and learning
• Temporal-safety proofs for systems code
• Falsifying safety properties through games on over-approximating models
• Verifying multithreaded recursive programs with integer variables
• Extending Model Checking with Dynamic Analysis
• Formal verification of C systems code. Structured types, separation logic and theorem proving
• An abstract interpretation toolkit for CRL
• Implementation and analysis of real-time communication protocol compositions

Describes a project that uses

Uses Software

• Bandera
• SPIN
• PVS
• Bebop
• SIMPLIFY

This page was built for publication: Automatically validating temporal safety properties of interfaces

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4531754)