On Relational Analysis of Algebraic Datatypes

We present a technique that enables the use of finite modelfinding to check the satisfiability of certain formulaswhose intended models are infinite. Such formulas arisewhen using the language of sets and relations to reasonabout structured values such as algebraic datatypes. Thekey idea of our te...

Full description

Bibliographic Details
Main Authors: Kuncak, Viktor, Jackson, Daniel
Other Authors: Computer Architecture
Language:en_US
Published: 2005
Online Access:http://hdl.handle.net/1721.1/30534