Interactive theorem proving provides a general approach to modeling and verification of both finite-state and infinite-state systems but requires significant human efforts to deal with many tedious proofs. On the other hand, model-checking is limited to some application domain with small finite-state space. A natural thought for this problem is to integrate these two approaches. To keep the consistency of the integration and ensure the correctness of verification, we suggest to use type theory based theorem provers (e.g. Lego) as the platform for the integration and build a model-checker to do parts of the verification automatically. We formalise a verification system of both CCS and an imperative language in the proof development system Lego which can be used to verify both finite-state and infinite-state problems. Then a model-checker, LegoMC, is implemented to generate Lego proof terras for finite-state problems automatically. Therefore people can use Lego to verify a general problem with some of its finite sub-problems verified by LegoMC. On the other hand, this integration extends the power of model-checking to verify more complicated and infinite-state models as well. The development of automatic techniques and the integration of different reasoning methods would directly benefit the verification community. It is expected that further extension and development of this verification environment would be able to handle real life systems. On the other hand, the research gives us some experiences about how to automate proofs in interactive theorem provers and therefore will improve the usability and applicability of the theorem proving technology.

Modern computer systems are advancing from multi-core to many-core designs and System-on-chips (SoC) are becoming increasingly complex while integrating a great variety of components, thus constituting complex distributed systems. Such architectures rely on extremely complex communication protocols to exchange data with required performance. Arguing formally about the correctness of communication is an acknowledged verification challenge. This thesis presents a generic framework that formalises the idea of incremental modelling and step-wise verification to tackle this challenge: to control the overall complexity, features are added incrementally to a simple initial model and the complexity of each feature is encapsulated into an independent modelling step. Two main strategies reduce the verification effort. First, models are constructed with verification support in mind and the verification process is spread over the modelling process. Second, generic correctness results for framework components allow the verification to be reduced to discharging local assumptions when a component is instantiated. Models in the framework are based on abstract state machines formalised in higher order logic using the Isabelle theorem prover. Two case studies show the utility and breadth of the approach: the ARM AMBA Advanced High-performance Bus protocol, an arbiter-based master-slave bus protocol, represents the family of SoC protocols; the PCI Express protocol, an off-chip point-to-point protocol, illustrates the application of the framework to sophisticated, performance-related features of current and future on-chip protocols. The presented methodology provides an alternative to the traditional monolithic and post-hoc verification approach.

As verification efforts using interactive theorem proving grow, we are in need of certified algorithms in computer algebra to tackle problems over the real numbers. This is important because uncertified procedures can drastically increase the size of the trust base and under- mine the overall confidence established by interactive theorem provers, which usually rely on a small kernel to ensure the soundness of derived results. This thesis describes an ongoing effort using the Isabelle theorem prover to certify the cylindrical algebraic decomposition (CAD) algorithm, which has been widely implemented to solve non-linear problems in various engineering and mathematical fields. Because of the sophistication of this algorithm, people are in doubt of the correctness of its implementation when deploying it to safety-critical verification projects, and such doubts motivate this thesis. In particular, this thesis proposes a library of real algebraic numbers, whose distinguishing features include a modular architecture and a sign determination algorithm requiring only rational arithmetic. With this library, an Isabelle tactic based on univariate CAD has been built in a certificate-based way: external, untrusted code delivers solutions in the form of certificates that are checked within Isabelle. To lay the foundation for the multivariate case, I have formalised various analytical results including Cauchy's residue theorem and the bivariate case of the projection theorem of CAD. During this process, I have also built a tactic to evaluate winding numbers through Cauchy indices and verified procedures to count complex roots in some domains. The formalisation effort in this thesis can be considered as the first step towards a certified computer algebra system inside a theorem prover, so that various engineering projections and mathematical calculations can be carried out in a high-confidence framework.

This dissertation is dedicated to study the modeling of drift control in foreign exchange reserves management and design the fast algorithm of statistical inference with its application in high dimensional data analysis. The thesis has two parts. The first topic involves the modeling of foreign exchange reserve management as an drift control problem. We show that, under certain conditions, the control band policies are optimal for the discounted cost drift control problem and develop an algorithm to calculate the optimal thresholds of the optimal control band policy. The second topic involves the fast computing algorithm of partial distance covariance statistics with its application in feature screening in high dimensional data. We show that an O(n log n) algorithm for a version of the partial distance covariance exists, compared with the O(n^2) algorithm implemented directly accordingly to its definition. We further propose an iterative feature screening procedure in high dimensional data based on the partial distance covariance. This procedure enjoys two advantages over the correlation learning. First, an important predictor that is marginally uncorrelated but jointly correlated with the response can be picked by our procedure and thus entering the estimation model. Second, our procedure is robust to model mis- specification.

Two optimisation problems were considered, in which market exposure is indirectly controlled. The first one models the capital of a company and an independent portfolio of new businesses, each one represented by a Cram\'r-Lundberg process. The company can choose the proportion of new business it wants to take on and can alter this proportion over time. Here the objective is to find a strategy that maximises the survival probability. We use a point processes framework to deal with the impact of an adapted strategy in the intensity of the new business. We prove that when Cram\'{e}r-Lundberg processes with exponentially distributed claims, it is optimal to choose a threshold type strategy, where the company switches between owning all new businesses or none depending on the capital level. For this type of processes that change both drift and jump measure when crossing the constant threshold, we solve the one and two-sided exit problems. This optimisation problem is also solved when the capital of the company and the new business are modelled by spectrally positive L\'vy processes of bounded variation. Here the one-sided exit problem is solved and we prove optimality of the same type of threshold strategy for any jump distribution. The second problem is a stochastic variation of the work done by Taylor about underwriting in a competitive market. Taylor maximised discounted future cash flows over a finite time horizon in a discrete time setting when the change of exposure from one period to the next has a multiplicative form involving the company's premium and the market average premium. The control is the company's premium strategy over a the mentioned finite time horizon. Taylor's work opened a rich line of research, and we discuss some of it. In contrast with Taylor's model, we consider the market average premium to be a Markov chain instead of a deterministic vector. This allows to model uncertainty in future conditions of the market. We also consider an infinite time horizon instead of finite. This solves the time dependency in Taylor's optimal strategies that were giving unrealistic results. Our main result is a formula to calculate explicitly the value function of a specific class of pricing strategies. Further we explore concrete examples numerically. We find a mix of optimal strategies where in some examples the company should follow the market while in other cases should go against it.