Miroslav N. Velev

Fellow of AAAS

Associate Fellow of AIAA

ACM Distinguished Member (Distinguished Scientist)

E-mail: mvelev AT gmail DOT com

Short Curriculum Vitae

Education

• Ph.D. in Electrical and Computer Engineering, Carnegie Mellon University, May 2004.
  Was advised by Prof. Randal E. Bryant, the inventor of Binary Decision Diagrams (BDDs) and the previous Dean of the School of Computer Science at Carnegie Mellon University.
• B.S.&M.S. in Electrical Engineering and B.S. in Economics, Yale University, May 1994.  

Professional Experience

• Founder and President, Aries Design Automation, Chicago, IL, May 2005 – present, where I lead R&D projects on formal verification topics for the U.S. Department of Defense, NASA, the U.S. Department of Energy, and NIST.
  
• Adjunct Assistant Professor, Department of Electrical and Computer Engineering at the University of Illinois at Chicago, Chicago, IL, 2006 – 2007.
  
• Visiting Assistant Professor, School of Electrical and Computer Engineering at the Georgia Institute of Technology, Atlanta, GA, 2002 – 2003: Taught a course integrating computer architecture and formal verification of microprocessors; advised graduate students.
  
• Summer Intern, Motorola, Austin, TX, May - August 1998: Worked on the formal verification of the M.CORE microprocessor.
• Ph.D. student in Electrical and Computer Engineering, Carnegie Mellon University, 1995 – 2001: Developed an Efficient Memory Model for behavioral abstraction of memory arrays in symbolic ternary simulation. This model was adopted by Intel, NEC, and Motorola in internal tools, by Synopsys in a prototype of a commercial tool, and by Innologic Systems in a commercial tool. Developed a tool flow and formal verification techniques that are highly automatic, and significantly outperform all previous methods for formal verification of pipelined microprocessors. This tool flow was used to formally verify a model of the M.CORE processor at Motorola, and detected bugs.
  
• Technical Associate, Information Services, CS First Boston Corporation, New York, NY, 1994 – 1995: Worked on the development of a global information system.  

Awards

• IEEE Aerospace and Electronic Systems Society (AESS) Industrial Innovation Award, 2021.
• Award of the European Organization for Information Technology and Microelectronics (EUROMICRO) for Extensive Long-Term Involvement in the Editorial Board of the EUROMICRO/Elsevier Journal of Microprocessors and Microsystems (MICPRO), 2018.
• IEEE Council on Electronic Design Automation Certificate of Appreciation in Recognition of Service as Associate Editor for the IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2018.
• Single Event Upset Award of the AIAA Computer Systems Technical Committee (CSTC) for Volunteer Contributions to the Organization of AIAA Forums, 2017.
• ACM Recognition of Service Award, 2017.
• EDAA Outstanding Dissertation Award for New Directions in Logic and System Design, 2005.
• Franz Tuteur Memorial Prize for the Most Outstanding Senior Project in Electrical Engineering, Yale University, May 1994.  

Research Interests

Formal Verification of Microprocessors, Decision Procedures, Boolean Satisfiability (SAT), SAT Solvers, Computer-Aided Design for VLSI, Constraint Satisfaction Problems (CSPs), Computer Architecture, Computer Engineering, Artificial Intelligence.