Specification, abduction, and proof

Konstantine Arkoudas

Paper: ps , pdf

Abstract:

Researchers in formal methods have emphasized the need to make specification analysis as automatic as possible and to provide an array of tools in a uniform setting. Athena is a new interactive proof system that supports specification, structured natural deduction proofs, and trusted tactics. It places heavy emphasis on automation, seamlessly incorporating off-the-shelf state-of-the-art tools for model generation and automated theorem proving. We use a case study of railroad safety to illustrate several aspects of Athena. A formal specification of a railroad system is given in Athena's multi-sorted first-order logic. Automatic model generation is used abductively to develop from scratch a policy for controlling the movement of trains on the tracks. The safety of the policy is proved automatically. Finally, a structured high-level proof of the policys correctness is presented in Athena's natural deduction calculus.

BibTeX Entry

@Inproceedings{ArkoudasATVA2004,
    AUTHOR = {K. Arkoudas},
    TITLE = {Specification, abduction, and proof},
    BOOKTITLE = {Second International Symposium on Automated Technology for Verification and Analysis
    (ATVA 2004)},
    YEAR = {2004},
    SERIES = {Lecture Notes in Computer Science},
    VOLUME = {3299},
    PAGES = {294--309},
    ADDRESS = {Taiwan},
    MONTH = {September},
    YEAR  = {2004},
    PUBLISHER = {Springer-Verlag}}

Back to the publication list of Konstantine Arkoudas