Automated Specification Analysis Using an Interactive Theorem Prover
Harsh Chamarthi and Panagiotis Manolios.
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.