Automatic verification of annotated code
UNSPECIFIED (2003) Automatic verification of annotated code. In: 23rd International Conference on Formal Techniques for Networked and Distributed Systems, BERLIN, GERMANY, SEP 29-OCT 02, 2003. Published in: FORMAL TECHNIQUES FOR NETWORKED AND DISTRIBUTED SYSTEMS - FORTE 2003, 2767 pp. 127-143.Full text not available from this repository.
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 axe 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.
|Item Type:||Conference Item (UNSPECIFIED)|
|Subjects:||Q Science > QA Mathematics > QA76 Electronic computers. Computer science. Computer software|
|Series Name:||LECTURE NOTES IN COMPUTER SCIENCE|
|Journal or Publication Title:||FORMAL TECHNIQUES FOR NETWORKED AND DISTRIBUTED SYSTEMS - FORTE 2003|
|Editor:||Konig, H and Heiner, M and Wolisz, A|
|Number of Pages:||17|
|Page Range:||pp. 127-143|
|Title of Event:||23rd International Conference on Formal Techniques for Networked and Distributed Systems|
|Location of Event:||BERLIN, GERMANY|
|Date(s) of Event:||SEP 29-OCT 02, 2003|
Actions (login required)