Exploiting positive equality in a logic of equality with uninterpreted functions

DOI10.1007/3-540-48683-6_40MaRDI QIDQ4818814zbMATH OpenFDO

Authors Randal E. Bryant, Steven M. German, Miroslav N. Velev

Publication date 24 September 2004

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-48683-6_40

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Processor verification using efficient reductions of the logic of uninterpreted functions to propositional logic
• EVC: A validity checker for the logic of equality with uninterpreted functions and memories, exploiting positive equality, and conservative transformations
• Building small equality graphs for deciding equality logic with uninterpreted functions
• BDD based procedures for a theory of equality with uninterpreted functions
• Tools and Algorithms for the Construction and Analysis of Systems

Cited in

(17)

• Word level bitwidth reduction for unbounded hardware model checking
• Algebraic models of correctness for abstract pipelines.
• The small model property: How small can it be?
• BDD based procedures for a theory of equality with uninterpreted functions
• NuMDG: a new tool for multiway decision graphs construction
• Building small equality graphs for deciding equality logic with uninterpreted functions
• Embedded software verification using symbolic execution and uninterpreted functions
• Generalizing DPLL and satisfiability for equalities
• Satisfiability modulo theories
• scientific article; zbMATH DE number 5173450 (Why is no real title available?)
• EVC: A validity checker for the logic of equality with uninterpreted functions and memories, exploiting positive equality, and conservative transformations
• Automatic abstraction of equations in a logic of equality
• Tools and Algorithms for the Construction and Analysis of Systems
• Automated Technology for Verification and Analysis
• Processor verification using efficient reductions of the logic of uninterpreted functions to propositional logic
• Efficient analysis of cyclic redundancy architectures via Boolean fault propagation
• A framework for verifying bit-level pipelined machines based on automated deduction and decision procedures

This page was built for publication: Exploiting positive equality in a logic of equality with uninterpreted functions

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