Name
Abstract | ||
|---|---|---|
In formal verification, we verify that a system is correct withrespect to a specification. Cases like antecedent failure can makea successful pass of the verification procedure meaningless.Vacuity detection can signal such "meaningless" passes of thespecification, and indeed vacuity checks are now a standardcomponent in many commercial model checkers.We address two dimensions of vacuity: the computational effortand the information that is given to the user. As for the firstdimension, we present several preliminary vacuity checks that canbe done without the design itself, which implies that someinformation can be found with a significantly smaller effort. Asfor the second dimension, we present algorithms for deriving twotypes of information that are not provided by standard vacuitychecks, assuming $M\models\varphi$ for a model M andformula φ: (a) behaviors that are possibly missingfrom M (or wrongly restricted by the environment) (b) thelargest subset of occurrences of literals in φ thatcan be replaced with false simultaneously without falsifyingφ in M. The complexity of each of theseproblems is proven. Overall this extra information can lead totighter specifications and more guidance for finding errors. |
Year | DOI | Venue |
|---|---|---|
2009 | 10.1007/s10703-008-0060-y | Formal Methods in System Design |
Keywords | Field | DocType |
Vacuity,Model-checking,Complexity | Model checking,Computer science,Theoretical computer science,Verification procedure,Formal verification | Journal |
Volume | Issue | ISSN |
34 | 1 | 0925-9856 |
Citations | PageRank | References |
7 | 0.43 | 29 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Hana Chockler | 1 | 482 | 38.31 |
| Ofer Strichman | 2 | 1071 | 63.61 |