MOUNTAIN VIEW, Calif.—(BUSINESS WIRE)—April 22, 2008— Jasper Design Automation, the leader in successful deployment of production-proven formal verification solutions, today named Tom Melham and Moshe Vardi as the newest members of its Technical Advisory Board (TAB). Tom Melham is a Professor of Computer Science at the University of Oxford and a Fellow of Balliol College. He is well-known for his technical contributions and publications on combined model checking and theorem proving, industrial-scale hardware verification, abstraction techniques, and for integrating formal verification into hardware design methodologies. Moshe Vardi is a Professor of Computer Science at Rice University, the Karen Ostrum George Professor in Computational Engineering, and Director of the Ken Kennedy Institute for Information Technology. The author of over 300 technical papers, as well as the editor of several collections, Prof. Vardi is a renowned expert in model checking, constraint satisfaction and database theory, common knowledge (logic), and theoretical computer science.

"In my research work, I have been applying formal techniques to RTL at the micro-architecture level," stated Prof. Melham. "I am pleased to be joining the Jasper TAB to advance the technology pipeline for applying formal technologies throughout the whole design and verification cycle, from architecture to silicon. I see Jasper taking the lead in formal technology applications at the architecture level, helping chip companies alleviate the most troubling downstream design and verification challenges."

Prof. Melham received his Ph.D. in 1990 from the University of Cambridge for his foundational research in formal hardware verification and mechanized reasoning, and was a co-developer of the original HOL theorem prover for higher order logic at Cambridge. In 1993, he joined the Computing Science Department at Glasgow University. He was appointed to a Professorship of Computing Science at Glasgow in 1998, before moving to Oxford in 2002. He was elected a Fellow of the Royal Society of Edinburgh in 2002.

"Having been involved with formal verification research and development for 25 years, I am excited about joining Jasper's TAB to participate in the ongoing development and growing proliferation of formal verification across a wide variety of horizontal industry segments,” stated Moshe Vardi. “With the rising importance of high-level models in design, formal verification is becoming critical to the industry. I expect Jasper to play a major role in this market."

Prior to joining Rice University, Prof. Vardi was at the IBM Almaden Research Center, where he managed the Mathematics and Related Computer Science Department. Vardi is the recipient of three IBM Outstanding Innovation Awards, and a co-winner of the 2000 Gödel Prize, the 2005 ACM Paris Kanellakis Award for Theory and Practice, and the LICS 2006 Test-of-Time Award. He holds honorary doctorates from the University of Saarland, Germany, and the University of Orleans, France, and received his Ph.D. from the Hebrew University of Jerusalem in 1981.

"We are delighted to welcome Moshe and Tom to our technical advisory board, and pleased to be working with two of the industry’s most respected formal verification visionaries," said Ziyad Hanna, chief architect and vice president of research at Jasper Design Automation. “These two gentlemen have contributed greatly to formal verification research and development, and will help Jasper advance its formal technology leadership."

About Jasper’s Technical Advisory Board

Jasper’s Technical Advisory Board (TAB) is made up of verification luminaries from the academic and commercial worlds. The TAB’s purpose is to advise Jasper’s management team on research trends in formal verification and formal technology exploration and expansion. The TAB also provides valued guidance on Jasper’s technical product development, and educates students and the market on trends in formal verification.

In addition to Tom Melham and Moshe Vardi, the TAB currently includes Brian Bailey, renowned verification industry veteran; Alan Hu, associate head of the Department of Computer Science at the University of British Columbia; Sharad Malik, professor in the Department of Electrical Engineering, Princeton University; and Satoshi Goto, professor at the Graduate School of Information, Production and Systems, Waseda University, Kitakyushu, Japan.

About Jasper Design Automation

Jasper Design Automation’s production-proven formal verification solutions are used by logic designers, verification engineers and silicon bring-up teams to design, explore and debug RTL, to ensure correctness of block-level functionality and for rapid post-silicon validation and debug. JasperGold® Verification System delivers complete “deep formal” systematic verification, ensuring correctness of critical design features without any testbench development. JasperGold Express, a “light formal” solution, complements simulation by accelerating bug-hunting and coverage attainment. For expert help with large scale formal verification deployment, RTL exploration or post-silicon debug, please visit http://www.jasper-da.com.

Jasper Design Automation, the Jasper Design Automation logo, JasperGold, Formal Testplanner, GamePlan, Proof Accelerators, Lossless Abstractions, Formal Scoreboard, and Design Tunneling are trademarks or registered trademarks of Jasper Design Automation, Inc. All other names mentioned are trademarks, registered trademarks, or service marks of their respective companies.