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

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


Patent

  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)

Tools

Open-WBO

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 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.

VerifOx

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

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

Walcyrie

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