Computer Aided Verification

DOI10.1007/B98490zbMATH Open1103.68604OpenAlexW4298302743MaRDI QIDQ5312923FDOQ5312923

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

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

Mathematics Subject Classification ID

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

Cited In (13)

• Efficient theory combination via Boolean search
• Interpolant Generation for UTVPI
• Weakly-relational shapes for numeric abstractions: Improved algorithms and proofs of correctness
• Strategies for combining decision procedures
• Zap: Automated Theorem Proving for Software Analysis
• Predicate abstraction and CEGAR for \(\nu \mathrm{HFL}_\mathbb{Z}\) validity checking
• Zapato
• 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
• An Improved Tight Closure Algorithm for Integer Octagonal Constraints

Uses Software

• veriSoft
• Bogor
• Bandera
• Eraser

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)