Verifying Safety Properties Using Non-deterministic Infinite-state Automata

Thumbnail
View/Open
PERMANENT LINK(S)
http://hdl.handle.net/1813/6836
Collections
Metadata
Show full item record
Author
Klarlund, Nils; Schneider, Fred B.
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.
Date Issued
1989-09
Publisher
Cornell University
Subject
computer science; technical report
Previously Published As
http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR89-1036
Type
Technical Report

Statistics