Computer Aided Verification

DOI10.1007/B98490MaRDI QIDQ5312923zbMATH OpenOpenAlexFDO

Authors Thomas Ball, Byron Cook, Shuvendu K. Lahiri, Lintao Zhang

Publication date 25 August 2005

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

Full work available at URL https://doi.org/10.1007/b98490

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Zap: Automated Theorem Proving for Software Analysis
• Thread-modular counterexample-guided abstraction refinement
• scientific article; zbMATH DE number 1956569
• scientific article; zbMATH DE number 1953015
• scientific article; zbMATH DE number 1670775

Cited in

(13)

• An Improved Tight Closure Algorithm for Integer Octagonal Constraints
• Efficient theory combination via Boolean search
• Weakly-relational shapes for numeric abstractions: Improved algorithms and proofs of correctness
• Interpolant Generation for UTVPI
• Strategies for combining decision procedures
• Zap: Automated Theorem Proving for Software Analysis
• Zapato
• Predicate abstraction and CEGAR for \(\nu \mathrm{HFL}_\mathbb{Z}\) validity checking
• SAT-Based Model Checking
• Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis
• Linear Arithmetic with Stars
• M\textbf{ath}SAT: Tight integration of SAT and mathematical decision procedures
• Distributing the workload in a lazy theorem-prover

Describes a project that uses

Uses Software

• Eraser
• Bandera
• Bogor
• veriSoft

This page was built for publication: Computer Aided Verification

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