ETAPS 2019
Sat 6 - Thu 11 April 2019 Prague, Czech Republic
Tue 9 Apr 2019 11:00 - 11:30 at JUPITER - Software Verification I Chair(s): Wil van der Aalst

Static program analysis often encounters problems in analyzing library code. Most real-world programs use library functions intensively, and library functions are usually written in different languages. For example, static analysis of JavaScript programs requires analysis of the standard built-in library implemented in host environments. A common approach to analyze such opaque code is for analysis developers to build models that provide the semantics of the opaque code. Models can be built either manually, which is time consuming and error prone, or automatically, which may limit application to different languages or analyzers. In this paper, we present a novel mechanism to support automatic modeling of opaque code, which is applicable to various languages and analyzers. For a given static analysis, our approach automatically computes analysis results of opaque code via dynamic testing during static analysis. By using testing techniques, the mechanism does not guarantee sound over-approximation of program behaviors in general. However, it is fully automatic, is scalable in terms of the size of opaque code, and provides more precise results than conventional over-approximation approaches. Our evaluation shows that although not all functionalities in opaque code can (or should) be modeled automatically using our technique, a large number of JavaScript built-in functions are approximated soundly yet more precisely than existing manual models.

Tue 9 Apr

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

10:30 - 12:30
Software Verification IFASE at JUPITER
Chair(s): Wil van der Aalst RWTH Aachen
10:30
30m
Talk
Tool Support for Correctness-by-Construction
FASE
Tobias Runge TU Braunschweig, Ina Schaefer Technische Universität Braunschweig, Loek Cleophas Eindhoven University of Technology (TU/e) and Stellenbosch University (SU), Thomas Thüm University of Ulm, Derrick Kourie Stellenbosch University, Bruce W Watson
Link to publication
11:00
30m
Talk
Automatic Modeling for Opaque Code in JavaScript Static Analysis
FASE
Joonyoung Park , Alexander Jordan Oracle Labs, Australia, Sukyoung Ryu KAIST, South Korea
Link to publication
11:30
30m
Talk
SMT-Based Bounded Schedulability Analysis of the Clock Constraint Specification Language
FASE
Min Zhang East China Normal University, Fu Song , Frederic Mallet Université Côte d'Azur, France, Xiaohong Chen
Link to publication
12:00
30m
Talk
A Hybrid Dynamic Logic for Event/Data-based SystemsBest paper nomination
FASE
Rolf Hennicker Ludwig Maximilians University Munich, Germany, Alexandre Madeira , Alexander Knapp
Link to publication