DocumentCode
561375
Title
Automated specification analysis using an interactive theorem prover
Author
Chamarthi, Harsh Raju ; Manolios, Panagiotis
Author_Institution
Northeastern Univ., Boston, MA, USA
fYear
2011
fDate
Oct. 30 2011-Nov. 2 2011
Firstpage
46
Lastpage
53
Abstract
A method for analyzing designs and their specifications is presented. The method makes essential use of an interactive theorem prover, but is fully automatic. Given a design and a specification, the method returns one of three possible answers. It can report that the design does not satisfy the specification, in which case a concrete counterexample is provided. It can report that the design does satisfy the specification, in which case a formal proof to that effect is provided. If neither of these cases hold, then a summary of the analysis is reported. We have implemented and experimentally validated the method in ACL2s, the ACL2 Sedan.
Keywords
formal specification; theorem proving; ACL2 Sedan; automated specification analysis; interactive theorem prover; Algorithm design and analysis; Cognition; Educational institutions; Engines; Mechanical factors; Reactive power; Testing;
fLanguage
English
Publisher
ieee
Conference_Titel
Formal Methods in Computer-Aided Design (FMCAD), 2011
Conference_Location
Austin, TX
Print_ISBN
978-1-4673-0896-0
Type
conf
Filename
6148910
Link To Document