Dependent Type-Checking Modulo Associativity and Commutativity

Writing software that follows its specification is important for many applications. One approach to guarantee this is formal verification in a dependently-typed programming language. Formal verification in these dependently-typed languages is based on proof writing. Sadly, while proofs are easy to check for computers, writing proofs can be...

Formally proving the correctness of the (un)currying refactoring: Using Agda with a simple Haskell-like programming language

When designing critical software, great care must be taken to guarantee its correctness. Refactoring is one of the techniques used to improve code readability, maintainability, and other factors without changing functionality. Thus, to ensure that it is properly applied, automated tools are used to perform refactoring. To ensure that the code...

Maybe a List would be better?: Correct by construction Maybe to List refactorings in a Haskell-like language

This paper concerns itself with correct by construction refactoring of Maybe values to List values in a Haskell-like language (HLL) as a case study on data-oriented refactorings. Our language makes use of intrinsically-typed syntax and de Bruijn indices for variables. Operational semantics are defined using big step semantics. We define a...

Mechanizing Hoare Style Proof Outlines for Imperative Programs in Agda

Formal verification of imperative programs can be carried out on paper by annotating programs to obtain an outline of a proof in the style of Hoare. This process has been mechanized by the introduction of Separation Logic and computer assisted verification tools. However, the tools fail to achieve the readability and convenience of manual paper...

Netlist Level Based Fault Injection Simulation

The issue of securing microchip designs against hardware attacks has grown in magnitude as more and more embedded systems are deployed in hostile environments, where security measures have to be taken to prevent attackers from accessing unwanted information.<br/>The first step in solving this problem is gaining awareness of the security...

Practical Verification of the Inductive Graph Library

Formal verification works better than testing, since the correctness of a program is proven. It is researched if it is possible and feasible to formally verify the Inductive Graph Library. The library is an abstract class in Haskell and is ported manually to Agda. Agda is a total and dependently typed language and thus can be used as a proof...

Lunar Zebro - Software Design Of The Locomotion Sub-System With The Dezyne Model Driven Development Tool

The TU Delft ZEs-Benige RObot (Zebro) project is presented with the opportunity to bring the Zebro concept to the surface of our moon. To maximise the probability of success, the Locomotion Sub-System (LSS) software of Lunar Zebro is developed using a novel model-driven design tool called Dezyne. Dezyne uses a proprietary language to describe...

Formal Abstraction of Stochastic Systems: Bringing Theory into Practice

Recent developed theories in the field of formal abstraction of stochastic systems have provided new methods for solving the safety and reach-avoid problems. These new methods have been extended to fit controlled stochastic systems, resulting in a policy that optimizes the safety and reach-avoid probabilities. The goal of this thesis is to put...