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.

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.

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.

Hyatt Place San Jose Downtown

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.

Uproar Brewing Company, 439 S 1st St, San Jose

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(r) Processor ISA features. His early years at Intel included performance and floating-point architecture development on the Pentium (r) 4 Processor family.