ABSTRACT. This tutorial provides an overview of SMT solving foundations and delves into recent advances in SMT taking as starting point methods developed in context of the Z3 SMT solver. Advances in SMT solving in the past decades have been based on the following interacting main themes: (1) Search technologies. An important discovery in the early 2000s was that modern SAT solving techniques, known as CDCL, could be used beyond propositional SAT. In a nutshell it applies a method of model extension and repair, which has inspired generalizations and search algorithms specific to theories. Recent advances beyond CDCL integrates cube&conquer methods to partition a search space. (2) Integrating Theory Solvers. The approach, based on the Nelson-Oppen combination, has been the backbone of mainstream SMT solvers. It works for signature disjoint theories. With recent trends in solvers for strings and sequences where theories share functions (such as string length) there is a recurrent interest in integration methods that go beyond Nelson-Oppen. (3) Theory Solvers. A significant set of SMT use cases require some reasoning about arithmetic. We summarize some highlights in their approaches to solving classes of arithmetical formulas, including linear real, integer, linear real with ReLu, polynomial real, and with recent advances in handling non-linear integer, polynomial GF, and transcendental functions.

ABSTRACT. This tutorial provides an overview of SMT solving foundations and delves into recent advances in SMT taking as starting point methods developed in context of the Z3 SMT solver. Advances in SMT solving in the past decades have been based on the following interacting main themes: (1) Search technologies. An important discovery in the early 2000s was that modern SAT solving techniques, known as CDCL, could be used beyond propositional SAT. In a nutshell it applies a method of model extension and repair, which has inspired generalizations and search algorithms specific to theories. Recent advances beyond CDCL integrates cube&conquer methods to partition a search space. (2) Integrating Theory Solvers. The approach, based on the Nelson-Oppen combination, has been the backbone of mainstream SMT solvers. It works for signature disjoint theories. With recent trends in solvers for strings and sequences where theories share functions (such as string length) there is a recurrent interest in integration methods that go beyond Nelson-Oppen. (3) Theory Solvers. A significant set of SMT use cases require some reasoning about arithmetic. We summarize some highlights in their approaches to solving classes of arithmetical formulas, including linear real, integer, linear real with ReLu, polynomial real, and with recent advances in handling non-linear integer, polynomial GF, and transcendental functions.

ABSTRACT. Symbolic execution is a systematic program analysis technique which explores multiple program behaviors all at once by collecting and solving symbolic path conditions over program paths. The technique has been recently extended with probabilistic reasoning. This approach computes the conditions to reach target program events of interest and uses model counting to quantify the fraction of the input domain satisfying these conditions thus computing the probability of event occurrence. This probabilistic information can be used for example to compute the reliability of an aircraft controller under different wind conditions (modeled probabilistically) or to quantify the leakage of sensitive data in a software system, using information theory metrics such as Shannon entropy. In this talk we review recent advances in symbolic execution and probabilistic reasoning and we discuss how they can be used to ensure the safety and security of software systems.

ABSTRACT. Symbolic execution is a systematic program analysis technique which explores multiple program behaviors all at once by collecting and solving symbolic path conditions over program paths. The technique has been recently extended with probabilistic reasoning. This approach computes the conditions to reach target program events of interest and uses model counting to quantify the fraction of the input domain satisfying these conditions thus computing the probability of event occurrence. This probabilistic information can be used for example to compute the reliability of an aircraft controller under different wind conditions (modeled probabilistically) or to quantify the leakage of sensitive data in a software system, using information theory metrics such as Shannon entropy. In this talk we review recent advances in symbolic execution and probabilistic reasoning and we discuss how they can be used to ensure the safety and security of software systems.

ABSTRACT. Cyber-physical systems (CPS) integrate computation with physical processes. In recent years, the fields of formal methods and machine learning have been coming together in intruiging ways, particularly in the design of CPS. On the one hand, learning-based methods have proven effective in certain tasks in formal methods, particularly in the synthesis of artifacts for formal verification and synthesis. On the other hand, formal methods is increasingly being applied to learning-based systems. In this tutorial, we will survey recent advances in formal specification, verification, and synthesis of CPS that build on this interplay between formal methods and machine learning. We will use three exemplar applications: (i) simulation-driven verification of temporal logic properties of industrial CPS; (ii) temporal logic motion planning of autonomous vehicles, and (iii) specification and verification of learning-based CPS, including those using deep neural networks.

ABSTRACT. Cyber-physical systems (CPS) integrate computation with physical processes. In recent years, the fields of formal methods and machine learning have been coming together in intruiging ways, particularly in the design of CPS. On the one hand, learning-based methods have proven effective in certain tasks in formal methods, particularly in the synthesis of artifacts for formal verification and synthesis. On the other hand, formal methods is increasingly being applied to learning-based systems. In this tutorial, we will survey recent advances in formal specification, verification, and synthesis of CPS that build on this interplay between formal methods and machine learning. We will use three exemplar applications: (i) simulation-driven verification of temporal logic properties of industrial CPS; (ii) temporal logic motion planning of autonomous vehicles, and (iii) specification and verification of learning-based CPS, including those using deep neural networks.