Verified Systems with F* and Ivy (22^nd July, 7:00am – 8:00am PST )

• Kenneth McMillan (Microsoft Research), Nikhil Swamy (Microsoft Research), Aseem Rastogi (Microsoft Research)
• Meeting link: https://us02web.zoom.us/j/82864899279
• Abstract: We will give an overview of Ivy and F*, two verification tools developed at Microsoft Research. Ivy is an open-source, multi-modal verification tool for correct design and implementation of distributed algorithms, supporting modular specification, implementation and proof. Ivy’s goal is to maximize the automation in proofs while providing predictability, stability and transparency. F* is a dependently-typed programming language and a proof assistant with SMT-based proof automation. Several critical software components such as cryptographic libraries and parsers, have been verified in F* and deployed in mainstream software (e.g. Firefox, Azure systems, etc.). More information on F* can be found at: http://fstar-lang.org/.

Armada: Low-Effort Verification of High-Performance Concurrent Programs (22^nd July, 11:30am – 12:30pm PST)

• Jay Lorch (Microsoft Research) and Upamanyu Sharma (University of Michigan, Microsoft Research)
• Meeting link : https://us02web.zoom.us/j/82444803238
• Abstract: Safely writing high-performance concurrent programs is notoriously difficult. To aid developers, we introduce Armada, a language and tool designed to formally verify such programs with relatively little effort. Via a C-like language and a small-step, state-machine-based semantics, Armada gives developers the flexibility to choose arbitrary memory layout and synchronization primitives so they are never constrained in their pursuit of performance. To reduce developer effort, Armada leverages SMT-powered automation and a library of powerful reasoning techniques, including rely-guarantee, TSO elimination, reduction, and alias analysis. All these techniques are proven sound, and Armada can be soundly extended with additional strategies over time. Using Armada, we verify four concurrent case studies and show that we can achieve performance equivalent to that of unverified code.

Almost two decades of software model checking at Microsoft (23^rd July, 7:00am – 8:00am PST)

• Shuvendu Lahiri (Microsoft Research) and Akash Lal (Microsoft Research)
• Meeting link: https://us02web.zoom.us/j/81938338032
• Abstract: The SLAM project, highlighted in CACM 2011, showcased a decade of successful software verification at Microsoft with application to Windows Device Drivers. This talk will describe the journey post SLAM to new verification algorithms, techniques, and tools, many of which have appeared at CAV over the years. With no shortage of software to verify, these tools continue to deliver value for Microsoft and its customers. The Corral verifier, hardened via close experimentation against SLAM, forms the base of these tools.  The Angelic Verifier is an extension to Corral that significantly reduces modeling and allowed the checking memory safety properties on Device Drivers for the first time. We will also describe new applications driven by these tools, such as the verification of smart contracts with VeriSol, as well as new challenges such as scalability and parallelization on the cloud.

Building Robust Asynchronous Systems with Microsoft Coyote (23^rd July, 11:30am – 12:30pm PST)

• Akash Lal (Microsoft Research), Pantazis Deligiannis (Microsoft Research), Chris Lovett (Microsoft Research), Suvam Mukherjee (Microsoft Research)
• Meeting link: https://us02web.zoom.us/j/81817677195
• Abstract: For developers, writing bug-free software that doesn’t crash is getting difficult in an increasingly competitive world where software needs to ship before it becomes obsolete. This challenge is especially apparent with online cloud services, which are often dictated by aggressive shipping deadlines. Cloud services are distributed programs comprising multiple back-end systems that continuously exchange asynchronous signals while responding to incoming web requests. They are complex by nature, hard to get right, and require protection from failures that could jeopardize client data or halt key services. A key challenge here is the non-determinism that arises from concurrency (thread interleavings, message orderings, etc.) as well as from the environment (crashes, timeouts, failures, etc.). This talk presents Coyote, an open-source .NET library from Microsoft Research for building robust asynchronous systems. Coyote provides a testing tool that takes over the non-determinism in the program and explores the state space using several intelligent search strategies looking for bugs. Coyote testing is fast and can be tightly integrated into the development cycle itself. Coyote is currently in use by several teams in Microsoft Azure to build production cloud services. Coyote is available on github: https://microsoft.github.io/coyote/

Network Verification for Azure Datacenters (24^th July, 7:00am – 8:00am PST)

• Andrey Rybalchenko, Nuno Lopes, Ryan Beckett (Microsoft Research) and Karthick Jayaraman (Microsoft Azure)
• Meeting link: https://us02web.zoom.us/j/82864367751
• Abstract: Network verification is a core fundamental for Azure Networking. The cost of network outages is high and router configuration changes are one of the major causes of outages. In this talk we will present our work on developing and deploying hyper-scalable network verification tools for Azure datacenter networks. These tools act as a gatekeeper verifying network configuration changes before their deployment in production, thus helping to prevent outages that may affect a large number of customers. We will start with a brief introduction into datacenter networking and verification problems, building analogies to classic model checking notions. Then we will deep dive into Network Logic Solver, a tool for efficient network simulation that scales to Azure datacenters. We will show how simulation results can be inspected using Spock, a network testing framework. Going beyond model checking, we will show how an interactive experience of executing changes is supported by One Network Emulator, a network emulation engine. Finally, we will demo the Azure gatekeeper service.