ETAPS 2016: 2-8 April 2016, Eindhoven, The Netherlands

TACAS 2016 programme

Most rooms are located in the Auditorium (building n.1). CZ 2 ("Collegezaal 2"), CZ 7 and CZ 8 are on the ground floor, the Blauwe Zaal is on the first level. The Zwarte Doos (building n.4) is located near the Auditorium.

Monday, April 4th
10h30 - 12h30 TACAS / Room: Blauwe Zaal
Abstraction and Verification I (Chair: Arie Gurfinkel)
  • Alexey Bakhirkin and Nir Piterman. Finding Recurrent Sets with Backwards Analysis and Trace Partitioning
  • Gudmund Grov and Vytautas Tumas. Tactics for the Dafny Program Verifier (EATCS award nominee)
  • Caterina Urban, Arie Gurfinkel and Temesghen Kahsai. Synthesizing Ranking Functions from Bits and Pieces
  • Radu Iosif, Adam Rogalewicz and Tomas Vojnar. Abstraction Refinement and Antichains for Trace Inclusion of Infinite State Systems
14h00 - 16h00 TACAS / Room: Blauwe Zaal
Probabilistic and Stochastic Systems I (Chair: Bernhard Steffen)
  • Luca Cardelli, Mirco Tribastone, Max Tschaikowski and Andrea Vandin. Efficient Syntax-driven Lumping of Differential Equations
  • Przemysław Daca, Thomas Henzinger, Jan Křetínský and Tatjana Petrov. Faster Statistical Model Checking for Unbounded Temporal Properties (EATCS award nominee)
  • Sebastian Junges, Nils Jansen, Christian Dehnert, Ufuk Topcu and Joost-Pieter Katoen. Safety-constrained Reinforcement Learning for MDPs
  • Sadegh Soudjani, Rupak Majumdar and Alessandro Abate. Safety Verification of Continuous-Space Pure Jump Markov Processes
16h30 - 18h00 TACAS / Room: Blauwe Zaal
Synthesis (Chair: Rupak Majumdar)
  • Christof Löding, Parthasarathy Madhusudan and Daniel Neider. Abstract Learning Frameworks for Synthesis
  • Parthasarathy Madhusudan, Daniel Neider and Shambwaditya Saha. Synthesizing Piece-wise Functions by Learning Classifiers (EASST award nominee)
  • Daniel Neider and Ufuk Topcu. An Automaton Learning Approach to Solving Safety Games over Infinite Graphs
Tuesday, April 5th
10h30 - 12h30 TACAS / Room: Blauwe Zaal
Probabilistic and Stochastic Systems II (Chair: Kim G. Larsen)
  • Olivier Bouissou, Eric Goubault, Sylvie Putot, Aleksandar Chakarov and Sriram Sankaranarayanan. Uncertainty Propagation using Probabilistic Affine Forms and Concentration of Measure Inequalities
  • Kim G. Larsen, Marius Mikucionis, Marco Muniz, Jiri Srba and Jakob Haahr Taankvist. Online and Compositional Learning of Controllers with Application to Floor Heating
  • Aleksandar Chakarov, Yuen-Lam Voronin and Sriram Sankaranarayanan. Deductive Proofs of Almost Sure Persistence and Recurrence Properties
  • Rayna Dimitrova, Luis María Ferrer Fioriti, Holger Hermanns and Rupak Majumdar. Probabilistic CTL* : The Deductive Way
15h30 - 18h00 TACAS / Room: Blauwe Zaal
Tools I (Chair: Dirk Beyer)
  • Zhe Chen, Zhemin Wang, Yunlong Zhu, Hongwei Xi and Zhibin Yang. Parametric Runtime Verification of C Programs
  • Alexander Faithfull, Jesper Bengtson, Tassi Enrico and Carst Tankink. Coqoon: an IDE for interactive proof development in Coq (EAPLS award nominee)
  • Tom van Dijk and Jaco van de Pol. Multi-core symbolic bisimulation minimisation
  • 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
TACAS / Zwarte Doos
Tools II (Chair: Radu Mateescu)
  • Souha Ben Rayana, Marius Bozga, Saddek Bensalem and Jacques Combaz. RTD-Finder: A Tool for Compositional Verification of Real-Time Component-based Systems
  • Martin Avanzini, Georg Moser and Michael Schaper. TcT: Tyrolean Complexity Tool
  • Maria Christakis, Rustan Leino, Peter Müller and Valentin Wüstholz. Integrated Environment for Diagnosing Verification Errors
  • Kasper Luckow, Dimitra Giannakopoulou, Falk Howar, Malte Isberner, Marko Dimjasevic, Zvonimir Rakamaric, Vishwanath Raman and Temesghen Kahsai. JDart: A Dynamic Symbolic Analysis Framework
  • [Tool demo] Marc Brockschmidt, Byron Cook, Samin Ishtiaq, Heidy Khlaaf and Nir Piterman. T2: Temporal Property Verification
Wednesday, April 6th
10h00 - 10h30 TACAS Tool Market / Room: Outside Blauwe Zaal, floor 1
10h30 - 12h30 TACAS / Room: Blauwe Zaal
Concurrency (Chair: Radu Calinescu)
  • Cédric Favre, Hagen Völzer and Peter Müller. Diagnostic Information for Control-Flow Analysis of Workflow Graphs (aka Free-ChoiceWorkflow Nets)
  • Michael Blondin, Alain Finkel, Christoph Haase and Serge Haddad. Approaching the Coverability Problem Continuously (EATCS award nominee)
  • Constantin Enea and Azadeh Farzan. On Atomicity in Presence of Non-atomic Writes
  • Daniel Poetzl and Daniel Kroening. Formalizing and Checking Thread Refinement for Data-Race-Free Execution Models
12h30 - 14h00 TACAS Tool Market / Room: Outside Blauwe Zaal, floor 1
14h00 - 16h00 TACAS / Room: Blauwe Zaal
Tool Demos (Chair: Radu Mateescu)
  • Benjamin Bittner, Marco Bozzano, Roberto Cavada, Alessandro Cimatti, Marco Gario, Alberto Griggio, Cristian Mattarei, Andrea Micheli and Gianni Zampedri. The xSAP Safety Analysis Platform
  • 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
  • Hugues Evrard. DLC: Compiling a Concurrent System Formal Specification to a Distributed Implementation
  • Marta Kwiatkowska, David Parker and Clemens Wiltsche. PRISM-games 2.0: A Tool for Multi-Objective Strategy Synthesis for Stochastic Games
  • Luca Compagna, Daniel Ricardo Dos Santos, Serena Elisa Ponta and Silvio Ranise. Cerberus: Automated Synthesis of Enforcement Mechanisms for Security-sensitive Business Processes
  • 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
16h00 - 16h30 TACAS Tool Market / Room: Outside Blauwe Zaal, floor 1
16h30 - 18h00 TACAS / Room: Blauwe Zaal
Abstraction and Verification II (Chair: Parosh Abdulla)
  • Kedar S. Namjoshi and Richard J. Trefler. Parameterized Compositional Model Checking
  • Jan Friso Groote and Anton Wijs. An O(m log n) Algorithm for Stuttering Equivalence and Branching Bisimulation
  • Sicun Gao and Damien Zufferey. Interpolants in Nonlinear Theories over the Reals
Thursday, April 7th
10h00 - 10h30 TACAS Tool Market / Room: Outside Blauwe Zaal, floor 1
10h30 - 12h30 TACAS / Room: Blauwe Zaal
Abstraction and Verification III (Chair: Marsha Chechik)
  • Filip Konecny. PTIME Computation of Transitive Closures of Octagonal Relations
  • Junkil Park, Miroslav Pajic, Insup Lee and Oleg Sokolsky. Scalable Verification of Linear Controller Software
  • 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
12h30 - 14h00 TACAS Tool Market / Room: Outside Blauwe Zaal, floor 1
14h00 - 16h00 TACAS / Room: Blauwe Zaal
Languages and Automata (Chair: Nir Piterman)
  • Ricardo Almeida, Lukas Holik and Richard Mayr. Minimization of Nondeterministic Tree Automata
  • Dogan Ulus, Thomas Ferrere, Eugene Asarin and Oded Maler. Online Timed Pattern Matching using Derivatives
  • Nima Roohi, Pavithra Prabhakar and Mahesh Viswanathan. Hybridization based CEGAR for Hybrid Automata with Affine Dynamics
  • František Blahoudek, Matthias Heizmann, Sven Schewe, Jan Strejček and Ming-Hsien Tsai. Complementing Semi-deterministic Büchi Automata
TACAS / Room: CZ 7
Competition on Software Verification - Open Jury Meeting and Technical Discussion  (Chair: Dirk Beyer) Starts at 15:00
16h30 - 18h00 TACAS / Room: CZ 2
Security (Chair: Marsha Chechik)
  • Yongwang Zhao, David Sanan, Fuyuan Zhang and Yang Liu. Reasoning About Information Flow Security of Separation Kernels with Channel-based Communication
  • Yaron Velner, Kalev Alpernas, Aurojit Panda, Alexander Rabinovich, Mooly Sagiv, Scott Shenker and Sharon Shoham. Some Complexity Results for Stateful Network Verification
TACAS / Room: CZ 8
Optimization (Chair: Jean-François Raskin)
  • Julien Lange and Nobuko Yoshida. Characteristic Formulae for Session Type
  • Alexander Nadel and Vadim Ryvchin. Bit-Vector Optimization
  • Normann Decker, Jannis Harder, Torben Scheffel, Malte Schmitz and Daniel Thoma. Runtime Monitoring with Union-Find Structures
TACAS / Room: CZ 7
Competition on Software Verification - Presentation (Chair: Dirk Beyer)