Miroslav N. Velev

E-mail: mvelev AT gmail DOT com

Curriculum Vitae

Education:

Ph.D. in Electrical and Computer Engineering, Carnegie Mellon University, May 2004.
B.S.&M.S. in Electrical Engineering and B.S. in Economics, Yale University, May 1994.

Some professional experience:

Founder and President, Aries Design Automation, Chicago, IL, May 2005 - present, where I lead R&D projects on formal verification topics for NASA, the U.S. Department of Defense, and the U.S. Department of Energy.
Adjunct Assistant Professor, Department of Electrical and Computer Engineering at the University of Illinois at Chicago, Chicago, IL, August 2006 - present: This is a part-time position that generally requires the teaching of one senior or graduate-level course per semester.
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:

EDAA Outstanding Dissertation Award for the Topic 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.

Senior Member of IEEE.

Listed in the Marquis editions of:

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.

Professional Activities

Workshop Organizer and Chair

CFV '09: Sixth International Workshop on Constraints in Formal Verification, Grenoble, France, June 2009. A workshop affiliated with the 21st International Conference on Computer Aided Verification (CAV 2009), Grenoble, France, June 26 - July 2, 2009.
CFV '08: Fifth International Workshop on Constraints in Formal Verification, Sydney, Australia, August 2008. A workshop affiliated with the 4th International Joint Conference on Automated Reasoning (IJCAR 2008), Sydney, Australia, August 10 - 15, 2008.
CFV '07: Fourth International Workshop on Constraints in Formal Verification, Bremen, Germany, July 16, 2007. A workshop affiliated with the 21st International Conference on Automated Deduction (CADE-21), Bremen, Germany, July 17 - 20, 2007.
ARW '06: Automated Reasoning Workshop, University of Bristol, Bristol, U.K., April 3 - 4, 2006. A workshop affiliated with Adaptation in Artificial and Biological Systems, University of Bristol, Bristol, U.K., April 3 - 6, 2006.
CFV '05: Third International Workshop on Constraints in Formal Verification, Tallinn, Estonia, July 23, 2005. A workshop affiliated with the 20th International Conference on Automated Deduction (CADE-20), Tallinn, Estonia, July 2005.

Conference Track Co-Chair

MWSCAS '09: 52nd IEEE International Midwest Symposium on Circuits and Systems (MWSCAS 2009), Cancun, Mexico, August 2 - 5, 2009. Co-chair of Track 8: Verification.
MWSCAS '08: 51st IEEE International Midwest Symposium on Circuits and Systems (MWSCAS 2008), Knoxville, Tennessee, U.S.A., August 10 - 13, 2008. Co-chair of Track 8: Verification.
MWSCAS-NEWCAS '07: 50th IEEE International Midwest Symposium on Circuits and Systems (MWSCAS 2007) and 5th IEEE International NEWCAS Conference (IEEE-NEWCAS 2007), Montréal, Canada, August 5 - 8, 2007. Co-chair of Track 16: Characterization and Testing.
ISOCC '05: International SoC Design Conference, Seoul, Korea, October 20 - 21, 2005. Co-chair of Track 9: SoC Testing and Verification.

Publicity Chair

HLDVT '10: 15th IEEE International High Level Design, Validation and Test Workshop, San Francisco, California, U.S.A., June 11 - 12, 2010.
HLDVT '09: IEEE International High Level Design, Validation and Test Workshop, San Francisco, California, U.S.A., November 4-6, 2009.

Plenary Chair

DSD '03: EUROMICRO Symposium on Digital System Design, Antalya, Turkey, September 3-5, 2003.

Industry Liaison Chair

SECURWARE '10: Fourth International Conference on Emerging Security Information, Systems and Technologies, Venice, Italy, July 18 - 25, 2010.

Program Committee Service

SECURWARE '11: Fifth International Conference on Emerging Security Information, Systems and Technologies, Côte d'Azur, France, August 21 - 27, 2011.
SAC '11: 26th ACM Symposium on Applied Computing, TaiChung, Taiwan, March 21 - 25, 2011. (Technical Program Committee for Track 17: Embedded Systems: Applications, Solutions, and Techniques)
ICIMP '11: Sixth International Conference on Internet Monitoring and Protection, St. Maarten, The Netherlands Antilles, March 20 - 25, 2011.
ISQED '11: 12th International Symposium on Quality Electronic Design, Santa Clara, California, U.S.A., March 14 - 16, 2011. (Technical Program Committee for the Design Verification and Design for Testability Track)
ASP-DAC '11: 16th Asia and South Pacific Design Automation Conference, Yokohama, Japan, January 25 - 28, 2011. (Technical Program Committee for Track 6: Validation and Verification for Behavioral/Logic Design)
AI '10: 23rd Australasian Joint Conference on Artificial Intelligence, Adelaide, Australia, December 7 - 10, 2010.
SASIMI '10: 16th Workshop on Synthesis and System Integration of Mixed Information Technologies, Taipei, Taiwan, October 18 - 19, 2010. (Technical Program Committee for the Behavioral/Logic/Layout Synthesis Track)
IWSBP '10: 9th International Workshop on Boolean Problems, Freiberg, Germany, September 16 - 17, 2010.
DSD '10: 13th EUROMICRO Conference on Digital System Design: Architectures, Methods and Tools, Lille, France, September 1 - 3, 2010.
ASQED '10: Asia Symposium on Quality Electronic Design, Penang, Malaysia, August 3 - 4, 2010.
SECURWARE '10: Fourth International Conference on Emerging Security Information, Systems and Technologies, Venice, Italy, July 18 - 25, 2010.
QSIC '10: 10th International Conference on Quality Software, Zhangjiajie, China, July 14 - 15, 2010.
DATICS-ICIS '10: Workshop on Design, Analysis, and Tools for Integrated Circuits and Systems, Chengdu, China, June 23 - 25, 2010. A workshop affiliated with the 3rd International Conference on Information Sciences and Interaction Sciences (ICIS'10), Chengdu, China, June 23 - 25, 2010.
HLDVT '10: 15th IEEE International High Level Design, Validation and Test Workshop, San Francisco, California, U.S.A., June 11 - 12, 2010.
ISCAS '10: IEEE International Symposium on Circuits and Systems, Paris, France, May 30 - June 2, 2010. (Technical Program Committee for Track 6: Computer-Aided Network Design)
DATICS-FutureTech '10: Workshop on Design, Analysis, and Tools for Integrated Circuits and Systems, Busan, Korea, May 21 - 23, 2010. A workshop affiliated with the 5th International Conference on Future Information Technology (FutureTech '10), Busan, Korea, May 21 - 23, 2010.
GLSVLSI '10: 20th ACM Great Lakes Symposium on VLSI, Providence, Rhode Island, U.S.A., May 16 - 18, 2010.
ICIMP '10: Fifth International Conference on Internet Monitoring and Protection, Barcelona, Spain, May 9 - 15, 2010.
ICST '10: Third IEEE International Conference on Software Testing, Verification and Validation, Paris, France, April 6 - 9, 2010
SAC '10: 25th Annual ACM Symposium on Applied Computing, Sierre, Switzerland, March 22 - 26, 2010. (Technical Program Committee for Track 17: Embedded Systems: Applications, Solutions, and Techniques)
ISQED '10: 11th International Symposium on Quality Electronic Design, San Jose, California, U.S.A., March 22 - 24, 2010. (Technical Program Committee for the Design Verification and Design for Testability Track)
DATICS-IMECS '10: Workshop on Design, Analysis, and Tools for Integrated Circuits and Systems, Hong Kong, March 17 - 19, 2010. A workshop affiliated with the International Multiconference of Engineers and Computer Scientists (IMECS'10), Hong Kong, March 17 - 19, 2010.
DATE '10: Design, Automation and Test in Europe, Dresden, Germany, March 8 - 12, 2010. (Technical Program Committee for Track E5: Embedded Software Applications--Architectures, Tools, and Methodologies)
ASP-DAC '10: 15th Asia and South Pacific Design Automation Conference, Taipei, Taiwan, January 18 - 21, 2010. (Technical Program Committee for Track 5: Validation and Verification for Behavioral/Logic Design)
ISAIM ’10: 11th International Symposium on Artificial Intelligence and Mathematics, Ft. Lauderdale, Florida, U.S.A., January 6 - 8, 2010.
MTV '09: 10th International Workshop on Microprocessor Test and Verification, Austin, Texas, U.S.A., December 7 - 8, 2009.
HLDVT '09: 14th IEEE International High Level Design, Validation and Test Workshop, San Francisco, California, U.S.A., November 4 - 6, 2009.
ICCD '09: XXVII IEEE International Conference on Computer Design, Resort at Squaw Creek, Lake Tahoe, California, U.S.A., October 4 - 7, 2009. (Technical Program Committee for the Logic and Circuit Design Track)
ESCS '09: Workshop on Embedded Systems and Communications Security, Niagara Falls, New York, U.S.A., September 27, 2009. A workshop affiliated with the 28th International Symposium on Reliable Distributed Systems (SRDS '09), Niagara Falls, New York, U.S.A., September 27 - 30, 2009.
DSD '09: 12th EUROMICRO Conference on Digital System Design: Architectures, Methods and Tools, Patras, Greece, August 27 - 29, 2009.
QSIC '09: 9th International Conference on Quality Software, Jeju, Korea, August 24 - 25, 2009.
DATICS-ICMS '09: Workshop on Design, Analysis, and Tools for Integrated Circuits and Systems, Istanbul, Turkey, August 4 - 10, 2009. A workshop affiliated with the International Conference of Mathematical Sciences 2009 (ICMS'09), Istanbul, Turkey, August 4 - 10, 2009.
SARA '09: Eighth Symposium on Abstraction, Reformulation and Approximation, Lake Arrowhead, California, U.S.A., July 6 - 9, 2009.
SECURWARE '09: Third International Conference on Emerging Security Information, Systems and Technologies, Athens, Greece, June 14 - 19, 2009.
DATICS-ICIEA '09: Design, Analysis, and Tools for Integrated Circuits and Systems, Xi'an, China, May 25 - 27, 2009. A special session in the 4th IEEE Conference on Industrial Electronics and Applications (ICIEA'09), Xi'an, China, May 25 - 27, 2009.
ICIMP '09: Fourth International Conference on Internet Monitoring and Protection, Venice, Italy, May 24 - 28, 2009.
ISCAS '09: IEEE International Symposium on Circuits and Systems, Taipei, Taiwan, May 24 - 27, 2009. (Technical Program Committee for Track 6: Computer-Aided Network Design)
GLSVLSI '09: 19th ACM Great Lakes Symposium on VLSI, Boston, Massachusetts, U.S.A., May 10 - 12, 2009.
DATE '09: Design, Automation and Test in Europe, Nice, France, April 20 - 24, 2009. (Technical Program Committee for Track E5: Embedded Software Applications: Tools, Languages, and Methodologies)
ISQED '09: 10th International Symposium on Quality Electronic Design, San Jose, California, U.S.A., March 23 - 25, 2009. (Technical Program Committee for the Design Verification and Design for Testability Track)
DATICS-IMECS '09: Design, Analysis, and Tools for Integrated Circuits and Systems, Hong Kong, March 18 - 20, 2009. A special session in the International Multiconference of Engineers and Computer Scientists (IMECS'09), Hong Kong, March 18 - 20, 2009.
SASIMI '09: 15th Workshop on Synthesis and System Integration of Mixed Information Technologies, Okinawa, Japan, March 9 - 10, 2009. (Technical Program Committee for the Behavioral/Logic/Layout Synthesis Track)
SAC '09: 24th Annual ACM Symposium on Applied Computing, Honolulu, Hawaii, U.S.A., March 8 - 12, 2009. (Technical Program Committee for Track 9: Computational Intelligence and Image Analysis)
SAC '09: 24th Annual ACM Symposium on Applied Computing, Honolulu, Hawaii, U.S.A., March 8 - 12, 2009. (Technical Program Committee for Track 19: Embedded Systems: Applications, Solutions, and Techniques)
HLDVT '08: IEEE International High Level Design, Validation and Test Workshop, Lake Tahoe, Nevada, U.S.A., November 19 - 21, 2008.
VLSI-SOC '08: 16th IFIP International Conference on Very Large Scale Integration, Rhodes Island, Greece, October 13 - 15, 2008
ICCD '08: XXVI IEEE International Conference on Computer Design, Resort at Squaw Creek, Lake Tahoe, California, U.S.A., October 12 - 15, 2008. (Technical Program Committee for the Logic and Circuit Design Track)
IWSBP '08: 8th International Workshop on Boolean Problems, Freiberg, Germany, September 18 - 19, 2008.
DSD '08: 11th EUROMICRO Conference on Digital System Design: Architectures, Methods and Tools, Parma, Italy, September 3 - 5, 2008.
SECURWARE '08: Second International Conference on Emerging Security Information, Systems and Technologies, Cap Esterel, France, August 25 - 31, 2008.
DTVCS '08: Design, Testing, and Formal Verification Techniques for Integrated Circuits and Systems, Kailua-Kona, Hawaii, U.S.A., August 18 - 20, 2008. A special session in the IASTED International Conference on Circuits and Systems (CS '08), Kailua-Kona, Hawaii, U.S.A., August 18 - 20, 2008.
STPSA '08: 3rd IEEE International Workshop on Security, Trust, and Privacy for Software Applications, Turku, Finland, July - August, 2008. In conjunction with 32nd Annual IEEE International Computer Software and Applications Conference (COMPSAC '08), July 28 - August 1, 2008.
DATICS '08: Design, Analysis, and Tools for Integrated Circuits and Systems, Heraklion, Crete Island, Greece, July 22 - 24, 2008. A special session in the 12th WSEAS International Conference on CIRCUITS, Heraklion, Crete Island, Greece, July 22 - 24, 2008.
GLSVLSI '08: 18th ACM Great Lakes Symposium on VLSI, Orlando, Florida, U.S.A., May 4-6, 2008.
ISCAS '08: IEEE International Symposium on Circuits and Systems, Seattle, Washington, U.S.A., May 18 - 21, 2008. (Technical Program Committee for Track 6: Computer-Aided Network Design)
ISQED '08: 9th International Symposium on Quality Electronic Design, San Jose, California, U.S.A., March 17 - 19, 2008. (Technical Program Committee for the Design Verification and Design for Testability Track)
SAC '08: 23rd Annual ACM Symposium on Applied Computing, Fortaleza, Brazil, March 16 - 20, 2008. (Technical Program Committee for Track 10: Computational Logic and Computational Intelligence in Signal and Image Analysis)
SAC '08: 23rd Annual ACM Symposium on Applied Computing, Fortaleza, Brazil, March 16 - 20, 2008. (Technical Program Committee for Track 23: Embedded Systems: Applications, Solutions, and Techniques)
DATE '08: Design, Automation and Test in Europe, Munich, Germany, March 10-14, 2008. (Technical Program Committee for Track D7: Innovative and Emerging Technologies, Systems, and Applications)
ASP-DAC '08: Asia and South Pacific Design Automation Conference, Seoul, Korea, January 21 - 24, 2008. (Technical Program Committee for Track 4: Validation and Verification for Behavioral/Logic Design)
SECURWARE '07: International Conference on Emerging Security Information, Systems and Technologies, Valencia, Spain, October 14 - 20, 2007.
VLSI-SOC '07: IFIP International Conference on Very Large Scale Integration, Atlanta, Georgia, U.S.A., October 15 - 17, 2007.
SASIMI '07: 14th Workshop on Synthesis And System Integration of Mixed Information Technologies, Hokkaido, Japan, October 15 - 16, 2007. (Technical Program Committee for the Layout/Logic/Behavioral Synthesis Track)
ICCD '07: XXV IEEE International Conference on Computer Design, Resort at Squaw Creek, Lake Tahoe, California, U.S.A., October 7 - 10, 2007. (Technical Program Committee for the Logic and Circuit Design Track)
DSD '07: 10th EUROMICRO Conference on Digital System Design: Architectures, Methods and Tools, Lübeck, Germany, August 29 - 31, 2007.
STPSA '07: 2nd IEEE International Workshop on Security, Trust, and Privacy for Software Applications, Beijing, China, July 23, 2007. In conjunction with 31st Annual IEEE International Computer Software and Applications Conference (COMPSAC '07), July 23 - 27, 2007.
SARA '07: Seventh Symposium on Abstraction, Reformulation and Approximation, Whistler, British Columbia, Canada, July 18 - 21, 2007.
ICGD&BC '07: First International Conference on Global Defense and Business Continuity, Silicon Valley, California, U.S.A., July 1 - 6, 2007. (Technical Program Committee for the track TRUST: Privacy and Trust in Pervasive Communications)
ISCAS '07: IEEE International Symposium on Circuits and Systems, New Orleans, Louisiana, U.S.A., May 27 - 30, 2007. (Technical Program Committee for Track 5: Circuits and Systems for Communications)
ISCAS '07: IEEE International Symposium on Circuits and Systems, New Orleans, Louisiana, U.S.A., May 27 - 30, 2007. (Technical Program Committee for Track 6: Computer-Aided Network Design)
ISVLSI '07: IEEE Computer Society Annual Symposium on VLSI, Porto Alegre, Brazil, May 9-11, 2007.
ITNG '07: 4th International Conference on Information Technology: New Generations, Las Vegas, Nevada, U.S.A., April 2 - 4, 2007. (Technical Program Committee for the Pervasive Computing Track)
ITNG '07: 4th International Conference on Information Technology: New Generations, Las Vegas, Nevada, U.S.A., April 2 - 4, 2007. (Technical Program Committee for the Graphs & Interconnection Networks Track)
ISQED '07: 8th International Symposium on Quality Electronic Design, San Jose, California, U.S.A., March 26 - 28, 2007. (Technical Program Committee for the Design Verification and Design for Testability Track)
SAC '07: 22nd Annual ACM Symposium on Applied Computing, Seoul, Korea, March 11 - 15, 2007. (Technical Program Committee for Track 1: Artificial Intelligence, Computational Logic, and Image Analysis)
SAC '07: 22nd Annual ACM Symposium on Applied Computing, Seoul, Korea, March 11 - 15, 2007. (Technical Program Committee for Track 4: Autonomic Computing)
SAC '07: 22nd Annual ACM Symposium on Applied Computing, Seoul, Korea, March 11 - 15, 2007. (Technical Program Committee for Track 20: Embedded Systems: Applications, Solutions, and Techniques)
GLSVLSI '07: 17th ACM Great Lakes Symposium on VLSI, Stresa-Lago Maggiore, Italy, March 11 - 13, 2007.
PRDC '06: 12th IEEE International Symposium Pacific Rim Dependable Computing, Riverside, California, U.S.A., December 18 - 20, 2006.
MTV '06: 7th International Workshop on Microprocessor Test and Verification, Austin, Texas, U.S.A., December 4 - 5, 2006.
CASES '06: International Conference on Compilers, Architectures, and Synthesis for Embedded Systems, Seoul, Korea, October 23 - 25, 2006.
VLSI-SOC '06: IFIP International Conference on Very Large Scale Integration, Nice, France, October 16 - 18, 2006.
IWBP '06: 7th International Workshop on Boolean Problems, Freiberg, Germany, September 21-22, 2006.
SPTPA '06: International Workshop on Security, Privacy, and Trust for Pervasive Applications, in association with the 30th Annual International Computer Software and Applications Conference (COMPSAC'06), Chicago, Illinois, U.S.A., September 18-21, 2006.
DSD '06: 9th EUROMICRO Conference on Digital System Design: Architectures, Methods and Tools, Cavtat, Croatia, August 30 - September 1, 2006.
SAT '06: Ninth International Conference on Theory and Applications of Satisfiability Testing, Seattle, Washington, U.S.A., August 12-15, 2006.
PRICAI '06: Ninth Pacific Rim International Conference on Artificial Intelligence, Guilin, China, August 7-11, 2006.
AAAI '06: Twenty-First National Conference on Artificial Intelligence, Boston, Massachusetts, U.S.A., July 16-20, 2006.
CSR '06: International Computer Science Symposium in Russia, St. Petersburg, Russia, June 8-12, 2006.
ISCAS '06: IEEE International Symposium on Circuits and Systems, Island of Kos, Greece, May 21-24, 2006. (Technical Program Committee for Track 5: Circuits and Systems for Communications)
ISCAS '06: IEEE International Symposium on Circuits and Systems, Island of Kos, Greece, May 21-24, 2006. (Technical Program Committee for Track 6: Computer-Aided Network Design)
GLSVLSI '06: 16th Great Lakes Symposium on VLSI, Philadelphia, Pennsylvania, U.S.A., April 30 - May 2, 2006.
SAC '06: 21st Annual ACM Symposium on Applied Computing, Dijon, France, April 23-27, 2006. (Technical Program Committee for Track 1: Artificial Intelligence, Computational Logic, and Image Analysis)
SAC '06: 21st Annual ACM Symposium on Applied Computing, Dijon, France, April 23-27, 2006. (Technical Program Committee for Track 19: Embedded Systems: Applications, Solutions, and Techniques)
ITNG '06: Third International Conference on Information Technology: New Generations, Las Vegas, Nevada, U.S.A., April 10-12, 2006.
SASIMI '06: 13th Workshop on Synthesis And System Integration of Mixed Information Technologies, Nagoya, Japan, April 3-4, 2006. (Technical Program Committee for the Layout/Logic/Behavioral Synthesis Track)
ISQED '06: 7th International Symposium on Quality Electronic Design, San Jose, California, U.S.A., March 27-29, 2006. (Technical Program Committee for the Design Verification and Design for Testability Track)
PerCSA '06: International Workshop on Pervasive Computing Systems & Application, March 2006, in association with the 4th ACS/IEEE International Conference on Computer Systems and Applications (AICCSA'06), Dubai/Sharjah, United Arab Emirates, March 8-11, 2006.
DATE '06: Design, Automation and Test in Europe, Munich, Germany, March 6-10, 2006. (Technical Program Committee for Track B2: Simulation and Validation)
ISVLSI '06: IEEE Computer Society Annual Symposium on VLSI, Karlsruhe, Germany, March 2-3, 2006.
PRDC '05: 11th Pacific Rim International Symposium on Dependable Computing, Changsha, Hunan, China, December 12-14, 2005.
IP/SOC '05: 14th IP Based SoC Design Forum & Exhibition, Grenoble, France, December 7-8, 2005.
HLDVT '05: IEEE International High Level Design Validation and Test Workshop, Napa Valley, California, U.S.A., November 30 - December 2, 2005.
BCI '05: 2nd Balkan Conference in Informatics, Ohrid, Macedonia, November 17-19, 2005.
SEEFM '05: 2nd South-East European Workshop on Formal Methods, Ohrid, Macedonia, November 18-19, 2005.
ASICON '05: 6th International Conference on ASIC, Shanghai, China, October 17-20, 2005.
VLSI-SOC '05: 14th IFIP International Conference on Very Large Scale Integration, Perth, Australia, October 17-19, 2005.
CHARME '05: 13th Advanced Research Working Conference on Correct Hardware Design and Verification Methods, Saarbrücken, Germany, October 3-6, 2005.
MASCOTS '05: 13th Annual IEEE/ACM International Symposium on Modeling, Analysis, and Simulation of Computer and Telecommunication Systems, Atlanta, Georgia, U.S.A., September 27-29, 2005.
CASES '05: International Conference on Compilers, Architectures, and Synthesis for Embedded Systems, San Francisco, California, U.S.A., September 2005.
CTCES '05: Workshop on Compilers and Tools for Constrained Embedded Systems, San Francisco, California, U.S.A., September 2005. A workshop affiliated with the International Conference on Compilers, Architectures, and Synthesis for Embedded Systems (CASES '05), San Francisco, California, U.S.A., September 2005.
FTP '05: International Workshop on First-Order Theorem Proving, Koblenz, Germany, September 2005. A workshop affiliated with the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX '05), Koblenz, Germany, September 11-14, 2005.
MTV '05: Microprocessor Test and Verification, Austin, Texas, U.S.A., September 2005.
DSD '05: 8th EUROMICRO Conference on Digital System Design: Architectures, Methods and Tools, Porto, Portugal, August 30 - September 3, 2005.
ICSEng '05: 18th International Conference on Systems Engineering, Las Vegas, Nevada, August 16-18, 2005.
MWSCAS '05: 48th IEEE International Midwest Symposium on Circuits and Systems, Cincinnati, Ohio, U.S.A., August 7-10, 2005.
SARA '05: Symposium on Abstraction, Reformulation and Approximation, Edinburgh, Scotland, U.K., July 26-29, 2005.
CADE-20: 20th International Conference on Automated Deduction, Tallinn, Estonia, July 22-27, 2005.
IWSOC '05: 5th IEEE International Workshop on System-on-Chip for Real-Time Applications, Banff, Alberta, Canada, July 20-24, 2005.
AAAI '05: Twentieth National Conference on Artificial Intelligence, Pittsburgh, Pennsylvania, U.S.A., July 9-13, 2005.
MSE '05: International Conference on Microelectronic Systems Education, Anaheim, California, U.S.A., June 12-13, 2005.
ISCAS '05: IEEE International Symposium on Circuits and Systems, Kobe, Japan, May 23-26, 2005. (Technical Program Committee for Track 5: Circuits and Systems for Communications)
ISCAS '05: IEEE International Symposium on Circuits and Systems, Kobe, Japan, May 23-26, 2005. (Technical Program Committee for Track 6: Computer-Aided Network Design)
ISVLSI '05: IEEE Computer Society Annual Symposium on VLSI, Tampa, Florida, U.S.A., May 11-12, 2005.
ITCC '05: International Conference on Information Technology, Las Vegas, Nevada, U.S.A., April 11-13, 2005. (Technical Program Committee for the Pervasive Computing Track)
CEES '05: Continuous Engineering of Embedded Systems, Edinburgh, Scotland, U.K., April 9, 2005. A workshop affiliated with the European Joint Conferences on Theory and Practice of Software (ETAPS '05), Edinburgh, Scotland, U.K., April 2-10, 2005.
ISQED '05: 6th International Symposium on Quality Electronic Design, San Jose, California, U.S.A., March 28-30, 2005. (Technical Program Committee for the System Level Design, Methodologies and Tools Track)
SAC '05: 20th Annual ACM Symposium on Applied Computing, Santa Fe, New Mexico, U.S.A., March 13-17, 2005. (Technical Program Committee for Track 1: Artificial Intelligence, Computational Logic, and Image Analysis)
DATE '05: Design, Automation and Test in Europe, Munich, Germany, March 7-11, 2005. (Technical Program Committee for Track B3: System Synthesis and Optimization)
RTAS '05: 11th IEEE Real-Time and Embedded Technology and Applications Symposium, San Francisco, California, U.S.A., March 7-10, 2005.
ASP-DAC '05: Asia and South Pacific Design Automation Conference, Shanghai, China, January 18-21, 2005. (Technical Program Committee for Track 1: System Level Design Methodology)
ASP-DAC '05: Asia and South Pacific Design Automation Conference, Shanghai, China, January 18-21, 2005. (Technical Program Committee for Track 3: Behavioral / Logic Synthesis and Optimization)
VLSI Design '05: 18th International Conference on VLSI Design and 4th International Conference on Embedded Systems, Kolkata, India, January 3-7, 2005.
IP/SOC '04: 13th IP Based SoC Design Forum & Exhibition, Grenoble, France, December 8-9, 2004.
ICTAC '04: International Colloquium on Theoretical Aspects of Computing, Guiyang, China, September 20-24, 2004.
CTCES '04: Workshop on Compilers and Tools for Constrained Embedded Systems, Washington D.C., U.S.A., September 22, 2004. A workshop affiliated with the International Conference on Compilers, Architectures, and Synthesis for Embedded Systems (CASES '04), Washington D.C., U.S.A., September 23-25, 2004.
MTV '04: Microprocessor Test and Verification, Austin, Texas, U.S.A., September 9-10, 2004.
DSD '04: EUROMICRO Symposium on Digital System Design: Architectures, Methods and Tools, Rennes, France, August 31 - September 3, 2004.
AAAI '04: Nineteenth National Conference on Artificial Intelligence, San Jose, California, U.S.A., July 25-29, 2004.
ISCAS '04: IEEE International Symposium on Circuits and Systems, Vancouver, British Columbia, Canada, May 23-26, 2004. (Technical Program Committee for Track 6.6: Advances in Formal Verification)
SAT '04: Seventh International Conference on Theory and Applications of Satisfiability Testing, Vancouver, British Columbia, Canada, May 10-13, 2004.
ICCD '03: International Conference on Computer Design, San Jose, California, U.S.A., October 13-15, 2003. (Technical Program Committee for the Tools and Methodology Track)
DSD '03: EUROMICRO Symposium on Digital System Design, Antalya, Turkey, September 3-5, 2003.
PDPAR '03: Pragmatics of Decision Procedures in Automated Reasoning, a workshop affiliated with CADE-19, Miami, Florida, U.S.A., July 28-29, 2003.
MEMOCODE '03: Formal Methods and Models for Codesign, Mont Saint-Michel, France, June 24-26, 2003.
MTV '03: Microprocessor Test and Verification, Austin, Texas, U.S.A., May 29-30, 2003.
SAT '03: Sixth International Conference on Theory and Applications of Satisfiability Testing, S. Margherita Ligure - Portofino, Italy, May 5-8, 2003.
ICCD '02: International Conference on Computer Design, Freiburg, Germany, September 16-18, 2002. (Technical Program Committee for the Tools and Methodology Track)
MTV '02: Microprocessor Test and Verification, Austin, Texas, U.S.A., June 6-7, 2002.
SAT '02: Fifth International Symposium on the Theory and Applications of Satisfiability Testing, Cincinnati, Ohio, U.S.A., May 6-9, 2002.
DEL '01: Design Environments and Languages, a workshop within the Forum on Design Languages (FDL '01), Lyon, France, September 2001.

Session Organizer

MWSCAS '05, Special Session on Advances in CAD for VLSI,
48th IEEE International Midwest Symposium on Circuits and Systems, Cincinnati, Ohio, U.S.A., August 7-10, 2005.
MTV '04, Special Session on SAT,
Microprocessor Test and Verification (MTV '04), Austin, Texas, U.S.A., September 8-10, 2004.
MTV '03, Special Session on SAT and ATPG Engines,
Microprocessor Test and Verification (MTV '03), Austin, Texas, U.S.A., May 29-30, 2003.
MTV '02, Special Session on SAT and ATPG Solvers for Verification,
Microprocessor Test and Verification (MTV '02), Austin, Texas, U.S.A., June 6-7, 2002.

Session Chair

AI '09, Session: Knowledge Representation and Reasoning I
22nd Australasian Joint Conference on Artificial Intelligence (AI'09), Melbourne, Australia, December 1 - 4, 2009.
ESCS '09, Session 1
Workshop on Embedded Systems and Communications Security, Niagara Falls, New York, U.S.A., September 27, 2009. A workshop affiliated with the 28th International Symposium on Reliable Distributed Systems (SRDS '09), Niagara Falls, New York, U.S.A., September 27 - 30, 2009.
SARA '09, Session: Interval Abstraction and Abstracting Intervals
Eighth Symposium on Abstraction, Reformulation and Approximation (SARA'09), Lake Arrowhead, California, U.S.A., July 6 - 9, 2009.
ISQED '09, Session 1B: Robust Circuits
10th International Symposium on Quality Electronic Design (ISQED'09), San Jose, California, U.S.A., March 16 - 18, 2009.
ISQED '09, Session 5A: Clock and Noise
10th International Symposium on Quality Electronic Design (ISQED'09), San Jose, California, U.S.A., March 16 - 18, 2009.
HLDVT '08, Session 4: Formal Verification
IEEE International High Level Design Validation and Test Workshop (HLDVT '08), Lake Tahoe, Nevada, U.S.A., November 19 - 21, 2008.
CFV '08 and VERIFY '08, Joint Invited Talk Session: Putting Flight Software Through the Paces with Testing, Model Checking, and Constraint-Solving by Dr. Alex D. Groce (NASA-JPL), Fifth International Workshop on Constraints in Formal Verification (CFV'08) and Fifth International Verification Workshop (VERIFY’08), Sydney, Australia, August 2008. Workshops affiliated with the 4th International Joint Conference on Automated Reasoning (IJCAR 2008), Sydney, Australia, August 10 - 15, 2008.
FMCAD '07, Session 1: SAT-Based Methods
Formal Methods in Computer Aided Design (FMCAD '07), Austin, Texas, U.S.A., November 11 - 14, 2007.
HLDVT '07, Session 5: Test Generation
IEEE International High Level Design Validation and Test Workshop (HLDVT '07), Irvine, California, U.S.A., November 7 - 9, 2007.
CFV '07, Session: Advances in Decision Procedures
Fourth International Workshop on Constraints in Formal Verification (CFV '07), Bremen, Germany, July 16, 2007. A workshop affiliated with the 21st International Conference on Automated Deduction (CADE-21), Bremen, Germany, July 17 - 20, 2007.
SAT '06, Session: Applications
Ninth International Conference on Theory and Applications of Satisfiability Testing, Seattle, Washington, U.S.A., August 12 - 15, 2006.
AAAI '06 & IAAI '06, AAAI Session: Satisfiability I
Twenty-First National Conference on Artificial Intelligence (AAAI '06) and Eighteenth Innovative Applications of Artificial Intelligence Conference (IAAI '06), Boston, Massachusetts, U.S.A., July 16 - 20, 2006.
AAAI '06 & IAAI '06, AAAI Session: Bayesian Networks
Twenty-First National Conference on Artificial Intelligence (AAAI '06) and Eighteenth Innovative Applications of Artificial Intelligence Conference (IAAI '06), Boston, Massachusetts, U.S.A., July 16 - 20, 2006.
ISQED '06, Session: Digital Test and Diagnosis Techniques
7th International Symposium on Quality Electronic Design (ISQED'06), San Jose, California, March 27 - 29, 2006.
AAAI '05 & IAAI '05, AAAI Session: Automated Reasoning
Twentieth National Conference on Artificial Intelligence (AAAI '05) and Seventeenth Innovative Applications of Artificial Intelligence Conference (IAAI '05), Pittsburgh, Pennsylvania, U.S.A., July 9 - 13, 2005.
AAAI '05 & IAAI '05, AAAI Session: Constraint Satisfaction 3
Twentieth National Conference on Artificial Intelligence (AAAI '05) and Seventeenth Innovative Applications of Artificial Intelligence Conference (IAAI '05), Pittsburgh, Pennsylvania, U.S.A., July 9 - 13, 2005.
HLDVT '04, Session 7: SAT Solving Approaches
IEEE International High Level Design Validation and Test Workshop (HLDVT '04), Sonoma Valley, California, U.S.A., November 10 - 12, 2004.
ICCD '04, Session 7.1: Formal Verification Techniques
22nd International Conference on Computer Design (ICCD '04), San Jose, California, U.S.A., October 11 - 13, 2004.
AAAI '04 & IAAI '04, AAAI Session: SAT
Nineteenth National Conference on Artificial Intelligence (AAAI '04) and Sixteenth Innovative Applications of Artificial Intelligence Conference (IAAI '04), San Jose, California, U.S.A., July 25 - 29, 2004.
AAAI '04 & IAAI '04, AAAI Session: MAX-SAT
Nineteenth National Conference on Artificial Intelligence (AAAI '04) and Sixteenth Innovative Applications of Artificial Intelligence Conference (IAAI '04), San Jose, California, U.S.A., July 25 - 29, 2004.
AAAI '04 & IAAI '04, AAAI Session: Syntax & Semantics
Nineteenth National Conference on Artificial Intelligence (AAAI '04) and Sixteenth Innovative Applications of Artificial Intelligence Conference (IAAI '04), San Jose, California, U.S.A., July 25 - 29, 2004.
AAAI '04 & IAAI '04, AAAI Session: Temporal Reasoning
Nineteenth National Conference on Artificial Intelligence (AAAI '04) and Sixteenth Innovative Applications of Artificial Intelligence Conference (IAAI '04), San Jose, California, U.S.A., July 25 - 29, 2004.
ICCD '02, Session 8.1: System Design Issues
International Conference on Computer Design (ICCD '02), Freiburg, Germany, September 16 - 18, 2002.
MTV '02, Session F: Semi-Formal Verification
Microprocessor Test and Verification (MTV '02), Austin, Texas, U.S.A., June 6 - 7, 2002.
VLSI-SOC '01, Session 11.a: Verification & Validation (2)
11th IFIP International Conference on Very Large Scale Integration, The Global System on Chip Design & CAD Conference (VLSI-SOC '01), Montpellier, France, December 2001.

Other professional activities

Patents Pending

P3: M.N. Velev, Method for Formal Verification of Liveness of Pipelined Microprocessors.
P2: M.N. Velev, Method for Elimination of Relational Operators in Translation to Boolean Logic.
P1: M.N. Velev, Method for Representation of Formulas for Efficient Satisfiability Solving.

Publications

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

J6: M.N. Velev, Automatic Formal Proof of Liveness for Pipelined Microprocessors, accepted to appear in Journal of Systems Architecture (JSA), Special Issue on New Architectures, Methods, and Tools for Circuit and System Synthesis, 2004.
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: M.N. Velev, and R.E. Bryant, Effective Use of Boolean Satisfiability Procedures in the Formal Verification of Superscalar and VLIW Microprocessors, Journal of Symbolic Computation (JSC), Vol. 35, No. 2 (February 2003), pp. 73-106.
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: R.E. Bryant, S. German, and M.N. Velev, Processor Verification Using Efficient Reductions of the Logic of Uninterpreted Functions to Propositional Logic, ACM Transactions on Computational Logic (TOCL), Vol. 2, No. 1 (January 2001), pp. 93-134.

Conference Papers

C44: M.N. Velev, and P. Gao, Method for Formal Verification of Soft-Error Tolerance Mechanisms in Pipelined Microprocessors, accepted to appear in 12th International Conference on Formal Engineering Methods (ICFEM '10), November 2010.
C43: M.N. Velev, and P. Gao, Efficient Pseudo-Boolean Satisfiability Encodings for Routing in Optical Networks, accepted to appear in International Conference on Operations Research (OR ’10), September 2010.
C42: M.N. Velev, and P. Gao, A Method for Debugging of Pipelined Processors in Formal Verification by Correspondence Checking, 15th 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, 11th International Symposium on Artificial Intelligence and Mathematics (ISAIM ’10), January 2010. [Invited talk]
C40: M.N. Velev, and P. Gao, Efficient SAT Techniques for Relative Encoding of Permutations with Constraints, 22nd 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, 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 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, 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 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 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.
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, 38th 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, 37th 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.
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: M.N. Velev, and R.E. Bryant, Exploiting Positive Equality and Partial Non-Consistency in the Formal Verification of Pipelined Microprocessors, 36th Design Automation Conference (DAC '99), June 1999, pp. 397-401.
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

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), part of 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, 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

T4: M.N. Velev, and R.E. Bryant, Formal Verification of Superscalar Microprocessors with Multicycle Functional Units, Exceptions, and Branch Prediction, Technical Report CMU-CS-00-116, Carnegie Mellon University, 2000.
T3: R.E. Bryant, and M.N. Velev, Boolean Satisfiability with Transitivity Constraints, Technical Report CMU-CS-00-101, Carnegie Mellon University, 2000.
T2: R.E. Bryant, S. German, and M.N. Velev, Processor Verification Using Efficient Reductions of the Logic of Uninterpreted Functions to Propositional Logic, Technical Report CMU-CS-99-115, Carnegie Mellon University, 1999.
T1: B. Rychlik, J.W. Faistl, B.P. Krug, A.Y. Kurland, J.J. Jung, M.N. Velev, and J.P. Shen, Efficient and Accurate Value Prediction Using Dynamic Classification, CMuART Technical Report CMuART-1998-01, Carnegie Mellon University, 1998.

Benchmark Suites

SAT benchmarks in CNF format (some suites are also available in BLIF, ISCAS, and Trace formats)