Nov 192013

Il Corso di Dottorato di Ricerca in Matematica e Informatica ricopre un
ampio spettro di discipline tra loro collegate sia sul piano culturale che
metodologico e applicativo. Il dottorato, attraverso la pratica della
ricerca scientifica in settori di punta della Matematica e
dell’Informatica, mira a formare persone di livello culturale adeguato a
contribuire alle attuali richieste d’innovazione e di sviluppo
dell’industria e della società dell’informazione, sia sul piano della
creatività scientifica, sia su quello della capacità progettuale.

In particolare, il corso di dottorato è finalizzato alla formazione di
specialisti dotati di avanzate conoscenze metodologiche e tecniche, oltre
ad un’adeguata preparazione linguistica, in grado di svolgere attività di
ricerca e sviluppo in larga autonomia in ambito universitario, in enti di
ricerca pubblici e privati ed in ambito industriale. L’attività del
dottorato è sostenuta da docenti e ricercatori che fanno parte di gruppi
attivamente impegnati nella ricerca a livello internazionale, garantendo
ampie possibilità di scambio e di accoglienza dei dottorandi presso
prestigiose università italiane ed estere, enti di ricerca ed aziende. Le
tematiche di indagine offerte dai due curricula disponibili si riconducono
in larga parte alle attività di ricerca dei membri del collegio dei docenti
e riguardano gli aspetti sia fondamentali che applicativi di molti settori
della Matematica e dell’Informatica.

La formazione acquisita durante il dottorato consente di svolgere attività
di ricerca e sviluppo in larga autonomia in ambito universitario, in enti
di ricerca pubblici e privati ed in ambito industriale. In particolare, i
principali sbocchi occupazionali previsti sono il proseguimento delle
attività di ricerca universitaria, il coordinamento e la direzione di
attività di ricerca & sviluppo presso industrie o enti pubblici e/o centri
di ricerca nazionali ed internazionali. Le capacità di analisi ed
elaborazione acquisite con la formazione tramite la ricerca consentono,
inoltre, di intraprendere percorsi che portino a mansioni manageriali sia
nel settore privato che in quello pubblico, oppure intraprendere attività
in proprio come collaboratore di enti, aziende e società di sviluppo


Link utili

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

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

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

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

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,

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

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.


[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

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.

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

Nascondi la toolbar