Loading...
Please wait, while we are loading the content...
Similar Documents
Program verification using templates over predicate abstraction.
| Content Provider | CiteSeerX |
|---|---|
| Author | Srivastava, Saurabh Gulwani, Sumit |
| Abstract | We address the problem of automatically generating invariants with quantified and boolean structure for proving the validity of given assertions or generating pre-conditions under which the assertions are valid. We present three novel algorithms, having different strengths, that combine template and predicate abstraction based formalisms to discover required sophisticated program invariants using SMT solvers. Two of these algorithms use an iterative approach to compute fixed-points (one computes a least fixed-point and the other computes a greatest fixed-point), while the third algorithm uses a constraint based approach to encode the fixed-point. The key idea in all these algorithms is to reduce the problem of invariant discovery to that of finding optimal solutions for unknowns (over conjunctions of some predicates from a given set) in a template formula such that |
| File Format | |
| Access Restriction | Open |
| Content Type | Text |
