Seminar: Reasoning Techniques for Concurrent Constraint Programming

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.