Lööw, Andreas Nantes-Sobrinho, Daniele Ayoun, Sacha-Élie Cronjäger, Caroline Maksimović, Petar Gardner, Philippa

The introduction of separation logic has led to the development of symbolic execution techniques and tools that are (functionally) compositional with function specifications that can be used in broader calling contexts. Many of the compositional symbolic execution tools developed in academia and industry have been grounded on a formal foundation, b...

Białecki, Tomasz Rybotycki, Tomasz Tworzydło, Jakub Bednorz, Adam
Published in
Frontiers in Physics

We analyze the results of the test of π/2 qubit rotations on a public quantum computer provided by IBM. We measure a single qubit rotated by π/2 about a random axis, and we accumulate vast statistics of the results. The test performed on different devices shows systematic deviations from the theoretical predictions, which appear at level 10–3. Some...

Abbasi, Fateme Banerjee, Sandip Byrka, Jarosław Chalermsook, Parinya Gadekar, Ameet Khodamoradi, Kamyar Marx, Dániel Sharma, Roohani Spoerhase, Joachim

We consider the well-studied Robust $(k, z)$-Clustering problem, which generalizes the classic $k$-Median, $k$-Means, and $k$-Center problems. Given a constant $z\ge 1$, the input to Robust $(k, z)$-Clustering is a set $P$ of $n$ weighted points in a metric space $(M,\delta)$ and a positive integer $k$. Further, each point belongs to one (or more) ...

Gürpınar, Emirhan Romashchenko, Andrei

It is known that the mutual information, in the sense of Kolmogorov complexity, of any pair of strings x and y is equal to the length of the longest shared secret key that two parties can establish via a probabilistic protocol with interaction on a public channel, assuming that the parties hold as their inputs x and y respectively. We determine the...

Dartois, Luc Gastin, Paul Germerie Guizouarn, Loïc Govind, R. Krishna, Shankaranarayanan

Deterministic two-way transducers capture the class of regular functions. The efficiency of composing two-way transducers has a direct implication in algorithmic problems related to synthesis, where transformation specifications are converted into equivalent transducers. These specifications are presented in a modular way, and composing the resulta...

Leray, Yann Gilbert, Gaëtan Tabareau, Nicolas Winterhalter, Théo

In dependently typed proof assistants, users can declare axioms to extend the ambient logic locally with new principles and propositional equalities governing them. Additionally, rewrite rules have recently been proposed to allow users to extend the logic with new definitional equalities, enabling them to handle new principles with a computational ...

Faissole, Florian Geneau de Lamarlière, Paul Melquiond, Guillaume

Designing an efficient yet accurate floating-point approximation of a mathematical function is an intricate and error-prone process. This warrants the use of formal methods, especially formal proof, to achieve some degree of confidence in the implementation. Unfortunately, the lack of automation or its poor interplay with the more manual parts of t...

Chen, Kuo-Chin Apers, Simon Hsieh, Min-Hsiu

This study examines clusterability testing for a signed graph in the bounded-degree model. Our contributions are two-fold. First, we provide a quantum algorithm with query complexity Õ(N^{1/3}) for testing clusterability, which yields a polynomial speedup over the best classical clusterability tester known [Adriaens and Apers, 2023]. Second, we pr...

Yung, Kingsley

The random k-XORSAT problem is a random constraint satisfaction problem of n Boolean variables and m = rn clauses, which a random instance can be expressed as a G𝔽(2) linear system of the form Ax = b, where A is a random m × n matrix with k ones per row, and b is a random vector. It is known that there exist two distinct thresholds r_{core}(k) r_{...

Das, Syamantak Kumar, Nikhil Vaz, Daniel

Flow sparsification is a classic graph compression technique which, given a capacitated graph G on k terminals, aims to construct another capacitated graph H, called a flow sparsifier, that preserves, either exactly or approximately, every multicommodity flow between terminals (ideally, with size as a small function of k). Cut sparsifiers are a res...