|
eCommons@Cornell >
College of Engineering >
Computer Science >
Computer Science Technical Reports >
Please use this identifier to cite or link to this item:
http://hdl.handle.net/1813/6836
| Title: | Verifying Safety Properties Using Non-deterministic Infinite-state Automata |
| Authors: | Klarlund, Nils
Schneider, Fred B. |
| Keywords: | computer science
technical report |
| Issue Date: | Sep-1989 |
| Publisher: | Cornell University |
| Citation: | http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR89-1036 |
| Abstract: | A new class of infinite-state automata, called safety automata, is introduced. Any safety property can be specified by using such an automaton. Sound and complete proof obligations for establishing that an implementation satisfies the property specified by a safety automaton are given. |
| URI: | http://hdl.handle.net/1813/6836 |
| Appears in Collections: | Computer Science Technical Reports
|
Items in eCommons are protected by copyright, with all rights reserved, unless otherwise indicated.
|
