- document
-
Sabharwal, Dixit (author)Equational reasoning based verification address some of the limitations of classical testing. The Curry-Howard correspondence shows a direct link between type systems and mathematical logic based proofs. Agda is a language with totality and dependent types which makes use of the CH isomorphism to support equational reasoning in its programs. ...bachelor thesis 2021
- 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
-
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
-
van Buren, Rico (author)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...bachelor thesis 2021
- document
-
Gouicem, Redha (author), Sprokholt, D.G. (author), Ruehl, Jasper (author), Rocha, Rodrigo C.O. (author), Spink, Tom (author), Chakraborty, S.S. (author), Bhatotia, Pramod (author)Dynamic Binary Translation (DBT) is a powerful approach to support cross-architecture emulation of unmodified binaries. However, DBT systems face correctness and performance challenges, when emulating concurrent binaries from strong to weak memory consistency architectures. As a matter of fact, we report several translation errors in QEMU,...conference paper 2022
- document
-
Esmaeil Zadeh Soudjani, S. (author), Abate, A. (author)This work is concerned with the generation of finite abstractions of general state-space processes to be employed in the formal verification of probabilistic properties by means of automatic techniques such as probabilistic model checkers. The work employs an abstraction procedure based on the partitioning of the state-space, which generates a...journal article 2013
- document
-
Coppola, Mario (author), Guo, J. (author), Gill, E.K.A. (author), de Croon, G.C.H.E. (author)In this paper we present a procedure to automatically design and verify the local behavior of robots with highly limited cognition. All robots are: anonymous, homogeneous, non-communicating, memoryless, reactive, do not know their global position, do not have global state information, and operate by a local clock. They only know: (1) the...journal article 2019
- document
-
Sharifi Kolarijani, A. (author)In networked systems, particularly over wireless or shared channels, the scarcity of communication resources makes the application of traditional control strategies with periodic sampling problematic. Alternative approaches with aperiodic sampling, such as: event triggered control and self triggered control, have been recently proposed to reduce...master thesis 2014
- document
-
Jongmans, S.S.T.Q. (author)This thesis presents a novel approach to model checking of agent programs written in an agent programming language. The language we consider is GOAL. The novelty of the approach is that we implement model checking algorithms from scratch on top of the standard language interpreter. In contrast, in the literature on agent program verification,...master thesis 2010
- document
-
Rouwen, Floris (author)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...master thesis 2018
- 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
-
Gevaerts, C.J.P. (author)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...master thesis 2014
- 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
-
Mulder, Ike (author)Packing problems are concerned with filling the space with copies of a certain object, so that the least amount of space stays unoccupied. The famous Kepler conjecture asserts that the cannonball packing of spheres is the most efficient packing achievable, and was recently formally proven by Hales.<br/><br/>Dostert, Guzman, Oliveira Filho and...master thesis 2019
- document
-
Van Roekel, B.J.M. (author)Annually over 60.000 people die and another 3.7 million get injured in car accidents in the United States and Europe combined. Automation of vehicles can reduce the number of accidents by 90%. Therefore, it is of great interest in academia and industry. For the automated vehicles that are being presented in industry however, proofs of safe...master thesis 2015
- 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
-
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
-
Marijan, Dusica (author), Lal, C. (author)As blockchain technology is gaining popularity in industry and society, solutions for Verification and Validation (V&V) of blockchain-based software applications (BC-Apps) have started gaining equal attention. To ensure that BC-Apps are properly developed before deployment, it is paramount to apply systematic V&V to verify their...review 2022