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:(Formal verification). Showing records 1 – 30 of 469 total matches.

[1] [2] [3] [4] [5] … [16]

Search Limiters

Last 2 Years | English Only

Degrees

Levels

Languages

Country

▼ Search Limiters


University of Waterloo

1. Shehata, Hazem. Formal Verification of Instruction Dependencies in Microprocessors.

Degree: 2011, University of Waterloo

 In microprocessors, achieving an efficient utilization of the execution units is a key factor in improving performance. However, maintaining an uninterrupted flow of instructions is… (more)

Subjects/Keywords: Formal Verification; Microprocessors

Record DetailsSimilar RecordsGoogle PlusoneFacebookTwitterCiteULikeMendeleyreddit

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

APA (6th Edition):

Shehata, H. (2011). Formal Verification of Instruction Dependencies in Microprocessors. (Thesis). University of Waterloo. Retrieved from http://hdl.handle.net/10012/6102

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):

Shehata, Hazem. “Formal Verification of Instruction Dependencies in Microprocessors.” 2011. Thesis, University of Waterloo. Accessed January 17, 2021. http://hdl.handle.net/10012/6102.

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

MLA Handbook (7th Edition):

Shehata, Hazem. “Formal Verification of Instruction Dependencies in Microprocessors.” 2011. Web. 17 Jan 2021.

Vancouver:

Shehata H. Formal Verification of Instruction Dependencies in Microprocessors. [Internet] [Thesis]. University of Waterloo; 2011. [cited 2021 Jan 17]. Available from: http://hdl.handle.net/10012/6102.

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

Council of Science Editors:

Shehata H. Formal Verification of Instruction Dependencies in Microprocessors. [Thesis]. University of Waterloo; 2011. Available from: http://hdl.handle.net/10012/6102

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


Texas A&M University

2. Zheng, Qingran. Hybrid Verification for Analog and Mixed-signal Circuits.

Degree: MS, Computer Engineering, 2017, Texas A&M University

 With increasing design complexity and reliability requirements, analog and mixedsignal (AMS) verification manifests itself as a key bottleneck. While formal methods and machine learning have… (more)

Subjects/Keywords: AMS Verification; Formal Verification; Machine Learning

Record DetailsSimilar RecordsGoogle PlusoneFacebookTwitterCiteULikeMendeleyreddit

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

APA (6th Edition):

Zheng, Q. (2017). Hybrid Verification for Analog and Mixed-signal Circuits. (Masters Thesis). Texas A&M University. Retrieved from http://hdl.handle.net/1969.1/173237

Chicago Manual of Style (16th Edition):

Zheng, Qingran. “Hybrid Verification for Analog and Mixed-signal Circuits.” 2017. Masters Thesis, Texas A&M University. Accessed January 17, 2021. http://hdl.handle.net/1969.1/173237.

MLA Handbook (7th Edition):

Zheng, Qingran. “Hybrid Verification for Analog and Mixed-signal Circuits.” 2017. Web. 17 Jan 2021.

Vancouver:

Zheng Q. Hybrid Verification for Analog and Mixed-signal Circuits. [Internet] [Masters thesis]. Texas A&M University; 2017. [cited 2021 Jan 17]. Available from: http://hdl.handle.net/1969.1/173237.

Council of Science Editors:

Zheng Q. Hybrid Verification for Analog and Mixed-signal Circuits. [Masters Thesis]. Texas A&M University; 2017. Available from: http://hdl.handle.net/1969.1/173237


University of New South Wales

3. Greenaway, David. Automated proof-producing abstraction of C code.

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

 Before software can be formally reasoned about, it must first be represented in some form of logic. There are two approaches to carrying out this… (more)

Subjects/Keywords: Interactive Theorem Proving; Formal Verification; Program Verification

Record DetailsSimilar RecordsGoogle PlusoneFacebookTwitterCiteULikeMendeleyreddit

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

APA (6th Edition):

Greenaway, D. (2014). Automated proof-producing abstraction of C code. (Doctoral Dissertation). University of New South Wales. Retrieved from http://handle.unsw.edu.au/1959.4/54260 ; https://unsworks.unsw.edu.au/fapi/datastream/unsworks:13743/SOURCE02?view=true

Chicago Manual of Style (16th Edition):

Greenaway, David. “Automated proof-producing abstraction of C code.” 2014. Doctoral Dissertation, University of New South Wales. Accessed January 17, 2021. http://handle.unsw.edu.au/1959.4/54260 ; https://unsworks.unsw.edu.au/fapi/datastream/unsworks:13743/SOURCE02?view=true.

MLA Handbook (7th Edition):

Greenaway, David. “Automated proof-producing abstraction of C code.” 2014. Web. 17 Jan 2021.

Vancouver:

Greenaway D. Automated proof-producing abstraction of C code. [Internet] [Doctoral dissertation]. University of New South Wales; 2014. [cited 2021 Jan 17]. Available from: http://handle.unsw.edu.au/1959.4/54260 ; https://unsworks.unsw.edu.au/fapi/datastream/unsworks:13743/SOURCE02?view=true.

Council of Science Editors:

Greenaway D. Automated proof-producing abstraction of C code. [Doctoral Dissertation]. University of New South Wales; 2014. Available from: http://handle.unsw.edu.au/1959.4/54260 ; https://unsworks.unsw.edu.au/fapi/datastream/unsworks:13743/SOURCE02?view=true


Rice University

4. Song, Daniel W. The Design and Implementation of a Verified File System with End-to-End Data Integrity.

Degree: PhD, Engineering, 2020, Rice University

 Despite significant research and engineering efforts, many of today's important computer systems suffer from bugs. To increase the reliability of software systems, recent work has… (more)

Subjects/Keywords: software security; systems; formal verification

Record DetailsSimilar RecordsGoogle PlusoneFacebookTwitterCiteULikeMendeleyreddit

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

APA (6th Edition):

Song, D. W. (2020). The Design and Implementation of a Verified File System with End-to-End Data Integrity. (Doctoral Dissertation). Rice University. Retrieved from http://hdl.handle.net/1911/108425

Chicago Manual of Style (16th Edition):

Song, Daniel W. “The Design and Implementation of a Verified File System with End-to-End Data Integrity.” 2020. Doctoral Dissertation, Rice University. Accessed January 17, 2021. http://hdl.handle.net/1911/108425.

MLA Handbook (7th Edition):

Song, Daniel W. “The Design and Implementation of a Verified File System with End-to-End Data Integrity.” 2020. Web. 17 Jan 2021.

Vancouver:

Song DW. The Design and Implementation of a Verified File System with End-to-End Data Integrity. [Internet] [Doctoral dissertation]. Rice University; 2020. [cited 2021 Jan 17]. Available from: http://hdl.handle.net/1911/108425.

Council of Science Editors:

Song DW. The Design and Implementation of a Verified File System with End-to-End Data Integrity. [Doctoral Dissertation]. Rice University; 2020. Available from: http://hdl.handle.net/1911/108425


Georgia Tech

5. Bobek, Jan. Hidden fallacies in formally verified systems.

Degree: MS, Computer Science, 2020, Georgia Tech

Formal verification or formal methods represent a rising trend in approaches to correct software construction, i.e. they help us answer the question of how to… (more)

Subjects/Keywords: Formal verification; Fuzzing; File systems

Record DetailsSimilar RecordsGoogle PlusoneFacebookTwitterCiteULikeMendeleyreddit

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

APA (6th Edition):

Bobek, J. (2020). Hidden fallacies in formally verified systems. (Masters Thesis). Georgia Tech. Retrieved from http://hdl.handle.net/1853/62855

Chicago Manual of Style (16th Edition):

Bobek, Jan. “Hidden fallacies in formally verified systems.” 2020. Masters Thesis, Georgia Tech. Accessed January 17, 2021. http://hdl.handle.net/1853/62855.

MLA Handbook (7th Edition):

Bobek, Jan. “Hidden fallacies in formally verified systems.” 2020. Web. 17 Jan 2021.

Vancouver:

Bobek J. Hidden fallacies in formally verified systems. [Internet] [Masters thesis]. Georgia Tech; 2020. [cited 2021 Jan 17]. Available from: http://hdl.handle.net/1853/62855.

Council of Science Editors:

Bobek J. Hidden fallacies in formally verified systems. [Masters Thesis]. Georgia Tech; 2020. Available from: http://hdl.handle.net/1853/62855


University of Edinburgh

6. Butler, David Thomas. Formalising cryptography using CryptHOL.

Degree: PhD, 2020, University of Edinburgh

 Security proofs are now a cornerstone of modern cryptography. Provable security has greatly increased the level of rigour of the security statements, however proofs of… (more)

Subjects/Keywords: formal verification; cryptography; Isabelle/HOL

Record DetailsSimilar RecordsGoogle PlusoneFacebookTwitterCiteULikeMendeleyreddit

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

APA (6th Edition):

Butler, D. T. (2020). Formalising cryptography using CryptHOL. (Doctoral Dissertation). University of Edinburgh. Retrieved from https://doi.org/10.7488/era/510 ; https://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.814924

Chicago Manual of Style (16th Edition):

Butler, David Thomas. “Formalising cryptography using CryptHOL.” 2020. Doctoral Dissertation, University of Edinburgh. Accessed January 17, 2021. https://doi.org/10.7488/era/510 ; https://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.814924.

MLA Handbook (7th Edition):

Butler, David Thomas. “Formalising cryptography using CryptHOL.” 2020. Web. 17 Jan 2021.

Vancouver:

Butler DT. Formalising cryptography using CryptHOL. [Internet] [Doctoral dissertation]. University of Edinburgh; 2020. [cited 2021 Jan 17]. Available from: https://doi.org/10.7488/era/510 ; https://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.814924.

Council of Science Editors:

Butler DT. Formalising cryptography using CryptHOL. [Doctoral Dissertation]. University of Edinburgh; 2020. Available from: https://doi.org/10.7488/era/510 ; https://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.814924


Texas A&M University

7. Kottapalli, Venkateshwar. Formal Verification of a MESI-based Cache Implementation.

Degree: MS, Computer Engineering, 2017, Texas A&M University

 Cache coherency is crucial to multi-core systems with a shared memory programming model. Coherency protocols have been formally verified at the architectural level with relative… (more)

Subjects/Keywords: Verification; Cache; Coherence; Memory Consistency; Formal Verification; Model Checking; RTL; Formal Property Verification; UVM; MESI

Record DetailsSimilar RecordsGoogle PlusoneFacebookTwitterCiteULikeMendeleyreddit

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

APA (6th Edition):

Kottapalli, V. (2017). Formal Verification of a MESI-based Cache Implementation. (Masters Thesis). Texas A&M University. Retrieved from http://hdl.handle.net/1969.1/165866

Chicago Manual of Style (16th Edition):

Kottapalli, Venkateshwar. “Formal Verification of a MESI-based Cache Implementation.” 2017. Masters Thesis, Texas A&M University. Accessed January 17, 2021. http://hdl.handle.net/1969.1/165866.

MLA Handbook (7th Edition):

Kottapalli, Venkateshwar. “Formal Verification of a MESI-based Cache Implementation.” 2017. Web. 17 Jan 2021.

Vancouver:

Kottapalli V. Formal Verification of a MESI-based Cache Implementation. [Internet] [Masters thesis]. Texas A&M University; 2017. [cited 2021 Jan 17]. Available from: http://hdl.handle.net/1969.1/165866.

Council of Science Editors:

Kottapalli V. Formal Verification of a MESI-based Cache Implementation. [Masters Thesis]. Texas A&M University; 2017. Available from: http://hdl.handle.net/1969.1/165866


University of Utah

8. Xu, Yang. Algorithms for automatic generation of relative timing constraints.

Degree: PhD, Electrical & Computer Engineering, 2011, University of Utah

 Asynchronous circuits exhibit impressive power and performance benefits over its synchronous counterpart. Asynchronous system design, however, is not widely adopted due to the fact that… (more)

Subjects/Keywords: Asynchronous circuits; Formal verification; Relative timing

Record DetailsSimilar RecordsGoogle PlusoneFacebookTwitterCiteULikeMendeleyreddit

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

APA (6th Edition):

Xu, Y. (2011). Algorithms for automatic generation of relative timing constraints. (Doctoral Dissertation). University of Utah. Retrieved from http://content.lib.utah.edu/cdm/singleitem/collection/etd3/id/197/rec/177

Chicago Manual of Style (16th Edition):

Xu, Yang. “Algorithms for automatic generation of relative timing constraints.” 2011. Doctoral Dissertation, University of Utah. Accessed January 17, 2021. http://content.lib.utah.edu/cdm/singleitem/collection/etd3/id/197/rec/177.

MLA Handbook (7th Edition):

Xu, Yang. “Algorithms for automatic generation of relative timing constraints.” 2011. Web. 17 Jan 2021.

Vancouver:

Xu Y. Algorithms for automatic generation of relative timing constraints. [Internet] [Doctoral dissertation]. University of Utah; 2011. [cited 2021 Jan 17]. Available from: http://content.lib.utah.edu/cdm/singleitem/collection/etd3/id/197/rec/177.

Council of Science Editors:

Xu Y. Algorithms for automatic generation of relative timing constraints. [Doctoral Dissertation]. University of Utah; 2011. Available from: http://content.lib.utah.edu/cdm/singleitem/collection/etd3/id/197/rec/177


Tampere University

9. Biswas, Prasun. Model-to-Model Transformation Of Nuclear Industry I&C Logic To Assist Model Checking .

Degree: 2020, Tampere University

 The demand for electricity has increased proportionately with massive urbanisation and in-dustrialisation. Nuclear energy is a strong candidate which can be one of the solutions… (more)

Subjects/Keywords: Model Transformation ; Formal Verification ; Model Checking ; NuSMV

Record DetailsSimilar RecordsGoogle PlusoneFacebookTwitterCiteULikeMendeleyreddit

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

APA (6th Edition):

Biswas, P. (2020). Model-to-Model Transformation Of Nuclear Industry I&C Logic To Assist Model Checking . (Masters Thesis). Tampere University. Retrieved from https://trepo.tuni.fi/handle/10024/121539

Chicago Manual of Style (16th Edition):

Biswas, Prasun. “Model-to-Model Transformation Of Nuclear Industry I&C Logic To Assist Model Checking .” 2020. Masters Thesis, Tampere University. Accessed January 17, 2021. https://trepo.tuni.fi/handle/10024/121539.

MLA Handbook (7th Edition):

Biswas, Prasun. “Model-to-Model Transformation Of Nuclear Industry I&C Logic To Assist Model Checking .” 2020. Web. 17 Jan 2021.

Vancouver:

Biswas P. Model-to-Model Transformation Of Nuclear Industry I&C Logic To Assist Model Checking . [Internet] [Masters thesis]. Tampere University; 2020. [cited 2021 Jan 17]. Available from: https://trepo.tuni.fi/handle/10024/121539.

Council of Science Editors:

Biswas P. Model-to-Model Transformation Of Nuclear Industry I&C Logic To Assist Model Checking . [Masters Thesis]. Tampere University; 2020. Available from: https://trepo.tuni.fi/handle/10024/121539


University of Ottawa

10. Sistany, Bahman. A Certified Core Policy Language .

Degree: 2016, University of Ottawa

 We present the design and implementation of a Certified Core Policy Language (ACCPL) that can be used to express access-control rules and policies. Although full-blown… (more)

Subjects/Keywords: access-control; formal verification; proofs; policy language

Record DetailsSimilar RecordsGoogle PlusoneFacebookTwitterCiteULikeMendeleyreddit

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

APA (6th Edition):

Sistany, B. (2016). A Certified Core Policy Language . (Thesis). University of Ottawa. Retrieved from http://hdl.handle.net/10393/34865

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):

Sistany, Bahman. “A Certified Core Policy Language .” 2016. Thesis, University of Ottawa. Accessed January 17, 2021. http://hdl.handle.net/10393/34865.

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

MLA Handbook (7th Edition):

Sistany, Bahman. “A Certified Core Policy Language .” 2016. Web. 17 Jan 2021.

Vancouver:

Sistany B. A Certified Core Policy Language . [Internet] [Thesis]. University of Ottawa; 2016. [cited 2021 Jan 17]. Available from: http://hdl.handle.net/10393/34865.

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

Council of Science Editors:

Sistany B. A Certified Core Policy Language . [Thesis]. University of Ottawa; 2016. Available from: http://hdl.handle.net/10393/34865

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


University of Newcastle

11. Hogavanaghatta Kumaraswamy, Jnanamurthy. Model-driven engineering to enhance the reliability of software development by verifying system properties and detecting clones.

Degree: PhD, 2019, University of Newcastle

Research Doctorate - Doctor of Philosophy (PhD)

Computer software is used in almost every facet of day-to-day life, such as air conditioners, refrigerators, washing machines,… (more)

Subjects/Keywords: formal verification; model-driven engineering; software clones

Record DetailsSimilar RecordsGoogle PlusoneFacebookTwitterCiteULikeMendeleyreddit

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

APA (6th Edition):

Hogavanaghatta Kumaraswamy, J. (2019). Model-driven engineering to enhance the reliability of software development by verifying system properties and detecting clones. (Doctoral Dissertation). University of Newcastle. Retrieved from http://hdl.handle.net/1959.13/1397849

Chicago Manual of Style (16th Edition):

Hogavanaghatta Kumaraswamy, Jnanamurthy. “Model-driven engineering to enhance the reliability of software development by verifying system properties and detecting clones.” 2019. Doctoral Dissertation, University of Newcastle. Accessed January 17, 2021. http://hdl.handle.net/1959.13/1397849.

MLA Handbook (7th Edition):

Hogavanaghatta Kumaraswamy, Jnanamurthy. “Model-driven engineering to enhance the reliability of software development by verifying system properties and detecting clones.” 2019. Web. 17 Jan 2021.

Vancouver:

Hogavanaghatta Kumaraswamy J. Model-driven engineering to enhance the reliability of software development by verifying system properties and detecting clones. [Internet] [Doctoral dissertation]. University of Newcastle; 2019. [cited 2021 Jan 17]. Available from: http://hdl.handle.net/1959.13/1397849.

Council of Science Editors:

Hogavanaghatta Kumaraswamy J. Model-driven engineering to enhance the reliability of software development by verifying system properties and detecting clones. [Doctoral Dissertation]. University of Newcastle; 2019. Available from: http://hdl.handle.net/1959.13/1397849


University of Colorado

12. Hassan, Zyad. Incremental, Inductive Model Checking.

Degree: PhD, Electrical, Computer & Energy Engineering, 2014, University of Colorado

  Model checking has become a widely adopted approach for the verification of hardware designs. The ever increasing complexity of these designs creates a continuous… (more)

Subjects/Keywords: Formal Verification; Model Checking; Satisfiability; Computer Engineering

Record DetailsSimilar RecordsGoogle PlusoneFacebookTwitterCiteULikeMendeleyreddit

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

APA (6th Edition):

Hassan, Z. (2014). Incremental, Inductive Model Checking. (Doctoral Dissertation). University of Colorado. Retrieved from https://scholar.colorado.edu/ecen_gradetds/86

Chicago Manual of Style (16th Edition):

Hassan, Zyad. “Incremental, Inductive Model Checking.” 2014. Doctoral Dissertation, University of Colorado. Accessed January 17, 2021. https://scholar.colorado.edu/ecen_gradetds/86.

MLA Handbook (7th Edition):

Hassan, Zyad. “Incremental, Inductive Model Checking.” 2014. Web. 17 Jan 2021.

Vancouver:

Hassan Z. Incremental, Inductive Model Checking. [Internet] [Doctoral dissertation]. University of Colorado; 2014. [cited 2021 Jan 17]. Available from: https://scholar.colorado.edu/ecen_gradetds/86.

Council of Science Editors:

Hassan Z. Incremental, Inductive Model Checking. [Doctoral Dissertation]. University of Colorado; 2014. Available from: https://scholar.colorado.edu/ecen_gradetds/86


University of Manchester

13. Carter, Rebekah. Verification of liveness properties on hybrid dynamical systems.

Degree: PhD, 2013, University of Manchester

 A hybrid dynamical system is a mathematical model for a part of the real world where discrete and continuous parts interact with each other. Typically… (more)

Subjects/Keywords: 511; Hybrid systems; Formal verification; Liveness

Record DetailsSimilar RecordsGoogle PlusoneFacebookTwitterCiteULikeMendeleyreddit

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

APA (6th Edition):

Carter, R. (2013). Verification of liveness properties on hybrid dynamical systems. (Doctoral Dissertation). University of Manchester. Retrieved from https://www.research.manchester.ac.uk/portal/en/theses/verification-of-liveness-properties-on-hybrid-dynamical-systems(8817319c-a63f-4cf3-927d-a2ddf69139b4).html ; http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.576886

Chicago Manual of Style (16th Edition):

Carter, Rebekah. “Verification of liveness properties on hybrid dynamical systems.” 2013. Doctoral Dissertation, University of Manchester. Accessed January 17, 2021. https://www.research.manchester.ac.uk/portal/en/theses/verification-of-liveness-properties-on-hybrid-dynamical-systems(8817319c-a63f-4cf3-927d-a2ddf69139b4).html ; http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.576886.

MLA Handbook (7th Edition):

Carter, Rebekah. “Verification of liveness properties on hybrid dynamical systems.” 2013. Web. 17 Jan 2021.

Vancouver:

Carter R. Verification of liveness properties on hybrid dynamical systems. [Internet] [Doctoral dissertation]. University of Manchester; 2013. [cited 2021 Jan 17]. Available from: https://www.research.manchester.ac.uk/portal/en/theses/verification-of-liveness-properties-on-hybrid-dynamical-systems(8817319c-a63f-4cf3-927d-a2ddf69139b4).html ; http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.576886.

Council of Science Editors:

Carter R. Verification of liveness properties on hybrid dynamical systems. [Doctoral Dissertation]. University of Manchester; 2013. Available from: https://www.research.manchester.ac.uk/portal/en/theses/verification-of-liveness-properties-on-hybrid-dynamical-systems(8817319c-a63f-4cf3-927d-a2ddf69139b4).html ; http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.576886


University of Illinois – Urbana-Champaign

14. Katelman, Michael. A meta-language for functional verification.

Degree: PhD, 0112, 2012, University of Illinois – Urbana-Champaign

 This dissertation perceives a similarity between two activities: that of coordinating the search for simulation traces toward reaching verification closure, and that of coordinating the… (more)

Subjects/Keywords: Programming Languages; Formal Methods; Hardware Verification

Record DetailsSimilar RecordsGoogle PlusoneFacebookTwitterCiteULikeMendeleyreddit

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

APA (6th Edition):

Katelman, M. (2012). A meta-language for functional verification. (Doctoral Dissertation). University of Illinois – Urbana-Champaign. Retrieved from http://hdl.handle.net/2142/29614

Chicago Manual of Style (16th Edition):

Katelman, Michael. “A meta-language for functional verification.” 2012. Doctoral Dissertation, University of Illinois – Urbana-Champaign. Accessed January 17, 2021. http://hdl.handle.net/2142/29614.

MLA Handbook (7th Edition):

Katelman, Michael. “A meta-language for functional verification.” 2012. Web. 17 Jan 2021.

Vancouver:

Katelman M. A meta-language for functional verification. [Internet] [Doctoral dissertation]. University of Illinois – Urbana-Champaign; 2012. [cited 2021 Jan 17]. Available from: http://hdl.handle.net/2142/29614.

Council of Science Editors:

Katelman M. A meta-language for functional verification. [Doctoral Dissertation]. University of Illinois – Urbana-Champaign; 2012. Available from: http://hdl.handle.net/2142/29614


University of Illinois – Urbana-Champaign

15. Kheradmand, Ali. A formal semantics of P4 and applications.

Degree: MS, Computer Science, 2018, University of Illinois – Urbana-Champaign

 Programmable packet processors and P4 as a programming language for such devices have gained significant interest, because their flexibility enables rapid development of a diverse… (more)

Subjects/Keywords: Formal Semantics; P4; K Framework; Network Verification

Record DetailsSimilar RecordsGoogle PlusoneFacebookTwitterCiteULikeMendeleyreddit

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

APA (6th Edition):

Kheradmand, A. (2018). A formal semantics of P4 and applications. (Thesis). University of Illinois – Urbana-Champaign. Retrieved from http://hdl.handle.net/2142/102486

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):

Kheradmand, Ali. “A formal semantics of P4 and applications.” 2018. Thesis, University of Illinois – Urbana-Champaign. Accessed January 17, 2021. http://hdl.handle.net/2142/102486.

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

MLA Handbook (7th Edition):

Kheradmand, Ali. “A formal semantics of P4 and applications.” 2018. Web. 17 Jan 2021.

Vancouver:

Kheradmand A. A formal semantics of P4 and applications. [Internet] [Thesis]. University of Illinois – Urbana-Champaign; 2018. [cited 2021 Jan 17]. Available from: http://hdl.handle.net/2142/102486.

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

Council of Science Editors:

Kheradmand A. A formal semantics of P4 and applications. [Thesis]. University of Illinois – Urbana-Champaign; 2018. Available from: http://hdl.handle.net/2142/102486

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


Boise State University

16. Joshaghani, Rezvan. UNICORN Framework: A User-Centric Approach Toward Formal Verification of Privacy Norms.

Degree: 2019, Boise State University

 In the development of complex systems, such as user-centric privacy management systems with multiple components and attributes, it is important to formalize the process and… (more)

Subjects/Keywords: privacy; formal verification; Other Computer Engineering

Record DetailsSimilar RecordsGoogle PlusoneFacebookTwitterCiteULikeMendeleyreddit

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

APA (6th Edition):

Joshaghani, R. (2019). UNICORN Framework: A User-Centric Approach Toward Formal Verification of Privacy Norms. (Thesis). Boise State University. Retrieved from https://scholarworks.boisestate.edu/td/1526

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):

Joshaghani, Rezvan. “UNICORN Framework: A User-Centric Approach Toward Formal Verification of Privacy Norms.” 2019. Thesis, Boise State University. Accessed January 17, 2021. https://scholarworks.boisestate.edu/td/1526.

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

MLA Handbook (7th Edition):

Joshaghani, Rezvan. “UNICORN Framework: A User-Centric Approach Toward Formal Verification of Privacy Norms.” 2019. Web. 17 Jan 2021.

Vancouver:

Joshaghani R. UNICORN Framework: A User-Centric Approach Toward Formal Verification of Privacy Norms. [Internet] [Thesis]. Boise State University; 2019. [cited 2021 Jan 17]. Available from: https://scholarworks.boisestate.edu/td/1526.

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

Council of Science Editors:

Joshaghani R. UNICORN Framework: A User-Centric Approach Toward Formal Verification of Privacy Norms. [Thesis]. Boise State University; 2019. Available from: https://scholarworks.boisestate.edu/td/1526

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


Clemson University

17. Smith, Hampton. Engineering Specifications and Mathematics for Verified Software.

Degree: PhD, Computer Science, 2013, Clemson University

 Developing a verifying compiler – a compiler that proves that components are correct with respect to their specifications – is a grand challenge for the computing community.… (more)

Subjects/Keywords: Formal Methods; Specficiation; Verification; Computer Sciences

Record DetailsSimilar RecordsGoogle PlusoneFacebookTwitterCiteULikeMendeleyreddit

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

APA (6th Edition):

Smith, H. (2013). Engineering Specifications and Mathematics for Verified Software. (Doctoral Dissertation). Clemson University. Retrieved from https://tigerprints.clemson.edu/all_dissertations/1132

Chicago Manual of Style (16th Edition):

Smith, Hampton. “Engineering Specifications and Mathematics for Verified Software.” 2013. Doctoral Dissertation, Clemson University. Accessed January 17, 2021. https://tigerprints.clemson.edu/all_dissertations/1132.

MLA Handbook (7th Edition):

Smith, Hampton. “Engineering Specifications and Mathematics for Verified Software.” 2013. Web. 17 Jan 2021.

Vancouver:

Smith H. Engineering Specifications and Mathematics for Verified Software. [Internet] [Doctoral dissertation]. Clemson University; 2013. [cited 2021 Jan 17]. Available from: https://tigerprints.clemson.edu/all_dissertations/1132.

Council of Science Editors:

Smith H. Engineering Specifications and Mathematics for Verified Software. [Doctoral Dissertation]. Clemson University; 2013. Available from: https://tigerprints.clemson.edu/all_dissertations/1132

18. Sogokon, Andrew. Direct methods for deductive verification of temporal properties in continuous dynamical systems.

Degree: PhD, 2016, University of Edinburgh

 This thesis is concerned with the problem of formal verification of correctness specifications for continuous and hybrid dynamical systems. Our main focus will be on… (more)

Subjects/Keywords: 004.2; hybrid systems; ODEs; formal verification

Record DetailsSimilar RecordsGoogle PlusoneFacebookTwitterCiteULikeMendeleyreddit

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

APA (6th Edition):

Sogokon, A. (2016). Direct methods for deductive verification of temporal properties in continuous dynamical systems. (Doctoral Dissertation). University of Edinburgh. Retrieved from http://hdl.handle.net/1842/20952

Chicago Manual of Style (16th Edition):

Sogokon, Andrew. “Direct methods for deductive verification of temporal properties in continuous dynamical systems.” 2016. Doctoral Dissertation, University of Edinburgh. Accessed January 17, 2021. http://hdl.handle.net/1842/20952.

MLA Handbook (7th Edition):

Sogokon, Andrew. “Direct methods for deductive verification of temporal properties in continuous dynamical systems.” 2016. Web. 17 Jan 2021.

Vancouver:

Sogokon A. Direct methods for deductive verification of temporal properties in continuous dynamical systems. [Internet] [Doctoral dissertation]. University of Edinburgh; 2016. [cited 2021 Jan 17]. Available from: http://hdl.handle.net/1842/20952.

Council of Science Editors:

Sogokon A. Direct methods for deductive verification of temporal properties in continuous dynamical systems. [Doctoral Dissertation]. University of Edinburgh; 2016. Available from: http://hdl.handle.net/1842/20952


Kansas State University

19. Zhang, Zhi. A formal approach to contract verification for high-integrity applications.

Degree: PhD, Department of Computing and Information Sciences, 2016, Kansas State University

 High-integrity applications are safety- and security-critical applications developed for a variety of critical tasks. The correctness of these applications must be thoroughly tested or formally… (more)

Subjects/Keywords: Formal Methods; Language Semantics; Program Verification

Record DetailsSimilar RecordsGoogle PlusoneFacebookTwitterCiteULikeMendeleyreddit

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

APA (6th Edition):

Zhang, Z. (2016). A formal approach to contract verification for high-integrity applications. (Doctoral Dissertation). Kansas State University. Retrieved from http://hdl.handle.net/2097/32880

Chicago Manual of Style (16th Edition):

Zhang, Zhi. “A formal approach to contract verification for high-integrity applications.” 2016. Doctoral Dissertation, Kansas State University. Accessed January 17, 2021. http://hdl.handle.net/2097/32880.

MLA Handbook (7th Edition):

Zhang, Zhi. “A formal approach to contract verification for high-integrity applications.” 2016. Web. 17 Jan 2021.

Vancouver:

Zhang Z. A formal approach to contract verification for high-integrity applications. [Internet] [Doctoral dissertation]. Kansas State University; 2016. [cited 2021 Jan 17]. Available from: http://hdl.handle.net/2097/32880.

Council of Science Editors:

Zhang Z. A formal approach to contract verification for high-integrity applications. [Doctoral Dissertation]. Kansas State University; 2016. Available from: http://hdl.handle.net/2097/32880


University of Sydney

20. Subotic, Pavle. Applying Elimination-Based Algorithms to Abstract Interpretation .

Degree: 2014, University of Sydney

 Unbounded abstract domains are used in static program analysis frameworks for representing ranges of variables, and their applications include elimination of assertions in programs, automatically… (more)

Subjects/Keywords: Static Analysis; Abstract Interpretation; Formal Verification; LLVM

Record DetailsSimilar RecordsGoogle PlusoneFacebookTwitterCiteULikeMendeleyreddit

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

APA (6th Edition):

Subotic, P. (2014). Applying Elimination-Based Algorithms to Abstract Interpretation . (Thesis). University of Sydney. Retrieved from http://hdl.handle.net/2123/12052

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):

Subotic, Pavle. “Applying Elimination-Based Algorithms to Abstract Interpretation .” 2014. Thesis, University of Sydney. Accessed January 17, 2021. http://hdl.handle.net/2123/12052.

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

MLA Handbook (7th Edition):

Subotic, Pavle. “Applying Elimination-Based Algorithms to Abstract Interpretation .” 2014. Web. 17 Jan 2021.

Vancouver:

Subotic P. Applying Elimination-Based Algorithms to Abstract Interpretation . [Internet] [Thesis]. University of Sydney; 2014. [cited 2021 Jan 17]. Available from: http://hdl.handle.net/2123/12052.

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

Council of Science Editors:

Subotic P. Applying Elimination-Based Algorithms to Abstract Interpretation . [Thesis]. University of Sydney; 2014. Available from: http://hdl.handle.net/2123/12052

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


University of New South Wales

21. von Tessin, Michael. The clustered multikernel: an approach to formal verification of multiprocessor operating-system kernels.

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

 The key software component of a computer system is the operating-system kernel. Italways needs to be trusted because it runs in the CPU’s privileged mode… (more)

Subjects/Keywords: Microkernel; Formal verification; Multiprocessor; seL4; Isabelle/HOL

Record DetailsSimilar RecordsGoogle PlusoneFacebookTwitterCiteULikeMendeleyreddit

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

APA (6th Edition):

von Tessin, M. (2013). The clustered multikernel: an approach to formal verification of multiprocessor operating-system kernels. (Doctoral Dissertation). University of New South Wales. Retrieved from http://handle.unsw.edu.au/1959.4/53099 ; https://unsworks.unsw.edu.au/fapi/datastream/unsworks:11785/SOURCE01?view=true

Chicago Manual of Style (16th Edition):

von Tessin, Michael. “The clustered multikernel: an approach to formal verification of multiprocessor operating-system kernels.” 2013. Doctoral Dissertation, University of New South Wales. Accessed January 17, 2021. http://handle.unsw.edu.au/1959.4/53099 ; https://unsworks.unsw.edu.au/fapi/datastream/unsworks:11785/SOURCE01?view=true.

MLA Handbook (7th Edition):

von Tessin, Michael. “The clustered multikernel: an approach to formal verification of multiprocessor operating-system kernels.” 2013. Web. 17 Jan 2021.

Vancouver:

von Tessin M. The clustered multikernel: an approach to formal verification of multiprocessor operating-system kernels. [Internet] [Doctoral dissertation]. University of New South Wales; 2013. [cited 2021 Jan 17]. Available from: http://handle.unsw.edu.au/1959.4/53099 ; https://unsworks.unsw.edu.au/fapi/datastream/unsworks:11785/SOURCE01?view=true.

Council of Science Editors:

von Tessin M. The clustered multikernel: an approach to formal verification of multiprocessor operating-system kernels. [Doctoral Dissertation]. University of New South Wales; 2013. Available from: http://handle.unsw.edu.au/1959.4/53099 ; https://unsworks.unsw.edu.au/fapi/datastream/unsworks:11785/SOURCE01?view=true


University of Texas – Austin

22. Yang, Hongkun. Efficient verification of packet networks.

Degree: PhD, Computer science, 2015, University of Texas – Austin

 Network management will benefit from automated tools based upon formal methods. In these tools, the algorithm for computing reachability is the core algorithm for verifying… (more)

Subjects/Keywords: Network verification; Formal methods; Automated tools

Record DetailsSimilar RecordsGoogle PlusoneFacebookTwitterCiteULikeMendeleyreddit

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

APA (6th Edition):

Yang, H. (2015). Efficient verification of packet networks. (Doctoral Dissertation). University of Texas – Austin. Retrieved from http://hdl.handle.net/2152/33271

Chicago Manual of Style (16th Edition):

Yang, Hongkun. “Efficient verification of packet networks.” 2015. Doctoral Dissertation, University of Texas – Austin. Accessed January 17, 2021. http://hdl.handle.net/2152/33271.

MLA Handbook (7th Edition):

Yang, Hongkun. “Efficient verification of packet networks.” 2015. Web. 17 Jan 2021.

Vancouver:

Yang H. Efficient verification of packet networks. [Internet] [Doctoral dissertation]. University of Texas – Austin; 2015. [cited 2021 Jan 17]. Available from: http://hdl.handle.net/2152/33271.

Council of Science Editors:

Yang H. Efficient verification of packet networks. [Doctoral Dissertation]. University of Texas – Austin; 2015. Available from: http://hdl.handle.net/2152/33271


University of New South Wales

23. Kolanski, Rafal Michal. Verification of programs in virtual memory using separation logic.

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

Formal reasoning about programs executing in virtual memory is a difficult problem, as it is an environment in which writing to memory can change its… (more)

Subjects/Keywords: Formal verification; Separation logic; Virtual memory

Record DetailsSimilar RecordsGoogle PlusoneFacebookTwitterCiteULikeMendeleyreddit

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

APA (6th Edition):

Kolanski, R. M. (2011). Verification of programs in virtual memory using separation logic. (Doctoral Dissertation). University of New South Wales. Retrieved from http://handle.unsw.edu.au/1959.4/51288 ; https://unsworks.unsw.edu.au/fapi/datastream/unsworks:9969/SOURCE02?view=true

Chicago Manual of Style (16th Edition):

Kolanski, Rafal Michal. “Verification of programs in virtual memory using separation logic.” 2011. Doctoral Dissertation, University of New South Wales. Accessed January 17, 2021. http://handle.unsw.edu.au/1959.4/51288 ; https://unsworks.unsw.edu.au/fapi/datastream/unsworks:9969/SOURCE02?view=true.

MLA Handbook (7th Edition):

Kolanski, Rafal Michal. “Verification of programs in virtual memory using separation logic.” 2011. Web. 17 Jan 2021.

Vancouver:

Kolanski RM. Verification of programs in virtual memory using separation logic. [Internet] [Doctoral dissertation]. University of New South Wales; 2011. [cited 2021 Jan 17]. Available from: http://handle.unsw.edu.au/1959.4/51288 ; https://unsworks.unsw.edu.au/fapi/datastream/unsworks:9969/SOURCE02?view=true.

Council of Science Editors:

Kolanski RM. Verification of programs in virtual memory using separation logic. [Doctoral Dissertation]. University of New South Wales; 2011. Available from: http://handle.unsw.edu.au/1959.4/51288 ; https://unsworks.unsw.edu.au/fapi/datastream/unsworks:9969/SOURCE02?view=true


The Ohio State University

24. Zaccai, Diego Sebastian. A Balanced Verification Effort for the Java Language.

Degree: PhD, Computer Science and Engineering, 2016, The Ohio State University

 Current tools used to verify software in languages with reference semantics, such as Java, are hampered by the possibility of aliases. Existing approaches to addressing… (more)

Subjects/Keywords: Computer Science; Formal Methods; Software Verification

Record DetailsSimilar RecordsGoogle PlusoneFacebookTwitterCiteULikeMendeleyreddit

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

APA (6th Edition):

Zaccai, D. S. (2016). A Balanced Verification Effort for the Java Language. (Doctoral Dissertation). The Ohio State University. Retrieved from http://rave.ohiolink.edu/etdc/view?acc_num=osu1461243619

Chicago Manual of Style (16th Edition):

Zaccai, Diego Sebastian. “A Balanced Verification Effort for the Java Language.” 2016. Doctoral Dissertation, The Ohio State University. Accessed January 17, 2021. http://rave.ohiolink.edu/etdc/view?acc_num=osu1461243619.

MLA Handbook (7th Edition):

Zaccai, Diego Sebastian. “A Balanced Verification Effort for the Java Language.” 2016. Web. 17 Jan 2021.

Vancouver:

Zaccai DS. A Balanced Verification Effort for the Java Language. [Internet] [Doctoral dissertation]. The Ohio State University; 2016. [cited 2021 Jan 17]. Available from: http://rave.ohiolink.edu/etdc/view?acc_num=osu1461243619.

Council of Science Editors:

Zaccai DS. A Balanced Verification Effort for the Java Language. [Doctoral Dissertation]. The Ohio State University; 2016. Available from: http://rave.ohiolink.edu/etdc/view?acc_num=osu1461243619


University of Oklahoma

25. Ralston, Ryan. Translating Clojure to ACL2 for Verification.

Degree: PhD, 2016, University of Oklahoma

 Software spends a significant portion of its life-cycle in the maintenance phase and over 20% of the maintenance effort is fixing defects. Formal methods, including… (more)

Subjects/Keywords: Software Verification; Formal Methods; Theorem Proving

Record DetailsSimilar RecordsGoogle PlusoneFacebookTwitterCiteULikeMendeleyreddit

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

APA (6th Edition):

Ralston, R. (2016). Translating Clojure to ACL2 for Verification. (Doctoral Dissertation). University of Oklahoma. Retrieved from http://hdl.handle.net/11244/42982

Chicago Manual of Style (16th Edition):

Ralston, Ryan. “Translating Clojure to ACL2 for Verification.” 2016. Doctoral Dissertation, University of Oklahoma. Accessed January 17, 2021. http://hdl.handle.net/11244/42982.

MLA Handbook (7th Edition):

Ralston, Ryan. “Translating Clojure to ACL2 for Verification.” 2016. Web. 17 Jan 2021.

Vancouver:

Ralston R. Translating Clojure to ACL2 for Verification. [Internet] [Doctoral dissertation]. University of Oklahoma; 2016. [cited 2021 Jan 17]. Available from: http://hdl.handle.net/11244/42982.

Council of Science Editors:

Ralston R. Translating Clojure to ACL2 for Verification. [Doctoral Dissertation]. University of Oklahoma; 2016. Available from: http://hdl.handle.net/11244/42982


Universitat Politècnica de València

26. Peiró Frasquet, Salvador. Metodología para hipervisores seguros utilizando técnicas de validación formal .

Degree: 2016, Universitat Politècnica de València

 [EN] The availability of new processors with more processing power for embedded systems has raised the development of applications that tackle problems of greater complexity.… (more)

Subjects/Keywords: Secure Hypervisor construction using formal verification; Partitioned system; Hypervisor; Formal methods; Security; Validation and verification

Record DetailsSimilar RecordsGoogle PlusoneFacebookTwitterCiteULikeMendeleyreddit

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

APA (6th Edition):

Peiró Frasquet, S. (2016). Metodología para hipervisores seguros utilizando técnicas de validación formal . (Doctoral Dissertation). Universitat Politècnica de València. Retrieved from http://hdl.handle.net/10251/63152

Chicago Manual of Style (16th Edition):

Peiró Frasquet, Salvador. “Metodología para hipervisores seguros utilizando técnicas de validación formal .” 2016. Doctoral Dissertation, Universitat Politècnica de València. Accessed January 17, 2021. http://hdl.handle.net/10251/63152.

MLA Handbook (7th Edition):

Peiró Frasquet, Salvador. “Metodología para hipervisores seguros utilizando técnicas de validación formal .” 2016. Web. 17 Jan 2021.

Vancouver:

Peiró Frasquet S. Metodología para hipervisores seguros utilizando técnicas de validación formal . [Internet] [Doctoral dissertation]. Universitat Politècnica de València; 2016. [cited 2021 Jan 17]. Available from: http://hdl.handle.net/10251/63152.

Council of Science Editors:

Peiró Frasquet S. Metodología para hipervisores seguros utilizando técnicas de validación formal . [Doctoral Dissertation]. Universitat Politècnica de València; 2016. Available from: http://hdl.handle.net/10251/63152

27. Bockenek, Joshua A. USIMPL: An Extension of Isabelle/UTP with Simpl-like Control Flow.

Degree: MS, Computer Engineering, 2017, Virginia Tech

 Writing bug-free code is fraught with difficulty, and existing tools for the formal verification of programs do not scale well to large, complicated codebases such… (more)

Subjects/Keywords: Formal Verification; Formal Methods; Isabelle; Unifying Theories of Programming; Verification Condition Generation

Record DetailsSimilar RecordsGoogle PlusoneFacebookTwitterCiteULikeMendeleyreddit

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

APA (6th Edition):

Bockenek, J. A. (2017). USIMPL: An Extension of Isabelle/UTP with Simpl-like Control Flow. (Masters Thesis). Virginia Tech. Retrieved from http://hdl.handle.net/10919/81710

Chicago Manual of Style (16th Edition):

Bockenek, Joshua A. “USIMPL: An Extension of Isabelle/UTP with Simpl-like Control Flow.” 2017. Masters Thesis, Virginia Tech. Accessed January 17, 2021. http://hdl.handle.net/10919/81710.

MLA Handbook (7th Edition):

Bockenek, Joshua A. “USIMPL: An Extension of Isabelle/UTP with Simpl-like Control Flow.” 2017. Web. 17 Jan 2021.

Vancouver:

Bockenek JA. USIMPL: An Extension of Isabelle/UTP with Simpl-like Control Flow. [Internet] [Masters thesis]. Virginia Tech; 2017. [cited 2021 Jan 17]. Available from: http://hdl.handle.net/10919/81710.

Council of Science Editors:

Bockenek JA. USIMPL: An Extension of Isabelle/UTP with Simpl-like Control Flow. [Masters Thesis]. Virginia Tech; 2017. Available from: http://hdl.handle.net/10919/81710


University of Utah

28. Pruss, Tim. Word-level abstraction from combinational circuits using algebraic geometry.

Degree: PhD, Electrical & Computer Engineering, 2015, University of Utah

 Abstraction plays an important role in digital design, analysis, and verification, as it allows for the refinement of functions through different levels of conceptualization. This… (more)

Subjects/Keywords: Abstraction; Digital Design; Formal Verification; Grobner Basis; Hardware Verification

Record DetailsSimilar RecordsGoogle PlusoneFacebookTwitterCiteULikeMendeleyreddit

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

APA (6th Edition):

Pruss, T. (2015). Word-level abstraction from combinational circuits using algebraic geometry. (Doctoral Dissertation). University of Utah. Retrieved from http://content.lib.utah.edu/cdm/singleitem/collection/etd3/id/3965/rec/2938

Chicago Manual of Style (16th Edition):

Pruss, Tim. “Word-level abstraction from combinational circuits using algebraic geometry.” 2015. Doctoral Dissertation, University of Utah. Accessed January 17, 2021. http://content.lib.utah.edu/cdm/singleitem/collection/etd3/id/3965/rec/2938.

MLA Handbook (7th Edition):

Pruss, Tim. “Word-level abstraction from combinational circuits using algebraic geometry.” 2015. Web. 17 Jan 2021.

Vancouver:

Pruss T. Word-level abstraction from combinational circuits using algebraic geometry. [Internet] [Doctoral dissertation]. University of Utah; 2015. [cited 2021 Jan 17]. Available from: http://content.lib.utah.edu/cdm/singleitem/collection/etd3/id/3965/rec/2938.

Council of Science Editors:

Pruss T. Word-level abstraction from combinational circuits using algebraic geometry. [Doctoral Dissertation]. University of Utah; 2015. Available from: http://content.lib.utah.edu/cdm/singleitem/collection/etd3/id/3965/rec/2938

29. 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… (more)

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 January 17, 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. 17 Jan 2021.

Vancouver:

Cheng Z. Formal Verification of Relational Model Transformations using an Intermediate Verification Language. [Internet] [Thesis]. RIAN; 2016. [cited 2021 Jan 17]. 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


Université de Grenoble

30. Damri, Laila. Génération de séquences de test pour l'accélération d'assertions : Generation of test sequences for accelerating assertions.

Degree: Docteur es, Sciences et technologie industrielles, 2012, Université de Grenoble

Avec la complexité croissante des systèmes sur puce, le processus de vérification devient une tâche de plus en plus cruciale à tous les niveaux du… (more)

Subjects/Keywords: Vérification formelle; Vérification à base d'assertions; Formal verification; Assertion-based verification

Record DetailsSimilar RecordsGoogle PlusoneFacebookTwitterCiteULikeMendeleyreddit

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

APA (6th Edition):

Damri, L. (2012). Génération de séquences de test pour l'accélération d'assertions : Generation of test sequences for accelerating assertions. (Doctoral Dissertation). Université de Grenoble. Retrieved from http://www.theses.fr/2012GRENT065

Chicago Manual of Style (16th Edition):

Damri, Laila. “Génération de séquences de test pour l'accélération d'assertions : Generation of test sequences for accelerating assertions.” 2012. Doctoral Dissertation, Université de Grenoble. Accessed January 17, 2021. http://www.theses.fr/2012GRENT065.

MLA Handbook (7th Edition):

Damri, Laila. “Génération de séquences de test pour l'accélération d'assertions : Generation of test sequences for accelerating assertions.” 2012. Web. 17 Jan 2021.

Vancouver:

Damri L. Génération de séquences de test pour l'accélération d'assertions : Generation of test sequences for accelerating assertions. [Internet] [Doctoral dissertation]. Université de Grenoble; 2012. [cited 2021 Jan 17]. Available from: http://www.theses.fr/2012GRENT065.

Council of Science Editors:

Damri L. Génération de séquences de test pour l'accélération d'assertions : Generation of test sequences for accelerating assertions. [Doctoral Dissertation]. Université de Grenoble; 2012. Available from: http://www.theses.fr/2012GRENT065

[1] [2] [3] [4] [5] … [16]

.