Francesco Logozzo, Manuel Fähndrich
Proceedings of the 20th International Static Analysis Symposium
SAS, 2013.

@proceedings{SAS-2013,
	address       = "Seattle, Washington, USA",
	doi           = "10.1007/978-3-642-38856-9",
	editor        = "Francesco Logozzo and Manuel Fähndrich",
	isbn          = "978-3-642-38855-2",
	publisher     = "{Springer International Publishing}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the 20th International Static Analysis Symposium}",
	volume        = 7935,
	year          = 2013,
}

Contents (25 items)

6 ×#source code
6 ×#verification
4 ×#abstract domain
4 ×#abstract interpretation
3 ×#analysis
3 ×#automaton
2 ×#automation
2 ×#concurrent
2 ×#memory management
2 ×#quantifier

SAS-2013-Goubault #abstract interpretation #source code #static analysis

Static Analysis by Abstract Interpretation of Numerical Programs and Systems, and FLUCTUAT (EG), pp. 1–3.

SAS-2013-Sankaranarayanan #static analysis

Static Analysis in the Continuously Changing World (SS), pp. 4–5.

SAS-2013-GangeNSSS #abstract domain #abstract interpretation

Abstract Interpretation over Non-lattice Abstract Domains (GG, JAN, PS, HS, PJS), pp. 6–24.

SAS-2013-AmatoS

Localizing Widening and Narrowing (GA, FS), pp. 25–42.

SAS-2013-Urban #abstract domain #ranking

The Abstract Domain of Segmented Ranking Functions (CU), pp. 43–62.

SAS-2013-PelegSYY #automaton #mining #specification

Symbolic Automata for Static Specification Mining (HP, SS, EY, HY), pp. 63–83.

SAS-2013-DanMVY #abstraction #memory management #modelling

Predicate Abstraction for Relaxed Memory Models (AMD, YM, MTV, EY), pp. 84–104.

SAS-2013-BjornerMR #horn clause #on the #quantifier

On Solving Universally Quantified Horn Clauses (NB, KLM, AR), pp. 105–125.

SAS-2013-Roy #source code

From Concrete Examples to Heap Manipulating Programs (SR), pp. 126–149.

SAS-2013-DragoiES #analysis #data type

Local Shape Analysis for Overlaid Data Structures (CD, CE, MS), pp. 150–171.

SAS-2013-0001MP #abstract domain #automaton #quantifier

Quantified Data Automata on Skinny Trees: An Abstract Domain for Lists (PG, PM, GP), pp. 172–193.

SAS-2013-KimDS #documentation #html #parsing #semantics #validation

Static Validation of Dynamically Generated HTML Documents Based on Abstract Parsing and Semantic Processing (HK, KGD, DAS), pp. 194–214.

SAS-2013-DudkaPV #low level #verification

Byte-Precise Verification of Low-Level List Manipulation (KD, PP, TV), pp. 215–237.

SAS-2013-PartushY #difference #semantics #source code

Abstract Semantic Differencing for Numerical Programs (NP, EY), pp. 238–258.

SAS-2013-Komondoor #abstract interpretation #imperative #precise #slicing #source code

Precise Slicing in Imperative Programs via Term-Rewriting and Abstract Interpretation (RK), pp. 259–282.

SAS-2013-RaychevVY #automation #concurrent #synthesis

Automatic Synthesis of Deterministic Concurrency (VR, MTV, EY), pp. 283–303.

SAS-2013-NamjoshiZ #program transformation

Witnessing Program Transformations (KSN, LDZ), pp. 304–323.

SAS-2013-BlazyLMP #abstract interpretation #analysis #c #verification

Formal Verification of a C Value Analysis Based on Abstract Interpretation (SB, VL, AM, DP), pp. 324–344.

SAS-2013-FouilheMP #abstract domain #correctness #generative #performance

Efficient Generation of Correctness Certificates for the Abstract Domain of Polyhedra (AF, DM, MP), pp. 345–365.

SAS-2013-MajumdarMW #message passing #source code #verification

Static Provenance Verification for Message Passing Programs (RM, RM, ZW), pp. 366–387.

SAS-2013-0001GHAN #concept #geometry #learning #verification

Verification as Learning Geometric Concepts (RS, SG, BH, AA, AVN), pp. 388–411.

SAS-2013-BrainDGHK #float #source code #verification

Interpolation-Based Verification of Floating-Point Programs with Abstract CDCL (MB, VD, AG, LH, DK), pp. 412–432.

SAS-2013-WhiteM #algebra #analysis #memory management #optimisation #using

Concise Analysis Using Implication Algebras for Task-Local Memory Optimisation (LW, AM), pp. 433–453.

SAS-2013-DOsualdoKO #automation #concurrent #verification

Automatic Verification of Erlang-Style Concurrency (ED, JK, CHLO), pp. 454–476.

SAS-2013-LammichMSW #automaton #network

Contextual Locking for Dynamic Pushdown Networks (PL, MMO, HS, AW), pp. 477–498.