| 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: |
|
| 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. |
| To obtain this publication: |
|
|
|
To purchase a printed copy of this publication please contact
MIT
Document Services.
|