Cesare Tinelli's Publications

Sava Krstić, Amit Goel, Jim Grundy and Cesare Tinelli. Combined Satisfiability Modulo Parametric Theories. In Proceedings of the 13th Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'07), Braga, Portugal, 2007.

Abstract. We give a fresh theoretical foundation for designing comprehensive SMT solvers, generalizing in a practically motivated direction. We define parametric theories that most appropriately express the "logic" of common data types. Our main result is a combination theorem for decision procedures for disjoint theories of this kind. Virtually all of the deeply nested data structures (lists of arrays of sets of ...) that arise in verification work are covered.