Colorectal cancer (CRC) is among the most frequent cancer entities worldwide. Multiple factors are causally associated with CRC development, such as genetic and epigenetic alterations, inflammatory bowel disease, lifestyle and dietary factors. During malignant transformation,the cellular energy metabolism is reprogrammed in order to promote cancer cell growth and proliferation. In this review, we first describe the main alterations of the energy metabolism found in CRC, revealing the critical impact of oncogenic signaling and driver mutations in key metabolic enzymes. Then, the central role of mitochondria and the tricarboxylic acid (TCA) cycle in this process is highlighted, also considering the metabolic crosstalk between tumor and stromal cells in the tumor microenvironment. The identified cancer-specific metabolic transformations provided new therapeutic targets for the development of small molecule inhibitors. Promising agents are in clinical trials and are directed against enzymes of the TCA cycle, including isocitrate dehydrogenase, pyruvate dehydrogenase kinase, pyruvate dehydrogenase complex (PDC) and α-ketoglutarate dehydrogenase (KGDH). Finally, we focus on the α-lipoic acid derivative CPI-613, an inhibitor of both PDC and KGDH, and delineate its anti-tumor effects for targeted therapy.

The consumption of red meat is probably carcinogenic to humans and is associated with an increased risk to develop colorectal cancer (CRC). Red meat contains high amounts of heme iron, which is thought to play a causal role in tumor formation. In this study, we investigated the genotoxic and cytotoxic effects of heme iron (i.e., hemin) versus inorganic iron in human colonic epithelial cells (HCEC), human CRC cell lines and murine intestinal organoids. Hemin catalyzed the formation of reactive oxygen species (ROS) and induced oxidative DNA damage as well as DNA strand breaks in both HCEC and CRC cells. In contrast, inorganic iron hardly affected ROS levels and only slightly increased DNA damage. Hemin, but not inorganic iron, caused cell death and reduced cell viability. This occurred preferentially in non-malignant HCEC, which was corroborated in intestinal organoids. Both hemin and inorganic iron were taken up into HCEC and CRC cells, however with differential kinetics and efficiency. Hemin caused stabilization and nuclear translocation of Nrf2, which induced heme oxygenase-1 (HO-1) and ferritin heavy chain (FtH). This was not observed after inorganic iron treatment. Chemical inhibition or genetic knockdown of HO-1 potentiated hemin-triggered ROS generation and oxidative DNA damage preferentially in HCEC. Furthermore, HO-1 abrogation strongly augmented the cytotoxic effects of hemin in HCEC, revealing its pivotal function in colonocytes and highlighting the toxicity of free intracellular heme iron. Taken together, this study demonstrated that hemin, but not inorganic iron, induces ROS and DNA damage, resulting in a preferential cytotoxicity in non-malignant intestinal epithelial cells. Importantly, HO-1 conferred protection against the detrimental effects of hemin.

Today, information systems are often distributed to achieve high availability and low latency. These systems can be realized by building on a highly available database to manage the distribution of data. However, it is well known that high availability and low latency are not compatible with strong consistency guarantees. For application developers, the lack of strong consistency on the database layer can make it difficult to reason about their programs and ensure that applications work as intended. We address this problem from the perspective of formal verification. We present a specification technique, which allows specifying functional properties of the application. In addition to data invariants, we support history properties. These let us express relations between events, including invocations of the application API and operations on the database. To address the verification problem, we have developed a proof technique that handles concurrency using invariants and thereby reduces the problem to sequential verification. The underlying system semantics, technique and its soundness proof are all formalized in the interactive theorem prover Isabelle/HOL. Additionally, we have developed a tool named Repliss which uses the proof technique to enable partially automated verification and testing of applications. For verification, Repliss generates verification conditions via symbolic execution and then uses an SMT solver to discharge them.

Life insurance companies are asked by the Solvency II regime to retain capital requirements against economically adverse developments. This ensures that they are continuously able to meet their payment obligations towards the policyholders. When relying on an internal model approach, an insurer's solvency capital requirement is defined as the 99.5% value-at-risk of its full loss probability distribution over the coming year. In the introductory part of this thesis, we provide the actuarial modeling tools and risk aggregation methods by which the companies can accomplish the derivations of these forecasts. Since the industry still lacks the computational capacities to fully simulate these distributions, the insurers have to refer to suitable approximation techniques such as the least-squares Monte Carlo (LSMC) method. The key idea of LSMC is to run only a few wisely selected simulations and to process their output further to obtain a risk-dependent proxy function of the loss. We dedicate the first part of this thesis to establishing a theoretical framework of the LSMC method. We start with how LSMC for calculating capital requirements is related to its original use in American option pricing. Then we decompose LSMC into four steps. In the first one, the Monte Carlo simulation setting is defined. The second and third steps serve the calibration and validation of the proxy function, and the fourth step yields the loss distribution forecast by evaluating the proxy model. When guiding through the steps, we address practical challenges and propose an adaptive calibration algorithm. We complete with a slightly disguised real-world application. The second part builds upon the first one by taking up the LSMC framework and diving deeper into its calibration step. After a literature review and a basic recapitulation, various adaptive machine learning approaches relying on least-squares regression and model selection criteria are presented as solutions to the proxy modeling task. The studied approaches range from ordinary and generalized least-squares regression variants over GLM and GAM methods to MARS and kernel regression routines. We justify the combinability of the regression ingredients mathematically and compare their approximation quality in slightly altered real-world experiments. Thereby, we perform sensitivity analyses, discuss numerical stability and run comprehensive out-of-sample tests. The scope of the analyzed regression variants extends to other high-dimensional variable selection applications. Life insurance contracts with early exercise features can be priced by LSMC as well due to their analogies to American options. In the third part of this thesis, equity-linked contracts with American-style surrender options and minimum interest rate guarantees payable upon contract termination are valued. We allow randomness and jumps in the movements of the interest rate, stochastic volatility, stock market and mortality. For the simultaneous valuation of numerous insurance contracts, a hybrid probability measure and an additional regression function are introduced. Furthermore, an efficient seed-related simulation procedure accounting for the forward discretization bias and a validation concept are proposed. An extensive numerical example rounds off the last part.

Small embedded devices are highly specialized platforms that integrate several pe- ripherals alongside the CPU core. Embedded devices extensively rely on Firmware (FW) to control and access the peripherals as well as other important functionality. Customizing embedded computing platforms to specific application domains often necessitates optimizing the firmware and/or the HW/SW interface under tight re- source constraints. Such optimizations frequently alter the communication between the firmware and the peripheral devices, possibly compromising functional correct- ness of the input/output behavior of the embedded system. This poses challenges to the development and verification of such systems. The system must be adapted and verified to each specific device configuration. This thesis presents a formal approach to formulate these verification tasks at several levels of abstraction, along with corresponding HW/SW co-equivalence checking techniques for verifying correct I/O behavior of peripherals under a modified firmware. The feasibility of the approach is shown on several case studies, including industrial driver software as well as open-source peripherals. In addition, a subtle bug in one of the peripherals and several undocumented preconditions for correct device behavior were detected by the verification method.