| Invited Talks |
| Embedded Systems Design - Scientific Challenges and Work Directions (Abstract) / Joseph Sifakis |
| Antichain Algorithms for Finite Automata / Laurent Doyen ; Jean-François Raskin |
| Probabilistic Systems and Optimization |
| Assume-Guarantee Verification for Probabilistic Systems / Marta Kwiatkowska ; Gethin Norman ; David Parker ; Hongyang Qu |
| Simple O(m log n) Time Markov Chain Lumping / Antti Valmari ; Giuliana Franceschinis |
| Model Checking Interactive Markov Chains / Lijun Zhang ; Martin R. Neuhäu?er |
| Approximating the Pareto Front of Multi-criteria Optimization Problems / Julien Legriel ; Colas Le Guernic ; Scott Cotton ; Oded Maler |
| Decision Procedures |
| An Alternative to SAT-Based Approaches for Bit-Vectors / Sébastien Bardin ; Philippe Herrmann ; Florian Perroud |
| Satisfiability Modulo the Theory of Costs: Foundations and Applications / Alessandro Cimatti ; Anders Franzén ; Alberto Griggio ; Roberto Sebastiani ; Cristian Stenico |
| Optimal Tableau Algorithms for Coalgebraic Logics / Rajeev Goré ; Clemens Kupke ; Dirk Pattinson |
| Blocked Clause Elimination / Matti Järvisalo ; Armin Biere ; Marijn Heule |
| Tools I |
| BOOM: Taking Boolean Program Model Checking One Step Further / Gerard Basler, Matthew Hague ; Daniel Kroening ; C.-H. Luke Ong ; Thomas Wahl ; Haoxian Zhao |
| The OpenSMT Solver / Roberto Bruttomesso ; Edgar Pek ; Natasha Sharygina ; Aliaksei Tsitovich |
| STRANGER: An Automata-Based String Analysis Tool for PHP / Fang Yu ; Muath Alkhalaf ; Tevfik Bultan |
| Automata Theory |
| When Simulation Meets Antichains: On Checking Language Inclusion of Nondeterministic Finite (Tree) Automata / Parosh Aziz Abdulla ; Yu-Fang Chen ; Lukás HolÃk ; Richard Mayr ; Tomás Vojnar |
| On Weak Modal Compatibility, Refinement, and the MIO Workbench / Sebastian S. Bauer ; Philip Mayer ; Andreas Schroeder ; Rolf Hennicker |
| Rational Synthesis / Dana Fisman ; Orna Kupferman ; Yoad Lustig |
| Efficient Büchi University Checking / Seth Fogarty ; Moshe Y. Vardi |
| Liveness |
| Automated Termination Analysis for Programs with Second-Order Recursion / Markus Aderhold |
| Ranking Function Synthesis for Bit-Vector Relations / Byron Cook ; Philipp Rümmer ; Christoph M. Wintersteiger |
| Fairness for Dynamic Control / Jochen Hoenicke ; Ernst-Rüdiger Olderog ; Andreas Podelski |
| Tools II |
| JTorX: A Tool for On-Line Model-Driven Test Derivation and Execution / Axel Belinfante |
| SLAB: A Certifying Model Checker for Infinite-State Concurrent Systems / Klaus Dräger ; Andrey Kupriyanov ; Bernd Finkbeiner ; Heike Wehrheim |
| Tracking Heaps That Hop with Heap-Hop / Jules Villard ; Étienne Lozes ; Cristiano Calcagno |
| Software Verification |
| Automatic Analysis of Scratch-Pad Memory Code for Heterogeneous Multicore Processors / Alastair F. Donaldson |
| Simplifying Linearizability Proofs with Reduction and Abstraction / Tayfun Elmas ; Shaz Qadeer ; Ali Sezgin ; Omer Subasi ; Serdar Tasiran |
| A Polymorphic Intermediate Verification Language: Design and Logical Encoding / K. Rustan M. Leino |
| Trace-Based Symbolic Analysis for Atomicity Violations / Chao Wang ; Rhishikesh Limaye ; Malay Ganai ; Aarti Gupta |
| Tools III |
| ACS: Automatic Converter Synthesis for SoC Bus Protocols / Karin Avnit ; Arcot Sowmya ; Jorgen Peddersen |
| AlPiNA: An Algebraic Petri Net Analyzer / Didier Buchs ; Steve Hostettler ; Alexis Marechal ; Matteo Risoldi |
| PASS: Abstraction Refinement for Infinite Probabilistic Models / Ernst Moritz Hahn ; Holger Hermanns ; Björn Wachter |
| Real Time and Information Flow |
| Arrival Curves for Real-Time Calculus: The Causality Problem and Its Solutions / Matthieu Moy ; Karine Altisen |
| Computing the Leakage of Information-Hiding Systems / Miguel E. Andrés ; Catuscia Palamidessi ; Peter van Rossum ; Geoffrey Smith |
| Statistical Measurement of Information Leakage / Konstantinos Chatzikokolakis ; Tom Chothia ; Apratim Guha |
| SAT Based Bounded Model Checking with Partial Order Semantics for Timed Automata / Janusz Malinowski ; Peter Niebert |
| Testing |
| Preemption Sealing for Efficient Concurrency Testing / Thomas Ball ; Sebastian Burckhardt ; Katherine E. Coons ; Madanlal Musuvathi |
| Code Mutation in Verification and Automatic Code Correction / Gal Katz ; Doron Peled |
| Efficient Detection of Errors in Java Components Using Random Environment and Restarts / Pavel Parizek ; Tomas Kalibera |
| Author Index |
| Invited Talks |
| Embedded Systems Design - Scientific Challenges and Work Directions (Abstract) / Joseph Sifakis |
| Antichain Algorithms for Finite Automata / Laurent Doyen ; Jean-François Raskin |
