 |
POPL 2015: 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming LanguagesTata Institute of Fundamental Research, Mumbai, India
|
POPL 2015 Tutorials
On Tuesday, 13 January 2015, POPL will host a number of tutorials. These are 90 min talks oriented towards students in particular and other POPL attendees in general.
- T1: Programming using Automata and Transducers
- T2: A Tutorial on Verifying Higher-Order, Effectful Programs Using F*
- T3: Probabilistic model checking
- T4: Reachability Modulo Theories: Algorithms and Applications
- T5: Probabilistic Programming Languages and Semantics
- T6: From Linear Logic to Session-Typed Concurrent Programming
To avoid conflicts, each tutorial will be given twice according to the following schedule:
| Time | Room HBA | Room AG69 | Room B333 |
|---|---|---|---|
| 09:00-10:30 | 5. Probab. PL | 1. Automata | 4. Reachability |
| 11:00-12:30 | 5. Probab. PL | 6. Session types | 3. Pr. model checking |
| 14:00-15:30 | 2. F* | 6. Session types | 4. Reachability |
| 16:00-17:30 | 2. F* | 1. Automata | 3. Pr. model checking |
T1: Programming using Automata and Transducers
Presenters: Loris D'Antoni and Margus Veanes
Abstract: Finite automata have proven to be an effective tool to reason about programs operating over strings, such as routing filters. Finite state transducers extend finite automata with outputs and can model functions from strings to strings such as natural language transformations and string sanitizers. Due to their closure and decidability properties, these models are widely used in practice, and many extensions/improvements have been proposed. In this tutorial we focus on language based approaches that aim at applying the properties of automata and transducers to practical applications. We first introduce the basics of automata and transducers over finite and infinite alphabets and their decidable properties, and then present some of the mechanisms for building programs based on these models. We present three different languages and show how they can be used to optimize and verify real programs with the aid of automata-based techniques. The first language, Bek, is used to verify string sanitizers for security to avoid cross-site scripting attacks; the second one, Bex, is used to verify the correctness of string encoders and decoders; and the third one, Fast, is used to optimize and verify functional programs over trees. Finally, we will discuss the limitations of these approaches and potential way to address such limitations.
Bio: Loris D'Antoni is a fifth year Ph.D. student in Computer Science at the Univer- sity of Pennsylvania advised by Rajeev Alur. Loris's research centers on the use of formal methods, in particular transducers, to reason about programs. Typical applications are security, program verification, and program optimization.
Margus Veanes is a senior researcher at Microsoft. Margus received his Ph.D. in Computer Science from the University of Uppsala. Before joining Microsoft he worked as a postdoc in the Programming Logic group at Max Planck Institute for Computer Science in Saarbruecken. Margus's research interests are in program analysis with a focus on the use of symbolic automata theory in combination with state-of-the-art satisfiability modulo theories techniques, and model based testing.
T2: A Tutorial on Verifying Higher-Order, Effectful Programs Using F*
Presenters: F* Team
Abstract: F* is a new ML-like programming language designed for program verification. Specifications are expressed using refinement types, and pre- and post-conditions in the style of the Dijkstra monad---together, they enable describing precise properties of higher-order, effectful programs, up to functional correctness. Given a program and a claimed specification for it, F* produces verification conditions and discharges them using an SMT solver.
F* has been successfully used to verify a variety of programs, including the security of cryptographic protocol implementations; authorization properties of web browser extensions and cloud-hosted web applications; memory invariants of a model of the JavaScript runtime; and even the soundness of (a previous version of) the F* type-checker itself. The newest version of F* is open source, and compiles to F# and Ocaml; a JavaScript backend is also in the works.
This tutorial will be presented in two 90-minute sessions. Each session will begin with the same 30-minute introductory lecture on F*. We will spend the remainder of each session working in smaller groups in interactive mode, using the F* tool to program and verify the correctness of a number of small programs, including classic functional programs, programs that use state and other effects, and some small security-oriented examples. Depending on interest, we will also cover the use of F* as a proof assistant, showing how it can be used to mechanize the metatheory of small programming languages.
For the interactive part of the tutorial, it may be useful to have F* installed on your machine. You can obtain binaries for a variety of platforms from https://github.com/FStarLang/FStar. Depending on connectivity, we will also have a web interface to F* available for participants.
Bio: F* is a collaborative effort between Microsoft Research, INRIA, and IMDEA Software Institute. This tutorial will be delivered by Karthikeyan Bhargavan, Cédric Fournet, Catalin Hritcu, Aseem Rastogi and Nikhil Swam.y
T3: Probabilistic model checking
Presenter: Marta Kwiatkowska
Abstract: Probabilistic model checking is a formal verification technique for the automated analysis of systems that exhibit stochastic behaviour. Such behaviour may be due to, for example, component failure, randomisation, or uncertainty on the frequency of event occurrences. Similarly to probabilistic programming, stochasticity is represented by a random choice made according to a probability distribution, but nondeterministic choice is often featured, for example to model input nondeterminism or environment's decisions. The techniques focus on system dynamics rather than data, and thus concern models of systems and whether they meet given temporal logic properties. The models are probabilistic extensions of transition systems which can be obtained from a variety of modelling notations, including imperative programs with random assignment. Properties are specified in probabilistic extensions of temporal logic, and verification reduces to the computation of the probability or expectation of the probability being satisfied. For systems with nondeterministic choice, one can also construct optimal controllers that ensure the satisfaction of an objective specified by multiple properties. The techniques have been implemented in PRISM (www.prismmodelchecker.org) and enable a range of quantitative analyses of probabilistic models against specifications such as the worst-case probability of failure within 10 seconds or the minimum expected power consumption over all possible schedulings, as well as synthesis of strategies that simultaneously minimise energy consumption and maximise the probability of termination.
This tutorial will give an introduction to probabilistic model checking, explaining the underlying theory and algorithms for model checking and strategy synthesis. The material will be illustrated with several case studies that have been modelled and analysed in PRISM.
Bio: Marta Kwiatkowska is Professor at the University of Oxford. Her research is concerned with quantitative/probabilistic verification, which has been applied to a range of systems, from communication and security protocols to DNA computing, with genuine flaws found and corrected. She is known for leading the development of the probabilistic model checker PRISM (www.prismmodelchecker.org). Kwiatkowska gave the Milner Lecture in 2012 in recognition of "excellent and original theoretical work which has a perceived significance for practical computing", delivered keynotes at the ESEC/FSE 2007, ETAPS/FASE 2011 and ATVA 2013 conferences, and has given numerous tutorials. She is a member of Academia Europea, and will shortly receive an honorary doctorate from KTH. Kwiatkowska serves on editorial boards of several journals, including IEEE Transactions on Software Engineering, Formal Methods in System Design, and Information and Computation. Her research has been supported by grant funding from EPSRC, ERC, EU, DARPA and Microsoft Research Cambridge, including the prestigious ERC Advanced Grant VERIWARE "From software verification to everyware verification".
T4: Reachability Modulo Theories: Algorithms and Applications
Presenter: Akash Lal
Abstract: Program verifiers that attempt to automatically verify programs pose the verification problem as the decision problem: ìDoes there exist a proof that establishes the absence of errors? We instead pose program verification as: Does there exist an execution that establishes the presence of an error? to most directly match the most important and common use of automated program verification---bug-finding and debugging. We formalize the search for bugs as Reachability Modulo Theories (RMT). This tutorial will present basic complexity results on RMT and discuss Corral, an efficient verifier for RMT.
Our line of work on RMT offers a unique perspective on building practical verification tools. Traditional verifiers rely on proof-generation techniques such as predicate abstraction or interpolation. We instead rely on efficient search techniques powered by SMT solvers. Corral does almost all semantic reasoning and path exploration using SMT solvers, while encoding domain-specific knowledge via simple program transformations. For instance, Corral uses a program transformation (now commonly labeled as sequentializations) to compile away concurrency and reduce to the simpler setting of a sequential program. Corral uses other transformations to efficiently compile away assertions. Even abstraction is done using a program transformation. Invariant generation techniques are used in a plug-and-play manner to increase the efficiency of the search. The tutorial will do a deep-dive into the design of Corral.
The tutorial will also cover the use of Corral in a production environment to power the Static Driver Verifier (SDV). Corral now ships with SDV in every new version of the Windows operating system and is used routinely by driver developers both inside and outside Microsoft. The tutorial will discuss the challenges and solutions involved in taking verification technology to a production level.
Bio: Akash Lal is a researcher at Microsoft Research, Bangalore. His interests are in the area of programming languages and program analysis, with a focus on building bug-finding tools for concurrent programs. He joined Microsoft in 2009 after completing his PhD from University of Wisconsin-Madison under the supervision of Prof. Thomas Reps. For his thesis, he received the Outstanding Graduate Researcher Award, given by the Computer Sciences Department of UW-Madison, and the ACM SIGPLAN Outstanding Doctoral Dissertation Award. He completed his Bachelor's degree from IIT-Delhi in 2003.
T5: Probabilistic Programming Languages and Semantics
Presenter: Prakash Panangaden
Abstract: Probabilistic reasoning has long been a part of computer science, however, probabilistic programming languages have recently emerged as a vital and growing area of interest to the POPL community. The 2014 POPL had a session on the topic. As far back as 1997 the probabilistic variant of concurrent constraint programming languages was proposed and in 1999 a POPL paper on the semantics of probabilistic ccp appeared. The recent reemergence of probabilistic ideas has been driven by an exciting new interaction between the machine learning community and the programming languages community.
Central to this interaction is the notion of conditional probability which is the analogue of implication, the fundamental logical counterpart to functional abstraction. Important topics that need to be understood are: (a) what are the probabilistic analogues of basic concepts like binary relations? (b) how does one describe behavioural similarity probabilistically? and (c) how does one capture probabilistic semantics?
Bio: Prakash has worked on probabilistic transition systems, bisimulation and probabilistic semantics for nearly 20 years. Along with Josee Desharnais and Abbas Edalat he proved a striking logical characterization theorem for bisimulation. He is the author of the book Labelled Markov Processes (Imperial College Press 2009) and several papers on probabilistic bisimulation, approxi- mation of Markov processes, metrics for Markov processes, probabilistic semantics and applications to machine learning.
T6: From Linear Logic to Session-Typed Concurrent Programming
Presenter: Frank Pfenning
In the realm of functional programming, the Curry-Howard isomorphism relates intuitionistic propositions to types, constructive proofs to programs, and proof reduction to computation. It has been an effective guide in designing programming abstractions because of the coherence between the logical and operational readings of programs. In this tutorial we apply this idea in the realm of message-passing concurrent computation. We interpret the propositions of linear logic as session types, its sequent proofs as process expressions, and cut reduction as communication. We then go a step further, adding recursive types, functional types, and recursively defined processes to arrive at a language with a rich combination of functional and concurrent programming constructs. We illustrate and explore programming in this language with a prototype implementation.
Bio Frank Pfenning is President's Professor and Head of the Computer Science Department at Carnegie Mellon University. He obtained his PhD in Mathematics at Carnegie Mellon University in 1987. He served as trustee and president of CADE, chaired several conferences and program committees including FoSSaCS 2013, LICS 2008, CADE 2007, and RTA 2006, and served on the editorial board of TCS, JAR, and JSC. His current research interests include expressive type systems for functional, concurrent, and logic programming languages, computer security, logical frameworks, and automated deduction.