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

POPL-2020-Research-Papers
14:00 - 15:05: Research Papers - Abstract Interpretation at Ile de France III (IDF III)
Chair(s): Xavier RivalINRIA/CNRS/ENS Paris
POPL-2020-Research-Papers14:00 - 14:21
Talk
Roberto BruniUniversity of Pisa, Roberto GiacobazziUniversity of Verona and IMDEA Software Institute, Roberta GoriUniversity of Pisa, Isabel Garcia-ContrerasIMDEA Software Institute, Dusko PavlovicUniversity of Hawaii
Link to publication DOI Media Attached File Attached
POPL-2020-Research-Papers14:21 - 14:43
Talk
Ryan BeckettMicrosoft Research, Aarti GuptaPrinceton University, Ratul MahajanUniversity of Washington, Intentionet, David WalkerPrinceton University
Link to publication DOI Media Attached File Attached
POPL-2020-Research-Papers14:43 - 15:05
Talk
Sung Kook KimUniversity of California, Davis, Arnaud J. VenetFacebook, Aditya V. ThakurUniversity of California, Davis
Link to publication DOI Pre-print Media Attached File Attached