Category Archives: News

Project “Formal Specification for Secured Software System” has been approved!

The project entitled “Formal Specification for Secured Software System” has been approved for funding. We would like to congratulate prof. Agostino Cortesi who is the Italian principal investigator and prof. Nabendu Chaki who is the Indian principal investigator. The objective of the project is to investigate whether security policies of a (possibly safety critical) system could be integrated into the formal requirement specification using formal methods, in order to detect ambiguities and inconsistencies within the specification phase in Software development life-cycle. The funding will cover the costs of researchers’ mobility between India and Italy.

Best Paper Award Valuetools 2016

The paper entitled:
“Fair workload distribution for multi-server systems with pulling strategies”
authored by Andrea Marin and Sabina Rossi has been awarded with the “best paper award” at Valuetools 2016.

Congratulations to the authors!

27/04/2016 – Tutorial day

Tutorial day

The ACADIA research centre organisms a tutorial day on hot topics in computer science.
Date: 27/04/2016
Location: Conference room, building Alpha, Scientific campus


- 11:00-13:00  Dale Miller (Ecole Polytechnique, Paris, France): ”Communicating and trusting formal proofs”

- 14:00-17:00 Young Im Cho (Gachon Univ., Seoul, Korea): ”Intelligent IoT Platforms for Smart City”

Abstract 1 (Communicating and trusting formal proofs)

In the mist of feeling insecure with our electronic communications, we can take solace in the advice that we can “trust the math” behind cryptography. Faced with concerns over the safety of fly-by-wire planes and self-driving cars, we should be able to find solace in the fact that some parts of our safety critical systems have been proved formally correct: that is, we should be able to “trust the proof”. The
way formal proofs are built today, however, makes trusting them difficult. While proof assistants are used to build formal proofs, those proofs are often locked to that assistant. Formal proofs produced by one proof assistant cannot usually be checked and trusted by another proof assistant nor by a future version of itself. Thus, one of the components of the scientific method that ensures trust-reproducibility – is missing from proof checking.
The field of proof theory, as initiated by Gentian in the 1930′s, has identified a great deal of structure in formal proofs. Given recent developments in this topic, it is now possible to apply what we know
about proofs in theory to what we would like to have for proofs in practice. To that end, I will present the Foundational Proof Certificates framework for defining the semantics of proof evidence.
Since such definitions are executable, it is possible to build proof checkers that can check a wide range of formal proofs. In this scheme, the logic engine that executes such definitions is the only thing that needs to be trusted. Since such a logic engine is based on well-known computational logic topics, anyone can write a logic engine in their choice of programming language and hardware in order for them to build a checker they can trust. I will also overview some of the consequences of defining proofs in this manner: provers can become networked far more richly than they are currently and both libraries and marketplaces of proofs are enabled in a technology independent


Abstract 2 (Intelligent IoT Platforms for Smart City)

Machine-to-Machine communications (M2M) is a phenomenon that has been proceeding quietly in the background, and it is coming into the phase where explosion of usage scenarios in businesses will happen. Sensors, actuators, RFID/NFC tags, vehicles, and intelligent machines all have
the ability to communicate. The number of M2M connections is continuously increasing, and it has been predicted to see billions of machines interconnected in a near future. M2M applications provide
advantages in various domains from building, energy, healthcare, industrial, transportation, retail, security to environmental services. This fast-growing ecosystem is leading M2M towards a promising future, however M2M market expansion opportunities are not straight forward.
M2M is suffering from the highly fragmented vertical domain specific approach, which has increased the R&D cost in each specific domain. In fact, various vertical M2M solutions have been designed independently and separately for different applications, which inevitably impacts or even impedes large-scale M2M deployment. The existence of multiple manufacturers, the lack of a common M2M Service Capability Layer and no clarity about what can be achieved have all combined to leave the field of M2M communications closer to dream than reality.
To reduce the standardization gap which exist between M2M domains, the ETSI Technical committee M2M defined an end to end M2M service platform with the intermediate service layer that are key components of the horizontal M2M solution. This standards based platform follows a RESTful approach with open interfaces to enable developing services and applications independently of the underlying network, thus easing the deployment of vertical applications for an effective interoperability, and facilitating innovation across industries.
The following topics will be covered by the tutorial:
- IoT basics
- Smart City basics
- IoT international platform focusing on OneM2M reference model
- Components and model description for IoT platform
- Examples in detail
- Case studies and demonstration etc.

6 open fully funded PhD positions in Computer Science. Deadline: April, 21st

Ca’ Foscari University, Venice, announces 6 open fully funded PhD position in Computer Science, one of which on the following specific subject:

- “Data Science”, funded by ZHAW (Zurich University of Applied Sciences) – School of Engineering (Switzerland). More information at

PhD students will have the opportunity to do their work in one of the three well-established research centers:

- KIIS (
- Dhv (Digital Humanities Venice), in collaboration with EPF de Lausanne and Telecom Italia

The PhD students will be based in the modern scientific campus of Mestre (, reachable in only 10 minutes from Venice by public transportation. The campus is highly international with both Master and PhD courses completely held in English.

For more information please contact the program coordinator Prof. Riccardo Focardi (

Application deadline is April, 21st 2016 1 PM (Italian time) and can be done on-line at:

- English:
- Italian:

See more info at this page

RuCTFE 2015 report

Yesterday the security gang of the University of Venice challenged the best hackers in the world in RuCTFE 2015, one of the most important information security competition. Despite some connectivity problems, at the end of a fierce battle we placed 12th out of 300, resulting once again the 1st Italian team.

Congratulations to out students and professors!

Cookies picture

28/01/2015 – Workshop on mobile agents and robots


January, 28th 9.30-12.30, Room 1, Bulding Z, Campus Scientifico


9.30-9.35 Workshop presentation.

9.35-10.20 Prof. Evangelos Kranakis Carleton University, Ottawa, Canada: “Evacuating Robots from an Unknown Exit in a Disk”.

Consider k mobile robots inside a circular disk of unit radius. The robots are required to evacuate the disk through an unknown exit point situated on its boundary. We assume all robots having the same (unit) maximal speed and starting at the centre of the disk. The robots may communicate in order to inform themselves about the presence (and its position) or the absence of an exit. The goal is for all the robots to evacuate through the exit in minimum time.

We consider two models of communication between the robots: in non-wireless (or localcommunication model robots exchange information only when simultaneously located at the same point, and wireless communication in which robots can communicate one another at any time. We study the following question for different values of k: what is the optimal evacuation time for k robots? We provide algorithms and show lower bounds in both communication models for k=2 and k=3 thus indicating a difference in evacuation time between the two models. We also obtain almost-tight bounds on the asymptotic relation between evacuation time and team size, for large k. We show that in the local communication model, a team of k robots can always evacuate in time 3 + (2Π)/k, whereas at least 3 + (2Π)/k – O(k^{-2}) time is sometimes required. In the wireless communication model, time 3 + Π/k + O(k^{-4/3}) always suffices to complete evacuation, and at least 3+ Π/k is sometimes required. This shows a clear separation between the local and the wireless communication models.


10.25-11.10 Prof. Danny Krizanc Wesleyan University, Middletown, CT, U.S.A.: “The Dynamic Map Visitation Problem: Foremost Coverage of Time-varying Graphs.”

We consider the Dynamic Map Visitation Problem (DMVP), in which a team of agents must visit a collection of critical locations as quickly as possible, in an environment that may change rapidly and unpredictably during the agents’ navigation. We apply recent formulations of time-varying graphs (TVGs) to DMVP, shedding new light on the computational hierarchy R ⊃ B ⊃ P of TVG classes by analyzing them in the context of graph navigation. We provide hardness results for all three classes, and for several restricted topologies, we show a separation between the classes by showing severe inapproximability in R, limited approximability in B, and tractability in P. We also give topologies in which DMVP in R is fixed parameter tractable, which may serve as a first step toward fully characterizing the features that make DMVP difficult.

11.10-11.40 coffee break (registration is required).

11.40-12.10 PhD students demos with LEGO MINDSTORMS Robots.

20/03/2014 – Talk by Paul-Andre Mellies

Title:  The free dialogue category with sums: an algebraic approach to game semantics
Time: 13:00
Location: Meeting room
Type: Research Result
Speaker: Paul-Andre Mellies (CNRS, Paris Diderot))
In this talk, I will give a direct combinatorial description of the free dialogue category with sums
as a category with dialogue games as objects and with innocent strategies as morphisms.
I will then explain how to apply this result in order to construct a functor from the category
of dialogue games and innocent strategies to the category of coherence spaces and cliques.
One obtains in this way another proof of the positionality theorem of innocent strategies,
which establishes moreover that the halting positions of an innocent strategy form a clique.

EPEW 2013 – In Venice

The European Workshop on Performance Engineering 2013 will be held in Venice on 16-17 September. The Deadline for the submission is May, 25th.
The European Performance Engineering Workshop is an annual event that aims to gather academic and industrial researchers working on all aspects of performance engineering. Original papers related to theoretical and methodological issues as well as case studies and automated tool support are solicited in the following three areas: Performance Modelling and Evaluation, System and network performance engineering, Software performance engineering.

See the call for papers
See the event website