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. For my thesis, I was a co-recipient of the ACM SIGPLAN Outstanding Doctoral Dissertation Award.

I have served (or will serve) on the program committees of: 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…

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…

Q Program Verifier

Established: May 9, 2013

The Q program verifier is a collection of front-ends that compile different source languages to an intermediate representation (IR), and back-ends that perform verification on the IR. Together, Q is a verification platform that hosts multiple tools and technologies for…


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…