A proof assistant for symbolic model-checking

J.C. Bradfield

doi:10.1007/3-540-56496-9_25

A proof assistant for symbolic model-checking

Research output: Chapter in Book/Report/Conference proceeding › Conference 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 language	English
Title of host publication	Computer Aided Verification
Subtitle of host publication	Fourth International Workshop, CAV '92 Montreal, Canada, June 29 – July 1, 1992 Proceedings
Editors	Gregor von Bochmann, DavidKarl Probst
Publisher	Springer
Pages	316-329
Number of pages	14
Volume	663
ISBN (Electronic)	978-3-540-47572-9
ISBN (Print)	978-3-540-56496-6
DOIs	https://doi.org/10.1007/3-540-56496-9_25
Publication status	Published - 1993

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer Berlin Heidelberg
Volume	663

Access to Document

10.1007/3-540-56496-9_25

http://dx.doi.org/10.1007/3-540-56496-9_25

Cite this

@inproceedings{e0b988600b284e19b7f18fe0cb730f41,

title = "A proof assistant for symbolic model-checking",

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.",

author = "J.C. Bradfield",

year = "1993",

doi = "10.1007/3-540-56496-9\_25",

language = "English",

isbn = "978-3-540-56496-6",

volume = "663",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "316--329",

editor = "\{von Bochmann\}, Gregor and DavidKarl Probst",

booktitle = "Computer Aided Verification",

address = "United Kingdom",

}

A proof assistant for symbolic model-checking. / Bradfield, J.C.
Computer Aided Verification: Fourth International Workshop, CAV '92 Montreal, Canada, June 29 – July 1, 1992 Proceedings. ed. / Gregor von Bochmann; DavidKarl Probst. Vol. 663 Springer, 1993. p. 316-329 (Lecture Notes in Computer Science; Vol. 663).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - A proof assistant for symbolic model-checking

AU - Bradfield, J.C.

PY - 1993

Y1 - 1993

N2 - 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.

AB - 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.

U2 - 10.1007/3-540-56496-9_25

DO - 10.1007/3-540-56496-9_25

M3 - Conference contribution

SN - 978-3-540-56496-6

VL - 663

T3 - Lecture Notes in Computer Science

SP - 316

EP - 329

BT - Computer Aided Verification

A2 - von Bochmann, Gregor

A2 - Probst, DavidKarl

PB - Springer

ER -

A proof assistant for symbolic model-checking

Abstract

Publication series

Access to Document

Fingerprint

Cite this