6 Search Results for "Grier, Daniel"

Document
DOI: 10.4230/LIPIcs.ITP.2024.36
Defining and Preserving More C Behaviors: Verified Compilation Using a Concrete Memory Model

Authors: Andrew Tolmach, Chris Chhak, and Sean Anderson

Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)

Abstract
We propose a concrete ("pointer as integer") memory semantics for C that supports verified compilation to a target environment having simple "public vs. private" data protection based on tagging or sandboxing (such as the WebAssembly virtual machine). Our semantics gives definition to a range of legacy programming idioms that cause undefined behavior in standard C, and are not covered by existing verified compilers, but that often work in practice. Compiler correctness in this context implies that target programs are secure against all control-flow attacks (although not against data-only attacks). To avoid tying our semantics too closely to particular compiler implementation choices, it is parameterized by a novel form of oracle that non-deterministically chooses the addresses of stack and heap allocations. As a proof-of-concept, we formalize a small RTL-like language and verify two-way refinement for a compiler from this language to a low-level machine and runtime system with hardware tagging. Our Coq formalization and proofs are provided as supplementary material.
Cite as

Andrew Tolmach, Chris Chhak, and Sean Anderson. Defining and Preserving More C Behaviors: Verified Compilation Using a Concrete Memory Model. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 36:1-36:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{tolmach_et_al:LIPIcs.ITP.2024.36,
  author =	{Tolmach, Andrew and Chhak, Chris and Anderson, Sean},
  title =	{{Defining and Preserving More C Behaviors: Verified Compilation Using a Concrete Memory Model}},
  booktitle =	{15th International Conference on Interactive Theorem Proving (ITP 2024)},
  pages =	{36:1--36:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-337-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{309},
  editor =	{Bertot, Yves and Kutsia, Temur and Norrish, Michael},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.36},
  URN =		{urn:nbn:de:0030-drops-207643},
  doi =		{10.4230/LIPIcs.ITP.2024.36},
  annote =	{Keywords: Compiler verification, C language semantics, Coq proof assistant}
}
Document
DOI: 10.4230/LIPIcs.ITCS.2021.32
Bounds on the QAC^0 Complexity of Approximating Parity

Authors: Gregory Rosenthal

Published in: LIPIcs, Volume 185, 12th Innovations in Theoretical Computer Science Conference (ITCS 2021)

Abstract
QAC circuits are quantum circuits with one-qubit gates and Toffoli gates of arbitrary arity. QAC^0 circuits are QAC circuits of constant depth, and are quantum analogues of AC^0 circuits. We prove the following: - For all d ≥ 7 and ε > 0 there is a depth-d QAC circuit of size exp(poly(n^{1/d}) log(n/ε)) that approximates the n-qubit parity function to within error ε on worst-case quantum inputs. Previously it was unknown whether QAC circuits of sublogarithmic depth could approximate parity regardless of size. - We introduce a class of "mostly classical" QAC circuits, including a major component of our circuit from the above upper bound, and prove a tight lower bound on the size of low-depth, mostly classical QAC circuits that approximate this component. - Arbitrary depth-d QAC circuits require at least Ω(n/d) multi-qubit gates to achieve a 1/2 + exp(-o(n/d)) approximation of parity. When d = Θ(log n) this nearly matches an easy O(n) size upper bound for computing parity exactly. - QAC circuits with at most two layers of multi-qubit gates cannot achieve a 1/2 + exp(-o(n)) approximation of parity, even non-cleanly. Previously it was known only that such circuits could not cleanly compute parity exactly for sufficiently large n. The proofs use a new normal form for quantum circuits which may be of independent interest, and are based on reductions to the problem of constructing certain generalizations of the cat state which we name "nekomata" after an analogous cat yōkai.
Cite as

Gregory Rosenthal. Bounds on the QAC^0 Complexity of Approximating Parity. In 12th Innovations in Theoretical Computer Science Conference (ITCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 185, pp. 32:1-32:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{rosenthal:LIPIcs.ITCS.2021.32,
  author =	{Rosenthal, Gregory},
  title =	{{Bounds on the QAC^0 Complexity of Approximating Parity}},
  booktitle =	{12th Innovations in Theoretical Computer Science Conference (ITCS 2021)},
  pages =	{32:1--32:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-177-1},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{185},
  editor =	{Lee, James R.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITCS.2021.32},
  URN =		{urn:nbn:de:0030-drops-135713},
  doi =		{10.4230/LIPIcs.ITCS.2021.32},
  annote =	{Keywords: quantum circuit complexity, QAC^0, fanout, parity, nekomata}
}
Document
RANDOM
DOI: 10.4230/LIPIcs.APPROX-RANDOM.2019.52
Approximating the Noise Sensitivity of a Monotone Boolean Function

Authors: Ronitt Rubinfeld and Arsen Vasilyan

Published in: LIPIcs, Volume 145, Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2019)

Abstract
The noise sensitivity of a Boolean function f: {0,1}^n - > {0,1} is one of its fundamental properties. For noise parameter delta, the noise sensitivity is denoted as NS_{delta}[f]. This quantity is defined as follows: First, pick x = (x_1,...,x_n) uniformly at random from {0,1}^n, then pick z by flipping each x_i independently with probability delta. NS_{delta}[f] is defined to equal Pr [f(x) != f(z)]. Much of the existing literature on noise sensitivity explores the following two directions: (1) Showing that functions with low noise-sensitivity are structured in certain ways. (2) Mathematically showing that certain classes of functions have low noise sensitivity. Combined, these two research directions show that certain classes of functions have low noise sensitivity and therefore have useful structure. The fundamental importance of noise sensitivity, together with this wealth of structural results, motivates the algorithmic question of approximating NS_{delta}[f] given an oracle access to the function f. We show that the standard sampling approach is essentially optimal for general Boolean functions. Therefore, we focus on estimating the noise sensitivity of monotone functions, which form an important subclass of Boolean functions, since many functions of interest are either monotone or can be simply transformed into a monotone function (for example the class of unate functions consists of all the functions that can be made monotone by reorienting some of their coordinates [O'Donnell, 2014]). Specifically, we study the algorithmic problem of approximating NS_{delta}[f] for monotone f, given the promise that NS_{delta}[f] >= 1/n^{C} for constant C, and for delta in the range 1/n <= delta <= 1/2. For such f and delta, we give a randomized algorithm performing O((min(1,sqrt{n} delta log^{1.5} n))/(NS_{delta}[f]) poly (1/epsilon)) queries and approximating NS_{delta}[f] to within a multiplicative factor of (1 +/- epsilon). Given the same constraints on f and delta, we also prove a lower bound of Omega((min(1,sqrt{n} delta))/(NS_{delta}[f] * n^{xi})) on the query complexity of any algorithm that approximates NS_{delta}[f] to within any constant factor, where xi can be any positive constant. Thus, our algorithm’s query complexity is close to optimal in terms of its dependence on n. We introduce a novel descending-ascending view of noise sensitivity, and use it as a central tool for the analysis of our algorithm. To prove lower bounds on query complexity, we develop a technique that reduces computational questions about query complexity to combinatorial questions about the existence of "thin" functions with certain properties. The existence of such "thin" functions is proved using the probabilistic method. These techniques also yield new lower bounds on the query complexity of approximating other fundamental properties of Boolean functions: the total influence and the bias.
Cite as

Ronitt Rubinfeld and Arsen Vasilyan. Approximating the Noise Sensitivity of a Monotone Boolean Function. In Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 145, pp. 52:1-52:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{rubinfeld_et_al:LIPIcs.APPROX-RANDOM.2019.52,
  author =	{Rubinfeld, Ronitt and Vasilyan, Arsen},
  title =	{{Approximating the Noise Sensitivity of a Monotone Boolean Function}},
  booktitle =	{Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2019)},
  pages =	{52:1--52:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-125-2},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{145},
  editor =	{Achlioptas, Dimitris and V\'{e}gh, L\'{a}szl\'{o} A.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.APPROX-RANDOM.2019.52},
  URN =		{urn:nbn:de:0030-drops-112672},
  doi =		{10.4230/LIPIcs.APPROX-RANDOM.2019.52},
  annote =	{Keywords: Monotone Boolean functions, noise sensitivity, influence}
}
Document
DOI: 10.4230/LIPIcs.CCC.2018.19
New Hardness Results for the Permanent Using Linear Optics

Authors: Daniel Grier and Luke Schaeffer

Published in: LIPIcs, Volume 102, 33rd Computational Complexity Conference (CCC 2018)

Abstract
In 2011, Aaronson gave a striking proof, based on quantum linear optics, that the problem of computing the permanent of a matrix is #P-hard. Aaronson's proof led naturally to hardness of approximation results for the permanent, and it was arguably simpler than Valiant's seminal proof of the same fact in 1979. Nevertheless, it did not show #P-hardness of the permanent for any class of matrices which was not previously known. In this paper, we present a collection of new results about matrix permanents that are derived primarily via these linear optical techniques. First, we show that the problem of computing the permanent of a real orthogonal matrix is #P-hard. Much like Aaronson's original proof, this implies that even a multiplicative approximation remains #P-hard to compute. The hardness result even translates to permanents of orthogonal matrices over the finite field F_{p^4} for p != 2, 3. Interestingly, this characterization is tight: in fields of characteristic 2, the permanent coincides with the determinant; in fields of characteristic 3, one can efficiently compute the permanent of an orthogonal matrix by a nontrivial result of Kogan. Finally, we use more elementary arguments to prove #P-hardness for the permanent of a positive semidefinite matrix. This result shows that certain probabilities of boson sampling experiments with thermal states are hard to compute exactly, despite the fact that they can be efficiently sampled by a classical computer.
Cite as

Daniel Grier and Luke Schaeffer. New Hardness Results for the Permanent Using Linear Optics. In 33rd Computational Complexity Conference (CCC 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 102, pp. 19:1-19:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{grier_et_al:LIPIcs.CCC.2018.19,
  author =	{Grier, Daniel and Schaeffer, Luke},
  title =	{{New Hardness Results for the Permanent Using Linear Optics}},
  booktitle =	{33rd Computational Complexity Conference (CCC 2018)},
  pages =	{19:1--19:29},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-069-9},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{102},
  editor =	{Servedio, Rocco A.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2018.19},
  URN =		{urn:nbn:de:0030-drops-88702},
  doi =		{10.4230/LIPIcs.CCC.2018.19},
  annote =	{Keywords: Permanent, Linear optics, #P-hardness, Orthogonal matrices}
}
Document
DOI: 10.4230/LIPIcs.ITCS.2017.23
The Classification of Reversible Bit Operations

Authors: Scott Aaronson, Daniel Grier, and Luke Schaeffer

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

Abstract
We present a complete classification of all possible sets of classical reversible gates acting on bits, in terms of which reversible transformations they generate, assuming swaps and ancilla bits are available for free. Our classification can be seen as the reversible-computing analogue of Post's lattice, a central result in mathematical logic from the 1940s. It is a step toward the ambitious goal of classifying all possible quantum gate sets acting on qubits. Our theorem implies a linear-time algorithm (which we have implemented), that takes as input the truth tables of reversible gates G and H, and that decides whether G generates H. Previously, this problem was not even known to be decidable (though with effort, one can derive from abstract considerations an algorithm that takes triply-exponential time). The theorem also implies that any n-bit reversible circuit can be "compressed" to an equivalent circuit, over the same gates, that uses at most 2^{n}poly(n) gates and O(1) ancilla bits; these are the first upper bounds on these quantities known, and are close to optimal. Finally, the theorem implies that every non-degenerate reversible gate can implement either every reversible transformation, or every affine transformation, when restricted to an "encoded subspace." Briefly, the theorem says that every set of reversible gates generates either all reversible transformations on n-bit strings (as the Toffoli gate does); no transformations; all transformations that preserve Hamming weight (as the Fredkin gate does); all transformations that preserve Hamming weight mod k for some k; all affine transformations (as the Controlled-NOT gate does); all affine transformations that preserve Hamming weight mod 2 or mod 4, inner products mod 2, or a combination thereof; or a previous class augmented by a NOT or NOTNOT gate. Prior to this work, it was not even known that every class was finitely generated. Ruling out the possibility of additional classes, not in the list, requires involved arguments about polynomials, lattices, and Diophantine equations.
Cite as

Scott Aaronson, Daniel Grier, and Luke Schaeffer. The Classification of Reversible Bit Operations. In 8th Innovations in Theoretical Computer Science Conference (ITCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 67, pp. 23:1-23:34, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{aaronson_et_al:LIPIcs.ITCS.2017.23,
  author =	{Aaronson, Scott and Grier, Daniel and Schaeffer, Luke},
  title =	{{The Classification of Reversible Bit Operations}},
  booktitle =	{8th Innovations in Theoretical Computer Science Conference (ITCS 2017)},
  pages =	{23:1--23:34},
  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.23},
  URN =		{urn:nbn:de:0030-drops-81737},
  doi =		{10.4230/LIPIcs.ITCS.2017.23},
  annote =	{Keywords: Reversible computation, Reversible gates, Circuit synthesis, Gate classification, Boolean logic, Post’s lattice}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2016.12
On the Complexity of Probabilistic Trials for Hidden Satisfiability Problems

Authors: Itai Arad, Adam Bouland, Daniel Grier, Miklos Santha, Aarthi Sundaram, and Shengyu Zhang

Published in: LIPIcs, Volume 58, 41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016)

Abstract
What is the minimum amount of information and time needed to solve 2SAT? When the instance is known, it can be solved in polynomial time, but is this also possible without knowing the instance? Bei, Chen and Zhang (STOC'13) considered a model where the input is accessed by proposing possible assignments to a special oracle. This oracle, on encountering some constraint unsatisfied by the proposal, returns only the constraint index. It turns out that, in this model, even 1SAT cannot be solved in polynomial time unless P=NP. Hence, we consider a model in which the input is accessed by proposing probability distributions over assignments to the variables. The oracle then returns the index of the constraint that is most likely to be violated by this distribution. We show that the information obtained this way is sufficient to solve 1SAT in polynomial time, even when the clauses can be repeated. For 2SAT, as long as there are no repeated clauses, in polynomial time we can even learn an equivalent formula for the hidden instance and hence also solve it. Furthermore, we extend these results to the quantum regime. We show that in this setting 1QSAT can be solved in polynomial time up to constant precision, and 2QSAT can be learnt in polynomial time up to inverse polynomial precision.
Cite as

Itai Arad, Adam Bouland, Daniel Grier, Miklos Santha, Aarthi Sundaram, and Shengyu Zhang. On the Complexity of Probabilistic Trials for Hidden Satisfiability Problems. In 41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 58, pp. 12:1-12:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{arad_et_al:LIPIcs.MFCS.2016.12,
  author =	{Arad, Itai and Bouland, Adam and Grier, Daniel and Santha, Miklos and Sundaram, Aarthi and Zhang, Shengyu},
  title =	{{On the Complexity of Probabilistic Trials for Hidden Satisfiability Problems}},
  booktitle =	{41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016)},
  pages =	{12:1--12:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-016-3},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{58},
  editor =	{Faliszewski, Piotr and Muscholl, Anca and Niedermeier, Rolf},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2016.12},
  URN =		{urn:nbn:de:0030-drops-64284},
  doi =		{10.4230/LIPIcs.MFCS.2016.12},
  annote =	{Keywords: computational complexity, satisfiability problems, trial and error, quantum computing, learning theory}
}
  • Refine by Author
  • 3 Grier, Daniel
  • 2 Schaeffer, Luke
  • 1 Aaronson, Scott
  • 1 Anderson, Sean
  • 1 Arad, Itai
  • Show More...

  • Refine by Classification
  • 1 Security and privacy → Logic and verification
  • 1 Software and its engineering → Compilers
  • 1 Software and its engineering → Semantics
  • 1 Theory of computation
  • 1 Theory of computation → Circuit complexity
  • Show More...

  • Refine by Keyword
  • 1 #P-hardness
  • 1 Boolean logic
  • 1 C language semantics
  • 1 Circuit synthesis
  • 1 Compiler verification
  • Show More...

  • Refine by Type
  • 6 document

  • Refine by Publication Year
  • 1 2016
  • 1 2017
  • 1 2018
  • 1 2019
  • 1 2021
  • Show More...

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