Online trading invariably involves dealings between strangers, so it is important for one party to be able to judge objectively the trustworthiness of the other. In such a setting,...
The GSPeeDI tool implements a decision procedure for the reachability analysis of GSPDIs, planar hybrid systems whose dynamics is given by differential inclusions, and that are not...
Abstract. Many software applications are based on collaborating, yet competing, agents or virtual organisations exchanging services. Contracts, expressing obligations, permissions ...
Testing from first-order specifications has mainly been studied for flat specifications, that are specifications of a single software module. However, the specifications of large s...
Abstract. Given a nite state machine denoting the specication of a system, nding some short interaction sequences capable to reach some/all states or transitions of this machine...
“Classical” program development by refinement [12, 2, 3] is a technique for ensuring that source-level program code remains faithful to the semantic goals set out in its corre...
Abstract. Regular expressions with numerical constraints are an extension of regular expressions, allowing to bound numerically the number of times that a subexpression should be m...
Abstract. In higher-order process calculi the values exchanged in communications may contain processes. There are only two capabilities for received processes: execution and forwar...
Abstract. We design a deadlock-free semantics for a concurrent, functional and imperative programming language where locks are implicitly and univocally associated with pointers. T...