Combined Satisfiability Modulo Parametric Theories

Sava Krstić; Amit Goel; Jim Grundy; Cesare Tinelli

doi:10.1007/978-3-540-71209-1_47

Back

Combined Satisfiability Modulo Parametric Theories

Book chapter

Open access

Peer reviewed

Combined Satisfiability Modulo Parametric Theories

Sava Krstić, Amit Goel, Jim Grundy and Cesare Tinelli

Tools and Algorithms for the Construction and Analysis of Systems, pp.602-617

Lecture Notes in Computer Science, Springer Berlin Heidelberg

2007

DOI: 10.1007/978-3-540-71209-1_47

Files and links (1)

url

https://doi.org/10.1007/978-3-540-71209-1_47View

Published (Version of record) Open Access

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.

Atomic Formula

Cardinality Constraint

Decision Procedure

Proof Assistant

Type Operator

Details

Title: Subtitle: Combined Satisfiability Modulo Parametric Theories
Creators: Sava Krstić - Intel (United States)
Amit Goel - Intel (United States)
Jim Grundy - Intel (United States)
Cesare Tinelli - University of Iowa
Resource Type: Book chapter
Publication Details: Tools and Algorithms for the Construction and Analysis of Systems, pp.602-617
Series: Lecture Notes in Computer Science
DOI: 10.1007/978-3-540-71209-1_47
eISSN: 1611-3349
ISSN: 0302-9743
Publisher: Springer Berlin Heidelberg; Berlin, Heidelberg
Language: English
Date published: 2007
Academic Unit: Computer Science
Record Identifier: 9984259419002771

Metrics

24 Record Views