Foundations for reasoning about holistic specifications
AuthorNguyen, Duc Than
AffiliationComputing and Information Systems
Document TypeMasters Research thesis
Access StatusOpen Access
© 2020 Duc Than Nguyen
Specifications of sufficient conditions may be enough for reasoning about complete and unchanging programs of a closed system. Nevertheless, there is no luxury of trusting external components of probably unknown provenance in an open world that may be buggy or potentially malicious. It is critical to ensure that our components are robust when cooperating with a wide variety of external components. Holistic specifications, which are concerned with sufficient and necessary conditions, could make programs more robust in an open-world setting. In this thesis, we lay the foundations for reasoning about holistic specifications. We give an Isabelle/HOL mechanization of holistic specifications focusing on object-based programs. We also pave a way to reason about holistic specifications via proving some key lemmas that we hope will be useful in the future to establish a general logic for holistic specifications.
KeywordsComputer System Security; Computational Logic and Formal Languages; Formal Specification and Verification
- Click on "Export Reference in RIS Format" and choose "open with... Endnote".
- Click on "Export Reference in RIS Format". Login to Refworks, go to References => Import References