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
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

10:30 - 12:30: Software Verification IFASE at JUPITER
Chair(s): Wil van der AalstRWTH Aachen
10:30 - 11:00
Talk
Tool Support for Correctness-by-Construction
FASE
Tobias RungeTU Braunschweig, Ina SchaeferTechnische Universität Braunschweig, Loek CleophasEindhoven University of Technology (TU/e) and Stellenbosch University (SU), Thomas ThümTU Braunschweig, Germany, Derrick KourieStellenbosch University, Bruce W Watson
Link to publication
11:00 - 11:30
Talk
Automatic Modeling for Opaque Code in JavaScript Static Analysis
FASE
Joonyoung Park, Alexander JordanOracle Labs, Australia, Sukyoung RyuKAIST, South Korea
Link to publication
11:30 - 12:00
Talk
SMT-Based Bounded Schedulability Analysis of the Clock Constraint Specification Language
FASE
Min ZhangEast China Normal University, Fu Song, Frederic MalletUniversité Côte d'Azur, France, Xiaohong Chen
Link to publication
12:00 - 12:30
Talk
A Hybrid Dynamic Logic for Event/Data-based SystemsBest paper nomination
FASE
Rolf HennickerLudwig Maximilians University Munich, Germany, Alexandre Madeira, Alexander Knapp
Link to publication