Name
Abstract | ||
|---|---|---|
We describe a method for computing a minimum-state automaton to act as an intermediate assertion in assume-guarantee reasoning, using a sampling approach and a Boolean satisfiability solver. For a set of synthetic benchmarks intended to mimic common situations in hardware verification, this is shown to be significantly more effective than earlier approximate methods based on Angluin's L* algorithm. For many of these benchmarks, this method also outperforms BDD-based model checking and interpolation-based model checking. We also demonstrate how domain knowledge can be incorporated into our algorithm to improve its performance. |
Year | DOI | Venue |
|---|---|---|
2008 | 10.1007/s10703-008-0050-0 | Formal Methods in System Design |
Keywords | Field | DocType |
Formal verification,Model checking,Compositional verification,Assume-guarantee,L,*,SAT,Decision tree | Functional verification,Model checking,Computer science,Intelligent verification,Boolean satisfiability problem,Algorithm,Theoretical computer science,Runtime verification,Solver,High-level verification,Formal verification | Journal |
Volume | Issue | ISSN |
32 | 3 | 0925-9856 |
Citations | PageRank | References |
40 | 1.36 | 16 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Anubhav Gupta | 1 | 284 | 17.18 |
| Kenneth L. McMillan | 2 | 2604 | 370.71 |
| Zhaohui Fu | 3 | 283 | 14.28 |