Paper Info
Title
Complexity and Algorithms for Monomial and Clausal Predicate Abstraction
Abstract
In this paper, we investigate the asymptotic complexity of various predicate abstraction problems relative to the asymptotic complexity of checking an annotated program in a given assertion logic. Unlike previous approaches, we pose the predicate abstraction problem as a decision problem, instead of the traditional inference problem. For assertion logics closed under weakest (liberal) precondition and Boolean connectives, we show two restrictions of the predicate abstraction problem where the two complexities match. The restrictions correspond to the case of monomial and clausal abstraction. For these restrictions, we show a symbolic encoding that reduces the predicate abstraction problem to checking the satisfiability of a single formula whose size is polynomial in the size of the program and the set of predicates. We also provide a new iterative algorithm for solving the clausal abstraction problem that can be seen as the dual of the Houdini algorithm for solving the monomial abstraction problem.
Year
DOI
Venue
2009
10.1007/978-3-642-02959-2_18
CADE
Keywords
Field
DocType
clausal abstraction problem,monomial abstraction problem,decision problem,predicate abstraction problem,traditional inference problem,clausal abstraction,assertion logic,asymptotic complexity,clausal predicate abstraction,houdini algorithm,various predicate abstraction problem,software development,iterative algorithm,satisfiability
Abstraction model checking,Discrete mathematics,Decision problem,Abstraction,Predicate abstraction,Computer science,Algorithm,Theoretical computer science,Precondition,Abstraction inversion,Monomial,Predicate (mathematical logic)
Conference
Volume
ISSN
Citations 
5663
0302-9743
7
PageRank 
References 
Authors
0.50
14
2
Name
Order
Citations
PageRank
Shuvendu K. Lahiri1142468.18
Shaz Qadeer23257239.11