00000cab a22000003a 4500 UP-99796217608835179 Buklod 20231007234838.0 m |o d | ta 090514s xx d | ||r ||||| || DENGII eng Kuncak, Viktor Relational analysis of algebraic datatypes. pp. 25 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. Software. Software engineering. Software / Program Verification. Model checking. Formal methods. Theory of computation. Logics and meanings of programs. Specifying and Verifying and Reasoning about Programs. Logics of programs. Mechanical verification. Specification techniques. Design. Reliability. Theory. Verification. Algebraic datatypes. Constraint solving. Model checking. Model finding. Transitive closure logic. Software engineering notes. 30, 5 (2005). FO UPD DENG-II Article