Thèses (M.Sc.)--Université de Sherbrooke (Canada), 2001. / Titre de l'écran-titre (visionné le 20 juin 2006). Publié aussi en version papier.

Thesis (Ph. D.)--University of Texas at Austin, 2002. / Vita. Includes bibliographical references. Available also from UMI Company.

Thesis (Ph. D.)--Hong Kong University of Science and Technology, 2004. / Includes bibliographical references (leaves 49-50). Also available in electronic version. Access restricted to campus users.

Thesis (Ph. D.)--University of Texas at Austin, 1998. / Vita. Includes bibliographical references (leaves 77-80). Available also in a digital version from Dissertation Abstracts.

Thesis (Ph. D.)--University of Washington, 1999. / Vita. Includes bibliographical references (p. 83-84).

Thesis (Ph. D.)--University of Wisconsin, 1967. / Typescript. Vita. eContent provider-neutral record in process. Description based on print version record. Includes bibliography.

No description available.

Due to the increasing complexity of today\'s cyber-physical systems, defects become inevitable and harder to detect. The complexity of such software is generally huge, with millions of lines of code. The impact of failure of such systems could be hazardous. The reliability of the system depends on the effectiveness and rigor of the testing procedures. Verification of the software behind such cyber-physical systems is required to ensure stability and reliability before the systems are deployed in field. We have investigated the verification of the software for Autonomous Underwater Vehicles (AUVs) to ensure safety of the system at any given time in the field. To accomplish this, we identified useful invariants that would aid as monitors in detecting abnormal behavior of the software. Potential invariants were extracted which had to be validated. The investigation attempts to uncover the possibility of performing this method on existing Software verification platforms. This was accomplished on Cloud9, which is built on KLEE and using the Microsoft\'s VCC tool. Experimental results show that this method of extracting invariants can help in identifying new invariants using these two tools and the invariants identified can be used to monitor the behavior of the autonomous vehicles to detect abnormality and failures in the system much earlier thereby improving the reliability of the system. Recommendations for improving software quality were provided. The work also explored safety measures and standards on software for safety critical systems and Autonomous vehicles. Metrics for measuring software complexity and quality along with the requirements to certify AUV software were also presented. The study helps in understanding verification issues, guidelines and certification requirements. / Master of Science

In this thesis, we report on two projects applying representation theoretic techniques to solve enumerative and geometric problems, which were carried out by the author during his pursuit of Ph.D. at Columbia. We first study the relative Gromov-Witten theory on T*P¹ x P¹ and show that certain equivariant limits give relative invariants on P¹ x P¹. By formulating the quantum multiplications on Hilb(T*P¹) computed by Davesh Maulik and Alexei Oblomkov as vertex operators and computing the product expansion, we demonstrate how to get the insertion operator computed by Yaim Cooper and Rahul Pandharipande in the equivariant limits. Brenti proves a non-recursive formula for the Kazhdan-Lusztig polynomials of Coxeter groups by combinatorial methods. In the case of the Weyl group of a split group over a finite field, a geometric interpretation is given by Sophie Morel via weight truncation of perverse sheaves. With suitable modifications of Morel's proof, we generalize the geometric interpretation to the case of finite and affine partial flag varieties. We demonstrate the result with essentially new examples using sl₃ and sl₄..

Post-Silicon validation is playing an increasingly important role as more chips are failing in the functional mode due to either manufacturing defects escaped during scan-based tests or design bugs missed during pre-silicon validation. Critical to the diagnosis engineer is the ability to observe as many relevant internal signal values as possible during debug. To do so, trace buffers have been proposed for enhancing the observability of internal signals during post-silicon debug. Trace Buffers are used to trace (record the values of) the internal signals in real-time when chip is in its normal operation. However, existing trace buffer architectures trace very few signals for a large number of cycles. Thus, even with a good subset of signals traced, one often still cannot restore all the relevant values in the circuit. In this work, we propose two different flexible trace buffer architectures that can restore the values for all signals by making the trace signals configurable. In addition, the buffer space can also be shared among different traced signals which makes the architectures highly flexible. As compared to conventional trace buffer architectures, the new architectures have comparable area overhead but offer the ability to restore all signals in the circuit. For cases of less than 100% restoration, the ability of circuit invariants to improve the signal restoration is explored. A promising direction for the future work is provided where targeted invariants may lead to better restoration scenario during post-silicon validation. / Master of Science