Static Analysis: 25th International Symposium, SAS 2018, Freiburg, Germany, August 29–31, 2018, Proceedings

Description

This book constitutes the refereed proceedings of the 25th International Static Analysis Symposium, SAS 2018, held in Freiburg, Germany, in August 2018. The 18 papers presented in this volume were carefully reviewed and selected from 37 submissions. The contributions cover a variety of multi-disciplinary topics in abstract domains: program verication, bug detection, compiler optimization, program understanding, and software maintenance. Front Matter ....Pages I-X Fairness: A Formal-Methods Perspective (Aws Albarghouthi)....Pages 1-4 The MISRA C Coding Standard and its Role in the Development and Analysis of Safety- and Security-Critical Embedded Software (Roberto Bagnara, Abramo Bagnara, Patricia M. Hill)....Pages 5-23 Numerical Invariants via Abstract Machines (Zachary Kincaid)....Pages 24-42 Deductive Verification in Decidable Fragments with Ivy (Kenneth L. McMillan, Oded Padon)....Pages 43-55 Experience Developing and Deploying Concurrency Analysis at Facebook (Peter O’Hearn)....Pages 56-70 New Applications of Software Synthesis: Verification of Configuration Files and Firewall Repair (Ruzica Piskac)....Pages 71-76 Interactive Verification of Distributed Protocols Using Decidable Logic (Sharon Shoham)....Pages 77-85 Abstract Interpretation of Stateful Networks (Kalev Alpernas, Roman Manevich, Aurojit Panda, Mooly Sagiv, Scott Shenker, Sharon Shoham et al.)....Pages 86-106 Block-Size Independence for GPU Programs (Rajeev Alur, Joseph Devietti, Nimit Singhania)....Pages 107-126 Extending Constraint-Only Representation of Polyhedra with Boolean Constraints (Alexey Bakhirkin, David Monniaux)....Pages 127-145 An Efficient Abstract Domain for Not Necessarily Closed Polyhedra (Anna Becchi, Enea Zaffanella)....Pages 146-165 Modular Software Fault Isolation as Abstract Interpretation (Frédéric Besson, Thomas Jensen, Julien Lepiller)....Pages 166-186 Closing the Performance Gap Between Doubles and Rationals for Octagons (Aziem Chawdhary, Andy King)....Pages 187-204 Verifying Properties of Differentiable Programs (Jan Hückelheim, Ziqing Luo, Sri Hari Krishna Narayanan, Stephen Siegel, Paul D. Hovland)....Pages 205-222 A Reduced Product of Absolute and Relative Error Bounds for Floating-Point Analysis (Maxime Jacquemin, Sylvie Putot, Franck Védrine)....Pages 223-242 Modular Static Analysis of String Manipulations in C Programs (Matthieu Journault, Antoine Miné, Abdelraouf Ouadjaout)....Pages 243-262 Verifying Bounded Subset-Closed Hyperproperties (Isabella Mastroeni, Michele Pasqua)....Pages 263-283 Process-Local Static Analysis of Synchronous Processes (Jan Midtgaard, Flemming Nielson, Hanne Riis Nielson)....Pages 284-305 The Impact of Program Transformations on Static Program Analysis (Kedar S. Namjoshi, Zvonimir Pavlinovic)....Pages 306-325 Efficiently Learning Safety Proofs from Appearance as well as Behaviours (Sumanth Prabhu, Kumar Madhukar, R. Venkatesh)....Pages 326-343 Invertible Linear Transforms of Numerical Abstract Domains (Francesco Ranzato, Marco Zanella)....Pages 344-363 Incremental Verification Using Trace Abstraction (Bat-Chen Rothenberg, Daniel Dietsch, Matthias Heizmann)....Pages 364-382 Volume-Based Merge Heuristics for Disjunctive Numeric Domains (Andrew Ruef, Kesha Hietala, Arlen Cox)....Pages 383-401 Abstract Interpretation of CTL Properties (Caterina Urban, Samuel Ueltschi, Peter Müller)....Pages 402-422 Inductive Termination Proofs with Transition Invariants and Their Relationship to the Size-Change Abstraction (Florian Zuleger)....Pages 423-444 Back Matter ....Pages 445-445