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.
Research Paper Committee
Artifact Evaluation Committee
Certified Programs and Proofs (CPP)
Principles of Secure Compilation(PriSC)
VMCAI 2019, co-located
Tuesday, January 15, 2019 | 9:00 AM–10:30 AM
Semantics for Compiler IRs: Undefined Behavior is not Evil!
Wednesday, January 16, 2019 | 1:45 PM–2:07 PM | Probabilistic Programming and Semantics
Probabilistic Programming with Densities in SlicStan: Efficient, Flexible and Deterministic
Friday, January 18, 2019 | 5:21 PM–5:43 PM | Verified Compilation and Concurrency
A Verified, Efficient Embedding of a Verifiable Assembly Language
Tuesday, January 15, 2019 | 4:30 PM–5:00 PM | Networks and Concurrency at VMCAI
Fast BGP Simulation of Large Datacenters
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.