| Submission Procedure |  |
|
|
|
||||||||
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 was a Visiting Assistant Professor at the School of Electrical and Computer Engineering at the Georgia Institute of Technology in Atlanta, Georgia. 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. Dr. Velev is the founder and president of Aries Design Automation, a company that develops formal verification technology for the U.S. Department of Defense and NASA. Dr. Velev is the author of 28 suites of SAT benchmarks, containing more than 1,100 Boolean formulas generated in formal verification of complex high-level models of pipelined, superscalar, and VLIW microprocessors. Many of these formulas are extremely challenging for the current state-of-the-art SAT solvers. His benchmarks have been used in hundreds of papers, as well as in the annual SAT-solver competitions since 2000, and have had a significant impact on the recent tremendous advances in the field of SAT. He has over 50 refereed publications. 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 or currently serves on the technical program committees of over 120 conferences, including AAAI, ASP-DAC, CADE, CASES, CHARME, DATE, GLSVLSI, ICCD, ISCAS, ISQED, MEMOCODE, RTAS, and SAT. He was 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 special issue of the Journal on Satisfiability, Boolean Modeling and Computation (JSAT) on the topic of Constraints in Formal Verification, May 2008. He was a co-chair of the International Workshop on Constraints in Formal Verification (CFV) in 2005, and chair in 2007 and 2008. Dr. Velev was an invited speaker at the International SoC Design Conference (ISOCC'05), Seoul, Korea, October 2005. A paper of his was nominated for the best paper award at the 7th International Symposium on Quality Electronic Design (ISQED'06), March 2006. He is the recipient of the Franz Tuteur Memorial Prize for the Most Outstanding Senior Project in Electrical Engineering, Yale University, May 1994, and of the 2005 EDAA Outstanding Dissertation Award for the Topic New Directions in Logic and System Design.
Main Research Interests:
|
