Write a Blog >>
Thu 23 Jan 2020 14:43 - 15:05 at Ile de France III (IDF III) - Abstract Interpretation Chair(s): Xavier Rival

Abstract interpretation is a general framework for expressing static program analyses. It reduces the problem of extracting properties of a program to computing an approximation of the least fixpoint of a system of equations. The de facto approach for computing an approximation of this fixpoint uses a sequential algorithm based on weak topological order (WTO). This paper presents a deterministic parallel algorithm for fixpoint computation by introducing the notion of weak partial order (WPO). We present an algorithm for constructing a WPO in almost-linear time. Finally, we describe PIKOS, our deterministic parallel abstract interpreter, which extends the sequential abstract interpreter IKOS. We evaluate the performance and scalability of PIKOS on a suite of 1017 C programs. When using 4 cores, PIKOS achieves an average speedup of 2.06x over IKOS, with a maximum speedup of 3.63x. When using 16 cores, PIKOS achieves a maximum speedup of 10.97x.

slides (slides.pptx)5.9MiB

Thu 23 Jan

Displayed time zone: Saskatchewan, Central America change

14:00 - 15:05
Abstract InterpretationResearch Papers at Ile de France III (IDF III)
Chair(s): Xavier Rival INRIA/CNRS/ENS Paris
14:00
21m
Talk
Abstract Extensionality: On the Properties of Incomplete Abstract Interpretations
Research Papers
Roberto Bruni University of Pisa, Roberto Giacobazzi University of Verona and IMDEA Software Institute, Roberta Gori University of Pisa, Isabel Garcia-Contreras IMDEA Software Institute, Dusko Pavlovic University of Hawaii
Link to publication DOI Media Attached File Attached
14:21
21m
Talk
Abstract Interpretation of Distributed Network Control Planes
Research Papers
Ryan Beckett Microsoft Research, Aarti Gupta Princeton University, Ratul Mahajan University of Washington, Intentionet, David Walker Princeton University
Link to publication DOI Media Attached File Attached
14:43
21m
Talk
Deterministic Parallel Fixpoint Computation
Research Papers
Sung Kook Kim University of California, Davis, Arnaud J. Venet Facebook, Aditya V. Thakur University of California, Davis
Link to publication DOI Pre-print Media Attached File Attached