- document
-
Antonopoulos, Tasos (author)Navi Mumbai is a city designed to diffuse the overpopulation problem of Mumbai. However, there were villages in the area that developed informally alongside the formal city. These villages present several problems such as inadequate housing, identity loss, lack of infrastructure, lack of public space, overcrowding and crammed streets. There are...master thesis 2023
- document
-
Miaskiwskyi, L.T. (author)The subject of this thesis is twofold: The first part is the study of local-to-global principles for the continuous Lie algebra (co-)homology of certain infinite-dimensional Lie algebras of geometric origin, specifically, Gelfand-Fuks cohomology and continuous cohomology of gauge algebras. It includes both an exposition to classical results of...doctoral thesis 2022
- document
-
Gracia Merino, Ibón (author)There is growing interest to control cyber-physical systems under complex specifications while retaining formal performance guarantees. In this thesis we present a framework for formal control of uncertain systems under complex specifications. We consider dynamical systems with random disturbances, whose probability distribution is unknown. When...master thesis 2022
- document
-
Augusto da Silva, F. (author)In recent years, advances in technology have enabled the employment of automated systems to control driving tasks. The idea of electronic devices having complete control over a vehicle promises to change the concept of mobility soon. However, allowing computers to control all the tasks in a vehicle demands sophisticated systems and significant...doctoral thesis 2022
- 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
-
de Albuquerque Gleizer, G. (author)Event-triggered control (ETC) and self-triggered control (STC) are sample-and-hold control paradigms in which sensor data is only updated to the controller when necessary, often aperiodically, in contrast to the well-established periodic sampling paradigm. In ETC, a state-dependent event triggers a transmission, while in STC the controller...doctoral 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
-
NAMWANJE, PRISCILLA (author)Uganda’s capital Kampala, is grappling with the effects of rapid urbanisation fueled by the population explosion that has transpired over the recent years. Due to the continued futility of urban planning efforts, the city’s growth has proceeded with minimal planning intervention, resulting in multiple urban development challenges.<br/>Kampala’s...master thesis 2022
- document
-
Bagbaba, Ahmet Cagri (author), Augusto da Silva, F. (author), Sonza Reorda, Matteo (author), Hamdioui, S. (author), Jenihhin, Maksim (author), Sauer, Christian (author)ISO 26262 requires classifying random hardware faults based on their effects (safe, detected, or undetected) within integrated circuits used in automobiles. In general, this classification is addressed using expert judgment and a combination of tools. However, the growth of integrated circuit complexity creates a huge fault space; hence, this...journal article 2022
- document
-
Ocadiz flores, J.A. (author), Konings, R. (author), Smith, A.L. (author)CALPHAD models to compute the density and viscosity of four keystone systems related to Molten Salt Reactor (MSR) technology have been optimized: NaCl-UCl<sub>3</sub>, LiF-ThF<sub>4</sub>, LiF-UF<sub>4</sub>, and LiF-ThF<sub>4</sub>-UF<sub>4</sub>. Revised thermodynamic assessments of all four systems, using the modified quasichemical...journal article 2022
- document
-
Verdier, C.F. (author), Kochdumper, Niklas (author), Althoff, Matthias (author), Mazo, M. (author)We propose a counterexample-guided inductive synthesis framework for the formal synthesis of closed-form sampled-data controllers for nonlinear systems to meet STL specifications over finite-time trajectories. Rather than stating the STL specification for a single initial condition, we consider an (infinite and bounded) set of initial...journal article 2022
- 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
-
Nikulina, Anna (author), Volker, Leentje (author), Bosch-Rekveldt, M.G.C. (author)Collaboration can bring multiple benefits to projects. Real collaboration appears, however, complex to implement. So far, there is no scientific agreement on the importance of the formal and relational (behavioural) sides of project collaboration. Through a qualitative study of two collaborating teams in large engineering and construction...journal article 2022
- document
-
Fuchs, P.S. (author), Remis, R.F. (author)In this article, we present full-wave signal models for magnetic and electric field measurements in magnetic resonance imaging (MRI). Our analysis is based on a scattering formalism in which the presence of an object or body is taken into account via an electric scattering source. We show that these signal models can be evaluated, provided...journal article 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
- document
-
Adams, S.J.L. (author), Lahijanian, Morteza (author), Laurenti, L. (author)Neural networks (NNs) are emerging as powerful tools to represent the dynamics of control systems with complicated physics or black-box components. Due to complexity of NNs, however, existing methods are unable to synthesize complex behaviors with guarantees for NN dynamic models (NNDMs). This letter introduces a control synthesis framework for...journal article 2022
- 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
-
van der Zijden, Tycho van der Zijden (author)In networked control systems (NCS), the components of the control system communicate over a network, which poses challenges to the control synthesis procedure. Signal sampling is one of those challenges. A typical approach is to sample the signal periodically, but this can be inefficient. Event-triggered control (ETC) is a more efficient way to...student report 2021
- 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
-
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