10 citations · 22 across the 13 of their papers we have counts for
13 papers
Runtime Verification via Rational Monitor with Imperfect Information
Angelo Ferrando, Vadim Malvone
Trusting software systems, particularly autonomous ones, is challenging. To address this, formal verification techniques can ensure these systems behave as expected. Runtime Verifi…
Solvent: liquidity verification of smart contracts
Massimo Bartoletti, Angelo Ferrando, Enrico Lipparini +1
Smart contracts are an attractive target for attackers, as evidenced by a long history of security incidents. A current limitation of smart contract verification tools is that they…
VITAMIN: A Compositional Framework for Model Checking of Multi-Agent Systems
Angelo Ferrando, Vadim Malvone
The verification of Multi-Agent Systems (MAS) poses a significant challenge. Various approaches and methodologies exist to address this challenge; however, tools that support them…
3vLTL: A Tool to Generate Automata for Three-valued LTL
Francesco Belardinelli, Angelo Ferrando, Vadim Malvone
Multi-valued logics have a long tradition in the literature on system verification, including run-time verification. However, comparatively fewer model-checking tools have been dev…
Scalable Verification of Strategy Logic through Three-valued Abstraction
Francesco Belardinelli, Angelo Ferrando, Wojciech Jamroga +2
The model checking problem for multi-agent systems against Strategy Logic specifications is known to be non-elementary. On this logic several fragments have been defined to tackle…
The Impact of Strategies and Information in Model Checking for Multi-Agent Systems
Vadim Malvone
System correctness is one of the most crucial and challenging objectives in software and hardware systems. With the increasing evolution of connected and distributed systems, ensur…
Program Semantics and a Verification Technique for Knowledge-Based Multi-Agent Systems
Francesco Belardinelli, Ioana Boureanu, Vadim Malvone +1
We give a relational and a weakest precondition semantics for "knowledge-based programs", i.e., programs that restrict observability of variables so as to richly express changes in…
Model Checking Strategic Abilities in Information-sharing Systems
Francesco Belardinelli, Ioana Boureanu, Catalin Dima +1
We introduce a subclass of concurrent game structures (CGS) with imperfect information in which agents are endowed with private data-sharing capabilities. Importantly, our CGSs are…
Towards the Combination of Model Checking and Runtime Verification on Multi-Agent Systems
Angelo Ferrando, Vadim Malvone
Multi-Agent Systems (MAS) are notoriously complex and hard to verify. In fact, it is not trivial to model a MAS, and even when a model is built, it is not always possible to verify…
Reasoning about Human-Friendly Strategies in Repeated Keyword Auctions
Francesco Belardinelli, Wojtek Jamroga, Vadim Malvone +3
In online advertising, search engines sell ad placements for keywords continuously through auctions. This problem can be seen as an infinitely repeated game since the auction is ex…
Towards the Verification of Strategic Properties in Multi-Agent Systems with Imperfect Information
Angelo Ferrando, Vadim Malvone
In logics for the strategic reasoning the main challenge is represented by their verification in contexts of imperfect information and perfect recall. In this work, we show a techn…
A Hennessy-Milner Theorem for ATL with Imperfect Information
Francesco Belardinelli, Catalin Dima, Vadim Malvone +1
We show that a history-based variant of alternating bisimulation with imperfect information allows it to be related to a variant of Alternating-time Temporal Logic (ATL) with imper…
Model Checking ATL* on vCGS
Francesco Belardinelli, Catalin Dima, Ioana Boureanu +1
We prove that the model checking ATL* on concurrent game structures with propositional control for atom-visibility (vCGS) is undecidable. To do so, we reduce this problem to model…