Giu 192013
 
Upcoming PhD course

Reversible Computing

July 15-19, 2013
Dipartimento di Matematica e Informatica - Via Ospedale 72, Cagliari

Ivan Lanese
Università di Bologna & INRIA FOCUS Team

Abstract. Reversible computing emerges spontaneously in many areas, such as  quantum computing or biological modeling. Also, reversible computing
allows for recoverability: when an error occurs reversibility allows one to go back to a past state and try again. Reversibility is well  understood in a sequential setting: to reverse a computation one has  to recursively undo the last step. This is not possible in a concurrent scenario, since it may not be clear which the last performed action is.

We will study reversibility for concurrent interacting systems. In particular, we consider causal consistent reversibility, where only actions which have produced no consequences can be undone. We consider uncontrolled forms of reversibility first. However, uncontrolled  reversibility is not suitable for programming safe applications, since  backward steps should be triggered only when an error state is reached. To this end we define a rollback operator allowing the  programmer to control when backward steps are performed. We also show that specifying alternatives is useful to avoid looping behaviors. We  make our intuitions formal using reversible process calculi.  Finally, we discuss applications of our theory to transactions and to debugging.


The official presentation of the course will be on July 15 (Monday) in Aula C, at 10:00. The schedule of the course will be fixed during this meeting.

Course schedule.
  • Monday 15, 10.00-12.00 Aula F [slides]
  • Tuesday 16, 10.00-12.00 Aula F [slides]
  • Wednesday 17, 10.00-12.00 Aula C [slides]
  • Thursday 18, 10.00-12.00 Aula C [slides]
  • Friday 19, 10.00-12.00 Aula C [slides]

The course has been funded by the PhD Course in Computer Science of the University of Cagliari.

 Scritto da in 19 Giugno 2013  Events  Commenti disabilitati su PhD course: Reversible Computing
Giu 192013
 
Upcoming Seminar

A Tool for Verifying Bisimilarity in CCP

June 26, 10.00 (Aula F)
Palazzo delle Scienze - Cagliari

Andres Aristizabal
Pontificia Universidad Javeriana Cali - Colombia


Abstract.
Concurrent constraint programming (ccp) is a well-established formalism for specifying processes posting and querying (partial) information in shared-memory concurrent systems. Bisimilarity is recognized as the finest behavioural equivalence in concurrency theory.

In this talk we present a tool for verifying the adequate notion of bisimilarity in ccp [FoSSaCS'11] following the theoretical algorithms presented in [SAC'12] and [ICE'12]. Also we intend to describe the structure of the tool, thus, the steps which have to be followed in order to obtain an efficient and consistent tool.

All in all, we give the main insights of a web-based tool to verify strong and weak bisimilarity in ccp, i.e., preliminary concepts, the syntax used by the tool, some flowcharts describing important implemented algorithms, the structure of the tool and the way it works while interacting with an user.  

 Scritto da in 19 Giugno 2013  Events  Commenti disabilitati su Seminar: A Tool for Verifying Bisimilarity in CCP
Apr 152013
 
Upcoming Seminar

Lending Petri Nets (and contracts)

April 16, 15.00 (Aula F)
April 17, 11.00 (Lab. 5)
Palazzo delle Scienze - Cagliari

G. Michele Pinna
Dipartimento di Matematica e Informatica - Università degli Studi di Cagliari


Abstract.
In the first part of this seminar, we give a brief introduction to Petri nets, one of the classical models of distributed systems. Petri nets have been applied in various areas, among which the description and analysis of business processes.

In the second part, w
e present Lending Petri nets, a variant of Petri nets which allows places to "lend" tokens under the guarantee that credits will be honoured - that is, lent tokens are eventually returned.

Lending Petri nets are then exploited to model contracts for business processes. In particular, we show how they can be used to formalise contracts which protect themselves while still realizing the desired choreography. We relate Lending Petri nets with Propositional Contract Logic, by showing a translation of formulae into our Petri nets which preserves the logical notion of agreement, and allows for compositional verification.

Mar 012013
 
Upcoming Seminar

A Calculus of Controlled Monotonicity

March 5, 15.00
Aula F - Palazzo delle Scienze - Cagliari

Gabriele Pulcini
Dipartimento di Informatica - Scienza e Ingegneria - Università di Bologna


Abstract.
We introduce a cut-free logical system involving serio-parallel structures relying on preorders. This system describes processes displaying a
kind of controlled monotonicity (e.g. biochemical processes) by means of a specific variant of standard Gentzen-style sequents called "embedded sequents".

Gen 292013
 
The Trustworthy Computational Societies research group (TCS) of the University of Cagliari  is looking for two post-docs to join our ongoing projects.

We seek applicants with strong interest in some of the following topics: programming language design and implementation, concurrency theory, program analysis and verification, and security foundations. The successful candidates will in work in the TCS group at the Department of Mathematics and Computer Science, University of Cagliari (Italy).


The scientific core of the group is the development of formal methods for security of concurrent and distributed systems, and the experimentation of these methods through actual implementations. The team is composed by both researchers in the fields of security and concurrency theory (process algebras, semantics and types for concurrency, linear logic) and developers. A detailed presentation of the research group TCS can be found at the website tcs.unica.it.

Positions: 2 positions, each of 2 years and renewable for another year

Gross salary: ~23K EU / year

Requisites: applicants must hold a PhD in Computer Science, Mathematics or related discipline, and must produce evidence of expertise on the above-mentioned topics. The PhD degree must have been obtained not later than 10 years before the postdoc starts.

Starting date: may 2013 (with possibility of delaying until sept. on candidate request)

Location: Cagliari is located on the southern coast of Sardinia, the second largest island in the Mediterranean see. The Cagliari airport is only 15’ from the city centre, and it is connected with >70 direct flights (many of which are low-cost Ryanair flights) to Italy and Europe. The climate is Mediterranean, with mild winters (average temp. 16.4C) and many sunny days (~300 days/year without precipitation). The main beach, Poetto, is only 10’ from the city centre. The Department of Mathematics and Computer Science is hosted in the Palazzo delle Scienze, located on top of a hill nearby the historical area of Castello.

Inquires may be made to Massimo Bartoletti,
bart@unica.it.

Set 052012
 
Upcoming Seminar

Circularity, event structures, and contracts

Sept 11, 12.00
Aula C - Palazzo delle Scienze - Cagliari

Tiziana Cimoli
Dipartimento di Matematica e Informatica - Università degli Studi di Cagliari


Abstract.
Contracts will play an increasingly important role in the specification and implementation of distributed (cloud) systems. Quoting from [1], “Absent radical improvements in security technology, we expect that users will use contracts and courts, rather than clever security engineering, to guard against provider malfeasance”. Contracts describe the promised behavior of a software agent, from the point of view of the actions it may perform, the interactions it may participate into, and its goals. A primary use of contracts if that of postponing actual interaction with other agents until an agreement on the mutually promised behaviour has been found. As in the real world, promises are not always kept by software systems, and so contracts may be helpful also after the agreement to disciplinate the interaction among agents, and to establish liability in case of violations.

At a very abstract level, a contract can be seen as sets of events, together with relations to specify the causal dependencies and the conflicts between events. This seems to suggest event structures - one of the fundamental causal models for concurrency - as a natural candidate for representing contracts. For instance, one can interpret the enabling b|-a of a stable event structure as the contract clause “I will do a after you have done b”.

However, event structures do not capture a crucial aspect of contracts, i.e. the capability of reaching an agreement in the presence of circularity in the declared promises. For instance, one would expect that the contract where A promises a in change of b, and B promises b in change of a, has an agreement. This contrasts with the fact that the event structure with enablings b|-a and a|-b has only one configuration - the empty set. This is because a|-b actually models the fact that b may only happen after a has been done, and b|-a as the fact that a may happen after b - and so neither a nor b can happen. Of course, A could simply declare to do a, without asking b to be performed first - but this would not protect A from a misbehaving B.

To reconcile causality with circularity, A could relax her contract, i.e. she could do a in change of the promise of B to do b. In this case A can safely do the first step, because either B does b, or he will be culpable of a contract violation.

In this talk we present an extension of event structures which allows for this kind of reasoning. The contract a||-b (intuitively, “I will do a if you promise to do b”) reaches an agreement with the dual contract b||-a, while protecting the participant who offers it. We characterise configurations of these event structures as provability of formulae in the contract logic PCL, an extension of intuitionistic logic with a “contractual implication” connective.

We then focus on the problem of determining, in any state of the execution of a contract, which events have to be done next. This problem is trivial in classical event structures (one has to do the events whose causes have already been done), while it becomes relevant in the presence of circularity: indeed, before performing an event a (whose causes have not already been done) one has to be sure that its causes will be done, eventually in the future. Also in this case we devise a logical characterisation via an encoding in the logic PCL.

References

[1]  Michael Armbrust, Armando Fox, Rean Griffith, Anthony D. Joseph, Randy Katz, Andy Konwinski, Gunho Lee, David Patterson, Ariel Rabkin, Ion Stoica, Matei Zaharia. A View of Cloud Computing. Communications of the ACM, Vol. 53 No. 4, Pages 50-58, 2010
Lug 092012
 
Upcoming PhD course

Bisimulation, process algebras, and coinduction

July 2012
Dipartimento di Matematica e Informatica - Via Ospedale 72, Cagliari

Emilio Tuosto
Department of Computer Science
University of Leicester (UK)

Abstract. After a brief (non technical) introduction of the abstract concept of bisimulation, the course will show how this notion can be used to define observational semantics of concurrent computations expressed as process algebras (with names). Finally, the course will highlight the coinductive nature of bisimulation and how to use coinduction to reason about the behaviour of concurrent (or diverging) applications.

The official presentation of the course will be on July 10 (Tuesday) in Aula Magna Matematica, at 18:00. The schedule of the course will be fixed during this meeting.

Course schedule.
  • Tuesday 10, 18.00-19.00 Aula Magna Matematica
  • Thursday 12, 18.00-19.00 Aula C
  • Monday 16, 15.00-17.00 Aula C
  • Tuesday 17, 15.00-17.00 Aula C

The course has been funded by the Autonomous Region of Sardinia through the Visiting Professor Program 2011-12.


Lug 092012
 
Upcoming Seminar

Formal Models in Systems Biology

July 10,
16.00-18.00 Aula Magna Matematica,
July 12, 16.00-18.00 Aula C,
Palazzo delle Scienze - Cagliari

Andrea Bracciali
SICSA Lecturer - University of Stirling (UK)

Abstract. Papers like "Protein molecules as computational elements in living cells" [Bray, Nature 1995] and "Cells as computation" [Regev and Shapiro, Nature 2002] have put forward the idea that many aspects of living systems have a computational nature. Specifically, the complex network of interaction and information exchange that occurs within the biochemistry at the inter and intra cellular level, can be assimilated to the functioning of a distributed, interactive computational system. In the words of Bray, proteins are "functionally linked ... into biochemical 'circuits' that perform a variety of simple computational tasks including amplification, integration and information storage".

Under this perspective, it has appeared natural to employ the techniques used to model and analyse interactive computational systems to the realm of living organisms. Such a research trend aims at further developments within Systems Biology, the research area that approaches the study of the living organisms at a systemic level (see "Systems Biology: a brief overview" [Kitano, Science 2002]). Computationally inspired formal models and analysis techniques are being used to carry out "in silico" experiments, which may often represent a cheaper, faster, more ethical, more easily measurable, and less constrained complement to the more traditional "in vitro/vivo" investigation.

This extended-seminar will briefly survey some of the formal techniques, particularly those originated from concurrency theory, which have been adopted, adapted and further developed for the research in Systems Biology. Starting from a historical perspective, the main ideas of the approach will be discussed and a few small examples discussed.


The course has been funded by the Autonomous Region of Sardinia through the Visiting Professor Program 2011-12.


Mag 282012
 
Upcoming Seminar

Nominal Automata for Resource Usage Control

May 29th, 12.00
Aula F, Palazzo delle Scienze - Cagliari

Pierpaolo Degano
Dipartimento di Informatica - Università di Pisa


Abstract.
Two classes of nominal automata, namely Usage Automata (UAs) and Variable Finite Automata (VFAs) are considered to express resource control policies
over program execution traces expressed by a nominal calculus (Usages).

We first discuss some closure properties of UAs, and then show UAs less
expressive than VFAs.

We finally carry over to VFAs the symbolic technique for model checking
Usages against UAs, so making it possible to verify the compliance of a program with a larger class of security properties.

Mag 162012
 
Upcoming Seminar

Differential Interaction Nets and True Concurrency

May 24th 15.00 & May 25th 14.00
Aula C, Palazzo delle Scienze - Cagliari

Damiano Mazza
Laboratoire d'Informatique de Paris Nord, CNRS (France)


Abstract.
Differential interaction nets have been introduced by Thomas Ehrhard and Laurent Regnier as an extension of linear logic proof-nets. Their main novelty is the presence of non-determinism in the cut-elimination procedure. This allowed Ehrhard and Laurent to prove that standard process calculi (e.g., pi-calculus, solos calculus) can be encoded into differential nets. However, such techniques exploit an ad-hoc treatment of reduction, which is needed to guarantee the existence of a bisimulation.

In the first part of this talk (May 24th) we will introduce interaction nets, and then differential interaction nets as a special case. In the second part (May 25th), we will analyse differential nets from a "true concurrency" point of view (non-interleaving semantics, in particular based on event structures). We will see that differential nets are inherently less expressive than standard process calculi; we will then see how to enhance their expressivity.

credits unica.it | accessibilità Università degli Studi di Cagliari
C.F.: 80019600925 - P.I.: 00443370929
note legali | privacy

Nascondi la toolbar