scientific article; zbMATH DE number 2080047

MaRDI QIDQ4472235zbMATH OpenFDO

Authors Thomas Ball, Andreas Podelski, Sriram K. Rajamani

Publication date 4 August 2004

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2280/22800158.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

• scientific article; zbMATH DE number 1953015
• scientific article; zbMATH DE number 1834576
• Model checking: from hardware to software.
• scientific article; zbMATH DE number 1759702
• scientific article; zbMATH DE number 1903343

Cited in

(11)

• Infinite-state invariant checking with IC3 and predicate abstraction
• A semantic framework for the abstract model checking of tccp programs
• Distributing the workload in a lazy theorem-prover
• Abstraction Refinement for Quantified Array Assertions
• Refinement of Trace Abstraction
• Combining theories with shared set operations
• Verification of multi-linked heaps
• Verification Modulo theories
• On recursion-free Horn clauses and Craig interpolation
• Verifying time partitioning in the DEOS scheduling kernel
• Verification and falsification of programs with loops using predicate abstraction

Describes a project that uses

Uses Software

• Bandera
• HyTech

This page was built for publication:

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