| 2013 | Effective Translation of LTL to Deterministic Rabin Automata: Beyond the (F, G)-Fragment. | Toms Babiak, Frantisek Blahoudek, Mojmr Kretnsk, Jan Strejcek |
| 2013 | A Theory for Control-Flow Graph Exploration. | Stephan Arlt, Philipp Rmmer, Martin Schf |
| 2013 | Merge and Conquer: State Merging in Parametric Timed Automata. | tienne Andr, Laurent Fribourg, Romain Soulat |
| 2013 | Precise Cost Analysis via Local Reasoning. | Diego Esteban Alonso-Blas, Puri Arenas, Samir Genaim |
| 2013 | Termination and Cost Analysis of Loops with Concurrent Interleavings. | Elvira Albert, Antonio Flores-Montoya, Samir Genaim, Enrique Martin-Martin |
| 2013 | Verification of a Dynamic Management Protocol for Cloud Applications. | Rim Abid, Gwen Salan, Francesco Bongiovanni, Noel De Palma |
| 2013 | Verification of Heap Manipulating Programs with Ordered Data by Extended Forest Automata. | Parosh Aziz Abdulla, Luks Holk, Bengt Jonsson, Ondrej Lengl, Cong Quy Trinh, Toms Vojnar |
| 2013 | Analysis of Message Passing Programs Using SMT-Solvers. | Parosh Aziz Abdulla, Mohamed Faouzi Atig, Jonathan Cederberg |
| 2012 | Verification of Computer Switching Networks: An Overview. | Shuyuan Zhang, Sharad Malik, Rick McGeer |
| 2012 | Higher-Order Approximations for Verification of Stochastic Hybrid Systems. | Sadegh Esmaeil Zadeh Soudjani, Alessandro Abate |
| 2012 | FunFrog: Bounded Model Checking with Interpolation-Based Function Summarization. | Ondrej Sery, Grigory Fedyukovich, Natasha Sharygina |
| 2012 | Parallel Assertions for Architectures with Weak Memory Models. | Daniel Schwartz-Narbonne, Georg Weissenbacher, Sharad Malik |
| 2012 | Tight Bounds for the Determinisation and Complementation of Generalised Bchi Automata. | Sven Schewe, Thomas Varghese |
| 2012 | Reachability Analysis of Polynomial Systems Using Linear Programming Relaxations. | Mohamed Amin Ben Sassi, Romain Testylier, Thao Dang, Antoine Girard |
| 2012 | An Experiment on Parallel Model Checking of a CTL Fragment. | Rodrigo T. Saad, Silvano Dal-Zilio, Bernard Berthomieu |
| 2012 | Interpolant Automata - (Invited Talk). | Andreas Podelski |
| 2012 | The Unary Fragments of Metric Interval Temporal Logic: Bounded versus Lower Bound Constraints. | Paritosh K. Pandya, Simoni S. Shah |
| 2012 | Dynamic Bayesian Networks: A Factored Model of Probabilistic Dynamics. | Sucheendra K. Palaniappan, P. S. Thiagarajan |
| 2012 | Computing Minimal Separating DFAs and Regular Invariants Using SAT and SMT Solvers. | Daniel Neider |
| 2012 | The COMICS Tool - Computing Minimal Counterexamples for DTMCs. | Nils Jansen, Erika brahm, Matthias Volk, Ralf Wimmer, Joost-Pieter Katoen, Bernd Becker |
| 2012 | Accelerating Interpolants. | Hossein Hojjat, Radu Iosif, Filip Konecn, Viktor Kuncak, Philipp Rmmer |
| 2012 | Approximating Deterministic Lattice Automata. | Shulamit Halamish, Orna Kupferman |
| 2012 | Improved Single Pass Algorithms for Resolution Proof Reduction. | Ashutosh Gupta |
| 2012 | Counterexample Guided Synthesis of Monitors for Realizability Enforcement. | Matthias Gdemann, Gwen Salan, Meriem Ouederni |
| 2012 | Model Checking Systems and Specifications with Parameterized Atomic Propositions. | Orna Grumberg, Orna Kupferman, Sarai Sheinvald |