2 Search Results for "Kincaid, Zachary"


Document
Domains for Higher-Order Games

Authors: Matthew Hague, Roland Meyer, and Sebastian Muskalla

Published in: LIPIcs, Volume 83, 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)


Abstract
We study two-player inclusion games played over word-generating higher-order recursion schemes. While inclusion checks are known to capture verification problems, two-player games generalize this relationship to program synthesis. In such games, non-terminals of the grammar are controlled by opposing players. The goal of the existential player is to avoid producing a word that lies outside of a regular language of safe words. We contribute a new domain that provides a representation of the winning region of such games. Our domain is based on (functions over) potentially infinite Boolean formulas with words as atomic propositions. We develop an abstract interpretation framework that we instantiate to abstract this domain into a domain where the propositions are replaced by states of a finite automaton. This second domain is therefore finite and we obtain, via standard fixed-point techniques, a direct algorithm for the analysis of two-player inclusion games. We show, via a second instantiation of the framework, that our finite domain can be optimized, leading to a (k+1)EXP algorithm for order-k recursion schemes. We give a matching lower bound, showing that our approach is optimal. Since our approach is based on standard Kleene iteration, existing techniques and tools for fixed-point computations can be applied.

Cite as

Matthew Hague, Roland Meyer, and Sebastian Muskalla. Domains for Higher-Order Games. In 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 83, pp. 59:1-59:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)


Copy BibTex To Clipboard

@InProceedings{hague_et_al:LIPIcs.MFCS.2017.59,
  author =	{Hague, Matthew and Meyer, Roland and Muskalla, Sebastian},
  title =	{{Domains for Higher-Order Games}},
  booktitle =	{42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)},
  pages =	{59:1--59:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-046-0},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{83},
  editor =	{Larsen, Kim G. and Bodlaender, Hans L. and Raskin, Jean-Francois},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2017.59},
  URN =		{urn:nbn:de:0030-drops-81409},
  doi =		{10.4230/LIPIcs.MFCS.2017.59},
  annote =	{Keywords: higher-order recursion schemes, games, semantics, abstract interpretation, fixed points}
}
Document
Invited Talk
A New Notion of Compositionality for Concurrent Program Proofs (Invited Talk)

Authors: Azadeh Farzan and Zachary Kincaid

Published in: LIPIcs, Volume 85, 28th International Conference on Concurrency Theory (CONCUR 2017)


Abstract
This paper presents a high level overview of Proof Spaces [Farzan, Kincaid, and Podelski, 2015] as an instance of a new approach to compositional verification of concurrent programs and discusses potential future work extending the approach beyond its current scope of applicability.

Cite as

Azadeh Farzan and Zachary Kincaid. A New Notion of Compositionality for Concurrent Program Proofs (Invited Talk). In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 4:1-4:11, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2017)


Copy BibTex To Clipboard

@InProceedings{farzan_et_al:LIPIcs.CONCUR.2017.4,
  author =	{Farzan, Azadeh and Kincaid, Zachary},
  title =	{{A New Notion of Compositionality for Concurrent Program Proofs}},
  booktitle =	{28th International Conference on Concurrency Theory (CONCUR 2017)},
  pages =	{4:1--4:11},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-048-4},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{85},
  editor =	{Meyer, Roland and Nestmann, Uwe},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.4},
  URN =		{urn:nbn:de:0030-drops-78097},
  doi =		{10.4230/LIPIcs.CONCUR.2017.4},
  annote =	{Keywords: Concurrency, Proofs, Dynamic Memory, Recursion}
}
  • Refine by Author
  • 1 Farzan, Azadeh
  • 1 Hague, Matthew
  • 1 Kincaid, Zachary
  • 1 Meyer, Roland
  • 1 Muskalla, Sebastian

  • Refine by Classification

  • Refine by Keyword
  • 1 Concurrency
  • 1 Dynamic Memory
  • 1 Proofs
  • 1 Recursion
  • 1 abstract interpretation
  • Show More...

  • Refine by Type
  • 2 document

  • Refine by Publication Year
  • 2 2017

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