SPLASH 2020
Sun 15 - Sat 21 November 2020 Online Conference
Thu 19 Nov 2020 04:00 - 04:20 at SPLASH-V - Session 1

Type checkers are the most commonly used form of static analysis, but their design is coupled to the rest of the language, making it hard or impossible to bring new kinds of reasoning to existing, unmodified code.

We propose a novel approach to checking advanced type invariants and properties in unmodified source code, while approaching the speed and ease of simple, syntax directed type checkers. The insight is that by combining a deep program analysis (symbolic execution) with a cheaper program abstraction (based on program slicing), it appears possible to reconstitute type-checking in the context of an underapproximate analysis. When the program’s ‘type level’ can be opportunistically disentangled from the ‘value level’, this is done by the program abstraction step, in some cases removing the underapproximation.

We implement a simple prototype that demonstrates this idea by checking the safety of generic pointers in C, pointing to benefits such as safe homogeneous and heterogeneous generic data structures.

Thu 19 Nov

Displayed time zone: Central Time (US & Canada) change

03:00 - 04:20
Session 1TAPAS at SPLASH-V
03:00
20m
Paper
Program Slicing with Exception Handling
TAPAS
03:20
20m
Paper
MetaCG: Annotated call-graphs to facilitate whole-program analysis
TAPAS
Jan-Patrick Lehr Scientific Computing, TU Darmstadt, Alexander Hück Institute for Scientific Computing, TU Darmstadt, Yannic Fischler TU Darmstadt, Christian Bischof Scientific Computing, TU Darmstadt
03:40
20m
Paper
Data Dependence for Object-Oriented Programs
TAPAS
04:00
20m
Paper
Type checking beyond type checkers, via Slice & Run
TAPAS
Justus Adam University of Kent, UK, Stephen Kell University of Kent
Pre-print