Advanced search options

Advanced Search Options 🞨

Browse by author name (“Author name starts with…”).

Find ETDs with:

in
/  
in
/  
in
/  
in

Written in Published in Earliest date Latest date

Sorted by

Results per page:

You searched for id:"oai:tigerprints.clemson.edu:all_dissertations-3522". One record found.

Search Limiters

Last 2 Years | English Only

No search limiters apply to these results.

▼ Search Limiters


Clemson University

1. Welch, Daniel Thomas. Scaling Up Automated Verification: A Case Study and a Formalization IDE for Building High Integrity Software.

Degree: PhD, School of Computing, 2019, Clemson University

Component-based software verification is a difficult challenge because developers must specify components formally and annotate implementations with suitable assertions that are amenable to automation. This research investigates the intrinsic complexity in this challenge using a component-based case study. Simultaneously, this work also seeks to minimize the extrinsic complexities of this challenge through the development and usage of a formalization integrated development environment (F-IDE) built for specifying, developing, and using verified reusable software components. The first contribution is an F-IDE built to support formal specification and automated verification of object-based software for the integrated specification and programming language RESOLVE. The F-IDE is novel, as it integrates a verifying compiler with a user-friendly interface that provides a number of amenities including responsive editing for model-based mathematical contracts and code, assistance for design by contract, verification, responsive error handling, and generation of property-preserving Java code that can be run within the F-IDE. The second contribution is a case study built using the F-IDE that involves an interplay of multiple artifacts encompassing mathematical units, component interfaces, and realizations. The object-based interfaces involved are specified in terms of new mathematical models and non-trivial theories designed to encapsulate data structures and algorithms. The components are designed to be amenable to modular verification and analysis. Advisors/Committee Members: Murali Sitaraman, Wayne D Goddard, John D McGregor, Nigamanth Sridhar.

Subjects/Keywords: Component-based software; Formal methods; Integrated development environments; Verification

Record DetailsSimilar RecordsGoogle PlusoneFacebookTwitterCiteULikeMendeleyreddit

APA · Chicago · MLA · Vancouver · CSE | Export to Zotero / EndNote / Reference Manager

APA (6th Edition):

Welch, D. T. (2019). Scaling Up Automated Verification: A Case Study and a Formalization IDE for Building High Integrity Software. (Doctoral Dissertation). Clemson University. Retrieved from https://tigerprints.clemson.edu/all_dissertations/2517

Chicago Manual of Style (16th Edition):

Welch, Daniel Thomas. “Scaling Up Automated Verification: A Case Study and a Formalization IDE for Building High Integrity Software.” 2019. Doctoral Dissertation, Clemson University. Accessed January 25, 2020. https://tigerprints.clemson.edu/all_dissertations/2517.

MLA Handbook (7th Edition):

Welch, Daniel Thomas. “Scaling Up Automated Verification: A Case Study and a Formalization IDE for Building High Integrity Software.” 2019. Web. 25 Jan 2020.

Vancouver:

Welch DT. Scaling Up Automated Verification: A Case Study and a Formalization IDE for Building High Integrity Software. [Internet] [Doctoral dissertation]. Clemson University; 2019. [cited 2020 Jan 25]. Available from: https://tigerprints.clemson.edu/all_dissertations/2517.

Council of Science Editors:

Welch DT. Scaling Up Automated Verification: A Case Study and a Formalization IDE for Building High Integrity Software. [Doctoral Dissertation]. Clemson University; 2019. Available from: https://tigerprints.clemson.edu/all_dissertations/2517

.