FMCAD 2019: FORMAL METHODS IN COMPUTER-AIDED DESIGN 2019
PROGRAM

Days: Tuesday, October 22nd Wednesday, October 23rd Thursday, October 24th Friday, October 25th

Tuesday, October 22nd

View this program: with abstractssession overviewtalk overview

10:00-12:00 Session 1: (Tutorial 1) Nadia Polikarpova, SuSLik: Synthesis of Safe Pointer-Manipulating Programs

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.

13:00-15:00 Session 2: (Tutorial 2) Mark Greenstreet, Integrating SMT with Theorem Proving for Verification of Analog and Mixed-Signal Circuits

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.

15:30-17:30 Session 3: (Tutorial 3) Avi Ziv, Challenges and Solutions in Post-Silicon Validation of High-end Processors

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.

Wednesday, October 23rd

View this program: with abstractssession overviewtalk overview

09:00-10:00 Session 4: Hardware Verification (Part 1)
09:00
Boosting Verification Scalability via Structural Grouping and Semantic Partitioning of Properties (abstract)
09:30
Input Elimination Transformations for Scalable Verification and Trace Reconstruction (abstract)
10:30-11:30 Session 5: Hardware Verification (Part 2)
10:30
Chasing Minimal Inductive Validity Cores in Hardware Model Checking (abstract)
11:00
Verifying Large Multipliers by Combining SAT and Computer Algebra (abstract)
13:30-15:00 Session 7: Software Vertification
13:30
Unification-based Pointer Analysis without Oversharing (abstract)
14:00
Concurrent Chaining Hash Map for Software Model Checking (abstract)
14:30
Proving Data Race Freedom in Task Parallel Programs with a Weaker Partial Order (abstract)
15:30-17:00 Session 8: Network Verification and Synthesis
15:30
BDD-Based Algorithms for Packet Classification (abstract)
16:00
TSNsched: Automated Schedule Generation for Time Sensitive Networking (abstract)
16:30
Verification and Synthesis of Symmetric Uni-Rings for Leads-To Properties (abstract)
Thursday, October 24th

View this program: with abstractssession overviewtalk overview

09:00-10:00 Session 9: Keynote: Safe and Interactive Autonomy: A Journey Starting from Formal Methods, Dorsa Sadigh, Stanford

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.

10:30-12:00 Session 10: Verification of Large Systems
10:30
Scalable Translation Validation of Unverified Legacy OS Code (abstract)
11:00
Kaizen: Building a Performant Blockchain System Verified for Consensus and Integrity (abstract)
11:30
KAIROS: Incremental Verification in High-Level Synthesis through Latency-Insensitive Design (abstract)
13:30-14:30 Session 12: Security and Safety
13:30
Verification of Authenticated Firmware Loaders (abstract)
14:00
Learning-Based Synthesis of Safety Controllers (abstract)
15:00-16:30 Session 13: Synthesis for Reactive Systems
15:00
Shield Synthesis for Real: Enforcing Safety in Cyber-Physical Systems (abstract)
15:30
Syntroids: Synthesizing a Game for FPGAs using Temporal Logic Specifications (abstract)
16:00
Synthesizing Reactive Systems Using a Robustness Specification (abstract)
Friday, October 25th

View this program: with abstractssession overviewtalk overview

09:00-10:00 Session 15: Keynote: An Increasing Need for Formality, Martin Dixon, Fellow, Intel

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.

10:30-12:00 Session 16: Reasoning about Relational Constraints
10:30
Property Directed Inference of Relational Invariants (abstract)
11:00
Knowledge Compilation for Boolean Functional Synthesis (abstract)
11:30
Verifying Relational Properties using Trace Logic (abstract)
13:00-14:30 Session 17: Quantifiers and SAT
13:00
Autarkies for DQCNF (abstract)
13:30
Localizing Quantifiers for DQBF (abstract)
14:00
Anytime Weighted MaxSAT with Improved Polarity Selection and Bit-Vector Optimization (abstract)
15:00-16:30 Session 18: SMT based Verification
15:00
GuidedSampler: Coverage-guided Sampling of SMT Solutions (abstract)
15:30
Extending enumerative function synthesis via SMT-driven classification (abstract)
16:00
Proving Non-Termination via Loop Acceleration (abstract)