37 Search Results for "Müller, Daniel"

Document
DOI: 10.4230/LIPIcs.AFT.2024.28
SoK: Attacks on DAOs

Authors: Rainer Feichtinger, Robin Fritsch, Lioba Heimbach, Yann Vonlanthen, and Roger Wattenhofer

Published in: LIPIcs, Volume 316, 6th Conference on Advances in Financial Technologies (AFT 2024)

Abstract
Decentralized Autonomous Organizations (DAOs) are blockchain-based organizations that facilitate decentralized governance. Today, DAOs not only hold billions of dollars in their treasury but also govern many of the most popular Decentralized Finance (DeFi) protocols. This paper systematically analyses security threats to DAOs, focusing on the types of attacks they face. We study attacks on DAOs that took place in the past, attacks that have been theorized to be possible, and potential attacks that were uncovered and prevented in audits. For each of these (potential) attacks, we describe and categorize the attack vectors utilized into four categories. This reveals that while many attacks on DAOs take advantage of the less tangible and more complex human nature involved in governance, audits tend to focus on code and protocol vulnerabilities. Thus, additionally, the paper examines empirical data on DAO vulnerabilities, outlines risk factors contributing to these attacks, and suggests mitigation strategies to safeguard against such vulnerabilities.
Cite as

Rainer Feichtinger, Robin Fritsch, Lioba Heimbach, Yann Vonlanthen, and Roger Wattenhofer. SoK: Attacks on DAOs. In 6th Conference on Advances in Financial Technologies (AFT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 316, pp. 28:1-28:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{feichtinger_et_al:LIPIcs.AFT.2024.28,
  author =	{Feichtinger, Rainer and Fritsch, Robin and Heimbach, Lioba and Vonlanthen, Yann and Wattenhofer, Roger},
  title =	{{SoK: Attacks on DAOs}},
  booktitle =	{6th Conference on Advances in Financial Technologies (AFT 2024)},
  pages =	{28:1--28:27},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-345-4},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{316},
  editor =	{B\"{o}hme, Rainer and Kiffer, Lucianna},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.AFT.2024.28},
  URN =		{urn:nbn:de:0030-drops-209640},
  doi =		{10.4230/LIPIcs.AFT.2024.28},
  annote =	{Keywords: blockchain, DAO, governance, security, measurements, voting systems}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2024.25
Compositional Symbolic Execution for Correctness and Incorrectness Reasoning

Authors: Andreas Lööw, Daniele Nantes-Sobrinho, Sacha-Élie Ayoun, Caroline Cronjäger, Petar Maksimović, and Philippa Gardner

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

Abstract
The introduction of separation logic has led to the development of symbolic execution techniques and tools that are (functionally) compositional with function specifications that can be used in broader calling contexts. Many of the compositional symbolic execution tools developed in academia and industry have been grounded on a formal foundation, but either the function specifications are not validated with respect to the underlying separation logic of the theory, or there is a large gulf between the theory and the implementation of the tool. We introduce a formal compositional symbolic execution engine which creates and uses function specifications from an underlying separation logic and provides a sound theoretical foundation for, and indeed was partially inspired by, the Gillian symbolic execution platform. This is achieved by providing an axiomatic interface which describes the properties of the consume and produce operations used in the engine to update compositionally the symbolic state, for example when calling function specifications. This consume-produce technique is used by VeriFast, Viper, and Gillian, but has not been previously characterised independently of the tool. As part of our result, we give consume and produce operations inspired by the Gillian implementation that satisfy the properties described by our axiomatic interface. A surprising property is that our engine semantics provides a common foundation for both correctness and incorrectness reasoning, with the difference in the underlying engine only amounting to the choice to use satisfiability or validity. We use this property to extend the Gillian platform, which previously only supported correctness reasoning, with incorrectness reasoning and automatic true bug-finding using incorrectness bi-abduction. We evaluate our new Gillian platform by using the Gillian instantiation to C. This instantiation is the first tool grounded on a common formal compositional symbolic execution engine to support both correctness and incorrectness reasoning.
Cite as

Andreas Lööw, Daniele Nantes-Sobrinho, Sacha-Élie Ayoun, Caroline Cronjäger, Petar Maksimović, and Philippa Gardner. Compositional Symbolic Execution for Correctness and Incorrectness Reasoning. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 25:1-25:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{loow_et_al:LIPIcs.ECOOP.2024.25,
  author =	{L\"{o}\"{o}w, Andreas and Nantes-Sobrinho, Daniele and Ayoun, Sacha-\'{E}lie and Cronj\"{a}ger, Caroline and Maksimovi\'{c}, Petar and Gardner, Philippa},
  title =	{{Compositional Symbolic Execution for Correctness and Incorrectness Reasoning}},
  booktitle =	{38th European Conference on Object-Oriented Programming (ECOOP 2024)},
  pages =	{25:1--25: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.25},
  URN =		{urn:nbn:de:0030-drops-208741},
  doi =		{10.4230/LIPIcs.ECOOP.2024.25},
  annote =	{Keywords: separation logic, incorrectness logic, symbolic execution, bi-abduction}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2024.26
Matching Plans for Frame Inference in Compositional Reasoning

Authors: Andreas Lööw, Daniele Nantes-Sobrinho, Sacha-Élie Ayoun, Petar Maksimović, and Philippa Gardner

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

Abstract
The use of function specifications to reason about function calls and the manipulation of user-defined predicates are two essential ingredients of modern compositional verification tools based on separation logic. To execute these operations successfully, these tools must be able to solve the frame inference problem, that is, to understand which parts of the state are relevant for the operation at hand. We introduce matching plans, a concept that is used in the Gillian verification platform to automate frame inference efficiently. We extract matching plans and their automation machinery from the Gillian implementation and present them in a tool-agnostic way, making the Gillian approach available to the broader verification community as a verification-tool design pattern.
Cite as

Andreas Lööw, Daniele Nantes-Sobrinho, Sacha-Élie Ayoun, Petar Maksimović, and Philippa Gardner. Matching Plans for Frame Inference in Compositional Reasoning. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 26:1-26:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{loow_et_al:LIPIcs.ECOOP.2024.26,
  author =	{L\"{o}\"{o}w, Andreas and Nantes-Sobrinho, Daniele and Ayoun, Sacha-\'{E}lie and Maksimovi\'{c}, Petar and Gardner, Philippa},
  title =	{{Matching Plans for Frame Inference in Compositional Reasoning}},
  booktitle =	{38th European Conference on Object-Oriented Programming (ECOOP 2024)},
  pages =	{26:1--26:20},
  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.26},
  URN =		{urn:nbn:de:0030-drops-208751},
  doi =		{10.4230/LIPIcs.ECOOP.2024.26},
  annote =	{Keywords: Compositional reasoning, separation logic, frame inference}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2024.34
Pipit on the Post: Proving Pre- and Post-Conditions of Reactive Systems

Authors: Amos Robinson and Alex Potanin

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

Abstract
Synchronous languages such as Lustre and Scade are used to implement safety-critical control systems; proving such programs correct and having the proved properties apply to the compiled code is therefore equally critical. We introduce Pipit, a small synchronous language embedded in F*, designed for verifying control systems and executing them in real-time. Pipit includes a verified translation to transition systems; by reusing F*’s existing proof automation, certain safety properties can be automatically proved by k-induction on the transition system. Pipit can also generate executable code in a subset of F* which is suitable for compilation and real-time execution on embedded devices. The executable code is deterministic and total and preserves the semantics of the original program.
Cite as

Amos Robinson and Alex Potanin. Pipit on the Post: Proving Pre- and Post-Conditions of Reactive Systems. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 34:1-34:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{robinson_et_al:LIPIcs.ECOOP.2024.34,
  author =	{Robinson, Amos and Potanin, Alex},
  title =	{{Pipit on the Post: Proving Pre- and Post-Conditions of Reactive Systems}},
  booktitle =	{38th European Conference on Object-Oriented Programming (ECOOP 2024)},
  pages =	{34:1--34: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.34},
  URN =		{urn:nbn:de:0030-drops-208836},
  doi =		{10.4230/LIPIcs.ECOOP.2024.34},
  annote =	{Keywords: Lustre, streaming, reactive, verification}
}
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.ECOOP.2024.47
Defining Name Accessibility Using Scope Graphs

Authors: Aron Zwaan and Casper Bach Poulsen

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

Abstract
Many programming languages allow programmers to regulate accessibility; i.e., annotating a declaration with keywords such as export and private to indicate where it can be accessed. Despite the importance of name accessibility for, e.g., compilers, editor auto-completion and tooling, and automated refactorings, few existing type systems provide a formal account of name accessibility. We present a declarative, executable, and language-parametric model for name accessibility, which provides a formal specification of name accessibility in Java, C#, C++, Rust, and Eiffel. We achieve this by defining name accessibility as a predicate on resolution paths through scope graphs. Since scope graphs are a language-independent model of name resolution, our model provides a uniform approach to defining different accessibility policies for different languages. Our model is implemented in Statix, a logic language for executable type system specification using scope graphs. We evaluate its correctness on a test suite that compares it with the C#, Java, and Rust compilers, and show we can synthesize access modifiers in programs with holes accurately.
Cite as

Aron Zwaan and Casper Bach Poulsen. Defining Name Accessibility Using Scope Graphs. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 47:1-47:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{zwaan_et_al:LIPIcs.ECOOP.2024.47,
  author =	{Zwaan, Aron and Bach Poulsen, Casper},
  title =	{{Defining Name Accessibility Using Scope Graphs}},
  booktitle =	{38th European Conference on Object-Oriented Programming (ECOOP 2024)},
  pages =	{47:1--47: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.47},
  URN =		{urn:nbn:de:0030-drops-208961},
  doi =		{10.4230/LIPIcs.ECOOP.2024.47},
  annote =	{Keywords: access modifier, visibility, scope graph, name resolution}
}
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.ITP.2024.23
A Generalised Union of Rely-Guarantee and Separation Logic Using Permission Algebras

Authors: Vincent Jackson, Toby Murray, and Christine Rizkallah

Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)

Abstract
This paper describes GenRGSep, an Isabelle/HOL library for the development of RGSep logics using a general algebraic state model. In particular, we develop an algebraic state models based on resource algebras that assume neither the presence of unit resources or the cancellativity law. If a new resource model is required, its components need only be proven an instance of a permission algebra, and then they can be composed together using tuples and functions. The proof of soundness is performed by Vafeiadis' operational soundness method. This method was originally formulated with respect to a concrete heap model. This paper adapts it to account for the absence of both units as well as the cancellativity law.
Cite as

Vincent Jackson, Toby Murray, and Christine Rizkallah. A Generalised Union of Rely-Guarantee and Separation Logic Using Permission Algebras. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 23:1-23:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{jackson_et_al:LIPIcs.ITP.2024.23,
  author =	{Jackson, Vincent and Murray, Toby and Rizkallah, Christine},
  title =	{{A Generalised Union of Rely-Guarantee and Separation Logic Using Permission Algebras}},
  booktitle =	{15th International Conference on Interactive Theorem Proving (ITP 2024)},
  pages =	{23:1--23:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-337-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{309},
  editor =	{Bertot, Yves and Kutsia, Temur and Norrish, Michael},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.23},
  URN =		{urn:nbn:de:0030-drops-207510},
  doi =		{10.4230/LIPIcs.ITP.2024.23},
  annote =	{Keywords: verification, concurrency, rely-guarantee, separation logic, resource algebras}
}
Document
DOI: 10.4230/LIPIcs.ITP.2024.33
Correctly Compiling Proofs About Programs Without Proving Compilers Correct

Authors: Audrey Seo, Christopher Lam, Dan Grossman, and Talia Ringer

Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)

Abstract
Guaranteeing correct compilation is nearly synonymous with compiler verification. However, the correctness guarantees for certified compilers and translation validation can be stronger than we need. While many compilers do have incorrect behavior, even when a compiler bug occurs it may not change the program’s behavior meaningfully with respect to its specification. Many real-world specifications are necessarily partial in that they do not completely specify all of a program’s behavior. While compiler verification and formal methods have had great success for safety-critical systems, there are magnitudes more code, such as math libraries, compiled with incorrect compilers, that would benefit from a guarantee of its partial specification. This paper explores a technique to get guarantees about compiled programs even in the presence of an unverified, or even incorrect, compiler. Our workflow compiles programs, specifications, and proof objects, from an embedded source language and logic to an embedded target language and logic. We implement two simple imperative languages, each with its own Hoare-style program logic, and a system for instantiating proof compilers out of compilers between these two languages that fulfill certain equational conditions in Coq. We instantiate our system on four compilers: one that is incomplete, two that are incorrect, and one that is correct but unverified. We use these instances to compile Hoare proofs for several programs, and we are able to leverage compiled proofs to assist in proofs of larger programs. Our proof compiler system is formally proven sound in Coq. We demonstrate how our approach enables strong target program guarantees even in the presence of incorrect compilation, opening up new options for which proof burdens one might shoulder instead of, or in addition to, compiler correctness.
Cite as

Audrey Seo, Christopher Lam, Dan Grossman, and Talia Ringer. Correctly Compiling Proofs About Programs Without Proving Compilers Correct. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 33:1-33:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{seo_et_al:LIPIcs.ITP.2024.33,
  author =	{Seo, Audrey and Lam, Christopher and Grossman, Dan and Ringer, Talia},
  title =	{{Correctly Compiling Proofs About Programs Without Proving Compilers Correct}},
  booktitle =	{15th International Conference on Interactive Theorem Proving (ITP 2024)},
  pages =	{33:1--33:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-337-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{309},
  editor =	{Bertot, Yves and Kutsia, Temur and Norrish, Michael},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.33},
  URN =		{urn:nbn:de:0030-drops-207612},
  doi =		{10.4230/LIPIcs.ITP.2024.33},
  annote =	{Keywords: proof transformations, compiler validation, program logics, proof engineering}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2024.13
The Power of Counting Steps in Quantitative Games

Authors: Sougata Bose, Rasmus Ibsen-Jensen, David Purser, Patrick Totzke, and Pierre Vandenhove

Published in: LIPIcs, Volume 311, 35th International Conference on Concurrency Theory (CONCUR 2024)

Abstract
We study deterministic games of infinite duration played on graphs and focus on the strategy complexity of quantitative objectives. Such games are known to admit optimal memoryless strategies over finite graphs, but require infinite-memory strategies in general over infinite graphs. We provide new lower and upper bounds for the strategy complexity of mean-payoff and total-payoff objectives over infinite graphs, focusing on whether step-counter strategies (sometimes called Markov strategies) suffice to implement winning strategies. In particular, we show that over finitely branching arenas, three variants of limsup mean-payoff and total-payoff objectives admit winning strategies that are based either on a step counter or on a step counter and an additional bit of memory. Conversely, we show that for certain liminf total-payoff objectives, strategies resorting to a step counter and finite memory are not sufficient. For step-counter strategies, this settles the case of all classical quantitative objectives up to the second level of the Borel hierarchy.
Cite as

Sougata Bose, Rasmus Ibsen-Jensen, David Purser, Patrick Totzke, and Pierre Vandenhove. The Power of Counting Steps in Quantitative Games. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 13:1-13:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{bose_et_al:LIPIcs.CONCUR.2024.13,
  author =	{Bose, Sougata and Ibsen-Jensen, Rasmus and Purser, David and Totzke, Patrick and Vandenhove, Pierre},
  title =	{{The Power of Counting Steps in Quantitative Games}},
  booktitle =	{35th International Conference on Concurrency Theory (CONCUR 2024)},
  pages =	{13:1--13:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-339-3},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{311},
  editor =	{Majumdar, Rupak and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2024.13},
  URN =		{urn:nbn:de:0030-drops-207852},
  doi =		{10.4230/LIPIcs.CONCUR.2024.13},
  annote =	{Keywords: Games on graphs, Markov strategies, quantitative objectives, infinite-state systems}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2024.28
Faster and Smaller Solutions of Obliging Games

Authors: Daniel Hausmann and Nir Piterman

Published in: LIPIcs, Volume 311, 35th International Conference on Concurrency Theory (CONCUR 2024)

Abstract
Obliging games have been introduced in the context of the game perspective on reactive synthesis in order to enforce a degree of cooperation between the to-be-synthesized system and the environment. Previous approaches to the analysis of obliging games have been small-step in the sense that they have been based on a reduction to standard (non-obliging) games in which single moves correspond to single moves in the original (obliging) game. Here, we propose a novel, large-step view on obliging games, reducing them to standard games in which single moves encode long-term behaviors in the original game. This not only allows us to give a meaningful definition of the environment winning in obliging games, but also leads to significantly improved bounds on both strategy sizes and the solution runtime for obliging games.
Cite as

Daniel Hausmann and Nir Piterman. Faster and Smaller Solutions of Obliging Games. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 28:1-28:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{hausmann_et_al:LIPIcs.CONCUR.2024.28,
  author =	{Hausmann, Daniel and Piterman, Nir},
  title =	{{Faster and Smaller Solutions of Obliging Games}},
  booktitle =	{35th International Conference on Concurrency Theory (CONCUR 2024)},
  pages =	{28:1--28:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-339-3},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{311},
  editor =	{Majumdar, Rupak and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2024.28},
  URN =		{urn:nbn:de:0030-drops-208008},
  doi =		{10.4230/LIPIcs.CONCUR.2024.28},
  annote =	{Keywords: Two-player games, reactive synthesis, Emerson-Lei games, parity games}
}
Document
DOI: 10.4230/LIPIcs.CP.2024.10
Anytime Weighted Model Counting with Approximation Guarantees for Probabilistic Inference

Authors: Alexandre Dubray, Pierre Schaus, and Siegfried Nijssen

Published in: LIPIcs, Volume 307, 30th International Conference on Principles and Practice of Constraint Programming (CP 2024)

Abstract
Weighted model counting (WMC) plays a central role in probabilistic reasoning. Given that this problem is #P-hard, harder instances can generally only be addressed using approximate techniques based on sampling, which provide statistical convergence guarantees: the longer a sampling process runs, the more accurate the WMC is likely to be. In this work, we propose a deterministic search-based approach that can also be stopped at any time and provides hard lower- and upper-bound guarantees on the true WMC. This approach uses a value heuristic that guides exploration first towards models with a high weight and leverages Limited Discrepancy Search to make the bounds converge faster. The validity, scalability, and convergence of our approach are tested and compared with state-of-the-art baseline methods on the problem of computing marginal probabilities in Bayesian networks and reliability estimation in probabilistic graphs.
Cite as

Alexandre Dubray, Pierre Schaus, and Siegfried Nijssen. Anytime Weighted Model Counting with Approximation Guarantees for Probabilistic Inference. In 30th International Conference on Principles and Practice of Constraint Programming (CP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 307, pp. 10:1-10:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{dubray_et_al:LIPIcs.CP.2024.10,
  author =	{Dubray, Alexandre and Schaus, Pierre and Nijssen, Siegfried},
  title =	{{Anytime Weighted Model Counting with Approximation Guarantees for Probabilistic Inference}},
  booktitle =	{30th International Conference on Principles and Practice of Constraint Programming (CP 2024)},
  pages =	{10:1--10:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-336-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{307},
  editor =	{Shaw, Paul},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2024.10},
  URN =		{urn:nbn:de:0030-drops-206956},
  doi =		{10.4230/LIPIcs.CP.2024.10},
  annote =	{Keywords: Projected Weighted Model Counting, Limited Discrepancy Search, Approximate Method, Probabilistic Inference}
}
Document
DOI: 10.4230/LIPIcs.CP.2024.16
A New Optimization Model for Multiple-Control Toffoli Quantum Circuit Design

Authors: Jihye Jung, Kevin Dalmeijer, and Pascal Van Hentenryck

Published in: LIPIcs, Volume 307, 30th International Conference on Principles and Practice of Constraint Programming (CP 2024)

Abstract
As quantum technology is advancing, the efficient design of quantum circuits has become an important area of research. This paper provides an introduction to the MCT quantum circuit design problem for reversible Boolean functions without assuming a prior background in quantum computing. While this is a well-studied problem, optimization models that minimize the true objective have only been explored recently. This paper introduces a new optimization model and symmetry-breaking constraints that improve solving time by up to two orders of magnitude compared to earlier work when a Constraint Programming solver is used. Experiments with up to seven qubits and using up to 15 quantum gates result in several new best-known circuits, obtained by any method, for well-known benchmarks. Finally, an extensive comparison with other approaches shows that optimization models may require more time but can provide superior circuits with optimality guarantees.
Cite as

Jihye Jung, Kevin Dalmeijer, and Pascal Van Hentenryck. A New Optimization Model for Multiple-Control Toffoli Quantum Circuit Design. In 30th International Conference on Principles and Practice of Constraint Programming (CP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 307, pp. 16:1-16:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{jung_et_al:LIPIcs.CP.2024.16,
  author =	{Jung, Jihye and Dalmeijer, Kevin and Van Hentenryck, Pascal},
  title =	{{A New Optimization Model for Multiple-Control Toffoli Quantum Circuit Design}},
  booktitle =	{30th International Conference on Principles and Practice of Constraint Programming (CP 2024)},
  pages =	{16:1--16:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-336-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{307},
  editor =	{Shaw, Paul},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2024.16},
  URN =		{urn:nbn:de:0030-drops-207010},
  doi =		{10.4230/LIPIcs.CP.2024.16},
  annote =	{Keywords: Constraint Programming, Quantum Circuit Design, Reversible Circuits}
}
Document
DOI: 10.4230/LIPIcs.CP.2024.19
An Efficient Local Search Solver for Mixed Integer Programming

Authors: Peng Lin, Mengchuan Zou, and Shaowei Cai

Published in: LIPIcs, Volume 307, 30th International Conference on Principles and Practice of Constraint Programming (CP 2024)

Abstract
Mixed integer programming (MIP) is a fundamental model in operations research. Local search is a powerful method for solving hard problems, but the development of local search solvers for MIP still needs to be explored. This work develops an efficient local search solver for solving MIP, called Local-MIP. We propose two new operators for MIP to adaptively modify variables for optimizing the objective function and satisfying constraints, respectively. Furthermore, we design a new weighting scheme to dynamically balance the priority between the objective function and each constraint, and propose a two-level scoring function structure to hierarchically guide the search for high-quality feasible solutions. Experiments are conducted on seven public benchmarks to compare Local-MIP with state-of-the-art MIP solvers, which demonstrate that Local-MIP significantly outperforms CPLEX, HiGHS, SCIP and Feasibility Jump, and is competitive with the most powerful commercial solver Gurobi. Moreover, Local-MIP establishes 4 new records for MIPLIB open instances.
Cite as

Peng Lin, Mengchuan Zou, and Shaowei Cai. An Efficient Local Search Solver for Mixed Integer Programming. In 30th International Conference on Principles and Practice of Constraint Programming (CP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 307, pp. 19:1-19:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{lin_et_al:LIPIcs.CP.2024.19,
  author =	{Lin, Peng and Zou, Mengchuan and Cai, Shaowei},
  title =	{{An Efficient Local Search Solver for Mixed Integer Programming}},
  booktitle =	{30th International Conference on Principles and Practice of Constraint Programming (CP 2024)},
  pages =	{19:1--19:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-336-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{307},
  editor =	{Shaw, Paul},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2024.19},
  URN =		{urn:nbn:de:0030-drops-207041},
  doi =		{10.4230/LIPIcs.CP.2024.19},
  annote =	{Keywords: Mixed Integer Programming, Local Search, Operator, Scoring Function}
}
Document
DOI: 10.4230/LIPIcs.WABI.2024.15
Swiftly Identifying Strongly Unique k-Mers

Authors: Jens Zentgraf and Sven Rahmann

Published in: LIPIcs, Volume 312, 24th International Workshop on Algorithms in Bioinformatics (WABI 2024)

Abstract
Motivation. Short DNA sequences of length k that appear in a single location (e.g., at a single genomic position, in a single species from a larger set of species, etc.) are called unique k-mers. They are useful for placing sequenced DNA fragments at the correct location without computing alignments and without ambiguity. However, they are not necessarily robust: A single basepair change may turn a unique k-mer into a different one that may in fact be present at one or more different locations, which may give confusing or contradictory information when attempting to place a read by its k-mer content. A more robust concept are strongly unique k-mers, i.e., unique k-mers for which no Hamming-distance-1 neighbor with conflicting information exists in all of the considered sequences. Given a set of k-mers, it is therefore of interest to have an efficient method that can distinguish k-mers with a Hamming-distance-1 neighbor in the collection from those that do not. Results. We present engineered algorithms to identify and mark within a set K of (canonical) k-mers all elements that have a Hamming-distance-1 neighbor in the same set. One algorithm is based on recursively running a 4-way comparison on sub-intervals of the sorted set. The other algorithm is based on bucketing and running a pairwise bit-parallel Hamming distance test on small buckets of the sorted set. Both methods consider canonical k-mers (i.e., taking reverse complements into account) and allow for efficient parallelization. The methods have been implemented and applied in practice to sets consisting of several billions of k-mers. An optimized combined approach running with 16 threads on a 16-core workstation, yields wall-clock running times below 20 seconds on the 2.5 billion distinct 31-mers of the human telomere-to-telomere reference genome. Availability. An implementation can be found at https://gitlab.com/rahmannlab/strong-k-mers.
Cite as

Jens Zentgraf and Sven Rahmann. Swiftly Identifying Strongly Unique k-Mers. In 24th International Workshop on Algorithms in Bioinformatics (WABI 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 312, pp. 15:1-15:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{zentgraf_et_al:LIPIcs.WABI.2024.15,
  author =	{Zentgraf, Jens and Rahmann, Sven},
  title =	{{Swiftly Identifying Strongly Unique k-Mers}},
  booktitle =	{24th International Workshop on Algorithms in Bioinformatics (WABI 2024)},
  pages =	{15:1--15:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-340-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{312},
  editor =	{Pissis, Solon P. and Sung, Wing-Kin},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.WABI.2024.15},
  URN =		{urn:nbn:de:0030-drops-206593},
  doi =		{10.4230/LIPIcs.WABI.2024.15},
  annote =	{Keywords: k-mer, Hamming distance, strong uniqueness, parallelization, algorithm engineering}
}
  • Refine by Author
  • 5 Müller, Rudolf
  • 3 Lehmann, Daniel
  • 3 Sandholm, Tuomas
  • 2 Ayoun, Sacha-Élie
  • 2 Gardner, Philippa
  • Show More...

  • Refine by Classification
  • 3 Mathematics of computing → Graph algorithms
  • 3 Theory of computation → Logic and verification
  • 3 Theory of computation → Parameterized complexity and exact algorithms
  • 3 Theory of computation → Separation logic
  • 2 Applied computing → Operations research
  • Show More...

  • Refine by Keyword
  • 3 separation logic
  • 2 Algorithms
  • 2 auctions
  • 2 complexity
  • 2 equilibrium
  • Show More...

  • Refine by Type
  • 37 document

  • Refine by Publication Year
  • 26 2024
  • 4 2005
  • 3 2009
  • 1 2002
  • 1 2007
  • Show More...

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