2 Search Results for "Morris, John"

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.ICLP.2012.235
Reconciling Well-Founded Semantics of DL-Programs and Aggregate Programs

Authors: Jia-Huai You, John Morris, and Yi Bi

Published in: LIPIcs, Volume 17, Technical Communications of the 28th International Conference on Logic Programming (ICLP'12) (2012)

Abstract
Logic programs with aggregates and description logic programs (dl-programs) are two recent extensions to logic programming. In this paper, we study the relationships between these two classes of logic programs, under the well-founded semantics. The main result is that, under a satisfaction-preserving mapping from dl-atoms to aggregates, the well-founded semantics of dl-programs by Eiter et al., coincides with the well-founded semantics of aggregate programs, defined by Pelov et al. as the least fixpoint of a 3-valued immediate consequence operator under the ultimate approximating aggregate. This result enables an alternative definition of the same well-founded semantics for aggregate programs, in terms of the first principle of unfounded sets. Furthermore, the result can be applied, in a uniform manner, to define the well-founded semantics for dl-programs with aggregates, which agrees with the existing semantics when either dl-atoms or aggregates are absent.
Cite as

Jia-Huai You, John Morris, and Yi Bi. Reconciling Well-Founded Semantics of DL-Programs and Aggregate Programs. In Technical Communications of the 28th International Conference on Logic Programming (ICLP'12). Leibniz International Proceedings in Informatics (LIPIcs), Volume 17, pp. 235-246, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{you_et_al:LIPIcs.ICLP.2012.235,
  author =	{You, Jia-Huai and Morris, John and Bi, Yi},
  title =	{{Reconciling Well-Founded Semantics of DL-Programs and Aggregate Programs}},
  booktitle =	{Technical Communications of the 28th International Conference on Logic Programming (ICLP'12)},
  pages =	{235--246},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-43-9},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{17},
  editor =	{Dovier, Agostino and Santos Costa, V{\'\i}tor},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICLP.2012.235},
  URN =		{urn:nbn:de:0030-drops-36258},
  doi =		{10.4230/LIPIcs.ICLP.2012.235},
  annote =	{Keywords: Well-founded semantics, description logic programs, aggregate logic programs, three-valued logic.}
}
  • Refine by Author
  • 1 Bi, Yi
  • 1 Lammich, Peter
  • 1 Morris, John
  • 1 You, Jia-Huai

  • 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
  • 2 document

  • Refine by Publication Year
  • 1 2012
  • 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