| 2016 | Verification of Concurrent Programs on Weak Memory Models. | Oleg Travkin, Heike Wehrheim |
| 2016 | ProofScript: Proof Scripting for the Masses. | Steven Obua, Phil Scott, Jacques D. Fleuriot |
| 2016 | Hybrid Automata as Coalgebras. | Renato Neves, Lus Soares Barbosa |
| 2016 | Unification for \lambda -calculi Without Propagation Rules. | Flvio L. C. de Moura |
| 2016 | Temporal Logic Verification for Delay Differential Equations. | Peter Nazier Mosaad, Martin Frnzle, Bai Xue |
| 2016 | Towards MC/DC Coverage of Properties Specification Patterns. | Ana C. V. de Melo, Corina S. Pasareanu, Simone Hanazumi |
| 2016 | Schedulers and Finishers: On Generating the Behaviours of an Event Structure. | Annabelle McIver, Tahiry M. Rabehaja, Georg Struth |
| 2016 | Specifying Properties of Dynamic Architectures Using Configuration Traces. | Diego Marmsoler, Mario Gleirscher |
| 2016 | Dynamic Logic with Binders and Its Application to the Development of Reactive Systems. | Alexandre Madeira, Lus Soares Barbosa, Rolf Hennicker, Manuel A. Martins |
| 2016 | Termination of Single-Path Polynomial Loop Programs. | Yi Li |
| 2016 | Synthesis of Petri Nets with Whole-Place Operations and Localities. | Jetty Kleijn, Maciej Koutny, Marta Pietkiewicz-Koutny |
| 2016 | An Abstract Model for Proving Safety of Autonomous Urban Traffic. | Martin Hilscher, Maike Schwammberger |
| 2016 | Soundly Proving B Method Formul Using Typed Sequent Calculus. | Pierre Halmagrand |
| 2016 | Deriving Inverse Operators for Modal Logic. | Michell Guzmn, Salim Perchy, Camilo Rueda, Frank D. Valencia |
| 2016 | Relation-Algebraic Verification of Prim's Minimum Spanning Tree Algorithm. | Walter Guttmann |
| 2016 | On the Expressiveness of Symmetric Communication. | Thomas Given-Wilson, Axel Legay |
| 2016 | Unifying Heterogeneous State-Spaces with Lenses. | Simon Foster, Frank Zeyda, Jim Woodcock |
| 2016 | Certified Impossibility Results and Analyses in Coq of Some Randomised Distributed Algorithms. | Allyx Fontaine, Akka Zemmari |
| 2016 | Derived-Term Automata for Extended Weighted Rational Expressions. | Akim Demaille |
| 2016 | Behavioural Models for FMI Co-simulations. | Ana Cavalcanti, Jim Woodcock, Nuno Amlio |
| 2016 | ML Pattern-Matching, Recursion, and Rewriting: From FoCaLiZe to Dedukti. | Raphal Cauderlier, Catherine Dubois |
| 2016 | Ensuring Correctness of Model Transformations While Remaining Decidable. | Jon Hal Brenas, Rachid Echahed, Martin Strecker |
| 2016 | Propositional Dynamic Logic for Petri Nets with Iteration. | Mario R. F. Benevides, Bruno Lopes, Edward Hermann Haeusler |
| 2016 | Weighted Register Automata and Weighted Logic on Data Words. | Parvaneh Babari, Manfred Droste, Vitaly Perevoshchikov |
| 2016 | Parametric Deadlock-Freeness Checking Timed Automata. | tienne Andr |