LCS Publication Details
Publication Title: On Relational Analysis of Algebraic Datatypes
Publication Author: Kuncak, Viktor
Additional Authors: Daniel Jackson
LCS Document Number: MIT-LCS-TR-985
Publication Date: 4-5-2005
LCS Group: Computer Architecture
Additional URL:
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.
To obtain this publication:

To purchase a printed copy of this publication please contact MIT Document Services.