Microsoft @ POPL 2019

Microsoft @ POPL 2019


Microsoft is excited to be a Platinum sponsor of the 46th ACM SIGPLAN Symposium on Principles of Programming Languages. Stop by our booth to learn about our latest research and find out about career opportunities with Microsoft.

Microsoft Attendees

Tom Ball
Antoine Delignat-Lavaud
Chris Hawblitzel
Nuno Lopes
Jonathan Protzenko
Tahina Ramananandro
Andrey Rybalchenko
Santiago Zanella-Beguelin
Andy Gordon
Nikhil Swamy

Research Paper Committee

Dimitrios Vytiniotis, Matthew Parkinson, Nikhil Swamy

Artifact Evaluation Committee

Jonathan Protzenko

Steering Committee

Andrew D. Gordon

Co-Located Conferences

Certified Programs and Proofs (CPP)

Chris Hawblitzel

Principles of Secure Compilation(PriSC)

Cédric Fournet

Invited Speakers

VMCAI 2019, co-located
Tuesday, January 15, 2019 | 9:00 AM–10:30 AM
Semantics for Compiler IRs: Undefined Behavior is not Evil!
Nuno Lopes

Accepted Papers

Wednesday, January 16, 2019 | 1:45 PM–2:07 PM | Probabilistic Programming and Semantics
Probabilistic Programming with Densities in SlicStan: Efficient, Flexible and Deterministic

Maria I. Gorinova, Andrew D. Gordon, Charles Sutton

Friday, January 18, 2019 | 5:21 PM–5:43 PM | Verified Compilation and Concurrency
A Verified, Efficient Embedding of a Verifiable Assembly Language

Aymeric Fromherz, Nick Giannarakis, Chris Hawblitzel, Bryan Parno, Aseem Rastogi, Nikhil Swamy

Co-Located Conferences

Tuesday, January 15, 2019 | 4:30 PM–5:00 PM | Networks and Concurrency at VMCAI
Fast BGP Simulation of Large Datacenters

Nuno Lopes, Andrey Rybalchenko

Open Source Tools

Open Source Tools for System Correctness

Automata: Automata is a .NET library that provides algorithms for composing and analyzing regular expressions, automata, and transducers. In addition to classical word automata, it also includes algorithms for analysis of tree automata and tree transducers. The library covers algorithms over finite alphabets as well as their symbolic counterparts. Predicates can be supported by an SMT solver as a plugin.

Corral Program Verifier: Corral is a whole-program analysis tool for Boogie programs. Corral uses goal-directed symbolic search techniques to find assertion violations. It leverages the automated theorem prover Z3. Corral, by default, does a bounded search up to a recursion depth and fixed number of context switches. Corral also supports the Duality extension for constructing inductive proofs of correctness of programs.

Ivy: IVy is a tool intended to allow interactive development of protocols and their proofs of correctness and to provide a platform for developing and experimenting with automated proof techniques. In particular, IVy provides interactive visualization of automated proofs, and supports a use model in which the human protocol designer and the automated tool interact to expose errors and prove correctness.

Lean Theorem Prover: Lean is an open source theorem prover and programming language. Lean aims to bridge the gap between interactive and automated theorem proving, by situating automated tools and methods in a framework that supports user interaction and the construction of fully specified axiomatic proofs.

P/P#: P/P# are languages for asynchronous event-driven programming that allow the programmer to specify the system as a collection of interacting state machines, which communicate with each other using events. P/P# unifies modeling and programming into one activity for the programmer. Not only can a P/P# program be compiled into executable code, but it can also be validated using systematic testing.

Project Everest: Everest is the combination of the following projects, that together are used to prove correct/secure and generate a C library that efficiently implements TLS 1.3

  • F*, a verification-oriented dialect of ML
  • HACL*, a verified library of cryptographic primitives written in F*
  • KreMLin, a compiler from a subset of F* to C
  • miTLS, an implementation of the TLS protocol, written in F*
  • Vale, a domain-specific language designed to implement verified cryptographic primitives in assembly

TLA+: TLA+ is based on the idea that the best way to describe things formally is with simple mathematics, and that a specification language should contain as little as possible beyond what is needed to write simple mathematics precisely. TLA+ is especially well suited for writing high-level specifications of concurrent and distributed systems.

Network Verification: Firewall Checker is a firewall analysis library using the Z3 SMT Solver from Microsoft Research. Includes console applications to check the equivalence of two firewalls, or analyze the action of a firewall on a single packet. It was developed for use inside Microsoft Azure to analyze changes to Windows Firewall generation logic. It is one part of much larger effort to verify aspects of data center configuration and behavior.

Verisol: VeriSol (Verifier for Solidity) is a prototype formal verification and analysis system for smart contracts developed in the popular Solidity programming language. It is based on translating programs in Solidity language to programs in Boogie intermediate verification language, and then leveraging the verification toolchain for Boogie programs.

Z3 Theorem Prover: Z3 is an automated theorem prover in the satisfiability-modulo-theories (SMT) family, under research/development for over a decade at Microsoft Research and widely deployed in the industry for a wide range of uses, from program verification to product configuration.

Microsoft Research blog