TACAS 2016 accepted papers
- Cédric Favre, Hagen Völzer and Peter Müller. Diagnostic Information for Control-Flow Analysis of Workflow Graphs (aka Free-ChoiceWorkflow Nets)
- Yongwang Zhao, David Sanan, Fuyuan Zhang and Yang Liu. Reasoning About Information Flow Security of Separation Kernels with Channel-based Communication
- Michael Blondin, Alain Finkel, Christoph Haase and Serge Haddad. Approaching the Coverability Problem Continuously
- Filip Konecny. PTIME Computation of Transitive Closures of Octagonal Relations
- Benjamin Bittner, Marco Bozzano, Roberto Cavada, Alessandro Cimatti, Marco Gario, Alberto Griggio, Cristian Mattarei, Andrea Micheli and Gianni Zampedri. The xSAP Safety Analysis Platform
- Julien Lange and Nobuko Yoshida. Characteristic Formulae for Session Types
- Alexander Nadel and Vadim Ryvchin. Bit-Vector Optimization
- Yaron Velner, Kalev Alpernas, Aurojit Panda, Alexander Rabinovich, Mooly Sagiv, Scott Shenker and Sharon Shoham. Some Complexity Results for Stateful Network Verification
- Alexey Bakhirkin and Nir Piterman. Finding Recurrent Sets with Backwards Analysis and Trace Partitioning
- Radu Calinescu, Kenneth Johnson and Colin Paterson. FACT: A Probabilistic Model Checker for Formal Verification with Confidence Intervals
- Sung-Shik T.Q. Jongmans and Farhad Arbab. PrDK: Protocol Programming with Automata
- Ricardo Almeida, Lukas Holik and Richard Mayr. Minimization of Nondeterministic Tree Automata
- Zhe Chen, Zhemin Wang, Hongwei Xi, Zhibin Yang and Yunlong Zhu. Parametric Runtime Verification of C Programs
- Hugues Evrard. DLC: Compiling a Concurrent System Formal Specification to a Distributed Implementation
- Luca Cardelli, Mirco Tribastone, Max Tschaikowski and Andrea Vandin. Efficient Syntax-driven Lumping of Differential Equations
- Gudmund Grov and Vytautas Tumas. Tactics for the Dafny Program Verifier
- Dogan Ulus, Thomas Ferrere, Eugene Asarin and Oded Maler. Online Timed Pattern Matching using Derivatives
- Przemysław Daca, Thomas Henzinger, Jan Křetínský and Tatjana Petrov. Faster Statistical Model Checking for Unbounded Temporal Properties
- Marta Kwiatkowska, David Parker and Clemens Wiltsche. PRISM-games 2.0: A Tool for Multi-Objective Strategy Synthesis for Stochastic Games
- Caterina Urban, Arie Gurfinkel and Temesghen Kahsai. Synthesizing Ranking Functions from Bits and Pieces
- Alexander Faithfull, Jesper Bengtson, Tassi Enrico and Carst Tankink. Coqoon: an IDE for interactive proof development in Coq
- Radu Iosif, Adam Rogalewicz and Tomas Vojnar. Abstraction Refinement and Antichains for Trace Inclusion of Infinite State Systems
- Tom van Dijk and Jaco van de Pol. Multi-core symbolic bisimulation minimisation
- Sebastian Junges, Nils Jansen, Christian Dehnert, Ufuk Topcu and Joost-Pieter Katoen. Safety-constrained Reinforcement Learning for MDPs
- Normann Decker, Jannis Harder, Torben Scheffel, Malte Schmitz and Daniel Thoma. Runtime Monitoring with Union-Find Structures
- Marc Brockschmidt, Byron Cook, Samin Ishtiaq, Heidy Khlaaf and Nir Piterman. T2: Temporal Property Verification
- Sadegh Soudjani, Rupak Majumdar and Alessandro Abate. Safety Verification of Continuous-Space Pure Jump Markov Processes
- Olivier Bouissou, Eric Goubault, Sylvie Putot, Aleksandar Chakarov and Sriram Sankaranarayanan. Uncertainty Propagation using Probabilistic Affine Forms and Concentration of Measure Inequalities
- Kedar S. Namjoshi and Richard J. Trefler. Parameterized Compositional Model Checking
- Kim G. Larsen, Marius Mikucionis, Marco Muniz, Jiri Srba and Jakob Haahr Taankvist. Online and Compositional Learning of Controllers with Application to Floor Heating
- Joachim Klein, Christel Baier, Philipp Chrszon, Marcus Daum, Clemens Dubslaff, Sascha Klüppelholz, Steffen Märcker and David Müller. Advances in Symbolic Probabilistic Model Checking with PRISM
- Milan Ceska, Petr Pilar, Nicola Paoletti, Lubos Brim and Marta Kwiatkowska. PRISM-PSY: Precise GPU-Accelerated Parameter Synthesis for Stochastic Systems
- Luca Compagna, Daniel Ricardo Dos Santos, Serena Elisa Ponta and Silvio Ranise. Cerberus: Automated Synthesis of Enforcement Mechanisms for Security-sensitive Business Processes
- Souha Ben Rayana, Marius Bozga, Saddek Bensalem and Jacques Combaz. RTD-Finder: A Tool for Compositional Verification of Real-Time Component-based Systems
- Constantin Enea and Azadeh Farzan. On Atomicity in Presence of Non-atomic Writes
- Yuhui Lin, Pierre Le Bras and Gudmund Grov. Developing & Debugging Proof Strategies by Tinkering
- Rajdeep Mukherjee, Michael Tautschnig and Daniel Kroening. v2c - A Verilog to C Translator Tool
- Jan Friso Groote and Anton Wijs. An O(m log n) Algorithm for Stuttering Equivalence and Branching Bisimulation
- Martin Avanzini, Georg Moser and Michael Schaper. TcT: Tyrolean Complexity Tool
- Sicun Gao and Damien Zufferey. Interpolants in Nonlinear Theories over the Reals
- Christof Löding, Parthasarathy Madhusudan and Daniel Neider. Abstract Learning Frameworks for Synthesis
- Nima Roohi, Pavithra Prabhakar and Mahesh Viswanathan. Hybridization based CEGAR for Hybrid Automata with Affine Dynamics
- P. Madhusudan, Daniel Neider and Shambwaditya Saha. Synthesizing Piece-wise Functions by Learning Classifiers
- Aleksandar Chakarov, Yuen-Lam Voronin and Sriram Sankaranarayanan. Deductive Proofs of Almost Sure Persistence and Recurrence Properties
- Maria Christakis, Rustan Leino, Peter Müller and Valentin Wüstholz. Integrated Environment for Diagnosing Verification Errors
- František Blahoudek, Matthias Heizmann, Sven Schewe, Jan Strejček and Ming-Hsien Tsai. Complementing Semi-deterministic Büchi Automata
- Junkil Park, Miroslav Pajic, Insup Lee and Oleg Sokolsky. Scalable Verification of Linear Controller Software
- Daniel Poetzl and Daniel Kroening. Formalizing and Checking Thread Refinement for Data-Race-Free Execution Models
- Kasper Luckow, Dimitra Giannakopoulou, Falk Howar, Malte Isberner, Marko Dimjasevic, Zvonimir Rakamaric, Vishwanath Raman and Temesghen Kahsai. JDart: A Dynamic Symbolic Analysis Framework
- Pallavi Maiya, Rahul Gupta, Aditya Kanade and Rupak Majumdar. Partial Order Reduction for Event-driven Multi-threaded Programs
- Mohamed Faouzi Atig, K. Narayan Kumar and Prakash Saivasan. Acceleration in Multi-Pushdown systems
- Rayna Dimitrova, Luis María Ferrer Fioriti, Holger Hermanns and Rupak Majumdar. Probabilistic CTL* : The Deductive Way
- Daniel Neider and Ufuk Topcu. An Automaton Learning Approach to Solving Safety Games over Infinite Graphs