Days: Tuesday, October 30th Wednesday, October 31st Thursday, November 1st Friday, November 2nd

Tuesday, October 30th

View this program: with abstractssession overviewtalk overview

10:00-12:00 Session 2: Formal Verification of Deep Neural Networks

Deep neural networks are among the most successful artificial intelligence technologies making impact in a variety of practical applications. However, many concerns were raised about the `magical’ power of these networks. It is disturbing that we are really lacking of understanding of the decision making process behind this technology. Therefore, a natural question is whether we can trust decisions that neural networks make. One way to address this issue is to define properties that we want a neural network to satisfy. Verifying whether a neural network fulfills these properties sheds light on the properties of the function that it represents. In this tutorial, we overview several approaches to verifying neural networks properties. The first set of methods encode neural networks into Integer Linear Programs or Satisfiability Modulo Theory formulas. They come up with domain-specific algorithms to solve verification problems. The second approach is to treat the neural network as a non-linear function and to use global optimization techniques for verification. The third line of work uses abstract interpretation to certify neural networks. Finally, we consider a special class of neural networks – Binarized Neural Networks – that can be represented and analyzed using Boolean Satisfiability. We discuss how we can take advantage of the structure of neural networks in the search procedure.

Formal Verification of Deep Neural Networks (abstract)
12:00-13:30Lunch Break

Tejas Conference Dining Room

13:30-15:30 Session 3: Formal Verification of Unsatisfiability Results

Satisfiability (SAT) solvers are used for determining the correctness of hardware and software systems. It is therefore crucial that these solvers justify their claims by providing proofs that can be independently verified. This holds also for various other applications that use SAT solvers. Just recently, long-standing mathematical problems were solved using SAT, including the Erdos Discrepancy Problem, the Pythagorean Triples Problem, and Schur Number Five. Especially in such cases, proofs are at the center of attention, and without them, the result of a solver is almost worthless.

What the mathematical problems and the industrial applications have in common, is that proofs are often of considerable size – in the case of the Schur Number Five about 2 petabytes in a highly compressed format. To demonstrate how to increase trust in the correctness of multi-CPU-year computations, we validated the poof of the Schur number five problem. We certified the proof using the ACL2 theorem proving system. Given the enormous size of the proof, we argue that any result produced by SAT solvers can now be validated using highly trustworthy systems with reasonable overhead.

The tutorial also covers how to use tools that validate proofs of unsatisfiability. Apart from verifying SAT-solving results, these tools support producing unsatisfiable cores and optimized proofs. Unsatisfiable cores can be useful in various debugging settings, while optimized proofs allow for fast validation by a formally-verified tool and an independent party

Formal Verification of Unsatisfiability Results (abstract)
15:30-16:00Coffee Break
16:00-18:00 Session 4: Deductive Verification of Distributed Protocols in First-Order Logic

Formal verification of infinite-state systems, and distributed systems in particular, is a long standing research goal. In the deductive verification approach, the programmer provides inductive invariants and pre/post specifications of procedures, reducing the verification problem to checking validity of logical verification conditions. This check is often performed by automated theorem provers and SMT solvers, substantially increasing productivity in the verification of complex systems. However, the unpredictability of automated provers presents a major hurdle to usability of these tools. This problem is particularly acute in case of provers that handle undecidable logics, for example, first-order logic with quantifiers and theories such as arithmetic. The resulting extreme sensitivity to minor changes has a strong negative impact on the convergence of the overall proof effort.

On the other hand, there is a long history of work on decidable logics or fragments of logics. Generally speaking, decision procedures for these logics perform more predictably and fail more transparently than provers for undecidable logics. In particular, in the case of a false proof goal, they usually can provide a concrete counter-model to help diagnose the problem. However, decidable logics pose severe limitations on expressiveness, and it is not immediately clear that such logics can be applied to proving complex protocols or systems.

In this tutorial, we will explore a practical approach to using first order-logic, and a decidable fragment thereof, to prove complex distributed protocols and systems. The approach, implemented in the Ivy verification tool, applies abstraction and modular reasoning techniques to mitigate the expressiveness limitations of decidable fragments. The high-level strategy involves the following ideas:

  • Abstracting infinite-state systems using first-order logic.
  • Carefully controlling quantifier-alternations to ensure decidability.
  • Using modular reasoning principles to decompose a proof into decidable lemmas.

Experience to date indicates that the approach, based on first-order logic, is surprisingly powerful, and it is possible to prove safety and liveness properties of complex protocols (e.g., Paxos variants), and also to produce verified low-level implementations, using decidable logics. Moreover, the effort required to structure the proof in this way is more than repaid by greater reliability of proof automation, which significantly reduces the overall verification effort. Better matching human reasoning capabilities to the capabilities of automated provers results in a more stable and predictable formal development process.

This tutorial is based on joint works with Jochen Hoenicke, Neil Immerman, Aleksandr Karbyshev, Giuliano Losa, Kenneth L. McMillan, Aurojit Panda, Andreas Podelski, Mooly Sagiv, Sharon Shoham, Marcelo Taube, James R. Wilcox, and Doug Woos

Deductive Verification of Distributed Protocols in First-Order Logic (abstract)
Wednesday, October 31st

View this program: with abstractssession overviewtalk overview

10:00-10:15Coffee Break
10:45-12:05 Session 9: Hardware
CoSA: Integrated Verification for Agile Hardware Design (abstract)
Integrating Memory Consistency Models with Instruction-Level Abstraction for Heterogeneous System-on-Chip Verification (abstract)
BMC with Memory Models as Modules (abstract)
12:05-13:30Lunch Break

Tejas Conference Dining Room

13:30-15:00 Session 10: Quantifiers and SAT
Complete Test Sets And Their Approximations (abstract)
Expansion-Based QBF Solving Without Recursion (abstract)
Bit-Vector Interpolation and Quantifier Elimination by Lazy Reduction (abstract)
15:00-15:30Coffee Break
15:40-17:00 Session 11: Liveness
Analyzing the Fundamental Liveness Property of the Chord Protocol (abstract)
k-FAIR = k-LIVENESS + FAIR: Revisiting SAT-based Liveness Algorithms (abstract)
Temporal Prophecy for Proving Temporal Properties of Infinite-State Systems (abstract)
17:45-19:00 reception

Reception, haloween

Thursday, November 1st

View this program: with abstractssession overviewtalk overview

09:00-10:00 Session 13: Concurrency
Automatic Synchronization for GPU Kernels (abstract)
Rely-Guarantee Reasoning for Automated Bound Analysis of Lock-Free Algorithms (abstract)
10:30-12:00 Session 14: Verification
Template-Based Verification of Heap-Manipulating Programs (abstract)
Using Loop Bound Analysis For Invariant Generation (abstract)
Post-Verification Debugging and Rectification of Finite Field Arithmetic Circuits using Computer Algebra Techniques (abstract)
12:00-13:30Lunch Break

Tejas Conference Dining Room

13:30-15:00 Session 15: Learning and Synthesis
Automata Learning for Symbolic Execution (abstract)
Functional Synthesis via Input-Output Separation (abstract)
Learning Linear Temporal Properties (abstract)
15:00-15:30Coffee Break
15:30-16:40 Session 17: SMT and CHC
The Eldarica Horn Solver (abstract)
Trau: SMT solver for string constraints (abstract)
Solving Constrained Horn Clauses Using Syntax and Data (abstract)
16:40-17:00Coffee Break
17:00-18:00 Session 18: Rails
Analysis of Relay Interlocking Systems via SMT-based Model Checking of Switched Multi-Domain Kirchhoff Networks (abstract)
Design-Time Railway Capacity Verification using SAT modulo Discrete Event Simulation (abstract)
19:00-21:00 banquet


Location: Clay Pit
Friday, November 2nd

View this program: with abstractssession overviewtalk overview

10:00-10:30Coffee Break
10:30-12:30 Session 20: Certificates
Complete and Efficient DRAT Proof Checking (abstract)
Semantic-based Automated Reasoning for AWS Access Policies using SMT (abstract)
A Verified Certificate Checker for Finite-Precision Error Bounds in Coq and HOL4 (abstract)
Certifying Proofs for LTL Model Checking (abstract)
12:30-14:00Lunch Break

Tejas Conference Dining Room