| 2015 | Stochastic Local Search for Falsification of Hybrid Systems. | Jyotirmoy V. Deshmukh, Xiaoqing Jin, James Kapinski, Oded Maler |
| 2015 | Learning the Language of Error. | Martin Chapman, Hana Chockler, Pascal Kesseli, Daniel Kroening, Ofer Strichman, Michael Tautschnig |
| 2015 | Optimal Continuous Time Markov Decisions. | Yuliya Butkova, Hassan Hatefi, Holger Hermanns, Jan Krcl |
| 2015 | Cooperative Reactive Synthesis. | Roderick Bloem, Rdiger Ehlers, Robert Knighofer |
| 2015 | Formal Verification of Infinite-State BIP Models. | Simon Bliudze, Alessandro Cimatti, Mohamad Jaber, Sergio Mover, Marco Roveri, Wajeb Saab, Qiang Wang |
| 2015 | Hierarchical Information Patterns and Distributed Strategy Synthesis. | Dietmar Berwanger, Anup Basil Mathew, Marie van den Bogaard |
| 2015 | Model Checking Failure-Prone Open Systems Using Probabilistic Automata. | Yue Ben, A. Prasad Sistla |
| 2015 | Improving Interpolants for Linear Arithmetic. | Ernst Althaus, Bjrn Beber, Joschka Kupilas, Christoph Scholl |
| 2015 | Test Case Generation of Actor Systems. | Elvira Albert, Puri Arenas, Miguel Gmez-Zamalloa |
| 2014 | Statistically Sound Verification and Optimization for Complex Systems. | Yan Zhang, Sriram Sankaranarayanan, Fabio Somenzi |
| 2014 | Trace Abstraction Refinement for Timed Automata. | Weifeng Wang, Li Jiao |
| 2014 | Symbolic Memory with Pointers. | Marek Trtk, Jan Strejcek |
| 2014 | Nested Reachability Approximation for Discrete-Time Markov Chains with Univariate Parameters. | Guoxin Su, David S. Rosenblum |
| 2014 | Using Flow Specifications of Parameterized Cache Coherence Protocols for Verifying Deadlock Freedom. | Divjyot Sethi, Muralidhar Talupur, Sharad Malik |
| 2014 | Formal Verification of Skiplists with Arbitrary Many Levels. | Alejandro Snchez, Csar Snchez |
| 2014 | Incremental Encoding and Solving of Cardinality Constraints. | Sven Reimer, Matthias Sauer, Tobias Schubert, Bernd Becker |
| 2014 | Symmetry Reduction in Infinite Games with Finite Branching. | Nicolas Markey, Steen Vester |
| 2014 | Efficiently and Completely Verifying Synchronized Consistency Models. | Yi Lv, Luming Sun, Xiaochun Ye, Dongrui Fan, Peng Wu |
| 2014 | A Bounded Model Checker for SPARK Programs. | Cludio Belo Loureno, Maria Joo Frade, Jorge Sousa Pinto |
| 2014 | The Context-Freeness Problem Is coNP-Complete for Flat Counter Systems. | Jrme Leroux, Vincent Penelle, Grgoire Sutre |
| 2014 | PeCAn: Compositional Verification of Petri Nets Made Easy. | Dinh-Thuan Le, Huu-Vu Nguyen, Van-Tinh Nguyen, Phuong-Nam Mai, Bao-Trung Pham-Duy, Thanh-Tho Quan, tienne Andr, Laure Petrucci, Yang Liu |
| 2014 | Rabinizer 3: Safraless Translation of LTL to Small Deterministic Automata. | Zuzana Komrkov, Jan Kretnsk |
| 2014 | Liveness Analysis for Parameterised Boolean Equation Systems. | Jeroen J. A. Keiren, Wieger Wesselink, Tim A. C. Willemse |
| 2014 | Deciding Entailments in Inductive Separation Logic with Tree Automata. | Radu Iosif, Adam Rogalewicz, Toms Vojnar |
| 2014 | Extensional Crisis and Proving Identity. | Ashutosh Gupta, Laura Kovcs, Bernhard Kragl, Andrei Voronkov |