Program Analysis

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.

OpenMP aware MHP Analysis for Improved Static Data-Race Detection

This paper employs MHP analysis inside LLOV, to increase coverage of OpenMP pragmas for data-race checking for OpenMP Programs.

LLOV: A Fast Static Data-Race Checker for OpenMP Programs

This paper presents a tool, LLOV, which leverages polyhedral compilation for fast data-race checking for OpenMP Programs.

LLOV

A static data-race checker for OpenMP programs.

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.

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.

Property-Driven Fence Insertion Using Reorder Bounded Model Checking

This paper introduces Re-Order Bounded Model Checking to efficiently repair programs on weak memory models.

A New Method of {MHP} Analysis for Languages with Dynamic Barriers

This paper presents a technique to perform May-Happen-in-Parallel analysis for languages with Dynamic Barriers.

Underspecified harnesses and interleaved bugs

This paper presents a technique to find interleaved bugs even with incomplete harness.