Relational analysis of algebraic datatypes

We present a technique that enables the use of finite model finding to check the satisfiability of certain formulas whose intended models are infinite. Such formulas arise when using the language of sets and relations to reason about structured values such as algebraic datatypes. The key idea of our technique is to identify a natural syntactic class of formulas in relational logic for which reasoning about infinite structures can be reduced to reasoning about finite structures. As a result, when a formula belongs to this class, we can use existing finite model finding tools to check whether the formula holds in the desired infinite model. Categories and Subject Descriptors D.2.4 [Software Engineering]: Software/Program Verification--model checking, formal methods; F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs--logics of programs, mechanical verification, specification techniques General Terms Design, Reliability, Theory, Verification Ke...

• Type: Conference
• Year: 2005
• Where: SIGSOFT
• Authors: Viktor Kuncak, Daniel Jackson
• Keywords: Finite Model, Model Finding Tools, SIGSOFT 2005, Software Engineering, Verification Keywords Model