42 citations · 64 across the 12 of their papers we have counts for
12 papers
Formal Verification of Legal Contracts: A Translation-based Approach (Extended Version)
Reiner Hähnle, Cosimo Laneve, Adele Veschetti
Stipula is a domain-specific programming language designed to model legal contracts with enforceable properties, especially those involving asset transfers and obligations. This pa…
Decidability Problems for Micro-Stipula
Giorgio Delzanno, Cosimo Laneve, Arnaud Sangnier +1
Micro-Stipula is a stateful calculus in which clauses can be activated either through interactions with the external environment or by the evaluation of time expressions. Despite t…
Assessing Code Understanding in LLMs
Cosimo Laneve, Alvise Spanò, Dalila Ressi +2
We present an empirical evaluation of Large Language Models in code understanding associated with non-trivial, semantic-preserving program transformations such as copy propagation…
Serverless Scheduling Policies based on Cost Analysis
Giuseppe De Palma, Saverio Giallorenzo, Cosimo Laneve +3
Current proprietary and open-source serverless platforms follow opinionated, hardcoded scheduling policies to deploy the functions to be executed over the available workers. Such p…
Pacta sunt servanda: legal contracts in Stipula
Silvia Crafa, Cosimo Laneve, Giovanni Sartor
There is a growing interest in running legal contracts on digital systems, at the same time, it is important to understand to what extent software contracts may capture legal conte…
Analysis of SLA Compliance in the Cloud -- An Automated, Model-based Approach
Frank S. de Boer, Elena Giachino, Stijn de Gouw +5
Service Level Agreements (SLA) are commonly used to specify the quality attributes between cloud service providers and the customers. A violation of SLAs can result in high penalti…
Deadlock detection of Java Bytecode
Abel Garcia, Cosimo Laneve
This paper presents a technique for deadlock detection of Java programs. The technique uses typing rules for extracting infinite-state abstract models of the dependencies among the…
Time complexity of concurrent programs
Elena Giachino, Einar Broch Johnsen, Cosimo Laneve +1
We study the problem of automatically computing the time complexity of concurrent object-oriented programs. To determine this complexity we use intermediate abstract descriptions t…
A framework for deadlock detection in core ABS
Elena Giachino, Cosimo Laneve, Michael Lienhardt
We present a framework for statically detecting deadlocks in a concurrent object-oriented language with asynchronous method calls and cooperative scheduling of method activations.…
Decidability Problems for Actor Systems
Frank De Boer, Mahdi Jaghoori, Cosimo Laneve +1
We introduce a nominal actor-based language and study its expressive power. We have identified the presence/absence of fields as a crucial feature: the dynamic creation of names in…
Deadlock detection in linear recursive programs
Elena Giachino, Cosimo Laneve
Deadlock detection in recursive programs that admit dynamic resource creation is extremely complex and solutions either give imprecise answers or do not scale. We define an algorit…
Reversibility in Massive Concurrent Systems
Luca Cardelli, Cosimo Laneve
Reversing a (forward) computation history means undoing the history. In concurrent systems, undoing the history is not performed in a deterministic way but in a causally consistent…