Software verification with BLAST

DOI10.1007/3-540-44829-2_17MaRDI QIDQ4426387zbMATH OpenFDO

Authors Ranjit Jhala, Rupak Majumdar, Grégoire Sutre, Thomas A. Henzinger

Publication date 16 September 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/2648/26480235.htm

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Static Analysis
• Model checking: from hardware to software.
• Temporal-safety proofs for systems code
• Experience of improving the BLAST static verification tool
• Lazy abstraction

Cited in

(31)

• Integration of verification methods for program systems
• BLAST
• A compiler for MSVL and its applications
• Experience of improving the BLAST static verification tool
• TASS: the toolkit for accurate scientific software
• Verification by gambling on program slices
• Rule-based static analysis of network protocol implementations
• Highly dependable concurrent programming using design for verification
• Logic verification of ANSI-C code with SPIN
• Reducing crash recoverability to reachability
• Infeasible paths elimination by symbolic execution techniques. Proof of correctness and preservation of paths
• Stochastic modelling of communication protocols from source code
• Automated formal analysis and verification: an overview
• TRACER: a symbolic execution tool for verification
• Featherweight VeriFast
• LCTD: test-guided proofs for C programs on LLVM
• C Wolf -- A toolset for extracting models from C programs
• Temporal-safety proofs for systems code
• Counterexample guided path reduction for static program analysis
• A Forward-Backward Abstraction Refinement Algorithm
• On-the-Fly Techniques for Game-Based Software Model Checking
• Static Analysis
• Tools and Algorithms for the Construction and Analysis of Systems
• Computer Aided Verification
• Computer Aided Verification
• Abstraction refinement and antichains for trace inclusion of infinite state systems
• An invariant-based approach to the verification of asynchronous parameterized networks
• Doomed program points
• SAT-based bounded model checking for propositional projection temporal logic
• Model-checking structured context-free languages
• Formal verification of C systems code. Structured types, separation logic and theorem proving

This page was built for publication: Software verification with BLAST

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