2 Search Results for "Li, Yishuai"


Document
Lessons for Interactive Theorem Proving Researchers from a Survey of Coq Users

Authors: Ana de Almeida Borges, Annalí Casanueva Artís, Jean-Rémy Falleri, Emilio Jesús Gallego Arias, Érik Martin-Dorel, Karl Palmskog, Alexander Serebrenik, and Théo Zimmermann

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


Abstract
The Coq Community Survey 2022 was an online public survey of users of the Coq proof assistant conducted during February 2022. Broadly, the survey asked about use of Coq features, user interfaces, libraries, plugins, and tools, views on renaming Coq and Coq improvements, and also demographic data such as education and experience with Coq and other proof assistants and programming languages. The survey received 466 submitted responses, making it the largest survey of users of an interactive theorem prover (ITP) so far. We present the design of the survey, a summary of key results, and analysis of answers relevant to ITP technology development and usage. In particular, we analyze user characteristics associated with adoption of tools and libraries and make comparisons to adjacent software communities. Notably, we find that experience has significant impact on Coq user behavior, including on usage of tools, libraries, and integrated development environments.

Cite as

Ana de Almeida Borges, Annalí Casanueva Artís, Jean-Rémy Falleri, Emilio Jesús Gallego Arias, Érik Martin-Dorel, Karl Palmskog, Alexander Serebrenik, and Théo Zimmermann. Lessons for Interactive Theorem Proving Researchers from a Survey of Coq Users. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 12:1-12:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@InProceedings{dealmeidaborges_et_al:LIPIcs.ITP.2023.12,
  author =	{de Almeida Borges, Ana and Casanueva Art{\'\i}s, Annal{\'\i} and Falleri, Jean-R\'{e}my and Gallego Arias, Emilio Jes\'{u}s and Martin-Dorel, \'{E}rik and Palmskog, Karl and Serebrenik, Alexander and Zimmermann, Th\'{e}o},
  title =	{{Lessons for Interactive Theorem Proving Researchers from a Survey of Coq Users}},
  booktitle =	{14th International Conference on Interactive Theorem Proving (ITP 2023)},
  pages =	{12:1--12: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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.12},
  URN =		{urn:nbn:de:0030-drops-183875},
  doi =		{10.4230/LIPIcs.ITP.2023.12},
  annote =	{Keywords: Coq, Community, Survey, Statistical Analysis}
}
Document
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-dev.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}
}
  • Refine by Author
  • 1 Beringer, Lennart
  • 1 Casanueva Artís, Annalí
  • 1 Falleri, Jean-Rémy
  • 1 Gallego Arias, Emilio Jesús
  • 1 Honoré, Wolf
  • Show More...

  • Refine by Classification
  • 1 General and reference → Empirical studies
  • 1 Software and its engineering → Formal methods
  • 1 Theory of computation → Program specifications
  • 1 Theory of computation → Program verification
  • 1 Theory of computation → Separation logic

  • Refine by Keyword
  • 2 Coq
  • 1 Community
  • 1 HTTP
  • 1 Statistical Analysis
  • 1 Survey
  • Show More...

  • Refine by Type
  • 2 document

  • Refine by Publication Year
  • 1 2021
  • 1 2023

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