Name
Abstract | ||
|---|---|---|
In this paper we describe the formal specification and verification of an efficient algorithm based on bitvectors for real-time model checking with the KIV system. We demonstrate that the verification captures the essentials of the C++ algorithm as implemented in the RAVEN model checker. Verification revealed several possibilities to reduce the size of the code and to improve its efficiency. |
Year | Venue | Keywords |
|---|---|---|
2001 | JOURNAL OF UNIVERSAL COMPUTER SCIENCE | model checking,interactive theorem proving,structured algebraic specifications,correctness proofs,program verification,optimization techniques,invariants,temporal logic |
Field | DocType | Volume |
Data mining,Abstraction model checking,Real time model,Model checking,Programming language,Computer science,Correctness,Automated proof checking,Symbolic trajectory evaluation | Journal | 7 |
Issue | ISSN | Citations |
2 | 0948-695X | 2 |
PageRank | References | Authors |
0.41 | 0 | 4 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Wolfgang Reif | 1 | 915 | 95.46 |
| Gerhard Schellhorn | 2 | 769 | 56.43 |
| Tobias Vollmer | 3 | 5 | 0.84 |
| Jürgen Ruf | 4 | 122 | 23.04 |