3 Search Results for "Reeves, Steve"

Document
DOI: 10.4230/OASIcs.SpaceCHI.2025.7
Unbound Human-Machine Interfaces for Interaction in Weightless Environments

Authors: Jessica R. Cauchard

Published in: OASIcs, Volume 130, Advancing Human-Computer Interaction for Space Exploration (SpaceCHI 2025)

Abstract
User interfaces are subject to the rules of physics (e.g., Newton and Archimedes' laws) relevant to the environment they are in. As such, most interfaces and interaction techniques have been designed for Earth surface. However, when interacting with technology in weightless environments, such as in space, both human and machine will be subject to different physical constraints. For instance, underwater or in Space, people can experience spatial disorientation, which will in turn affect how they use a system. This position paper conceptualizes unbound Human-Machine Interfaces (HMIs) as interfaces where either, or both, human and machine are located beyond Earth surface. In particular, it describes how traditional HCI needs to be rethought for interaction in weightless environments and how theoretical models such as joint cognition can support future developments of unbound interfaces.
Cite as

Jessica R. Cauchard. Unbound Human-Machine Interfaces for Interaction in Weightless Environments. In Advancing Human-Computer Interaction for Space Exploration (SpaceCHI 2025). Open Access Series in Informatics (OASIcs), Volume 130, pp. 7:1-7:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{cauchard:OASIcs.SpaceCHI.2025.7,
  author =	{Cauchard, Jessica R.},
  title =	{{Unbound Human-Machine Interfaces for Interaction in Weightless Environments}},
  booktitle =	{Advancing Human-Computer Interaction for Space Exploration (SpaceCHI 2025)},
  pages =	{7:1--7:8},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-384-3},
  ISSN =	{2190-6807},
  year =	{2025},
  volume =	{130},
  editor =	{Bensch, Leonie and Nilsson, Tommy and Nisser, Martin and Pataranutaporn, Pat and Schmidt, Albrecht and Sumini, Valentina},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.SpaceCHI.2025.7},
  URN =		{urn:nbn:de:0030-drops-239970},
  doi =		{10.4230/OASIcs.SpaceCHI.2025.7},
  annote =	{Keywords: human-robot interaction, gravity, space, interaction technique}
}
Document
DOI: 10.4230/OASIcs.FMBC.2025.8
Formal Verification of a Fail-Safe Cross-Chain Bridge

Authors: Filip Marić, Bernhard Scholz, and Pavle Subotić

Published in: OASIcs, Volume 129, 6th International Workshop on Formal Methods for Blockchains (FMBC 2025)

Abstract
Cross-chain bridges are financial services that interconnect blockchains. High monetary values flow through these bridges, and their security must be safeguarded. However, designing real-world cross-chain bridges is a difficult endeavor. Due to blockchain’s closed-world nature, tokens cannot be transferred from a sender to a receiver chain; on the contrary, they need complex logic that maintains an equilibrium on both chains, even if either the chains or the bridge fail. This paper formally verifies a model of a novel fail-safe cross-chain bridge to ensure correctness. We define formal requirements and prove the bridge is safe using the Isabelle/HOL proof assistant.
Cite as

Filip Marić, Bernhard Scholz, and Pavle Subotić. Formal Verification of a Fail-Safe Cross-Chain Bridge. In 6th International Workshop on Formal Methods for Blockchains (FMBC 2025). Open Access Series in Informatics (OASIcs), Volume 129, pp. 8:1-8:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{maric_et_al:OASIcs.FMBC.2025.8,
  author =	{Mari\'{c}, Filip and Scholz, Bernhard and Suboti\'{c}, Pavle},
  title =	{{Formal Verification of a Fail-Safe Cross-Chain Bridge}},
  booktitle =	{6th International Workshop on Formal Methods for Blockchains (FMBC 2025)},
  pages =	{8:1--8:18},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-371-3},
  ISSN =	{2190-6807},
  year =	{2025},
  volume =	{129},
  editor =	{Marmsoler, Diego and Xu, Meng},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2025.8},
  URN =		{urn:nbn:de:0030-drops-230342},
  doi =		{10.4230/OASIcs.FMBC.2025.8},
  annote =	{Keywords: Cross-Chain Bridge, Formal Verification, Logic, Security}
}
Document
Short Paper
DOI: 10.4230/OASIcs.FMBC.2021.3
Using Coq to Enforce the Checks-Effects-Interactions Pattern in DeepSEA Smart Contracts (Short Paper)

Authors: Daniel Britten, Vilhelm Sjöberg, and Steve Reeves

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

Abstract
Using the DeepSEA system for smart contract proofs, this paper investigates how to use the Coq theorem prover to enforce that smart contracts follow the Checks-Effects-Interactions Pattern. This pattern is widely understood to mitigate the risks associated with reentrancy. The infamous "The DAO" exploit is an example of the risks of not following the Checks-Effects-Interactions Pattern. It resulted in the loss of over 50 million USD and involved reentrancy - the exploit used would not have been possible if the Checks-Effects-Interactions Pattern had been followed. Remix IDE, for example, already has a tool to check that the Checks-Effects-Interactions Pattern has been followed as part of the Solidity Static Analysis module which is available as a plugin. However, aside from simply replicating the Remix IDE feature, implementing a Checks-Effects-Interactions Pattern checker in the proof assistant Coq also allows us to use the proofs, which are generated in the process, in other proofs related to the smart contract. As an example of this, we will demonstrate an idea for how the modelling of Ether transfer can be simplified by using automatically generated proofs of the property that each smart contract function will call the Ether transfer method at most once (excluding any calls related to invoking other smart contracts). This property is a consequence of following a strict version of the Checks-Effects-Interactions Pattern as given in this paper.
Cite as

Daniel Britten, Vilhelm Sjöberg, and Steve Reeves. Using Coq to Enforce the Checks-Effects-Interactions Pattern in DeepSEA Smart Contracts (Short Paper). In 3rd International Workshop on Formal Methods for Blockchains (FMBC 2021). Open Access Series in Informatics (OASIcs), Volume 95, pp. 3:1-3:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{britten_et_al:OASIcs.FMBC.2021.3,
  author =	{Britten, Daniel and Sj\"{o}berg, Vilhelm and Reeves, Steve},
  title =	{{Using Coq to Enforce the Checks-Effects-Interactions Pattern in DeepSEA Smart Contracts}},
  booktitle =	{3rd International Workshop on Formal Methods for Blockchains (FMBC 2021)},
  pages =	{3:1--3:8},
  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.3},
  URN =		{urn:nbn:de:0030-drops-154272},
  doi =		{10.4230/OASIcs.FMBC.2021.3},
  annote =	{Keywords: smart contracts, formal methods, blockchain}
}
  • Refine by Type
  • 3 Document/PDF
  • 2 Document/HTML

  • Refine by Publication Year
  • 2 2025
  • 1 2021

  • Refine by Author
  • 1 Britten, Daniel
  • 1 Cauchard, Jessica R.
  • 1 Marić, Filip
  • 1 Reeves, Steve
  • 1 Scholz, Bernhard
  • Show More...

  • Refine by Series/Journal
  • 3 OASIcs

  • Refine by Classification
  • 1 Computer systems organization → Distributed architectures
  • 1 Computer systems organization → External interfaces for robotics
  • 1 Human-centered computing → HCI theory, concepts and models
  • 1 Human-centered computing → Interaction paradigms
  • 1 Security and privacy → Logic and verification
  • Show More...

  • Refine by Keyword
  • 1 Cross-Chain Bridge
  • 1 Formal Verification
  • 1 Logic
  • 1 Security
  • 1 blockchain
  • 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