FMCAD 2022: FORMAL METHODS IN COMPUTER-AIDED DESIGN
PROGRAM

Days: Tuesday, October 18th Wednesday, October 19th Thursday, October 20th Friday, October 21st

Tuesday, October 18th

View this program: with abstractssession overviewtalk overview

09:00-11:00 Session 2: VSTTE Tutorial

Sanjit Seshia. Towards Verified Artificial Intelligence with Scenic and VerifAI

Abstract. Verified artificial intelligence (AI) is the goal of designing AI-based systems that have strong, verified assurances of safety and trustworthiness with respect to mathematically-specified requirements. This goal is particularly important for AI-based autonomous and semi-autonomous systems. In this tutorial, I will describe the main technical challenges for achieving Verified AI, survey some of the existing solutions, and outline some promising directions for future work. In particular, I will present Scenic and VerifAI, two open-source software systems for the formal modeling, design, analysis, and synthesis of systems that include AI and machine learning components. Scenic is a probabilistic programming system for formal modeling and data generation. VerifAI is an algorithmic toolkit supporting a variety of use cases including writing multi-modal system-level specifications, simulation-based verification and testing, automated diagnosis of errors, specification-driven parameter synthesis and retraining, and run-time assurance. The tutorial concepts will be illustrated with examples from the domain of intelligent cyber-physical systems, with a particular focus on deep neural network-based autonomy in transportation systems.

11:30-12:30 Session 4: FMCAD Tutorial 1 (part 1)

Oded Padon. Verification of Distributed Protocols: Decidable Modeling and Invariant Inference

Abstract. Verification of distributed protocols and systems, where both the number of nodes in the systems and the state-space of each node are unbounded, is a long-standing research goal. In recent years, efforts around the Ivy verification tool have pushed a strategy of modeling distributed protocols and systems in a new way that enables decidable deductive verification, i.e., given a candidate inductive invariant, it is possible to automatically check if it is inductive, and to produce a finite counterexample to induction in case it is not inductive. Complex protocols require quantifiers in both models and their invariants, including forall-exists quantifier alternations. Still, it is possible to obtain decidability by enforcing a stratification structure on quantifier alternations, often achieved using modular decomposition techniques, which are supported by Ivy. Stratified quantifiers lead not only to theoretical decidability, but to reliably good solver performance in practice, which is in contrast to the typical instability of SMT solvers over formulas with complex quantification.

Reliable automation of invariant checking and finite counterexamples open the path to automating invariant inference. An invariant inference algorithm can propose a candidate invariant, automatically check it, and get a finite counterexample that can be used to inform the next candidate. For a complex protocol, this check would typically be performed thousands of times before an invariant is found, so reliable automation of invariant checking is a critical enabler. Recently, several invariant inference algorithms have been developed that can find complex quantified invariants for challenging protocols, including Paxos and some of its most intricate variants.

In the tutorial I will provide an overview of Ivy’s principles and techniques for modeling distributed protocols in a decidable fragment of first-order logic. I will then survey several recently developed invariant inference algorithms for quantified invariants, and present one such algorithm in depth: Primal-Dual Houdini. Primal-Dual Houdini is based on a new mathematical duality, and is obtained by deriving the formal dual of the well-known Houdini algorithm. As a result, Primal-Dual Houdini possesses an interesting formal symmetry between the search for proofs and for counterexamples.

13:30-14:30 Session 6: FMCAD Tutorial 1 (part 2)

Oded Padon. Verification of Distributed Protocols: Decidable Modeling and Invariant Inference

14:30-15:30 Session 7: FMCAD Tutorial 2 (part 1)

Håkan Hjort. On applying Model Checking in Formal Verification

Abstract. Use of Hardware model checking in the EDA industry is wide spread and now considered an essential part of verification. While there are many papers, and books, about SAT, SMT and Symbolic model checking, often very little is written about how these methods can be applied. Choices made when modeling systems can have large impacts on applicability and scalability. There is generally no formal semantics defined for the hardware design languages, nor for the intermediate representations in common use. As unsatisfactory as it may be, industry conventions and behaviour exhibited by real hardware have instead been the guides. In this tutorial we will give an overview of some of the steps needed to apply hardware model checking in an EDA tool. We will touch on synthesis, hierarchy flattening, gate lowering, driver resolution, issues with discrete/synchronous time models, feedback loops and environment constraints, input rating and initialisation/reset.

16:00-17:00 Session 9: FMCAD Tutorial 2 (part 2)

Håkan Hjort. On applying Model Checking in Formal Verification

18:00-20:00 FMCAD reception

Welcome reception at the Grand Hotel Trento

Wednesday, October 19th

View this program: with abstractssession overviewtalk overview

09:00-10:00 Session 11: Invited Talk 1

June Andronick. The seL4 verification journey: how have the challenges and opportunities evolved

Abstract. The formal verification journey of the seL4 microkernel is nearing two decades, and still has an busy roadmap for the years ahead. It started as a research project aiming for a highly challenging problem with the potential of significant impact. Today, a whole ecosystem of developers, researchers, adopters and supporters are part of the seL4 community. With increasing uptake and adoption, seL4 is evolving, supporting more platforms, architectures, configurations, and features. This creates both opportunities and challenges: verification is what makes seL4 unique; as the seL4 code evolves, so must its formal proofs. With more than a million lines of formal, machine-checked proofs, seL4 is the most highly assured OS kernel, with proofs of an increasing number of properties (functional correctness, binary correctness, security –integrity and confidentiality– and system initialisation) and for an increasing number of hardware architectures: Arm (32-bit), x86 (64-bit) and RISC-V (64-bit), with proofs now starting for Arm (64-bit). In this talk we will reflect on the evolution of the challenges and opportunities the seL4 verification faced along its long, and continuing, journey.

10:30-12:00 Session 13: ML Verification
10:30
Proving Robustness of KNNs Against Adversarial Data Poisoning (abstract)
10:55
On Optimizing Back-Substitution Methods for Neural Network Verification (abstract)
11:20
Verification-Aided Deep Ensemble Selection (abstract)
11:35
Neural Network Verification with Proof Production (abstract)
12:00-12:40 Session 14: Student forum talks - Part 1
Partial Order Reduction for Abstraction-Based Verification of Concurrent Software (abstract)
Axiomatic Analysis of Distributed Systems (abstract)
Lazy Abstraction for Probabilistic Systems (abstract)
A Formalization of Heisenbugs and Their Causes (abstract)
Fine-Grained Reconstruction of cvc5 Proofs in Isabelle/HOL (abstract)
Tuning the Learning of Circuit-Based Classifiers (abstract)
Verification-Driven Ensemble Selection (abstract)
Formal Verification of Algebraic Effects (abstract)
Lazy abstraction for time in eager CEGAR (abstract)
Symbolic Coloured Model Checking for HCTL (abstract)
Strategies for Parallel SMT Solving (abstract)
14:00-15:30 Session 16: Hardware and RTL - Part 1
14:00
Formally Verified Isolation of DMA (abstract)
14:25
Foundations and Tools in HOL4 for Analysis of Microarchitectural Out-of-Order Execution (abstract)
14:50
Synthesizing Instruction Selection Rewrite Rules from RTL using SMT (abstract)
15:15
Error Correction Code Algorithm and Implementation Verification using Symbolic Representations (abstract)
16:00-17:20 Session 18: SAT and SMT - Part 1
16:00
Compact Symmetry Breaking for Tournaments (abstract)
16:25
Enumerative Data Types with Constraints (abstract)
16:50
Reducing NEXP-complete problems to DQBF (abstract)
17:05
Bounded Model Checking for LLVM (abstract)
Thursday, October 20th

View this program: with abstractssession overviewtalk overview

09:00-10:05 Session 21: Proofs - Part 1
09:00
Small Proofs from Congruence Closure (abstract)
09:25
Reconstructing Fine-Grained Proofs of Complex Rewrites Using a Domain-Specific Language (abstract)
09:50
TBUDDY: A Proof-Generating BDD Package (abstract)
10:30-11:00 Session 23: Proofs - Part 2
10:30
Stratified Certification for k-Induction (abstract)
10:45
Proof-Stitch: Proof Combination for Divide-and-Conquer SAT Solvers (abstract)
11:00-12:05 Session 24: SAT and SMT - Part 2
11:00
First-Order Subsumption via SAT Solving (abstract)
11:25
BaxMC: a CEGAR approach to MAX#SAT (abstract)
PRESENTER: Thomas Vigouroux
11:50
INC: A Scalable Incremental Weighted Sampler (abstract)
12:05-12:40 Session 25: Student forum talks - Part 2
GAMBIT: An Interactive Playground for Concurrent Programs Under Relaxed Memory Models (abstract)
Commutativity in Concurrent Program Verification (abstract)
SEAURCHIN: Bounded Model Checking for Rust (abstract)
Proof Production for Neural Network Verification (abstract)
Trading Accuracy For Smaller Cardinality Constraints (abstract)
Formal Approach to Identifying Genes and Microbes Significant to Inflammatory Bowel Disease  (abstract)
Understanding Trust Assumptions for Attestation in Confidential Computing (abstract)
On Optimizing Back-Substitution Methods for Neural Network Verification (abstract)
Incremental Weighted Sampling (abstract)
14:00-15:30 Session 27: Parameterized systems and quantified reasoning
14:00
Automatic Repair and Deadlock Detection for Parameterized Systems (abstract)
14:25
Synthesizing Locally Symmetric Parameterized Protocols from Temporal Specifications (abstract)
14:50
Synthesizing Self-Stabilizing Parameterized Protocols with Unbounded Variables (abstract)
15:15
The Rapid Software Verification Framework (abstract)
16:00-17:15 Session 29: Hardware and RTL - Part 2
16:00
Reconciling Verified-Circuit Development and Verilog Development (abstract)
16:25
Timed Causal Fanin Analysis for Symbolic Circuit Simulation (abstract)
16:50
Divider Verification Using Symbolic Computer Algebra and Delayed Don’t Care Optimization (abstract)
18:30-22:30 Banquet at Cantina Martinelli

Social dinner in a beautiful historical winery of Trentino.

https://www.cantinamartinelli.com/?lang=en

Friday, October 21st

View this program: with abstractssession overviewtalk overview

09:00-10:00 Session 31: Invited Talk 2

Hana Chockler. Why do things go wrong (or right)? Applications of causal reasoning to verification

Abstract. In this talk I will look at the connections between causality and learning from one side, and verification and synthesis from the other side. I will introduce the relevant concepts and discuss how causality and learning can help to improve the quality of systems and reduce the amount of human effort in designing and verifying systems. I will (briefly) introduce the theory of actual causality as defined by Halpern and Pearl. This theory turns out to be extremely useful in various areas of computer science due to a good match between the results it produces and our intuition. I will illustrate the definitions by examples from formal verification. I will also argue that active learning can be viewed as a type of causal discovery. Tackling the problem of reducing the human effort from the other direction, I will discuss ways to improve the quality of specifications and will focus in particular on synthesis.

10:30-12:10 Session 33: Reachability and safety verification
10:30
Automating Geometric Proofs of Collision Avoidance with Active Corners (abstract)
10:55
Differential Testing of Pushdown Reachability with a Formally Verified Oracle (abstract)
11:20
Automated Conversion of Axiomatic to Operational Models: Theoretical and Practical Results (abstract)
11:45
Split Transition Power Abstraction for Unbounded Safety (abstract)
12:10
TriCera: Verifying C Programs Using the Theory of Heaps (abstract)
12:25
Formally Verified Quite OK Image Format (abstract)
14:00-15:30 Session 35: Synthesis
14:00
Synthesizing Transducers from Complex Specifications (abstract)
14:25
Synthesis of Semantic Actions in Attribute Grammars (abstract)
14:50
Reactive Synthesis Modulo Theories using Abstraction Refinement (abstract)
15:15
Learning Deterministic Finite Automata Decompositions from Examples and Demonstrations (abstract)
16:00-17:15 Session 37: Distributed systems
16:00
ACORN: Network Control Plane Abstraction using Route Nondeterminism (abstract)
16:25
Plain and Simple Inductive Invariant Inference for Distributed Protocols in TLA+ (abstract)
16:50
Awaiting for Godot: Stateless Model Checking that Avoids Executions where Nothing Happens (abstract)