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
Times are displayed in time zone: Central Time (US & Canada) change

03:00 - 04:20: Session 1TAPAS at SPLASH-V
03:00 - 03:20
Paper
TAPAS
03:20 - 03:40
Paper
TAPAS
Jan-Patrick LehrScientific Computing, TU Darmstadt, Alexander HückInstitute for Scientific Computing, TU Darmstadt, Yannic FischlerTU Darmstadt, Christian BischofScientific Computing, TU Darmstadt
03:40 - 04:00
Paper
TAPAS
04:00 - 04:20
Paper
TAPAS
Justus AdamUniversity of Kent, UK, Stephen KellUniversity of Kent
Pre-print