Constraint-Based Invariant Inference over Predicate Abstraction

DOI10.1007/978-3-540-93900-9_13MaRDI QIDQ3600470zbMATH OpenOpenAlexFDO

Authors Sumit Gulwani, Saurabh Srivastava, Ramarathnam Venkatesan

Publication date 10 February 2009

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

Full work available at URL https://doi.org/10.1007/978-3-540-93900-9_13

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

• Predicate abstraction of ANSI-C programs using SAT
• Predicate abstraction in a program logic calculus
• Predicate Abstraction in a Program Logic Calculus
• Predicate abstraction for program verification
• Verification, Model Checking, and Abstract Interpretation

Cited in

(15)

• On the complexity of the quantified bit-vector arithmetic with binary encoding
• Synthesis of domain specific CNF encoders for bit-vector solvers
• From invariant checking to invariant inference using randomized search
• Automatically inferring loop invariants via algorithmic learning
• Truncating abstraction of bit-vector operations for BDD-based SMT solvers
• Counterexample-guided precondition inference
• Predicate Generation for Learning-Based Quantifier-Free Loop Invariant Inference
• Efficiently solving quantified bit-vector formulas
• Complexity and Algorithms for Monomial and Clausal Predicate Abstraction
• Bugs, moles and skeletons: symbolic reasoning for software development
• Verification Constraint Problems with Strengthening
• Programming Languages and Systems
• Combining model checking and data-flow analysis
• Counterexample-Guided Model Synthesis
• Predicate generation for learning-based quantifier-free loop invariant inference

Describes a project that uses

Uses Software

• Saturn

This page was built for publication: Constraint-Based Invariant Inference over Predicate Abstraction

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