Verification of Pipelined Microprocessors by Comparing Memory Execution Sequences in Symbolic Simulation. - Randal E. Bryant; Miroslav N. Velev (ASIAN, 1997)

Efficient Modeling of Memory Arrays in Symbolic Simulation. - Miroslav N. Velev; Randal E. Bryant; Alok Jain (CAV, 1997)

Verification of Pipelined Microprocessors by Correspondence Checking in Symbolic Ternary Simulation. - Miroslav N. Velev; Randal E. Bryant (ACSD, 1998)

Bit-Level Abstraction in the Verfication of Pipelined Microprocessors by Correspondence Checking. - Miroslav N. Velev; Randal E. Bryant (FMCAD, 1998)

Incorporating timing constraints in the efficient memory model for symbolic ternary simulation. - Miroslav N. Velev; Randal E. Bryant (ICCD, 1998)

Efficient Modeling of Memory Arrays in Symbolic Ternary Simulation. - Miroslav N. Velev; Randal E. Bryant (TACAS, 1998)

Exploiting Positive Equality in a Logic of Equality with Uninterpreted Functions. - Randal E. Bryant; Steven M. German; Miroslav N. Velev (CAV, 1999)

Superscalar Processor Verification Using Efficient Reductions of the Logic of Equality with Uninterpreted Functions to Propositional Logic. - Miroslav N. Velev; Randal E. Bryant (CHARME, 1999)

Exploiting Positive Equality and Partial Non-Consistency in the Formal Verification of Pipelined Microprocessors. - Miroslav N. Velev; Randal E. Bryant (DAC, 1999)

Microprocessor Verification Using Efficient Decision Procedures for a Logic of Equality with Uninterpreted Functions. - Randal E. Bryant; Steven M. German; Miroslav N. Velev (TABLEAUX, 1999)

Formal Verification of VLIW Microprocessors with Speculative Execution. - Miroslav N. Velev (CAV, 2000)

Formal verification of superscale microprocessors with multicycle functional units, exception, and branch prediction. - Miroslav N. Velev; Randal E. Bryant (DAC, 2000)

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 (CAV, 2001)

Automatic Abstraction of Memories in the Formal Verification of Superscalar Microprocessors. - Miroslav N. Velev (TACAS, 2001)

Processor verification using efficient reductions of the logic of uninterpreted functions to propositional logic. - Randal E. Bryant; Steven M. German; Miroslav N. Velev (ACM Trans. Comput. Log., 2001)

Using Rewriting Rules and Positive Equality to Formally Verify Wide-Issue Out-of-Order Microprocessors with a Reorder Buffer. - Miroslav N. Velev (DATE, 2002)

Boolean satisfiability with transitivity constraints. - Randal E. Bryant; Miroslav N. Velev (ACM Trans. Comput. Log., 2002)

Collection of High-Level Microprocessor Bugs from Formal Verification of Pipelined and Superscalar Designs. - Miroslav N. Velev (ITC, 2003)

Formal Verification of an Intel XScale Processor Model with Scoreboarding, Specialized Execution Pipelines, and Impress Data-Memory Exceptions. - Sudarshan K. Srinivasan; Miroslav N. Velev (MEMOCODE, 2003)

Automatic Abstraction of Equations in a Logic of Equality. - Miroslav N. Velev (TABLEAUX, 2003)

Effective use of Boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors. - Miroslav N. Velev; Randal E. Bryant (J. Symb. Comput., 2003)

Efficient translation of boolean formulas to CNF in formal verification of microprocessors. - Miroslav N. Velev (ASP-DAC, 2004)

Using positive equality to prove liveness for pipelined microprocessors. - Miroslav N. Velev (ASP-DAC, 2004)

Exploiting Signal Unobservability for Efficient Translation to CNF in Formal Verification of Microprocessors. - Miroslav N. Velev (DATE, 2004)

Efficient formal verification of pipelined processors with instruction queues. - Miroslav N. Velev (ACM Great Lakes Symposium on VLSI, 2004)

Formal verification of pipelined processors with load-value prediction. - Miroslav N. Velev (HLDVT, 2004)

Comparative Study of Strategies for Formal Verification of High-Level Processors. - Miroslav N. Velev (ICCD, 2004)

Using Automatic Case Splits and Efficient CNF Translation to Guide a SAT-solver when Formally Verifying Out-Of-Order Processors. - Miroslav N. Velev (AI&M, 2004)

A new generation of ISCAS benchmarks from formal verification of high-level microprocessors. - Miroslav N. Velev (ISCAS (5), 2004)

Encoding Global Unobservability for Efficient Translation to SAT. - Miroslav N. Velev (SAT, 2004)

Tuning SAT for Formal Verification and Testing. - Miroslav N. Velev (J. Univers. Comput. Sci., 2004)

Comparison of schemes for encoding unobservability in translation to SAT. - Miroslav N. Velev (ASP-DAC, 2005)

Automatic Formal Verification of Liveness for Pipelined Processors with Multicycle Functional Units. - Miroslav N. Velev (CHARME, 2005)

TLSim and EVC: a term-level symbolic simulator and an efficient decision procedure for the logic of equality with uninterpreted functions and memories. - Miroslav N. Velev; Randal E. Bryant (Int. J. Embed. Syst., 2005)

Integrating formal verification into an advanced computer architecture course. - Miroslav N. Velev (IEEE Trans. Educ., 2005)

Using Abstraction for Efficient Formal Verification of Pipelined Processors with Value Prediction. - Miroslav N. Velev (ISQED, 2006)

Formal Verification of Pipelined Microprocessors with Delayed Branches. - Miroslav N. Velev (ISQED, 2006)

Exploiting hierarchy and structure to efficiently solve graph coloring as SAT. - Miroslav N. Velev (ICCAD, 2007)

Comparison of Boolean Satisfiability Encodings on FPGA Detailed Routing Problems. - Miroslav N. Velev; Ping Gao 002 (DATE, 2008)

Editor's Introduction to the Special Volume on Application of Constraints to Formal Verification. - Miroslav N. Velev (J. Satisf. Boolean Model. Comput., 2008)

Efficient SAT Techniques for Relative Encoding of Permutations with Constraints. - Miroslav N. Velev; Ping Gao 002 (Australasian Conference on Artificial Intelligence, 2009)

Exploiting hierarchical encodings of equality to design independent strategies in parallel SMT decision procedures for a logic of equality. - Miroslav N. Velev; Ping Gao 002 (HLDVT, 2009)

Efficient SAT-based techniques for Design of Experiments by using static variable ordering. - Miroslav N. Velev; Ping Gao 002 (ISQED, 2009)

Efficient SAT Techniques for Absolute Encoding of Permutation Problems: Application to Hamiltonian Cycles. - Miroslav N. Velev; Ping Gao 002 (SARA, 2009)

A method for debugging of pipelined processors in formal verification by correspondence checking. - Miroslav N. Velev; Ping Gao 002 (ASP-DAC, 2010)

Method for Formal Verification of Soft-Error Tolerance Mechanisms in Pipelined Microprocessors. - Miroslav N. Velev; Ping Gao 002 (ICFEM, 2010)

Design of parallel portfolios for SAT-based solving of Hamiltonian cycle problems. - Miroslav N. Velev; Ping Gao 002 (ISAIM, 2010)

Automatic formal verification of reconfigurable DSPs. - Miroslav N. Velev; Ping Gao 002 (ASP-DAC, 2011)

Automatic formal verification of multithreaded pipelined microprocessors. - Miroslav N. Velev; Ping Gao 002 (ICCAD, 2011)

Exploiting Abstraction for Efficient Formal Verification of DSPs with Arrays of Reconfigurable Functional Units. - Miroslav N. Velev; Ping Gao 002 (ICFEM, 2011)

CNF encodings of cardinality in formal methods for robustness checking of gate-level circuits. - Miroslav N. Velev; Ping Gao 002 (ISCAS, 2011)

Efficient Pseudo-Boolean Satisfiability Encodings for Routing and Wavelength Assignment in Optical Networks. - Miroslav N. Velev; Ping Gao 002 (SARA, 2011)

Modular Schemes for Constructing Equivalent Boolean Encodings of Cardinality Constraints and Application to Error Diagnosis in Formal Verification of Pipelined Microprocessors. - Miroslav N. Velev; Ping Gao 002 (SARA, 2011)

Automated debugging of counterexamples in formal verification of pipelined microprocessors. - Miroslav N. Velev; Ping Gao 002 (ASP-DAC, 2012)

Application of Hierarchical Hybrid Encodings to Efficient Translation of CSPs to SAT. - Van-Hau Nguyen; Miroslav N. Velev; Pedro Barahona (ICTAI, 2013)

Efficient parallel GPU algorithms for BDD manipulation. - Miroslav N. Velev; Ping Gao 002 (ASP-DAC, 2014)

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 002 (ICCAD, 2014)

Formal verification of safety of polymorphic heterogeneous multi-core architectures. - Miroslav N. Velev; Ping Gao 002 (ISQED, 2014)

Application of constraints to formal verification and artificial intelligence. - Miroslav N. Velev; John V. Franco (Ann. Math. Artif. Intell., 2014)

Exploiting abstraction, learning from random simulation, and SVM classification for efficient dynamic prediction of software health problems. - Miroslav N. Velev; Chaoqiang Zhang; Ping Gao 002; Alex David Groce (ISQED, 2015)

Welcome Message. - Prab Varma; Miroslav N. Velev (HLDVT, 2016)

Application of Hierarchical Hybrid Encodings to Solve CSPs as Equivalent SAT Problems. - Miroslav N. Velev; Ping Gao 002 (ISAIM, 2016)

Editorial. - Krishnendu Chakrabarty; Massimo Alioto; Bevan M. Baas; Chirn Chye Boon; Meng-Fan Chang; Naehyuck Chang; Yao-Wen Chang; Chip-Hong Chang; Shih-Chieh Chang; Poki Chen; Masud H. Chowdhury; Pasquale Corsonello; et al. (IEEE Trans. Very Large Scale Integr. Syst., 2017)

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 (ISAIM, 2018)

Automatic Formal Verification of RISC-V Pipelined Microprocessors with Fault Tolerance by Spatial Redundancy at a High Level of Abstraction. - Miroslav N. Velev (iFM, 2023)