Panagiotis (Pete) Manolios
College of Computer and Information Science
Northeastern University

Automated Specification Analysis Using an Interactive Theorem Prover

Harsh Chamarthi and Panagiotis Manolios.
FMCAD, 2011.

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.

PDF