LOGO
Formal Methods in
Computer-Aided Design
Oct 22 - 25, 2019
Hyatt Place San Jose Downtown, San Jose, California, USA

Tutorials and Keynotes

Tutorials

The tutorials will take place on October 22, 2019.

Nadia Polikarpova, UCSD

SuSLik: Synthesis of Safe Pointer-Manipulating Programs  slides

Abstract: SuSLik is a program synthesizer that generates provably safe pointer-manipulating programs automatically from high-level specifications. More precisely, the input to SuSLik is a pair of assertions in separation logic, which describe what the heap looks like before and after executing the program. Using only this information, SuSLik is able to synthesize a wide range of operations on linked data structures, such as singly- and doubly-linked lists, sorted lists, and trees. In this tutorial you will get hands-on experience with SuSLik (bring your laptops!) and learn how synthesis is made possible by a novel proof system we call synthetic separation logic. Experience with separation logic and program synthesis is helpful but not required.

Bio: Nadia Polikarpova is an assistant professor at CSE, and a member of the Programming Systems group. She received her Ph.D. in computer science from ETH Zurich in 2014. She then spent three years as a postdoctoral researcher at MIT. Dr. Polikarpova’s work spans the areas of programming languages and formal methods; in particular, she is interested in building practical tools and techniques that make it easier for programmers to construct secure and reliable software.

Mark Greenstreet, UBC

Integrating SMT with Theorem Proving for Verification of Analog and Mixed-Signal Circuits  slides

Abstract: The complementary strengths of interactive theorem proving and SMT solvers have motivated several efforts at integration including Sledgehammer for Isabelle/HOL, CoqSMT. The goal of these efforts is to combine the generality of interactive theorem provers, especially support for inductive proofs, with the automation of SMT solvers for discharging tedious subgoals. In practice, such efforts have been hindered by the gaps between the logic of the theorem prover and the SMT solver. Typically, goals in the theorem prover are expressed in an untyped logic, making often making extensive use of recursive functions and quantifiers. In contrast, the logic of SMT solvers is first-order, many-sorted, and lacks recursive functions. In practice, the effort to transform proof goals into formulations that are amenable to SMT techniques can dominate the proof effort.

This tutorial describes Smtlink, our integration of Z3 into ACL2, and presents examples demonstrating the effectiveness of the approach. Smtlink makes extensive use of reflection. By inspecting proof goals and extracting already proven facts, Smtlink automates much of the translation of goals from the untyped logic of ACL2 to the many-sorted logic of Z3. From the user’s perspective, Smtlink can discharge goals that include user-defined data types, recursive functions, and whose proofs build on previously established theorems.

We present several examples from analog and mixed-signal circuits. We also present a simple proof of the Cauchy-Schwartz inequality. In our experience, these proofs were surprisingly straightforward: we identified the obvious, inductive lemmas, and these lemmas were discharged without further effort by the user. As we will show with these examples, the SMT integration makes the theorem proving process productive and fun.

This tutorial is based on joint work with Carl Kwan and Yan Peng.

Bio: Mark Greenstreet is a Professor in the Department of Computer Science at the University of British Columbia. His research interests span a wide range of topics in formal verification and VLSI design, especially, analog, mixed-signal, and asynchronous circuits. Dr. Greenstreet earned his Ph.D. at Princeton University (1992) and his B.Sc. at Caltech (1981). Between Caltech and Princeton, he was a chip designer at ESL, a TRW subsidiary, and a guest researcher at Aarhus University, in Denmark. While at UBC, Dr. Grenstreet has enjoyed collaborations with R&D groups at many companies including Intel, Oracle, Rambus, and SUN Microsystems.

Avi Ziv, IBM

Challenges and Solutions in Post-Silicon Validation of High-end Processors  slides

Abstract: Due to the complexity of designs, post-silicon validation remains a major challenge with few systematic solutions. In this tutorial, we describe the main challenges in post-silicon validation of high-end processors and provide an overview of the state-of-the-art post silicon validation process used by IBM to verify its latest IBM POWER9 processor. We focus on numerous innovations that led to discovery of 30% more bugs in 20% less time over the previous generation. We demonstrate our methodology by describing several bugs from fail detection to root cause.

Bio: Dr. Avi Ziv is a Research Staff Member in the Hardware Verification Technologies Department at the IBM Research Laboratory in Haifa, Israel. Since joining IBM in 1996, Avi has been working on developing technologies and methodologies for various topics of simulations-based functional verification including stimuli generation, checking, functional coverage, coverage directed generation and post-silicon validation.

Avi received the B.Sc. degree in Computer Engineering from the Technion - Israel Institute of Technology in 1990 and the M.Sc. and Ph.D. degrees in Electrical Engineering from Stanford University in 1992 and 1995, respectively. He is the author of more than 50 papers and the inventor of more than 10 patents, mostly in the area of functional verification.

Keynotes

Dorsa Sadigh, Stanford University

Safe and Interactive Autonomy: A Journey Starting from Formal Methods  slides

Abstract: Today’s society is rapidly advancing towards autonomous systems that interact and collaborate with humans, e.g., semiautonomous vehicles interacting with drivers and pedestrians, medical robots used in collaboration with doctors, or service robots interacting with their users in smart homes. With the emergence of autonomous systems in our every day lives, we need to design algorithms and tools that enable safe and seamless interactions with people.

In this talk, I will start with my journey in providing safety for human-robot systems by discussing a spectrum of views on safe autonomous systems including a formal methods perspective for synthesizing provably correct controllers, a robust control approach, and more recent advances in safe learning and verification. I will then discuss one of the main challenges of safety of human-robot systems, i.e., studying how robots influence humans’ actions in one-on-one or group settings. This is usually overlooked by assuming humans act as external disturbances just like moving obstacles, or assuming that automation can always help societies without actually considering how humans can be impacted. I will talk about our recent work in building computational models of human behavior from expert demonstrations and preferences in interaction with autonomous systems and challenges it introduces for safety and robustness verification.

Bio: Dorsa Sadigh is an assistant professor in Computer Science and Electrical Engineering at Stanford University. Her research interests lie in the intersection of robotics, learning and control theory, and algorithmic human-robot interaction. Specifically, she works on developing efficient algorithms for autonomous systems that safely and reliably interact with people. Dorsa has received her doctoral degree in Electrical Engineering and Computer Sciences (EECS) at UC Berkeley in 2017, and has received her bachelor’s degree in EECS at UC Berkeley in 2012. She is awarded the Amazon Faculty Research Award, the NSF and NDSEG graduate research fellowships as well as the Leon O. Chua departmental award.

Martin Dixon, Intel

An Increasing Need for Formality

Abstract: The talk will touch on a number of practical opportunities for formal modeling and methods that Intel sees in HW security research including: instruction sets; the proliferation of programmable agents within SoC’s; and negative space testing.

Bio: Martin G. Dixon is an Intel Fellow. He is responsible for guiding future research and architecture decisions to secure Intel’s platforms. He defined and holds patents on new instruction set features for many of the Core® Processor ISA features. His early years at Intel included performance and floating-point architecture development on the Pentium ® 4 Processor family.