Constraint-Based Invariant Inference over Predicate Abstraction
From MaRDI portal
Publication:3600470
DOI10.1007/978-3-540-93900-9_13zbMath1206.68087OpenAlexW1877129949MaRDI QIDQ3600470
Sumit Gulwani, Ramarathnam Venkatesan, Saurabh Srivastava
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
Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items (9)
Combining Model Checking and Data-Flow Analysis ⋮ On the complexity of the quantified bit-vector arithmetic with binary encoding ⋮ Efficiently solving quantified bit-vector formulas ⋮ Counterexample-Guided Model Synthesis ⋮ From invariant checking to invariant inference using randomized search ⋮ Automatically inferring loop invariants via algorithmic learning ⋮ Bugs, Moles and Skeletons: Symbolic Reasoning for Software Development ⋮ Complexity and Algorithms for Monomial and Clausal Predicate Abstraction ⋮ Synthesis of Domain Specific CNF Encoders for Bit-Vector Solvers
Uses Software
This page was built for publication: Constraint-Based Invariant Inference over Predicate Abstraction