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

Full description

Bibliographic Details
Published in:Software engineering notes. 30, 5 (2005).
Main Author: Kuncak, Viktor
Format: Article
Language:English
Subjects: