Related papers: Affine automata verifiers
We introduce a logic to express structural properties of automata with string inputs and, possibly, outputs in some monoid. In this logic, the set of predicates talking about the output values is parametric, and we provide sufficient…
An introductory formal languages course exposes advanced undergraduate and early graduate students to automata theory, grammars, constructive proofs, computability, and decidability. Programming students find these topics to be challenging…
Quantum finite automata have been studied intensively since their introduction in late 1990s as a natural model of a quantum computer with finite-dimensional quantum memory space. This paper seeks their direct application to interactive…
In previous work we describe a novel approach to dependent typing based on a multivalued term language. In this technical report we formalise the runtime, a kind of operational semantics, for that language. We describe a fairly…
We build a SAT solver implementing the DPLL algorithm in the verification-enabled programming language Dafny. The resulting solver is fully verified (soundness, completeness and termination are computer checked). We benchmark our Dafny…
We study the classical problem of verifying programs with respect to formal specifications given in the linear temporal logic (LTL). We first present novel sound and complete witnesses for LTL verification over imperative programs. Our…
Scalable and automatic formal verification for concurrent systems is always demanding. In this paper, we propose a verification framework to support automated compositional reasoning for concurrent programs with shared variables. Our…
In this paper, we present a proof of the NP-completeness of computing the smallest Deterministic Finite Automaton (DFA) that distinguishes two given regular languages as DFAs. A distinguishing DFA is an automaton that recognizes a language…
We present an efficient proof system for Multipoint Arithmetic Circuit Evaluation: for every arithmetic circuit $C(x_1,\ldots,x_n)$ of size $s$ and degree $d$ over a field ${\mathbb F}$, and any inputs $a_1,\ldots,a_K \in {\mathbb F}^n$,…
$\omega$-regular languages are a natural extension of the regular languages to the setting of infinite words. Likewise, they are recognised by a host of automata models, one of the most important being Alternating Parity Automata (APAs), a…
Building on work by Alfonseca et al. (2021), we study the conditions necessary for it to be logically possible to prove that an arbitrary artificially intelligent machine will exhibit certain behavior. To do this, we develop a formalism…
Writing accurate numerical software is hard because of many sources of unavoidable uncertainties, including finite numerical precision of implementations. We present a programming model where the user writes a program in a real-valued…
We consider the problem of automatically verifying programs which manipulate arbitrary data structures. Our specification language is expressive, contains a notion of \emph{separation}, and thus enables a precise specification of…
Smale's alpha-theory uses estimates related to the convergence of Newton's method to give criteria implying that Newton iterations will converge quadratically to solutions to a square polynomial system. The program alphaCertified implements…
We give a process for verifying numerical programs against their functional specifications. Our implementation is capable of automatically verifying programs against tight error bounds featuring common elementary functions. We demonstrate…
Signature verification is a critical task in many applications, including forensic science, legal judgments, and financial markets. However, current signature verification systems are often difficult to explain, which can limit their…
A number of flexible tactic-based logical frameworks are nowadays available that can implement a wide range of mathematical theories using a common higher-order metalanguage. Used as proof assistants, one of the advantages of such powerful…
Despite the vast body of research literature proposing algorithms with formal guarantees, the amount of verifiable code in today's systems remains minimal. This discrepancy stems from the inherent difficulty of verifying code, particularly…
In deductive verification and software model checking, dealing with certain specification language constructs can be problematic when the back-end solver is not sufficiently powerful or lacks the required theories. One way to deal with this…
While prior work established a verifier-based polynomial-time framework for NP, explicit deterministic machines for concrete NP-complete problems have remained elusive. In this paper, we construct fully specified deterministic Turing…