A proof assistant for symbolic model-checking

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

We describe a prototype of a tool to assist in the model-checking of infinite systems by a tableau-based method. The tool automatically applies those tableau rules that require no user intervention, and checks the correctness of user-applied rules. It also provides help with checking the well-foundedness conditions required to prove liveness properties. The tool has a general tableau-manager module, and may use different reasoning modules for different models of systems; a module for Petri nets has been implemented.
Original languageEnglish
Title of host publicationComputer Aided Verification
Subtitle of host publicationFourth International Workshop, CAV '92 Montreal, Canada, June 29 – July 1, 1992 Proceedings
EditorsGregor von Bochmann, DavidKarl Probst
PublisherSpringer Berlin Heidelberg
Pages316-329
Number of pages14
Volume663
ISBN (Electronic)978-3-540-47572-9
ISBN (Print)978-3-540-56496-6
DOIs
Publication statusPublished - 1993

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg
Volume663

Fingerprint Dive into the research topics of 'A proof assistant for symbolic model-checking'. Together they form a unique fingerprint.

Cite this