List of Accepted Papers
Regular Papers
- Amir Ben-Amram. Size-Change Termination, Monotonicity Constraints and Ranking Functions
- David Monniaux. On using floating-point computations to help an exact linear arithmetic decision procedure
- Thomas Gawlitza and Helmut Seidl. Games through Nested Fixpoints
- Isil Dillig, Thomas Dillig and Alex Aiken. Cuts from Proofs: A Complete and Practical Technique for Solving Linear Inequalities over Integers
- Pavol Cerny and Rajeev Alur. Automated Analysis of Java Methods for Confidentiality
- Sven Verdoolaege, Gerda Janssens and Maurice Bruynooghe. Equivalence Checking of Static Affine Programs using Widening to Handle Recurrences
- Nathan Kitchen and Andreas Kuehlmann. A Markov Chain Monte Carlo Sampler for Mixed Boolean/Integer Constraints
- Thomas A. Henzinger, Maria Mateescu and Verena Wolf. Sliding Window Abstraction for Infinite Markov Chains
- Peter Lammich, Markus Müller-Olm and Alexander Wenner. Predecessor Sets of Dynamic Pushdown Networks with Tree-Regular Constraints
- Oded Fuhrmann and Shlomo Hoory. On Extending Bounded Proofs to Inductive Proofs
- Ru-Gang Xu and Rupak Majumdar. Reducing Test Inputs using Information Partitions
- Jie-Hong Jiang. Quantifier Elimination via Functional Composition
- Yeting Ge and Leonardo de Moura. Complete instantiation for quantified SMT formulas
- Aditya Kanade, Rajeev Alur, Franjo Ivancic, S. Ramesh, Sriram Sankaranarayanan and K.C. Shashidhar. Generating and Analyzing Symbolic Traces of Simulink/Stateflow Models
- Colas Le Guernic and Antoine Girard. Reachability Analysis of Hybrid Systems using Support Functions
- Roderick Bloem, Krishnendu Chatterjee, Thomas Henzinger and Barbara Jobstmann. Better Quality in Synthesis through Quantitative Objectives
- Thao Dang and David Salinas. Image computation for polynomial dynamical systems using Bernstein expansion
- Ilan Beer, Shoham Ben-David, Hana Chockler, Avigail Orni and Richard Trefler. Explaining a Counterexample Using Causality
- Ananda Basu, Saddek Bensalem, Doron Peled and Joseph Sifakis. Priority Scheduling of Distributed Systems Based on Model Checking
- Radu Iosif, Marius Bozga, Peter Habermehl, Tomas Vojnar and Filip Konecny. Automatic Verification of Integer Array Programs
- Gerard Basler, Daniel Kroening, Michele Mazzucchi and Thomas Wahl. Symbolic Counter Abstraction for Concurrent Software
- Nicolas Coste, Holger Hermanns, Etienne Lantreibecq and Wendelin Serwe. Towards Compositional Performance Prediction of Industrial GALS Designs
- Swen Jacobs. Incremental Instance Generation in Local Reasoning
- Emmanuel Filiot, Naiyong Jin and Jean-François Raskin. An Antichain Algorithm for LTL Realizability
- Vineet Kahlon, Chao Wang and Aarti Gupta. Monotonic Partial Order Reduction: An Optimal Symbolic Partial Order Reduction Technique
- Azadeh Farzan, P. Madhusudan and Francesco Sorrentino. Meta-analysis of Concurrent Program Runs with Nested Locking for Atomicity Violations
- Salvatore La Torre, P. Madhusudan and Gennaro Parlato. Reducing context-bounded concurrent reachability to sequential reachability
- Nikolaj Bjorner and Joe Hendrix. Linear Functional Fixed-Points
- Alessandro Cimatti, Marco Roveri and Stefano Tonetta. Requirements Validation for Hybrid Systems
- Shuvendu Lahiri, Shaz Qadeer, Juan Galeotti, Jan Voung and Thomas Wies. Intra-module inference
- Warren Hunt and Sol Swords. Centaur Technology Media Unit Verification
- Shuvendu Lahiri, Shaz Qadeer and Zvonimir Rakamaric. Static and Precise Detection of Concurrency Errors in Systems Code using SMT solvers
- Roope Kaivola, Rajnish Ghughal, Naren Narasimhan, Amber Telfer, Jesse Whittemore, Sudhindra Pandav, Anna Slobodova, Christopher Taylor, Vladimir Frolov, Erik Reeber and Armaghan Naik. Replacing testing with formal verification in Intel Core i7 processor execution engine validation
- Rachid Guerraoui, Thomas Henzinger and Vasu Singh. Software Transactional Memory on Relaxed Memory Models
- Juan Antonio Navarro Perez, Andrey Rybalchenko and Atul Singh. Cardinality Abstraction for Declarative Networking
- Andreas Kuehlmann, Kenneth McMillan and Shmuel Sagiv. Generalizing DPLL to Richer Logics
Tool Papers
- Michael Ryabtsev and Ofer Strichman. Translation validation: from Simulink to C
- Christoph Wintersteiger, Youssef Hamadi and Leonardo de Moura. A Concurrent Portfolio Approach to SMT Solving
- Pallavi Joshi, Mayur Naik, Chang-Seo Park and Koushik Sen. An Extensible Active Testing Framework for Concurrent Programs
- David Hopkins and Luke Ong. Homer: a Higher-order Observational equivalence Model checkER
- Susmit Jha, Rhishikesh Limaye and Sanjit A. Seshia. Beaver: Engineering an Efficient SMT Solver for Bit-Vector Arithmetic
- Saddek Bensalem, Marius Bozga, Thanh-Hung Nguyen and Joseph Sifakis. D-Finder: A Tool for Compositional Deadlock Detection and Verification
- Ashutosh Gupta and Andrey Rybalchenko. InvGen: An efficiant invariant generator
- Alessio Lomuscio, Hongyang Qu and Franco Raimondi. MCMAS: A Model Checker for the verification of Multi-Agent Systems
- Minxue Pan, Lei Bu and Xuandong Li. TASS: Timing Analyzer of Scenario-Based Specifications
- Khalil Ghorbal, Eric Goubault and Sylvie Putot. The Zonotope Abstract Domain Taylor1+
- Olivier Bouissou, Eric Goubault, Sylvie Putot, Karim Tekkal and Franck Vedrine. HybridFluctuat: a static analyzer of numerical programs within a continuous environment
- Sylvain Halle and Roger Villemaire. Browser-based Enforcement of Interface Contracts in Web Applications with BeepBeep
- Jun Sun, yang liu, jin song dong and Jun Pang. Towards Flexible Verification under Fairness
- Saurabh Srivastava, Sumit Gulwani and Jeffrey Foster. VS3: SMT Solvers for Program Verification
- Ernst Moritz Hahn, Holger Hermanns, Björn Wachter and Lijun Zhang. INFAMY: An Infinite-State Markov Model Checker
- Bertrand Jeannet and Antoine Miné. APRON: A Library of Numerical Abstract Domains for Static Analysis