| 2016 | 2LS for Program Analysis - (Competition Contribution). Peter Schrammel, Daniel Kroening |
| 2016 | Abstract Learning Frameworks for Synthesis. Christof Löding, P. Madhusudan, Daniel Neider |
| 2016 | Abstraction Refinement and Antichains for Trace Inclusion of Infinite State Systems. Radu Iosif, Adam Rogalewicz, Tomás Vojnar |
| 2016 | Acceleration in Multi-PushDown Systems. Mohamed Faouzi Atig, K. Narayan Kumar, Prakash Saivasan |
| 2016 | Advances in Symbolic Probabilistic Model Checking with PRISM. Joachim Klein, Christel Baier, Philipp Chrszon, Marcus Daum, Clemens Dubslaff, Sascha Klüppelholz, Steffen Märcker, David Müller |
| 2016 | An Automaton Learning Approach to Solving Safety Games over Infinite Graphs. Daniel Neider, Ufuk Topcu |
| 2016 | An O(m\log n) Algorithm for Stuttering Equivalence and Branching Bisimulation. Jan Friso Groote, Anton Wijs |
| 2016 | Approaching the Coverability Problem Continuously. Michael Blondin, Alain Finkel, Christoph Haase, Serge Haddad |
| 2016 | Bit-Vector Optimization. Alexander Nadel, Vadim Ryvchin |
| 2016 | CIVL: Applying a General Concurrency Verification Framework to C/Pthreads Programs (Competition Contribution). Manchun Zheng, John G. Edenhofner, Ziqing Luo, Mitchell J. Gerrard, Michael S. Rogers, Matthew B. Dwyer, Stephen F. Siegel |
| 2016 | CPA-BAM: Block-Abstraction Memoization with Value Analysis and Predicate Analysis - (Competition Contribution). Karlheinz Friedberger |
| 2016 | CPA-RefSel: CPAchecker with Refinement Selection - (Competition Contribution). Stefan Löwe |
| 2016 | Cerberus: Automated Synthesis of Enforcement Mechanisms for Security-Sensitive Business Processes. Luca Compagna, Daniel Ricardo dos Santos, Serena Elisa Ponta, Silvio Ranise |
| 2016 | Characteristic Formulae for Session Types. Julien Lange, Nobuko Yoshida |
| 2016 | Complementing Semi-deterministic Büchi Automata. Frantisek Blahoudek, Matthias Heizmann, Sven Schewe, Jan Strejcek, Ming-Hsien Tsai |
| 2016 | Coqoon - An IDE for Interactive Proof Development in Coq. Alexander John Faithfull, Jesper Bengtson, Enrico Tassi, Carst Tankink |
| 2016 | DIVINE: Explicit-State LTL Model Checker - (Competition Contribution). Vladimír Still, Petr Rockai, Jiri Barnat |
| 2016 | DLC: Compiling a Concurrent System Formal Specification to a Distributed Implementation. Hugues Evrard |
| 2016 | Deductive Proofs of Almost Sure Persistence and Recurrence Properties. Aleksandar Chakarov, Yuen-Lam Voronin, Sriram Sankaranarayanan |
| 2016 | Developing and Debugging Proof Strategies by Tinkering. Yuhui Lin, Pierre Le Bras, Gudmund Grov |
| 2016 | Diagnostic Information for Control-Flow Analysis of Workflow Graphs (a.k.a. Free-Choice Workflow Nets). Cédric Favre, Hagen Völzer, Peter Müller |
| 2016 | Efficient Syntax-Driven Lumping of Differential Equations. Luca Cardelli, Mirco Tribastone, Max Tschaikowski, Andrea Vandin |
| 2016 | FACT: A Probabilistic Model Checker for Formal Verification with Confidence Intervals. Radu Calinescu, Kenneth Johnson, Colin Paterson |
| 2016 | Faster Statistical Model Checking for Unbounded Temporal Properties. Przemyslaw Daca, Thomas A. Henzinger, Jan Kretínský, Tatjana Petrov |
| 2016 | Finding Recurrent Sets with Backward Analysis and Trace Partitioning. Alexey Bakhirkin, Nir Piterman |
| 2016 | Formalizing and Checking Thread Refinement for Data-Race-Free Execution Models. Daniel Poetzl, Daniel Kroening |
| 2016 | Hunting Memory Bugs in C Programs with Map2Check - (Competition Contribution). Herbert O. Rocha, Raimundo S. Barreto, Lucas C. Cordeiro |
| 2016 | Hybridization Based CEGAR for Hybrid Automata with Affine Dynamics. Nima Roohi, Pavithra Prabhakar, Mahesh Viswanathan |
| 2016 | Integrated Environment for Diagnosing Verification Errors. Maria Christakis, K. Rustan M. Leino, Peter Müller, Valentin Wüstholz |
| 2016 | Interpolants in Nonlinear Theories Over the Reals. Sicun Gao, Damien Zufferey |
| 2016 | JDart: A Dynamic Symbolic Analysis Framework. Kasper Søe Luckow, Marko Dimjasevic, Dimitra Giannakopoulou, Falk Howar, Malte Isberner, Temesghen Kahsai, Zvonimir Rakamaric, Vishwanath Raman |
| 2016 | LCTD: Tests-Guided Proofs for C Programs on LLVM - (Competition Contribution). Olli Saarikivi, Keijo Heljanko |
| 2016 | LPI: Software Verification with Local Policy Iteration - (Competition Contribution). Egor George Karpenkov |
| 2016 | MU-CSeq 0.4: Individual Memory Location Unwindings - (Competition Contribution). Ermenegildo Tomasco, Truc L. Nguyen, Omar Inverso, Bernd Fischer, Salvatore La Torre, Gennaro Parlato |
| 2016 | Multi-core Symbolic Bisimulation Minimisation. Tom van Dijk, Jaco van de Pol |
| 2016 | On Atomicity in Presence of Non-atomic Writes. Constantin Enea, Azadeh Farzan |
| 2016 | Online Timed Pattern Matching Using Derivatives. Dogan Ulus, Thomas Ferrère, Eugene Asarin, Oded Maler |
| 2016 | Online and Compositional Learning of Controllers with Application to Floor Heating. Kim G. Larsen, Marius Mikucionis, Marco Muñiz, Jirí Srba, Jakob Haahr Taankvist |
| 2016 | Optimized PredatorHP and the SV-COMP Heap and Memory Safety Benchmark - (Competition Contribution). Michal Kotoun, Petr Peringer, Veronika Soková, Tomás Vojnar |
| 2016 | PRISM-Games 2.0: A Tool for Multi-objective Strategy Synthesis for Stochastic Games. Marta Kwiatkowska, David Parker, Clemens Wiltsche |
| 2016 | PRISM-PSY: Precise GPU-Accelerated Parameter Synthesis for Stochastic Systems. Milan Ceska, Petr Pilar, Nicola Paoletti, Lubos Brim, Marta Z. Kwiatkowska |
| 2016 | PTIME Computation of Transitive Closures of Octagonal Relations. Filip Konecný |
| 2016 | Parameterized Compositional Model Checking. Kedar S. Namjoshi, Richard J. Trefler |
| 2016 | Parametric Runtime Verification of C Programs. Zhe Chen, Zhemin Wang, Yunlong Zhu, Hongwei Xi, Zhibin Yang |
| 2016 | Partial Order Reduction for Event-Driven Multi-threaded Programs. Pallavi Maiya, Rahul Gupta, Aditya Kanade, Rupak Majumdar |
| 2016 | PrDK: Protocol Programming with Automata. Sung-Shik T. Q. Jongmans, Farhad Arbab |
| 2016 | Probabilistic CTL Rayna Dimitrova, Luis María Ferrer Fioriti, Holger Hermanns, Rupak Majumdar |
| 2016 | RTD-Finder: A Tool for Compositional Verification of Real-Time Component-Based Systems. Souha Ben Rayana, Marius Bozga, Saddek Bensalem, Jacques Combaz |
| 2016 | Reasoning About Information Flow Security of Separation Kernels with Channel-Based Communication. Yongwang Zhao, David Sanán, Fuyuan Zhang, Yang Liu |
| 2016 | Reduction of Nondeterministic Tree Automata. Ricardo Almeida, Lukás Holík, Richard Mayr |
| 2016 | Reliable and Reproducible Competition Results with BenchExec and Witnesses (Report on SV-COMP 2016). Dirk Beyer |
| 2016 | Robots at the Edge of the Cloud. Rupak Majumdar |
| 2016 | Run Forester, Run Backwards! - (Competition Contribution). Lukás Holík, Martin Hruska, Ondrej Lengál, Adam Rogalewicz, Jirí Simácek, Tomás Vojnar |
| 2016 | Runtime Monitoring with Union-Find Structures. Normann Decker, Jannis Harder, Torben Scheffel, Malte Schmitz, Daniel Thoma |
| 2016 | Safety Verification of Continuous-Space Pure Jump Markov Processes. Sadegh Esmaeil Zadeh Soudjani, Rupak Majumdar, Alessandro Abate |
| 2016 | Safety-Constrained Reinforcement Learning for MDPs. Sebastian Junges, Nils Jansen, Christian Dehnert, Ufuk Topcu, Joost-Pieter Katoen |
| 2016 | Scalable Verification of Linear Controller Software. Junkil Park, Miroslav Pajic, Insup Lee, Oleg Sokolsky |
| 2016 | Some Complexity Results for Stateful Network Verification. Yaron Velner, Kalev Alpernas, Aurojit Panda, Alexander Rabinovich, Mooly Sagiv, Scott Shenker, Sharon Shoham |
| 2016 | Symbiotic 3: New Slicer and Error-Witness Generation - (Competition Contribution). Marek Chalupa, Martin Jonás, Jiri Slaby, Jan Strejcek, Martina Vitovská |
| 2016 | Synthesizing Piece-Wise Functions by Learning Classifiers. Daniel Neider, Shambwaditya Saha, P. Madhusudan |
| 2016 | Synthesizing Ranking Functions from Bits and Pieces. Caterina Urban, Arie Gurfinkel, Temesghen Kahsai |
| 2016 | T2: Temporal Property Verification. Marc Brockschmidt, Byron Cook, Samin Ishtiaq, Heidy Khlaaf, Nir Piterman |
| 2016 | Tactics for the Dafny Program Verifier. Gudmund Grov, Vytautas Tumas |
| 2016 | TcT: Tyrolean Complexity Tool. Martin Avanzini, Georg Moser, Michael Schaper |
| 2016 | The xSAP Safety Analysis Platform. Benjamin Bittner, Marco Bozzano, Roberto Cavada, Alessandro Cimatti, Marco Gario, Alberto Griggio, Cristian Mattarei, Andrea Micheli, Gianni Zampedri |
| 2016 | Tools and Algorithms for the Construction and Analysis of Systems - 22nd International Conference, TACAS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings Marsha Chechik, Jean-François Raskin |
| 2016 | Ultimate Automizer with Two-track Proofs - (Competition Contribution). Matthias Heizmann, Daniel Dietsch, Marius Greitschus, Jan Leike, Betim Musa, Claus Schätzle, Andreas Podelski |
| 2016 | Uncertainty Propagation Using Probabilistic Affine Forms and Concentration of Measure Inequalities. Olivier Bouissou, Eric Goubault, Sylvie Putot, Aleksandar Chakarov, Sriram Sankaranarayanan |
| 2016 | Vienna Verification Tool: IC3 for Parallel Software - (Competition Contribution). Henning Günther, Alfons Laarman, Georg Weissenbacher |
| 2016 | v2c - A Verilog to C Translator. Rajdeep Mukherjee, Michael Tautschnig, Daniel Kroening |