Miroslav N. Velev

Publication Activity (10 Years)

Years Active: 1997-2023
Publications (10 Years): 5

Top Topics

Symmetry Breaking

Boolean Formula

Formal Verification

Top Venues

Ann. Math. Artif. Intell.

Publications

Miroslav N. Velev
Automatic Formal Verification of RISC-V Pipelined Microprocessors with Fault Tolerance by Spatial Redundancy at a High Level of Abstraction. iFM (2023)
Miroslav N. Velev
Survey of Techniques for Efficient Solving of Boolean Formulas from Formal Verification of Pipelined, Superscalar, and VLIW Microprocessors at a High Level of Abstraction. ISAIM (2018)
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, Ibrahim Abe M. Elfadel, Said Hamdioui, Masanori Hashimoto, Tsung-Yi Ho, Houman Homayoun, Yuh-Shyan Hwang, Rajiv V. Joshi, Tanay Karnik, Mehran Mozaffari Kermani, Chulwoo Kim, Tae-Hyoung Kim, Jaydeep P. Kulkarni, Eren Kursun, Erik Larsson, Hai (Helen) Li, Huawei Li, Patrick P. Mercier, Prabhat Mishra, Makoto Nagata, Arun S. Natarajan, Koji Nii, Partha Pratim Pande, Ioannis Savidis, Mingoo Seok, Sheldon X.-D. Tan, Mark M. Tehranipoor, Aida Todri-Sanial, Miroslav N. Velev, Xiaoqing Wen, Jiang Xu, Wei Zhang, Zhengya Zhang, Stacey Weber Jackson
Editorial. IEEE Trans. Very Large Scale Integr. Syst. 25 (1) (2017)
Prab Varma, Miroslav N. Velev
Welcome Message. HLDVT (2016)
Miroslav N. Velev, Ping Gao
Application of Hierarchical Hybrid Encodings to Solve CSPs as Equivalent SAT Problems. ISAIM (2016)
Miroslav N. Velev, Chaoqiang Zhang, Ping Gao, Alex David Groce
Exploiting abstraction, learning from random simulation, and SVM classification for efficient dynamic prediction of software health problems. ISQED (2015)
Miroslav N. Velev, John Franco
Application of constraints to formal verification and artificial intelligence. Ann. Math. Artif. Intell. 70 (4) (2014)
Miroslav N. Velev, Ping Gao
Improving the efficiency of automated debugging of pipelined microprocessors by symmetry breaking in modular schemes for boolean encoding of cardinality. ICCAD (2014)
Miroslav N. Velev, Ping Gao
Efficient parallel GPU algorithms for BDD manipulation. ASP-DAC (2014)
Miroslav N. Velev, Ping Gao
Formal verification of safety of polymorphic heterogeneous multi-core architectures. ISQED (2014)
Van-Hau Nguyen, Miroslav N. Velev, Pedro Barahona
Application of Hierarchical Hybrid Encodings to Efficient Translation of CSPs to SAT. ICTAI (2013)
Miroslav N. Velev, Ping Gao
Automated debugging of counterexamples in formal verification of pipelined microprocessors. ASP-DAC (2012)
Miroslav N. Velev, Ping Gao
Exploiting Abstraction for Efficient Formal Verification of DSPs with Arrays of Reconfigurable Functional Units. ICFEM (2011)
Miroslav N. Velev, Ping Gao
Automatic formal verification of multithreaded pipelined microprocessors. ICCAD (2011)
Miroslav N. Velev, Ping Gao
Automatic formal verification of reconfigurable DSPs. ASP-DAC (2011)
Miroslav N. Velev, Ping Gao
CNF encodings of cardinality in formal methods for robustness checking of gate-level circuits. ISCAS (2011)
Miroslav N. Velev, Ping Gao
Modular Schemes for Constructing Equivalent Boolean Encodings of Cardinality Constraints and Application to Error Diagnosis in Formal Verification of Pipelined Microprocessors. SARA (2011)
Miroslav N. Velev, Ping Gao
Efficient Pseudo-Boolean Satisfiability Encodings for Routing and Wavelength Assignment in Optical Networks. SARA (2011)
Miroslav N. Velev, Ping Gao
Design of parallel portfolios for SAT-based solving of Hamiltonian cycle problems. ISAIM (2010)
Miroslav N. Velev, Ping Gao
Method for Formal Verification of Soft-Error Tolerance Mechanisms in Pipelined Microprocessors. ICFEM (2010)
Miroslav N. Velev, Ping Gao
A method for debugging of pipelined processors in formal verification by correspondence checking. ASP-DAC (2010)
Miroslav N. Velev, Ping Gao
Efficient SAT Techniques for Relative Encoding of Permutations with Constraints. Australasian Conference on Artificial Intelligence (2009)
Miroslav N. Velev, Ping Gao
Efficient SAT Techniques for Absolute Encoding of Permutation Problems: Application to Hamiltonian Cycles. SARA (2009)
Miroslav N. Velev, Ping Gao
Efficient SAT-based techniques for Design of Experiments by using static variable ordering. ISQED (2009)
Miroslav N. Velev, Ping Gao
Exploiting hierarchical encodings of equality to design independent strategies in parallel SMT decision procedures for a logic of equality. HLDVT (2009)
Miroslav N. Velev, Ping Gao
Comparison of Boolean Satisfiability Encodings on FPGA Detailed Routing Problems. DATE (2008)
Miroslav N. Velev
Editor's Introduction to the Special Volume on Application of Constraints to Formal Verification. J. Satisf. Boolean Model. Comput. 5 (1-4) (2008)
Miroslav N. Velev
Exploiting hierarchy and structure to efficiently solve graph coloring as SAT. ICCAD (2007)
Miroslav N. Velev
Using Abstraction for Efficient Formal Verification of Pipelined Processors with Value Prediction. ISQED (2006)
Miroslav N. Velev
Formal Verification of Pipelined Microprocessors with Delayed Branches. ISQED (2006)
Miroslav N. Velev
Integrating formal verification into an advanced computer architecture course. IEEE Trans. Educ. 48 (2) (2005)
Miroslav N. Velev
Comparison of schemes for encoding unobservability in translation to SAT. ASP-DAC (2005)
Miroslav N. Velev, Randal E. Bryant
TLSim and EVC: a term-level symbolic simulator and an efficient decision procedure for the logic of equality with uninterpreted functions and memories. Int. J. Embed. Syst. 1 (1/2) (2005)
Miroslav N. Velev
Automatic Formal Verification of Liveness for Pipelined Processors with Multicycle Functional Units. CHARME (2005)
Miroslav N. Velev
Exploiting Signal Unobservability for Efficient Translation to CNF in Formal Verification of Microprocessors. DATE (2004)
Miroslav N. Velev
Comparative Study of Strategies for Formal Verification of High-Level Processors. ICCD (2004)
Miroslav N. Velev
Tuning SAT for Formal Verification and Testing. J. Univers. Comput. Sci. 10 (12) (2004)
Miroslav N. Velev
Encoding Global Unobservability for Efficient Translation to SAT. SAT (2004)
Miroslav N. Velev
A new generation of ISCAS benchmarks from formal verification of high-level microprocessors. ISCAS (5) (2004)
Miroslav N. Velev
Using positive equality to prove liveness for pipelined microprocessors. ASP-DAC (2004)
Miroslav N. Velev
Formal verification of pipelined processors with load-value prediction. HLDVT (2004)
Miroslav N. Velev
Efficient formal verification of pipelined processors with instruction queues. ACM Great Lakes Symposium on VLSI (2004)
Miroslav N. Velev
Efficient translation of boolean formulas to CNF in formal verification of microprocessors. ASP-DAC (2004)
Miroslav N. Velev
Using Automatic Case Splits and Efficient CNF Translation to Guide a SAT-solver when Formally Verifying Out-Of-Order Processors. AI&M (2004)
Sudarshan K. Srinivasan, Miroslav N. Velev
Formal Verification of an Intel XScale Processor Model with Scoreboarding, Specialized Execution Pipelines, and Impress Data-Memory Exceptions. MEMOCODE (2003)
Miroslav N. Velev
Collection of High-Level Microprocessor Bugs from Formal Verification of Pipelined and Superscalar Designs. ITC (2003)
Miroslav N. Velev, Randal E. Bryant
Effective use of Boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors. J. Symb. Comput. 35 (2) (2003)
Miroslav N. Velev
Automatic Abstraction of Equations in a Logic of Equality. TABLEAUX (2003)
Randal E. Bryant, Miroslav N. Velev
Boolean satisfiability with transitivity constraints. ACM Trans. Comput. Log. 3 (4) (2002)
Miroslav N. Velev
Using Rewriting Rules and Positive Equality to Formally Verify Wide-Issue Out-of-Order Microprocessors with a Reorder Buffer. DATE (2002)
Miroslav N. Velev, Randal E. Bryant
EVC: A Validity Checker for the Logic of Equality with Uninterpreted Functions and Memories, Exploiting Positive Equality, and Conservative Transformations. CAV (2001)
Miroslav N. Velev
Automatic Abstraction of Memories in the Formal Verification of Superscalar Microprocessors. TACAS (2001)
Randal E. Bryant, Steven M. German, Miroslav N. Velev
Processor verification using efficient reductions of the logic of uninterpreted functions to propositional logic. ACM Trans. Comput. Log. 2 (1) (2001)
Miroslav N. Velev, Randal E. Bryant
Effective Use of Boolean Satisfiability Procedures in the Formal Verification of Superscalar and VLIW Microprocessors. DAC (2001)
Randal E. Bryant, Miroslav N. Velev
Boolean Satisfiability with Transitivity Constraints. CAV (2000)
Miroslav N. Velev, Randal E. Bryant
Formal verification of superscale microprocessors with multicycle functional units, exception, and branch prediction. DAC (2000)
Miroslav N. Velev
Formal Verification of VLIW Microprocessors with Speculative Execution. CAV (2000)
Randal E. Bryant, Miroslav N. Velev
Boolean Satisfiability with Transitivity Constraints CoRR (2000)
Randal E. Bryant, Steven M. German, Miroslav N. Velev
Microprocessor Verification Using Efficient Decision Procedures for a Logic of Equality with Uninterpreted Functions. TABLEAUX (1999)
Miroslav N. Velev, Randal E. Bryant
Superscalar Processor Verification Using Efficient Reductions of the Logic of Equality with Uninterpreted Functions to Propositional Logic. CHARME (1999)
Randal E. Bryant, Steven M. German, Miroslav N. Velev
Exploiting Positive Equality in a Logic of Equality with Uninterpreted Functions. CAV (1999)
Randal E. Bryant, Steven M. German, Miroslav N. Velev
Processor Verification Using Efficient Reductions of the Logic of Uninterpreted Functions to Propositional Logic CoRR (1999)
Miroslav N. Velev, Randal E. Bryant
Exploiting Positive Equality and Partial Non-Consistency in the Formal Verification of Pipelined Microprocessors. DAC (1999)
Miroslav N. Velev, Randal E. Bryant
Efficient Modeling of Memory Arrays in Symbolic Ternary Simulation. TACAS (1998)
Miroslav N. Velev, Randal E. Bryant
Incorporating timing constraints in the efficient memory model for symbolic ternary simulation. ICCD (1998)
Miroslav N. Velev, Randal E. Bryant
Verification of Pipelined Microprocessors by Correspondence Checking in Symbolic Ternary Simulation. ACSD (1998)
Miroslav N. Velev, Randal E. Bryant
Bit-Level Abstraction in the Verfication of Pipelined Microprocessors by Correspondence Checking. FMCAD (1998)
Miroslav N. Velev, Randal E. Bryant, Alok Jain
Efficient Modeling of Memory Arrays in Symbolic Simulation. CAV (1997)
Randal E. Bryant, Miroslav N. Velev
Verification of Pipelined Microprocessors by Comparing Memory Execution Sequences in Symbolic Simulation. ASIAN (1997)