Massimo Bartoletti

CoRR, 2024

2023

Sound approximate and asymptotic probabilistic bisimulations for PCTL.

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2023

DeFi composability as MEV non-interference.

[BibT_eX]

[DOI]

Riccardo Marchesin

CoRR, 2023

Secure compilation of rich smart contracts on poor UTXO blockchains.

[BibT_eX]

[DOI]

Riccardo Marchesin

CoRR, 2023

A theoretical basis for Blockchain Extractable Value.

[BibT_eX]

[DOI]

CoRR, 2023

2022

Verifying liquidity of recursive Bitcoin contracts.

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2022

A theory of Automated Market Makers in DeFi.

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2022

Formal Analysis of Lending Pools in Decentralized Finance.

[BibT_eX]

[DOI]

Tommi Junttila

Massimiliano Mirelli

Andrea Vandin

Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation. Adaptation and Learning, 2022

Maximizing Extractable Value from Automated Market Makers.

[BibT_eX]

[DOI]

Proceedings of the Financial Cryptography and Data Security, 2022

A Sound Up-to-n, δ Bisimilarity for PCTL.

[BibT_eX]

[DOI]

Proceedings of the Coordination Models and Languages, 2022

MEV-Freedom, in DeFi and Beyond (Invited Talk).

[BibT_eX]

[DOI]

Proceedings of the 4th International Workshop on Formal Methods for Blockchains, 2022

2021

A theory of transaction parallelism in blockchains.

[BibT_eX]

[DOI]

Letterio Galletta

Log. Methods Comput. Sci., 2021

Cryptocurrency Scams: Analysis and Perspectives.

[BibT_eX]

[DOI]

IEEE Access, 2021

SoK: Lending Pools in Decentralized Finance.

[BibT_eX]

[DOI]

Proceedings of the Financial Cryptography and Data Security. FC 2021 International Workshops, 2021

Towards a Theory of Decentralized Finance.

[BibT_eX]

[DOI]

Proceedings of the Financial Cryptography and Data Security. FC 2021 International Workshops, 2021

A Formal Model of Algorand Smart Contracts.

[BibT_eX]

[DOI]

Proceedings of the Financial Cryptography and Data Security, 2021

Computationally sound Bitcoin tokens.

[BibT_eX]

[DOI]

Proceedings of the 34th IEEE Computer Security Foundations Symposium, 2021

2020

Dissecting Ponzi schemes on Ethereum: Identification, analysis, and impact.

[BibT_eX]

[DOI]

Future Gener. Comput. Syst., 2020

Smart Contracts Contracts.

[BibT_eX]

[DOI]

Frontiers Blockchain, 2020

Verification of recursive Bitcoin contracts.

[BibT_eX]

[DOI]

CoRR, 2020

Bitcoin Covenants Unchained.

[BibT_eX]

[DOI]

Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation: Applications, 2020

Renegotiation and Recursion in Bitcoin Contracts.

[BibT_eX]

[DOI]

Proceedings of the Coordination Models and Languages, 2020

A True Concurrent Model of Smart Contracts Executions.

[BibT_eX]

[DOI]

Letterio Galletta

Proceedings of the Coordination Models and Languages, 2020

2019

Preface for the special issue on Interaction and Concurrency Experience 2017.

[BibT_eX]

[DOI]

J. Log. Algebraic Methods Program., 2019

A Journey into Bitcoin Metadata.

[BibT_eX]

[DOI]

Bryn Bellomy

J. Grid Comput., 2019

Formal Models of Bitcoin Contracts: A Survey.

[BibT_eX]

[DOI]

Frontiers Blockchain, 2019

Developing secure bitcoin contracts with BitML.

[BibT_eX]

[DOI]

Proceedings of the ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, 2019

A Minimal Core Calculus for Solidity Contracts.

[BibT_eX]

[DOI]

Letterio Galletta

Proceedings of the Data Privacy Management, Cryptocurrencies and Blockchain Technology, 2019

2018

Preface for the special issue on Interaction and Concurrency Experience 2016.

[BibT_eX]

[DOI]

J. Log. Algebraic Methods Program., 2018

Verifying liquidity of Bitcoin contracts.

[BibT_eX]

[DOI]

IACR Cryptol. ePrint Arch., 2018

BitML: a calculus for Bitcoin smart contracts.

[BibT_eX]

[DOI]

IACR Cryptol. ePrint Arch., 2018

Fun with Bitcoin smart contracts.

[BibT_eX]

[DOI]

IACR Cryptol. ePrint Arch., 2018

SoK: unraveling Bitcoin smart contracts.

[BibT_eX]

[DOI]

IACR Cryptol. ePrint Arch., 2018

Blockchain for social good: a quantitative analysis.

[BibT_eX]

[DOI]

Proceedings of the 4th EAI International Conference on Smart Objects and Technologies for Social Good, 2018

Data Mining for Detecting Bitcoin Ponzi Schemes.

[BibT_eX]

[DOI]

Barbara Pes

Sergio Serusi

Proceedings of the Crypto Valley Conference on Blockchain Technology, 2018

Progress-Preserving Refinements of CTA.

[BibT_eX]

[DOI]

Laura Bocchi

Proceedings of the 29th International Conference on Concurrency Theory, 2018

2017

Timed Session Types.

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2017

Verifiable abstractions for contract-oriented systems.

[BibT_eX]

[DOI]

J. Log. Algebraic Methods Program., 2017

A Proof-of-Stake protocol for consensus on Bitcoin subchains.

[BibT_eX]

[DOI]

Alessandro Sebastian Podda

IACR Cryptol. ePrint Arch., 2017

A formal model of Bitcoin transactions.

[BibT_eX]

[DOI]

IACR Cryptol. ePrint Arch., 2017

A general framework for Bitcoin analytics.

[BibT_eX]

[DOI]

CoRR, 2017

A Survey of Attacks on Ethereum Smart Contracts (SoK).

[BibT_eX]

[DOI]

Nicola Atzei

Proceedings of the Principles of Security and Trust - 6th International Conference, 2017

A general framework for blockchain analytics.

[BibT_eX]

[DOI]

Proceedings of the 1st Workshop on Scalable and Resilient Infrastructures for Distributed Ledgers, 2017

An Empirical Analysis of Smart Contracts: Platforms, Applications, and Design Patterns.

[BibT_eX]

[DOI]

Proceedings of the Financial Cryptography and Data Security, 2017

An Analysis of Bitcoin OP_RETURN Metadata.

[BibT_eX]

[DOI]

Proceedings of the Financial Cryptography and Data Security, 2017

2016

Contracts as games on event structures.

[BibT_eX]

[DOI]

J. Log. Algebraic Methods Program., 2016

Constant-deposit multiparty lotteries on Bitcoin.

[BibT_eX]

[DOI]

IACR Cryptol. ePrint Arch., 2016

A survey of attacks on Ethereum smart contracts.

[BibT_eX]

[DOI]

Nicola Atzei

IACR Cryptol. ePrint Arch., 2016

Honesty by Typing

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2016

Faderank: An Incremental Algorithm for Ranking Twitter Users.

[BibT_eX]

[DOI]

Alessandro Massa

Proceedings of the Web Information Systems Engineering - WISE 2016, 2016

Developing Honest Java Programs with Diogenes.

[BibT_eX]

[DOI]

Nicola Atzei

Proceedings of the Formal Techniques for Distributed Objects, Components, and Systems, 2016

2015

Choreographies in the wild.

[BibT_eX]

[DOI]

Sci. Comput. Program., 2015

Lending Petri nets.

[BibT_eX]

[DOI]

G. Michele Pinna

Sci. Comput. Program., 2015

Vicious circles in contracts and in logic.

[BibT_eX]

[DOI]

Paolo Di Giamberardino

Sci. Comput. Program., 2015

Model checking usage policies.

[BibT_eX]

[DOI]

Math. Struct. Comput. Sci., 2015

Combining behavioural types with security analysis.

[BibT_eX]

[DOI]

Mariangiola Dezani-Ciancaglini

Ilaria Castellani

Pierre-Malo Deniélou

J. Log. Algebraic Methods Program., 2015

The LTS WorkBench.

[BibT_eX]

[DOI]

Alceste Scalas

Proceedings of the Proceedings 8th Interaction and Concurrency Experience, 2015

On the Decidability of Honesty and of Its Variants.

[BibT_eX]

[DOI]

Proceedings of the Web Services, Formal Methods, and Behavioral Types, 2015

Models of Circular Causality.

[BibT_eX]

[DOI]

Proceedings of the Distributed Computing and Internet Technology, 2015

Compliance and Subtyping in Timed Session Types.

[BibT_eX]

[DOI]

Alessandro Sebastian Podda

Proceedings of the Formal Techniques for Distributed Objects, Components, and Systems, 2015

A Contract-Oriented Middleware.

[BibT_eX]

[DOI]

Alessandro Sebastian Podda

Proceedings of the Formal Aspects of Component Software - 12th International Conference, 2015

Debits and Credits in Petri Nets and Linear Logic.

[BibT_eX]

[DOI]

Paolo Di Giamberardino

Proceedings of the Logic, Rewriting, and Concurrency, 2015

Compliance in Behavioural Contracts: A Brief Survey.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages with Applications to Biology and Security, 2015

2014

Circular Causality in Event Structures.

[BibT_eX]

[DOI]

Fundam. Informaticae, 2014

A note on two notions of compliance.

[BibT_eX]

[DOI]

G. Michele Pinna

Proceedings of the Proceedings 7th Interaction and Concurrency Experience, 2014

Modelling and Verifying Contract-Oriented Systems in Maude.

[BibT_eX]

[DOI]

Proceedings of the Rewriting Logic and Its Applications - 10th International Workshop, 2014

A Semantic Deconstruction of Session Types.

[BibT_eX]

[DOI]

Alceste Scalas

Proceedings of the CONCUR 2014 - Concurrency Theory - 25th International Conference, 2014

2013

Contract agreements via logic.

[BibT_eX]

[DOI]

Paolo Di Giamberardino

Proceedings of the Proceedings 6th Interaction and Concurrency Experience, 2013

A Theory of Agreements and Protection.

[BibT_eX]

[DOI]

Proceedings of the Principles of Security and Trust - Second International Conference, 2013

Lending Petri Nets and Contracts.

[BibT_eX]

[DOI]

G. Michele Pinna

Proceedings of the Fundamentals of Software Engineering - 5th International Conference, 2013

2012

Contract-Oriented Computing in CO2.

[BibT_eX]

[DOI]

Emilio Tuosto

Sci. Ann. Comput. Sci., 2012

An event-based model for contracts

[BibT_eX]

[DOI]

Proceedings of the Proceedings Fifth Workshop on Programming Language Approaches to Concurrency- and Communication-cEntric Software, 2012

On the Realizability of Contracts in Dishonest Systems.

[BibT_eX]

[DOI]

Emilio Tuosto

Proceedings of the Coordination Models and Languages - 14th International Conference, 2012

2011

Contracts in distributed systems

[BibT_eX]

[DOI]

Emilio Tuosto

Proceedings of the Proceedings Fourth Interaction and Concurrency Experience, 2011

Call-by-Contract for Service Discovery, Orchestration and Recovery.

[BibT_eX]

[DOI]

Proceedings of the Rigorous Software Engineering for Service-Oriented Systems, 2011

Tools and Verification.

[BibT_eX]

[DOI]

Proceedings of the Rigorous Software Engineering for Service-Oriented Systems, 2011

2010

Primitives for Contract-based Synchronization

[BibT_eX]

[DOI]

Proceedings of the Proceedings Third Interaction and Concurrency Experience: Guaranteed Interaction, 2010

Static Enforcement of Service Deadlines.

[BibT_eX]

[DOI]

Proceedings of the 8th IEEE International Conference on Software Engineering and Formal Methods, 2010

A Calculus of Contracting Processes.

[BibT_eX]

[DOI]

Proceedings of the 25th Annual IEEE Symposium on Logic in Computer Science, 2010

2009

Local policies for resource usage analysis.

[BibT_eX]

[DOI]

ACM Trans. Program. Lang. Syst., 2009

Securing Java with Local Policies.

[BibT_eX]

[DOI]

J. Object Technol., 2009

Planning and verifying service composition.

[BibT_eX]

[DOI]

J. Comput. Secur., 2009

Jalapa: Securing Java with Local Policies: Tool Demonstration.

[BibT_eX]

[DOI]

Gabriele Costa

Proceedings of the Fourth Workshop on Bytecode Semantics, 2009

Usage Automata.

[BibT_eX]

[DOI]

Proceedings of the Foundations and Applications of Security Analysis, 2009

A Logic for Contracts.

[BibT_eX]

Proceedings of the Theoretical Computer Science, 11th Italian Conference, 2009

<i>nu</i>-Types for Effects and Freshness Analysis.

[BibT_eX]

[DOI]

Proceedings of the Theoretical Aspects of Computing, 2009

2008

Semantics-Based Design for Secure Web Services.

[BibT_eX]

[DOI]

IEEE Trans. Software Eng., 2008

Hard Life with Weak Binders.

[BibT_eX]

[DOI]

Proceedings of the 15th Workshop on Expressiveness in Concurrency, 2008

2007

Types and Effects for Resource Usage Analysis.

[BibT_eX]

[DOI]

Proceedings of the Foundations of Software Science and Computational Structures, 2007

Secure Service Orchestration.

[BibT_eX]

[DOI]

Proceedings of the Foundations of Security Analysis and Design IV, 2007

2006

Security Issues in Service Composition.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods for Open Object-Based Distributed Systems, 2006

Types and Effects for Secure Service Orchestration.

[BibT_eX]

[DOI]

Proceedings of the 19th IEEE Computer Security Foundations Workshop, 2006

2005

Language-based security.

[BibT_eX]

[DOI]

PhD thesis, 2005

Policy framings for access control.

[BibT_eX]

[DOI]

Proceedings of the POPL 2005 Workshop on Issues in the Theory of Security, 2005

Checking Risky Events Is Enough for Local Policies.

[BibT_eX]

[DOI]

Proceedings of the Theoretical Computer Science, 9th Italian Conference, 2005

History-Based Access Control with Local Policies.

[BibT_eX]

[DOI]

Proceedings of the Foundations of Software Science and Computational Structures, 2005

Enforcing Secure Service Composition.

[BibT_eX]

[DOI]

Proceedings of the 18th IEEE Computer Security Foundations Workshop, 2005

2004

Stack inspection and secure program transformations.

[BibT_eX]

[DOI]

Int. J. Inf. Sec., 2004

2003

Program Transformations under Dynamic Security Policies.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods for Security and Time: Proceedings of the MEFISTO Project 2003, 2003

Security-Aware Program Transformations.

[BibT_eX]

[DOI]

Proceedings of the Theoretical Computer Science, 8th Italian Conference, 2003

2001

Static Analysis for Stack Inspection.

[BibT_eX]

[DOI]