Loading...
Please wait, while we are loading the content...
Similar Documents
Relational analysis of algebraic datatypes (2005)
| Content Provider | CiteSeerX |
|---|---|
| Author | Kuncak, Viktor Jackson, Daniel |
| 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. 1 |
| File Format | |
| Publisher Date | 2005-01-01 |
| Publisher Institution | In Proceedings of Foundations of Software Egineering |
| Access Restriction | Open |
| Subject Keyword | Finite Structure Relational Analysis Natural Syntactic Class Finite Model Infinite Structure Desired Infinite Model Intended Model Key Idea Relational Logic Finite Model Finding Tool Certain Formula Algebraic Datatypes |
| Content Type | Text |
| Resource Type | Proceeding |
