4 Search Results for "Doan, Thi Thu Ha"

Document
DOI: 10.4230/LIPIcs.ECOOP.2024.3
A Dynamic Logic for Symbolic Execution for the Smart Contract Programming Language Michelson

Authors: Barnabas Arvay, Thi Thu Ha Doan, and Peter Thiemann

Published in: LIPIcs, Volume 313, 38th European Conference on Object-Oriented Programming (ECOOP 2024)

Abstract
Verification of smart contracts is an important topic in the context of blockchain technology. We study an approach to verification that is based on symbolic execution. As a formal basis for symbolic execution, we design a dynamic logic for Michelson, the smart contract language of the Tezos blockchain, and prove its soundness in the proof assistant Agda. Towards the soundness proof we formalize the concrete semantics as well as its symbolic counterpart in a unified setting. The logic encompasses single contract runs as well as inter-contract runs chained in a single transaction.
Cite as

Barnabas Arvay, Thi Thu Ha Doan, and Peter Thiemann. A Dynamic Logic for Symbolic Execution for the Smart Contract Programming Language Michelson. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 3:1-3:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{arvay_et_al:LIPIcs.ECOOP.2024.3,
  author =	{Arvay, Barnabas and Doan, Thi Thu Ha and Thiemann, Peter},
  title =	{{A Dynamic Logic for Symbolic Execution for the Smart Contract Programming Language Michelson}},
  booktitle =	{38th European Conference on Object-Oriented Programming (ECOOP 2024)},
  pages =	{3:1--3:26},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-341-6},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{313},
  editor =	{Aldrich, Jonathan and Salvaneschi, Guido},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2024.3},
  URN =		{urn:nbn:de:0030-drops-208529},
  doi =		{10.4230/LIPIcs.ECOOP.2024.3},
  annote =	{Keywords: Smart Contract, Blockchain, Formal Verification, Symbolic Execution}
}
Document
DOI: 10.4230/LITES.8.2.2
Swarms of Mobile Robots: Towards Versatility with Safety

Authors: Pierre Courtieu, Lionel Rieg, Sébastien Tixeuil, and Xavier Urbain

Published in: LITES, Volume 8, Issue 2 (2022): Special Issue on Distributed Hybrid Systems. Leibniz Transactions on Embedded Systems, Volume 8, Issue 2

Abstract
We present Pactole, a formal framework to design and prove the correctness of protocols (or the impossibility of their existence) that target mobile robotic swarms. Unlike previous approaches, our methodology unifies in a single formalism the execution model, the problem specification, the protocol, and its proof of correctness. The Pactole framework makes use of the Coq proof assistant, and is specially targeted at protocol designers and problem specifiers, so that a common unambiguous language is used from the very early stages of protocol development. We stress the underlying framework design principles to enable high expressivity and modularity, and provide concrete examples about how the Pactole framework can be used to tackle actual problems, some previously addressed by the Distributed Computing community, but also new problems, while being certified correct.
Cite as

Pierre Courtieu, Lionel Rieg, Sébastien Tixeuil, and Xavier Urbain. Swarms of Mobile Robots: Towards Versatility with Safety. In LITES, Volume 8, Issue 2 (2022): Special Issue on Distributed Hybrid Systems. Leibniz Transactions on Embedded Systems, Volume 8, Issue 2, pp. 02:1-02:36, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@Article{courtieu_et_al:LITES.8.2.2,
  author =	{Courtieu, Pierre and Rieg, Lionel and Tixeuil, S\'{e}bastien and Urbain, Xavier},
  title =	{{Swarms of Mobile Robots: Towards Versatility with Safety}},
  journal =	{Leibniz Transactions on Embedded Systems},
  pages =	{02:1--02:36},
  ISSN =	{2199-2002},
  year =	{2022},
  volume =	{8},
  number =	{2},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LITES.8.2.2},
  URN =		{urn:nbn:de:0030-drops-192942},
  doi =		{10.4230/LITES.8.2.2},
  annote =	{Keywords: distributed algorithm, mobile autonomous robots, formal proof}
}
Document
Short Paper
DOI: 10.4230/OASIcs.FMBC.2021.5
Towards Contract Modules for the Tezos Blockchain (Short Paper)

Authors: Thi Thu Ha Doan and Peter Thiemann

Published in: OASIcs, Volume 95, 3rd International Workshop on Formal Methods for Blockchains (FMBC 2021)

Abstract
Programmatic interaction with a blockchain is often clumsy. Many interfaces handle only loosely structured data, often in JSON format, that is inconvenient to handle and offers few guarantees. Contract modules provide a statically checked interface to interact with contracts on the Tezos blockchain. A module specification provides all types as well as information about potential failure conditions of the contract. The specification is checked against the contract implementation using symbolic execution. An OCaml module is generated that contains a function for each entry point of the contract. The types of these functions fully describe the interface including the failure conditions and guarantee type-safe and sometimes fail-safe invocation of the contract on the blockchain.
Cite as

Thi Thu Ha Doan and Peter Thiemann. Towards Contract Modules for the Tezos Blockchain (Short Paper). In 3rd International Workshop on Formal Methods for Blockchains (FMBC 2021). Open Access Series in Informatics (OASIcs), Volume 95, pp. 5:1-5:9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{doan_et_al:OASIcs.FMBC.2021.5,
  author =	{Doan, Thi Thu Ha and Thiemann, Peter},
  title =	{{Towards Contract Modules for the Tezos Blockchain}},
  booktitle =	{3rd International Workshop on Formal Methods for Blockchains (FMBC 2021)},
  pages =	{5:1--5:9},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-209-9},
  ISSN =	{2190-6807},
  year =	{2021},
  volume =	{95},
  editor =	{Bernardo, Bruno and Marmsoler, Diego},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2021.5},
  URN =		{urn:nbn:de:0030-drops-154294},
  doi =		{10.4230/OASIcs.FMBC.2021.5},
  annote =	{Keywords: contract API, modules, static checking}
}
Document
DOI: 10.4230/LIPIcs.OPODIS.2017.12
Model Checking of Robot Gathering

Authors: Ha Thi Thu Doan, François Bonnet, and Kazuhiro Ogata

Published in: LIPIcs, Volume 95, 21st International Conference on Principles of Distributed Systems (OPODIS 2017)

Abstract
Recent advances in distributed computing highlight models and algorithms for autonomous mo- bile robots that self-organize and cooperate together in order to solve a global objective. As results, a large number of algorithms have been proposed. These algorithms are given together with proofs to assess their correctness. However, those proofs are informal, which are error prone. This paper presents our study on formal verification of mobile robot algorithms. We first propose a formal model for mobile robot algorithms on anonymous ring shape network under multiplicity and asynchrony assumptions. We specify this formal model in Maude, a specification and pro- gramming language based on rewriting logic. We then use its model checker to formally verify an algorithm for robot gathering problem on ring enjoys some desired properties. As the result of the model checking, counterexamples have been found. We detect the sources of some unforeseen design errors. We, furthermore, give our interpretations of these errors.
Cite as

Ha Thi Thu Doan, François Bonnet, and Kazuhiro Ogata. Model Checking of Robot Gathering. In 21st International Conference on Principles of Distributed Systems (OPODIS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 95, pp. 12:1-12:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{doan_et_al:LIPIcs.OPODIS.2017.12,
  author =	{Doan, Ha Thi Thu and Bonnet, Fran\c{c}ois and Ogata, Kazuhiro},
  title =	{{Model Checking of Robot Gathering}},
  booktitle =	{21st International Conference on Principles of Distributed Systems (OPODIS 2017)},
  pages =	{12:1--12:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-061-3},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{95},
  editor =	{Aspnes, James and Bessani, Alysson and Felber, Pascal and Leit\~{a}o, Jo\~{a}o},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.OPODIS.2017.12},
  URN =		{urn:nbn:de:0030-drops-86324},
  doi =		{10.4230/LIPIcs.OPODIS.2017.12},
  annote =	{Keywords: Mobile Robot, Robot Gathering, Formal Verification, Model Checking, Maude}
}
  • Refine by Type
  • 4 Document/PDF

  • Refine by Publication Year
  • 1 2024
  • 1 2022
  • 1 2021
  • 1 2018

  • Refine by Author
  • 2 Doan, Thi Thu Ha
  • 2 Thiemann, Peter
  • 1 Arvay, Barnabas
  • 1 Bonnet, François
  • 1 Courtieu, Pierre
  • Show More...

  • Refine by Series/Journal
  • 2 LIPIcs
  • 1 OASIcs
  • 1 LITES

  • Refine by Classification
  • 1 Software and its engineering → Automated static analysis
  • 1 Software and its engineering → Formal methods
  • 1 Software and its engineering → Specification languages
  • 1 Theory of computation → Distributed computing models
  • 1 Theory of computation → Logic
  • Show More...

  • Refine by Keyword
  • 2 Formal Verification
  • 1 Blockchain
  • 1 Maude
  • 1 Mobile Robot
  • 1 Model Checking
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact