Saurabh Joshi bio photo

Saurabh Joshi

Assistant Professor, Department of CSE, Academic Block C, Cabin:312/F, IIT Hyderabad, Kandi, Sangareddy, Telangana- 502285, India

Email Google Scholar Github Orcid


Research simplified

An essential part of science is to be able to explain your work in simple terms to others. Here are some simple explanations by some of my students about their work in their own words.

Research Interests

Formal verification, automated repair, model-checking, concurrent programs, program analysis and constraint solving


  1. Saurabh Joshi, Shuvendu Lahiri and Akash Lal, “REDUCING FALSE ALARMS FOR STATIC ANALYSIS OF CONCURRENT PROGRAMS”, US Patent No : 8793664.

  1. DST Early Career Research Award for “Scope Enrichment of Verification Technologies” 2017-2020 (INR 22.5 lakh)



Open-WBO is an open source MaxSAT solver which can use any MiniSAT like off-the-shelf SAT solver underneath.

Accolades won by OpenWBO:

  • MaxSAT Evaluations 2019: 2 Bronze medal
  • MaxSAT Evaluations 2018: 1 Gold medal, 1 Silver medal
  • MaxSAT Evaluations 2017: 2 Gold medals, 1 Silver medal
  • MaxSAT Evaluations 2016: 1 Gold medal, 1 Silver medal, 1 Bronze medal
  • Pseudo-Boolean Evaluations 2016: 2 Silver medals, 2 Bronze medals
  • MaxSAT Evaluations 2015 : 1 Gold medal, 1 Silver medal
  • MaxSAT Floc Olympic Games 2014: 2 Gold medals
  • MaxSAT Evaluations 2014: 1 Gold medal, 1 Silver medal

Relevant papers are here, here and here.


Pinaka (named after the bow of Lord Shiva) is a symbolic execution engine built on top of CPROVER/SYMEX framework.

Accolade won by Pinaka:

  • 2nd place in ReachSafety-Floats subcategory in SVCOMP 2019.

VerifOx is a symbolic execution engine built on top of CPROVER framework. It is especially optimized for behaviourally equivalent C programs that are generated from Verilog circuits. paper

Summarizer (aka 2LS)

summarizer is a software verifier for C programs which uses a holistic combination of bounded model-checking, k-induction and abstract interpretation. paper summarizer aka 2LS won gold in floating point category at SVCOMP 2016


CBMC-Repair is built on top of CPROVER model-checking frame work which suggests optimum fence placement in a C program. paper


Walcyrie is a modification over CBMC model-checker that employs better encoding to make the model-checking more efficient over relaxed memory models.