Title: Secure Verification Platform based on HOL and MDG

Speaker: Otmane Ait Mohamed, Ph.D., 

　　　　　Associate Professor

　　　　　Electrical and Computer Engineering Department

　　　　　Concordia University, Montreal, Quebec, Canada

Time:3:00pm, March 1

Venue: Lecture room, Lab for Computer Science, Level 3 Building #5, Institute of Software, CAS

Abstract:

Formal verification of digital systems is achieved, today,  using one of two main approaches: states exploration  (mainly model checking and equivalence checking) or 　deductive reasoning (theorem proving). Indeed, the combination of the 　two approaches, states exploration and deductive reasoning promises to 　overcome the limitation and to enhance the capabilities of each. 　A comparison between both categories is discussed in details. 　We are interested in presenting a verification platform based on 　Multiway Decision Graphs (MDGs) and HOL theorem prover. 　Based on this platform, many conversions such as the reachability analysis  and reduction techniques can be implemented that uses the MDG theory within  the HOL theorem prover. We will discuss the best formalization principle  of decision graphs to build such a platform in theorem proving since a set  of basic operations are used to efficiently manipulate the decision graphs  which constitute the kernel of the model checking algorithms, by describing  two alternatives to formalize these decision graphs. Then we contrast between  them according to their efficiency, complexity and feasibility.

Biography:

Dr. Otmane Ait Mohamed received his Ph.D. (1996) in Computer Science from Université Henri Poincaré, Nancy 1. Before his arrival at Concordia in 2002, he worked as a Postdoctoral Fellow at Université de Montréal, a Research Scientist at Cistel, and a Senior Verification Engineer at Nortel Networks in Ottawa. Dr. Ait Mohamed has been working on formal verification for hardware and  communication protocol since 1992. He contributed to the development of the MDG tool, a formal verification tool developed at the University of Montreal from 1996-1998. He joined Cistel Technology, and then Nortel Networks where he introduced the use of formal method techniques in the hardware design flow to identify critical issues in the protocols used in Nortel’s Virtual Processor Subsystems. His work with the verification team consisted of verifying four different ASICs used in the communication data switch. His main research areas include hardware model checking, assertion based verification, automatic test generations, and FPGA-based design and verification. He is the principal or co-investigator of several team grants from agencies such as NATEQ, MDEIE, and various companies. Dr. Ait Mohamed also served as a reviewer for several related conferences and journals and he maintains collaborations with AMD, ST, Synopsys, Texas Instruments, and Qualcomm. Dr. Ait Mohamed was the program co-chair for the prestigious 21st TPHOLs conference in 2008. He is a registered  professional engineer with the Ordre des ingénieurs du Québec, member of IEEE, and member of ACM. He is a Concordia representative in the executive committee of RESMiQ, the largest strategic microelectronic alliance in Québec.