Portrait of Akash Lal

Akash Lal

Senior Researcher


I am a member of the Programming Languages and Tools Group at Microsoft Research India. I am broadly interested in the areas of programming languages, verification and model checking with a focus on concurrent programs. I graduated with a PhD from the Computer Sciences Department of University of Wisconsin-Madison, advised by Tom Reps.



I have served (or will serve) on the program committees of: VMCAI 2017, POPL 2017, FSTTCS 2016 (co-chair), CAV 2016, ISSTA 2016, TACAS 2016, NETYS 2016, ICSE (Demos) 2016, SCORE 2016, APSEC 2016, ISEC 2016, WEPL 2015, CAV 2015, ICSE 2015, VMCAI 2015 (co-chair), ASE 2015 (ERC), INFINITY 2014 (Scientific Committee), EC2 2014 (co-chair), ASE 2014 (ERC), MUSEPAT 2014, MUSEPAT 2013ESOP 2013, DSN 2013, VMCAI 2013, PADTAD 2012, APLAS 2012, CPP 2011, INFINITY 2011, INFINITY 2010, VMCAI 2011,CAV 2011, SPIN 2011, and PASTE 2011.


Safe Asynchronous Programming with P and P#

Established: March 15, 2016

We are designing programming languages for building safe and reliable asynchronous systems. The languages are based on the programming idiom of communicating state machines. They offer first-class support for writing safety and liveness specifications as well as building abstract models of code. They offer systematic testing capabilities that exhaustively (in the limit) tests all possible executions of the program, weeding out even hard-to-find concurrency bugs. P is a (domain-specific) programming language for modeling and specifying protocols…

Trusted Cloud

Established: August 31, 2015

The Trusted Cloud project at Microsoft Research aims to provide customers of cloud computing complete control over their data: no one should be able to access the data without the customer’s permission. Even if there are malicious employees in the cloud service provider, or hackers break into the data center, they still should not be able to get access to customer data. Trust model: We use a non-hierarchical trust model. That is, we don’t want…

Angelic Verification

Established: January 1, 2015

Angelic verification (AV) is a project for bringing the benefits of static assertion checking to production software without inundating users with false alarms and not burdening them with upfront modeling. In other words, the goal of AV is to democratize static assertion checking for any developer. Technically, this translates to finding precise interprocedural defect traces of assertion violations in open programs with under constrained environment (inputs and external methods). The philosophy of AV is to provide…

Corral Program Verifier

Established: May 9, 2013

Corral is a whole-program analysis tool for Boogie programs. Corral uses goal-directed symbolic search techniques to find assertion violations. It leverages the powerful theorem prover Z3. It is available open source on GitHub. 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. New: Microsoft Static Driver Verifier Benchmarks Corral powers Microsoft's Static Driver Verifier tool. This work has…


Established: February 7, 2012

Duality solves Relation Post-Fixed Point problems using Craig interpolation. In can be used, for example, to generate proofs for procedural programs in the form of procedure summaries. Duality is envisioned as a generic engine for program analysis, supporting applications such as automatic verification of sequential, concurrent and functional programs, as well as interactive refinement of manual proofs.

Boogie: An Intermediate Verification Language

Established: December 10, 2008

Boogie is an intermediate verification language, intended as a layer on which to build program verifiers for other languages. Several program verifiers have been built in this way, including the VCC and HAVOC verifiers for C and the verifiers for Dafny, Chalice, and Spec#. A previous version of the language was called BoogiePL. The current language (version 2) is currently known as just Boogie, which is also the name of the verification tool that takes…













Microsoft Static Driver Verifier Benchmarks

August 2017

This repository contains a subset of the internal tests used by Microsoft’s Static Driver Verifier tool. These tests are generated from Window’s Device Drivers while checking for one of the various properties that WDM drivers must satisfy.

    Click the icon to access this download

  • Website

Context-Bounded-Analysis Package

May 2010

    Click the icon to access this download

  • Website