Miroslav Velev's Publications & Talks

C57

M.N. Velev, Automatic Formal Verification of RISC-V Pipelined Microprocessors with Fault Tolerance by Spatial Redundancy at a High Level of Abstraction, 18^th International Conference on integrated Formal Methods (iFM ’23), P. Herber, and A. Wijs, eds., LNCS 14300, November 2023, pp. 193–213.

C56

M.N. Velev, and P. Gao, Application of Hierarchical Hybrid Encodings to Solve CSPs as Equivalent SAT Problems, 14^th International Symposium on Artificial Intelligence and Mathematics (ISAIM '16), January 2016.

C55

M.N. Velev, C. Zhang, P. Gao, and A.D. Groce, Exploiting Abstraction, Learning from Random Simulation, and SVM Classification for Efficient Dynamic Prediction of Software Health Problems, 16^th IEEE International Symposium on Quality Electronic Design (ISQED '15), March 2015, pp. 412-418. [Invited talk]

C54

M.N. Velev, and P. Gao, Improving the Efficiency of Automated Debugging of Pipelined Microprocessors by Symmetry Breaking in Modular Schemes for Boolean Encoding of Cardinality, 33^rd IEEE/ACM International Conference on Computer-Aided Design (ICCAD '14), November 2014, pp. 676-683.

C53

M.N. Velev, and P. Gao, Formal Verification of Safety of Polymorphic Heterogeneous Multi-Core Architectures, 15^th IEEE International Symposium on Quality Electronic Design (ISQED '14), March 2014, pp. 611-617.

C52

M.N. Velev, and P. Gao, Efficient Parallel GPU Algorithms for BDD Manipulation, 19^th Asia and South Pacific Design Automation Conference (ASP-DAC '14), January 2014, pp. 750-755.

C51

V.-H. Nguyen, M.N. Velev, and P. Barahona, Application of Hierarchical Hybrid Encodings to Efficient Translation of CSPs to SAT, 25^th IEEE International Conference on Tools with Artificial Intelligence (ICTAI '13), November 2013, pp. 1028-1035.

C50

M.N. Velev, and P. Gao, Automated Debugging of Counterexamples in Formal Verification of Pipelined Microprocessors, 17^th Asia and South Pacific Design Automation Conference (ASP-DAC '12), January - February 2012, pp. 689-694.

C49

M.N. Velev, and P. Gao, Automatic Formal Verification of Multithreaded Pipelined Microprocessors, 30^th IEEE/ACM International Conference on Computer-Aided Design (ICCAD '11), November 2011, pp. 679-686.

C48

M.N. Velev, and P. Gao, Exploiting Abstraction for Efficient Formal Verification of DSPs with Arrays of Reconfigurable Functional Units, 13^th International Conference on Formal Engineering Methods (ICFEM '11), S. Qin and Z. Qiu, eds., LNCS 6991, Springer, October 2011, pp. 307-322.

C47

M.N. Velev, and P. Gao, Modular Schemes for Constructing Equivalent Boolean Encodings of Cardinality Constraints and Application to Error Diagnosis in Formal Verification of Pipelined Microprocessors, 9^th Symposium on Abstraction, Reformulation and Approximation (SARA '11), July 2011, pp. 125-131.

C46

M.N. Velev, and P. Gao, Efficient Pseudo-Boolean Satisfiability Encodings for Routing and Wavelength Assignment in Optical Networks, 9^th Symposium on Abstraction, Reformulation and Approximation (SARA '11), July 2011, pp. 117-124.

C45

M.N. Velev, and P. Gao, CNF Encodings of Cardinality in Formal Methods for Robustness Checking of Gate-Level Circuits, IEEE International Symposium on Circuits and Systems (ISCAS '11), May 2011, pp. 1479-1482.

C44

M.N. Velev, and P. Gao, Automatic Formal Verification of Reconfigurable DSPs, 16^th Asia and South Pacific Design Automation Conference (ASP-DAC '11), January 2011, pp. 293-296. [Invited talk]

C43

M.N. Velev, and P. Gao, Method for Formal Verification of Soft-Error Tolerance Mechanisms in Pipelined Microprocessors, 12^th International Conference on Formal Engineering Methods (ICFEM '10), J.S. Dong and H. Zhu, eds., LNCS 6447, Springer, November 2010, pp. 355-370.

C42

M.N. Velev, and P. Gao, A Method for Debugging of Pipelined Processors in Formal Verification by Correspondence Checking, 15^th Asia and South Pacific Design Automation Conference (ASP-DAC '10), January 2010, pp. 619-624.

C41

M.N. Velev, and P. Gao, Design of Parallel Portfolios for SAT-Based Solving of Hamiltonian Cycle Problems, 11^th International Symposium on Artificial Intelligence and Mathematics (ISAIM '10), January 2010.

C40

M.N. Velev, and P. Gao, Efficient SAT Techniques for Relative Encoding of Permutations with Constraints, 22^nd Australasian Joint Conference on Artificial Intelligence (AI '09), A. Nicholson, and X. Li, eds., LNAI 5866, Springer-Verlag, December 2009, pp. 517-527.

C39

M.N. Velev, and P. Gao, Efficient SAT Techniques for Absolute Encoding of Permutation Problems: Application to Hamiltonian Cycles, 8^th Symposium on Abstraction, Reformulation and Approximation (SARA '09), July 2009, pp. 159-166.

C38

M.N. Velev, and P. Gao, Efficient SAT-Based Techniques for Design of Experiments by Using Static Variable Ordering, 10^th IEEE International Symposium on Quality Electronic Design (ISQED '09), March 2009, pp. 371-376.

C37

M.N. Velev, and P. Gao, Comparison of Boolean Satisfiability Encodings on FPGA Detailed Routing Problems, Design, Automation and Test in Europe (DATE '08), March 2008, pp. 1268-1273.

C36

M.N. Velev, Exploiting Hierarchy and Structure to Efficiently Solve Graph Coloring as SAT, 26^th IEEE/ACM International Conference on Computer-Aided Design (ICCAD '07), November 2007, pp. 135-142.

C35

M.N. Velev, Using Abstraction for Efficient Formal Verification of Pipelined Processors with Value Prediction, 7^th IEEE International Symposium on Quality Electronic Design (ISQED '06), March 2006, pp. 51-56. [Nominated for best paper award]

C34

M.N. Velev, Formal Verification of Pipelined Microprocessors with Delayed Branches, 7^th IEEE International Symposium on Quality Electronic Design (ISQED '06), March 2006, pp. 296-299.

C33

M.N. Velev, Efficient Formal Verification of Pipelined Microprocessors, International SoC Design Conference (ISOCC '05), October 2005, pp. 1-4. [Invited talk]

C32

M.N. Velev, Automatic Formal Verification of Liveness for Pipelined Processors with Multicycle Functional Units, 13^th Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME '05), D. Borrione, and W.J. Paul, eds., LNCS 3725, Springer-Verlag, October 2005, pp. 97-113.

C31

M.N. Velev, Comparison of Schemes for Encoding Unobservability in Translation to SAT, Asia and South Pacific Design Automation Conference (ASP-DAC '05), January 2005, pp. 1056-1059.

C30

M.N. Velev, Comparative Study of Strategies for Formal Verification of High-Level Processors, 22^nd International Conference on Computer Design (ICCD '04), October 2004, pp. 119-124.

C29

M.N. Velev, A New Correctness Proof for Positive Equality, International Colloquium on Theoretical Aspects of Computing (ICTAC '04), September 2004, pp. 495-512.

C28

M.N. Velev, A New Generation of ISCAS Benchmarks from Formal Verification of High-Level Microprocessors, International Symposium on Circuits and Systems (ISCAS '04), Vol. 5, May 2004, pp. 213-216.

C27

M.N. Velev, Encoding Global Unobservability for Efficient Translation to SAT, 7^th International Conference on Theory and Applications of Satisfiability Testing (SAT '04), May 2004, pp. 197-204.

C26

M.N. Velev, Efficient Formal Verification of Pipelined Processors with Instruction Queues, Great Lakes Symposium on VLSI (GLSVLSI '04), April 2004, pp. 92-95.

C25

M.N. Velev, Exploiting Signal Unobservability for Efficient Translation to CNF in Formal Verification of Microprocessors, Design, Automation and Test in Europe (DATE '04), February 2004, pp. 266-271.

C24

M.N. Velev, Using Positive Equality to Prove Liveness for Pipelined Microprocessors, Asia and South Pacific Design Automation Conference (ASP-DAC '04), January 2004, pp. 316-321.

C23

M.N. Velev, Efficient Translation of Boolean Formulas to CNF in Formal Verification of Microprocessors, Asia and South Pacific Design Automation Conference (ASP-DAC '04), January 2004, pp. 310-315. [One of four papers nominated for the 10^th Anniversary Retrospective Most Influential Paper Award at ASP-DAC'14, based on the references reported by Google Scholar for all papers published at ASP-DAC'04]

C22

M.N. Velev, Using Automatic Case Splits and Efficient CNF Translation to Guide a SAT-Solver When Formally Verifying Out-of-Order Processors, Artificial Intelligence and Mathematics (AI&MATH '04), January 2004, pp. 242-254.

C21

M.N. Velev, Collection of High-Level Microprocessor Bugs from Formal Verification of Pipelined and Superscalar Designs, International Test Conference (ITC '03), October 2003, pp. 138-147.

C20

M.N. Velev, Automatic Abstraction of Equations in a Logic of Equality, Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX '03), M.C. Mayer, and F. Pirri, eds., LNAI 2796, Springer-Verlag, September 2003, pp. 196-213.

C19

S.K. Srinivasan, and M.N. Velev, Formal Verification of an Intel XScale Processor Model with Scoreboarding, Specialized Execution Pipelines, and Imprecise Data-Memory Exceptions, Formal Methods and Models for Codesign (MEMOCODE '03), June 2003, pp. 65-74.

C18

M.N. Velev, Integrating Formal Verification into an Advanced Computer Architecture Course, ASEE Annual Conference & Exposition, June 2003.

C17

M.N. Velev, Using Rewriting Rules and Positive Equality to Formally Verify Wide-Issue Out-Of-Order Microprocessors with a Reorder Buffer, Design, Automation and Test in Europe (DATE '02), March 2002, pp. 28-35.

C16

M.N. Velev, and R.E. Bryant, EVC: A Validity Checker for the Logic of Equality with Uninterpreted Functions and Memories, Exploiting Positive Equality and Conservative Transformations, Computer-Aided Verification (CAV '01), G. Berry, H. Comon, and A. Finkel, eds., LNCS 2102, Springer-Verlag, July 2001, pp. 235-240.

C15

M.N. Velev, and R.E. Bryant, Effective Use of Boolean Satisfiability Procedures in the Formal Verification of Superscalar and VLIW Microprocessors, 38^th Design Automation Conference (DAC '01), June 2001, pp. 226-231.

C14

M.N. Velev, Automatic Abstraction of Memories in the Formal Verification of Superscalar Microprocessors, Tools and Algorithms for the Construction and Analysis of Systems (TACAS '01), T. Margaria and W. Yi, eds., LNCS 2031, Springer-Verlag, April 2001, pp. 252-267.

C13

M.N. Velev, Formal Verification of VLIW Microprocessors with Speculative Execution, Computer-Aided Verification (CAV '00), E.A. Emerson and A.P. Sistla, eds., LNCS 1855, Springer-Verlag, July 2000, pp. 296-311.

C12

R.E. Bryant, and M.N. Velev, Boolean Satisfiability with Transitivity Constraints, Computer-Aided Verification (CAV '00), E.A. Emerson and A.P. Sistla, eds., LNCS 1855, Springer-Verlag, July 2000, pp. 86-98.

C11

M.N. Velev, and R.E. Bryant, Formal Verification of Superscalar Microprocessors with Multicycle Functional Units, Exceptions, and Branch Prediction, 37^th Design Automation Conference (DAC '00), June 2000, pp. 112-117.

C10

M.N. Velev, and R.E. Bryant, Superscalar Processor Verification Using Efficient Reductions of the Logic of Equality with Uninterpreted Functions to Propositional Logic, Correct Hardware Design and Verification Methods (CHARME '99), L. Pierre and T. Kropf, eds., LNCS 1703, Springer-Verlag, September 1999, pp. 37-53.

R.E. Bryant, S. German, and M.N. Velev, Exploiting Positive Equality in a Logic of Equality with Uninterpreted Functions, Computer-Aided Verification (CAV '99), N. Halbwachs and D. Peled, eds., LNCS 1633, Springer-Verlag, July 1999, pp. 470-482.

M.N. Velev, and R.E. Bryant, Exploiting Positive Equality and Partial Non-Consistency in the Formal Verification of Pipelined Microprocessors, 36^th Design Automation Conference (DAC '99), June 1999, pp. 397-401.

R.E. Bryant, S. German, and M.N. Velev, Processor Verification Using Efficient Decision Procedures for a Logic of Uninterpreted Functions, Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX '99), N.V. Murray, ed., LNAI 1617, Springer-Verlag, June 1999, pp. 1-13.

M.N. Velev, and R.E. Bryant, Bit-Level Abstraction in the Verification of Pipelined Microprocessors by Correspondence Checking, Formal Methods in Computer-Aided Design (FMCAD '98), G. Gopalakrishnan and P. Windley, eds., LNCS 1522, Springer-Verlag, November 1998, pp. 18-35.

M.N. Velev, and R.E. Bryant, Incorporating Timing Constraints in the Efficient Memory Model for Symbolic Ternary Simulation, 16^th International Conference on Computer Design (ICCD '98), October 1998, pp. 400-406.

M.N. Velev, and R.E. Bryant, Verification of Pipelined Microprocessors by Correspondence Checking in Symbolic Ternary Simulation, International Conference on Application of Concurrency to System Design (CSD '98), IEEE Computer Society, March 1998, pp. 200-212.

M.N. Velev, and R.E. Bryant, Efficient Modeling of Memory Arrays in Symbolic Ternary Simulation, Tools and Algorithms for the Construction and Analysis of Systems (TACAS '98), B. Steffen, ed., LNCS 1384, Springer-Verlag, March-April 1998, pp. 136-150.

R.E. Bryant, and M.N. Velev, Verification of Pipelined Microprocessors by Comparing Memory Execution Sequences in Symbolic Simulation, Asian Computer Science Conference (ASIAN '97), R.K. Shyamasundar and K. Ueda, eds., LNCS 1345, Springer-Verlag, December 1997, pp. 18-31.

M.N. Velev, R.E. Bryant, and A. Jain, Efficient Modeling of Memory Arrays in Symbolic Simulation, Computer-Aided Verification (CAV '97), O. Grumberg, ed., LNCS 1254, Springer-Verlag, June 1997, pp. 388-399.

Keynote Speaker

Invited Speaker

Thesis

Journal Papers

Conference Papers

Workshop Papers

Technical Reports