We propose an automated method for computing inductive invariants used to proving
deadlock freedom of parametric component-based systems. The method generalizes the …

Since the nineties, the Man-in-The-Middle (MITM) attack has been one of the most effective
strategies adopted for compromising information security in network environments. In this …

We introduce a term algebra as a new formal specification language for the coordinating
architectures of distributed systems consisting of a finite yet unbounded number of …

We describe the main ideas behind the framework of regular model checking in a tutorial-
like manner. First, we recall the original framework, and then describe an over …

This paper presents a Hoare-style calculus for formal reasoning about reconfiguration
programs of distributed systems. Such programs create and delete components and/or …

We develop quantifier elimination procedures for fragments of higher order logic arising from
the formalization of distributed systems (especially of fault-tolerant ones). Such procedures …

There is currently an increasing demand for concurrent programs. Checking the correctness
of concurrent programs is a complex task due to the interleavings of processes. Sometimes …