Paper Info
Title
Specification, Abduction, and Proof
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 policy's correctness is presented in Athena's natural deduction calculus.
Year
DOI
Venue
2004
10.1007/978-3-540-30476-0_25
Lecture Notes in Computer Science
Keywords
Field
DocType
natural deduction,formal method,formal specification,first order logic,automated theorem proving
Programming language,Natural deduction,Computer science,Automated theorem proving,Correctness,Proof theory,Theoretical computer science,Formal specification,First-order logic,Mathematical proof,Artificial intelligence,Formal methods
Conference
Volume
ISSN
Citations 
3299
0302-9743
6
PageRank 
References 
Authors
0.62
11
1
Name
Order
Citations
PageRank
Konstantine Arkoudas118619.63