Programme

 

September 9 September 10 September 11
9:30-10:30 Invited Young Researcher talk:
Ugo Dal Lago
Session 6
10:30-11:00 Opening and Welcome Coffee break Coffee break (11.10)
11:00-12:40 Invited talk: Luca Aceto
Session 1
Session 4 Session 7 (11.30)
Closing
12:40-14:20 Lunch Lunch Lunch (13.15)
14:20-16:00 Session 2 ICTCS Awards and Presentation
Session 5
16:00-16:30 Coffee break Coffee break
16:30-18:30 Session 3 EATCS-IT Meeting
20:15  Social Dinner  (map)

 

Wednesday, September 9

 

10.45: Opening
11.00: Invited Speaker (Chair: Michele Loreti)
Luca Aceto (Reykjavik University)
Title: Logical vs. graphical specifications (reloaded)
Abstract
: Characteristic formulae provide a complete logical characterization of the behaviour of  processes modulo some notion of behavioural equivalence or preorder. When they exist, such formulae can be used to reduce equivalence/preorder checking to model checking. In the setting of the modal logic that characterizes modal refinement over modal transition systems, Boudol and Larsen showed more than 20 years ago that the formulae for which model checking can be reduced to preorder checking, that is, the characteristic formulae, are exactly the consistent and prime ones. This pleasing result shows the very close connection between logical and behavioural approaches to system verification in a specific setting. But, how general is it? Do similar results hold for the plethora of other process semantics and their modal characterizations studied in the literature? And, if so, are there general sufficient conditions guaranteeing that characteristic formulae are exactly the consistent and prime ones? The aim of this talk is to provide answers to those questions. In particular, I will present general, sufficient conditions guaranteeing that characteristic formulae are exactly the consistent and prime ones and I will also argue that the given conditions apply to the logics characterizing all the standard semantics in van Glabbeek’s branching-time spectrum. The talk, which is based on joint work with Dario Della Monica, Ignacio Fabregas and Anna Ingólfsdóttir,  will be self-contained and will be accessible to a wide audience.
12.00: Session 1 

On the structure of context-free languages
Flavio D’Alessandro and Benedetto Intrigila
Locally Chain-Parsable Languages
Stefano Crespi Reghizzi, Violetta Lonati, Dino Mandrioli, and Matteo Pradella
12.40: Lunch
14.20: Session 2 (Chair: Ivan Visconti)
On the betweenness centrality augmentation problem
Gianlorenzo D’Angelo, Lorenzo Severini, and Yllka Velaj
Bounds and Fixed-Parameter Algorithms for Weighted Improper Coloring
Bjarki Ágúst Guðmundsson, Tómas Ken Magnússon, and Björn Orri Sæmundsson
Into the Square – On the Complexity of Some Quadratic-Time Solvable Problems
Michele Borassi, Pierluigi Crescenzi, and Michel Habib
The decision problem for a three-sorted fragment of set theory with restricted quantification and finite enumerations
Domenico Cantone and Marianna Nicolosi-Asmundo
16.00: Coffee Break
16.30: Session 3 (Chair: Mario Coppo)
Call-by-value, Elementary Time and Intersection Types
Erika De Benedetti and Simona Ronchi Della Rocca
Semantic subtyping between coinductive mutable record types with unions and intersections.
Davide Ancona and Andrea Corradi
Compliance and subtyping in timed session types
Maurizio Murgia, Massimo Bartoletti, Tiziana Cimoli, Alessandro Sebastian Podda, and Livio Pompianu
Compliance of binary session contracts
Franco Barbanera and Ugo De’ Liguoro
Petri Nets, Counter Machines and parallel matching computations
Stefano Crespi Reghizzi and Pierluigi San Pietro
18.10: End

Thursday, September 10

 

9.30:  ICTCS Young TCS Research Award and Presentation (Chair: Simona Ronchi Della Rocca)

Ugo Dal Lago (Università di Bologna)
Title:
 Higher-Order Probabilistic Computation: Calculi, Observational Equivalence, and Implicit Complexity
Abstract: Probabilistic models are more and more pervasive in computer science, and randomized algorithms are the ones offering the best performances in many domains. Higher-order probabilistic computation – in which a probabilistic function may be passed as a parameter and returned as a result – is on the other hand a relatively underdeveloped field, which is however receiving more and more attention. We give a survey of what is known about probabilistic lambda-calculi, later focusing on some of our recent results on implicitc complexity and on inductive and coinductive techniques for program equivalence. Finally, we hint at how all this could be useful when structuring proofs of security for cryptographic primitives, but also when expressing probabilistic models in the context of machine learning.
10.30: Coffee Break
11.00: Session 4 (Chair: Ugo Dal Lago)

Partial and Complete Processes in Multiparty Sessions
Mario Coppo, Mariangiola Dezani, Ines Margaria, and Maddalena Zacchi
Exploiting linearity in sharing analysis of object-oriented programs
Gianluca Amato, Maria Chiara Meo, and Francesca Scozzari
Is hyper-extensionality preservable under deletions of graph elements?
Alberto Casagrande, Carla Piazza, and Alberto Policriti
Constraining cycle alternations in model checking for interval temporal logic
Alberto Molinari, Angelo Montanari, and Adriano Peron
12.40: Lunch
14.20: Session 5 (Chair: Andrea Pietracaprina)

Synchronous Robots vs Asynchronous Lights-Enhanced Robots on Graphs

Mattia D’Emidio, Daniele Frigioni, and Alfredo Navarra
Correcting Gene Trees by Leaf Insertions: Complexity and Approximation
Stefano Beretta and Riccardo Dondi
Unbounded recursion and non-size-increasing functions
Stefano Mazzanti
15.35: ICTCS AWARDS
15.45: ICTCS Doctoral Research Award, Presentation (Chair: Tiziana Calamoneri)
Ornela Dardha (University of Glasgow)
Title: Type Systems for Distributed Programs: Components and Sessions
Abstract: Distributed systems are everywhere around us and guaranteeing their correctness is of paramount importance. It is natural to expect that these systems are reliable and above all usable. Compositional models of software systems need to account for i) consistent dynamic reconfiguration (i.e., changing at runtime the communication patterns of a program), in order to be reliable, and ii) interaction (i.e., communication patterns among components collaborating to achieve a common task), in order to be useful. In this work, we develop techniques based on types and type systems for the verification of correctness, consistency and safety properties related to dynamic reconfiguration and communication in complex distributed systems. On the reconfiguration side, we design a type system for a component-based calculus to statically ensure consistency of dynamic reconfigurations. On the communication side, we study advanced safety properties related to communication in complex distributed systems, like deadlock freedom, livelock freedom and progress. Most importantly, we define an encoding of types and terms of the session pi calculus into the standard typed pi calculus in order to understand the expressive power of these concurrent calculi. We show how to derive in the session pi calculus basic properties, like type safety or complex ones, like progress, by exploiting this encoding.
16.10: Coffee Break
16.40: ICTCS Meeting
Chair: Tiziana Calamoneri (Sapienza Università di Roma).
20.15: Social Dinner

Friday, September 11

 

9.30: Session 6 (Chair: Betti Venneri)

A Class of Reversible Primitive Recursive Functions

Luca Paolini, Mauro Piccolo, and Luca Roversi
An imperative pure calculus
Andrea Capriccioli, Marco Servetto, and Elena Zucca
Formal Attributes Traceability in Modular Language Development Frameworks
Walter Cazzola, Paola Giannini, and Albert Shaqiri
Incremental rebinding with name polymorphism
Davide Ancona, Paola Giannini, and Elena Zucca
11.10: Coffee Break
11.30: Session 7 (Chair: Geppo Pucci)

Dynamically Operating on Threshold Graphs and Related Classes (Extended Abstract)

Tiziana Calamoneri, Angelo Monti, and Rossella Petreschi
Probabilistic Self-Stabilization
Luca Becchetti, Andrea Clementi, Emanuele Natale, and Francesco Pasquale
Towards Visualising Security with Arguments
Stefano Bistarelli, Fabio Rossi, Francesco Santini, and Carlo Taticchi
Mergeable Functional Encryption
Vincenzo Iovino and Karol Zebrowski
On the Exhaustive Generation of k-Convex Polyominoes
Paolo Massazza, Stefano Brocchi, and Giuseppa Castiglione
13.10: Closing
13.15: Lunch