| Thursday, April 10th |
| 09h00 - 10h00 |
Room: Amphitheater
ETAPS Invited Speaker
John Launchbury (Galois, US)
Practical Challenges to Secure Computation |
| 10h00 - 10h30 |
Coffee Break |
| 10h30 - 12h30 |
ESOP / Room: Mont Blanc
Program Verification II (chair: Lennart Beringer)
- Takuya Kuwahara, Tachio Terauchi, Hiroshi Unno and Naoki Kobayashi. Automatic Termination Verification for Higher-Order Functional Programs
- Caterina Urban and Antoine Miné. An Abstract Domain to Infer Ordinal-Valued Ranking Functions
- Martin Brain, Cristina David, Daniel Kroening and Peter Schrammel. Model and Proof Generation for Heap-Manipulating Programs
- João Matos, João Garcia and Paolo Romano. REAP: Reporting Errors Using Alternative Path
|
|
FOSSACS / Room: Makalu
Games and synthesis (chair: Bernd Finkbeiner)
- Martin Lang. Resource Reachability Games on Pushdown Graphs
- Krishnendu Chatterjee, Laurent Doyen, Hugo Gimbert and Youssouf Oualhadj. Perfect-Information Stochastic Mean-Payoff Parity Games
- Shaull Almagor and Orna Kupferman. Latticed-LTL Synthesis in the Presence of Noisy Inputs
- Krishnendu Chatterjee, Laurent Doyen, Sumit Nain and Moshe Y. Vardi. The Complexity of Partial-observation Stochastic Parity Games With Finite-memory Strategies
|
TACAS / Room: Amphitheater
Competition on software verification (chair: Dirk Beyer)
- Status Report on Software Verification. Dirk Beyer
- BLAST 2.7.2. Pavel Shved, Mikhail Mandrykin, and Vadim Mutilin
- CBMC. Daniel Kröning and Michael Tautschnig
- CPAchecker. Stefan Löwe, Mikhail Mandrykin, and Philipp Wendler
- CPAlien. Petr Muller and Tomas Vojnar
- CSeq-Lazy. Omar Inverso, Ermenegildo Tomasco, Bernd Fischer, Salvatore La Torre, and Gennaro Parlato
- CSeq-MU. Ermenegildo Tomasco, Omar Inverso, Bernd Fischer, Salvatore La Torre, and Gennaro Parlato
- ESBMC 1.22. Jeremy Morse, Mikhail Ramalho, Lucas Cordeiro, Denis Nicole, and Bernd Fischer
- FrankenBit. Arie Gurfinkel and Anton Belov
- LLBMC. Stephan Falke, Florian Merz, and Carsten Sinz
- Predator. Kamil Dudka, Petr Peringer, and Tomas Vojnar
- Symbiotic 2. Jiri Slaby and Jan Strejcek
- Threader. Corneliu Popeea and Andrey Rybalchenko
- UFO. Aws Albarghouthi and Arie Gurfinkel
- Ultimate Automizer. Matthias Heizmann, Jürgen Christ, Daniel Dietsch, Jochen Hoenicke, Markus Lindenmann, Betim Musa, Christian Schilling, Stefan Wissert, and Andreas Podelski
- Ultimate Kojak. Evren Ermis, Alexander Nutz, Daniel Dietsch, Jochen Hoenicke, and Andreas Podelski
|
| 12h30 - 14h00 |
Lunch |
| 14h00 - 15h00 |
Room: Amphitheater
TACAS Invited Speaker
Orna Kupferman (Hebrew University Jerusalem, Israel)
Variations on Safety |
| 15h00 - 16h00 |
ESOP / Room: Mont Blanc
Network and Process Calculi (chair: Zhong Shao)
- Tony Garnock-Jones, Sam Tobin-Hochstadt and Matthias Felleisen. The Network as a Language Construct
- Laura Bocchi, Hernan Melgratti and Emilio Tuosto. Resolving Non-determinism in Choreographies
|
FASE / Room: Kilimandjaro
Analysis and repair (chair: Marieke Huisman)
- Yu Pei, Carlo Furia, Martin Nordio and Bertrand Meyer. Automatic Program Repair by Fixing Contracts
- Shahram Esmaeilsabzali, Rupak Majumdar, Thomas Wies and Damien Zufferey. Dynamic Package Interfaces
|
FOSSACS / Room: Makalu
Compositional reasoning (chair: Krishnendu Chatterjee)
- Javier Esparza and Jörg Desel. On Negotiation as Concurrency Primitive II: Deterministic Cyclic Negotiations
- Serdar Erbatur, Deepak Kapur, Andrew M. Marshall, Catherine Meadows, Paliath Narendran and Christophe Ringeissen. On Asymmetric Unification and the Combination Problem in Disjoint Theories
|
TACAS / Room: Amphitheater
Specifying and checking linear time properties (chair: Joost-Pieter Katoen)
- Shaull Almagor, Udi Boker and Orna Kupferman. Discounting in LTL
- Ala Eddine Ben Salem, Alexandre Duret-Lutz, Fabrice Kordon and Yann Thierry-Mieg. Symbolic Model Checking of Stutter-Invariant Properties Using Generalized Testing Automata
|
| 16h00 - 16h30 |
Coffee Break |
TACAS / Room: Atrium
Tool Demonstrations |
| 16h30 - 18h00 |
ESOP / Room: Mont Blanc
Program Analysis (chair: Naoki Kobayashi)
- Ravi Mangal, Mayur Naik and Hongseok Yang. A Correspondence between Two Approaches to Interprocedural Analysis in the Presence of Join (nomination for best paper award)
- Zhoulai Fu. Targeted update -- Aggressive Memory Abstraction Beyond Common Sense and its Application on Static Numeric Analysis
- Aparna Kotha, Kapil Anand, Timothy Creech, Khaled Elwazeer, Matthew Smithson and Rajeev Barua. Affine Parallelization of Loops with Run-time Dependent Bounds from Binaries
|
FASE / Room: Kilimandjaro
Verification and validation (chair: Stefania Gnesi)
- Marcello Maria Bersani, Domenico Bianculli, Carlo Ghezzi, Srdjan Krstic and Pierluigi San Pietro. SMT-based Checking of SOLOIST over Sparse Traces (nomination for best paper award)
- Luc Moreau, Trung D. Huynh and Danius Michaelides. An Online Validator for Provenance: Algorithmic Design, Testing, and API
- Meriem Ouederni, Gwen Salaun, Javier Camara and Ernesto Pimentel. Comparator: A Tool for Quantifying Behavioural Compatibility (tool paper)
|
TUTORIAL / Room: Makalu
Bernd Finkbeiner (University of Saarland, Germany)
Synthesizing reactive components and systems
|
TACAS / Room: Amphitheater
Synthesis and learning (chair: Rance Cleaveland)
- Xiaowei Huang and Ron van der Meyden. Symbolic Synthesis for Epistemic Specifications with Observational Semantics
- Wenchao Li, Dorsa Sadigh, S. Shankar Sastry and Sanjit A. Seshia. Synthesis for Human-in-the-Loop Control Systems
- Oded Maler and Irini Eleftheria Mens. Learning Regular Languages over Large Alphabets
|
| 18h15 - 20h15 |
ETAPS Steering Committee Meeting |
| 20h30 - 23h00 |
ETAPS Steering Committee Dinner |