Post date: 12-Mar-2015 16:41:21
Upcoming Seminar
Reasoning Techniques for Concurrent Constraint Programming
March 17, 14.30 (Aula F)
Palazzo delle Scienze - Cagliari
Luis Fernando Pino Duque
Dipartimento di Matematica e Informatica - Università degli Studi di Cagliari
Abstract. Concurrent constraint programming (CCP) is a mature linguistic formalism from the family of process calculi and hence it treats processes much like the λ-calculus treats computable functions. CCP is based on shared-memory communication where processes interact by adding and querying partial information represented as constraints (e.g., x > 42) in a global store. In this talk I will present some novel reasoning techniques for program equivalence in CCP and their efficient verification.
More concretely, in the first part of the talk I will describe an algorithm for deciding strong bisimilarity for finite CCP processes. In the second part I will present the weak semantics for CCP and how it can be used to verify CCP program equivalence. In the third part the focus is shifted towards efficiency on the verification of weak bisimilarity.