Predicate Abstraction via Symbolic Decision Procedures
We present a new approach for performing predicate abstraction based on symbolic decision procedures. Intuitively, a symbolic decision procedure for a theory takes a set of predicates in the theory and symbolically executes a decision procedure on all the subsets over the set of predicates. The resu...
Main Authors: | Shuvendu K. Lahiri, Thomas Ball, Byron Cook |
---|---|
Format: | Article |
Language: | English |
Published: |
Logical Methods in Computer Science e.V.
2007-04-01
|
Series: | Logical Methods in Computer Science |
Subjects: | |
Online Access: | https://lmcs.episciences.org/2218/pdf |
Similar Items
-
Proof-irrelevant model of CC with predicative induction and judgmental equality
by: Gyesik Lee, et al.
Published: (2011-11-01) -
Formalization of Abstract State Transition Systems for SAT
by: Filip Maric, et al.
Published: (2011-09-01) -
Automatic Modular Abstractions for Template Numerical Constraints
by: David Monniaux
Published: (2010-07-01) -
On Irrelevance and Algorithmic Equality in Predicative Type Theory
by: Andreas Abel, et al.
Published: (2012-03-01) -
Reasoning about Strategies: on the Satisfiability Problem
by: Fabio Mogavero, et al.
Published: (2017-03-01)