计算机科学中的逻辑

In the synthesis problem, we are given a specification, and we automatically generate a system that satisfies the specification in all environments. We introduce and study {\em synthesis with guided environments} (SGE, for short), where the…

This paper contributes to the Alpay Algebra by demonstrating that the stable outcome of a self referential process, obtained by iterating a transformation through all ordinal stages, is identical to the unique equilibrium of an unbounded…

We present Lisp-Z3, an extension to the ACL2s systems programming framework (ASPF) that supports the use of the Z3 satisfiability modulo theories (SMT) solver. Lisp-Z3 allows one to develop tools written using the full feature set of Common…

Floodsub is a simple, robust and popular peer-to-peer publish/subscribe (pubsub) protocol, where nodes can arbitrarily leave or join the network, subscribe to or unsubscribe from topics and forward newly received messages to all of their…

Yul is an intermediate language used in the compilation of the Solidity programming language for Ethereum smart contracts. The compiler applies customizable sequences of transformations to Yul code. To help ensure the correctness of these…

We present an experimental, verified clause processor ctv-cp that fits into the framework used at Arm for formal verification of arithmetic hardware designs. This largely automates the ACL2 proof development effort for integer multiplier…

We present a simple ACL2 simulator for the RISC-V 32-bit base instruction set architecture, written in the operational semantics style. Like many other ISA models, our RISC-V state object is a single-threaded object and we prove…

The Schr\"oder-Bernstein theorem states that, for any two sets P and Q, if there exists an injection from P to Q and an injection from Q to P, then there must exist a bijection between the two sets. Classically, it follows that the ordering…

The ACL2 Workshop series is the major technical forum for users of the ACL2 theorem proving system to present research related to the ACL2 theorem prover and its applications. ACL2 is an industrial-strength automated reasoning system, the…

We show that, when the actions of a Mazurkiewicz trace are considered not merely as atomic (i.e., mere names) but transformations from a specified type of inputs to a specified type of outputs, we obtain a novel notion of presentation for…

We derive multiple program logics, including correctness, incorrectness, and relational Hoare logic, from the axioms of imperative categories: uniformly traced distributive copy-discard categories. We introduce an internal language for…

The most studied and accepted pseudometric for probabilistic processes is one based on the Kantorovich distance between distributions. It comes with many theoretical and motivating results, in particular it is the fixpoint of a given…

We present \texttt{muRelBench}, a framework for synthetic benchmarks for weakly-relational abstract domains and their operations. This extensible microbenchmarking framework enables researchers to experimentally evaluate proposed algorithms…

We present a new theoretical framework that unifies category-theoretic fixed-point constructions, transfinite recursion, and game-based semantics to model how interpretations of language can stabilize through unlimited self-reference. By…

Expansions of the monadic second-order (MSO) theory of the structure $\langle \mathbb{N} ; < \rangle$ have been a fertile and active area of research ever since the publication of the seminal papers of B\"uchi and Elgot & Rabin on the…

We introduce a language for formally reasoning about programs that combine differential constructs with probabilistic ones. The language harbours, for example, such systems as adaptive cruise controllers, continuous-time random walks, and…

We establish various complexity results for the entailment problem between formulas in Separation Logic with user-defined predicates denoting recursive data structures. The considered fragments are characterized by syntactic conditions on…

Fixpoints are ubiquitous in computer science as they play a central role in providing a meaning to recursive and cyclic definitions. Bisimilarity, behavioural metrics, termination probabilities for Markov chains and stochastic games are…

In this paper, we present a linear and reversible programming language with inductives types and recursion. The semantics of the languages is based on pattern-matching; we show how ensuring syntactical exhaustivity and non-overlapping of…

Quantified constraints over the reals appear in numerous contexts. Usually existential quantification occurs when some parameter can be chosen by the user of a system, and univeral quantification when the exact value of a parameter is…