Name
Abstract | ||
|---|---|---|
The paper presents a method, called the method of verification by invisible invariants, for the automatic verification of a large class of parameterized systems. The method is based on the automatic calculation of candidate inductive assertions and checking for their inductiveness, using symbolic model-checking techniques for both tasks. First, we show how to use model-checking techniques over finite (and small) instances of the parameterized system in order to derive candidates for invariant assertions. Next, we show that the premises of the standard deductive INV rule for proving invariance properties can be automatically resolved by finite-state (BDD-based) methods with no need for interactive theorem proving. Combining the automatic computation of invariants with the automatic resolution of the VCs (verification conditions) yields a (necessarily) incomplete but fully automatic sound method for verifying large classes of parameterized systems. The generated invariants can be transferred to the VC-validation phase without ever been examined by the user, which explains why we refer to them as "invisible". The efficacy of the method is demonstrated by automatic verification of diverse parameterized systems in a fully automatic and efficient manner. |
Year | DOI | Venue |
|---|---|---|
2001 | 10.1007/3-540-44585-4_19 | CAV |
Keywords | Field | DocType |
large class,automatic verification,automatically computed inductive assertions,automatic resolution,automatic sound method,invisible invariants,parameterized system,verification condition,automatic calculation,parameterized verification,diverse parameterized system,automatic computation,model checking | Atomic formula,Discrete mathematics,Parameterized complexity,Invariant (physics),Computer science,Automated theorem proving,Algorithm,Symbolic computation,Theoretical computer science,Invariant (mathematics),Mutual exclusion,Proof assistant | Conference |
Volume | ISSN | ISBN |
2102 | 0302-9743 | 3-540-42345-1 |
Citations | PageRank | References |
111 | 3.68 | 31 |
Authors | ||
5 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Tamarah Arons | 1 | 278 | 14.59 |
| Amir Pnueli | 2 | 12964 | 2377.59 |
| Sitvanit Ruah | 3 | 293 | 13.04 |
| Jiazhao Xu | 4 | 118 | 4.59 |
| Lenore D. Zuck | 5 | 1559 | 141.69 |