14,842 papers · page 4 of 743
Abstract Efforts to verify Zero-Knowledge Proof circuit encodings have highlighted the challenge of proving the correctness of quantifier-free statements that make use of both bitvector and finite field operations. Existing verification workflows are either manual or rely on SMT …
Abstract Reasoning about array data structures is a key requirement for many applications in hardware and software verification, especially in combination with machine integers. The Satisfiability Modulo Theories (SMT) theory of extensional arrays provides array read and write op…
Abstract We present the Cooperating Proof Calculus (CPC), an evolving set of proof rules encompassing all inferences used in the mainstream theories of the SMT solver cvc5. CPC consists of 585 proof rules, which are formalized in 8025 lines of definitions in the logical framework…
Abstract At the core of modern electronic design automation (EDA) tools is rewriting : a mechanism by which local transformations are iteratively applied to circuits to make them faster and more efficient. These rewrites are crucial for producing high-quality hardware, and they o…
Abstract Neural network verification is an active and rapidly maturing research area, with a growing ecosystem of solvers and tools. The VNN-LIB standard was introduced to support interoperability in this ecosystem, but Version 1.0 has several serious short-comings as a formal fo…
Abstract In recent years, protocol state fuzzing has emerged as an effective technique to analyze and test network protocol implementations, uncovering numerous security vulnerabilities, bugs, and non-conformance issues in them. This paper presents ProtocolState-Fuzzer ( PSF ), a…
Abstract Consistency-based diagnosis is a formal approach to software fault localization that explains failing executions by identifying program components whose modification would restore correctness. Tools such as BugAssist and (more recently) CFaults instantiate this idea usin…
Abstract The reliability of autonomous systems depends on their robustness, i.e., their ability to meet their objectives under uncertainty. In this paper, we study spatiotemporal robustness of temporal logic specifications evaluated over discrete-time signals. Existing work has p…
Abstract This tool paper presents the latest (2026) version of Mallob – a distributed platform for automated reasoning on demand. Mallob features a world-leading distributed SAT solving engine, which is the first of its kind that supports proof checking, incremental SAT queries, …
Abstract is a deductive verifier for probabilistic programs. At its core lies , a quantitative intermediate verification language based on the real-valued logic . allows users to express a probabilistic program, its specifications, and proof rules in a programming-language style,…
Abstract Burrow is a proof framework for weak memory mapping proofs. Those mappings appear as optimizations and translations between languages inside compilers and binary translators. However, their mechanized proofs, when defined over formal axiomatic weak memory semantics, are …
Abstract Modern neural network verifiers often encode neural network verification as constraint satisfaction problems. When dealing with standard piecewise-linear activation functions, such as ReLUs, verifiers typically employ branching heuristics that break a complex constraint …
Abstract We present a case study on proof-driven software understanding of mature, security-critical infrastructure. While formal methods are traditionally applied during the design phase, we present our experience applying formal reasoning onto a mature industrial C++ codebase. …
Abstract Hoare-style verification provides a principled foundation for reasoning about the correctness of quantum programs, but existing approaches do not allow fully automatic verification. While automata-based verification scales well when specifications are given directly as a…
Abstract We study the fully automated amortised analysis of purely functional data structures like skew heaps , as well as weight - and rank-biased leftist heaps. For that we generalise earlier works on automated amortised resource analysis by developing a type inference based ap…
Abstract Formal verification is paramount for neural networks in safety-critical domains yet remains constrained by the trade-off between precision and scalability, especially with modern high frequency activation functions. However, the inherent NP-hardness of the problem forces…
Abstract Mutexes are fundamental synchronization primitives in concurrent programming, but their improper use can lead to deadlocks. Conventional assume-based modeling abstracts mutex semantics via assumptions, simplifying safety verification but hindering deadlock verification. …
Abstract Verifying stateful software systems remains challenging due to complex control structures and intricate state interactions, often necessitating pre-existing behavioral models. We introduce , an abstract interpreter that automatically derives sound and precise symbolic fi…
Abstract Matrix product states (MPS) are a standard tensor-network representation for ground states of one-dimensional quantum many-body systems, and they underpin widely used simulation tools such as DMRG. However, while quantum model checking has been developed mainly for quant…
Abstract Formal hardware verification ensures that a design satisfies its specifications, but writing these specifications requires substantial manual effort. Specification mining automates this process, and existing work has their own merits. The classic approaches rely on pre-d…