May 2015 – July 2015

Microsoft Research India

Software Engineering Intern

TruMP: Trusted Multi Party Computations using SGX
May 2014 – July 2014

Laboratory for Specification and Verification, ENS

Research Intern

Nash Equilibrium in Pushdown Games
May 2013 – July 2013

Microsoft Research- INRIA Joint Centre

Research Intern

Developing libraries for TLA-Proof System


. Automatic Repair of Resource Leaks in Android Applications. Under Submission, 2020.


. Almost Event-Rate Independent Monitoring. Journal: Formal Methods in System Design (FMSD), 2019.


. Optimal Proofs for Linear Temporal Logic on Lasso Words. In Automated Technology for Verification and Analysis (ATVA), [Distinguished Paper Award] , 2018.

Preprint PDF Code Slides DOI

. Game-based cryptography in HOL. In Archive of Formal Proofs, 2017.

PDF Source Document

. Almost Event-Rate Independent Monitoring of Metric Temporal Logic. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2017.

Preprint PDF Code Slides DOI


DroidPLUMB: Repairing Resource-Leak bugs with Static Analysis
Dec 5, 2019
Event-Rate Independence in Runtime Monitoring
Dec 8, 2016
TruMP: Trusted Multi Party Computation on SGX Enclaves
Jul 10, 2015
Logics for Dependence and Independence
Oct 14, 2014


Teaching Duties at ETH Zurich:

  • Formal Methods and Functional Programming (FMFP): Spring 2016, Spring 2017
  • Informatics for Mathematics and Physics (IFMP): Fall 2016, Fall 2017

Teaching Duties at USI Lugano:

  • Software Analysis: Spring 2019, Spring 2020
  • Web Atelier: Fall 2019
  • Systems Programming: Spring 2019


  • bhattb@usi.ch
  • bhargavbh
  • Software Institute, USI Lugano, via Giuseppe Buffi 13, 6900 Lugano
  • On Appointment: 309 (Level 3), Software Institute, Via S Balestra 22, 6900 Lugano.