This paper presents a tool and a technique to fix data-race and barrier divergence errors in CUDA and OpenCL programs.
This paper describes, Pinaka, a symbolic execution engine that leverages incremental SAT solving.
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 describes an efficient technique for equivalence checking of a real-world Floating Point Unit.
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 for automatically constructing a fix for buggy concurrent programs: given a concurrent program that does not satisfy user-provided assertions, we infer atomic blocks that fix the program. An atomic block protects a …
This paper presents a technique to find interleaved bugs even with incomplete harness.
SystemC is a popular language used in modeling system-on-chip implementations. To support this task at a high level of abstraction, transaction-level modeling (TLM) libraries have been recently developped. While TLM libraries are useful, it is …