相关论文: Formal verification in Coq of program properties i…

Theory of choreographic languages typically includes a number of complex results that are proved by structural induction. The high number of cases and the subtle details in some of them lead to long reviewing processes, and occasionally to…

This report presents a formalization of May's theorem in the proof assistant Coq. It describes how the theorem statement is first translated into Coq definitions, and how it is subsequently proved. Various aspects of the proof and related…

As new advancements in the field of quantum computing lead to the development of increasingly complex programs, approaches to validate and debug these programs are becoming more important. To this end, methods employed in classical…

The compactness lemma in programming language theory states that any recursive function can be simulated by a finite unrolling of the function. One important use case it has is in the logical relations proof technique for proving properties…

Some aspects of the physical nature of language are discussed. In particular, physical models of language must exist that are efficiently implementable. The existence requirement is essential because without physical models no communication…

The interplay between process behaviour and spatial aspects of computation has become more and more relevant in Computer Science, especially in the field of collective adaptive systems, but also, more generally, when dealing with systems…

For years, Integrated Development Environments have demonstrated their usefulness in order to ease the development of software. High-level security or safety systems require proofs of compliance to standards, based on analyses such as code…

With recent progress on experimental quantum information processing, an important question has arisen as to whether it is possible to verify arbitrary computation performed on a quantum processor. A number of protocols have been proposed to…

In this paper, we show a new approach to transformations of an imperative program with function calls and global variables into a logically constrained term rewriting system. The resulting system represents transitions of the whole…

The paper gives a detailed presentation of a framework, embedded into the simply typed higher-order logic and aimed at the support of sound and structured reasoning about various properties of models of imperative programs with interleaved…

Probabilistic programming provides a convenient lingua franca for writing succinct and rigorous descriptions of probabilistic models and inference tasks. Several probabilistic programming languages, including Anglican, Church or Hakaru,…

Relational verification of quantum programs has many potential applications in quantum and post-quantum security and other domains. We propose a relational program logic for quantum programs. The interpretation of our logic is based on a…

Qubits are a great way to build a quantum computer, but a limited way to program one. We replace the usual "states and gates" formalism with a "props and ops" (propositions and operators) model in which (a) the C*-algebra of observables…

Formal verification has been successfully developed in computer science for verifying combinatorial classes of models and specifications. In like manner, formal verification methods have been developed for dynamical systems. However, the…

We consider the problem of automated reasoning about dynamically manipulated data structures. The state-of-the-art methods are limited to the unfold-and-match (U+M) paradigm, where predicates are transformed via (un)folding operations…

In this paper, we present a formalization of Kozen's propositional modal $\mu$-calculus, in the Calculus of Inductive Constructions. We address several problematic issues, such as the use of higher-order abstract syntax in inductive sets in…

VeriFast is a powerful tool for verification of various correctness properties of C programs using symbolic execution. However, VeriFast itself has not been verified. We present a proof-of-concept extension which generates a correctness…

Term rewriting systems have a simple syntax and semantics and facilitate proofs of correctness. However, they are not as popular in industry or academia as imperative languages. We define a term rewriting based abstract programming language…

We formulate a framework for describing behaviour of effectful higher-order recursive programs. Examples of effects are implemented using effect operations, and include: execution cost, nondeterminism, global store and interaction with a…

In this paper, we introduce a system called GamePad that can be used to explore the application of machine learning methods to theorem proving in the Coq proof assistant. Interactive theorem provers such as Coq enable users to construct…