Temporal-safety proofs for systems code

DOI10.1007/3-540-45657-0_45MaRDI QIDQ4804923zbMATH OpenFDO

Authors Ranjit Jhala, Rupak Majumdar, George C. Necula, Grégoire Sutre, Westley Weimer, Thomas A. Henzinger

Publication date 1 May 2003

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/2404/24040526.htm

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Software verification with BLAST
• scientific article; zbMATH DE number 2163030
• scientific article; zbMATH DE number 2110618
• Automatically validating temporal safety properties of interfaces
• Certifying model checkers

Cited in

(22)

• Experience of improving the BLAST static verification tool
• A local approach for temporal model checking of Java bytecode
• Reusing predicate precision in value analysis
• Decomposing data structure commutativity proofs with \(mn\)-differencing
• Theory and practice of unparsed patterns for metacompilation
• Modular strategies for recursive game graphs
• The word problem for visibly pushdown languages described by grammars
• Deep specifications and certified abstraction layers
• Combining model checking and data-flow analysis
• Model checking procedural programs
• AUSPICE-R: automatic safety-property proofs for realistic features in machine code
• Algorithmic Analysis of Array-Accessing Programs
• Software verification with BLAST
• Automatically validating temporal safety properties of interfaces
• Static Analysis
• Proving LTL Properties of Bitvector Programs and Decompiled Binaries
• Making \(\mathsf{IP}=\mathsf{PSPACE}\) practical: efficient interactive protocols for BDD algorithms
• Per-dereference verification of temporal heap safety via adaptive context-sensitive analysis
• A resolution-based interactive proof system for UNSAT
• From verification to causality-based explications (invited talk)
• A resolution-based interactive proof system for UNSAT
• Verification and falsification of programs with loops using predicate abstraction

This page was built for publication: Temporal-safety proofs for systems code

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