Seminar: Coinduction Up-To for Non Deterministic Automata

Mag 162014
 
Upcoming Seminar

Coinduction Up-To for Non Deterministic Automata

May 21, 11.00 (Aula F)
Palazzo delle Scienze - Cagliari

Filippo Bonchi
Ecole Normale Supérieure de Lyon - France


Abstract. In this talk, I will introduce the Coinduction proof principle and its enhancements by mean of up-to techniques.
I will introduce bisimulation up to congruence as a technique for proving language equivalence of non-deterministic finite automata. Such technique can be effectively implemented in an algorithm that exponentially improves the state of the art.

Doing scientific research: context and guidelines

Mar 112014
 

The lectures of the course will be given at the Aula Magna of the Teatro di Anatomia, Via Ospedale 121, Cagliari. The schedule is the following

  • Monday, April 7, 9:00-13.30
  • Tuesday, April 8, 9:00-13.30
  • Thursday, April 10, 9:00-13.30
  • Friday, April 11, 9:00-13.30

Registration to this course is mandatory. To register, complete the application form.

Slides:

 Scritto da in 11 Marzo 2014  Senza categoria  Commenti disabilitati su Doing scientific research: context and guidelines

BISS 2014 – Bertinoro International Spring School

Dic 182013
 

The consortium of Italian Computer Science PhD granting institutions under the auspices of GRIN, organizes an annual school offering three graduate-level courses aimed at first-year PhD students in Computer Science. In addition to introducing students to timely research topics, the school is meant to promote acquaintance and collaboration among young European researchers. The 2014 edition of the School is the 20th in the series.

The school will offer 3 courses each consisting of 13 hours of lectures:

  • Big Data Analysis of Patterns in Media Content – Nello Cristianini, University of Bristol (UK)
  • An Introduction to Probabilistic and Quantum Programming – Ugo Dal Lago, University of Bologna (Italy)
  • Development of dynamically evolving and self-adaptive software – Carlo Ghezzi, Politecnico di Milano (Italy)

Full details about the school are available here.

Bando XXIX ciclo

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
software.

 

Link utili

PhD course: Reversible Computing

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  Senza categoria  Commenti disabilitati su PhD course: Reversible Computing

Seminar: A Tool for Verifying Bisimilarity in CCP

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  Senza categoria  Commenti disabilitati su Seminar: A Tool for Verifying Bisimilarity in CCP

Seminar: Lending Petri Nets (and contracts)

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, we 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.
 Precedenti  Successivi
contatti | accessibilità Università degli Studi di Cagliari
C.F.: 80019600925 - P.I.: 00443370929		 note legali | privacy