Back to Search Start Over

Automatic Verification of Annotated Code

Automatic Verification of Annotated Code

Authors :
Hongyang Qu
Doron Peled
Source :
Formal Techniques for Networked and Distributed Systems-FORTE 2003 ISBN: 9783540201755, FORTE
Publication Year :
2003
Publisher :
Springer Berlin Heidelberg, 2003.

Abstract

Model checking is an automatic approach for the verification of systems. Explicit states model checking applies a search algorithm (e.g., depth or breadth first search) to the state space of the verified system. In concurrent systems, and in particular in communication protocols, the number of states can grow exponentially with the number of independent components (processes). There are many different methods that attempt to automatically reduce the number of checked states. Such methods show encouraging results, but often still fail to reduce the number of states required for the verification to become manageable. We propose here the use of code annotation in order to control the verification process and reduce the number of states searched. Our extension of the C programming language allows the user to put into the code instructions that are executed by the model checker during the verification. With the new language construct, we may exploit additional insight that the verifier may have about the checked program in order to limit the search. We describe our implementation and present some experimental results.

Details

ISBN :
978-3-540-20175-5
ISBNs :
9783540201755
Database :
OpenAIRE
Journal :
Formal Techniques for Networked and Distributed Systems-FORTE 2003 ISBN: 9783540201755, FORTE
Accession number :
edsair.doi...........671ce5e17b149d2b457b0276e7c4b71c
Full Text :
https://doi.org/10.1007/978-3-540-39979-7_9