Miroslav Velev's Publications and Talks

Keynote Speaker

Invited Speaker

Thesis

TH
M.N. Velev, Formal Verification of Pipelined Microprocessors by Correspondence Checking, Ph.D. thesis, Department of Electrical and Computer Engineering, Carnegie Mellon University, May 2004.  

Journal Papers

J5
M.N. Velev, Integrating Formal Verification into an Advanced Computer Architecture Course, IEEE Transactions on Education, Vol. 48, No. 2 (May 2005), pp. 216-222.  
J4
M.N. Velev, and R.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, Special Issue on Hardware-Software Codesign for Systems-on-Chip, International Journal of Embedded Systems (IJES), Vol. 1, Nos. 1/2 (2005), pp. 134-149.  
J3
J2
R.E. Bryant, and M.N. Velev, Boolean Satisfiability with Transitivity Constraints, ACM Transactions on Computational Logic (TOCL), Vol. 3, No. 4 (October 2002), pp. 604-627.  
J1

Conference Papers

C57
C56
C55
C54
C53
C52
C51
C50
C49
C48
C47
C46
C45
C44
C43
C42
C41
C40
C39
M.N. Velev, and P. Gao, Efficient SAT Techniques for Absolute Encoding of Permutation Problems: Application to Hamiltonian Cycles, 8th 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, 10th 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, 26th 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, 7th 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, 7th 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, 13th 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, 22nd 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, 7th 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 10th 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
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
C18
C17
C16
C15
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
C10
C9
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.  
C8
C7
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.  
C6
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.  
C5
M.N. Velev, and R.E. Bryant, Incorporating Timing Constraints in the Efficient Memory Model for Symbolic Ternary Simulation, 16th International Conference on Computer Design (ICCD '98), October 1998, pp. 400-406.  
C4
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.  
C3
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.  
C2
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.  
C1
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.  

Workshop Papers

W11
W10
W9
M.N. Velev, and P. Gao, Exploiting Hierarchical Encodings of Equality to Design Independent Strategies in Parallel SMT Decision Procedures for a Logic of Equality, 14th IEEE International High Level Design Validation and Test Workshop (HLDVT '09), November 2009, pp. 8-13.  
W8
M.N. Velev, Formal Verification of Pipelined Processors with Load-Value Prediction, 9th IEEE International High Level Design Validation and Test Workshop (HLDVT '04), November 2004.  
W7
M.N. Velev, Collection of EUFM Benchmark Suites from Formal Verification of Microprocessors, Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR '03), workshop affiliated with Conference on Automated Deduction (CADE-19), July 2003, pp. 77-93.  
W6
M.N. Velev, First Results from Introducing Formal Verification to an Advanced Computer Architecture Course, 2003 Annual Meeting of the Southeastern Section of the American Society for Engineering Education, April 2003.  
W5
M.N. Velev, and R.E. Bryant, Techniques for Fast Counterexample Generation in the Formal Verification of Superscalar and VLIW Microprocessors, SRC TECHCON '00, September 2000.  
W4
M.N. Velev, and R.E. Bryant, Encoding Techniques for Symbolic Data Values in the Verification of Pipelined Microprocessors by Correspondence Checking, 3rd IEEE International High Level Design Validation and Test Workshop (HLDVT '98), November 1998, pp. 9-16.  
W3
M.N. Velev, and R.E. Bryant, Exploiting the Logic of Positive Equality for Formal Verification of Pipelined Microprocessors, IEEE International Workshop on Microprocessor Test and Verification (MTV '98), October 1998.  
W2
M.N. Velev, and R.E. Bryant, Bit-Level Abstraction in Pipelined Microprocessor Verification, SRC TECHCON '98, September 1998.  
W1
M.N. Velev, and R.E. Bryant, Efficient Modeling of Memory Arrays with Timing Requirements in Symbolic Ternary Simulation, International Workshop on Timing Issues in the Specification and Synthesis of Digital Systems (TAU '97), December 1997, pp. 28-38.  

Technical Reports


Last updated on April 29, 2022.