| 2023 | IFM | Automatic Formal Verification of RISC-V Pipelined Microprocessors with Fault Tolerance by Spatial Redundancy at a High Level of Abstraction. | Miroslav N. Velev |
| 2018 | ISAIM | Survey of Techniques for Efficient Solving of Boolean Formulas from Formal Verification of Pipelined, Superscalar, and VLIW Microprocessors at a High Level of Abstraction. | Miroslav N. Velev |
| 2016 | ISAIM | Application of Hierarchical Hybrid Encodings to Solve CSPs as Equivalent SAT Problems. | Miroslav N. Velev, Ping Gao |
| 2014 | ASPDAC | Efficient parallel GPU algorithms for BDD manipulation. | Miroslav N. Velev, Ping Gao |
| 2014 | ICCAD | Improving the efficiency of automated debugging of pipelined microprocessors by symmetry breaking in modular schemes for boolean encoding of cardinality. | Miroslav N. Velev, Ping Gao |
| 2013 | ICTAI | Application of Hierarchical Hybrid Encodings to Efficient Translation of CSPs to SAT. | Van-Hau Nguyen, Miroslav N. Velev, Pedro Barahona |
| 2012 | ASPDAC | Automated debugging of counterexamples in formal verification of pipelined microprocessors. | Miroslav N. Velev, Ping Gao |
| 2011 | ASPDAC | Automatic formal verification of reconfigurable DSPs. | Miroslav N. Velev, Ping Gao |
| 2011 | ICCAD | Automatic formal verification of multithreaded pipelined microprocessors. | Miroslav N. Velev, Ping Gao |
| 2011 | ICFEM | Exploiting Abstraction for Efficient Formal Verification of DSPs with Arrays of Reconfigurable Functional Units. | Miroslav N. Velev, Ping Gao |
| 2011 | ISCAS | CNF encodings of cardinality in formal methods for robustness checking of gate-level circuits. | Miroslav N. Velev, Ping Gao |
| 2010 | ASPDAC | A method for debugging of pipelined processors in formal verification by correspondence checking. | Miroslav N. Velev, Ping Gao |
| 2010 | ICFEM | Method for Formal Verification of Soft-Error Tolerance Mechanisms in Pipelined Microprocessors. | Miroslav N. Velev, Ping Gao |
| 2010 | ISAIM | Design of parallel portfolios for SAT-based solving of Hamiltonian cycle problems. | Miroslav N. Velev, Ping Gao |
| 2008 | DATE | Comparison of Boolean Satisfiability Encodings on FPGA Detailed Routing Problems. | Miroslav N. Velev, Ping Gao |
| 2007 | ICCAD | Exploiting hierarchy and structure to efficiently solve graph coloring as SAT. | Miroslav N. Velev |
| 2005 | ASPDAC | Comparison of schemes for encoding unobservability in translation to SAT. | Miroslav N. Velev |
| 2004 | ASPDAC | Efficient translation of boolean formulas to CNF in formal verification of microprocessors. | Miroslav N. Velev |
| 2004 | ASPDAC | Using positive equality to prove liveness for pipelined microprocessors. | Miroslav N. Velev |
| 2004 | DATE | Exploiting Signal Unobservability for Efficient Translation to CNF in Formal Verification of Microprocessors. | Miroslav N. Velev |
| 2004 | ICCD | Comparative Study of Strategies for Formal Verification of High-Level Processors. | Miroslav N. Velev |
| 2004 | ISAIM | Using Automatic Case Splits and Efficient CNF Translation to Guide a SAT-solver when Formally Verifying Out-Of-Order Processors. | Miroslav N. Velev |
| 2004 | ISCAS | A new generation of ISCAS benchmarks from formal verification of high-level microprocessors. | Miroslav N. Velev |
| 2004 | SAT | Encoding Global Unobservability for Efficient Translation to SAT. | Miroslav N. Velev |
| 2003 | ITC | Collection of High-Level Microprocessor Bugs from Formal Verification of Pipelined and Superscalar Designs. | Miroslav N. Velev |
| 2003 | MEMOCODE | Formal Verification of an Intel XScale Processor Model with Scoreboarding, Specialized Execution Pipelines, and Impress Data-Memory Exceptions. | Sudarshan K. Srinivasan, Miroslav N. Velev |
| 2003 | TABLEAUX | Automatic Abstraction of Equations in a Logic of Equality. | Miroslav N. Velev |
| 2002 | DATE | Using Rewriting Rules and Positive Equality to Formally Verify Wide-Issue Out-of-Order Microprocessors with a Reorder Buffer. | Miroslav N. Velev |
| 2001 | CAV | EVC: A Validity Checker for the Logic of Equality with Uninterpreted Functions and Memories, Exploiting Positive Equality, and Conservative Transformations. | Miroslav N. Velev, Randal E. Bryant |
| 2001 | DAC | Effective Use of Boolean Satisfiability Procedures in the Formal Verification of Superscalar and VLIW Microprocessors. | Miroslav N. Velev, Randal E. Bryant |
| 2001 | TACAS | Automatic Abstraction of Memories in the Formal Verification of Superscalar Microprocessors. | Miroslav N. Velev |
| 2000 | CAV | Boolean Satisfiability with Transitivity Constraints. | Randal E. Bryant, Miroslav N. Velev |
| 2000 | CAV | Formal Verification of VLIW Microprocessors with Speculative Execution. | Miroslav N. Velev |
| 2000 | DAC | Formal verification of superscale microprocessors with multicycle functional units, exception, and branch prediction. | Miroslav N. Velev, Randal E. Bryant |
| 1999 | CAV | Exploiting Positive Equality in a Logic of Equality with Uninterpreted Functions. | Randal E. Bryant, Steven M. German, Miroslav N. Velev |
| 1999 | DAC | Exploiting Positive Equality and Partial Non-Consistency in the Formal Verification of Pipelined Microprocessors. | Miroslav N. Velev, Randal E. Bryant |
| 1999 | TABLEAUX | Microprocessor Verification Using Efficient Decision Procedures for a Logic of Equality with Uninterpreted Functions. | Randal E. Bryant, Steven M. German, Miroslav N. Velev |
| 1998 | FMCAD | Bit-Level Abstraction in the Verfication of Pipelined Microprocessors by Correspondence Checking. | Miroslav N. Velev, Randal E. Bryant |
| 1998 | ICCD | Incorporating timing constraints in the efficient memory model for symbolic ternary simulation. | Miroslav N. Velev, Randal E. Bryant |
| 1998 | TACAS | Efficient Modeling of Memory Arrays in Symbolic Ternary Simulation. | Miroslav N. Velev, Randal E. Bryant |
| 1997 | CAV | Efficient Modeling of Memory Arrays in Symbolic Simulation. | Miroslav N. Velev, Randal E. Bryant, Alok Jain |