| 2016 | Partial-Order Reduction for GPU Model Checking. | Thomas Neele, Anton Wijs, Dragan Bosnacki, Jaco van de Pol |
| 2016 | Solving Mean-Payoff Games on the GPU. | Philipp J. Meyer, Michael Luttenberger |
| 2016 | Efficient Verification of Program Fragments: Eager POR. | Patrick Metzler, Habib Saissi, Pter Bokor, Robin Hesse, Neeraj Suri |
| 2016 | Synchronous Products of Rewrite Systems. | scar Martn, Alberto Verdejo, Narciso Mart-Oliet |
| 2016 | Clause Sharing and Partitioning for Cloud-Based SMT Solving. | Matteo Marescotti, Antti E. J. Hyvrinen, Natasha Sharygina |
| 2016 | Equivalence-Based Abstraction Refinement for \mu HORS Model Checking. | Xin Li, Naoki Kobayashi |
| 2016 | On Finite Domains in First-Order Linear Temporal Logic. | Denis Kuperberg, Julien Brunel, David Chemouil |
| 2016 | How Hard is It to Verify Flat Affine Counter Systems with the Finite Monoid Property? | Radu Iosif, Arnaud Sangnier |
| 2016 | A Sketching-Based Approach for Debugging Using Test Cases. | Jinru Hua, Sarfraz Khurshid |
| 2016 | Synthesizing and Completely Testing Hardware Based on Templates Through Small Numbers of Test Patterns. | Masahiro Fujita |
| 2016 | Synthesizing Skeletons for Reactive Systems. | Bernd Finkbeiner, Hazem Torfah |
| 2016 | Specifying and Verifying Secrecy in Workflows with Arbitrarily Many Agents. | Bernd Finkbeiner, Helmut Seidl, Christian Mller |
| 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 | Heuristics for Checking Liveness Properties with Partial Order Reductions. | Alexandre Duret-Lutz, Fabrice Kordon, Denis Poitrenaud, Etienne Renault |
| 2016 | Symbolic Model Checking for Factored Probabilistic Models. | David Deininger, Rayna Dimitrova, Rupak Majumdar |
| 2016 | Tighter Loop Bound Analysis. | Pavel Cadek, Jan Strejcek, Marek Trtk |
| 2016 | Decidability Results for Multi-objective Stochastic Games. | Romain Brenguier, Vojtech Forejt |
| 2016 | Optimizing the Expected Mean Payoff in Energy Markov Decision Processes. | Toms Brzdil, Antonn 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 Safrnek |
| 2016 | Observational Refinement and Merge for Disjunctive MTSs. | Shoham Ben-David, Marsha Chechik, Sebastin Uchitel |
| 2016 | Greener Bits: Formal Analysis of Demand Response. | Christel Baier, Sascha Klppelholz, Hermann de Meer, Florian Niedermeier, Sascha Wunderlich |
| 2016 | Solving Language Equations Using Flanked Automata. | Florent Avellaneda, Silvano Dal-Zilio, Jean-Baptiste Raclet |
| 2016 | Approximate Policy Iteration for Markov Decision Processes via Quantitative Adaptive Aggregations. | Alessandro Abate, Milan Ceska, Marta Kwiatkowska |
| 2016 | Bounded Model Checking for Probabilistic Programs. | Nils Jansen, Christian Dehnert, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Lukas Westhofen |
| 2015 | Formal Verification of Simulink/Stateflow Diagrams. | Liang Zou, Naijun Zhan, Shuling Wang, Martin Frnzle |