Counterexample-guided precondition inference

DOI10.1007/978-3-642-37036-6_25MaRDI QIDQ5326301zbMATH OpenOpenAlexFDO

Authors Mohamed Nassim Seghir, Daniel Kroening

Publication date 5 August 2013

Published in Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-37036-6_25

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

• Necessary and Sufficient Preconditions via Eager Abstraction
• Precondition inference from intermittent assertions and application to contracts on collections
• An iterative approach to precondition inference using constrained Horn clauses
• Constraint-Based Invariant Inference over Predicate Abstraction
• Sufficient Preconditions for Modular Assertion Checking

Cited in

(8)

• Instrumenting a weakest precondition calculus for counterexample generation
• Precondition inference from intermittent assertions and application to contracts on collections
• An iterative approach to precondition inference using constrained Horn clauses
• Inferring sufficient conditions with backward polyhedral under-approximations
• Counterexample-guided focus
• Sufficient Preconditions for Modular Assertion Checking
• Transformation-Enabled Precondition Inference
• A query-based constraint acquisition approach for enhanced precision in program precondition inference

This page was built for publication: Counterexample-guided precondition inference

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