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