|
Developments in Computational Models A satellite event of ICTAC 2015 28 October 2015, Universidad Javeriana, Cali - Colombia |
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Programme Committee
|
| Mario Benevides | Brazil |
| Luís Caires | Portugal |
| Ugo Dal Lago | Italy |
| Nachum Dershowitz | Israel |
| Jérôme Feret | France |
| Marcelo Frias | Argentina |
| Russ Harmer | France |
| Ivan Lanese | Italy |
| Radu Mardare | Denmark |
| Elvira Mayordomo | Spain |
| César A. Muñoz (co-chair) | USA |
| Jorge A. Pérez (co-chair) | The Netherlands |
| Andrés Sicard-Ramírez | Colombia |
| Alexandra Silva | UK |
| Daniele Varacca | France |
|
Mauricio Ayala Rincón, Universidade de Brasilia (Brazil).
Formalising Confluence. Confluence is a critical property of computational systems which is related with determinism and non ambiguity and thus with other relevant computational attributes of functional specifications and rewriting system as termination and completion. Several criteria have been explored that guarantee confluence and their formalisations provide further interesting information. This talk will discuss topics related with the formalisation of confluence properties in the prototype verification system PVS. Gilles Dowek, INRIA (France). Discrete version of special and general relativistic trajectories (joint work with Pablo Arrighi) If we assume information has a bounded density and a bounded velocity, physical phenomena should have a description in terms of cellular automata. In this talk, I will describe several attempts to describe the trajectories of bodies in Newtonian mechanics, special relativity, and general relativity with cellular automata. Interestingly, the local nature of relativity make it more amenable to a description in terms of cellular automata than Newtonian mechanics. Pawel Sobocinski, University of Southampton (UK). Compositional model checking of concurrent systems, with Petri nets (joint work with Julian Rathke and Owen Stephens) Compositionality and process equivalence are both standard concepts of process algebra. Compositionality means that the behaviour of a compound system relies only on the behaviour of its components, i.e. there is no emergent behaviour. Process equivalence means that the explicit statespace of a system takes a back seat to its interaction patterns: the information that an environment can obtain though interaction. Petri nets are a classical, yet widely used and understood, model of concurrency. Nevertheless, they have often been described as a non-compositional model, and tools tend to deal with monolithic, globally-specified models. In this talk I will introduce Petri Nets with Boundaries (PNB), which is a compositional, graphical algebra of elementary net systems, an important class of Petri nets. I will show that compositionality and process equivalence are a powerful combination that can be harnessed to improve the performance of checking reachability and coverability in several common examples where Petri nets model realistic concurrent systems. |
Workshop web page: http://dcm-workshop.org.uk/2015
| Call for Papers (PDF) |
|
|
| Poster (PDF) |
|
|
| Topics of interest |
|
|
| Submissions |
|
|
| Important Dates |
|
|
| Programme Committee |
|
|
| Invited Speakers |
|
|
| Contact |
|
|
| Cali Travel Guide |
|
|
|