Static Analysis

Interpretation over Non-lattice Abstract Domains . . . . . . . . . . . . 6 Graeme Gange, Jorge A. Navas, Peter Schachte, Harald Søndergaard, and Peter J. Stuckey Localizing Widening and Narrowing . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 Gianluca Amato and Francesca Scozzari The Abstract Domain of Segmented Ranking Functions . . . . . . . . . . . . . . . 43 Caterina Urban Symbolic Automata for Static Specification Mining . . . . . . . . . . . . . . . . . . . 63 Hila Peleg, Sharon Shoham, Eran Yahav, and Hongseok Yang Predicate Abstraction for Relaxed Memory Models . . . . . . . . . . . . . . . . . . . 84 Andrei Marian Dan, Yuri Meshman, Martin Vechev, and Eran Yahav On Solving Universally Quantified Horn Clauses . . . . . . . . . . . . . . . . . . . . . 105 Nikolaj Bjørner, Ken McMillan, and Andrey Rybalchenko From Concrete Examples to Heap Manipulating Programs . . . . . . . . . . . . 126 Subhajit Roy Local Shape Analysis for Overlaid Data Structures . . . . . . . . . . . . . . . . . . . 150 Cezara Drăgoi, Constantin Enea, and Mihaela Sighireanu Quantified Data Automata on Skinny Trees: An Abstract Domain for Lists . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 172 Pranav Garg, P. Madhusudan, and Gennaro Parlato Static Validation of Dynamically Generated HTML Documents Based on Abstract Parsing and Semantic Processing . . . . . . . . . . . . . . . . . . 194 Hyunha Kim, Kyung-Goo Doh, and David A. Schmidt Byte-Precise Verification of Low-Level List Manipulation . . . . . . . . . . . . . . 215 Kamil Dudka, Petr Peringer, and Tomáš Vojnar