Name
Abstract | ||
|---|---|---|
In this paper we describe the formal specification and veri fication of the efficient algorithm for real-time model checking implemented in the model checker RAVEN. It was specified and proved using the KIV system. We demonstrate how to decompose the correctness proof into several independent subtasks and indicate the corresponding verification efforts. The formal verification revealed some errors, reduced the code size, and improved the efficiency of the implementation. |
Year | Venue | Keywords |
|---|---|---|
2000 | FMCAD | model checker,corresponding verification effort,real-time model checking,formal specification,model checker raven,independent subtasks,code size,efficient algorithm,kiv system,correctness proof,formal verification,model checking,real time |
Field | DocType | Volume |
Correctness proofs,Programming language,Model checking,Code size,Computer science,Formal specification,Theoretical computer science,Proof obligation,Formal verification | Conference | 1954 |
ISSN | ISBN | Citations |
0302-9743 | 3-540-41219-0 | 3 |
PageRank | References | Authors |
0.43 | 7 | 4 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Wolfgang Reif | 1 | 915 | 95.46 |
| Jürgen Ruf | 2 | 122 | 23.04 |
| Gerhard Schellhorn | 3 | 769 | 56.43 |
| Tobias Vollmer | 4 | 5 | 0.84 |