Techniques based on formal logic, such as model checking, satisfiability, static analysis, and automated theorem proving, are finding a broad range of applications in modeling, analysis, verification, and synthesis. This school, the eighth in the series, will focus on the principles and practice of formal techniques, with a strong emphasis on the hands-on use and development of this technology. It primarily targets graduate students and young researchers who are interested in developing and using formal techniques in their research. A prior background in formal methods is helpful but not required. Participants at the school will have a seriously fun time experimenting with the tools and techniques presented in the lectures during laboratory sessions. The main lectures in the school which take place during May 21-25, 2018, are preceded by a background course on logic during May 19-20, 2018.
This is a joint work with Marcelo Taube (TAU), Giuliano Losa(UCLA), Ken McMillan(Microsoft Research), Oded Padon and Sharon Shoham(TAU). The techniques have been implemented in IVY https://www.microsoft.com/en-us/research/project/ivy/
Bio: Professor Mooly Sagiv works at the School of Computer Science, Tel Aviv University, where his research focuses broadly on easing the task of developing reliable and efficient programs via program analysis.This tutorial provides a general introduction to F* followed by a focus on Low*, a subset of F* that extracts to C code for efficient, low-level programming. The examples we present are drawn from Project Everest, an ongoing effort using F* and Low* to verify and deploy secure components in the HTTPS ecosystem, including protocols such TLS and the cryptographic algorithms that underlie it.
Bio: Nikhil Swamy is a Senior Researcher in the RiSE group at MSR Redmond. My work covers various topics including type systems, program logics, functional programming, program verification and interactive theorem proving. I often think about how to use these techniques to build provably secure programs, including web applications, web browsers, crypto protocol implementations, and low-level systems code.In this tutorial, I will give a brief introduction to dependent types and the dependently-typed language Agda developed at Chalmers. We will understand the theoretical concepts as we walk through some representative use cases. In the first part, we will learn how to elegantly represent binary search trees and their ordering invariant in Agda. In the second part, we will look at examples from programming language, like representation of expressions, evaluation, and equational reasoning.
The tutorial is accompanied by Agda programming and reasoning exercises.
Bio: Dr. Andreas Abel has a Diploma, PhD, and Habilitation from Ludwig-Maximilians-University (LMU), Munich, Germany. He is a Senior lecturer at Chalmers / Gothenburg University where he has been since 2013. He has been active in the development of Agda since 2004. He has over 70 publications on types, programming languages, semantics, and verification.Abstract: The goal of this lecture is to bridge the gap between verification research and software engineering. Consequently, the lecture starts with theory and concepts, continues with a unifying view on several different verification algorithms, and finally addresses some practical problems that occur in software verification. The first part gives an introduction of the framework of configurable program analysis and shows how state-of-the-art concepts like cartesian and boolean abstraction, lazy abstraction, CEGAR, interpolation, and large-block encoding can be integrated in a configurable way. The second part consolidates knowledge and we show how to express the four different ``schools of thought'' of software verification in one unifying framework: bounded model checking, k-induction, predicate abstraction, and lazy abstraction with interpolants. We also shed light on practical aspects of software model checking and explain approaches like regression verification, witness-based result validation, conditional model checking, and reducer-based verification.
Bio: Dirk Beyer is Full Professor of Computer Science and has a Research Chair for Software and Computational Systems at LMU Munich, Germany (since 2016). Before, he was Full Professor of Computer Science at University of Passau, Germany (2009-2016). He was Assistant and Associate Professor at Simon Fraser University, B.C., Canada (2006-2009), and Postdoctoral Researcher at EPFL in Lausanne, Switzerland (2004-2006) and at the University of California, Berkeley, USA (2003-2004) in the group of Tom Henzinger. Dirk Beyer holds a Dipl.-Inf. degree (1998) and a Dr. rer. nat. degree (2002) in Computer Science from the Brandenburg University of Technology in Cottbus, Germany. In 1998 he was Software Engineer with Siemens AG, SBS Dept. Major Projects in Dresden, Germany. His research focuses on models, algorithms, and tools for the construction and analysis of reliable software systems. He is the architect, designer, and implementor of several successful tools. For example, CrocoPat is the first efficient interpreter for relational programming, CCVisu is a successful tool for visual clustering, and CPAchecker and BLAST are two well-known and successful software model checkers.Abstract: Understanding properties of deep neural networks is an important challenge in deep learning. In this paper, we take a step in this direction by proposing a rigorous way of verifying properties of a popular class of neural networks, Binarized Neural Networks, using the well-developed means of Boolean satisfiability. Our main contribution is a construction that creates a representation of a binarized neural network as a Boolean formula. Our encoding is the first exact Boolean representation of a deep neural network. Using this encoding, we leverage the power of modern SAT solvers along with a proposed counterexample-guided search procedure to verify various properties of these networks. A particular focus will be on the critical property of robustness to adversarial perturbations. For this property, our experimental results demonstrate that our approach scales to medium-size deep neural networks used in image classification tasks. To the best of our knowledge, this is the first work on verifying properties of deep neural networks using an exact Boolean encoding of the network.
Bio: Nina Narodytska is a researcher at VMware Research. Prior to VMWare Research, she was a researcher at Samsung Research America, a postdoctoral researcher in the Carnegie Mellon University School of Computer Science and the University of Toronto. She received her PhD from the University of New South Wales in 2011 and she was a member of the NICTA Optimisation group. Nina works on developing efficient search algorithms for decision and optimization problems. She was named one of “AI’s 10 to Watch” young researchers in the field of AI.We investigate the semantics of a simple first-order functional programming language with reals, product types, and a first-class reverse-mode differentiation operator (reverse-mode differentiation generalises gradients). The semantics employs a standard concept of real analysis: smooth multivariate functions with open domain. It turns out that such partial functions fit well with programming constructs such as conditionals and recursion; indeed they form a complete partial order, and so standard fixed-point methods can be applied. From a programming language point of view, however, many types are lacking, particularly sum types and recursive types, such as list types. We conclude with a brief presentation of notions of shapely datatypes and smooth functions. These can be used to give the semantics of such types and the usual functions between them while retaining first-class differentiation.
Bio: Gordon David Plotkin, FRS, FRSE is a theoretical computer scientist in the School of Informatics at the University of Edinburgh. Plotkin is probably best known for his introduction of structural operational semantics (SOS) and his work on denotational semantics. In particular, his notes on A Structural Approach to Operational Semantics were very influential.Plotkin was elected a Fellow of the Royal Society in 1992, is a Fellow of the Royal Society of Edinburgh and a Member of the Academia Europæa. He received the 2012 Royal Society Milner Award for “his fundamental research into programming semantics with lasting impact on both the principles and design of programming languages.” and the 2010, ACM SIGPLAN Programming Languages Achievement Award.
3.5GB ova file for VirtualBox, sha1 hash d843805da3406dfc38d8906f8b783b540796726e
Information about previous Summer Schools on Formal Techniques can
be found at
We expect to provide support for the travel and accommodation for (a
limited number of students) registered at US universities. We also welcome
applications from non-US students as well as non-students (if space
permits). Non-US students will have to cover their own travel and
will be charged around US$800 for meals and lodging. Applications
should be submitted together with names of two references (preferably
advisors, professors, or senior colleagues) using the form below.
Questions on any aspect of the school can be posted
here.
Schedule
SSFT18 VM
†NOTE: Underrepresented minority refers to African Americans, Mexican-Americans, Native Americans (American Indians, Alaska Natives, and Native Hawaiians), Pacific Islanders, and mainland Puerto Ricans.