Propositional satisfiability (SAT) is the cornerstone NP-Complete problem of determining whether there exists an interpretation that satisfies a Boolean formula. The time complexity of SAT is exponential unless P=NP. Yet modern SAT solvers are routinely used to solve a variety of real-world problems, often translated into huge SAT instances having millions of clauses and more. As Donald Knuth put it: ``SAT is evidently a killer app, because it is key to the solution of so many other problems.'' Our tutorial consists of three parts: (1) The internals of a SAT solver: the goal is to understand the fundamental principles, data structures and algorithms which make modern SAT solvers so efficient. (2) Beyond plain SAT: various extensions of SAT turned out to be essential over the years. We survey the extensions and have a deeper look at some of them, including incremental SAT solving, unsatisfiable core extraction and Boolean optimization (MaxSAT). (3) SAT Applications: we review applications of SAT and dive into several of them, including Bounded Model Checking (BMC) and placement in physical design.
Bio: Dr. Alexander Nadel is a research scientist and engineer. He is leading the development of SAT technology at Intel, including SAT, MaxSAT and SMT solvers and model checkers, deployed in Intel to automate various tasks in physical design, formal verification and other domains. He is the author/co-author of over 30 papers, including the best paper at FMCAD’10. He served on the program committee of over 25 conferences and workshops. Recently, Alexander co-chaired the SMT Workshop 2021 and served as the workshop chair at the SAT conference 2022. Open-source solvers, developed by Alexander, won several competitions, including a category at the SAT Competition 2004, the SAT Competition 2018 and several tracks at MaxSAT Evaluations 2019 and 2020.
Satisfiability Modulo Theories (SMT) extends Boolean SAT solving with support for reasoning in background logical theories. SMT solving has become a cornerstone of automated reasoning with many applications in model checking, software verification, analysis of security policies, among others. The tutorial is an introduction to the techniques and algorithms employed by SMT solvers. It will cover the common approach to SMT based on combining a SAT solver with specialized theory solvers. The tutorial will then present techniques for combining theory solvers and for handling quantifier reasoning. Example applications, open issues, and alternative techniques to SMT solving will be discussed.
Bio: Bruno Dutertre is a Senior Principal Applied Scientist at Amazon Web Services, where he works on development and applications of SMT solving. He has worked on automated reasoning and applications for more than 20 years. He is one of the main developers of the Yices SMT solver.
Neural networks have shown tremendous success in many domains. At the same time, recent years have shown the simplicity of fooling neural networks by adversarial example attacks. These attacks undermine the reliability of deep learning-based systems. In this lecture, we will learn about these attacks, the challenges in verifying the safety of neural networks, and a couple of techniques to prove safety. We will conclude with open problems.
Bio: Dana Drachsler Cohen is an assistant professor at the Faculty of Electrical and Computer Engineering, Technion. Her research focuses on bringing safety guarantees to deep learning models.
Talk cancelled [planned slides]
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 Keller's conjecture. 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 proofs using formally-verified checkers. Given the enormous size of the proofs, 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.
Bio: Marijn Heule is an Associate Professor at Carnegie Mellon University and received his PhD at Delft University of Technology, the Netherlands. His contributions to automated reasoning have enabled him and others to solve hard problems in formal verification and mathematics. His recent contributions to computer-aided mathematics include solving the Pythagorean Triples Problem, the fifth Schur number, and Keller's Conjecture. Heule has co-authored 8 award-winning papers and he has developed award-winning SAT solvers. His preprocessing and proof producing techniques are used in many state-of-the-art solvers. His work on proofs of unsatisfiability made proof validation mainstream in the SAT community, thereby boosting confidence that these tools produce correct results. Heule is also an editor of the Handbook of Satisfiability, which has become a standard for the SAT community and it is a tremendous resource for future scientists.
Deep neural networks have emerged as a widely used and effective means for tackling complex, real-world problems. However, a major obstacle in applying them to safety-critical systems is the great difficulty in providing formal guarantees about their behavior. In recent years, many approaches for formally verifying neural networks have been proposed, but scalability remains a significant challenge. We will discuss two techniques for improving the scalability of such verifiers: (1) an abstraction-based technique, which allows to reduce the size of the network being verified; and (2) an invariant-based approach, which can significantly simplify the problem of verifying recurrent neural networks.
Based on joint work with Yizhak Elboher, Justin Gottschlich, Elazar Cohen, Yuval Jacoby and Clark Barrett
Bio: Guy Katz is an assistant professor at the Hebrew University of Jerusalem, Israel. He received his Ph.D. at the Weizmann Institute of Science in 2015. His research interests lie at the intersection between Formal Methods and Software Engineering, and in particular in the application of formal methods to software systems with components generated via machine learning.
Syntax-Guided Synthesis has emerged as a practical solution to the computationally hard problem of program synthesis. Program synthesis asks the problem whether it is possible to derive an executable implementation from a specification of a system given as a logical formula. The exact complexity of the problem depends on the type of the logical formalism and the corresponding type of systems and is either undecidable or of very high computational complexity. To overcome the computational hardness a thread of research works in program synthesis and program optimization emerged, in which in addition to the logical formula describing the functionality of the desired implementation, some syntactic set of constraints is given in order to limit the search space of viable solutions. The commonalities of these works have been identified and unified into what is termed today Syntax-Guided Synthesis.
Syntax-Guided Synthesis (SyGuS) is the computational problem of finding an implementation f that meets both a semantic constraint given by a logical formula φ (in a background theory T), and a syntactic constraint given by a grammar G, which specifies the allowed set of candidate implementations. Such a synthesis problem can be formally defined in SyGuS-IF, a language that is built on top of SMT-LIB. In order to facilitate, bring together and accelerate research and development of efficient solvers for SyGuS the Syntax-Guided Synthesis Competition (SyGuS-Comp) was initiated. In this talk we will get acquainted with the problem of syntax-guided synthesis and several distinct approaches for solving it.
Bio: Dana Fisman is an Associate Professor at the Computer Science Department of Ben-Gurion University. Before joining BGU she was a research scientist at the University of Pennsylvania, the Associate Director of the NSF expedition ExCAPE about system synthesis, and a visiting fellow at Yale University. She did her PhD at the Weizmann Institute of Science, and worked many years in the industry in IBM Haifa Research Labs, and in Synopsys Inc. Dana’s research interests are in the area of formal methods in system design, automata and logic. She is mostly known for her works on automata learning, and on PSL, the IEEE standard for property specification language, on which she received numerous awards from IEEE, IBM and Synopsys.
Safety verification is reducible to finding a safe inductive invariant. Most SAT/SMT-based model checking algorithms synthesize a safe inductive invariant by proving no counterexample of a specific length exists and generalizing this proof (of unsatisfiability) into a candidate invariant. A well-known generalization technique is based on Craig’s Interpolation theorem. In this tutorial we will show how interpolants are computed from proofs of unsatisfiability generated by a SAT solver (resolution and DRUP) , discuss how they are used in safety verification and will cover challenges and future research directions. During the tutorial we will build a safety verification engine based on interpolation. If time permits, we will briefly discuss other usages for proofs of unsatisfiability in the context of safety verification.
Bio: Yakir Vizel is an Assistant Professor in the Computer Science Department at The Technion. Previously he was a Postdoctoral Research Associate at Princeton University in the Electrical Engineering Department. He has received a B.Sc. in Mathematics and CS from the Technion and a Ph.D. in CS from the Technion. He has worked on developing Formal Verification algorithms and tools for hardware and software verification at Intel, Jasper Design Automation, Cadence, Mellanox and NVIDIA.
I will introduce formal theorem proving and Isabelle/HOL. The topics will include formal specifications; structured proofs and proof scripts; higher-order logic: induction, recursive data structures and recursive functions; as well as automation.
Bio: Cezary Kaliszyk is an associate professor at the University of Innsbruck, Austria. His research focuses on automation for formal proofs. He received his PhD in 2009, from the Radboud University, Netherlands. After two postdocs, one at TU Munich working on Nominal/Isabelle and one at the University of Tsukuba, he joined the University of Innsbruck, Austria.
This tutorial is for those interested in verification using formal methods in semi-automatic proof environments. We will showcase and exercise proving functional correctness and termination of functional programs using well-founded induction — an extended form of induction that generalizes the regular, structural induction in Coq. We will also inspect reasoning about imperative programs using Hoare logic, and, depending on the audience, will also present (simple) reasoning about memory access using Separation Logic. There is going to be a lot of hands-on learning (a computer running Coq is required). While there will be some overlap between the material covered in this tutorial and some of the material from the Programming Language Foundations (PLF) volume of Software Foundations; but those familiar with the material will find further examples of programs to apply formal reasoning to.
Bio: the instructor is a faculty member at the CS faculty at Technion. Previously, he was a postdoctoral associate at MIT CSAIL working with Prof. Armando Solar-Lezama and even more previously a Ph.D student supervised by Prof. Mooly Sagiv at Tel Aviv University. His interests are everything related to automated reasoning, verification, and software synthesis. And, of course, lots of coding.
Craig interpolation is a method for computing separating formulas for unsatisfiable conjunctions (or equivalently valid implications) and has over the last years become a standard technique for constructing abstractions in model checking. This lecture will survey some of the recent work on Craig interpolation for the theories used in SMT, including theories of arithmetic, bit-vectors, and data-types. The lecture will then discuss how Craig interpolation can be used to compute solutions of Constrained Horn clauses, an intermediate language applied in software model checking.
Bio: Philipp Rümmer is Professor at the Department of Informatics and Data Science of the University of Regensburg, Germany. His research alternates between automated reasoning, SMT solving, formal methods, and various other topics.
Constraint programming is a powerful formalism for expressing combinatorial problems, either satisfaction or optimization. In this talk, we will see an overview of the basics of constraint programming, the high level languages that have been developed for writing constraint programs, and show the modeling power they enable.
In the second part, we will talk about how techniques from the SAT world and the CP world interact and influence each other. We will look at staples of SAT solving such as propagation, clause learning, restarting, preprocessing, but also touch on topics in optimization, explanation, quantification, counting, proof generation, and contrast how both fields have approached these different generalizations of the base problem.
We present a learning scheme for solvers of the Constraint Satisfaction Problem (CSP), which is based on learning (general) constraints. When a general constraint is too complicated to implement, we fall-back to signed-resolution over generalized no-goods or signed-clauses.This scheme is integrated in a conflict-analysis algorithm reminiscent of a modern systematic propositional satisfiability (SAT) solver: it traverses the conflict graph backwards and gradually builds an asserting conflict constraint. This construction is based on inference rules that are tailored for various pairs of constraints types, e.g., x ≤ y1 + k1 and x ≥ y2 + k2, or (x1 xor x2)=0 and (x2 xor x3)=0. The learned constraint is stronger than what can be learned via signed resolution. Our experiments show that our solver HCSP backtracks orders of magnitude less than classical CSP solvers.
Many hard combinatorial problems involve huge numbers of symmetries which derive from isomorphic representations of objects in the search space. Restricting search to avoid symmetries - aka "symmetry breaking" - makes a big difference when trying to solve such problems.
Symmetry breaking in constraint programming is often achieved by introducing symmetry breaking constraints which are satisfied by at least one member of each isomorphism class. Complete symmetry breaking constraints are satisfied by exactly one member from each class and other symmetry breaks are called partial.
In this tutorial I will focus mainly on breaking symmetries in graph search problems. The search for complete symmetry breaking constraints for graph search problems is itself a hard problem and it is unknown if there exists a complete symmetry breaking constraint that is polynomial in the size of the graph.
In computer science when the problem is hard - we typically follow one or more from three alternatives: (1) clever brute force computation, (2) approximation algorithms, or (3) identifying special cases where the problem is easier.
This tutorial will focus on how each of these three alternatives comes into play when solving hard graph search problems. I will also talk about breaking symmetries for other hard combinatorial problems.
Bio: Michael Codish is a Professor of Computer Science at Ben-Gurion University. He is known for his early work on Termination Analysis, and on the application of SAT solving in this context. In recent years he has performed studies on symmetry in constraint problems. Together with his research team, he has applied SAT solving techniques to solve two problems which had remained open since the 1960's: (1) The 25-comparator sorting network for 9 inputs, found by Floyd in 1964 is optimal. There is no smaller network to sort 9 inputs; and (2) Computing the value of the Ramsey Number R(4,3,3) which is 30.
EVM (Ethereum virtual machine) bytecode programs, known as *smart contracts*, are usually short and relatively simple. This makes them perfect candidates for formal verification. At Certora, we translate the combination of our own specification language with the bytecode of such smart contracts into SMT formulas and then use SMT-solvers to check for their satisfiability. Amazingly, this works, and we have real customers paying real money for formal verification.
However, the story does not end there, and as contracts grow in size and complexity, we quickly reach the solving power limits of state of the art SMT-solvers. A great deal of effort in Certora is in making the generated formulas easier for the solvers. In this talk I will briefly go over some of the challenges we face and the techniques we use, e.g., avoiding non-linearity by using a partial linear axiomatization, CEGAR, simplifying the highly non standard EVM storage model, partially modeling bitwise operations, trying to avoid bitwise operations, etc.
Bio: Dr. Yoav Rodeh is currently a senior researcher at Certora. He previously worked in IBM, Google and NDS, and taught in a number of colleges in Israel. His papers span Formal Verification, Probabilistic and Distributed search, and ant colonies.