Formal Verification

LLOR: Automated Repair of OpenMP Programs

This paper presents a tool and a technique to fix data-race in certain subset of OpenMP programs by suggesting barrier insertions.

GPURepair: Automated Repair of GPU Kernels (Extended Version)

This paper presents a tool and a technique to fix data-race and barrier divergence errors in CUDA and OpenCL programs.

GPURepair: Automated Repair of GPU Kernels

This paper presents a tool and a technique to fix data-race and barrier divergence errors in CUDA and OpenCL programs.

Pinaka: Symbolic Execution Meets Incremental Solving - (Competition Contribution)

This paper describes, Pinaka, a symbolic execution engine that leverages incremental SAT solving.

GPURepair

A tool for automated repair of CUDA and OpenCL kernels

Pinaka

A symbolic execution engine

Precise Predictive Analysis for Discovering Communication Deadlocks in MPI Programs

This paper shows NP-completeness of deadlock detection in certain class of MPI programs. It also presents encoding to analyze a class of MPI programs with respect to deadlocks.

Equivalence Checking of a Floating-Point Unit Against a High-Level C Model

This paper describes an efficient technique for equivalence checking of a real-world Floating Point Unit.

The virtues of conflict: analysing modern concurrency

This paper presents a different encoding that makes Bounded Model Checking faster for concurrent programs.

Safety Verification and Refutation by $k$-Invariants and $k$-Induction

This paper describes a sound and complete tool, 2LS, for program verification and the techniques behind its working.