Invited Speakers

Tobias Nipkow
Prof. Tobias Nipkow

Theorem Proving Group, Faculty of Computer Science,

Technical University of Munich, Germany

Verified Textbook Algorithms A Biased Survey

Abstract:

This article surveys the state of the art of verifying standard textbook algorithms. We focus largely on the classic text by Cormen et al. Both correctness and running time complexity are considered.

David Dill
Prof. David Dill

Computer Science, The School of Engineering, Emeritus

Stanford University

Formal verification of Move programs for the Libra blockchain

Abstract:

The Libra blockchain, which was initiated in 2018 by Facebook, includes a novel programming language called Move for implementing smart contracts. The correctness of Move programs is especially important because the blockchain will host large amounts of assets, those assets are managed by smart contracts, and because there is a history of large losses on other blockchains because of bugs in smart contracts. The Move language is designed to be as safe as we can make it, and it is accompanied by a formal specification and automatic verification tool, called the Move Prover. A project to specify and formally verify as many important properties of the Move standard library is now well underway.

This talk will be about the goals of the project and the most interesting insights we’ve had as of the time of the presentation. The entire blockchain implementation, including the Move language, virtual machine, the Move Prover, and near-final various Move modules are available on http://github.com/libra

Klaus Havelund
Dr. Klaus Havelund

Senior Research Scientist (SRS) at NASA’s Jet Propulsion Laboratory

California Institute of Technology (Caltech)

First-Order Timed Runtime Verification using BDDs*

Abstract:

Runtime Verification (RV) expedites the analyses of execution traces for detecting system errors and for statistical and quality analysis. Having started modestly, with checking temporal properties that are based on propositional (yes/no) values, the current practice of RV often involves properties that are parameterized by the data observed in the input trace. The specifications are based on various formalisms, such as automata, temporal logics, rule systems and stream processing. Checking execution traces that are data intensive against a specification that requires strong dependencies between the data poses a non-trivial challenge; in particular if runtime verification has to be performed online, where many events that carry data appear within small time proximities. Towards achieving this goal, we recently suggested to represent relations over the observed data values as BDDs, where data elements are enumerated and then converted into bit vectors. We extend here the capabilities of BDD-based RV with the ability to express timing constraints, where the monitored events include clock values. We show how to efficiently operate on BDDs that represent both relations on (enumerations of) values and time dependencies. We demonstrate our algorithm with an efficient implementation and provide experimental results.