ABSTRACT. This paper contributes to the theory of typed first-order logic. We present a sound and complete axiomatization lifting restriction imposed by previous results. We resolve an issue with modular reasoning. As a third contribution this paper provides complete axiomatizations for the type predicates $instance_{T}$, $exactInstance_{T}$, and functions $cast_{T}$ indispensible for reasoning about object-oriented programming languges.

ABSTRACT. We compare and contrast our experiences in specifying, implementing and verifying the monotonicity property of a simple plurality voting scheme using modern light-weight and heavy-weight verification tools.

ABSTRACT. Compiler verification is difficult and expensive. Instead of formally verifying a compiler, we introduce a sound deductive compilation approach, whereby verified bytecode is generated based on symbolic execution of source code embedded in a program logic. The generated bytecode is weakly bisimilar to the original source code relative to a set of observable locations. The framework is instantiated for Java source and bytecode. The compilation process is fully automatic and first-order solvers are employed for bytecode optimization.

ABSTRACT. In this paper, we discuss the challenge of verifying a system which does not exist today, but may be of the utmost importance in the future: an Artificial General Intelligence (AGI) as smart or smarter than human beings, and capable of improving itself further.

A self-improving AGI with the potential to become more powerful than any human would be a system we'd need to design for safety from the ground up. We argue that this will lead to foreseeable technical difficulties which we can and should start working on today, despite the fact that we do not yet know how to build an AGI. In this paper, we focus on one particular such difficulty: We could require an AGI to exhibit a formal proof that each of its actions and self-rewrites satisfy a certain safety property, and otherwise switch to a baseline controller (a variation on the well-known simplex architecture), but straight-forward ways of implementing this for a self-rewriting AGI run into problems related to Gödel's incompleteness theorems. We review several potential solutions to this problem and discuss reasons to think that it is likely to be an issue for a wide variety of potential approaches to constructing a safe self-improving AGI.

ABSTRACT. In the ForMaRE project formal mathematical reasoning is applied to economics. After an initial exploratory phase, it focused on auction theory and has produced, as its first results, formalized theorems and certified executable code.

ABSTRACT. Regression verification is an approach to prevent regressions in software development using formal verification. The goal is to prove that two versions of a program behave equally or differ in a specified way. We worked on an approach for regression verification, extending Strichman and Godlin's work by relational equivalence and two ways of using counterexamples.