arXiv subjects

Adele Veschetti

Publications and source records attributed to Adele Veschetti.

3 recordsLinked to original sources

arXiv2025

Formal Verification of Legal Contracts: A Translation-based Approach (Extended Version)

Stipula is a domain-specific programming language designed to model legal contracts with enforceable properties, especially those involving asset transfers and obligations. This paper presents a methodology to formally verify the correctness of Stipula contracts through translation into Java code annotated with Java Modeling Language specifications. As a verification backend, the deductive verification tool KeY is used. Both, the translation and the verification of partial and total correctness for a large subset of Stipula contracts, those with disjoint cycles, is fully automatic. Our work demonstrates that a general-purpose deductive verification tool can be used successfully in a translation approach.

cs.SE↗

arXiv2025

A Probabilistic Choreography Language for PRISM

We present a choreographic framework for modelling and analysing concurrent probabilistic systems based on the PRISM model-checker. This is achieved through the development of a choreography language, which is a specification language that allows to describe the desired interactions within a concurrent system from a global viewpoint. Using choreographies gives a clear and complete view of system interactions, making it easier to understand the process flow and identify potential errors, which helps ensure correct execution and improves system reliability. We equip our language with a probabilistic semantics and then define a formal encoding into the PRISM language and discuss its correctness. Properties of programs written in our choreographic language can be model-checked by the PRISM model-checker via their translation into the PRISM language. Finally, we implement a compiler for our language and demonstrate its practical applicability via examples drawn from the use cases featured in the PRISM website.

cs.LO↗

arXiv2024

SmartML: Towards a Modeling Language for Smart Contracts

Smart contracts codify real-world transactions and automatically execute the terms of the contract when predefined conditions are met. This paper proposes SmartML, a modeling language for smart contracts that is platform independent and easy to comprehend. We detail its formal semantics and type system with a focus on its role in addressing security vulnerabilities. We show along a case study, how SmartML contributes to the prevention of reentrancy attacks, illustrating its efficacy in reinforcing the reliability and security of smart contracts within decentralized systems.

cs.SE↗