SPLASH Workshops 2020
2020 ACM SIGPLAN International Conference on Systems, Programming, Languages, and Applications: Software for Humanity (SPLASH Workshops 2020)
Powered by
Conference Publishing Consulting

11th ACM SIGPLAN International Workshop on Tools for Automatic Program Analysis (TAPAS 2020), November 17, 2020, Virtual, USA

TAPAS 2020 – Preliminary Table of Contents

Contents - Abstracts - Authors

11th ACM SIGPLAN International Workshop on Tools for Automatic Program Analysis (TAPAS 2020)


Title Page

Message from the Chairs


API Analytics for Curating Static Analysis Rules
Vineeth Kashyap, Roger Scott, Joseph Ranieri, David Melski, and Lucja Kot
(GrammaTech, USA)
Use of third-party library APIs is pervasive, but can be error-prone. API-usage errors can be detected via static analysis if specifications of correct usage are available, but manually creating such specifications is a bottleneck. We showcase a semi-automated "big code" solution, where we use large code corpora to mine patterns in API usage, and ask human experts to perform analytics on those patterns to create static analysis rules.

Article Search
MetaCG: Annotated Call-Graphs to Facilitate Whole-Program Analysis
Jan-Patrick Lehr, Alexander Hück, Yannic Fischler, and Christian Bischof
(TU Darmstadt, Germany)
The paper presents the extendable C/C++ whole-program call-graph tool MetaCG. We introduce its graph library, the Clang-based tool CGCollector to construct the call graph and attach meta information, and CGValidate to check for missing edges given a particular execution. MetaCG offers extendability through its metadata function-annotation mechanism to transfer information between tools. It preserves inheritance hierarchies and can be serialized into JSON. We evaluate CG-Collector’s ability to construct whole-program call-graphs for C/C++ code and, subsequently, present a performance profiler and a memory sanitizer that rely on MetaCG for whole-program call-graph information

Article Search
Online Verification of Commutativity
Aditi Kabra, Dietrich Geisler, and Adrian Sampson
(Carnegie Mellon University, USA; Cornell University, USA)
Systems of transformations arise in many programming systems, such as in graphs of implicit type conversion functions. It is important to ensure that these diagrams commute: that composing any path of transformations from the same source to the same destination yields the same result. However, a straightforward approach to verifying commutativity must contend with cycles, and even so it runs in exponential time. Previous work has shown how to verify commutativity in the special case of acyclic diagrams in O(|V|4|E|2) time, but this is a batch algorithm: the entire diagram must be known ahead of time. We present an online algorithm that efficiently verifies that a commutative diagram remains commutative when adding a new edge. The new incremental algorithm runs in O(|V|2(|E| + |V|)) time. For the case when checking the equality of paths is expensive, we also present an optimization that runs in O(|V|4) time but reduces to the minimum possible number of equality checks. We implement the algorithms and compare them to batch baselines, and we demonstrate their practical application in the compiler of a domain-specific language for geometry types. To study the algorithms’ scalability to large diagrams, we apply them to discover discrepancies in currency conversion graphs.

Article Search
Towards Checkpoint Placement for Dynamic Memory Allocation in Intermittent Computing
Nicholas Shoemaker, Ruzica Piskac, and Mark Santolucito
(Branford High School, USA; Yale University, USA; Barnard College, USA)
Energy harvesting allows computational devices to run without a battery, opening new application domains of computing. Such devices work under an intermittent computing model, where the system may power cycle several times a second. To ensure progress, intermittent computing uses checkpoints, with much work being dedicated to this direction. However, no existing approaches handle programs using dynamically allocated memory in the intermittent computing model. We pose this as a challenge area, demonstrate the complexities of checkpointing in this space, and propose key characteristics of an effective solution.

Article Search
Type Checking beyond Type Checkers, via Slice & Run
Justus Adam and Stephen Kell
(University of Kent, UK)

Article Search

proc time: 1.47