Verifying Safety Properties Using Non-deterministic Infinite-state Automata

Klarlund, Nils; Schneider, Fred B.

Verifying Safety Properties Using Non-deterministic Infinite-state Automata

File(s)

89-1036.ps (514.68 KB)

89-1036.pdf (2.05 MB)

Permanent Link(s)

https://hdl.handle.net/1813/6836

Collections

Computer Science Technical Reports

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

Keywords

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