Constraint-Based Invariant Inference over Predicate Abstraction

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

Mathematics Subject Classification ID

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

• Saturn

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