The Library
A counterexample-guided refinement tool for open procedural programs
Tools
UNSPECIFIED (2006) A counterexample-guided refinement tool for open procedural programs. In: 13th International SPIN Workshop on Model Checking Software, Vienna, AUSTRIA, MAR 30-APR 01, 2006. Published in: MODEL CHECKING SOFTWARE, PROCEEDINGS, 3925 pp. 288-292. ISBN 3-540-33102-6. 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
We present a model checking tool based on game semantics and CSP for verifying safety properties of software, such as assertion violations or array-out-of-bounds errors. The tool implements a data-abstraction refinement procedure applicable to open programs with infinite integer types. The procedure is guaranteed to terminate for unsafe inputs.
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: | MODEL CHECKING SOFTWARE, PROCEEDINGS | ||||
Publisher: | SPRINGER-VERLAG BERLIN | ||||
ISBN: | 3-540-33102-6 | ||||
ISSN: | 0302-9743 | ||||
Editor: | Valmari, A | ||||
Official Date: | 2006 | ||||
Dates: |
|
||||
Volume: | 3925 | ||||
Number of Pages: | 5 | ||||
Page Range: | pp. 288-292 | ||||
Publication Status: | Published | ||||
Title of Event: | 13th International SPIN Workshop on Model Checking Software | ||||
Location of Event: | Vienna, AUSTRIA | ||||
Date(s) of Event: | MAR 30-APR 01, 2006 |
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 |