5 Search Results for "Kennedy, Christopher"

Document
DOI: 10.4230/LIPIcs.ECOOP.2025.14
IsaBIL: A Framework for Verifying (In)correctness of Binaries in Isabelle/HOL

Authors: Matt Griffin, Brijesh Dongol, and Azalea Raad

Published in: LIPIcs, Volume 333, 39th European Conference on Object-Oriented Programming (ECOOP 2025)

Abstract
This paper presents IsaBIL, a binary analysis framework in Isabelle/HOL that is based on the widely used Binary Analysis Platform (BAP). Specifically, in IsaBIL, we formalise BAP’s intermediate language, called BIL and integrate it with Hoare logic (to enable proofs of correctness) as well as incorrectness logic (to enable proofs of incorrectness). IsaBIL inherits the full flexibility of BAP, allowing us to verify binaries for a wide range of languages (C, C++, Rust), toolchains (LLVM, Ghidra) and target architectures (x86, RISC-V), and can also be used when the source code for a binary is unavailable. To make verification tractable, we develop a number of big-step rules that combine BIL’s existing small-step rules at different levels of abstraction to support reuse. We develop high-level reasoning rules for RISC-V instructions (our main target architecture) to further optimise verification. Additionally, we develop Isabelle proof tactics that exploit common patterns in C binaries for RISC-V to discharge large numbers of proof goals (often in the 100s) automatically. IsaBIL includes an Isabelle/ML based parser for BIL programs, allowing one to automatically generate the associated Isabelle/HOL program locale from a BAP output. Taken together, IsaBIL provides a highly flexible proof environment for program binaries. As examples, we prove correctness of key examples from the Joint Strike Fighter coding standards and the MITRE database.
Cite as

Matt Griffin, Brijesh Dongol, and Azalea Raad. IsaBIL: A Framework for Verifying (In)correctness of Binaries in Isabelle/HOL. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 14:1-14:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{griffin_et_al:LIPIcs.ECOOP.2025.14,
  author =	{Griffin, Matt and Dongol, Brijesh and Raad, Azalea},
  title =	{{IsaBIL: A Framework for Verifying (In)correctness of Binaries in Isabelle/HOL}},
  booktitle =	{39th European Conference on Object-Oriented Programming (ECOOP 2025)},
  pages =	{14:1--14:30},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-373-7},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{333},
  editor =	{Aldrich, Jonathan and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2025.14},
  URN =		{urn:nbn:de:0030-drops-233070},
  doi =		{10.4230/LIPIcs.ECOOP.2025.14},
  annote =	{Keywords: Binary Analysis Platform, Isabelle/HOL, Hoare Logic, Incorrectness Logic}
}
Document
DOI: 10.4230/LIPIcs.ICDT.2025.12
Tractable Conjunctive Queries over Static and Dynamic Relations

Authors: Ahmet Kara, Zheng Luo, Milos Nikolic, Dan Olteanu, and Haozhe Zhang

Published in: LIPIcs, Volume 328, 28th International Conference on Database Theory (ICDT 2025)

Abstract
We investigate the evaluation of conjunctive queries over static and dynamic relations. While static relations are given as input and do not change, dynamic relations are subject to inserts and deletes. We characterise syntactically three classes of queries that admit constant update time and constant enumeration delay. We call such queries tractable. Depending on the class, the preprocessing time is linear, polynomial, or exponential (under data complexity, so the query size is constant). To decide whether a query is tractable, it does not suffice to analyse separately the sub-queries over the static relations and over the dynamic relations, respectively. Instead, we need to take the interaction between the static and the dynamic relations into account. Even when the sub-query over the dynamic relations is not tractable, the overall query can become tractable if the dynamic relations are sufficiently constrained by the static ones.
Cite as

Ahmet Kara, Zheng Luo, Milos Nikolic, Dan Olteanu, and Haozhe Zhang. Tractable Conjunctive Queries over Static and Dynamic Relations. In 28th International Conference on Database Theory (ICDT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 328, pp. 12:1-12:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{kara_et_al:LIPIcs.ICDT.2025.12,
  author =	{Kara, Ahmet and Luo, Zheng and Nikolic, Milos and Olteanu, Dan and Zhang, Haozhe},
  title =	{{Tractable Conjunctive Queries over Static and Dynamic Relations}},
  booktitle =	{28th International Conference on Database Theory (ICDT 2025)},
  pages =	{12:1--12:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-364-5},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{328},
  editor =	{Roy, Sudeepa and Kara, Ahmet},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICDT.2025.12},
  URN =		{urn:nbn:de:0030-drops-229534},
  doi =		{10.4230/LIPIcs.ICDT.2025.12},
  annote =	{Keywords: fully dynamic algorithm, constant enumeration delay, constant update time}
}
Document
DOI: 10.4230/LIPIcs.ICDT.2025.32
The Free Termination Property of Queries over Time

Authors: Conor Power, Paraschos Koutris, and Joseph M. Hellerstein

Published in: LIPIcs, Volume 328, 28th International Conference on Database Theory (ICDT 2025)

Abstract
Building on prior work on distributed databases and the CALM Theorem, we define and study the question of free termination: in the absence of distributed coordination, what query properties allow nodes in a distributed (database) system to unilaterally terminate execution even though they may receive additional data or messages in the future? This completeness question is complementary to the soundness questions studied in the CALM literature. We also develop a new model based on semiautomata that allows us to bridge from the relational transducer model of the CALM papers to algebraic models that are popular among software engineers (e.g. CRDTs) and of increasing interest to database theory for datalog extensions and incremental view maintenance.
Cite as

Conor Power, Paraschos Koutris, and Joseph M. Hellerstein. The Free Termination Property of Queries over Time. In 28th International Conference on Database Theory (ICDT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 328, pp. 32:1-32:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{power_et_al:LIPIcs.ICDT.2025.32,
  author =	{Power, Conor and Koutris, Paraschos and Hellerstein, Joseph M.},
  title =	{{The Free Termination Property of Queries over Time}},
  booktitle =	{28th International Conference on Database Theory (ICDT 2025)},
  pages =	{32:1--32:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-364-5},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{328},
  editor =	{Roy, Sudeepa and Kara, Ahmet},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICDT.2025.32},
  URN =		{urn:nbn:de:0030-drops-229736},
  doi =		{10.4230/LIPIcs.ICDT.2025.32},
  annote =	{Keywords: distributed systems, algebraic data models, coordination-free systems}
}
Document
DOI: 10.4230/LIPIcs.ITCS.2025.63
Complexity Classification of Product State Problems for Local Hamiltonians

Authors: John Kallaugher, Ojas Parekh, Kevin Thompson, Yipu Wang, and Justin Yirka

Published in: LIPIcs, Volume 325, 16th Innovations in Theoretical Computer Science Conference (ITCS 2025)

Abstract
Product states, unentangled tensor products of single qubits, are a ubiquitous ansatz in quantum computation, including for state-of-the-art Hamiltonian approximation algorithms. A natural question is whether we should expect to efficiently solve product state problems on any interesting families of Hamiltonians. We completely classify the complexity of finding minimum-energy product states for Hamiltonians defined by any fixed set of allowed 2-qubit interactions. Our results follow a line of work classifying the complexity of solving Hamiltonian problems and classical constraint satisfaction problems based on the allowed constraints. We prove that estimating the minimum energy of a product state is in 𝖯 if and only if all allowed interactions are 1-local, and NP-complete otherwise. Equivalently, any family of non-trivial two-body interactions generates Hamiltonians with NP-complete product-state problems. Our hardness constructions only require coupling strengths of constant magnitude. A crucial component of our proofs is a collection of hardness results for a new variant of the Vector Max-Cut problem, which should be of independent interest. Our definition involves sums of distances rather than squared distances and allows linear stretches. We similarly give a proof that the original Vector Max-Cut problem is NP-complete in 3 dimensions. This implies hardness of optimizing product states for Quantum Max-Cut (the quantum Heisenberg model) is NP-complete, even when every term is guaranteed to have positive unit weight.
Cite as

John Kallaugher, Ojas Parekh, Kevin Thompson, Yipu Wang, and Justin Yirka. Complexity Classification of Product State Problems for Local Hamiltonians. In 16th Innovations in Theoretical Computer Science Conference (ITCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 325, pp. 63:1-63:32, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{kallaugher_et_al:LIPIcs.ITCS.2025.63,
  author =	{Kallaugher, John and Parekh, Ojas and Thompson, Kevin and Wang, Yipu and Yirka, Justin},
  title =	{{Complexity Classification of Product State Problems for Local Hamiltonians}},
  booktitle =	{16th Innovations in Theoretical Computer Science Conference (ITCS 2025)},
  pages =	{63:1--63:32},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-361-4},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{325},
  editor =	{Meka, Raghu},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITCS.2025.63},
  URN =		{urn:nbn:de:0030-drops-226910},
  doi =		{10.4230/LIPIcs.ITCS.2025.63},
  annote =	{Keywords: quantum complexity, quantum algorithms, local hamiltonians}
}
Document
DOI: 10.4230/LIPIcs.ITCS.2017.53
Fast Cross-Polytope Locality-Sensitive Hashing

Authors: Christopher Kennedy and Rachel Ward

Published in: LIPIcs, Volume 67, 8th Innovations in Theoretical Computer Science Conference (ITCS 2017)

Abstract
We provide a variant of cross-polytope locality sensitive hashing with respect to angular distance which is provably optimal in asymptotic sensitivity and enjoys \mathcal{O}(d \ln d ) hash computation time. Building on a recent result in (Andoni, Indyk, Laarhoven, Razenshteyn '15), we show that optimal asymptotic sensitivity for cross-polytope LSH is retained even when the dense Gaussian matrix is replaced by a fast Johnson-Lindenstrauss transform followed by discrete pseudo-rotation, reducing the hash computation time from \mathcal{O}(d^2) to \mathcal{O}(d \ln d ). Moreover, our scheme achieves the optimal rate of convergence for sensitivity. By incorporating a low-randomness Johnson-Lindenstrauss transform, our scheme can be modified to require only \mathcal{O}(\ln^9(d)) random bits.
Cite as

Christopher Kennedy and Rachel Ward. Fast Cross-Polytope Locality-Sensitive Hashing. In 8th Innovations in Theoretical Computer Science Conference (ITCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 67, pp. 53:1-53:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{kennedy_et_al:LIPIcs.ITCS.2017.53,
  author =	{Kennedy, Christopher and Ward, Rachel},
  title =	{{Fast Cross-Polytope Locality-Sensitive Hashing}},
  booktitle =	{8th Innovations in Theoretical Computer Science Conference (ITCS 2017)},
  pages =	{53:1--53:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-029-3},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{67},
  editor =	{Papadimitriou, Christos H.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITCS.2017.53},
  URN =		{urn:nbn:de:0030-drops-81936},
  doi =		{10.4230/LIPIcs.ITCS.2017.53},
  annote =	{Keywords: Locality-sensitive hashing, Dimension reduction, Johnson-Lindenstrauss lemma}
}
  • Refine by Type
  • 5 Document/PDF
  • 4 Document/HTML

  • Refine by Publication Year
  • 4 2025
  • 1 2017

  • Refine by Author
  • 1 Dongol, Brijesh
  • 1 Griffin, Matt
  • 1 Hellerstein, Joseph M.
  • 1 Kallaugher, John
  • 1 Kara, Ahmet
  • Show More...

  • Refine by Series/Journal
  • 5 LIPIcs

  • Refine by Classification
  • 1 Information systems → Data streams
  • 1 Information systems → Database views
  • 1 Information systems → Parallel and distributed DBMSs
  • 1 Information systems → Stream management
  • 1 Theory of computation → Database query processing and optimization (theory)
  • Show More...

  • Refine by Keyword
  • 1 Binary Analysis Platform
  • 1 Dimension reduction
  • 1 Hoare Logic
  • 1 Incorrectness Logic
  • 1 Isabelle/HOL
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact