A5047065626- Distributed systems and fault tolerance
- Logic, programming, and type systems
- Security and Verification in Computing
- Formal Methods in Verification
- Logic, Reasoning, and Knowledge
- Access Control and Trust
- Artificial Intelligence in Law
- Advanced Malware Detection Techniques
- Computability, Logic, AI Algorithms
- Evolutionary Algorithms and Applications
- Multi-Agent Systems and Negotiation
- Parallel Computing and Optimization Techniques
- Service-Oriented Architecture and Web Services
- Model-Driven Software Engineering Techniques
- Semantic Web and Ontologies
- Cryptography and Data Security
- Origins and Evolution of Life
- Mobile Agent-Based Network Management
- Blockchain Technology Applications and Security
- Explainable Artificial Intelligence (XAI)
- Ethics and Social Impacts of AI
- Personal Information Management and User Behavior
- Bayesian Modeling and Causal Inference
- Advanced Database Systems and Queries
- Business Process Modeling and Analysis
University of Padua
2014-2024
Civita
2018
Instituto Nacional de Matemática Pura e Aplicada
2007
Ca' Foscari University of Venice
2000-2005
École Normale Supérieure - PSL
2001
Département d'Informatique
2001
Boxed Ambients are a variant of Mobile that result from dropping the open capability and introducing new primitives for ambient communication. The model communication is faithful to principles distribution location-awareness Ambients, complements constructs in out mobility with finer-grained mechanisms interaction. We introduce calculus, study impact typing mobility, show they yield an effective framework resource protection access control distributed systems.
Formal verification plays a crucial role in making smart contracts safer, being able to find bugs or guarantee their absence, as well checking whether the business logic is correctly implemented. For Solidity, even though there already exist several mature tools, semantical quirks of language can make quite hard practice. Move, on other hand, has been designed with security and mind, it accompanied since its early stages by formal tool, Move Prover. In this paper, we investigate through...
We propose a logic for true concurrency whose formulae predicate about events in computations and their causal dependencies. The induced logical equivalence is hereditary history-preserving bisimilarity, fragments of the can be identified which correspond to other concurrent behavioural equivalences literature: step, pomset bisimilarity. Standard Hennessy-Milner logic, thus (interleaving) also recovered as fragment. an extension with fixpoint operators, allowing describe properties infinite...
We study the problem of secure information flow for Boxed Ambients in terms non-interference. develop a sound type system that provides static guarantees absence unwanted well typed processes. Non-interference is stated, and proved, notion contextual equivalence akin to corresponding defined Mobile Ambients.
We study a novel approach to typestate-oriented programming based on the chemical metaphor: state and operations objects are molecules of messages transformations reactions. This allows us investigate typestate in an inherently concurrent setting, whereby can be accessed modified concurrently by several processes, each potentially changing only part their state. introduce simple behavioral type theory express uniform way both private public interfaces objects, describe enforce structured...
Decentralized blockchain platforms support the secure exchange of assets among users without relying on trusted third parties. These exchanges are programmed with smart contracts, computer programs directly executed by nodes. Multiple contract languages available nowadays to developers, each its own distinctive features, strengths, and weaknesses. In this paper, we examine used in six major platforms: Ethereum, Solana, Cardano, Algorand, Aptos, Tezos. Starting a high-level overview their...
A number of algorithms for computing the simulation preorder on Kripke structures and labelled transition systems are available. Among them, algorithm by Ranzato Tapparo [2007] has best time complexity,while Gentilini
We introduce a novel approach to typestate-oriented programming based on the chemical metaphor: state and operations objects are molecules of messages, transformations reactions. This allows us investigate typestate in an inherently concurrent setting, whereby can be accessed modified concurrently by several processes, each potentially changing only part their state. simple behavioral type theory express uniform way both private public interfaces objects; describe enforce structured object...