The small model property: How small can it be?

DOI10.1016/S0890-5401(02)93175-5zbMath1012.03040OpenAlexW2021915358MaRDI QIDQ1854568

Ofer Strichman, Amir Pnueli, Michael Siegel, Yoav Rodeh

Publication date: 14 January 2003

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/s0890-5401(02)93175-5

Mathematics Subject Classification ID

Graph theory (including graph drawing) in computer science (68R10) Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Decidability of theories and sets of sentences (03B25)

Related Items

Mind the Gap: Bit-vector Interpolation recast over Linear Integer Arithmetic, Formally verified algorithms for upper-bounding state space diameters, Local Search For Satisfiability Modulo Integer Arithmetic Theories, Monotonicity inference for higher-order formulas, Building small equality graphs for deciding equality logic with uninterpreted functions, Unnamed Item, Monotonicity Inference for Higher-Order Formulas, EufDpll - A Tool to Check Satisfiability of Equality Logic Formulas, Word level bitwidth reduction for unbounded hardware model checking, Generating Minimum Transitivity Constraints in P-time for Deciding Equality Logic

Uses Software

• CVT

Cites Work

• Unnamed Item
• Unnamed Item
• The code validation tool (CVT). Automatic verification of a compilation process
• BDD based procedures for a theory of equality with uninterpreted functions
• Solvable cases of the decision problem
• Graph-Based Algorithms for Boolean Function Manipulation
• Processor verification using efficient reductions of the logic of uninterpreted functions to propositional logic