Complexity and Algorithms for Monomial and Clausal Predicate Abstraction

predicate abstraction Shuvendu K. Lahiri and Shaz Qadeer Microsoft Research 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. Unvious 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 monomial and clausal abstraction. For these restrictions, we show ic 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 e algorithm for solving the clausal abstraction problem that can be seen as the dual of the Houdi...

• Type: Conference
• Year: 2009
• Where: CADE
• Authors: Shuvendu K. Lahiri, Shaz Qadeer
• Keywords: Automated Reasoning, CADE 2009, Clausal Abstraction, Predicate Abstraction Problem, Various Predicate Abstraction