Validating SMT solvers via semantic fusion
Dominik Winterer, Chengyu Zhang, Zhendong Su
Abstract
We introduce Semantic Fusion, a general, effective methodology for validating Satisfiability Modulo Theory (SMT) solvers. Our key idea is to fuse two existing equisatisfiable (i.e., both satisfiable or unsatisfiable) formulas into a new formula that combines the structures of its ancestors in a novel manner and preserves the satisfiability by construction. This fused formula is then used for validating SMT solvers.
Topics & Concepts
Satisfiability modulo theoriesComputer scienceSatisfiabilityKey (lock)ModuloFuse (electrical)Theoretical computer scienceProgramming languageFormal verificationSemantics (computer science)AlgorithmDiscrete mathematicsMathematicsComputer securityElectrical engineeringEngineeringSoftware Testing and Debugging TechniquesFormal Methods in VerificationSoftware Reliability and Analysis Research