Finding bugs in an alpha microprocessor using satisfiability solvers

DOI10.1007/3-540-44585-4_44MaRDI QIDQ4553262zbMATH OpenFDO

Authors Per Bjesse, Tim Leonard, Abdel Mokkedem

Publication date 4 November 2002

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

Full work available at URL https://doi.org/10.1007/3-540-44585-4_44

Mathematics Subject Classification ID

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

Recommendations

• Industrial model checking based on satisfiability solvers
• Bounded model checking using satisfiability solving
• Symbolic reachability analysis based on SAT-solvers
• Effective use of Boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors.
• scientific article; zbMATH DE number 5605058

Cited in

(20)

• Effective use of Boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors.
• A formal methods approach to predicting new features of the eukaryotic vesicle traffic system
• A taxonomy of exact methods for partial Max-SAT
• Complete Boolean satisfiability solving algorithms based on local search
• Backdoors to q-Horn
• The state of SAT
• A semantic condition for data independence and applications in hardware verification
• Quantifier reordering for QBF
• Backdoors to satisfaction
• 3-Valued Circuit SAT for STE with Automatic Refinement
• An automata-theoretic approach to infinite-state systems
• A transformation-based approach to implication of GSTE assertion graphs
• scientific article; zbMATH DE number 1324661 (Why is no real title available?)
• Benchmarking a model checker for algorithmic improvements and tuning for performance
• Scalable error detection using Boolean satisfiability
• SCIP: solving constraint integer programs
• Unrestricted vs restricted cut in a tableau method for Boolean circuits
• SAT-solving in practice, with a tutorial example from supervisory control
• Design and results of the first satisfiability modulo theories competition (SMT-COMP 2005)
• Soundness of \(\mathcal{Q}\)-resolution with dependency schemes

Describes a project that uses

Uses Software

• Cadence SMV

This page was built for publication: Finding bugs in an alpha microprocessor using satisfiability solvers

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