Keynotes
| Speaker | Affiliation | Keynote Title | Slides |
| Ziyad Hanna | Cadence Design Systems | Democratization of Formal Verification with Collective Intelligence | [Slides] |
| Sharad Malik | Princeton University | Detecting Hardware Trojans: A Tale of Two Techniques | [Slides] |
| Allen Emerson | The University of Texas at Austin | The Genesis and Development of Model Checking: Fact vs. Fiction |
Abstracts
Title: Democratization of Formal Verification with Collective IntelligenceSpeaker: Ziyad Hanna
Day: Monday, September 28
Formal verification has become an essential method for design, integration and verification of the emerging design IPs and complex systems-on-chips. Despite the great success in proliferating formal in the industry and making it a great companion to simulation and emulation methods, its full power has not been leveraged yet to address the larger spectrum of applications by non-formal experts. To handle this challenge a major effort is still needed to boost its scalability and usability to cope with the emerging complexity of design under verification. In this talk we discuss a new approach for boosting the productivity of formal verification users using an expert system, which is powered by collective intelligence technology, human-machine interface and self guiding and learning rules. Besides the emerging advancements in model checking and proof strategies, expert system helps to break the formal verification complexity and scalability barriers, and make it affordable for a larger set of users, for yet another major leap in the applications and productivity of formal.
Title: Detecting Hardware Trojans: A Tale of Two Techniques
Speaker: Sharad Malik
Day: Tuesday, September 29
Integrated Circuits (ICs) are designed and fabricated in a globalized multi-vendor environment making them vulnerable to malicious design changes and the insertion of hardware Trojans/malware. In this talk I will cover two distinct techniques to address the problem of detecting hardware Trojans. The first uses SAT and BDD-based functional analysis to reverse engineer ICs. The goal here is to derive the higher- level function of IC through algorithmic analysis of its netlist to help expose the Trojan logic. The second uses statistical analysis of chip simulation data in a clustering algorithm to isolate the Trojan logic. I will discuss these techniques, their practical application on benchmark circuits and their complementary strengths.
This is joint work with Burcin Cakir and Pramod Subramanyan.
Title: The Genesis and Development of Model Checking: Fact vs. Fiction
Speaker: Allen Emerson
Day: Wednesday, September 30
Clarke and Emerson are noted for the invention and development of model checking [CE81]. In this presentation, I will recall the roles of the principals. I was responsible for the initial conception of model checking, as a spinoff of my work on program synthesis. This entailed the checking of candidate models of a temporal specification algorithmically, and explains the coining of the term model checking. Model checking plainly was a form of verification circumventing proofs. As a part of some consulting work, Ed Clarke had been consulting on verification of protocols using temporal specifications and deductive proofs. As I discussed model checking with Ed, he envisioned that it could be a really practical verification method, applicable to protocols and more. Later, Ed commented that neither one of us could have achieved model checking without the other.
There are alternative perspectives on this history. In broad brush, these agree, but they vary in detail. I will elaborate with additional crucial facts, and examine their impact on various apparent discrepancies. I would like to suggest the relevance of Pnueli's Principle here: The junior researcher lives in the problem, while the senior researcher lives in a constant stream of interrupts. A Corollary is: The junior researcher will singlemindedly acquire a detailed memory concerning the problem and its solution; The overburdened, timesharing senior researcher will lack sufficient focused attention, blocks of time, and depth of understanding to have good recall.
[CE81] Edmund M. Clarke and E. Allen Emerson: Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic. Logics of Programs, Workshop, Yorktown Heights, New York, May 1981.