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

ETAPS 2014 Programme Sunday April 6th

Sunday, April 6th
09h00 - 10h30
CMCS
Room: F320
  • Ichiro Hasuo. Towards coalgebraic model checking (invited talk)
  • Bart Jacobs. Dijkstra monads in monadic computation
DICE
Room: F316
  • Dan Ghica. Resource control via bounded linear typing (invited talk)
FIDE
Room: F112
  • Rustan Leino and Valentin Wüstholz. The Dafny Integrated Development Environment
  • Jens Bendisposto, Sebastian Krings and Michael Leuschel. Who watches the watchers: Validating the ProB Validation Tool
FPS
Room: MJK
  • Alberto Sangiovanni-Vincentelli. Let's get physical: computer science meets systems
  • Janos Sztipanovits. OpenMETA: A Model- and Component-Based Design Tool Chain for Cyber-Physical Systems
GTVMT
Room: F018
  • Dániel Varró. Distributed Incremental Model Queries (invited talk)
MBT
Room: F109
  • Alexandre Petrenko. How Does Nondeterminism Occur in Test Models and What Do We Do with It? (invited talk)
MEALS
Room: F111
  • Goran Frehse. Scalable Verification of Cyber-Physical Systems Using Support Functions (invited talk)
  • Eric Wognsen. Battery-Aware Scheduling of Mixed Criticality Systems
REPP
Room: F114
  • Sebastian Hahn, Jan Reineke, and Reinhard Wilhelm. Compositionality in Execution Time Analysis
  • David Broman. Precision Timed Processors and WCET-Aware Code Management for Mixed-Criticality Systems
SR
Room: F309
  • Wiebe Van Der Hoek. Two Themes in Modal Logic (invited talk)
SYNCOP
Room: F116
  • Didier Lime. TBA (invited talk)
WRLA
Room: F022
  • Alberto Lluch-Lafuente. Can we efficiently check concurrent programs under relaxed memory models in Maude? (invited talk)
  • Peter D. Mosses and Ferdinand Vesely. FunKons: Component-Based Semantics in K
10h30 - 11h00 Coffee Break
11h00 - 12h30
CMCS
Room: F320
  • Baltasar Trancón Y Widemann and Michael Hauhs. Algebraic-coalgebraic recursion theory of history-dependent dynamical system models
  • Filippo Bonchi, Daniela Petrisan, Damien Pous and Jurriaan Rot. Coinduction up-to in a fibrational setting
  • Pierre Lescanne. An exercise on streams: convergence acceleration (an abstract)
  • Sergey Goncharov, Stefan Milius and Alexandra Silva. Towards a coalgebraic Chomsky hierarchy
DICE
Room: F316
  • Michael Schaper. A Complexity Preserving Transformation from Jinja Bytecode to Rewrite Systems
  • Mauro Piccolo, Claudio Sacerdoti Coen and Paolo Tranquilli. The labelling approach to precise resource analysis on the source code, revisited
FIDE
Room: F112
  • Mathieu Jaume and Théo Laurent. Teaching Formal Methods and Discrete Mathematics
  • David R. Cok and Scott Johnson. SPEEDY: An Eclipse-based IDE for invariant inference
  • Damien Doligez, Christele Faure, Thérèse Hardin and Manuel Maarek. Experience in using a typed functional language for the development of a security application
FPS
Room: MJK
  • David Harel. Steps Towards Scenario-Based Programming with a Natural Language Interface
  • Manfred Broy. A Model of Dynamic Systems
  • Martin Wirsing. Assembly Theories for Communication-Safe Component Systems
GTVMT
Room: F018
  • Christian Brenner, Joel Greenyer, Jörg Holtmann, Grischa Liebel and Matthias Tichy. ScenarioTools Real-Time Play-Out for Test Sequence Validation in an Automotive Case Study
  • Abdullah Alshanqiti and Reiko Heckel. Towards Dynamic Reverse Engineering Visual Contracts from Java
MBT
Room: F109
  • Christian Colombo, Mark Micallef and Mark Scerri. Verifying Web Applications: From Business Level Specifications to Automated Model-Based Testing
  • Arjan van der Meer, Rachid Kherrazi and Marc Hamilton. Using Formal Specifications to Support Model Based Testing ASDSpec: A Tool Combining the Best of Two Techniques
MEALS
Room: F111
  • Pedro D'Argenio. Structured Operational Semantics for Probabilistic and Nondeterministic Languages
  • Anton Wijs. GPU-Based Graph Decomposition into Strongly Connected and Maximal End Components
  • Joost-Pieter Katoen. Probably Safe or Live?
REPP
Room: F114
  • Sophie Quinton and Rolf Ernst. Typical Worst-Case Analysis: Designing Real-Time Systems for the Hard and Weakly-Hard Case
  • Joerg Mische, Stefan Metzlaff, and Theo Ungerer. Distributed Memory on Chip - Bringing Together Low Power and Real-Time
  • Thomas Carle, Manel Djemal, Dumitru Potop Butucaru, Robert de Simone, Zhen Zhang, Francois Pecheux, and Franck Wajbuerst. Reconciling performance and predictability on a many-core through off-line mapping
SR
Room: F309
  • Dimitar Guelev. Refining and Delegating Strategic Ability in ATL
  • Clàudia Nalon, Lan Zhang, Clare Dixon, and Ullrich Hustadt. A Resolution Calculus for Coalition Logics
  • Xiang Jiang and Arno Pauly. Decomposing Bimatrix Games
SYNCOP
Room: F116
  • Karin Quaas. MTL-model checking of One-Clock Parameterized Timed Automata is Undecidable
  • Vahid Hashemi, Hassan Hatefi and Jan Krcal. Probabilistic Bisimulations for PCTL Model Checking of Interval MDPs
  • Stefano Schivo, Jetse Scholma, Marcel Karperien, Janine N. Post, Jaco Van De Pol and Rom Langerak. Setting parameters for biological models with ANIMO
WRLA
Room: F022
  • Andrei Arusoaie, Dorel Lucanu, Vlad Rusu, Traian Florin Serbanuta, Grigore Rosu and Andrei Stefanescu. Language Definitions as Rewrite Theories
  • Min Zhang, Yunja Choi and Kazuhiro Ogata. A Formal Semantics of the OSEK/VDX Standard in K Framework and its Applications
  • Adrian Riesco. An integration of CafeOBJ into Full Maude
12h30 - 14h00 Lunch
14h00 - 16h00
CMCS
Room: F320
  • Robert Myers, Jiri Adámek, Stefan Milius and Henning Urbat. Canonical nondeterministic automata
  • Henning Kerstan, Barbara König and Bram Westerbaan. Lifting adjunctions to coalgebras to (re)discover automata constructions
  • Tomasz Brengos. On coalgebras with internal moves
  • Filippo Bonchi, Stefan Milius, Alexandra Silva and Fabio Zanasi. How to kill epsilons with a dagger - a coalgebraic take on systems with algebraic label structure
DICE
Room: F316
  • Damiano Mazza (to be confirmed). Non-Uniform Polytime Computation in the Infinitary Affine Lambda-Calculus (invited talk)
  • Matthieu Perrinel. Context semantics for interaction nets
FIDE
Room: F112
  • Carlo Furia and Julian Tschannen. The Gotthard approach: Designing an Integrated Verification Environment for Eiffel (invited talk)
  • François Pessaux. FoCaLiZe: Inside an F-IDE
  • David Cok. OpenJML: Software verification for Java 7 using JML, OpenJDK, and Eclipse
FPS
Room: MJK
  • Moshe Vardi. TBA
  • Kim Guldstrand Larsen. Parametric and Quantitative Extensions of Modal Transition Systems
  • Lenore Zuck. Reasoning about Network Topologies in Space
  • Doron Peled. Compositional Branching-Time Measurements
GTVMT
Room: F018
  • Xiaoliang Wang, Yngve Lamo and Fabian Büttner. Verification of Graph-based Model Transformations Using Alloy
  • Discussion
MBT
Room: F109
  • Adenilso Simao and Alexandre Petrenko. Generating Complete and Finite Test Suite for IOCO: Is It Possible?
  • Harsh Beohar and Mohammadreza Mousavi. Spinal Test Suites for Software Product Lines
  • Kalou Cabrera Castillos, Frederic Dadeau and Jacques Julliand. Coverage Criteria for Model-Based Testing using Property Patterns
MEALS
Room: F111
  • Allan van Hulst. Control Synthesis for Modal Logic
  • Emilio Tuosto. Synthesis of Graphical Multiparty Session Types
  • Hernan Melgratti. On the Behaviour of Programs Running over Weak Consistent Stores
  • Arnd Hartmanns. The MoDeST Toolset
REPP
Room: F114
  • Pascal Raymond, Claire Maiza, Catherine Parent-Vigouroux, Fabienne Carrier, and Mihail Asavoae. Timing Analysis Enhancement for Synchronous Program
  • Florian Kluge, Mike Gerdes, Florian Haas, and Theo Ungerer. A Generic Timing Model for Cyber-Physical Systems
  • Insa Fuhrmann, David Broman, Steven Smyth, and Reinhard von Hanxleden. Towards Interactive Timing Analysis for Designing Reactive Systems
  • Michael Mendler, Brino Bodin, Partha Roop, and Jai Jie Wang. The WCRT analysis of synchronous programs: Studying the tick alignment problem
SR
Room: F309
  • Benjamin Aminof and Sasha Rubin. Cycle Games
  • Dietmar Berwanger and Anup Basil Mathew. Games with Recurring Certainty
  • Wolfgang Thomas. TBA (invited talk)
SYNCOP
Room: F116
  • Alexandre Donzé. Parameter Synthesis for Signal Temporal Logic (invited talk)
  • Giuseppe Lipari, Youcheng Sun, Étienne André and Fribourg Laurent. Toward Parametric Timed Interfaces for Real-Time Components
  • Mladen Skelin, Marc Geilen, Francky Catthoor and Sverre Hendseth. Worst-case Throughput Analysis for Parametric Rate and Parametric Actor Execution Time Scenario-Aware Dataflow Graphs
WRLA
Room: F022
  • Francisco Durán. On the composition of graph-transformation-based DSL definitions (invited talk)
  • Massimo Bartoletti, Maurizio Murgia, Alceste Scalas and Roberto Zunino. Modelling and verifying contract-oriented systems in Maude
  • Mu Sun and José Meseguer. Formal Specification of Button-Related Fault-Tolerance Micropatterns
16h00 - 16h30 Coffee Break
16h30 - 18h00
CMCS
Room: F320
  • Baltasar Trancón Y Widemann. Towards systematic construction of temporal logics for dynamical systems via coalgebra
  • Corina Cirstea. A modular approach to linear-time logics
  • Benedikt Ahrens and Régis Spadotti. Coinitial semantics for redecoration of triangular matrices
  • Faris Abou-Saleh and James McKinna. A coalgebraic approach to bidirectional transformations
DICE
Room: F316
  • Business Meeting
FIDE
Room: F112
  • John Witulski and Michael Leuschel. Checking Computations of Formal Method Tools - A Secondary Toolchain for ProB
  • Discussion
FPS
Room: MJK
  • Michel Raynal. What Can be Computed in a Distributed System ?
  • Joseph Sifakis. Toward a System Design Science
MEALS
Room: F111
  • MEALS Business
REPP
Room: F114
  • Moderated Discussion
SR
Room: F309
  • Guillaume Aucher, Bastien Maubert, and Sophie Pinchinat. Automata Techniques for Epistemic Protocol Synthesis
  • Piero Bonatti, Marco Faella, and Luigi Sauro. Partial Preferences for Mediated Bargaining
WRLA
Room: F022
  • Nissreen El-Saber and Artur Boronat. Formalization and Verification of BPMN Models using Maude
  • Mu Sun, José Meseguer and Lui Sha. A Formal Heartbeat Pattern for Open-Loop Safety of Networked Medical Devices
  • Lenz Belzner. Value Iteration for Relational MDPs in Rewriting Logic
  • Andrew Cholewa, Fan Yang, Catherine Meadows and Jose Meseguer. Maude-PSL : Reconciling Intuitive and Formal Specification in Cryptographic Protocol Analysis
20h00 - 23h00
Dinner at Restaurant Chez le Per'Gras