Keynote Talks

• Sanjit A. Seshia (University of California, Berkeley, USA)

  • Runtime Assurance for Verified AI-Based Autonomy
  • Abstract: Verified artificial intelligence (AI) is the goal of designing AI-based systems that have
    strong, verified assurances of correctness with respect to mathematically-specified
    requirements. This goal is particularly important for autonomous and semi-autonomous
    systems. In this talk, I will review the progress towards Verified AI from the perspective
    of formal methods with a special focus on autonomy. The talk will focus mainly on the use
    of formal methods for run-time assurance, which is especially important as many AI-based
    autonomous systems are designed to operate in unknown and uncertain environments.
    The presented research 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.
    For a brief Bio: please see here: https://people.eecs.berkeley.edu/~sseshia/bio.html

• Xinyu Feng (Nanjing University, China)

  • Compositional Reasoning about Concurrent Randomized Programs
  • Abstract: Behaviors of concurrent randomized programs may vary with different scheduling policy. In the oblivious adversary model, the scheduling of a concurrent randomized program needs to be fixed before the program execution, and cannot rely on the program states and the results of probabilistic choices. Algorithms have been proposed to take advantage of this scheduling policy for better performance, but are extremely difficult for modular verification because the interaction between threads is very sensitive to the program structure and the execution steps. We propose a new program logic for thread-local verification of concurrent randomized programs in the oblivious adversary model. With a novel “split” mechanism, one can split the state distribution into smaller partitions, and the reasoning can be done based on each partition independently, which allows us to avoid considering different execution paths of if-statements and while-loops simultaneously. The logic rules are compositional and are natural extensions of their classical (non-probabilistic) counterparts. Using our program logic, we can verify typical algorithms in the oblivious adversary model.

• Shaz Qadeer (Meta, USA)

  • The Civl verifier
  • Abstract: The Civl verifier introduces layered refinement, a new approach to the construction of verified concurrent programs and their proofs. This approach simplifies and scales (human and automated) reasoning by enabling a concurrent program to be represented and manipulated at multiple layers of abstraction. These abstraction layers are chained together via simple program transformations; each transformation is justified by a collection of automatically-checked verification conditions. Civl proofs are maintainable and reusable, specifically eliminating the need to write complex invariants on the low-level encoding of the concurrent program as a flat transition system. Civl has been used to construct verified low-level implementations of complex systems such as a concurrent garbage collector, a consensus protocol, and shared-memory data structures.
    Civl is jointly developed with Bernhard Kragl and publicly available.

• Jean-François Raskin (Université Libre de Bruxelles, Belgium)

  • Subgame Perfect Equilibrium with an Algorithmic Perspective
  • Abstract: In this invited talk, we will recall the notion of subgame perfect equilibrium (SPE) for games of infinite duration played on graph. We will introduce new algorithmic ideas in this context. In particular, we will provide an effective characterization of all the SPEs in infinite duration games played on finite graphs for the case of parity objectives and for the case of mean-payoff objectives. To this end, we will introduce the notion of requirement and the notion of negotiation function. We will establish that the set of plays that are supported by SPEs are exactly those that are consistent with the least fixed point of the negotiation function. By studying the properties of the least fixed point of the negotiation function, we will provide provably optimal algorithms to solve relevant decision problems related to SPEs.

• Mohamed Faouzi Atig (Uppsala University, Sweden)

  • Flattening String Constraints
  • Abstract: String data type is present in all modern programming and is a part of the core semantics of programming languages such as JavaScript and Python. The testing and verification of such programs require a decision procedure for string constraints. The types of constraints include: (1) equality constraints of the form t1 = t2 where t1 and t2 consist of a sequence of string variables and constants, (2) regular constraints of the form x 2 R where x is a string variable and R is a regular language, and (3) integer constraints which are linear arithmetic formulas over the length of the string variables. In this keynote talk, we will present our recent decision procedure for string constraints. We will focus on the decision procedure that uses the Counter-Example Guided Abstraction Re nement (CEGAR) framework which contains both an under- and an over-approximation module running in an alternating manner. The flow of information between these modules is used to increase their precision in an automatic manner.
    This talk will be based on join work with Parosh Aziz Abdulla, Yu-Fang Chen, Bui Phi Diep, Julian Dolby, Lukas Holik, Denghang Hu, Petr Janku, Hsin-Hung Lin, Ahmed Rezine, Philipp Rummer, Wei-Lun
    Tsai, Wei-Cheng Wu, Zhillin Wu and Di-De Yen.

Tutorials

• Constantin Enea (LIX, Ecole Polytechnique, France)

  • Verifying Consistency of Large-Scale Storage Systems and Applications
  • Abstract: Modern applications, such as social networking systems and e-commerce platforms are centered around using large-scale storage systems for storing and retrieving data. In the presence of concurrent accesses, these storage systems trade off consistency for performance. The weaker the consistency level, the more behaviors a storage system is allowed to exhibit and it is up to the developer to ensure that their application can tolerate those behaviors. However, these weak behaviors only occur rarely in practice and outside the control of the application, making it difficult for developers to check the robustness of their code against weak consistency levels. In this tutorial I will present a framework for formalizing consistency levels and algorithmic methods for checking whether a storage system conforms to a certain consistency level or that an application satisfies its intended specification when run under a given consistency level.

• Mahesh Viswanathan (University of Illinois at Urbana-Champaign, USA)

  • Verifying the Privacy and Accuracy of Algorithms for Differential Privacy
  • Abstract: Differential privacy is a mathematical framework for performing privacy-preserving computations over sensitive data. One important feature of differential privacy algorithms is their ability to achieve provable individual privacy guarantees and at the same time ensure that the outputs are reasonably accurate. Such algorithms compute noisy versions of the right answers to aggregate queries on sensitive data to ensure privacy. Privacy guarantees demand that the algorithm running on “similar” data sets produce responses that are statistically similar; this provides a very strong form of individual privacy. Accuracy, on the other hand, demands that the algorithms output, though noised, be sufficient close to the correct answer for a query. In this tutorial we will present approaches to checking the privacy and accuracy requirements for a given algorithm.