| 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 |
|
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 |
|
REPP
Room: F114 |
|
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 |