Francesco Ranzato
Proceedings of the 24th International Static Analysis Symposium
SAS, 2017.

@proceedings{SAS-2017,
	doi           = "10.1007/978-3-319-66706-5",
	editor        = "Francesco Ranzato",
	isbn          = "['978-3-319-66705-8', '978-3-319-66706-5']",
	publisher     = "{Springer}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the 24th International Static Analysis Symposium}",
	volume        = 10422,
	year          = 2017,
}

Contents (22 items)

SAS-2017-Albarghouthi #horn clause #probability #verification

Probabilistic Horn Clause Verification (AA), pp. 1–22.

SAS-2017-BakhirkinM #abstract interpretation #horn clause

Combining Forward and Backward Abstract Interpretation of Horn Clauses (AB, DM), pp. 23–45.

SAS-2017-BouajjaniEL #concurrent #difference #evolution #semantics #source code

Abstract Semantic Diffing of Evolving Concurrent Programs (AB, CE, SKL), pp. 46–65.

SAS-2017-BrockschmidtCKK #analysis #learning

Learning Shape Analysis (MB, YC, PK, SK, DT), pp. 66–87.

SAS-2017-DengN

Securing the SSA Transform (CD, KSN), pp. 88–105.

SAS-2017-FacchinettiPS #abstraction

Relative Store Fragments for Singleton Abstraction (LF, ZP, SFS0), pp. 106–127.

SAS-2017-GreitschusDP #invariant

Loop Invariants from Counterexamples (MG, DD, AP), pp. 128–147.

SAS-2017-GurfinkelN #c #c++ #memory management #source code #verification

A Context-Sensitive Memory Model for Verification of C/C++ Programs (AG, JAN), pp. 148–168.

SAS-2017-HolikMVW #analysis #heuristic #summary #thread

Effect Summaries for Thread-Modular Analysis - Sound Analysis Despite an Unsound Heuristic (LH, RM0, TV, SW), pp. 169–191.

SAS-2017-Guernic #analysis #towards

Toward a Sound Analysis of Guarded LTI Loops with Inputs by Abstract Acceleration (CLG), pp. 192–211.

SAS-2017-MarechalMP #linear #parametricity #programming #scalability

Scalable Minimizing-Operators on Polyhedra via Parametric Linear Programming (AM, DM, MP), pp. 212–231.

SAS-2017-MastroeniP #framework #semantics #verification

Hyperhierarchy of Semantics - A Formal Framework for Hyperproperties Verification (IM, MP), pp. 232–252.

SAS-2017-MukherjeePSDR #abstraction #performance #semantics #source code #thread

Thread-Local Semantics and Its Efficient Sequential Abstractions for Race-Free Programs (SM, OP, SS, DD, NR), pp. 253–276.

SAS-2017-OuadjaoutM #communication #markov #protocol #static analysis #using

Quantitative Static Analysis of Communication Protocols Using Abstract Markov Chains (AO, AM), pp. 277–298.

SAS-2017-LeonFHM #analysis #memory management #modelling

Portability Analysis for Weak Memory Models. PORTHOS: One Tool for all Models (HPdL, FF, KH, RM0), pp. 299–320.

SAS-2017-Sankaranarayanan

Template Polyhedra with a Twist (SS0, MABS), pp. 321–341.

SAS-2017-SharmaR #abstraction #framework

A New Abstraction Framework for Affine Transformers (TS, TWR), pp. 342–363.

SAS-2017-SoO #imperative #source code #static analysis

Synthesizing Imperative Programs from Examples Guided by Static Analysis (SS, HO), pp. 364–381.

SAS-2017-ToroT

A Gradual Interpretation of Union Types (MT, ÉT), pp. 382–404.

SAS-2017-TrostanetskiGK #analysis #composition #difference #semantics

Modular Demand-Driven Analysis of Semantic Difference for Program Versions (AT, OG, DK), pp. 405–427.

SAS-2017-ChakrabortyGU #array #source code #verification

Verifying Array Manipulating Programs by Tiling (SC, AG, DU), pp. 428–449.

SAS-2017-ZhangSX #analysis #incremental #probability #source code

Incremental Analysis for Probabilistic Programs (JZ, YS, JX), pp. 450–472.