A simple proof checker for real-time systems

This thesis presents a practical approach to verifying real-time properties of V L S I designs. A simple proof checker with built-in decision procedures for linear programming and predicate calculus offers a pragmatic approach to verifying real-time systems in return for a slight loss of formal r...

Full description

Bibliographic Details
Main Author: Leung, Catherine
Format: Others
Language:English
Published: 2009
Online Access:http://hdl.handle.net/2429/3826
id ndltd-UBC-oai-circle.library.ubc.ca-2429-3826
record_format oai_dc
spelling ndltd-UBC-oai-circle.library.ubc.ca-2429-38262018-01-05T17:31:39Z A simple proof checker for real-time systems Leung, Catherine This thesis presents a practical approach to verifying real-time properties of V L S I designs. A simple proof checker with built-in decision procedures for linear programming and predicate calculus offers a pragmatic approach to verifying real-time systems in return for a slight loss of formal rigor when compared with traditional theorem provers. In this approach, an abstract data type represents the hypotheses, claim, and pending proof obligations at each step. A complete proof is a program that generates a proof state with the derived claim and no pending obligations. The user provides replacements for obligations and relies on the proof checker to validate the soundness of each operation. This design decision distinguishes the proof checker from traditional theorem provers, and enhances the view of "proofs as programs". This approach makes proofs robust to incremental changes, and there are few "surprises" when applying rewrite rules or decision procedures to proof obligations. A hand-written proof constructed to verify the timing correctness of a high bandwidth communication protocol was verified using this checker. Science, Faculty of Computer Science, Department of Graduate 2009-01-21T19:37:27Z 2009-01-21T19:37:27Z 1995 1995-11 Text Thesis/Dissertation http://hdl.handle.net/2429/3826 eng For non-commercial purposes only, such as research, private study and education. Additional conditions apply, see Terms of Use https://open.library.ubc.ca/terms_of_use. 9136973 bytes application/pdf
collection NDLTD
language English
format Others
sources NDLTD
description This thesis presents a practical approach to verifying real-time properties of V L S I designs. A simple proof checker with built-in decision procedures for linear programming and predicate calculus offers a pragmatic approach to verifying real-time systems in return for a slight loss of formal rigor when compared with traditional theorem provers. In this approach, an abstract data type represents the hypotheses, claim, and pending proof obligations at each step. A complete proof is a program that generates a proof state with the derived claim and no pending obligations. The user provides replacements for obligations and relies on the proof checker to validate the soundness of each operation. This design decision distinguishes the proof checker from traditional theorem provers, and enhances the view of "proofs as programs". This approach makes proofs robust to incremental changes, and there are few "surprises" when applying rewrite rules or decision procedures to proof obligations. A hand-written proof constructed to verify the timing correctness of a high bandwidth communication protocol was verified using this checker. === Science, Faculty of === Computer Science, Department of === Graduate
author Leung, Catherine
spellingShingle Leung, Catherine
A simple proof checker for real-time systems
author_facet Leung, Catherine
author_sort Leung, Catherine
title A simple proof checker for real-time systems
title_short A simple proof checker for real-time systems
title_full A simple proof checker for real-time systems
title_fullStr A simple proof checker for real-time systems
title_full_unstemmed A simple proof checker for real-time systems
title_sort simple proof checker for real-time systems
publishDate 2009
url http://hdl.handle.net/2429/3826
work_keys_str_mv AT leungcatherine asimpleproofcheckerforrealtimesystems
AT leungcatherine simpleproofcheckerforrealtimesystems
_version_ 1718586608723165184