Marko van Eekelen

Raphaela Butz, Renée Schulz, Arjen Hommersom et al.

Explaining predictions from Bayesian networks, for example to physicians, is non-trivial. Various explanation methods for Bayesian network inference have appeared in literature, focusing on different aspects of the underlying reasoning. While there has been a lot of technical research, there is very little known about how well humans actually understand these explanations. In this paper, we present ongoing research in which four different explanation approaches were compared through a survey by asking a group of human participants to interpret the explanations.

Andreas Schuderer, Stefano Bromuri, Marko van Eekelen

Reinforcement learning (RL) is one of the most active fields of AI research. Despite the interest demonstrated by the research community in reinforcement learning, the development methodology still lags behind, with a severe lack of standard APIs to foster the development of RL applications. OpenAI Gym is probably the most used environment to develop RL applications and simulations, but most of the abstractions proposed in such a framework are still assuming a semi-structured methodology. This is particularly relevant for agent-based models whose purpose is to analyse adaptive behaviour displayed by self-learning agents in the simulation. In order to bridge this gap, we present a workflow and tools for the decoupled development and maintenance of multi-purpose agent-based models and derived single-purpose reinforcement learning environments, enabling the researcher to swap out environments with ones representing different perspectives or different reward models, all while keeping the underlying domain model intact and separate. The Sim-Env Python library generates OpenAI-Gym-compatible reinforcement learning environments that use existing or purposely created domain models as their simulation back-ends. Its design emphasizes ease-of-use, modularity and code separation.

Marc Schoolderman, Jonathan Moerman, Sjaak Smetsers et al.

Code that is highly optimized poses a problem for program-level verification: programmers can employ various clever tricks that are non-trivial to reason about. For cryptography on low-power devices, it is nonetheless crucial that implementations be functionally correct, secure, and efficient. These are usually crafted in hand-optimized machine code that eschew conventional control flow as much as possible. We have formally verified such code: a library which implements elliptic curve cryptography on 8-bit AVR microcontrollers. The chosen implementation is the most efficient currently known for this microarchitecture. It consists of over 3000 lines of assembly instructions. Building on earlier work, we use the Why3 platform to model the code and prove verification conditions, using automated provers. We expect the approach to be re-usable and adaptable, and it allows for validation. Furthermore, an error in the original implementation was found and corrected, at the same time reducing its memory footprint. This shows that practical verification of cutting-edge code is not only possible, but can in fact add to its efficiency -- and is clearly necessary.

Hans-Dieter A. Hiep, Olaf Maathuis, Jinting Bian et al.

As a particular case study of the formal verification of state-of-the-art, real software, we discuss the specification and verification of a corrected version of the implementation of a linked list as provided by the Java Collection framework. Keywords: Java, standard library, deductive verification, KeY, Java Modeling Language, case study, bug