ETAPS 2014: 5-13 April 2014, Grenoble, France

ETAPS 2014 Programme Thursday April 10th

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