Saturday April 5th |
| 9:00 - 10:00: | Peter Ölveczky (Invited Talk). |
| Real-Time Maude and its Applications |
| 10:00 - 10:30: |
Si Liu, Peter Csaba Ölveczky and José Meseguer. |
| A Frework for Mobile Ad hoc Networks in Real-Time Maude |
| 10:30 - 11:00: | coffee break |
| 11:00 - 11:30: |
Kyungmin Bae and Jose Meseguer. |
|
Infinite-State Model Checking of LTLR Formulas Using Narrowing |
| 11:30 - 12:00: |
Thomas Genet. |
| Towards Static Analysis of Functional Progrs using Tree Automata Completion |
| 12:00 - 12:30: |
Salvador Lucas and Jose Meseguer. |
| 2D Dependency Pairs for Proving Operational Termination of CTRSs |
| 12:30 - 14:00: | Lunch |
| 14:00 - 15:00: |
Cesare Tinelli (Invited Talk) |
| Extending SMT solving with constrained deduction and rewrite rules |
| 15:00 - 15:30: |
Cilo Rocha, José Meseguer and Cesar Muñoz. |
| Rewriting Modulo SMT and Open System Analysis |
| 15:30 - 16:00: |
Luis Aguirre, Narciso Marti-Oliet, Miguel Palomino and Isabel Pita. |
| Conditional Narrowing Modulo in Rewriting Logic and Maude |
| 16:00 - 16:30: | coffee break |
| 16:30 - 17:00: |
Salvador Lucas and Jose Meseguer. |
| Strong and Weak Operational Termination of Order-Sorted Rewrite Theories |
| 17:00 - 17:30: |
Dominik Klein. |
| Key-Secrecy of PACE with OTS/CafeOBJ |
| 17:30 - 18:00: |
Si Liu, Muntasir Raihan Rahman, Stephen Skeirik, Indranil Gupta and José Meseguer. |
| Formal Modeling and Analysis of Cassandra in Maude |
| 18:00 - 18:30: |
Irina Mariuca Asavoae, Mihail Asavoae and Adrian Riesco. |
| Towards a Formal Semantics-Based Technique for Interprocedural Slicing |
Sunday April 6th |
| 9:00 - 10:00: |
Alberto Lluch-Lafuente (Invited Talk) |
| Can we efficiently check concurrent progrs under relaxed memory models in Maude? |
| 10:00 - 10:30: |
Peter D. Mosses and Ferdinand Vesely. |
| FunKons: Component-Based Semantics in K |
| 10:30 - 11:00: | coffee break |
| 11:00 - 11:30: |
Andrei Arusoaie, Dorel Lucanu, Vlad Rusu, Traian Florin Serbanuta, Grigore Rosu and Andrei Stefanescu. |
| Language Definitions as Rewrite Theories |
| 11:30 - 12:00: |
Min Zhang, Yunja Choi and Kazuhiro Ogata. |
| A Formal Semantics of the OSEK/VDX Standard in K Frework and its Applications |
| 12:00 - 12:30: |
Adrian Riesco. |
| An integration of CafeOBJ into Full Maude |
| 12:30 - 14:00: | Lunch |
| 14:00 - 15:00: |
Francisco Durán (Invited Talk) |
| On the composition of graph-transformation-based DSL definitions |
| 15:00 - 15:30: |
Massimo Bartoletti, Maurizio Murgia, Alceste Scalas and Roberto Zunino. |
| Modelling and verifying contract-oriented systems in Maude |
| 15:30 - 16:00: |
Mu Sun and José Meseguer. |
| Formal Specification of Button-Related Fault-Tolerance Micropatterns |
| 16:00 - 16:30: | coffee break |
| 16:30 - 17:00: |
Nissreen El-Saber and Artur Boronat. |
| Formalization and Verification of BPMN Models using Maude |
| 17:00 - 17:30: |
Mu Sun, José Meseguer and Lui Sha. |
| A Formal Heartbeat Pattern for Open-Loop Safety of Networked Medical Devices |
| 17:30 - 18:00: |
Lenz Belzner. |
| Value Iteration for Relational MDPs in Rewriting Logic |
| 18:00 - 18:30: |
Andrew Cholewa, Fan Yang, Catherine Meadows and Jose Meseguer. |
| Maude-PSL : Reconciling Intuitive and Formal Specification in Cryptographic Protocol Analysis |
