Correctness of Efficient Real-Time Model Checking
Дата
Авторы
Reif,Wolfgang
Schellhorn,Gerhard
Vollmer,Tobias
Ruf,Jürgen
Journal Title
Journal ISSN
Volume Title
Издатель
Journal of Universal Computer Science
Аннотация
Описание
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.
Ключевые слова
model checking , interactive theorem proving , structured algebraic specifications , correctness proofs , program verification , optimization techniques , invariants , temporal logic