Cesare Tinelli's Publications
Sava Krstić, Amit Goel, Jim Grundy and Cesare Tinelli. Combined Satisfiability Modulo Parametric Theories. Technical report, October 2006.
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.