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.

ABSTRACT. We present an extension to an on-demand abstraction framework, which integrates deductive verification and abstract interpretation. Our extension allows for a significantly higher precision when reasoning about programs containing arrays. We demonstrate the usefulness of our approach in the context of reasoning about secure information flow. In addition to abstracting arrays that may have been modified, our approach can also keep full precision while adding additional information about array elements which have been only read but not modified.

ABSTRACT. A crucial point in program analysis is the computation of loop invariants. Accurate invariants are required to prove properties on a program but they are difficult to compute. Extensive research has been carried out but, to the best of our knowledge, no benchmark has ever been developed to compare algorithms and tools.

We present ALICe, a toolset to compare automatic computation techniques of affine loop scalar invariants. It comes with a benchmark that we built using 102 test cases which we found in the loop invariant bibliography, and interfaces with three analysis programs, that rely on different techniques: Aspic, isl and PIPS. Conversion tools are provided to handle format heterogeneity of these programs.

Experimental results show the importance of model coding and the poor performances of PIPS on concurrent loops. To tackle these issues, we use two model restructurations techniques whose correctness is proved in Coq, and discuss the improvements realized.

ABSTRACT. Some of the intrinsic limitations of the widely used static techniques for loop invariant inference can be offset by combining them with dynamic techniques---based on executing automatically generated tests. We show how useful loop invariant candidates can be generated by systematically mutating postconditions; then, we apply dynamic checking to weed out invalid candidates, and static checking to select provably valid ones. We present a framework that automatically applies these techniques to carry out functional correctness proofs without manually written loop invariants. Applied to 28 methods (including 39 different loops) from various java.util classes, our DynaMate prototype automatically discharged 97% of all proof obligations, resulting in automatic complete correctness proofs of 25 out of the 28 methods---outperforming several state-of-the-art tools for fully automatic functional verification of programs with loops.

ABSTRACT. The effectiveness of interactive theorem provers (ITPs) has increased in a way that the bottleneck in the interactive process shifted from effectiveness to efficiency. Proving large theorems still needs a lot of effort for the user interacting with the system. This issue is recognized by the ITP-communities and improvements are being developed. However, in contrast to properties like soundness or completeness, where rigorous methods are applied to provide evidence, the evidence for a better usability is lacking in many cases. Our contribution is the application of methods from the human-computer-interaction (HCI) field to ITPs. We report on the application of focus groups to evaluate the usability of Isabelle/HOL and the KeY system. We apply usability evaluation methods in order to a) detect usability issues in the interaction between ITPs and their users, and b) to analyze whether methods such as focus groups are applicable to the field of ITP.

ABSTRACT. We developed a method that allows to check the satisfiability of a formula in the combined theories of sets and the bridging functions card, sum, avg, min, max by using a prover for linear arithmetic. Since abstractions of certain verification task lie in this fragment, this method can be used for checking the behaviour of a program.

ABSTRACT. Motivated by the theory of relations on graphs and applications to spatial reasoning, we present a bi-intuitionistic logic BISKT with tense operators. The logic is shown to be decidable and have the effective finite model property. We present a sound, complete and terminating tableau calculus for the logic and use the MetTeL system to generate an implementation. A significant part of the presentation will focus on how we developed the calculus using our tableau synthesis framework and give a demonstration of how to use the MetTeL tableau prover generation tool.