scientific article; zbMATH DE number 1798182

MaRDI QIDQ4553255zbMATH OpenFDO

Authors Miroslav N. Velev, Randal E. Bryant

Publication date 4 November 2002

Mathematics Subject Classification ID

Computing methodologies and applications (68U99) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical problems of computer architecture (68M07)

Recommendations

• scientific article; zbMATH DE number 2102727
• Processor verification using efficient reductions of the logic of uninterpreted functions to propositional logic
• Artificial Intelligence and Symbolic Computation
• Tools and Algorithms for the Construction and Analysis of Systems
• Building small equality graphs for deciding equality logic with uninterpreted functions

Cited in

(8)

• Processor verification using efficient reductions of the logic of uninterpreted functions to propositional logic
• Automated Technology for Verification and Analysis
• scientific article; zbMATH DE number 2102727 (Why is no real title available?)
• EVC
• Building small equality graphs for deciding equality logic with uninterpreted functions
• Effective use of Boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors.
• Producing and verifying extremely large propositional refutations
• Tools and Algorithms for the Construction and Analysis of Systems

Describes a project that uses

Uses Software

• PVS
• CUDD
• Chaff
• Velev SAT Benchmarks

This page was built for publication:

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