3 Search Results for "Pratt, Simon"

Document
DOI: 10.4230/LIPIcs.ITP.2019.22
Generating Verified LLVM from Isabelle/HOL

Authors: Peter Lammich

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

Abstract
We present a framework to generate verified LLVM programs from Isabelle/HOL. It is based on a code generator that generates LLVM text from a simplified fragment of LLVM, shallowly embedded into Isabelle/HOL. On top, we have developed a separation logic, a verification condition generator, and an LLVM backend to the Isabelle Refinement Framework. As case studies, we have produced verified LLVM implementations of binary search and the Knuth-Morris-Pratt string search algorithm. These are one order of magnitude faster than the Standard-ML implementations produced with the original Refinement Framework, and on par with unverified C implementations. Adoption of the original correctness proofs to the new LLVM backend was straightforward. The trusted code base of our approach is the shallow embedding of the LLVM fragment and the code generator, which is a pretty printer combined with some straightforward compilation steps.
Cite as

Peter Lammich. Generating Verified LLVM from Isabelle/HOL. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 22:1-22:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{lammich:LIPIcs.ITP.2019.22,
  author =	{Lammich, Peter},
  title =	{{Generating Verified LLVM from Isabelle/HOL}},
  booktitle =	{10th International Conference on Interactive Theorem Proving (ITP 2019)},
  pages =	{22:1--22: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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.22},
  URN =		{urn:nbn:de:0030-drops-110777},
  doi =		{10.4230/LIPIcs.ITP.2019.22},
  annote =	{Keywords: Isabelle/HOL, LLVM, Separation Logic, Verification Condition Generator, Code Generation}
}
Document
DOI: 10.4230/LIPIcs.SWAT.2016.30
Time-Space Trade-offs for Triangulating a Simple Polygon

Authors: Boris Aronov, Matias Korman, Simon Pratt, André van Renssen, and Marcel Roeloffzen

Published in: LIPIcs, Volume 53, 15th Scandinavian Symposium and Workshops on Algorithm Theory (SWAT 2016)

Abstract
An s-workspace algorithm is an algorithm that has read-only access to the values of the input, write-only access to the output, and only uses O(s) additional words of space. We give a randomized s-workspace algorithm for triangulating a simple polygon P of n vertices, for any s up to n. The algorithm runs in O(n^2/s+n(log s)log^5(n/s)) expected time using O(s) variables, for any s up to n. In particular, the algorithm runs in O(n^2/s) expected time for most values of s.
Cite as

Boris Aronov, Matias Korman, Simon Pratt, André van Renssen, and Marcel Roeloffzen. Time-Space Trade-offs for Triangulating a Simple Polygon. In 15th Scandinavian Symposium and Workshops on Algorithm Theory (SWAT 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 53, pp. 30:1-30:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{aronov_et_al:LIPIcs.SWAT.2016.30,
  author =	{Aronov, Boris and Korman, Matias and Pratt, Simon and van Renssen, André and Roeloffzen, Marcel},
  title =	{{Time-Space Trade-offs for Triangulating a Simple Polygon}},
  booktitle =	{15th Scandinavian Symposium and Workshops on Algorithm Theory (SWAT 2016)},
  pages =	{30:1--30:12},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-011-8},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{53},
  editor =	{Pagh, Rasmus},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.SWAT.2016.30},
  URN =		{urn:nbn:de:0030-drops-60522},
  doi =		{10.4230/LIPIcs.SWAT.2016.30},
  annote =	{Keywords: simple polygon, triangulation, shortest path, time-space trade-off}
}
Document
DOI: 10.4230/LIPIcs.SoCG.2016.28
Two Approaches to Building Time-Windowed Geometric Data Structures

Authors: Timothy M. Chan and Simon Pratt

Published in: LIPIcs, Volume 51, 32nd International Symposium on Computational Geometry (SoCG 2016)

Abstract
Given a set of geometric objects each associated with a time value, we wish to determine whether a given property is true for a subset of those objects whose time values fall within a query time window. We call such problems time-windowed decision problems, and they have been the subject of much recent attention, for instance studied by Bokal, Cabello, and Eppstein [SoCG 2015]. In this paper, we present new approaches to this class of problems that are conceptually simpler than Bokal et al.'s, and also lead to faster algorithms. For instance, we present algorithms for preprocessing for the time-windowed 2D diameter decision problem in O(n log n) time and the time-windowed 2D convex hull area decision problem in O(n alpha(n) log n) time (where alpha is the inverse Ackermann function), improving Bokal et al.'s O(n log^2 n) and O(n log n loglog n) solutions respectively. Our first approach is to reduce time-windowed decision problems to a generalized range successor problem, which we solve using a novel way to search range trees. Our other approach is to use dynamic data structures directly, taking advantage of a new observation that the total number of combinatorial changes to a planar convex hull is near linear for any FIFO update sequence, in which deletions occur in the same order as insertions. We also apply these approaches to obtain the first O(n polylog n) algorithms for the time-windowed 3D diameter decision and 2D orthogonal segment intersection detection problems.
Cite as

Timothy M. Chan and Simon Pratt. Two Approaches to Building Time-Windowed Geometric Data Structures. In 32nd International Symposium on Computational Geometry (SoCG 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 51, pp. 28:1-28:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{chan_et_al:LIPIcs.SoCG.2016.28,
  author =	{Chan, Timothy M. and Pratt, Simon},
  title =	{{Two Approaches to Building Time-Windowed Geometric Data Structures}},
  booktitle =	{32nd International Symposium on Computational Geometry (SoCG 2016)},
  pages =	{28:1--28:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-009-5},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{51},
  editor =	{Fekete, S\'{a}ndor and Lubiw, Anna},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.SoCG.2016.28},
  URN =		{urn:nbn:de:0030-drops-59201},
  doi =		{10.4230/LIPIcs.SoCG.2016.28},
  annote =	{Keywords: time window, geometric data structures, range searching, dynamic convex hull}
}
  • Refine by Author
  • 2 Pratt, Simon
  • 1 Aronov, Boris
  • 1 Chan, Timothy M.
  • 1 Korman, Matias
  • 1 Lammich, Peter
  • Show More...

  • Refine by Classification
  • 1 Theory of computation → Logic and verification
  • 1 Theory of computation → Program verification
  • 1 Theory of computation → Separation logic

  • Refine by Keyword
  • 1 Code Generation
  • 1 Isabelle/HOL
  • 1 LLVM
  • 1 Separation Logic
  • 1 Verification Condition Generator
  • Show More...

  • Refine by Type
  • 3 document

  • Refine by Publication Year
  • 2 2016
  • 1 2019

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