\textsf{CC(X)}: semantic combination of congruence closure with solvable theories

DOI10.1016/J.ENTCS.2008.04.080MaRDI QIDQ2864404zbMATH OpenOpenAlexFDO

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

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

congruence closuredecision proceduresequality theoryverification

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• Fast congruence closure and extensions
• Congruence closure with free variables
• Term Rewriting and Applications
• Abstract congruence closure
• On Shostak's decision procedure for combinations of theories

Cites work

• Canonization for disjoint unions of theories
• Deciding Combinations of Theories
• Fast congruence closure and extensions
• Fast Decision Procedures Based on Congruence Closure
• scientific article; zbMATH DE number 1798183 (Why is no real title available?)
• Simplification by Cooperating Decision Procedures
• Theoretical Aspects of Computing - ICTAC 2004
• Variations on the Common Subexpression Problem

Cited in

(11)

• Formal analysis of the compact position reporting algorithm
• A formally verified floating-point implementation of the compact position reporting algorithm
• Trusting computations: a mechanized proof from partial differential equations to actual program
• Congruence closure in intensional type theory
• Congruence closure with free variables
• Wave equation numerical resolution: a comprehensive mechanized proof of a C program
• Combining Coq and Gappa for Certifying Floating-Point Programs
• Verification conditions for source-level imperative programs
• Rocket-Fast Proof Checking for SMT Solvers
• Multi-prover verification of floating-point programs
• Provably correct floating-point implementation of a point-in-polygon algorithm

Describes a project that uses

Uses Software

• Alt-Ergo
• OCaml
• SMT-LIB

This page was built for publication: \textsf{CC(X)}: semantic combination of congruence closure with solvable theories

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2864404)