Verification of floating point programs

In this thesis we present an approach to automated verification of floating point programs. Existing techniques for automated generation of correctness theorems are extended to produce proof obligations for accuracy guarantees and absence of floating point exceptions. A prototype automated real number theorem prover is presented, demonstrating a novel application of function interval arithmetic in the context of subdivision-based numerical theorem proving. The prototype is tested on correctness theorems for two simple yet nontrivial programs, proving exception freedom and tight accuracy guarantees automatically. The prover demonstrates a novel application of function interval arithmetic in the context of subdivision-based numerical theorem proving. The experiments show how function intervals can be used to combat the information loss problems that limit the applicability of traditional interval arithmetic in the context of hard real number theorem proving.

On bandwidth request mechanism with piggyback in fixed IEEE 802.16 networks

This paper investigates the random channel access mechanism specified in the IEEE 802.16 standard for the uplink traffic in a Point-to-MultiPoint (PMP) network architecture. An analytical model is proposed to study the impacts of the channel access parameters, bandwidth configuration and piggyback policy on the performance. The impacts of physical burst profile and non-saturated network traffic are also taken into account in the model. Simulations validate the proposed analytical model. It is observed that the bandwidth utilization can be improved if the bandwidth for random channel access can be properly configured according to the channel access parameters, piggyback policy and network traffic.

Performance comparison of OFDM bandwidth request schemes in fixed IEEE 802.16 networks

IEEE 802.16 standard specifies two contention based bandwidth request schemes working with OFDM physical layer specification in point-to-multipoint (PMP) architecture, the mandatory one used in region-full and the optional one used in region-focused. This letter presents a unified analytical model to study the bandwidth efficiency and channel access delay performance of the two schemes. The impacts of access parameters, available bandwidth and subchannelization have been taken into account. The model is validated by simulations. The mandatory scheme is observed to perform closely to the optional one when subchannelization is active for both schemes.

Polynomial function intervals for floating-point software verification

The focus of our work is the verification of tight functional properties of numerical programs, such as showing that a floating-point implementation of Riemann integration computes a close approximation of the exact integral. Programmers and engineers writing such programs will benefit from verification tools that support an expressive specification language and that are highly automated. Our work provides a new method for verification of numerical software, supporting a substantially more expressive language for specifications than other publicly available automated tools. The additional expressivity in the specification language is provided by two constructs. First, the specification can feature inclusions between interval arithmetic expressions. Second, the integral operator from classical analysis can be used in the specifications, where the integration bounds can be arbitrary expressions over real variables. To support our claim of expressivity, we outline the verification of four example programs, including the integration example mentioned earlier. A key component of our method is an algorithm for proving numerical theorems. This algorithm is based on automatic polynomial approximation of non-linear real and real-interval functions defined by expressions. The PolyPaver tool is our implementation of the algorithm and its source code is publicly available. In this paper we report on experiments using PolyPaver that indicate that the additional expressivity does not come at a performance cost when comparing with other publicly available state-of-the-art provers. We also include a scalability study that explores the limits of PolyPaver in proving tight functional specifications of progressively larger randomly generated programs. © 2014 Springer International Publishing Switzerland.

Survivorship and Clinical Outcome of the Minimally Invasive Uniglide Medial Fixed Bearing, All-polyethylene Tibia, Unicompartmental Knee Arthroplasty at a Mean Follow-up of 7.3 Years

Background: Medial UKA performed in England and Wales represents 7 to 11% of all knee arthroplasty procedures, and is most commonly performed using mobile-bearing designs. Fixed bearing eliminates the risk of bearing dislocation, however some studies have shown higher revision rates for all-polyethylene tibial components compared to those that utilize metal-backed implants. The aim of the study is to analyse survivorship and maximum 8-year clinical outcome of medial fixed bearing, Uniglide unicompartmental knee arthroplasty performed using an all-polyethylene tibial component with a minimal invasive approach. Methods: Between 2002 and 2009, 270 medial fixed UKAs were performed in our unit. Patients were reviewed pre-operatively, 5 and 8 years post-operatively. Clinical and radiographic reviews were carried out. Patients’ outcome scores (Oxford, WOMAC and American Knee Score) were documented in our database and analysed. Results: Survival and clinical outcome data of 236 knees with a mean 7.3 years follow-up are reported. Every patient with less than 4.93 years follow-up underwent a revision. The patients’ average age at the time of surgery was 69.5 years. The American Knee Society Pain and Function scores, the Oxford Knee Score and the WOMAC score all improved significantly. The 5 years survival rate was 94.1% with implant revision surgery as an end point. The estimated 10 years survival rate is 91.3%. 14 patients were revised before the 5 year follow-up. Conclusion: Fixed bearing Uniglide UKA with an all-polyethylene tibial component is a valuable tool in the management of a medial compartment osteoarthritis, affording good short term survivorship.

Asymptotic Change-Point Analysis of the Dependencies in Time Series

In recent papers, Wied and his coauthors have introduced change-point procedures to detect and estimate structural breaks in the correlation between time series. To prove the asymptotic distribution of the test statistic and stopping time as well as the change-point estimation rate, they use an extended functional Delta method and assume nearly constant expectations and variances of the time series. In this thesis, we allow asymptotically infinitely many structural breaks in the means and variances of the time series. For this setting, we present test statistics and stopping times which are used to determine whether or not the correlation between two time series is and stays constant, respectively. Additionally, we consider estimates for change-points in the correlations. The employed nonparametric statistics depend on the means and variances. These (nuisance) parameters are replaced by estimates in the course of this thesis. We avoid assuming a fixed form of these estimates but rather we use "blackbox" estimates, i.e. we derive results under assumptions that these estimates fulfill. These results are supplement with examples. This thesis is organized in seven sections. In Section 1, we motivate the issue and present the mathematical model. In Section 2, we consider a posteriori and sequential testing procedures, and investigate convergence rates for change-point estimation, always assuming that the means and the variances of the time series are known. In the following sections, the assumptions of known means and variances are relaxed. In Section 3, we present the assumptions for the mean and variance estimates that we will use for the mean in Section 4, for the variance in Section 5, and for both parameters in Section 6. Finally, in Section 7, a simulation study illustrates the finite sample behaviors of some testing procedures and estimates.

Locating the maximum power point for thermoelectric generators for constant heat operation

Thermoelectric generators (TEGs) are solid-state devices that can be used for the direct conversion between heat and electricity. These devices are an attractive option for generating clean energy from heat. There are two modes of operation for TEGs; constant heat and constant temperature. It is a well-known fact that for constant temperature operation, TEGs have a maximum power point lying at half the open circuit voltage of the TEG, for a particular temperature. This work aimed to investigate the position of the maximum power point for Bismuth Telluride TEGs working under constant heat conditions i.e. the heat supply to the TEG is fixed however the temperature across the TEG can vary depending upon its operating conditions. It was found that for constant heat operation, the maximum power point for a TEG is greater than half the open circuit voltage of the TEG.