Wed 28 Oct 2015 13:52 - 14:15 at Grand Station 1 - 3. Verification Chair(s): Guangtai Liang

We present jumping, a form of selective control-flow abstraction useful for improving the scalability of goal-directed static analyses. Jumping is useful for analyzing programs with complex control-flow such as event-driven systems. In such systems, accounting for orderings between certain events is important for precision, yet analyzing the product graph of all possible event orderings is intractable. Jumping solves this problem by allowing the analysis to selectively abstract away control-flow between events irrelevant to a goal query while preserving information about the ordering of relevant events. We present a framework for designing sound jumping analyses and create an instantiation of the framework for per- forming precise inter-event analysis of Android applications. Our experimental evaluation showed that using jumping to augment a precise goal-directed analysis with inter-event reasoning enabled our analysis to prove 90–97% of dereferences safe across our benchmarks.

Wed 28 Oct

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

13:30 - 15:00
3. VerificationOOPSLA at Grand Station 1
Chair(s): Guangtai Liang IBM Research - China
13:30
22m
Talk
Conditionally Correct Superoptimization
OOPSLA
Rahul Sharma Stanford University, Eric Schkufza Stanford University, Berkeley Churchill Stanford University, Alex Aiken Stanford University
DOI
13:52
22m
Talk
Selective Control-Flow Abstraction via JumpingOOPSLA Artifact
OOPSLA
Sam Blackshear University of Colorado at Boulder, USA, Bor-Yuh Evan Chang University of Colorado at Boulder, USA, Manu Sridharan Samsung Research America
Link to publication
14:15
22m
Talk
Automating Grammar ComparisonOOPSLA Artifact
OOPSLA
Ravichandhran Madhavan EPFL, Switzerland, Mikaël Mayer EPFL, Switzerland, Sumit Gulwani Microsoft Research, USA, Viktor Kunčak EPFL, Switzerland
Link to publication
14:37
22m
Talk
Reasoning about the POSIX File System: Local Update and Global Pathnames
OOPSLA
Gian Ntzik Imperial College London, UK, Philippa Gardner Imperial College London, UK
DOI