Computing All Implied Equalities via SMT-Based Partition Refinement

DOI10.1007/978-3-319-08587-6_12zbMath1423.68408OpenAlexW97129115MaRDI QIDQ3192188

Josh Berdine, Nikolaj Bjørner

Publication date: 26 September 2014

Published in: Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-08587-6_12

zbMATH Keywords

software verificationsatisfiability modulo theoriesdecision procedurescongruence closureconsequence findingimplied equalities

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Related Items (2)

Symbolic computation of differential equivalences ⋮ Quantitative Abstractions for Collective Adaptive Systems

This page was built for publication: Computing All Implied Equalities via SMT-Based Partition Refinement