LANEVE , Cosimo

Deadlock analysis of multi-threaded programs with reentrant locks is complex because these programs may have infinitely many states. We define a simple calculus featuring recursion, threads and synchronizations that guarantee exclusive access to objects. We detect deadlocks by associating an abstract model to programs-the extended lam model-and...

Deadlock analysis of multi-threaded programs with reentrant locks is complex because these programs may have infinitely many states. We define a simple calculus featuring recursion, threads and synchroniza-tions that guarantee exclusive access to objects. We detect deadlocks by associating an abstract model to programs-the extended lam...

This paper is an introduction to the framework for the deadlock analysis of object-oriented languages we have defined in [6, 5]. We present a basic Java-like language and the deadlock analysis model in an accessible way. We also overview the algorithm for deciding deadlock-freeness by discussing a number of paradigmatic examples. We finally...

Lamping's optimal graph reduction technique for the l-calculus is generalized to a new class of higher order rewriting systems, called interaction systems. Interaction systems provide a nice integration of the functional paradigm with a rich class of data structures (all inductive types) and some basic control flow constructs such as...

Deadlock detection in concurrent programs that create networks with arbitrary numbers of nodes is extremely complex and solutions either give imprecise answers or do not scale. To enable the analysis of such programs, (1) we define an algorithm for detecting deadlocks of a basic model featuring recursion and fresh name generation: the lam...

In cloud computing, resources as files, databases, applica-tions, and virtual machines may either scale or move from one machine to another in response to load increases and decreases (resource deploy-ment). We study a type-based technique for analysing the deployments of resources in cloud computing. In particular, we design a type system for...

We are studying semantics of a small object-based language, with the following main characteristics: parallelism, dynamicity, high order parameters, notion of a global instant, and reactivity. We give formal semantics using two related formalisms , namely $\pi$-calculus and the so-called «Chemical Abstract Machine» (\Name{CHAM}). These...

In this paper we study the semantics of the $\lambda$-calculus induced by Milner's encoding into the $\pi$-calculus. We show that the resulting may testing preorder on $\lambda$-terms coincides with the inclusion of Lévy-Longo trees. To establish this result, we use a refinement of the $\lambda$-calculus where the argument of a function may be...

JaDA is a static deadlock analyzer that targets Java byte-code. The core of JaDA is a behavioral type system especially designed to record dependencies between concurrent code. These behavioural types are thereafter analyzed by means of a fixpoint algorithm that reports potential deadlocks in the original Java code. We give a practical...

Deadlock detection in recursive programs that admit dy-namic resource creation is extremely complex and solutions either give imprecise answers or do not scale. We define an algorithm for detecting deadlocks of linear recursive pro-grams of a basic model. The theory that underpins the algorithm is a generalization of the theory of permutations...

We study a natural notion of compliance between clients and services in terms of their bpel (abstract) descriptions. The induced preorder shows interesting connections with the must preorder and has normal form representatives that are parallel-free finite-state activities, called contracts. The preorder also admits the notion of least service...

Deadlock detection in concurrent programs that create networks with arbitrary numbers of nodes is extremely complex and solutions either give im-precise answers or do not scale. To enable the analysis of such programs, (1) we define an algorithm for detecting deadlocks of a basic model featuring recursion and fresh name generation: the lam...

We present a framework for statically detecting deadlocks in a concurrent object-oriented language with asynchronous method calls and cooperative scheduling of method activations. Since this language features recursion and dynamic resource creation, deadlock detection is extremely complex and state-of-the-art solutions either give imprecise...

Smart contracts are pieces of software stored on the blockchain that control the transfer of assets between parties under certain conditions. In this paper we analyze the bahaviour of smart contracts and the interaction with external actors in order to maximize objective functions. We define a core language of programs with a minimal set of...

We propose a static analysis technique that computes upper bounds of virtual machine usages in a concurrent language with explicit acquire and release operations of virtual machines. In our language it is possible to delegate other (ad-hoc or third party) concurrent code to release virtual machines (by passing them as arguments of...

We propose a static analysis technique that computes upper bounds of virtual machine usages in a concurrent language with explicit acquire and release operations of virtual machines. In our language it is possible to delegate other (ad-hoc or third party) concurrent code to release virtual machines (by passing them as arguments of invocations)....