ExplainHoudini: making Houdini inference transparent

DOI10.1007/978-3-642-18275-4_22MaRDI QIDQ3075491zbMATH OpenOpenAlexFDO

Authors Shuvendu K. Lahiri, Julien Vanegue

Publication date 15 February 2011

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

Full work available at URL https://doi.org/10.1007/978-3-642-18275-4_22

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 1693447
• Precondition inference from intermittent assertions and application to contracts on collections
• Annotation inference for modular checkers
• Modular inference of subprogram contracts for safety checking
• Explaining Verification Conditions

Cites work

• Abstractions from proofs
• Complexity and Algorithms for Monomial and Clausal Predicate Abstraction
• Generating error traces from verification-condition counterexamples
• scientific article; zbMATH DE number 1693447 (Why is no real title available?)
• Interpolation and SAT-based model checking.
• Unifying type checking and property checking for low-level code

Describes a project that uses

Uses Software

• z3
• Spec#
• ESC/Java
• VCC
• PVS
• Houdini
• ExplainHoudini
• Boogie

This page was built for publication: ExplainHoudini: making Houdini inference transparent

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