| 2013 | A Framework for Ranking Vacuity Results. Shoham Ben-David, Orna Kupferman |
| 2013 | A Theory for Control-Flow Graph Exploration. Stephan Arlt, Philipp Rümmer, Martin Schäf |
| 2013 | Acceleration for Petri Nets. Jérôme Leroux |
| 2013 | An Automata-Theoretic Approach to Reasoning about Parameterized Systems and Specifications. Orna Grumberg, Orna Kupferman, Sarai Sheinvald |
| 2013 | An Automatic Technique for Checking the Simulation of Timed Systems. Elie Fares, Jean-Paul Bodeveix, Mamoun Filali-Amine, Manuel Garnacho |
| 2013 | An Expressive Framework for Verifying Deadlock Freedom. Duy-Khanh Le, Wei-Ngan Chin, Yong Meng Teo |
| 2013 | Analysis of Message Passing Programs Using SMT-Solvers. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Jonathan Cederberg |
| 2013 | Automated Technology for Verification and Analysis - 11th International Symposium, ATVA 2013, Hanoi, Vietnam, October 15-18, 2013. Proceedings Dang Van Hung, Mizuhito Ogawa |
| 2013 | Automated Verification and Strategy Synthesis for Probabilistic Systems. Marta Z. Kwiatkowska, David Parker |
| 2013 | CCMC: A Conditional CSL Model Checker for Continuous-Time Markov Chains. Yang Gao, Ernst Moritz Hahn, Naijun Zhan, Lijun Zhang |
| 2013 | CELL: A Compositional Verification Framework. Kun Ji, Yang Liu, Shang-Wei Lin, Jun Sun, Jin Song Dong, Truong Khanh Nguyen |
| 2013 | Compact Symbolic Execution. Jiri Slaby, Jan Strejcek, Marek Trtík |
| 2013 | Control Flow Refinement and Symbolic Computation of Average Case Bound. Hong Yi Chen, Supratik Mukhopadhyay, Zheng Lu |
| 2013 | Cunf: A Tool for Unfolding and Verifying Petri Nets with Read Arcs. César Rodríguez, Stefan Schwoon |
| 2013 | Effective Translation of LTL to Deterministic Rabin Automata: Beyond the (F, G)-Fragment. Tomás Babiak, Frantisek Blahoudek, Mojmír Kretínský, Jan Strejcek |
| 2013 | Expected Termination Time in BPA Games. Dominik Wojtczak |
| 2013 | Improved Upper and Lower Bounds for Büchi Disambiguation. Hrishikesh Karmarkar, Manas Joglekar, Supratik Chakraborty |
| 2013 | Integrating Policy Iterations in Abstract Interpreters. Pierre Roux, Pierre-Loïc Garoche |
| 2013 | Interpolation Properties and SAT-Based Model Checking. Arie Gurfinkel, Simone Fulvio Rollini, Natasha Sharygina |
| 2013 | Kleene Algebras and Semimodules for Energy Problems. Zoltán Ésik, Uli Fahrenberg, Axel Legay, Karin Quaas |
| 2013 | LTL Model Checking with Neco. Lukasz Fronc, Alexandre Duret-Lutz |
| 2013 | Linear Ranking for Linear Lasso Programs. Matthias Heizmann, Jochen Hoenicke, Jan Leike, Andreas Podelski |
| 2013 | Looking at Mean-Payoff and Total-Payoff through Windows. Krishnendu Chatterjee, Laurent Doyen, Mickael Randour, Jean-François Raskin |
| 2013 | Manipulating LTL Formulas Using Spot 1.0. Alexandre Duret-Lutz |
| 2013 | Merge and Conquer: State Merging in Parametric Timed Automata. Étienne André, Laurent Fribourg, Romain Soulat |
| 2013 | MoTraS: A Tool for Modal Transition Systems and Their Extensions. Jan Kretínský, Salomon Sickert |
| 2013 | Multi-threaded Explicit State Space Exploration with State Reconstruction. Sami Evangelista, Lars Michael Kristensen, Laure Petrucci |
| 2013 | NLTOOLBOX: A Library for Reachability Computation of Nonlinear Dynamical Systems. Romain Testylier, Thao Dang |
| 2013 | Precise Cost Analysis via Local Reasoning. Diego Esteban Alonso-Blas, Puri Arenas, Samir Genaim |
| 2013 | Pushdown Systems with Stack Manipulation. Yuya Uezato, Yasuhiko Minamide |
| 2013 | PyEcdar: Towards Open Source Implementation for Timed Systems. Axel Legay, Louis-Marie Traonouez |
| 2013 | Rabinizer 2: Small Deterministic Automata for LTL ∖ GU. Jan Kretínský, Ruslán Ledesma-Garza |
| 2013 | Robustness Analysis of String Transducers. Roopsha Samanta, Jyotirmoy V. Deshmukh, Swarat Chaudhuri |
| 2013 | SAT Based Verification of Network Data Planes. Shuyuan Zhang, Sharad Malik |
| 2013 | SMT-Based Software Model Checking - Explicit Scheduler, Symbolic Threads. Alessandro Cimatti |
| 2013 | SmacC: A Retargetable Symbolic Execution Engine. Armin Biere, Jens Knoop, Laura Kovács, Jakob Zwirchmayr |
| 2013 | Solving Parity Games on the GPU. Philipp Hoffmann, Michael Luttenberger |
| 2013 | Synthesis of Bounded Integer Parameters for Parametric Timed Reachability Games. Aleksandra Jovanovic, Didier Lime, Olivier H. Roux |
| 2013 | Synthesizing Masking Fault-Tolerant Systems from Deontic Specifications. Ramiro Demasi, Pablo F. Castro, T. S. E. Maibaum, Nazareno Aguirre |
| 2013 | Termination and Cost Analysis of Loops with Concurrent Interleavings. Elvira Albert, Antonio Flores-Montoya, Samir Genaim, Enrique Martin-Martin |
| 2013 | The Quest for Precision: A Layered Approach for Data Race Detection in Static Analysis. Jakob Mund, Ralf Huuck, Ansgar Fehnker, Cyrille Artho |
| 2013 | Time-Bounded Reachability for Monotonic Hybrid Automata: Complexity and Fixed Points. Thomas Brihaye, Laurent Doyen, Gilles Geeraerts, Joël Ouaknine, Jean-François Raskin, James Worrell |
| 2013 | VCS: A Verifier for Component-Based Systems. Fei He, Liangze Yin, Bow-Yaw Wang, Lianyi Zhang, Guanyu Mu, Wenrui Meng |
| 2013 | Verification of Heap Manipulating Programs with Ordered Data by Extended Forest Automata. Parosh Aziz Abdulla, Lukás Holík, Bengt Jonsson, Ondrej Lengál, Cong Quy Trinh, Tomás Vojnar |
| 2013 | Verification of a Dynamic Management Protocol for Cloud Applications. Rim Abid, Gwen Salaün, Francesco Bongiovanni, Noel De Palma |
| 2013 | Weighted Safety. Sigal Weiner, Matan Hasson, Orna Kupferman, Eyal Pery, Zohar Shevach |