1,721,122 research outputs found
Legal contracts amending with [inline-graphic not available: see fulltext]
Full text linkPublished: 19 June 2023Legal contracts can be amended during their lifetime through the agreement of the parties or in accordance with the doctrines of force majeure and hardship. When legal contracts are defined using a programming language, amendments are made through runtime adjustments to the contract’s behavior and must be expressed by means of appropriate language features. In this paper, we examine the extension of Stipula, a formal language for legal contracts, with higher-order functionality to enable the dynamic updating of contract codes. We discuss the semantics of the language when amendments either extend or override the contract’s functionality. Additionally, we study two techniques for constraining amendments, one using annotations within the contract and another that allows for runtime agreements between parties
Integration of statutory norms in computable contracts
No full textLegal contracts are governed not only by their explicit terms but also by statutory norms, a principle recognized
across legal systems. As contracts become computable and executable as code, ensuring compliance with these
norms becomes critical. This paper introduces a method for integrating legislative provisions into computable
contracts using the Stipula language, via a novel import construct. We distinguish between mandatory and
default imports to model imperative and optional legal norms, respectively, and define a mechanism to
enforce the priorities between these norms and contract’s provisions. This approach supports the automated
creation of legally compliant contracts and lays the foundation for a broader framework aimed at enhancing
the effectiveness of consumer rights through programmable legal tools
Stipula: a domain specific language for legal contracts
Full text linkWe illustrate Stipula, a novel domain specific language that can assist lawyers
in programming legal contracts through specific software patterns. The language is based
on a small set of programming abstractions that have a precise correspondence with the
distinctive elements of legal contracts. We overview the language by using a simple rental
contract, we discuss a number of formal methods developed for Stipula, and we hint at its
implementation, that can take advantage of (but is not limited to) a blockchain platform
Resilience of Hybrid Casper under varying values of parameters
Full text linkHybrid Casper is the new Ethereum blockchain protocol that uses both Proof of Work and Proof of Stake to reach a consensus between nodes. Here, we analyse the protocol using PRISM+, an extension of the probabilistic model checker PRISM with primitives for expressing blockchain data types. First, we extend PRISM+ to include data types and operations for modelling and analysing Proof of Stake-based consensus protocols. Then, we model Hybrid Casper in PRISM+ as a parallel composition of stochastic processes, thus precisely describing the behaviour of the protocol and highlighting its corner cases. PRISM+ is therefore used to rapidly and automatically analyse the resilience of Hybrid Casper when tuning, up or down, several basic parameters of the protocol, such as the rates of creating blocks, and the strategies for determining penalties. Finally, we study the robustness of Hybrid Casper to two well known attacks: the Eclipse attack and the majority attack
Deadlock detection of java bytecode
No full textThis 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 components of the Java intermediate language – the Java bytecode. Models are subsequently analysed by means of an extension of a solver that we have defined for detecting deadlocks in process calculi. Our technique is complemented by a prototype verifier that also covers most of the Java features
SRA - Static Resource Analyzer for ABS
No full textWe 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). Our technique is modular and consists of (i) a type system associating programs with behavioural types that records relevant information for resource usage (creations, releases, and concurrent operations), (ii) a translation function that takes behavioural types and return cost equations, and (iii) an automatic off-the-shelf solver for the cost equations. A soundness proof of the type system establishes the correctness of our technique with respect to the cost equations. We have experimentally evaluated our technique using a cost analysis solver and we report some results. The experiments show that our analysis allows us to derive bounds for programs that are better than other techniques, such as those based on amortized analysis
DF4ABS - Deadlock Framework for ABS
No full textWe 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 answers or do not scale.
In order to augment precision and scalability we propose a modular framework that allows several techniques to be combined. The basic component of the framework is a front-end inference algorithm that extracts abstract behavioural descriptions of methods, called contracts, which retain resource dependency information.
This component is integrated with a number of possible different back-ends that analyse contracts and derive deadlock information. As a proof-of-concept, we discuss two such back-ends: (i) an evaluator that computes a fixpoint semantics and (ii) an evaluator using abstract model checking
Le forme del falso negli smart contract
No full textLa categoria di falso sembra aver acquisito oggi una speciale centralità: le fake news sembrano incalzarci, le versioni della Storia sembrano cambiare, perfino le verità giudiziarie diventano discutibili. Cosa è successo alla categoria di verità? Sono cambiate le idee di evidenza, certezza, fatto? O sono le istituzioni che garantivano l’affidabilità della verità ad essere in crisi? I contributi di questo volume prendono le mosse da queste domande per tematizzare, con differenti sguardi disciplinari, la questione del falso. Il falso si manifesta in forme diverse nelle opere artistiche, nella comunicazione di massa (e con ulteriori specificità nei discorsi on line), nei procedimenti e nella prassi del diritto, in politica e nelle relazioni internazionali, negli archivi tradizionali e digitali. Cosa rende le falsificazioni “credibili”, quando sono invece irricevibili, quali strumenti hanno le nostre istituzioni (di sapere, di legge, di informazione) per gestirle
Pacta sunt servanda: Legal contracts in Stipula
Full text linkWe present Stipula, a domain specific language that may assist legal practitioners in programming legal contracts through specific patterns. The language is based on a small set of programming abstractions that correspond to common patterns in legal contracts. We illustrate the language by means of two paradigmatic legal contracts: a bike rental and a bet contract. Stipula comes with a formal semantics, an observational equivalence and a type inference system, that provide for a clear account of the contracts' behaviour and illustrate how several concepts from concurrency theory can be adapted to automatically verify the properties and the correctness of software-based legal contracts. We also discuss a prototype centralized implementation of Stipula
Deadlock analysis of unbounded process networks
Full text linkInternational audienceDeadlock 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 programs, and (2) we design a type system for value-passing CCS that returns lam programs. We show the soundness of the type system, and develop a type inference algorithm for it. The resulting algorithm is able to check deadlock-freedom of programs that cannot be handled by previous analyses, such as those that build unbounded networks
- …
