The Library
A counterexample-guided refinement tool for open procedural programs
Tools
Tools
Tools
UNSPECIFIED (2006) A counterexample-guided refinement tool for open procedural programs. In: 13th International SPIN Workshop on Model Checking Software, MAR 30-APR 01, 2006, Vienna, AUSTRIA.
Full text not available from this repository.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 |
| Date: | 2006 |
| 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 |
| URI: | http://wrap.warwick.ac.uk/id/eprint/33577 |
Data sourced from Thomson Reuters' Web of Knowledge
Actions (login required)
 |
View Item |
