| 2016 | A Decision Procedure for Separation Logic in SMT. Andrew Reynolds, Radu Iosif, Cristina Serban, Tim King |
| 2016 | A Sketching-Based Approach for Debugging Using Test Cases. Jinru Hua, Sarfraz Khurshid |
| 2016 | Approximate Policy Iteration for Markov Decision Processes via Quantitative Adaptive Aggregations. Alessandro Abate, Milan Ceska, Marta Kwiatkowska |
| 2016 | Automated Technology for Verification and Analysis - 14th International Symposium, ATVA 2016, Chiba, Japan, October 17-20, 2016, Proceedings Cyrille Artho, Axel Legay, Doron Peled |
| 2016 | Bounded Model Checking for Probabilistic Programs. Nils Jansen, Christian Dehnert, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Lukas Westhofen |
| 2016 | Certified Symbolic Execution. Rui Qiu, Corina S. Pasareanu, Sarfraz Khurshid |
| 2016 | Clause Sharing and Partitioning for Cloud-Based SMT Solving. Matteo Marescotti, Antti E. J. Hyvärinen, Natasha Sharygina |
| 2016 | Decidability Results for Multi-objective Stochastic Games. Romain Brenguier, Vojtech Forejt |
| 2016 | Efficient Verification of Program Fragments: Eager POR. Patrick Metzler, Habib Saissi, Péter Bokor, Robin Hesse, Neeraj Suri |
| 2016 | Equivalence-Based Abstraction Refinement for \mu HORS Model Checking. Xin Li, Naoki Kobayashi |
| 2016 | Greener Bits: Formal Analysis of Demand Response. Christel Baier, Sascha Klüppelholz, Hermann de Meer, Florian Niedermeier, Sascha Wunderlich |
| 2016 | Heuristics for Checking Liveness Properties with Partial Order Reductions. Alexandre Duret-Lutz, Fabrice Kordon, Denis Poitrenaud, Etienne Renault |
| 2016 | How Hard is It to Verify Flat Affine Counter Systems with the Finite Monoid Property? Radu Iosif, Arnaud Sangnier |
| 2016 | Lazy Sequentialization for the Safety Verification of Unbounded Concurrent Programs. Truc L. Nguyen, Bernd Fischer, Salvatore La Torre, Gennaro Parlato |
| 2016 | MoChiBA: Probabilistic LTL Model Checking Using Limit-Deterministic Büchi Automata. Salomon Sickert, Jan Kretínský |
| 2016 | Observational Refinement and Merge for Disjunctive MTSs. Shoham Ben-David, Marsha Chechik, Sebastián Uchitel |
| 2016 | On Finite Domains in First-Order Linear Temporal Logic. Denis Kuperberg, Julien Brunel, David Chemouil |
| 2016 | Optimizing the Expected Mean Payoff in Energy Markov Decision Processes. Tomás Brázdil, Antonín Kucera, Petr Novotný |
| 2016 | Parallel SMT-Based Parameter Synthesis with Application to Piecewise Multi-affine Systems. Nikola Benes, Lubos Brim, Martin Demko, Samuel Pastva, David Safránek |
| 2016 | Parameter Synthesis for Markov Models: Faster Than Ever. Tim Quatmann, Christian Dehnert, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen |
| 2016 | Partial-Order Reduction for GPU Model Checking. Thomas Neele, Anton Wijs, Dragan Bosnacki, Jaco van de Pol |
| 2016 | Polynomial Invariants by Linear Algebra. Steven de Oliveira, Saddek Bensalem, Virgile Prevosto |
| 2016 | STL Model Checking of Continuous and Hybrid Systems. Hendrik Roehm, Jens Oehlerking, Thomas Heinz, Matthias Althoff |
| 2016 | Skolem Functions for DQBF. Karina Wimmer, Ralf Wimmer, Christoph Scholl, Bernd Becker |
| 2016 | Solving Language Equations Using Flanked Automata. Florent Avellaneda, Silvano Dal-Zilio, Jean-Baptiste Raclet |
| 2016 | Solving Mean-Payoff Games on the GPU. Philipp J. Meyer, Michael Luttenberger |
| 2016 | Specifying and Verifying Secrecy in Workflows with Arbitrarily Many Agents. Bernd Finkbeiner, Helmut Seidl, Christian Müller |
| 2016 | Spot 2.0 - A Framework for LTL and \omega -Automata Manipulation. Alexandre Duret-Lutz, Alexandre Lewkowicz, Amaury Fauchille, Thibaud Michaud, Etienne Renault, Laurent Xu |
| 2016 | Symbolic Model Checking for Factored Probabilistic Models. David Deininger, Rayna Dimitrova, Rupak Majumdar |
| 2016 | Synchronous Products of Rewrite Systems. Óscar Martín, Alberto Verdejo, Narciso Martí-Oliet |
| 2016 | Synthesizing Skeletons for Reactive Systems. Bernd Finkbeiner, Hazem Torfah |
| 2016 | Synthesizing and Completely Testing Hardware Based on Templates Through Small Numbers of Test Patterns. Masahiro Fujita |
| 2016 | Tighter Loop Bound Analysis. Pavel Cadek, Jan Strejcek, Marek Trtík |