Saurabh Joshi
Assistant Professor Department of CSE, Academic Block C, Cabin: 312/F, IIT Hyderabad Kandi, Sangareddy Telangana, India - 502285 Email : sbjoshi@iith.ac.in
Assistant Professor Department of CSE, Academic Block C, Cabin: 312/F, IIT Hyderabad Kandi, Sangareddy Telangana, India - 502285 Email : sbjoshi@iith.ac.in
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.
Formal verification, automated repair, model-checking, concurrent programs, program analysis and constraint solving
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
CBMC-Repair is built on top of CPROVER model-checking frame work which suggests optimum fence placement in a C program. paper
Open-WBO is an open source MaxSAT solver which can use any MiniSAT like off-the-shelf SAT solver underneath. Open-WBO won 2 gold and 1 silver in the MaxSAT 2017 evaluations. It also won the MaxSAT 2014 evaluations for unweighted MaxSAT category for industrial benchmarks. It also secured a second place for partial MaxSAT category for industrial benchmarks. It was ranked secnd and third for various categories of benchmarks in Pseudo-Boolean Competition 2016. Relevant papers are here and here.
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
Walcyrie is a modification over CBMC model-checker that employs better encoding to make the model-checking more efficient over relaxed memory models.