ETAPS 2019
Sat 6 - Thu 11 April 2019 Prague, Czech Republic
Thu 11 Apr 2019 15:30 - 16:00 at SUN I - Safety and Fault-tolerant Systems Chair(s): Rance Cleaveland

Static program analysis is used to automatically determine program properties, or to detect bugs or security vulnerabilities in programs. It can be used as a stand-alone tool or to aid compiler optimization as an intermediary step. Developing precise, inter-procedural static analyses, however, is a challenging task, due to the algorithmic complexity, implementation effort, and the threat of state explosion which leads to unsatisfactory performance. Software written in C and C++ is notoriously hard to analyze because of the deliberately unsafe type system, unrestricted use of pointers, and (for C++) virtual dispatch. In this work, we describe the design and implementation of the LLVM-based static analysis framework for C/C++ code. PhASAR allows data-flow problems to be solved in a fully automated manner. It provides class hierarchy, call-graph, points-to, and data-flow information, hence requiring analysis developers only to specify a definition of the data-flow problem. PhASAR thus hides the complexity of static analysis behind a high-level API, making static program analysis more accessible and easy to use. PhASAR is available as an open-source project. We evaluate PhASAR’s scalability during whole-program analysis. Analyzing 12 real-world programs using a taint analysis written in PhASAR, we found ’s abstractions and their implementations to provide a whole-program analysis that scales well to real-world programs. Furthermore, we peek into the details of analysis runs, discuss our experience in developing static analyses for C/C++, and present possible future improvements.

Thu 11 Apr

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

14:00 - 16:00
Safety and Fault-tolerant SystemsTACAS at SUN I
Chair(s): Rance Cleaveland University of Maryland
14:00
30m
Talk
Digital Bifurcation Analysis of TCP Dynamics
TACAS
Link to publication
14:30
30m
Talk
Verifying Safety of Synchronous Fault-Tolerant Algorithms by Bounded Model Checking
TACAS
Ilina Stoilkovska Vienna University of Technology , Igor Konnov Inria Nancy, Josef Widder TU Wien, Florian Zuleger Vienna University of Technology
Link to publication
15:00
30m
Talk
Measuring Masking Fault-Tolerance
TACAS
Pablo Castro Dept. of Computer Science FCEFQyN, University of Rio Cuarto, Pedro D'Argenio , Ramiro Demasi , Luciano Putruele
Link to publication
15:30
30m
Talk
PhASAR: An Inter-Procedural Static Analysis Framework for C/C++
TACAS
Philipp Dominik Schubert Heinz Nixdorf Institut, Paderborn University, Ben Hermann University of Paderborn, Eric Bodden Heinz Nixdorf Institut, Paderborn University and Fraunhofer IEM
Link to publication