Miroslav N. Velev

Curriculum Vitae:

Ph.D. in Electrical and Computer Engineering, Carnegie Mellon University, 2004; B.S.&M.S. in Electrical Engineering and B.S. in Economics, Yale University, 1994. In 2002 and 2003, he held the position of Instructor at the School of Electrical and Computer Engineering at the Georgia Institute of Technology in Atlanta, Georgia. He is currently working as an independent consultant. He has developed a highly automatic tool flow and formal verification techniques that were adopted by Motorola, and used to detect bugs in their M.CORE processor. He has also developed an Efficient Memory Model for the behavioral abstraction of memory arrays in bit-level symbolic simulation; this work was adopted by Intel, Motorola, and NEC in their internal tools, and by Synopsys and Innologic Systems in commercial tools.

Miroslav Velev is the author of over 45 refereed publications, and 28 benchmark suites of more than 1,100 SAT formulas that are used widely in the research community. He is member of the editorial boards of the Journal of Universal Computer Science (J.UCS), and the Journal on Satisfiability, Boolean Modeling and Computation (JSAT). He has served on the technical program committees of over 65 conferences, including AAAI, ASP-DAC, CADE, CASES, CHARME, DATE, ICCD, ISCAS, ISQED, MEMOCODE, RTAS, and SAT. He is the guest editor of a special issue of the Journal of Universal Computer Science on the topic of Tuning SAT for Formal Verification and Testing, December 2004, and a co-chair of the 3rd International Workshop on Constraints in Formal Verification (CFV'05), which was held as a satellite event at the 20th International Conference on Automated Deduction (CADE-20), July 2005. He was an invited speaker at the International SoC Design Conference (ISOCC'05), Seoul, Korea, October 2005.

Miroslav Velev is the recipient of the Franz Tuteur Memorial Prize for the Most Outstanding Senior Project in Electrical Engineering, Yale University, May 1994.

Main Research Interests:

• automatic formal verification of microprocessors
• formal verification of hardware
• Boolean Satisfiability (SAT) methods
• model checking
• Abstract State Machines
• computer architecture
• decision procedures
• CAD for VLSI
• computer engineering
• Artificial Intelligence (AI)