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:

Sorted by: relevance · author · university · dateNew search

You searched for subject:(Intermediate Verification Language). Showing records 1 – 3 of 3 total matches.

Search Limiters

Last 2 Years | English Only

No search limiters apply to these results.

▼ Search Limiters

1. Cheng, Zheng. Formal Verification of Relational Model Transformations using an Intermediate Verification Language.

Degree: 2016, RIAN

Model-driven engineering has been recognised as an effective way to manage the complexity of software development. Model transformation is widely acknowledged as one of its central ingredients. Among different paradigms of model transformations, we are specifically interested in relational model transformations. Proving the correctness of relational model transformations is our major concern. Typically “correctness” is specified by MTr developers using contracts. Contracts are the annotations on the MTr which express constraints under which the MTr are considered to be correct. Our main objective is to develop an approach to designing a deductive verifier in a modular and sound way for a given target relational model transformation language, which enables formal verification of the correctness of MTr. To this end, we have developed the VeriMTLr framework. Its role is to assist in designing verifiers that allow verification (via automatic theorem proving) of the correctness of relational model transformations. VeriMTLr draws on the Boogie intermediate verification language to systematically design modular and reusable verifiers for a target relational model transformation language. Our framework encapsulates an EMF metamodels library and an OCL library within Boogie. The result is reduced cost and time required for a verifier’s construction. Furthermore, VeriMTLr includes an ASM and EMFTVM bytecode library, enabling an automated translation validation approach to ensuring the soundness of the verification of the designed verifier. We demonstrate our VeriMTLr framework with the design of verifiers for the Atlas Transformation Language and the SimpleGT graph transformation language.

Subjects/Keywords: Formal Verification; Relational Model Transformations; Intermediate Verification Language

Record DetailsSimilar RecordsGoogle PlusoneFacebookTwitterCiteULikeMendeleyreddit

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

APA (6th Edition):

Cheng, Z. (2016). Formal Verification of Relational Model Transformations using an Intermediate Verification Language. (Thesis). RIAN. Retrieved from http://eprints.maynoothuniversity.ie/7089/

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

Chicago Manual of Style (16th Edition):

Cheng, Zheng. “Formal Verification of Relational Model Transformations using an Intermediate Verification Language.” 2016. Thesis, RIAN. Accessed February 26, 2021. http://eprints.maynoothuniversity.ie/7089/.

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

MLA Handbook (7th Edition):

Cheng, Zheng. “Formal Verification of Relational Model Transformations using an Intermediate Verification Language.” 2016. Web. 26 Feb 2021.

Vancouver:

Cheng Z. Formal Verification of Relational Model Transformations using an Intermediate Verification Language. [Internet] [Thesis]. RIAN; 2016. [cited 2021 Feb 26]. Available from: http://eprints.maynoothuniversity.ie/7089/.

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

Council of Science Editors:

Cheng Z. Formal Verification of Relational Model Transformations using an Intermediate Verification Language. [Thesis]. RIAN; 2016. Available from: http://eprints.maynoothuniversity.ie/7089/

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

2. Cheng, Zheng. Formal Verification of Relational Model Transformations using an Intermediate Verification Language.

Degree: 2016, RIAN

Model-driven engineering has been recognised as an effective way to manage the complexity of software development. Model transformation is widely acknowledged as one of its central ingredients. Among different paradigms of model transformations, we are specifically interested in relational model transformations. Proving the correctness of relational model transformations is our major concern. Typically “correctness” is specified by MTr developers using contracts. Contracts are the annotations on the MTr which express constraints under which the MTr are considered to be correct. Our main objective is to develop an approach to designing a deductive verifier in a modular and sound way for a given target relational model transformation language, which enables formal verification of the correctness of MTr. To this end, we have developed the VeriMTLr framework. Its role is to assist in designing verifiers that allow verification (via automatic theorem proving) of the correctness of relational model transformations. VeriMTLr draws on the Boogie intermediate verification language to systematically design modular and reusable verifiers for a target relational model transformation language. Our framework encapsulates an EMF metamodels library and an OCL library within Boogie. The result is reduced cost and time required for a verifier’s construction. Furthermore, VeriMTLr includes an ASM and EMFTVM bytecode library, enabling an automated translation validation approach to ensuring the soundness of the verification of the designed verifier. We demonstrate our VeriMTLr framework with the design of verifiers for the Atlas Transformation Language and the SimpleGT graph transformation language.

Subjects/Keywords: Formal Verification; Relational Model Transformations; Intermediate Verification Language

Record DetailsSimilar RecordsGoogle PlusoneFacebookTwitterCiteULikeMendeleyreddit

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

APA (6th Edition):

Cheng, Z. (2016). Formal Verification of Relational Model Transformations using an Intermediate Verification Language. (Thesis). RIAN. Retrieved from http://mural.maynoothuniversity.ie/7089/

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

Chicago Manual of Style (16th Edition):

Cheng, Zheng. “Formal Verification of Relational Model Transformations using an Intermediate Verification Language.” 2016. Thesis, RIAN. Accessed February 26, 2021. http://mural.maynoothuniversity.ie/7089/.

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

MLA Handbook (7th Edition):

Cheng, Zheng. “Formal Verification of Relational Model Transformations using an Intermediate Verification Language.” 2016. Web. 26 Feb 2021.

Vancouver:

Cheng Z. Formal Verification of Relational Model Transformations using an Intermediate Verification Language. [Internet] [Thesis]. RIAN; 2016. [cited 2021 Feb 26]. Available from: http://mural.maynoothuniversity.ie/7089/.

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

Council of Science Editors:

Cheng Z. Formal Verification of Relational Model Transformations using an Intermediate Verification Language. [Thesis]. RIAN; 2016. Available from: http://mural.maynoothuniversity.ie/7089/

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation


University of New South Wales

3. Zadarnowski, Patryk. C, Lambda Calculus and Compiler Verification - a study in Haskell of purely-functional techniques for a formal specification of imperative programming languages and an epistemically-sound verification of their compilers.

Degree: Computer Science & Engineering, 2011, University of New South Wales

Formal verification of a compiler is a long-standing problem in computer science and,although recent years have seen substantial achievements in the area, most of the proposedsolutions do not scale very well with the complexity of modern software developmentenvironments. In this thesis, I present a formal semantic model of the popularC programming language described in the ANSI/ISO/IEC Standard 9899:1990, in theform of a mapping of C programs to computable functions expressed in a suitable variantof lambda calculus. The specification is formulated in a highly readable functionalstyle and is accompanied by a complete Haskell implementation of the compiler, coveringall aspects of the translation from a parse tree of a C program down to the actualsequence of executable machine instructions, resolving issues of separate compilation,allowing for optimising program transformations and providing rigorous guarantees ofthe implementation's conformance to a formal definition of the language.In order to achieve these goals, I revisit the challenge of compiler verificationfrom its very philosophical foundations. Beginning with the basic epistemic notions ofknowledge, correctness and proof, I show that a fully rigorous solution of the problemrequires a constructive formulation of the correctness criteria in terms of the translationprocess itself, in contrast with the more popular extensional approaches to compilerverification, in which correctness is generally defined as commutativity of the systemwith respect to a formal semantics of the source and target languages, effectively formalisingvarious aspects of the compiler independently of each other and separatelyfrom its eventual implementation. I argue that a satisfactory judgement of correctnessshould always constitute a direct formal description of the job performed by the softwarebeing judged, instead of an axiomatic definition of some abstract property suchas commutativity of the translation system, since the later approach fails to establish acrucial causal connection between a judgement of correctness and a knowledge of it.The primary contribution of this thesis is the new notion of linear correctness,which strives to provide a constructive formulation of a compiler's validity criteria byderiving its judgement directly from a formal description of the language translationprocess itself. The approach relies crucially on a denotational semantic model of thesource and target languages, in which the domains of program meanings are unifiedwith the actual intermediate program representation of the underlying compiler implementation.By defining the concepts of a programming language, compiler and compilercorrectness in category theoretic terms, I show that every linearly correct compileris also valid in the more traditional sense of the word. Further, by presenting a completeverified translation of the standard C programming language within this framework, Idemonstrate that linear correctness is a highly effective approach to the problem ofcompiler verification and that it scales… Advisors/Committee Members: Chakravarty, Manuel M.T., Computer Science & Engineering, Faculty of Engineering, UNSW.

Subjects/Keywords: Lambda calculus; C; Programming languages; Compiler verification; Language semantics; ANSI/ISO/IEC 9899:1990; Haskell; Purely functional intermediate representations

Record DetailsSimilar RecordsGoogle PlusoneFacebookTwitterCiteULikeMendeleyreddit

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

APA (6th Edition):

Zadarnowski, P. (2011). C, Lambda Calculus and Compiler Verification - a study in Haskell of purely-functional techniques for a formal specification of imperative programming languages and an epistemically-sound verification of their compilers. (Doctoral Dissertation). University of New South Wales. Retrieved from http://handle.unsw.edu.au/1959.4/50242 ; https://unsworks.unsw.edu.au/fapi/datastream/unsworks:9120/SOURCE02?view=true

Chicago Manual of Style (16th Edition):

Zadarnowski, Patryk. “C, Lambda Calculus and Compiler Verification - a study in Haskell of purely-functional techniques for a formal specification of imperative programming languages and an epistemically-sound verification of their compilers.” 2011. Doctoral Dissertation, University of New South Wales. Accessed February 26, 2021. http://handle.unsw.edu.au/1959.4/50242 ; https://unsworks.unsw.edu.au/fapi/datastream/unsworks:9120/SOURCE02?view=true.

MLA Handbook (7th Edition):

Zadarnowski, Patryk. “C, Lambda Calculus and Compiler Verification - a study in Haskell of purely-functional techniques for a formal specification of imperative programming languages and an epistemically-sound verification of their compilers.” 2011. Web. 26 Feb 2021.

Vancouver:

Zadarnowski P. C, Lambda Calculus and Compiler Verification - a study in Haskell of purely-functional techniques for a formal specification of imperative programming languages and an epistemically-sound verification of their compilers. [Internet] [Doctoral dissertation]. University of New South Wales; 2011. [cited 2021 Feb 26]. Available from: http://handle.unsw.edu.au/1959.4/50242 ; https://unsworks.unsw.edu.au/fapi/datastream/unsworks:9120/SOURCE02?view=true.

Council of Science Editors:

Zadarnowski P. C, Lambda Calculus and Compiler Verification - a study in Haskell of purely-functional techniques for a formal specification of imperative programming languages and an epistemically-sound verification of their compilers. [Doctoral Dissertation]. University of New South Wales; 2011. Available from: http://handle.unsw.edu.au/1959.4/50242 ; https://unsworks.unsw.edu.au/fapi/datastream/unsworks:9120/SOURCE02?view=true

.