83 Search Results for "Zhang, Simon"

Document
DOI: 10.4230/LIPIcs.ECOOP.2024.1
A Sound Type System for Secure Currency Flow

Authors: Luca Aceto, Daniele Gorla, and Stian Lybech

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

Abstract
In this paper we focus on TinySol, a minimal calculus for Solidity smart contracts, introduced by Bartoletti et al. We start by rephrasing its syntax (to emphasise its object-oriented flavour) and give a new big-step operational semantics. We then use it to define two security properties, namely call integrity and noninterference. These two properties have some similarities in their definition, in that they both require that some part of a program is not influenced by the other part. However, we show that the two properties are actually incomparable. Nevertheless, we provide a type system for noninterference and show that well-typed programs satisfy call integrity as well; hence, programs that are accepted by our type system satisfy both properties. We finally discuss the practical usability of the type system and its limitations by means of some simple examples.
Cite as

Luca Aceto, Daniele Gorla, and Stian Lybech. A Sound Type System for Secure Currency Flow. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 1:1-1:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{aceto_et_al:LIPIcs.ECOOP.2024.1,
  author =	{Aceto, Luca and Gorla, Daniele and Lybech, Stian},
  title =	{{A Sound Type System for Secure Currency Flow}},
  booktitle =	{38th European Conference on Object-Oriented Programming (ECOOP 2024)},
  pages =	{1:1--1:27},
  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.1},
  URN =		{urn:nbn:de:0030-drops-208508},
  doi =		{10.4230/LIPIcs.ECOOP.2024.1},
  annote =	{Keywords: smart contracts, call integrity, noninterference, type system}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2024.2
Runtime Instrumentation for Reactive Components

Authors: Luca Aceto, Duncan Paul Attard, Adrian Francalanza, and Anna Ingólfsdóttir

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

Abstract
Reactive software calls for instrumentation methods that uphold the reactive attributes of systems. Runtime verification imposes another demand on the instrumentation, namely that the trace event sequences it reports to monitors are sound - that is, they reflect actual executions of the system under scrutiny. This paper presents RIARC, a novel decentralised instrumentation algorithm for outline monitors meeting these two demands. Asynchrony in reactive software complicates the instrumentation due to potential trace event loss or reordering. RIARC overcomes these challenges using a next-hop IP routing approach to rearrange and report events soundly to monitors. RIARC is validated in two ways. We subject its corresponding implementation to rigorous systematic testing to confirm its correctness. In addition, we assess this implementation via extensive empirical experiments, subjecting it to large realistic workloads to ascertain its reactiveness. Our results show that RIARC optimises its memory and scheduler usage to maintain latency feasible for soft real-time applications. We also compare RIARC to inline and centralised monitoring, revealing that it induces comparable latency to inline monitoring in moderate concurrency settings where software performs long-running, computationally-intensive tasks, such as in Big Data stream processing.
Cite as

Luca Aceto, Duncan Paul Attard, Adrian Francalanza, and Anna Ingólfsdóttir. Runtime Instrumentation for Reactive Components. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 2:1-2:33, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{aceto_et_al:LIPIcs.ECOOP.2024.2,
  author =	{Aceto, Luca and Attard, Duncan Paul and Francalanza, Adrian and Ing\'{o}lfsd\'{o}ttir, Anna},
  title =	{{Runtime Instrumentation for Reactive Components}},
  booktitle =	{38th European Conference on Object-Oriented Programming (ECOOP 2024)},
  pages =	{2:1--2:33},
  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.2},
  URN =		{urn:nbn:de:0030-drops-208511},
  doi =		{10.4230/LIPIcs.ECOOP.2024.2},
  annote =	{Keywords: Runtime instrumentation, decentralised monitoring, reactive systems}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2024.15
Rose: Composable Autodiff for the Interactive Web

Authors: Sam Estep, Wode Ni, Raven Rothkopf, and Joshua Sunshine

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

Abstract
Reverse-mode automatic differentiation (autodiff) has been popularized by deep learning, but its ability to compute gradients is also valuable for interactive use cases such as bidirectional computer-aided design, embedded physics simulations, visualizing causal inference, and more. Unfortunately, the web is ill-served by existing autodiff frameworks, which use autodiff strategies that perform poorly on dynamic scalar programs, and pull in heavy dependencies that would result in unacceptable webpage sizes. This work introduces Rose, a lightweight autodiff framework for the web using a new hybrid approach to reverse-mode autodiff, blending conventional tracing and transformation techniques in a way that uses the host language for metaprogramming while also allowing the programmer to explicitly define reusable functions that comprise a larger differentiable computation. We demonstrate the value of the Rose design by porting two differentiable physics simulations, and evaluate its performance on an optimization-based diagramming application, showing Rose outperforming the state-of-the-art in web-based autodiff by multiple orders of magnitude.
Cite as

Sam Estep, Wode Ni, Raven Rothkopf, and Joshua Sunshine. Rose: Composable Autodiff for the Interactive Web. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 15:1-15:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{estep_et_al:LIPIcs.ECOOP.2024.15,
  author =	{Estep, Sam and Ni, Wode and Rothkopf, Raven and Sunshine, Joshua},
  title =	{{Rose: Composable Autodiff for the Interactive Web}},
  booktitle =	{38th European Conference on Object-Oriented Programming (ECOOP 2024)},
  pages =	{15:1--15:27},
  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.15},
  URN =		{urn:nbn:de:0030-drops-208642},
  doi =		{10.4230/LIPIcs.ECOOP.2024.15},
  annote =	{Keywords: Automatic differentiation, differentiable programming, compilers, web}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2024.19
Fearless Asynchronous Communications with Timed Multiparty Session Protocols

Authors: Ping Hou, Nicolas Lagaillardie, and Nobuko Yoshida

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

Abstract
Session types using affinity and exception handling mechanisms have been developed to ensure the communication safety of protocols implemented in concurrent and distributed programming languages. Nevertheless, current affine session types are inadequate for specifying real-world asynchronous protocols, as they are usually imposed by time constraints which enable timeout exceptions to prevent indefinite blocking while awaiting valid messages. This paper proposes the first formal integration of affinity, time constraints, timeouts, and time-failure handling based on multiparty session types for supporting reliability in asynchronous distributed systems. With this theory, we statically guarantee that asynchronous timed communication is deadlock-free, communication safe, while being fearless - never hindered by timeout errors or abrupt terminations. To implement our theory, we introduce MultiCrusty^T, a Rust toolchain designed to facilitate the implementation of safe affine timed protocols. MultiCrusty^T leverages generic types and the time library to handle timed communications, integrated with optional types for affinity. We evaluate MultiCrusty^T by extending diverse examples from the literature to incorporate time and timeouts. We also showcase the correctness by construction of our approach by implementing various real-world use cases, including protocols from the Internet of Remote Things domain and real-time systems.
Cite as

Ping Hou, Nicolas Lagaillardie, and Nobuko Yoshida. Fearless Asynchronous Communications with Timed Multiparty Session Protocols. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 19:1-19:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{hou_et_al:LIPIcs.ECOOP.2024.19,
  author =	{Hou, Ping and Lagaillardie, Nicolas and Yoshida, Nobuko},
  title =	{{Fearless Asynchronous Communications with Timed Multiparty Session Protocols}},
  booktitle =	{38th European Conference on Object-Oriented Programming (ECOOP 2024)},
  pages =	{19:1--19:30},
  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.19},
  URN =		{urn:nbn:de:0030-drops-208681},
  doi =		{10.4230/LIPIcs.ECOOP.2024.19},
  annote =	{Keywords: Session Types, Concurrency, Time Failure Handling, Affinity, Timeout, Rust}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2024.20
Taking a Closer Look: An Outlier-Driven Approach to Compilation-Time Optimization

Authors: Florian Huemer, David Leopoldseder, Aleksandar Prokopec, Raphael Mosaner, and Hanspeter Mössenböck

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

Abstract
Improving compilation time in optimizing compilers is challenging due to their large number of interconnected components. This includes compiler optimizations, compiler tiers, heuristics, and profiling information. Despite this complexity, research in compilation-time optimization is often guided by analyzing metrics of entire program runs, such as the total compilation time and overall memory footprint. This coarse-grained perspective hides relevant information, such as source program functions for which the compiler allocates a lot of memory or compiler optimizations with a high impact on the total compilation time. This leaves high-level metrics as the only reference point for driving optimization design. Consequently, compilation-time regressions in one program function that are obscured by improvements in other functions stay undetected, while the impacts of compiler changes on untouched parts of the compiler are mainly unknown. Furthermore, developers overlook long-standing compiler defects because their high-level metrics do not change over time. To address these limitations, we propose ICON, a new data-driven approach to compilation-time optimization that breaks up high-level metrics into individual source program functions, compiler optimizations, or even into individual instructions in the compiler source code. Our methodology enables an iterative in-depth compilation-time analysis, focusing on outliers to identify optimization opportunities. We show that outliers, both in terms of time spent in a particular compiler optimization, and in terms of individual compilations that take substantially longer, can reveal potential problems in the compiler implementation. We applied our approach to GraalVM and extracted data for multiple of its language runtimes. We analyzed the resulting data, present the first detailed look into the distribution of compilation time in the GraalVM compiler, a state-of-the-art multi-language compiler, and identified defects that led to regressions in overall compilation time or the compilation time of specific languages. We furthermore designed two optimizations based on the identified outliers that improve compilation time between 2.25% and 9.45%. We believe that our approach can guide compiler developers in finding usually overlooked optimization potential and defects, and focus future research efforts in making compilers more efficient.
Cite as

Florian Huemer, David Leopoldseder, Aleksandar Prokopec, Raphael Mosaner, and Hanspeter Mössenböck. Taking a Closer Look: An Outlier-Driven Approach to Compilation-Time Optimization. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 20:1-20:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{huemer_et_al:LIPIcs.ECOOP.2024.20,
  author =	{Huemer, Florian and Leopoldseder, David and Prokopec, Aleksandar and Mosaner, Raphael and M\"{o}ssenb\"{o}ck, Hanspeter},
  title =	{{Taking a Closer Look: An Outlier-Driven Approach to Compilation-Time Optimization}},
  booktitle =	{38th European Conference on Object-Oriented Programming (ECOOP 2024)},
  pages =	{20:1--20:28},
  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.20},
  URN =		{urn:nbn:de:0030-drops-208693},
  doi =		{10.4230/LIPIcs.ECOOP.2024.20},
  annote =	{Keywords: Compilation time, outliers, dynamic languages, virtual machines, GraalVM, ICON}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2024.23
InferType: A Compiler Toolkit for Implementing Efficient Constraint-Based Type Inference

Authors: Senxi Li, Tetsuro Yamazaki, and Shigeru Chiba

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

Abstract
Supporting automatic type inference is in demand in modern language development. It is a challenging task but without appropriate supporting toolkits. This paper presents InferType, a Java library that helps implement constraint-based type inference. A compiler writer uses InferType’s classes and methods to describe type constraints and typing rules for type inference. InferType then performs constraint solving by translation to the Z3 SMT solver. InferType is equipped with our developed optimization technique. It reduces the search space for type variables by pre-computing the structures of those type variables for mitigating the performance bottleneck of constraint solving with deeply nested types. We use InferType to implement type inference for a subset of Python, and conduct experiments to evaluate how the developed optimization technique can affect the performance of type inference. Our results show that InferType’s optimization can greatly mitigate the performance bottleneck for programs with deeply nested types, and can potentially improve the performance for large nested types.
Cite as

Senxi Li, Tetsuro Yamazaki, and Shigeru Chiba. InferType: A Compiler Toolkit for Implementing Efficient Constraint-Based Type Inference. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 23:1-23:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{li_et_al:LIPIcs.ECOOP.2024.23,
  author =	{Li, Senxi and Yamazaki, Tetsuro and Chiba, Shigeru},
  title =	{{InferType: A Compiler Toolkit for Implementing Efficient Constraint-Based Type Inference}},
  booktitle =	{38th European Conference on Object-Oriented Programming (ECOOP 2024)},
  pages =	{23:1--23:28},
  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.23},
  URN =		{urn:nbn:de:0030-drops-208728},
  doi =		{10.4230/LIPIcs.ECOOP.2024.23},
  annote =	{Keywords: Domain Specific Languages, Compilation, Static Analysis, Type Inference, Constraint Solving, SMT Solver}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2024.39
Formalizing, Mechanizing, and Verifying Class-Based Refinement Types

Authors: Ke Sun, Di Wang, Sheng Chen, Meng Wang, and Dan Hao

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

Abstract
Refinement types have been extensively used in class-based languages to specify and verify fine-grained logical specifications. Despite the advances in practical aspects such as applicability and usability, two fundamental issues persist. First, the soundness of existing class-based refinement type systems is inadequately explored, casting doubts on their reliability. Second, the expressiveness of existing systems is limited, restricting the depiction of semantic properties related to object-oriented constructs. This work tackles these issues through a systematic framework. We formalize a declarative class-based refinement type calculus (named RFJ), that is expressive and concise. We rigorously develop the soundness meta-theory of this calculus, followed by its mechanization in Coq. Finally, to ensure the calculus’s verifiability, we propose an algorithmic verification approach based on a fragment of first-order logic (named LFJ), and implement this approach as a type checker.
Cite as

Ke Sun, Di Wang, Sheng Chen, Meng Wang, and Dan Hao. Formalizing, Mechanizing, and Verifying Class-Based Refinement Types. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 39:1-39:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{sun_et_al:LIPIcs.ECOOP.2024.39,
  author =	{Sun, Ke and Wang, Di and Chen, Sheng and Wang, Meng and Hao, Dan},
  title =	{{Formalizing, Mechanizing, and Verifying Class-Based Refinement Types}},
  booktitle =	{38th European Conference on Object-Oriented Programming (ECOOP 2024)},
  pages =	{39:1--39:30},
  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.39},
  URN =		{urn:nbn:de:0030-drops-208881},
  doi =		{10.4230/LIPIcs.ECOOP.2024.39},
  annote =	{Keywords: Refinement Types, Program Verification, Object-oriented Programming}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2024.41
Refinements for Multiparty Message-Passing Protocols: Specification-Agnostic Theory and Implementation

Authors: Martin Vassor and Nobuko Yoshida

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

Abstract
Multiparty message-passing protocols are notoriously difficult to design, due to interaction mismatches that lead to errors such as deadlocks. Existing protocol specification formats have been developed to prevent such errors (e.g. multiparty session types (MPST)). In order to further constrain protocols, specifications can be extended with refinements, i.e. logical predicates to control the behaviour of the protocol based on previous values exchanged. Unfortunately, existing refinement theories and implementations are tightly coupled with specification formats. This paper proposes a framework for multiparty message-passing protocols with refinements and its implementation in Rust. Our work decouples correctness of refinements from the underlying model of computation, which results in a specification-agnostic framework. Our contributions are threefold. First, we introduce a trace system which characterises valid refined traces, i.e. a sequence of sending and receiving actions correct with respect to refinements. Second, we give a correct model of computation named refined communicating system (RCS), which is an extension of communicating automata systems with refinements. We prove that RCS only produce valid refined traces. We show how to generate RCS from mainstream protocol specification formats, such as refined multiparty session types (RMPST) or refined choreography automata. Third, we illustrate the flexibility of the framework by developing both a static analysis technique and an improved model of computation for dynamic refinement evaluation. Finally, we provide a Rust toolchain for decentralised RMPST, evaluate our implementation with a set of benchmarks from the literature, and observe that refinement overhead is negligible.
Cite as

Martin Vassor and Nobuko Yoshida. Refinements for Multiparty Message-Passing Protocols: Specification-Agnostic Theory and Implementation. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 41:1-41:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{vassor_et_al:LIPIcs.ECOOP.2024.41,
  author =	{Vassor, Martin and Yoshida, Nobuko},
  title =	{{Refinements for Multiparty Message-Passing Protocols: Specification-Agnostic Theory and Implementation}},
  booktitle =	{38th European Conference on Object-Oriented Programming (ECOOP 2024)},
  pages =	{41:1--41:29},
  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.41},
  URN =		{urn:nbn:de:0030-drops-208906},
  doi =		{10.4230/LIPIcs.ECOOP.2024.41},
  annote =	{Keywords: Message-Passing Concurrency, Session Types, Specification}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2024.42
Failure Transparency in Stateful Dataflow Systems

Authors: Aleksey Veresov, Jonas Spenger, Paris Carbone, and Philipp Haller

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

Abstract
Failure transparency enables users to reason about distributed systems at a higher level of abstraction, where complex failure-handling logic is hidden. This is especially true for stateful dataflow systems, which are the backbone of many cloud applications. In particular, this paper focuses on proving failure transparency in Apache Flink, a popular stateful dataflow system. Even though failure transparency is a critical aspect of Apache Flink, to date it has not been formally proven. Showing that the failure transparency mechanism is correct, however, is challenging due to the complexity of the mechanism itself. Nevertheless, this complexity can be effectively hidden behind a failure transparent programming interface. To show that Apache Flink is failure transparent, we model it in small-step operational semantics. Next, we provide a novel definition of failure transparency based on observational explainability, a concept which relates executions according to their observations. Finally, we provide a formal proof of failure transparency for the implementation model; i.e., we prove that the failure-free model correctly abstracts from the failure-related details of the implementation model. We also show liveness of the implementation model under a fair execution assumption. These results are a first step towards a verified stack for stateful dataflow systems.
Cite as

Aleksey Veresov, Jonas Spenger, Paris Carbone, and Philipp Haller. Failure Transparency in Stateful Dataflow Systems. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 42:1-42:31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{veresov_et_al:LIPIcs.ECOOP.2024.42,
  author =	{Veresov, Aleksey and Spenger, Jonas and Carbone, Paris and Haller, Philipp},
  title =	{{Failure Transparency in Stateful Dataflow Systems}},
  booktitle =	{38th European Conference on Object-Oriented Programming (ECOOP 2024)},
  pages =	{42:1--42:31},
  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.42},
  URN =		{urn:nbn:de:0030-drops-208911},
  doi =		{10.4230/LIPIcs.ECOOP.2024.42},
  annote =	{Keywords: Failure transparency, stateful dataflow, operational semantics, checkpoint recovery}
}
Document
DOI: 10.4230/LIPIcs.DNA.30.1
Geometric Enumeration of Localized DNA Strand Displacement Reaction Networks

Authors: Matthew R. Lakin and Sarika Kumar

Published in: LIPIcs, Volume 314, 30th International Conference on DNA Computing and Molecular Programming (DNA 30) (2024)

Abstract
Localized molecular devices are a powerful tool for engineering complex information-processing circuits and molecular robots. Their practical advantages include speed and scalability of interactions between components tethered near to each other on an underlying nanostructure, and the ability to restrict interactions between more distant components. The latter is a critical feature that must be factored into computational tools for the design and simulation of localized molecular devices: unlike in solution-phase systems, the geometries of molecular interactions must be accounted for when attempting to determine the network of possible reactions in a tethered molecular system. This work aims to address that challenge by integrating, for the first time, automated approaches to analysis of molecular geometry with reaction enumeration algorithms for DNA strand displacement reaction networks that can be applied to tethered molecular systems. By adapting a simple approach to solving the biophysical constraints inherent in molecular interactions to be applicable to tethered systems, we produce a localized reaction enumeration system that enhances previous approaches to reaction enumeration in tethered system by not requiring users to explicitly specify the subsets of components that are capable of interacting. This greatly simplifies the user’s task and could also be used as the basis of future systems for automated placement or routing of signal-transmission and logical processing in molecular devices. We apply this system to several published example systems from the literature, including both tethered molecular logic systems and molecular robots.
Cite as

Matthew R. Lakin and Sarika Kumar. Geometric Enumeration of Localized DNA Strand Displacement Reaction Networks. In 30th International Conference on DNA Computing and Molecular Programming (DNA 30). Leibniz International Proceedings in Informatics (LIPIcs), Volume 314, pp. 1:1-1:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{lakin_et_al:LIPIcs.DNA.30.1,
  author =	{Lakin, Matthew R. and Kumar, Sarika},
  title =	{{Geometric Enumeration of Localized DNA Strand Displacement Reaction Networks}},
  booktitle =	{30th International Conference on DNA Computing and Molecular Programming (DNA 30)},
  pages =	{1:1--1:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-344-7},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{314},
  editor =	{Seki, Shinnosuke and Stewart, Jaimie Marie},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DNA.30.1},
  URN =		{urn:nbn:de:0030-drops-209294},
  doi =		{10.4230/LIPIcs.DNA.30.1},
  annote =	{Keywords: Localized circuits, reaction enumeration, DNA strand displacement, geometry, molecular computing}
}
Document
DOI: 10.4230/LIPIcs.COSIT.2024.1
Wayfinding Stages: The Role of Familiarity, Gaze Events, and Visual Attention

Authors: Negar Alinaghi and Ioannis Giannopoulos

Published in: LIPIcs, Volume 315, 16th International Conference on Spatial Information Theory (COSIT 2024)

Abstract
Understanding the cognitive processes involved in wayfinding is crucial for both theoretical advances and practical applications in navigation systems development. This study explores how gaze behavior and visual attention contribute to our understanding of cognitive states during wayfinding. Based on the model proposed by Downs and Stea, which segments wayfinding into four distinct stages: self-localization, route planning, monitoring, and goal recognition, we conducted an outdoor wayfinding experiment with 56 participants. Given the significant role of spatial familiarity in wayfinding behavior, each participant navigated six different routes in both familiar and unfamiliar environments, with their eye movements being recorded. We provide a detailed examination of participants' gaze behavior and the actual objects of focus. Our findings reveal distinct gaze behavior patterns and visual attention, differentiating wayfinding stages while emphasizing the impact of spatial familiarity. This examination of visual engagement during wayfinding explains adaptive cognitive processes, demonstrating how familiarity influences navigation strategies. The results enhance our theoretical understanding of wayfinding and offer practical insights for developing navigation aids capable of predicting different wayfinding stages.
Cite as

Negar Alinaghi and Ioannis Giannopoulos. Wayfinding Stages: The Role of Familiarity, Gaze Events, and Visual Attention. In 16th International Conference on Spatial Information Theory (COSIT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 315, pp. 1:1-1:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{alinaghi_et_al:LIPIcs.COSIT.2024.1,
  author =	{Alinaghi, Negar and Giannopoulos, Ioannis},
  title =	{{Wayfinding Stages: The Role of Familiarity, Gaze Events, and Visual Attention}},
  booktitle =	{16th International Conference on Spatial Information Theory (COSIT 2024)},
  pages =	{1:1--1:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-330-0},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{315},
  editor =	{Adams, Benjamin and Griffin, Amy L. and Scheider, Simon and McKenzie, Grant},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.COSIT.2024.1},
  URN =		{urn:nbn:de:0030-drops-208161},
  doi =		{10.4230/LIPIcs.COSIT.2024.1},
  annote =	{Keywords: Eye-tracking, Wayfinding, Spatial Familiarity, Visual Attention, Gaze Behavior}
}
Document
DOI: 10.4230/LIPIcs.COSIT.2024.2
A Salience-Based Framework for Terrain Modelling: From the Surface Network to Topo-Contexts

Authors: Éric Guilbert and Bernard Moulin

Published in: LIPIcs, Volume 315, 16th International Conference on Spatial Information Theory (COSIT 2024)

Abstract
Twenty years after Mark and Smith’s seminal paper, a Science of Topography, we revisit some of their fundamental questions about how landforms are recognised by people and how they can be automatically extracted or delimited from representations of topographic surfaces. Many approaches and tools, essentially based on GeoOBIA, can extract objects associated with landforms from image data. But, they cannot relate these objects to the topology and topography of the terrain. Yet, geo-scientists can easily recognise landforms, considering terrain characteristics and other factors composing the context of appearance of those landforms. Revisiting Gestalt Theory, we propose a salience-based approach fostering a holistic view of the terrain which fits with the geoscientists' ability to recognise landforms using the topographic and hydrologic contexts. The terrain is represented as an extended surface network (ESN), a graph composed of elementary saliences (peaks, pits, saddles, thalweg and ridge networks) and obtained from raster data. The ESN combines both the surface and the drainage networks in a sound topological representation of the terrain. A skeletonisation technique of the ESN’s thalweg and ridge networks is proposed to geometrically and topologically characterise landforms, as well as ensembles of landforms. On this basis and to represent the context of appearance of landforms, geo/topo-contexts are introduced as structures grounded in the properties of the ESN and using the skeletonisation technique. We give an illustration of how a geomorphologist can apply our approach and tools, using the depressions and drainage basins as examples of useful geo/topo-contexts.
Cite as

Éric Guilbert and Bernard Moulin. A Salience-Based Framework for Terrain Modelling: From the Surface Network to Topo-Contexts. In 16th International Conference on Spatial Information Theory (COSIT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 315, pp. 2:1-2:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{guilbert_et_al:LIPIcs.COSIT.2024.2,
  author =	{Guilbert, \'{E}ric and Moulin, Bernard},
  title =	{{A Salience-Based Framework for Terrain Modelling: From the Surface Network to Topo-Contexts}},
  booktitle =	{16th International Conference on Spatial Information Theory (COSIT 2024)},
  pages =	{2:1--2:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-330-0},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{315},
  editor =	{Adams, Benjamin and Griffin, Amy L. and Scheider, Simon and McKenzie, Grant},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.COSIT.2024.2},
  URN =		{urn:nbn:de:0030-drops-208177},
  doi =		{10.4230/LIPIcs.COSIT.2024.2},
  annote =	{Keywords: DTM, surface network, landform, topographic context, saliences}
}
Document
DOI: 10.4230/LIPIcs.COSIT.2024.5
Spatial Nudging: Converging Persuasive Technologies, Spatial Design, and Behavioral Theories

Authors: Ayda Grisiute and Martin Raubal

Published in: LIPIcs, Volume 315, 16th International Conference on Spatial Information Theory (COSIT 2024)

Abstract
This paper presents the Spatial Nudging framework - a theory-based framework that maps out nudging strategies in the mobility domain and refines its existing definitions. We link these strategies by highlighting the role of perceived affordances across physical and digital interventions based on the Nudge Theory and the Theory of Affordances. Furthermore, we propose to use graph representation techniques as a supportive methodology to better align perceived and actual environments, thereby enhancing the intervention strategies' effectiveness. We illustrate the applicability of the Spatial Nudging framework and the supportive methodology in the context of an E-bike City vision. This paper lays the foundation for future research on theoretically integrating physical and digital interventions to promote sustainable mobility.
Cite as

Ayda Grisiute and Martin Raubal. Spatial Nudging: Converging Persuasive Technologies, Spatial Design, and Behavioral Theories. In 16th International Conference on Spatial Information Theory (COSIT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 315, pp. 5:1-5:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{grisiute_et_al:LIPIcs.COSIT.2024.5,
  author =	{Grisiute, Ayda and Raubal, Martin},
  title =	{{Spatial Nudging: Converging Persuasive Technologies, Spatial Design, and Behavioral Theories}},
  booktitle =	{16th International Conference on Spatial Information Theory (COSIT 2024)},
  pages =	{5:1--5:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-330-0},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{315},
  editor =	{Adams, Benjamin and Griffin, Amy L. and Scheider, Simon and McKenzie, Grant},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.COSIT.2024.5},
  URN =		{urn:nbn:de:0030-drops-208206},
  doi =		{10.4230/LIPIcs.COSIT.2024.5},
  annote =	{Keywords: spatial nudging, active mobility, Nudge Theory, Theory of Affordances, cognitive graphs}
}
Document
DOI: 10.4230/LIPIcs.COSIT.2024.6
Is Familiarity Reflected in the Spatial Knowledge Revealed by Sketch Maps?

Authors: Markus Kattenbeck, Daniel R. Montello, Martin Raubal, and Ioannis Giannopoulos

Published in: LIPIcs, Volume 315, 16th International Conference on Spatial Information Theory (COSIT 2024)

Abstract
Despite the frequent use of sketch maps in assessing environmental knowledge, it remains unclear how and to what degree familiarity impacts sketch map content. In the present study, we assess whether different levels of familiarity relate to differences in the content and spatial accuracy of environmental knowledge depicted in sketch maps drawn for the purpose of route instructions. To this end, we conduct a real-world wayfinding study with 91 participants, all of whom have to walk along a pre-defined route of approximately 2.3km length. Prior to the walk, we collect self-report familiarity ratings from participants for both a set of 15 landmarks and a set of areas we define as hexagons along the route. Once participants finished walking the route, they were asked to sketch a map of the route, specifically a sketch that would enable a person who had never walked the route to follow it. We found that participants unfamiliar with the areas along the route sketched fewer features than familiar people did. Contrary to our expectations, however, we found that landmarks were sketched or not regardless of participants' level of familiarity with the landmarks. We were also surprised that the level of familiarity was not correlated to the accuracy of the sketched order of features along the route, of the position of sketched features in relation to the route, nor to the metric locational accuracy of feature placement on the sketches. These results lead us to conclude that different aspects of feature salience influence whether the features are included on sketch maps, independent of familiarity. They also point to the influence of task context on the content of sketch maps, again independent of familiarity. We propose further studies to more fully explore these ideas.
Cite as

Markus Kattenbeck, Daniel R. Montello, Martin Raubal, and Ioannis Giannopoulos. Is Familiarity Reflected in the Spatial Knowledge Revealed by Sketch Maps?. In 16th International Conference on Spatial Information Theory (COSIT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 315, pp. 6:1-6:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{kattenbeck_et_al:LIPIcs.COSIT.2024.6,
  author =	{Kattenbeck, Markus and Montello, Daniel R. and Raubal, Martin and Giannopoulos, Ioannis},
  title =	{{Is Familiarity Reflected in the Spatial Knowledge Revealed by Sketch Maps?}},
  booktitle =	{16th International Conference on Spatial Information Theory (COSIT 2024)},
  pages =	{6:1--6:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-330-0},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{315},
  editor =	{Adams, Benjamin and Griffin, Amy L. and Scheider, Simon and McKenzie, Grant},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.COSIT.2024.6},
  URN =		{urn:nbn:de:0030-drops-208215},
  doi =		{10.4230/LIPIcs.COSIT.2024.6},
  annote =	{Keywords: Familiarity, Spatial Knowledge, Sketch Maps}
}
Document
DOI: 10.4230/LIPIcs.COSIT.2024.11
Semantic Perspectives on the Lake District Writing: Spatial Ontology Modeling and Relation Extraction for Deeper Insights

Authors: Erum Haris, Anthony G. Cohn, and John G. Stell

Published in: LIPIcs, Volume 315, 16th International Conference on Spatial Information Theory (COSIT 2024)

Abstract
Extracting spatial details from historical texts can be difficult, hindering our understanding of past landscapes. The study addresses this challenge by analyzing the Corpus of the Lake District Writing, focusing on the English Lake District region. We systematically link the theoretical notions from the core concepts of spatial information to provide basis for the problem domain. The conceptual foundation is further complemented with a spatial ontology and a custom gazetteer, allowing a formal and insightful semantic exploration of the massive unstructured corpus. The other contrasting side of the framework is the usage of LLMs for spatial relation extraction. We formulate prompts leveraging understanding of the LLMs of the intended task, curate a list of spatial relations representing the most recurring proximity or vicinity relations terms and extract semantic triples for the top five place names appearing in the corpus. We compare the extraction capabilities of three benchmark LLMs for a scholarly significant historical archive, representing their potential in a challenging and interdisciplinary research problem. Finally, the network comprising the semantic triples is enhanced by incorporating a gazetteer-based classification of the objects involved thus improving their spatial profiling.
Cite as

Erum Haris, Anthony G. Cohn, and John G. Stell. Semantic Perspectives on the Lake District Writing: Spatial Ontology Modeling and Relation Extraction for Deeper Insights. In 16th International Conference on Spatial Information Theory (COSIT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 315, pp. 11:1-11:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{haris_et_al:LIPIcs.COSIT.2024.11,
  author =	{Haris, Erum and Cohn, Anthony G. and Stell, John G.},
  title =	{{Semantic Perspectives on the Lake District Writing: Spatial Ontology Modeling and Relation Extraction for Deeper Insights}},
  booktitle =	{16th International Conference on Spatial Information Theory (COSIT 2024)},
  pages =	{11:1--11:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-330-0},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{315},
  editor =	{Adams, Benjamin and Griffin, Amy L. and Scheider, Simon and McKenzie, Grant},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.COSIT.2024.11},
  URN =		{urn:nbn:de:0030-drops-208268},
  doi =		{10.4230/LIPIcs.COSIT.2024.11},
  annote =	{Keywords: spatial humanities, spatial narratives, ontology, large language models}
}
  • Refine by Author
  • 2 Aceto, Luca
  • 2 Fleury, Mathias
  • 2 Giannopoulos, Ioannis
  • 2 Guns, Tias
  • 2 Li, Chu-Min
  • Show More...

  • Refine by Classification
  • 6 Software and its engineering → Compilers
  • 5 Theory of computation → Constraint and logic programming
  • 4 Computing methodologies → Artificial intelligence
  • 4 Computing methodologies → Knowledge representation and reasoning
  • 4 Theory of computation → Oracles and decision trees
  • Show More...

  • Refine by Keyword
  • 4 Large Language Models
  • 3 Scheduling
  • 2 CDCL
  • 2 Computational Complexity
  • 2 Concurrency
  • Show More...

  • Refine by Type
  • 83 document

  • Refine by Publication Year
  • 71 2024
  • 7 2023
  • 3 2020
  • 1 2019
  • 1 2021

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

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