- document
-
Wang, Sunny (author)While learning-based control techniques often outperform classical controller designs, safety requirements limit the acceptance of such methods in many applications. Recent developments address this issue through Certified Learning (CL), which combines a learning-based controller with formal methods to provide safety guarantees. This thesis...master thesis 2024
- document
-
van Bergeijk, Ferd (author)Model-based testing (MBT) is applied for the verification of simple simulation models used in modeling & simulation for decision-making. It is found that MBT of simulation models is not discussed much in literature, and that existing case studies on this topic do not give guidelines for test model design. It is established that testing...master thesis 2024
- document
-
Holten, Lucas (author)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...master thesis 2023
- document
-
Miranda Challapa, Victor Hugo (author)Tailings dam failures are one of the most destructive phenomena in terms of the number of victims and the environmental impact generated. Over the years, different causes have been identified, with flow liquefaction being a prominent factor to consider when assessing the stability of tailings deposits. Due to the complex nature of these events,...master thesis 2023
- document
-
Bezsilla, Janos (author)Nowadays, many space missions require highly accurate pointing for Earth observation or cosmic vision purposes. However, the vibration environment from a spacecraft's structure and reaction wheels can cause disturbances in its line-of-sight stability and severely impact image quality. Additionally, these effects are not known precisely due to...master thesis 2023
- document
-
Jóźwik, Michał (author)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...bachelor thesis 2023
- document
-
Padilla Cancio, José (author)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...bachelor thesis 2023
- document
-
Juhošová, Sára (author)Formal verification is a powerful tool for ensuring program correctness but is often hard to learn to use and has not yet spread into the commercial world. This thesis focuses on finding an easy-to-use solution to make formal verification available in popular programming language ecosystems. We propose a solution where users can write code in an...master thesis 2023
- document
-
Frijns, Jesper (author)Laser satellite communications for ground-to-ground and ground-to space links is influenced by atmospheric turbulence. Typically, theoretical models are used to predict link performance and the influence of the atmosphere on variables such as beam wander, spot size and scintillation at the receiver. These variables are used as input for system...master thesis 2023
- document
-
Stavridou, EVDOKIA (author)Although relevant information regarding the curtain walls structural damage state is available, hardly any data referring to the seismic loading effect on the overall façade performance is found in the literature. The present research attempts to assess the unitised curtain walls seismic performance by identifying the occurring damage mechanisms...master thesis 2023
- document
-
de Haas, Olav (author)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...master thesis 2022
- document
-
Reukers, Matthijs (author)Tydi is an open specification for streaming dataflow designs in digital circuits, allowing designers to express how composite and variable-length data structures are transferred over streams using clear, data-centric types. This provides a higher-level method for defining interfaces between components as opposed to existing bit- and byte-based...master thesis 2022
- document
-
Massar, Marnix (author)agda2hs is a tool which translates a subset of Agda to readable Haskell. Using agda2hs, programmers can implement libraries in this subset of Agda, formally verify them, and then convert them to Haskell. In this paper we present a new, verified implementation of the lens data type, which is used to access data structures in a readable yet...bachelor thesis 2022
- document
-
Schifferstein, Michelle (author)The formal verification of concurrent programs is of particular importance, because concurrent programs are notoriously difficult to test. Because Haskell is a purely functional language, it is relatively easy to reason about the correctness of such programs and write down manual proofs. However, since these methods are still prone to error,...bachelor thesis 2022
- document
-
Bărbunţoiu, Teodora (author)Deployment of renewable energy is essential to reach a carbon neutral economy. Offshore wind farms have caught the interest of many developed countries since they are an essential source of green energy. The interest of this thesis lays in the design of the foundation used for offshore wind farms, in particular the interaction between the...master thesis 2021
- document
-
Pejić, Saša Pejić (author)In recent years the AEC industry has started implementing more new technologies. Still, the adoption process is slow. One of the crucial steps during the building designing is a justification of design according to previously defined requirements. That process is still manual to a large extent, therefore unnecessarily time-consuming and prone to...master thesis 2021
- document
-
Belloli, Davide (author)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...master thesis 2021
- document
-
Raghavendra Rao, Shreenidhi (author)Success of the project depends on compliance to requirements amongst other things (Wheeler, 2003). This forms Requirements Management process an important step in the Systems Engineering life cycle. However, poor definition of requirements is an obstacle in automating the verification process. The existing solutions based on various approaches...master thesis 2021
- document
-
Koetsier, Mathieu (author)The increase in road traffic intensity and loading capacity of a truck over the last decades causes fatigue problems in existing bridges built in the 1960s and 1970s. For steel bridges, this means that the deck structure does not meet the current demands. A solution would be to replace these existing deck structures with Glas Fibre-Reinforced...master thesis 2021
- document
-
Huygen, Wouter (author)Automatic Dependent Surveillance – Broadcast (ADS-B) is an operational enhancement as part of next-generation air transportation systems in Air Traffic Control. It enables aircraft and airport vehicles to periodically broadcast the information from their on-board equipment, like their identification, GPS location, velocity, and intent. Compared...master thesis 2021