Automated Flaw Detection in Algebraic Specifications

作者：Dunets Andriy^*; Schellhorn Gerhard; Reif Wolfgang

来源：Journal of Automated Reasoning, 2010, 45(4): 359-395.

DOI：10.1007/s10817-010-9166-1

• Algebraic specifications
• Abstract data types
• First-order logic
• Theorem proving
• SAT checking
• Finite models
• Formal methods

In interactive theorem proving practice a significant amount of time is spent on unsuccessful proof attempts of wrong conjectures. An automatic method that reveals them by generating finite counter examples would offer an extremely valuable support or a proof engineer by saving his time and effort. In practice, such counter examples tend to be small, so usually there is no need to search for big instances. Most definitions of functions or predicates on infinite structures do not preserve the semantics if a transition to arbitrary finite substructures is made. We propose constraints which, guarantee a correct axiomatization on finite structures and present an approach which uses the Alloy Analyzer to generate finite instances of theories in the theorem prover KIV. It is evaluated on the library of basic data types as well as on some challenging case studies in KIV. The technique is implemented using the Kodkod constraint solver which is a successor of Alloy.

• 出版日期2010