| 2018 | From Natural Projection to Partial Model Checking and Back. | Gabriele Costa, David A. Basin, Chiara Bodei, Pierpaolo Degano, Letterio Galletta |
| 2018 | Fine-Grained Complexity of Safety Verification. | Peter Chini, Roland Meyer, Prakash Saivasan |
| 2018 | ICE-Based Refinement Type Discovery for Higher-Order Functional Programs. | Adrien Champion, Tomoya Chiba, Naoki Kobayashi, Ryosuke Sato |
| 2018 | SYMBIOTIC 5: Boosted Instrumentation - (Competition Contribution). | Marek Chalupa, Martina Vitovsk, Jan Strejcek |
| 2018 | Approximate Reduction of Finite Automata for High-Speed Network Intrusion Detection. | Milan Ceska, Vojtech Havlena, Luks Holk, Ondrej Lengl, Toms Vojnar |
| 2018 | A Verified Implementation of the Bounded List Container. | Raphal Cauderlier, Mihaela Sighireanu |
| 2018 | A Statistical Model Checker for Nondeterminism and Rare Events. | Carlos E. Budde, Pedro R. D'Argenio, Arnd Hartmanns, Sean Sedwards |
| 2018 | Chain Reduction for Binary and Zero-Suppressed Decision Diagrams. | Randal E. Bryant |
| 2018 | Strategy Representation by Decision Trees in Reactive Synthesis. | Toms Brzdil, Krishnendu Chatterjee, Jan Kretnsk, Viktor Toman |
| 2018 | Bayesian Statistical Parameter Synthesis for Linear Temporal Properties of Stochastic Models. | Luca Bortolussi, Simone Silvetti |
| 2018 | Automatic Generation of Precise and Useful Commutativity Conditions. | Kshitij Bansal, Eric Koskinen, Omer Tripp |
| 2018 | Parameterized Verification of Synchronization in Constrained Reconfigurable Broadcast Networks. | A. R. Balasubramanian, Nathalie Bertrand, Nicolas Markey |
| 2018 | Optimal Dynamic Partial Order Reduction with Observers. | Stavros Aronis, Bengt Jonsson, Magnus Lng, Konstantinos Sagonas |
| 2018 | CPA-BAM-Slicing: Block-Abstraction Memoization and Slicing with Region-Based Dependency Analysis - (Competition Contribution). | Pavel S. Andrianov, Vadim S. Mutilin, Mikhail U. Mandrykin, Anton A. Vasilyev |
| 2017 | Static Detection of DoS Vulnerabilities in Programs that Use Regular Expressions. | Valentin Wstholz, Oswaldo Olivo, Marijn J. H. Heule, Isil Dillig |
| 2017 | HQSpre - An Effective Preprocessor for QBF and DQBF. | Ralf Wimmer, Sven Reimer, Paolo Marin, Bernd Becker |
| 2017 | Discriminating Traces with Time. | Saeid Tizpaz-Niari, Pavol Cern, Bor-Yuh Evan Chang, Sriram Sankaranarayanan, Ashutosh Trivedi |
| 2017 | On Optimization Modulo Theories, MaxSMT and Sorting Networks. | Roberto Sebastiani, Patrick Trentin |
| 2017 | An Abstraction Technique for Parameterized Model Checking of Leader Election Protocols: Application to FTSP. | Ocan Sankur, Jean-Pierre Talpin |
| 2017 | CSimpl: A Rely-Guarantee-Based Framework for Verifying Concurrent Programs. | David Sann, Yongwang Zhao, Zhe Hou, Fuyuan Zhang, Alwen Tiu, Yang Liu |
| 2017 | HARE: A Hybrid Abstraction Refinement Engine for Verifying Non-linear Hybrid Automata. | Nima Roohi, Pavithra Prabhakar, Mahesh Viswanathan |
| 2017 | DepthK: A k-Induction Verifier Based on Invariant Inference for C Programs - (Competition Contribution). | Williame Rocha, Herbert Rocha, Hussama Ismail, Lucas C. Cordeiro, Bernd Fischer |
| 2017 | Counterexample-Guided Model Synthesis. | Mathias Preiner, Aina Niemetz, Armin Biere |
| 2017 | Automatic Verification of Finite Precision Implementations of Linear Controllers. | Junkil Park, Miroslav Pajic, Oleg Sokolsky, Insup Lee |
| 2017 | Connecting Program Synthesis and Reachability: Automatic Program Repair Using Test-Input Generation. | ThanhVu Nguyen, Westley Weimer, Deepak Kapur, Stephanie Forrest |