31 citations · 53 across the 15 of their papers we have counts for
17 papers
SolBehave: Evaluating the Behavioural Correctness of LLM-Generated Smart Contracts
Giovanni Pio Delvecchio, Stefano Fantazzini, Giacomo Frisoni +4
Large language models increasingly generate Solidity smart contracts that, once deployed, can never be patched, making a single latent fault permanent and exploitable. Yet current…
A Sound and Complete Characterization of Fair Asynchronous Session Subtyping
Mario Bravetti, Luca Padovani, Gianluigi Zavattaro
Session types are abstractions of communication protocols enabling the static analysis of message-passing processes. Refinement notions for session types are key to support safe fo…
A Session Subtyping Tool (Extended Version)
Lorenzo Bacchiani, Mario Bravetti, Julien Lange +1
Session types are becoming popular and have been integrated in several mainstream programming languages. Nevertheless, while many programming languages consider asynchronous fifo c…
Microservice Dynamic Architecture-Level Deployment Orchestration (Extended Version)
Lorenzo Bacchiani, Mario Bravetti, Saverio Giallorenzo +3
In the context of the BI-REX (Big Data Innovation and Research Excellence) competence center SEAWALL (SEAmless loW lAtency cLoud pLatforms) project (scientific coordinator Prof. Ma…
Fair Asynchronous Session Subtyping
Mario Bravetti, Julien Lange, Gianluigi Zavattaro
Session types are widely used as abstractions of asynchronous message passing systems. Refinement for such abstractions is crucial as it allows improvements of a given component wi…
Microservice Interface Based Deployment Orchestration
Lorenzo Bacchiani, Mario Bravetti, Saverio Giallorenzo +3
Following previous work on the automated deployment orchestration of component based applications, where orchestrations are expressed in terms of behaviours satisfying component in…
Behavioural Types for Memory and Method Safety in a Core Object-Oriented Language
Mario Bravetti, Adrian Francalanza, Iaroslav Golovanov +4
We present a type-based analysis ensuring memory safety and object protocol completion in the Java-like language Mungo. Objects are annotated with usages, typestates-like specifica…
Axiomatizing Maximal Progress and Discrete Time
Mario Bravetti
Milner's complete proof system for observational congruence is crucially based on the possibility to equate divergent expressions to non-divergent ones by means of the axiom $r…
A Sound Algorithm for Asynchronous Session Subtyping and its Implementation
Mario Bravetti, Marco Carbone, Julien Lange +2
Session types, types for structuring communication between endpoints in distributed systems, are recently being integrated into mainstream programming languages. In practice, a ver…
Optimal and Automated Deployment for Microservices
Mario Bravetti, Saverio Giallorenzo, Jacopo Mauro +2
Microservices are highly modular and scalable Service Oriented Architectures. They underpin automated deployment practices like Continuous Deployment and Autoscaling. In this paper…
On the Boundary between Decidability and Undecidability of Asynchronous Session Subtyping
Mario Bravetti, Marco Carbone, Gianluigi Zavattaro
Session types are behavioural types for guaranteeing that concurrent programs are free from basic communication errors. Recent work has shown that asynchronous session subtyping is…
Undecidability of Asynchronous Session Subtyping
Mario Bravetti, Marco Carbone, Gianluigi Zavattaro
Session types are used to describe communication protocols in distributed systems and, as usual in type theories, session subtyping characterizes substitutability of the communicat…
Towards Dynamic Updates in Service Composition
Mario Bravetti
We survey our results about verification of adaptable processes. We present adaptable processes as a way of overcoming the limitations that process calculi have for describing patt…
Reduction Semantics in Markovian Process Algebra
Mario Bravetti
Stochastic (Markovian) process algebra extend classical process algebra with probabilistic exponentially distributed time durations denoted by rates (the parameter of the exponenti…
Choreographies and Behavioural Contracts on the Way to Dynamic Updates
Mario Bravetti, Gianluigi Zavattaro
We survey our work on choreographies and behavioural contracts in multiparty interactions. In particular theories of behavioural contracts are presented which enable reasoning abou…
Adaptable processes
Mario Bravetti, Cinzia Di Giusto, Jorge A Perez +1
We propose the concept of adaptable processes as a way of overcoming the limitations that process calculi have for describing patterns of dynamic process evolution. Such patterns r…
File Managing and Program Execution in Web Operating Systems
Mario Bravetti
Web Operating Systems can be seen as an extension of traditional Operating Systems where the addresses used to manage files and execute programs (via the basic load/execution mecha…