CC(X): Semantic Combination of Congruence Closure with Solvable Theories

DOI10.1016/j.entcs.2008.04.080zbMath1277.68240OpenAlexW2151546473MaRDI QIDQ2864404

Sylvain Conchon, Evelyne Contejean, Stéphane Lescuyer, Johannes Kanig

Publication date: 6 December 2013

Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.entcs.2008.04.080

zbMATH Keywords

verificationdecision procedurescongruence closureequality theory

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items

Wave equation numerical resolution: a comprehensive mechanized proof of a C program, Trusting computations: a mechanized proof from partial differential equations to actual program, Verification conditions for source-level imperative programs, Formal analysis of the compact position reporting algorithm, Multi-Prover Verification of Floating-Point Programs, A formally verified floating-point implementation of the compact position reporting algorithm, Rocket-Fast Proof Checking for SMT Solvers, Combining Coq and Gappa for Certifying Floating-Point Programs

Uses Software

• SMT-LIB
• Alt-Ergo
• OCaml

Cites Work

• Unnamed Item
• Fast congruence closure and extensions
• Canonization for disjoint unions of theories
• Deciding Combinations of Theories
• Fast Decision Procedures Based on Congruence Closure
• Simplification by Cooperating Decision Procedures
• Variations on the Common Subexpression Problem
• Theoretical Aspects of Computing - ICTAC 2004