Name
Title | ||
|---|---|---|
Integrated Formal Verification: Using Model Checking with Automated Abstraction, Invariant Generation, and Theorem Proving |
Abstract | ||
|---|---|---|
Mechanized formal methods that use both model checking and theorem proving seem to hold most promise for the future. Effective use of both technologies requires they be recast as methods for calculating properties of speciflcations, rather than merely verifying them. The most valuable properties are those that contribute to the development of invariants and property-preserving abstractions. We outline an architecture for verification tools based on iterated use of such capabilities. |
Year | DOI | Venue |
|---|---|---|
1999 | 10.1007/3-540-48234-2_1 | SPIN |
Keywords | Field | DocType |
theorem proving,iterated use,mechanized formal method,automated abstraction,valuable property,model checking,verification tool,integrated formal verification,invariant generation,property-preserving abstraction,effective use,formal method,formal verification | Discrete mathematics,Model checking,Programming language,Computer science,Automated theorem proving,Automated proof checking,Automation,Invariant (mathematics),Formal methods,Iterated function,Formal verification | Conference |
Volume | ISSN | ISBN |
1680 | 0302-9743 | 3-540-66499-8 |
Citations | PageRank | References |
17 | 1.00 | 15 |
Authors | ||
1 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| John Rushby | 1 | 2459 | 235.69 |