Issue Downloads
Proving Correctness of Parallel Implementations of Transition System Models
This article addresses the long-standing problem of program correctness for programs that describe systems of parallel executing processes. We propose a new method for proving correctness of parallel implementations of high-level models expressed as ...
(De/Re)-Composition of Data-Parallel Computations via Multi-Dimensional Homomorphisms
Data-parallel computations, such as linear algebra routines and stencil computations, constitute one of the most relevant classes in parallel computing, e.g., due to their importance for deep learning. Efficiently de-composing such computations for the ...
Limits and Difficulties in the Design of Under-Approximation Abstract Domains
The main goal of most static analyses is to prove the absence of bugs: if the analysis reports no alarms, then the program will not exhibit any unwanted behaviours. For this reason, they are designed to over-approximate program behaviours and, ...