计算机科学中的逻辑

We present realizability and realization logic, two program logics that jointly address the problem of finding solutions in semantics-guided synthesis. What is new is that we proceed eagerly and not only analyze a single candidate program…

One approach to probabilistic inference involves counting the number of models of a given Boolean formula. Here, we are interested in inferences involving higher-order objects, i.e., functions. We study the following task: Given a Boolean…

We present a generalization of first-order unification to a term algebra where variable indexing is part of the object language. We exploit variable indexing by associating some sequences of variables ($X_0,\ X_1,\ X_2,\dots$) with a…

Classically, in saturation-based proof systems, unification has been considered atomic. However, it is also possible to move unification to the calculus level, turning the steps of the unification algorithm into inferences. For calculi that…

In this article, we study the relationship between notions of depth for sequences, namely, Bennett's notions of strong and weak depth, and deep $\Pi^0_1$ classes, introduced by the authors and motivated by previous work of Levin. For the…

We present a first-order theorem proving framework for establishing the correctness of functional programs implementing sorting algorithms with recursive data structures. We formalize the semantics of recursive programs in many-sorted…

Hyperproperties relate multiple executions of a program and are commonly used to specify security and information-flow policies. Most existing work has focused on the verification of $k$-safety properties, i.e., properties that state that…

We introduce a novel quantum programming language featuring higher-order programs and quantum controlflow which ensures that all qubit transformations are unitary. Our language boasts a type system guaranteeingboth unitarity and…

A barrier certificate, defined over the states of a dynamical system, is a real-valued function whose zero level set characterizes an inductively verifiable state invariant separating reachable states from unsafe ones. When combined with…

Timed automata are the formal model for real-time systems. Extensions with discrete probabilistic branching have been considered in the literature and successfully applied. Probabilistic timed automata (PTA) do require all branching…

Pointer arithmetic is widely used in low-level programs, e.g. memory allocators. The specification of such programs usually requires using pointer arithmetic inside inductive definitions to define the common data structures, e.g. heap lists…

We consider the parameterized verification of arbitrarily large networks of agents which communicate by broadcasting and receiving messages. In our model, the broadcast topology is reconfigurable so that a sent message can be received by…

We give a lightweight alternative construction of Jacobs's distributive law for multisets and distributions that does not involve any combinatorics. We first give a distributive law for lists and distributions, then apply a general theorem…

Probabilistic model checking is a widely used formal verification technique to automatically verify qualitative and quantitative properties for probabilistic models. However, capturing such systems, writing corresponding properties, and…

Interlocking logics are at the core of critical systems controlling the traffic within stations. In this paper, we consider a generic interlocking logic, which can be instantiated to control a wide class of stations. We tackle the problem…

Much of the software we use in everyday life consists of distributed components (running on separate cores or even computers) that collaborate through communication (by exchanging messages). It is crucial to develop robust methods that can…

Binary classifiers are traditionally studied by propositional logic (PL). PL can only represent them as white boxes, under the assumption that the underlying Boolean function is fully known. Binary classifiers used in practical applications…

The optimization phase of a compiler is responsible for transforming an intermediate representation (IR) of a program into a more efficient form. Modern optimizers, such as that used in the GraalVM compiler, use an IR consisting of a…

Rewriting techniques based on reduction orderings generate "just enough" consequences to retain first-order completeness. This is ideal for superposition-based first-order theorem proving, but for at least one approach to inductive…

This paper addresses the problem of checking invariant properties for a large class of symbolic transition systems, defined by a combination of SMT theories and quantifiers. State variables can be functions from an uninterpreted sort…