ATVA 2018: INTERNATIONAL SYMPOSIUM ON AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS
PROGRAM FOR SUNDAY, OCTOBER 7TH
Days:
next day
all days

View: session overviewtalk overview

09:00-10:00 Session 2: Tutorial 1-A ( Grace Ford Salvatori Hall, Room 207)
Chair:
09:00
Recent advances in SMT

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.

10:00-10:30Coffee Break
10:30-11:30 Session 3: Tutorial 1-B
Chair:
10:30
Recent advances in SMT (cont'd)

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.

11:30-12:30 Session 4: Tutorial 2-A
11:30
Symbolic Execution and Probabilistic Reasoning

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.

12:30-14:00Lunch Break
14:00-15:00 Session 5: Tutorial 2-B
14:00
Symbolic Execution and Probabilistic Reasoning (cont'd)

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.

15:00-16:00 Session 6: Tutorial 3-A
15:00
Formal Methods, Machine Learning, and Cyber-Physical 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.

16:00-16:30Coffee Break
16:30-17:30 Session 7: Tutorial 3-B
Chair:
16:30
Formal Methods, Machine Learning, and Cyber-Physical Systems (contd)

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.