3 papers
cs.CR2026
KindHML: formal verification of smart contracts based on Hennessy-Milner logic
Massimo Bartoletti, Angelo Ferrando, Enrico Lipparini +1
Smart contracts deployed on blockchains such as Ethereum routinely manage large amounts of assets, making their security critical. Empirical studies show that real-world attacks of…
cs.LO2025
A Timed Obstruction Logic for Dynamic Game Models
David Cortes, Jean Leneutre, Vadim Malvone +1
Real-time cybersecurity and privacy applications require reliable verification methods and system design tools to ensure their correctness. Many of these reactive real-time applica…
cs.LO2024
Probabilistic Obstruction Temporal Logic: a Probabilistic Logic to Reason about Dynamic Models
Jean Leneutre, Vadim Malvone, James Ortiz
In this paper, we propose a novel formalism called Probabilistic Obstruction Temporal Logic (POTL), which extends Obstruction Logic (OL) by incorporating probabilistic elements. PO…