divyeshunadkat
PhD, CSE, IIT Bombay. Advisers: Prof. Supratik Chakraborty and Prof. Ashutosh Gupta. Areas: software verification, program analysis, compilers.
Indian Institute of Technology BombayMumbai, India
Pinned Repositories
aeval
AE-solver and Skolemizer
diffy-artifact
Artifact for the paper titled "Diffy: Inductive Reasoning of Array Programs using Difference Invariants" in CAV 2021
divyeshunadkat.github.io
Personal Webpage
PARQ
PARQ is an automatic parallelization engine based on Skolem Function Synthesis and Quantified Invariant Generation. It is aimed at parallelization of array modifying programs written as Constrained Horn Clause (CHC) formulas.
sv-benchmarks
Collection of Verification Tasks
torch-mlir
The Torch-MLIR project aims to provide first class support from the PyTorch ecosystem to the MLIR ecosystem.
VAJRA
TACAS 2020 Artifacts for "Verifying Array Manipulating Programs with Full-program Induction"
freqhorn
A CHC solver that supports linear clauses, Integer arithmetic, and arrays.
sv-benchmarks
Collection of Verification Tasks (MOVED, please follow the link)
divyeshunadkat's Repositories
divyeshunadkat/VAJRA
TACAS 2020 Artifacts for "Verifying Array Manipulating Programs with Full-program Induction"
divyeshunadkat/PARQ
PARQ is an automatic parallelization engine based on Skolem Function Synthesis and Quantified Invariant Generation. It is aimed at parallelization of array modifying programs written as Constrained Horn Clause (CHC) formulas.
divyeshunadkat/aeval
AE-solver and Skolemizer
divyeshunadkat/diffy-artifact
Artifact for the paper titled "Diffy: Inductive Reasoning of Array Programs using Difference Invariants" in CAV 2021
divyeshunadkat/divyeshunadkat.github.io
Personal Webpage
divyeshunadkat/sv-benchmarks
Collection of Verification Tasks
divyeshunadkat/torch-mlir
The Torch-MLIR project aims to provide first class support from the PyTorch ecosystem to the MLIR ecosystem.