计算机科学中的逻辑

Logics for resource-bounded agents have been getting more and more attention in recent years since they provide us with more realistic tools for modelling and reasoning about multi-agent systems. While many existing approaches are based on…

We propose to study transformations on graphs, and more generally structures, by looking at how the cut-rank (as introduced by Oum) of subsets is affected when going from the input structure to the output structure. We consider…

A bottleneck in modern active automata learning is to test whether a hypothesized Mealy machine correctly describes the system under learning. The search space for possible counterexamples is given by so-called test suites, consisting of…

Blockchains are decentralized systems that provide trustable execution guarantees. Smart contracts are programs written in specialized programming languages running on blockchains that govern how tokens and cryptocurrency are sent and…

The textbook proofs of Commoner's theorem characterizing liveness in free-choice Petri nets are given in contexts of technical notions and claims that make the proofs look a bit long. The aim of this note is to give a concise self-contained…

We formally introduce IsaVODEs (Isabelle verification with Ordinary Differential Equations), a framework for the verification of cyber-physical systems. We describe the semantic foundations of the framework's formalisation in the…

In 1926-1927, Tarski designed a set of axioms for Euclidean geometry which reached its final form in a manuscript by Schwabh\"auser, Szmielew and Tarski in 1983. The differences amount to simplifications obtained by Tarski and Gupta. Gupta…

Proof assistants like Coq are increasingly popular to help mathematicians carry out proofs of the results they conjecture. However, formal proofs remain highly technical and are especially difficult to reuse. In this paper, we present a…

Since its establishment, propositional dynamic logic (PDL) has been a subject of intensive academic research and frequent use in the industry. We have studied the complexity of some PDL problems and in this paper, we show results for some…

Given a Linear Temporal Logic (LTL) formula over input and output variables, reactive synthesis requires us to design a deterministic Mealy machine that gives the values of outputs at every time step for every sequence of inputs, such that…

We study propositional proof systems with inference rules that formalize restricted versions of the ability to make assumptions that hold without loss of generality, commonly used informally to shorten proofs. Each system we study is built…

Current static verification techniques support a wide range of programs. However, such techniques only support complete and detailed specifications, which places an undue burden on users. To solve this problem, prior work proposed gradual…

While most of the current synthesis algorithms only focus on correctness-by-construction, ensuring robustness has remained a challenge. Hence, in this paper, we address the robust-by-construction synthesis problem by considering the…

It is widely accepted that every system should be robust in that ``small'' violations of environment assumptions should lead to ``small'' violations of system guarantees, but it is less clear how to make this intuition mathematically…

The HaliVer tool integrates deductive verification into the popular scheduling language Halide, used for image processing pipelines and array computations. HaliVer uses Vercors, a separation logic-based verifier, to verify the correctness…

ADG is a forum to exchange ideas and views, to present research results and progress, and to demonstrate software tools at the intersection between geometry and automated deduction. The conference is held every two years. The previous…

Characterizing programming languages with variable binding as initial objects, was first achieved by Fiore, Plotkin, and Turi in their seminal paper published at LICS'99. To do so, in particular to prove initiality theorems, they developed…

The real numbers are important in both mathematics and computation theory. Computationally, real numbers can be represented in several ways; most commonly using inexact floating-point data-types, but also using exact arbitrary-precision…

Formalised libraries of combinatorial mathematics have rapidly expanded over the last five years, but few use one of the most important tools: probability. How can often intuitive probabilistic arguments on the existence of combinatorial…

Computing schedulers that optimize reachability probabilities in MDPs is a standard verification task. To address scalability concerns, we focus on MDPs that are compositionally described in a high-level description formalism. In…