17 Search Results for "Nipkow, Tobias"

Document
RANDOM
DOI: 10.4230/LIPIcs.APPROX/RANDOM.2023.35
An Embarrassingly Parallel Optimal-Space Cardinality Estimation Algorithm

Authors: Emin Karayel

Published in: LIPIcs, Volume 275, Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2023)

Abstract
In 2020 Błasiok (ACM Trans. Algorithms 16(2) 3:1-3:28) constructed an optimal space streaming algorithm for the cardinality estimation problem with the space complexity of O(ε^{-2} ln(δ^{-1}) + ln n) where ε, δ and n denote the relative accuracy, failure probability and universe size, respectively. However, his solution requires the stream to be processed sequentially. On the other hand, there are algorithms that admit a merge operation; they can be used in a distributed setting, allowing parallel processing of sections of the stream, and are highly relevant for large-scale distributed applications. The best-known such algorithm, unfortunately, has a space complexity exceeding Ω(ln(δ^{-1}) (ε^{-2} ln ln n + ln n)). This work presents a new algorithm that improves on the solution by Błasiok, preserving its space complexity, but with the benefit that it admits such a merge operation, thus providing an optimal solution for the problem for both sequential and parallel applications. Orthogonally, the new algorithm also improves algorithmically on Błasiok’s solution (even in the sequential setting) by reducing its implementation complexity and requiring fewer distinct pseudo-random objects.
Cite as

Emin Karayel. An Embarrassingly Parallel Optimal-Space Cardinality Estimation Algorithm. In Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 275, pp. 35:1-35:22, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{karayel:LIPIcs.APPROX/RANDOM.2023.35,
  author =	{Karayel, Emin},
  title =	{{An Embarrassingly Parallel Optimal-Space Cardinality Estimation Algorithm}},
  booktitle =	{Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2023)},
  pages =	{35:1--35:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-296-9},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{275},
  editor =	{Megow, Nicole and Smith, Adam},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.APPROX/RANDOM.2023.35},
  URN =		{urn:nbn:de:0030-drops-188607},
  doi =		{10.4230/LIPIcs.APPROX/RANDOM.2023.35},
  annote =	{Keywords: Distinct Elements, Distributed Algorithms, Randomized Algorithms, Expander Graphs, Derandomization, Sketching}
}
Document
DOI: 10.4230/LIPIcs.ITP.2023.4
Fast, Verified Computation for Candle

Authors: Oskar Abrahamsson and Magnus O. Myreen

Published in: LIPIcs, Volume 268, 14th International Conference on Interactive Theorem Proving (ITP 2023)

Abstract
This paper describes how we have added an efficient function for computation to the kernel of the Candle interactive theorem prover. Candle is a CakeML port of HOL Light which we have, in prior work, proved sound w.r.t. the inference rules of the higher-order logic. This paper extends the original implementation and soundness proof with a new kernel function for fast computation. Experiments show that the new computation function is able to speed up certain evaluation proofs by several orders of magnitude.
Cite as

Oskar Abrahamsson and Magnus O. Myreen. Fast, Verified Computation for Candle. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 4:1-4:17, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{abrahamsson_et_al:LIPIcs.ITP.2023.4,
  author =	{Abrahamsson, Oskar and Myreen, Magnus O.},
  title =	{{Fast, Verified Computation for Candle}},
  booktitle =	{14th International Conference on Interactive Theorem Proving (ITP 2023)},
  pages =	{4:1--4:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-284-6},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{268},
  editor =	{Naumowicz, Adam and Thiemann, Ren\'{e}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.4},
  URN =		{urn:nbn:de:0030-drops-183797},
  doi =		{10.4230/LIPIcs.ITP.2023.4},
  annote =	{Keywords: Prover soundness, Higher-order logic, Interactive theorem proving}
}
Document
DOI: 10.4230/LIPIcs.ITP.2023.29
Real-Time Double-Ended Queue Verified (Proof Pearl)

Authors: Balazs Toth and Tobias Nipkow

Published in: LIPIcs, Volume 268, 14th International Conference on Interactive Theorem Proving (ITP 2023)

Abstract
We present the first verification of the real-time doubled-ended queue by Chuang and Goldberg where all operations take constant time. The main contributions are the full system invariant, the precise definition of all abstraction functions, the structure of the proof and the main lemmas.
Cite as

Balazs Toth and Tobias Nipkow. Real-Time Double-Ended Queue Verified (Proof Pearl). In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 29:1-29:18, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{toth_et_al:LIPIcs.ITP.2023.29,
  author =	{Toth, Balazs and Nipkow, Tobias},
  title =	{{Real-Time Double-Ended Queue Verified (Proof Pearl)}},
  booktitle =	{14th International Conference on Interactive Theorem Proving (ITP 2023)},
  pages =	{29:1--29:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-284-6},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{268},
  editor =	{Naumowicz, Adam and Thiemann, Ren\'{e}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.29},
  URN =		{urn:nbn:de:0030-drops-184044},
  doi =		{10.4230/LIPIcs.ITP.2023.29},
  annote =	{Keywords: Double-ended queue, data structures, verification, Isabelle}
}
Document
DOI: 10.4230/LIPIcs.ITP.2022.21
Formalization of Randomized Approximation Algorithms for Frequency Moments

Authors: Emin Karayel

Published in: LIPIcs, Volume 237, 13th International Conference on Interactive Theorem Proving (ITP 2022)

Abstract
In 1999 Alon et al. introduced the still active research topic of approximating the frequency moments of a data stream using randomized algorithms with minimal space usage. This includes the problem of estimating the cardinality of the stream elements - the zeroth frequency moment. Higher-order frequency moments provide information about the skew of the data stream which is, for example, critical information for parallel processing. (The k-th frequency moment of a data stream is the sum of the k-th powers of the occurrence counts of each element in the stream.) They introduce both lower bounds and upper bounds on the space complexity of the problems, which were later improved by newer publications. The algorithms have guaranteed success probabilities and accuracies without making any assumptions on the input distribution. They are an interesting use case for formal verification because their correctness proofs require a large body of deep results from algebra, analysis and probability theory. This work reports on the formal verification of three algorithms for the approximation of F₀, F₂ and F_k for k ≥ 3. The results include the identification of significantly simpler algorithms with the same runtime and space complexities as the previously known ones as well as the development of several reusable components, such as a formalization of universal hash families, amplification methods for randomized algorithms, a model for one-pass data stream algorithms or a generic flexible encoding library for the verification of space complexities.
Cite as

Emin Karayel. Formalization of Randomized Approximation Algorithms for Frequency Moments. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 21:1-21:21, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{karayel:LIPIcs.ITP.2022.21,
  author =	{Karayel, Emin},
  title =	{{Formalization of Randomized Approximation Algorithms for Frequency Moments}},
  booktitle =	{13th International Conference on Interactive Theorem Proving (ITP 2022)},
  pages =	{21:1--21:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-252-5},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{237},
  editor =	{Andronick, June and de Moura, Leonardo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.21},
  URN =		{urn:nbn:de:0030-drops-167308},
  doi =		{10.4230/LIPIcs.ITP.2022.21},
  annote =	{Keywords: Formal Verification, Isabelle/HOL, Randomized Algorithms, Frequency Moments}
}
Document
DOI: 10.4230/LIPIcs.ITP.2019.11
A Verified and Compositional Translation of LTL to Deterministic Rabin Automata

Authors: Julian Brunner, Benedikt Seidl, and Salomon Sickert

Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)

Abstract
We present a formalisation of the unified translation approach from linear temporal logic (LTL) to omega-automata from [Javier Esparza et al., 2018]. This approach decomposes LTL formulas into "simple" languages and allows a clear separation of concerns: first, we formalise the purely logical result yielding this decomposition; second, we develop a generic, executable, and expressive automata library providing necessary operations on automata to re-combine the "simple" languages; third, we instantiate this generic theory to obtain a construction for deterministic Rabin automata (DRA). We extract from this particular instantiation an executable tool translating LTL to DRAs. To the best of our knowledge this is the first verified translation of LTL to DRAs that is proven to be double-exponential in the worst case which asymptotically matches the known lower bound.
Cite as

Julian Brunner, Benedikt Seidl, and Salomon Sickert. A Verified and Compositional Translation of LTL to Deterministic Rabin Automata. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 11:1-11:19, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{brunner_et_al:LIPIcs.ITP.2019.11,
  author =	{Brunner, Julian and Seidl, Benedikt and Sickert, Salomon},
  title =	{{A Verified and Compositional Translation of LTL to Deterministic Rabin Automata}},
  booktitle =	{10th International Conference on Interactive Theorem Proving (ITP 2019)},
  pages =	{11:1--11:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-122-1},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{141},
  editor =	{Harrison, John and O'Leary, John and Tolmach, Andrew},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.11},
  URN =		{urn:nbn:de:0030-drops-110664},
  doi =		{10.4230/LIPIcs.ITP.2019.11},
  annote =	{Keywords: Automata Theory, Automata over Infinite Words, Deterministic Automata, Linear Temporal Logic, Model Checking, Verified Algorithms}
}
Document
DOI: 10.4230/LIPIcs.ITP.2019.23
Proof Pearl: Purely Functional, Simple and Efficient Priority Search Trees and Applications to Prim and Dijkstra

Authors: Peter Lammich and Tobias Nipkow

Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)

Abstract
The starting point of this paper is a new, purely functional, simple and efficient data structure combining a search tree and a priority queue, which we call a priority search tree. The salient feature of priority search trees is that they offer a decrease-key operation, something that is missing from other simple, purely functional priority queue implementations. As two applications of this data structure we verify purely functional, simple and efficient implementations of Prim’s and Dijkstra’s algorithms. This constitutes the first verification of an executable and even efficient version of Prim’s algorithm.
Cite as

Peter Lammich and Tobias Nipkow. Proof Pearl: Purely Functional, Simple and Efficient Priority Search Trees and Applications to Prim and Dijkstra. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 23:1-23:18, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{lammich_et_al:LIPIcs.ITP.2019.23,
  author =	{Lammich, Peter and Nipkow, Tobias},
  title =	{{Proof Pearl: Purely Functional, Simple and Efficient Priority Search Trees and Applications to Prim and Dijkstra}},
  booktitle =	{10th International Conference on Interactive Theorem Proving (ITP 2019)},
  pages =	{23:1--23:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-122-1},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{141},
  editor =	{Harrison, John and O'Leary, John and Tolmach, Andrew},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.23},
  URN =		{urn:nbn:de:0030-drops-110788},
  doi =		{10.4230/LIPIcs.ITP.2019.23},
  annote =	{Keywords: Priority queue, Dijkstra’s algorithm, Prim’s algorithm, verification, Isabelle}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.MFCS.2019.1
Trustworthy Graph Algorithms (Invited Talk)

Authors: Mohammad Abdulaziz, Kurt Mehlhorn, and Tobias Nipkow

Published in: LIPIcs, Volume 138, 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)

Abstract
The goal of the LEDA project was to build an easy-to-use and extendable library of correct and efficient data structures, graph algorithms and geometric algorithms. We report on the use of formal program verification to achieve an even higher level of trustworthiness. Specifically, we report on an ongoing and largely finished verification of the blossom-shrinking algorithm for maximum cardinality matching.
Cite as

Mohammad Abdulaziz, Kurt Mehlhorn, and Tobias Nipkow. Trustworthy Graph Algorithms (Invited Talk). In 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 138, pp. 1:1-1:22, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{abdulaziz_et_al:LIPIcs.MFCS.2019.1,
  author =	{Abdulaziz, Mohammad and Mehlhorn, Kurt and Nipkow, Tobias},
  title =	{{Trustworthy Graph Algorithms}},
  booktitle =	{44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)},
  pages =	{1:1--1:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-117-7},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{138},
  editor =	{Rossmanith, Peter and Heggernes, Pinar and Katoen, Joost-Pieter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2019.1},
  URN =		{urn:nbn:de:0030-drops-109456},
  doi =		{10.4230/LIPIcs.MFCS.2019.1},
  annote =	{Keywords: graph algorithms, formal correct proofs, Isabelle, LEDA, certifying algorithms}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2017.5
Formalized Proof Systems for Propositional Logic

Authors: Julius Michaelis and Tobias Nipkow

Published in: LIPIcs, Volume 104, 23rd International Conference on Types for Proofs and Programs (TYPES 2017)

Abstract
We have formalized a range of proof systems for classical propositional logic (sequent calculus, natural deduction, Hilbert systems, resolution) in Isabelle/HOL and have proved the most important meta-theoretic results about semantics and proofs: compactness, soundness, completeness, translations between proof systems, cut-elimination, interpolation and model existence.
Cite as

Julius Michaelis and Tobias Nipkow. Formalized Proof Systems for Propositional Logic. In 23rd International Conference on Types for Proofs and Programs (TYPES 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 104, pp. 5:1-5:16, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{michaelis_et_al:LIPIcs.TYPES.2017.5,
  author =	{Michaelis, Julius and Nipkow, Tobias},
  title =	{{Formalized Proof Systems for Propositional Logic}},
  booktitle =	{23rd International Conference on Types for Proofs and Programs (TYPES 2017)},
  pages =	{5:1--5:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-071-2},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{104},
  editor =	{Abel, Andreas and Nordvall Forsberg, Fredrik and Kaposi, Ambrus},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2017.5},
  URN =		{urn:nbn:de:0030-drops-100537},
  doi =		{10.4230/LIPIcs.TYPES.2017.5},
  annote =	{Keywords: formalization of logic, proof systems, sequent calculus, natural deduction, resolution}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2016.49
Verified Analysis of List Update Algorithms

Authors: Maximilian P. L. Haslbeck and Tobias Nipkow

Published in: LIPIcs, Volume 65, 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)

Abstract
This paper presents a machine-verified analysis of a number of classical algorithms for the list update problem: 2-competitiveness of move-to-front, the lower bound of 2 for the competitiveness of deterministic list update algorithms and 1.6-competitiveness of the randomized COMB algorithm, the best randomized list update algorithm known to date. The analysis is verified with help of the theorem prover Isabelle; some low-level proofs could be automated.
Cite as

Maximilian P. L. Haslbeck and Tobias Nipkow. Verified Analysis of List Update Algorithms. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 49:1-49:15, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{haslbeck_et_al:LIPIcs.FSTTCS.2016.49,
  author =	{Haslbeck, Maximilian P. L. and Nipkow, Tobias},
  title =	{{Verified Analysis of List Update Algorithms}},
  booktitle =	{36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
  pages =	{49:1--49:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-027-9},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{65},
  editor =	{Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.49},
  URN =		{urn:nbn:de:0030-drops-68849},
  doi =		{10.4230/LIPIcs.FSTTCS.2016.49},
  annote =	{Keywords: Program Verification, Algorithm Analysis, Online Algorithms}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2016.4
Verified Analysis of Functional Data Structures

Authors: Tobias Nipkow

Published in: LIPIcs, Volume 52, 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)

Abstract
In recent work the author has analyzed a number of classical functional search tree and priority queue implementations with the help of the theorem prover Isabelle/HOL. The functional correctness proofs of AVL trees, red-black trees, 2-3 trees, 2-3-4 trees, 1-2 brother trees, AA trees and splay trees could be automated. The amortized logarithmic complexity of skew heaps, splay trees, splay heaps and pairing heaps had to be proved manually.
Cite as

Tobias Nipkow. Verified Analysis of Functional Data Structures. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 4:1-4:2, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{nipkow:LIPIcs.FSCD.2016.4,
  author =	{Nipkow, Tobias},
  title =	{{Verified Analysis of Functional Data Structures}},
  booktitle =	{1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
  pages =	{4:1--4:2},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-010-1},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{52},
  editor =	{Kesner, Delia and Pientka, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.4},
  URN =		{urn:nbn:de:0030-drops-59701},
  doi =		{10.4230/LIPIcs.FSCD.2016.4},
  annote =	{Keywords: Program Verification, Algorithm Analysis, Functional Programming}
}
Document
DOI: 10.4230/DagRep.3.10.1
Deduction and Arithmetic (Dagstuhl Seminar 13411)

Authors: Nikolaj Bjorner, Reiner Hähnle, Tobias Nipkow, and Christoph Weidenbach

Published in: Dagstuhl Reports, Volume 3, Issue 10 (2014)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 13411 "Deduction and Arithmetic". The aim of this seminar was to bring together researchers working in deduction and fields related to arithmetic constraint solving. Current research in deduction can be categorized in three main strands: SMT solvers, automated first-order provers, and interactive provers. Although dealing with arithmetic has been in focus of all three for some years, there is still need of much better support of arithmetic. Reasong about arithmetic will stay at the center of attention in all three main approaches to automated deduction during the coming five to ten years. The seminar was an important event for the subcommunities involved that made it possible to communicate with each other so as to avoid duplicate effort and to exploit synergies. It succeeded also in identifying a number of important trends and open problems.
Cite as

Nikolaj Bjorner, Reiner Hähnle, Tobias Nipkow, and Christoph Weidenbach. Deduction and Arithmetic (Dagstuhl Seminar 13411). In Dagstuhl Reports, Volume 3, Issue 10, pp. 1-24, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@Article{bjorner_et_al:DagRep.3.10.1,
  author =	{Bjorner, Nikolaj and H\"{a}hnle, Reiner and Nipkow, Tobias and Weidenbach, Christoph},
  title =	{{Deduction and Arithmetic (Dagstuhl Seminar 13411)}},
  pages =	{1--24},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2014},
  volume =	{3},
  number =	{10},
  editor =	{Bjorner, Nikolaj and H\"{a}hnle, Reiner and Nipkow, Tobias and Weidenbach, Christoph},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.3.10.1},
  URN =		{urn:nbn:de:0030-drops-44250},
  doi =		{10.4230/DagRep.3.10.1},
  annote =	{Keywords: Automated Deduction; Program Verification; Arithmetic Constraint Solving}
}
Document
DOI: 10.4230/DagSemProc.09411.1
09411 Abstracts Collection – Interaction versus Automation: The two Faces of Deduction

Authors: Thomas Ball, Jürgen Giesl, Reiner Hähnle, and Tobias Nipkow

Published in: Dagstuhl Seminar Proceedings, Volume 9411, Interaction versus Automation: The two Faces of Deduction (2010)

Abstract
From 04.10. to 09.10.2009, the Dagstuhl Seminar 09411 ``Interaction versus Automation: The two Faces of Deduction'' was held in Schloss Dagstuhl~--~Leibniz Center for Informatics. During the seminar, several participants presented their current research, and ongoing work and open problems were discussed. Abstracts of the presentations given during the seminar as well as abstracts of seminar results and ideas are put together in this paper. The first section describes the seminar topics and goals in general. Links to extended abstracts or full papers are provided, if available.
Cite as

Thomas Ball, Jürgen Giesl, Reiner Hähnle, and Tobias Nipkow. 09411 Abstracts Collection – Interaction versus Automation: The two Faces of Deduction. In Interaction versus Automation: The two Faces of Deduction. Dagstuhl Seminar Proceedings, Volume 9411, pp. 1-18, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{ball_et_al:DagSemProc.09411.1,
  author =	{Ball, Thomas and Giesl, J\"{u}rgen and H\"{a}hnle, Reiner and Nipkow, Tobias},
  title =	{{09411 Abstracts Collection – Interaction versus Automation: The two Faces of Deduction}},
  booktitle =	{Interaction versus Automation: The two Faces of Deduction},
  pages =	{1--18},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{9411},
  editor =	{Thomas Ball and J\"{u}rgen Giesl and Reiner H\"{a}hnle and Tobias Nipkow},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.09411.1},
  URN =		{urn:nbn:de:0030-drops-25032},
  doi =		{10.4230/DagSemProc.09411.1},
  annote =	{Keywords: Formal Logic, Deduction, Artificial Intelligence}
}
Document
DOI: 10.4230/DagSemProc.09411.2
09411 Executive Summary – Interaction versus Automation: The two Faces of Deductions

Authors: Thomas Ball, Jürgen Giesl, Reiner Hähnle, and Tobias Nipkow

Published in: Dagstuhl Seminar Proceedings, Volume 9411, Interaction versus Automation: The two Faces of Deduction (2010)

Abstract
This seminar was the ninth in the series of the Dagstuhl "Deduction" seminars held biennially since 1993. Its goal was to bring together the closely related but unnecessarily disjoint communities of researchers working in interactive and automatic program verification.
Cite as

Thomas Ball, Jürgen Giesl, Reiner Hähnle, and Tobias Nipkow. 09411 Executive Summary – Interaction versus Automation: The two Faces of Deductions. In Interaction versus Automation: The two Faces of Deduction. Dagstuhl Seminar Proceedings, Volume 9411, pp. 1-4, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{ball_et_al:DagSemProc.09411.2,
  author =	{Ball, Thomas and Giesl, J\"{u}rgen and H\"{a}hnle, Reiner and Nipkow, Tobias},
  title =	{{09411 Executive Summary – Interaction versus Automation: The two Faces of Deductions}},
  booktitle =	{Interaction versus Automation: The two Faces of Deduction},
  pages =	{1--4},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{9411},
  editor =	{Thomas Ball and J\"{u}rgen Giesl and Reiner H\"{a}hnle and Tobias Nipkow},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.09411.2},
  URN =		{urn:nbn:de:0030-drops-24213},
  doi =		{10.4230/DagSemProc.09411.2},
  annote =	{Keywords: Formal Logic, Deduction, Artificial Intelligence}
}
Document
DOI: 10.4230/DagSemProc.09411.3
Automated reasoning in extensions of theories of constructors with recursively defined functions and homomorphisms

Authors: Viorica Sofronie-Stokkermans

Published in: Dagstuhl Seminar Proceedings, Volume 9411, Interaction versus Automation: The two Faces of Deduction (2010)

Abstract
We study possibilities of reasoning about extensions of base theories with functions which satisfy certain recursion and homomorphism properties. Our focus is on emphasizing possibilities of hierarchical and modular reasoning in such extensions and combinations thereof. \begin{itemize} item[(1)] We show that the theory of absolutely free constructors is local, and locality is preserved also in the presence of selectors. These results are consistent with existing decision procedures for this theory (e.g. by Oppen). item[(2)] We show that, under certain assumptions, extensions of the theory of absolutely free constructors with functions satisfying a certain type of recursion axioms satisfy locality properties, and show that for functions with values in an ordered domain we can combine recursive definitions with boundedness axioms without sacrificing locality. We also address the problem of only considering models whose data part is the {em initial} term algebra of such theories. item[(3)] We analyze conditions which ensure that similar results can be obtained if we relax some assumptions about the absolute freeness of the underlying theory of data types, and illustrate the ideas on an example from cryptography. end{itemize} The locality results we establish allow us to reduce the task of reasoning about the class of recursive functions we consider to reasoning in the underlying theory of data structures (possibly combined with the theories associated with the co-domains of the recursive functions). As a by-product, the methods we use provide a possibility of presenting in a different light (and in a different form) locality phenomena studied in cryp-to-gra-phy; we believe that they will allow to better separate rewriting from proving, and thus to give simpler proofs.
Cite as

Viorica Sofronie-Stokkermans. Automated reasoning in extensions of theories of constructors with recursively defined functions and homomorphisms. In Interaction versus Automation: The two Faces of Deduction. Dagstuhl Seminar Proceedings, Volume 9411, pp. 1-33, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{sofroniestokkermans:DagSemProc.09411.3,
  author =	{Sofronie-Stokkermans, Viorica},
  title =	{{Automated reasoning in extensions of theories of constructors with recursively defined functions and homomorphisms}},
  booktitle =	{Interaction versus Automation: The two Faces of Deduction},
  pages =	{1--33},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{9411},
  editor =	{Thomas Ball and J\"{u}rgen Giesl and Reiner H\"{a}hnle and Tobias Nipkow},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.09411.3},
  URN =		{urn:nbn:de:0030-drops-24241},
  doi =		{10.4230/DagSemProc.09411.3},
  annote =	{Keywords: Decision procedures, recursive datatypes, recursive functions, homomorphisms, verification, cryptography}
}
Document
DOI: 10.4230/DagSemProc.09411.4
Inductive Theorem Proving meets Dependency Pairs

Authors: Stephan Swiderski, Michael Parting, Jürgen Giesl, Carsten Fuhs, and Peter Schneider-Kamp

Published in: Dagstuhl Seminar Proceedings, Volume 9411, Interaction versus Automation: The two Faces of Deduction (2010)

Abstract
Current techniques and tools for automated termination analysis of term rewrite systems (TRSs) are already very powerful. However, they fail for algorithms whose termination is essentially due to an inductive argument. Therefore, we show how to couple the dependency pair method for TRS termination with inductive theorem proving. As confirmed by the implementation of our new approach in the tool AProVE, now TRS termination techniques are also successful on this important class of algorithms.
Cite as

Stephan Swiderski, Michael Parting, Jürgen Giesl, Carsten Fuhs, and Peter Schneider-Kamp. Inductive Theorem Proving meets Dependency Pairs. In Interaction versus Automation: The two Faces of Deduction. Dagstuhl Seminar Proceedings, Volume 9411, pp. 1-4, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{swiderski_et_al:DagSemProc.09411.4,
  author =	{Swiderski, Stephan and Parting, Michael and Giesl, J\"{u}rgen and Fuhs, Carsten and Schneider-Kamp, Peter},
  title =	{{Inductive Theorem Proving meets Dependency Pairs}},
  booktitle =	{Interaction versus Automation: The two Faces of Deduction},
  pages =	{1--4},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{9411},
  editor =	{Thomas Ball and J\"{u}rgen Giesl and Reiner H\"{a}hnle and Tobias Nipkow},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.09411.4},
  URN =		{urn:nbn:de:0030-drops-24220},
  doi =		{10.4230/DagSemProc.09411.4},
  annote =	{Keywords: Termination, Term Rewriting, Dependency Pairs, Inductive Theorem Proving}
}
  • Refine by Author
  • 10 Nipkow, Tobias
  • 4 Giesl, Jürgen
  • 3 Hähnle, Reiner
  • 2 Ball, Thomas
  • 2 Fuhs, Carsten
  • Show More...

  • Refine by Classification
  • 2 Mathematics of computing → Probabilistic algorithms
  • 2 Software and its engineering → Formal software verification
  • 2 Theory of computation → Data structures design and analysis
  • 2 Theory of computation → Pseudorandomness and derandomization
  • 1 Software and its engineering → Functional languages
  • Show More...

  • Refine by Keyword
  • 3 Isabelle
  • 3 verification
  • 2 Algorithm Analysis
  • 2 Artificial Intelligence
  • 2 Deduction
  • Show More...

  • Refine by Type
  • 17 document

  • Refine by Publication Year
  • 5 2010
  • 4 2019
  • 3 2023
  • 2 2016
  • 1 2006
  • 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 Schloss Dagstuhl - LZI GmbH Imprint Privacy Contact