1 Search Results for "Qu, Weihao"

Document
DOI: 10.4230/LIPIcs.ITP.2022.30
Formalizing Algorithmic Bounds in the Query Model in EasyCrypt

Authors: Alley Stoughton, Carol Chen, Marco Gaboardi, and Weihao Qu

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

Abstract
We use the EasyCrypt proof assistant to formalize the adversarial approach to proving lower bounds for computational problems in the query model. This is done using a lower bound game between an algorithm and adversary, in which the adversary answers the algorithm’s queries in a way that makes the algorithm issue at least the desired number of queries. A complementary upper bound game is used for proving upper bounds of algorithms; here the adversary incrementally and adaptively realizes an algorithm’s input. We prove a natural connection between the lower and upper bound games, and apply our framework to three computational problems, including searching in an ordered list and comparison-based sorting, giving evidence for the generality of our notion of algorithm and the usefulness of our framework.
Cite as

Alley Stoughton, Carol Chen, Marco Gaboardi, and Weihao Qu. Formalizing Algorithmic Bounds in the Query Model in EasyCrypt. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 30:1-30:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{stoughton_et_al:LIPIcs.ITP.2022.30,
  author =	{Stoughton, Alley and Chen, Carol and Gaboardi, Marco and Qu, Weihao},
  title =	{{Formalizing Algorithmic Bounds in the Query Model in EasyCrypt}},
  booktitle =	{13th International Conference on Interactive Theorem Proving (ITP 2022)},
  pages =	{30:1--30: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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.30},
  URN =		{urn:nbn:de:0030-drops-167399},
  doi =		{10.4230/LIPIcs.ITP.2022.30},
  annote =	{Keywords: query model, lower bound, upper bound, adversary argument, EasyCrypt}
}
  • Refine by Author
  • 1 Chen, Carol
  • 1 Gaboardi, Marco
  • 1 Qu, Weihao
  • 1 Stoughton, Alley

  • Refine by Classification
  • 1 Theory of computation → Design and analysis of algorithms
  • 1 Theory of computation → Logic and verification
  • 1 Theory of computation → Models of computation

  • Refine by Keyword
  • 1 EasyCrypt
  • 1 adversary argument
  • 1 lower bound
  • 1 query model
  • 1 upper bound

  • Refine by Type
  • 1 document

  • Refine by Publication Year
  • 1 2022

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