613 papers · page 2 of 31
On Computational Indistinguishability and Logical Relations
Relative Completeness of Incorrectness Separation Logic
Abstract Incorrectness Separation Logic (ISL) is a proof system that is tailored specifically to resolve problems of under-approximation in programs that manipulate heaps, and it primarily focuses on bug detection. This approach is different from the over-approximation methods th…
Building a Correct-by-Construction Type Checker for a Dependently Typed Core Language
Generic Reasoning of the Locally Nameless Representation
Random-Access Lists, from EE to FP
Effective Search Space Pruning for Testing Deep Neural Networks
Efficiently Adapting Stateless Model Checking for C11/C++11 to Mixed-Size Accesses
Abstract Stateless model checking (SMC) is crucial for productivity in verified concurrent programming, and its recent developments for C/C++ and weak memory models are remarkable. The state-of-the-art SMC for C, GenMC, efficiently verifies C programs based on C11 atomics and pth…
OBRA: Oracle-Based, Relational, Algorithmic Type Verification
Explaining Explanations in Probabilistic Logic Programming
Type-Based Verification of Connectivity Constraints in Lattice Surgery
Abstract Fault-tolerant quantum computation using lattice surgery can be abstracted as operations on graphs, wherein each logical qubit corresponds to a vertex of the graph, and multi-qubit measurements are accomplished by connecting the vertices with paths between them. Operatio…
A Diamond Machine for Strong Evaluation
Oracle Computability and Turing Reducibility in the Calculus of Inductive Constructions
m-CFA Exhibits Perfect Stack Precision
Typed Non-determinism in Functional and Concurrent Calculi
Argument Reduction of Constrained Horn Clauses Using Equality Constraints
Transport via Partial Galois Connections and Equivalences
Multiple types can represent the same concept. For example, lists and trees can both represent sets. Unfortunately, this easily leads to incomplete libraries: some set-operations may only be available on lists, others only on trees. Similarly, subtypes and quotients are commonly …