This paper employs MHP analysis inside LLOV, to increase coverage of OpenMP pragmas for data-race checking for OpenMP Programs.
This paper presents a tool, LLOV, which leverages polyhedral compilation for fast data-race checking for OpenMP Programs.
A static data-race checker for OpenMP 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.
This paper presents a different encoding that makes Bounded Model Checking faster for concurrent programs.
This paper describes a sound and complete tool, 2LS, for program verification and the techniques behind its working.
This paper introduces Re-Order Bounded Model Checking to efficiently repair programs on weak memory models.
This paper presents a technique to perform May-Happen-in-Parallel analysis for languages with Dynamic Barriers.
This paper presents a technique to find interleaved bugs even with incomplete harness.
Static assertion checking of open programs requires setting up a precise harness to capture the environment assumptions. For instance, a library may require a file handle to be properly initialized before it is passed into it. A harness is used to …