paper ps
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.

### Citation

Viktor Kuncak and Daniel Jackson.
Relational analysis of algebraic datatypes.
In *10th European Soft. Eng. Conf. (ESEC) and 13th Symp.
Foundations of Software Engineering (FSE)*, 2005.
See [43] for
full version.### BibTex Entry

@inproceedings{KuncakJackson05RelationalAnalysisAlgebraicDatatypes,
author = {Viktor Kuncak and Daniel Jackson},
title = {Relational Analysis of Algebraic Datatypes},
booktitle = {10th European Soft. Eng. Conf. (ESEC) and 13th
Symp. Foundations of Software Engineering (FSE)},
year = 2005,
note = {See \cite{KuncakJackson05OnRelationalAnalysisAlgebraicDatatypes}
for full version.},
abstract = {
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.
}
}