26,098 papers · page 42 of 1,305
Differential privacy is a statistical definition of privacy that has attracted the interest of both academia and industry. Its formulations are easy to understand, but the differential privacy of databases is complicated to determine. One of the reasons for this is that small cha…
In this paper, we present an Isabelle/HOL formalization of co-rewrite pairs for non-reachability analysis in term rewriting. In particular, we formalize polynomial interpretations over negative integers as well as the weighted path order (WPO) and its variant co-WPO. With this fo…
The paper "Sorting with Bialgebras and Distributive Laws" by Hinze et al. uses the framework of bialgebraic semantics to define sorting algorithms. From distributive laws between functors they construct pairs of sorting algorithms using both folds and unfolds. Pairs of sorting al…
This paper presents a semantic characterization of leakage-freeness through timing side-channels for Jasmin programs. Our characterization covers probabilistic Jasmin programs that are not constant-time. In addition, we provide a characterization in terms of probabilistic relatio…
Number fields and their rings of integers, which generalize the rational numbers and the integers, are foundational objects in number theory. There are several computer algebra systems and databases concerned with the computational aspects of these. In particular, computing the r…
Monadic interpreters have gained attention as a powerful tool for modeling and reasoning about first order languages. In particular in the Coq ecosystem, the Choice Tree (CTree) library provides generic tools to craft such interpreters in presence of divergence, stateful effects,…
Regular expressions can be extended with lookarounds for contextual matching. This paper discusses a Coq formalization of the theory of regular expressions with lookarounds. We provide an efficient and purely functional algorithm for matching expressions with lookarounds and veri…
The Burrows-Wheeler transform (BWT) is an invertible lossless transformation that permutes input sequences into alternate sequences of the same length that frequently contain long localized regions that involve clusters consisting of just a few distinct symbols, and sometimes als…
Proof assistants like Isabelle/HOL provide the perfect opportunity to develop more than just one-off formalizations, but frameworks for developing new results within a given area. Completeness results for logical calculi often include bespoke versions of Lindenbaum's lemma. In th…
As the standardization process for post-quantum cryptography progresses, the need for computer-verified security proofs against classical and quantum attackers increases. Even though some tools are already tackling this issue, none are foundational. We take a first step in this d…
We present a library of formalized results around symmetric functions and the character theory of symmetric groups. Written in Coq/Rocq and based on the Mathematical Components library, it covers a large part of the contents of a graduate level textbook in the field. The flagship…
Just as imaginary numbers extend real numbers and simplify certain mathematical proofs, we introduce the concept of imaginary specifications to enhance program verification. In mathematics, imaginary numbers enable expressing intermediate steps that cannot be captured using real …
We report on the formalization of a sufficient condition for confluence of first-order left-linear rewrite systems within the proof assistant Isabelle/HOL. This criterion, originally proposed by Okui (1998), is based on simultaneous critical pairs, which finitely represent peaks …
White-box proof search tactics such as Coq's auto, Isabelle's auto and Lean's Aesop apply proof rules that often translate directly to lower-level tactics. When these search tactics find a proof, they can, at least in principle, generate a tactic script, i.e. a sequence of lower-…
We contribute CertiCoq-Wasm, a verified WebAssembly backend for CertiCoq. CertiCoq-Wasm is implemented and verified in the Coq proof assistant, and is mechanised with respect to the WasmCert-Coq formalisation of the WebAssembly standard. CertiCoq-Wasm works from CertiCoq's minima…
Post Correspondence Problem (PCP) is a classic example of an undecidable problem, with various heuristic algorithms proposed to tackle its instances. In this study, we focus on solving a particular subset of instances known as PCP[3,4]. We introduce a novel algorithm that leverag…
A fault attack is a malicious manipulation of the hardware (e.g., electromagnetic or laser pulse) that modifies the behavior of the software. Fault attacks typically target sensitive applications such as cryptography services, authentication, boot-loaders or firmware updaters. Th…
As mathematics becomes increasingly complicated, the prospect of using a computer proof assistant to (i) certify the correctness of one’s own work and (ii) interact with the formalized mathematical literature becomes increasingly attractive. In this talk, we will describe some ch…
Matching logic is the foundation of the K semantic environment for the specification of programming languages and automated generation of evaluators and verification tools. NLML is a formalization of nominal logic, which facilitates specification and reasoning about languages wit…
As separation logic is a logic of resources, the way in which resources can soundly change and be updated is a fundamental aspect. Such changes have typically been restricted to certain local or frame-preserving updates. However, recently we have seen separation logics where the …