Unknown Title

Description

This book constitutes the refereed proceedings of the 24th International Static Analysis Symposium, SAS 2017, held in New York, NY, USA, in August/September 2017. The 22 papers presented in this volume were carefully reviewed and selected from 50 submissions. The papers cover various aspects of the presentation of theoretical, practical, and applicational advances in area of static analysis that is recognized as a fundamental tool for program verification, bug detection, compiler organization, program understanding, and software maintenance. Front Matter ....Pages I-XIV Probabilistic Horn Clause Verification (Aws Albarghouthi)....Pages 1-22 Combining Forward and Backward Abstract Interpretation of Horn Clauses (Alexey Bakhirkin, David Monniaux)....Pages 23-45 Abstract Semantic Diffing of Evolving Concurrent Programs (Ahmed Bouajjani, Constantin Enea, Shuvendu K. Lahiri)....Pages 46-65 Learning Shape Analysis (Marc Brockschmidt, Yuxin Chen, Pushmeet Kohli, Siddharth Krishna, Daniel Tarlow)....Pages 66-87 Securing the SSA Transform (Chaoqiang Deng, Kedar S. Namjoshi)....Pages 88-105 Relative Store Fragments for Singleton Abstraction (Leandro Facchinetti, Zachary Palmer, Scott F. Smith)....Pages 106-127 Loop Invariants from Counterexamples (Marius Greitschus, Daniel Dietsch, Andreas Podelski)....Pages 128-147 A Context-Sensitive Memory Model for Verification of C/C++ Programs (Arie Gurfinkel, Jorge A. Navas)....Pages 148-168 Effect Summaries for Thread-Modular Analysis (Lukáš Holík, Roland Meyer, Tomáš Vojnar, Sebastian Wolff)....Pages 169-191 Toward a Sound Analysis of Guarded LTI Loops with Inputs by Abstract Acceleration (Colas Le Guernic)....Pages 192-211 Scalable Minimizing-Operators on Polyhedra via Parametric Linear Programming (Alexandre Maréchal, David Monniaux, Michaël Périn)....Pages 212-231 Hyperhierarchy of Semantics - A Formal Framework for Hyperproperties Verification (Isabella Mastroeni, Michele Pasqua)....Pages 232-252 Thread-Local Semantics and Its Efficient Sequential Abstractions for Race-Free Programs (Suvam Mukherjee, Oded Padon, Sharon Shoham, Deepak D’Souza, Noam Rinetzky)....Pages 253-276 Quantitative Static Analysis of Communication Protocols Using Abstract Markov Chains (Abdelraouf Ouadjaout, Antoine Miné)....Pages 277-298 Portability Analysis for Weak Memory Models porthos: OneToolfor allModels (Hernán Ponce-de-León, Florian Furbach, Keijo Heljanko, Roland Meyer)....Pages 299-320 Template Polyhedra with a Twist (Sriram Sankaranarayanan, Mohamed Amin Ben Sassi)....Pages 321-341 A New Abstraction Framework for Affine Transformers (Tushar Sharma, Thomas Reps)....Pages 342-363 Synthesizing Imperative Programs from Examples Guided by Static Analysis (Sunbeom So, Hakjoo Oh)....Pages 364-381 A Gradual Interpretation of Union Types (Matías Toro, Éric Tanter)....Pages 382-404 Modular Demand-Driven Analysis of Semantic Difference for Program Versions (Anna Trostanetski, Orna Grumberg, Daniel Kroening)....Pages 405-427 Verifying Array Manipulating Programs by Tiling (Supratik Chakraborty, Ashutosh Gupta, Divyesh Unadkat)....Pages 428-449 Incremental Analysis for Probabilistic Programs (Jieyuan Zhang, Yulei Sui, Jingling Xue)....Pages 450-472 Back Matter ....Pages 473-473