The Library
Automatic verification of annotated code
Tools
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. ISBN 3-540-20175-0. ISSN 0302-9743.
Research output not available from this repository.
Request-a-Copy directly from author or use local Library Get it For Me service.
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 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 | ||||
Publisher: | SPRINGER-VERLAG BERLIN | ||||
ISBN: | 3-540-20175-0 | ||||
ISSN: | 0302-9743 | ||||
Editor: | Konig, H and Heiner, M and Wolisz, A | ||||
Official Date: | 2003 | ||||
Dates: |
|
||||
Volume: | 2767 | ||||
Number of Pages: | 17 | ||||
Page Range: | pp. 127-143 | ||||
Publication Status: | Published | ||||
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 |
Data sourced from Thomson Reuters' Web of Knowledge
Request changes or add full text files to a record
Repository staff actions (login required)
View Item |