DROPS

Document

DOI: 10.4230/LIPIcs.ITP.2021.32

Verifying an HTTP Key-Value Server with Interaction Trees and VST

Authors: Hengchu Zhang, Wolf Honoré, Nicolas Koh, Yao Li, Yishuai Li, Li-Yao Xia, Lennart Beringer, William Mansky, Benjamin Pierce, and Steve Zdancewic

Published in: LIPIcs, Volume 193, 12th International Conference on Interactive Theorem Proving (ITP 2021)

Abstract

We present a networked key-value server, implemented in C and formally verified in Coq. The server interacts with clients using a subset of the HTTP/1.1 protocol and is specified and verified using interaction trees and the Verified Software Toolchain. The codebase includes a reusable and fully verified C string library that provides 17 standard POSIX string functions and 17 general purpose non-POSIX string functions. For the KVServer socket system calls, we establish a refinement relation between specifications at user-space level and at CertiKOS kernel-space level.

Cite as

Hengchu Zhang, Wolf Honoré, Nicolas Koh, Yao Li, Yishuai Li, Li-Yao Xia, Lennart Beringer, William Mansky, Benjamin Pierce, and Steve Zdancewic. Verifying an HTTP Key-Value Server with Interaction Trees and VST. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 32:1-32:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{zhang_et_al:LIPIcs.ITP.2021.32,
  author =	{Zhang, Hengchu and Honor\'{e}, Wolf and Koh, Nicolas and Li, Yao and Li, Yishuai and Xia, Li-Yao and Beringer, Lennart and Mansky, William and Pierce, Benjamin and Zdancewic, Steve},
  title =	{{Verifying an HTTP Key-Value Server with Interaction Trees and VST}},
  booktitle =	{12th International Conference on Interactive Theorem Proving (ITP 2021)},
  pages =	{32:1--32:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-188-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{193},
  editor =	{Cohen, Liron and Kaliszyk, Cezary},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.32},
  URN =		{urn:nbn:de:0030-drops-139273},
  doi =		{10.4230/LIPIcs.ITP.2021.32},
  annote =	{Keywords: formal verification, Coq, HTTP, deep specification}
}

Document

DOI: 10.4230/OASIcs.WPTE.2014.15

Verifying Optimizations for Concurrent Programs

Authors: William Mansky and Elsa L. Gunter

Published in: OASIcs, Volume 40, First International Workshop on Rewriting Techniques for Program Transformations and Evaluation (2014)

Abstract

While program correctness for compiled languages depends fundamentally on compiler correctness, compiler optimizations are not usually formally verified due to the effort involved, particularly in the presence of concurrency. In this paper, we present a framework for stating and reasoning about compiler optimizations and transformations on programs in the presence of relaxed memory models. The core of the framework is the PTRANS specification language, in which program transformations are expressed as rewrites on control flow graphs with temporal logic side conditions. We demonstrate our technique by verifying the correctness of a redundant store elimination optimization in a simple LLVM-like intermediate language, relying on a theorem that allows us to lift single-thread simulation relations to simulations on multithreaded programs.

Cite as

William Mansky and Elsa L. Gunter. Verifying Optimizations for Concurrent Programs. In First International Workshop on Rewriting Techniques for Program Transformations and Evaluation. Open Access Series in Informatics (OASIcs), Volume 40, pp. 15-26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{mansky_et_al:OASIcs.WPTE.2014.15,
  author =	{Mansky, William and Gunter, Elsa L.},
  title =	{{Verifying Optimizations for Concurrent Programs}},
  booktitle =	{First International Workshop on Rewriting Techniques for Program Transformations and Evaluation},
  pages =	{15--26},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-70-5},
  ISSN =	{2190-6807},
  year =	{2014},
  volume =	{40},
  editor =	{Schmidt-Schau{\ss}, Manfred and Sakai, Masahiko and Sabel, David and Chiba, Yuki},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.WPTE.2014.15},
  URN =		{urn:nbn:de:0030-drops-45869},
  doi =		{10.4230/OASIcs.WPTE.2014.15},
  annote =	{Keywords: optimizing compilers, interactive theorem proving, program transformations, temporal logic, relaxed memory models}
}

Search Results

Documents authored by Mansky, William

Verifying an HTTP Key-Value Server with Interaction Trees and VST

Abstract

Cite as

Verifying Optimizations for Concurrent Programs

Abstract

Cite as

Thanks for your feedback!

Could not send message