计算机科学中的逻辑

The graph parameter shrub-depth is a dense analog of tree-depth. We characterize classes of bounded shrub-depth by forbidden induced subgraphs. The obstructions are well-controlled flips of large half-graphs and of disjoint unions of many…

Creating safe concurrent algorithms is challenging and error-prone. For this reason, a formal verification framework is necessary especially when those concurrent algorithms are used in safety-critical systems. The goal of this guide is to…

In this work, we generalize the concept of bisimulation metric in order to metrize the behaviour of continuous-time processes. Similarly to what is done for discrete-time systems, we follow two approaches and show that they coincide: as a…

De Nicola and Hennessy's must-preorder is a contextual refinement which states that a server q refines a server p if all clients satisfied by p are also satisfied by q. Owing to the universal quantification over clients, this definition…

Computing many useful properties of Boolean formulas, such as their weighted or unweighted model count, is intractable on general representations. It can become tractable when formulas are expressed in a special form, such as the decision…

This note discusses our formalisation in Lean of the classification of the groups of order $p q$ for (not necessarily distinct) prime numbers $p$ and $q$, together with various intermediate results such as the characterisation of internal…

We provide a finite equational presentation of graphs of treewidth at most three, solving an instanceof an open problem by Courcelle and Engelfriet. We use a syntax generalising series-parallel expressions, denoting graphs with a small…

Dependency pairs (DPs) are one of the most powerful techniques for automated termination analysis of term rewrite systems. Recently, we adapted the DP framework to the probabilistic setting to prove almost-sure termination (AST) via…

Nielsen transformations form the basis of a simple and widely used procedure for solving word equations. We make progress on the problem of determining when this procedure terminates in the presence of length constraints. To do this, we…

The possibility of errors in human-engineered formal verification software, such as model checkers, poses a serious threat to the purpose of these tools. An established approach to mitigate this problem are certificates -- lightweight,…

Deductive verification has become a mature paradigm for the verification of industrial software. Applying deductive verification, however, requires that every function in the code base is annotated with a function contract specifying its…

The formalisation of mathematics is starting to become routine, but the value of this technology to the work of mathematicians remains to be shown. There are few examples of using proof assistants to verify brand-new work. This paper…

Authenticated data structures allow untrusted third parties to carry out operations which produce proofs that can be used to verify an operation's output. Such data structures are challenging to develop and implement correctly. This paper…

Assurance cases offer a structured way to present arguments and evidence for certification of systems where safety and security are critical. However, creating and evaluating these assurance cases can be complex and challenging, even for…

We propose a stable model semantics for higher-order logic programs. Our semantics is developed using Approximation Fixpoint Theory (AFT), a powerful formalism that has successfully been used to give meaning to diverse non-monotonic…

Property-based testing (PBT) is a technique for validating code against an executable specification by automatically generating test-data. We present a proof-theoretical reconstruction of this style of testing for relational specifications…

In this note, we introduce the notion of support graph to define explanations for any model of a logic program. An explanation is an acyclic support graph that, for each true atom in the model, induces a proof in terms of program rules…

In this paper we show how prescritive type checking and constraint solving can be combined to increase automation during software verification. We do so by defining a type system and implementing a typechecker for {log} (read `setlog'), a…

Recently, we have proposed a framework for verification of agents' abilities in asynchronous multi-agent systems, together with an algorithm for automated reduction of models. The semantics was built on the modeling tradition of distributed…

Core spanners are a class of document spanners that capture the core functionality of IBM's AQL. FC is a logic on strings built around word equations that when extended with constraints for regular languages can be seen as a logic for core…