News

From Global Choreographies to Verifiable Efficient Distributed Implementations

Paper From Global Choreographies to Veri able Efficient Distributed Implementations has been accepted for publication in the Journal of Logical and Algebraic Methods in Programming. The abstract of the paper is below. We define a method to automatically synthesize efficient distributed implementations from high-level global choreographies. A global choreography describes the execution and communication logic between a set […]

Read More

Runtime enforcement of timed properties using games

The paper Runtime enforcement of timed properties using games has been accepted for publication in Format Aspect of Computing. The abstract of the paper is below. This paper deals with runtime enforcement of timed properties with uncontrollable events. Runtime enforcement consists in defining and using an enforcement mechanism that modifies the executions of a running system […]

Read More

Special issue on improving software quality through formal methods in Springer Software Quality Journal

Our special issue improving software quality through formal methods in Springer Software Quality Journal is out. The special issue is devoted to the use of formal methods for improving the quality of software systems. The included articles focus on the use of runtime techniques, such as runtime verification and trace analysis. Following an open call, […]

Read More

In the program committee of IFIP-ICTSS 2020

I have been invited to the program committee of IFIP ICTSS 2020, the 32nd IFIP International Conference On Testing Software And Systems, 6-8 October, 2020, Napoli, Italy. IFIP – ICTSS  is a well established conference where researchers, practitioners and educators gather together to present and discuss the most recent innovations, experiences and open challenges in […]

Read More

A survey of challenges for runtime verification from advanced application domains (beyond software)

The paper A survey of challenges for runtime verification from advanced application domains (beyond software) has been published in Formal Methods in System Design, a Springer journal. The paper can be downloaded by following this link. This is joint work with César Sánchez, Gerardo Schneider, Wolfgang Ahrendt, Ezio Bartocci, Domenico Bianculli, Christian Colombo, Adrian Francalanza, […]

Read More

Tutorial @ RV 2019, Porto

Today, I have presented a tutorial on Runtime Enforcement of Timed Properties at RV 2019. This tutorial summarizes a line of work on the topic with colleagues and also introduces a taxonomy for runtime enforcement. The tutorial material (including slides, papers, and a virtual machine with TiPeX pre-installed) can be obtained here.

Read More

On the Monitoring of Decentralized Specifications: Semantics, Properties, Analysis, and Simulation

The paper On the Monitoring of Decentralized Specifications: Semantics, Properties, Analysis, and Simulation has been accepted for publication in TOSEM, the ACM Transactions on Software Engineering and Methodology. We define two complementary approaches to monitor decentralized systems. The first relies on those with a centralized specification, i.e, when the specification is written for the behavior of […]

Read More