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 396 total matches.

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

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 27, 2020. 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. 27 Jan 2020.

Vancouver:

Shehata H. Formal Verification of Instruction Dependencies in Microprocessors. [Internet] [Thesis]. University of Waterloo; 2011. [cited 2020 Jan 27]. 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 27, 2020. http://hdl.handle.net/1969.1/173237.

MLA Handbook (7th Edition):

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

Vancouver:

Zheng Q. Hybrid Verification for Analog and Mixed-signal Circuits. [Internet] [Masters thesis]. Texas A&M University; 2017. [cited 2020 Jan 27]. 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 27, 2020. 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. 27 Jan 2020.

Vancouver:

Greenaway D. Automated proof-producing abstraction of C code. [Internet] [Doctoral dissertation]. University of New South Wales; 2014. [cited 2020 Jan 27]. 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


University of Waterloo

4. Vediramana Krishnan, Hari Govind. Strong Induction in Hardware Model Checking.

Degree: 2019, University of Waterloo

 Symbolic Model checking is a widely used technique for automated verification of both hardware and software systems. Unbounded SAT-based Symbolic Model Checking (SMC) algorithms are… (more)

Subjects/Keywords: model checking; formal methods; formal verification; hardware verification

Record DetailsSimilar RecordsGoogle PlusoneFacebookTwitterCiteULikeMendeleyreddit

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

APA (6th Edition):

Vediramana Krishnan, H. G. (2019). Strong Induction in Hardware Model Checking. (Thesis). University of Waterloo. Retrieved from http://hdl.handle.net/10012/14885

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

Vediramana Krishnan, Hari Govind. “Strong Induction in Hardware Model Checking.” 2019. Thesis, University of Waterloo. Accessed January 27, 2020. http://hdl.handle.net/10012/14885.

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

MLA Handbook (7th Edition):

Vediramana Krishnan, Hari Govind. “Strong Induction in Hardware Model Checking.” 2019. Web. 27 Jan 2020.

Vancouver:

Vediramana Krishnan HG. Strong Induction in Hardware Model Checking. [Internet] [Thesis]. University of Waterloo; 2019. [cited 2020 Jan 27]. Available from: http://hdl.handle.net/10012/14885.

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

Council of Science Editors:

Vediramana Krishnan HG. Strong Induction in Hardware Model Checking. [Thesis]. University of Waterloo; 2019. Available from: http://hdl.handle.net/10012/14885

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


Texas A&M University

5. 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 27, 2020. http://hdl.handle.net/1969.1/165866.

MLA Handbook (7th Edition):

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

Vancouver:

Kottapalli V. Formal Verification of a MESI-based Cache Implementation. [Internet] [Masters thesis]. Texas A&M University; 2017. [cited 2020 Jan 27]. 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 Oxford

6. Kattenbelt, Mark Alex. Automated quantitative software verification.

Degree: PhD, 2010, University of Oxford

 Many software systems exhibit probabilistic behaviour, either added explicitly, to improve performance or to break symmetry, or implicitly, through interaction with unreliable networks or faulty… (more)

Subjects/Keywords: 005.3; Theory and automated verification; model checking; quantitative; verification; software; formal methods; formal verification; software verification

Record DetailsSimilar RecordsGoogle PlusoneFacebookTwitterCiteULikeMendeleyreddit

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

APA (6th Edition):

Kattenbelt, M. A. (2010). Automated quantitative software verification. (Doctoral Dissertation). University of Oxford. Retrieved from http://ora.ox.ac.uk/objects/uuid:62430df4-7fdf-4c4f-b3cd-97ba8912c9f5 ; https://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.540281

Chicago Manual of Style (16th Edition):

Kattenbelt, Mark Alex. “Automated quantitative software verification.” 2010. Doctoral Dissertation, University of Oxford. Accessed January 27, 2020. http://ora.ox.ac.uk/objects/uuid:62430df4-7fdf-4c4f-b3cd-97ba8912c9f5 ; https://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.540281.

MLA Handbook (7th Edition):

Kattenbelt, Mark Alex. “Automated quantitative software verification.” 2010. Web. 27 Jan 2020.

Vancouver:

Kattenbelt MA. Automated quantitative software verification. [Internet] [Doctoral dissertation]. University of Oxford; 2010. [cited 2020 Jan 27]. Available from: http://ora.ox.ac.uk/objects/uuid:62430df4-7fdf-4c4f-b3cd-97ba8912c9f5 ; https://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.540281.

Council of Science Editors:

Kattenbelt MA. Automated quantitative software verification. [Doctoral Dissertation]. University of Oxford; 2010. Available from: http://ora.ox.ac.uk/objects/uuid:62430df4-7fdf-4c4f-b3cd-97ba8912c9f5 ; https://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.540281


University of Utah

7. 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 27, 2020. 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. 27 Jan 2020.

Vancouver:

Xu Y. Algorithms for automatic generation of relative timing constraints. [Internet] [Doctoral dissertation]. University of Utah; 2011. [cited 2020 Jan 27]. 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

8. 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 27, 2020. 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. 27 Jan 2020.

Vancouver:

Sogokon A. Direct methods for deductive verification of temporal properties in continuous dynamical systems. [Internet] [Doctoral dissertation]. University of Edinburgh; 2016. [cited 2020 Jan 27]. 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


University of Illinois – Urbana-Champaign

9. 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 27, 2020. http://hdl.handle.net/2142/29614.

MLA Handbook (7th Edition):

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

Vancouver:

Katelman M. A meta-language for functional verification. [Internet] [Doctoral dissertation]. University of Illinois – Urbana-Champaign; 2012. [cited 2020 Jan 27]. 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


The Ohio State University

10. 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 27, 2020. 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. 27 Jan 2020.

Vancouver:

Zaccai DS. A Balanced Verification Effort for the Java Language. [Internet] [Doctoral dissertation]. The Ohio State University; 2016. [cited 2020 Jan 27]. 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 Manchester

11. 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 27, 2020. 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. 27 Jan 2020.

Vancouver:

Carter R. Verification of liveness properties on hybrid dynamical systems. [Internet] [Doctoral dissertation]. University of Manchester; 2013. [cited 2020 Jan 27]. 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 Sydney

12. 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 27, 2020. 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. 27 Jan 2020.

Vancouver:

Subotic P. Applying Elimination-Based Algorithms to Abstract Interpretation . [Internet] [Thesis]. University of Sydney; 2014. [cited 2020 Jan 27]. 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


Clemson University

13. 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 27, 2020. https://tigerprints.clemson.edu/all_dissertations/1132.

MLA Handbook (7th Edition):

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

Vancouver:

Smith H. Engineering Specifications and Mathematics for Verified Software. [Internet] [Doctoral dissertation]. Clemson University; 2013. [cited 2020 Jan 27]. 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


University of Colorado

14. 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 27, 2020. https://scholar.colorado.edu/ecen_gradetds/86.

MLA Handbook (7th Edition):

Hassan, Zyad. “Incremental, Inductive Model Checking.” 2014. Web. 27 Jan 2020.

Vancouver:

Hassan Z. Incremental, Inductive Model Checking. [Internet] [Doctoral dissertation]. University of Colorado; 2014. [cited 2020 Jan 27]. 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 Ottawa

15. 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 27, 2020. 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. 27 Jan 2020.

Vancouver:

Sistany B. A Certified Core Policy Language . [Internet] [Thesis]. University of Ottawa; 2016. [cited 2020 Jan 27]. 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 Oklahoma

16. 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 27, 2020. http://hdl.handle.net/11244/42982.

MLA Handbook (7th Edition):

Ralston, Ryan. “Translating Clojure to ACL2 for Verification.” 2016. Web. 27 Jan 2020.

Vancouver:

Ralston R. Translating Clojure to ACL2 for Verification. [Internet] [Doctoral dissertation]. University of Oklahoma; 2016. [cited 2020 Jan 27]. 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


University of Illinois – Urbana-Champaign

17. 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 27, 2020. 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. 27 Jan 2020.

Vancouver:

Kheradmand A. A formal semantics of P4 and applications. [Internet] [Thesis]. University of Illinois – Urbana-Champaign; 2018. [cited 2020 Jan 27]. 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


Kansas State University

18. 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 27, 2020. http://hdl.handle.net/2097/32880.

MLA Handbook (7th Edition):

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

Vancouver:

Zhang Z. A formal approach to contract verification for high-integrity applications. [Internet] [Doctoral dissertation]. Kansas State University; 2016. [cited 2020 Jan 27]. 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 New South Wales

19. 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 27, 2020. 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. 27 Jan 2020.

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 2020 Jan 27]. 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


Boise State University

20. 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 27, 2020. 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. 27 Jan 2020.

Vancouver:

Joshaghani R. UNICORN Framework: A User-Centric Approach Toward Formal Verification of Privacy Norms. [Internet] [Thesis]. Boise State University; 2019. [cited 2020 Jan 27]. 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


University of New South Wales

21. Elkaduwe, Karunadipathi Wasala H. M. R. D. D. B. A Principled approach to kernel memory management.

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

 Small kernels are a promising approach to secure and reliable system construction. These systems reduce the size of the kernel to a point where it… (more)

Subjects/Keywords: Kernel memory management; Microkernels; Security; Formal verification

Record DetailsSimilar RecordsGoogle PlusoneFacebookTwitterCiteULikeMendeleyreddit

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

APA (6th Edition):

Elkaduwe, K. W. H. M. R. D. D. B. (2010). A Principled approach to kernel memory management. (Doctoral Dissertation). University of New South Wales. Retrieved from http://handle.unsw.edu.au/1959.4/45068 ; https://unsworks.unsw.edu.au/fapi/datastream/unsworks:8363/SOURCE02?view=true

Chicago Manual of Style (16th Edition):

Elkaduwe, Karunadipathi Wasala H M R D D B. “A Principled approach to kernel memory management.” 2010. Doctoral Dissertation, University of New South Wales. Accessed January 27, 2020. http://handle.unsw.edu.au/1959.4/45068 ; https://unsworks.unsw.edu.au/fapi/datastream/unsworks:8363/SOURCE02?view=true.

MLA Handbook (7th Edition):

Elkaduwe, Karunadipathi Wasala H M R D D B. “A Principled approach to kernel memory management.” 2010. Web. 27 Jan 2020.

Vancouver:

Elkaduwe KWHMRDDB. A Principled approach to kernel memory management. [Internet] [Doctoral dissertation]. University of New South Wales; 2010. [cited 2020 Jan 27]. Available from: http://handle.unsw.edu.au/1959.4/45068 ; https://unsworks.unsw.edu.au/fapi/datastream/unsworks:8363/SOURCE02?view=true.

Council of Science Editors:

Elkaduwe KWHMRDDB. A Principled approach to kernel memory management. [Doctoral Dissertation]. University of New South Wales; 2010. Available from: http://handle.unsw.edu.au/1959.4/45068 ; https://unsworks.unsw.edu.au/fapi/datastream/unsworks:8363/SOURCE02?view=true


University of New South Wales

22. 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 27, 2020. 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. 27 Jan 2020.

Vancouver:

Kolanski RM. Verification of programs in virtual memory using separation logic. [Internet] [Doctoral dissertation]. University of New South Wales; 2011. [cited 2020 Jan 27]. 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


University of Texas – Austin

23. -4047-4940. Extending capability of formal tools : applying semiformal verification on large design.

Degree: MSin Engineering, Electrical and Computer Engineering, 2019, University of Texas – Austin

 Simulation and formal verification are the two most commonly used techniques for verifying a digital design described at the Register-Transfer Level (RTL). Compared to simulation,… (more)

Subjects/Keywords: Formal engine; Semiformal verification; Waypoint; Neural network

Record DetailsSimilar RecordsGoogle PlusoneFacebookTwitterCiteULikeMendeleyreddit

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

APA (6th Edition):

-4047-4940. (2019). Extending capability of formal tools : applying semiformal verification on large design. (Masters Thesis). University of Texas – Austin. Retrieved from http://dx.doi.org/10.26153/tsw/5533

Note: this citation may be lacking information needed for this citation format:
Author name may be incomplete

Chicago Manual of Style (16th Edition):

-4047-4940. “Extending capability of formal tools : applying semiformal verification on large design.” 2019. Masters Thesis, University of Texas – Austin. Accessed January 27, 2020. http://dx.doi.org/10.26153/tsw/5533.

Note: this citation may be lacking information needed for this citation format:
Author name may be incomplete

MLA Handbook (7th Edition):

-4047-4940. “Extending capability of formal tools : applying semiformal verification on large design.” 2019. Web. 27 Jan 2020.

Note: this citation may be lacking information needed for this citation format:
Author name may be incomplete

Vancouver:

-4047-4940. Extending capability of formal tools : applying semiformal verification on large design. [Internet] [Masters thesis]. University of Texas – Austin; 2019. [cited 2020 Jan 27]. Available from: http://dx.doi.org/10.26153/tsw/5533.

Note: this citation may be lacking information needed for this citation format:
Author name may be incomplete

Council of Science Editors:

-4047-4940. Extending capability of formal tools : applying semiformal verification on large design. [Masters Thesis]. University of Texas – Austin; 2019. Available from: http://dx.doi.org/10.26153/tsw/5533

Note: this citation may be lacking information needed for this citation format:
Author name may be incomplete


University of Newcastle

24. 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 27, 2020. 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. 27 Jan 2020.

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 2020 Jan 27]. 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

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

Degree: MS, Electrical and 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 27, 2020. 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. 27 Jan 2020.

Vancouver:

Bockenek JA. USIMPL: An Extension of Isabelle/UTP with Simpl-like Control Flow. [Internet] [Masters thesis]. Virginia Tech; 2017. [cited 2020 Jan 27]. 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


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 27, 2020. 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. 27 Jan 2020.

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 2020 Jan 27]. 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


University of Utah

27. 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 27, 2020. 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. 27 Jan 2020.

Vancouver:

Pruss T. Word-level abstraction from combinational circuits using algebraic geometry. [Internet] [Doctoral dissertation]. University of Utah; 2015. [cited 2020 Jan 27]. 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


Université de Grenoble

28. 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 27, 2020. 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. 27 Jan 2020.

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 2020 Jan 27]. 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

29. Moore, Brandon Michael. Coinductive program verification.

Degree: PhD, Computer Science, 2016, University of Illinois – Urbana-Champaign

 We present a program-verification approach based on coinduction, which makes it feasible to verify programs given an operational semantics of a programming language, without constructing… (more)

Subjects/Keywords: Program Verification; Coinduction; Operational Semantics; Formal Methods; Software Verification

Record DetailsSimilar RecordsGoogle PlusoneFacebookTwitterCiteULikeMendeleyreddit

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

APA (6th Edition):

Moore, B. M. (2016). Coinductive program verification. (Doctoral Dissertation). University of Illinois – Urbana-Champaign. Retrieved from http://hdl.handle.net/2142/95372

Chicago Manual of Style (16th Edition):

Moore, Brandon Michael. “Coinductive program verification.” 2016. Doctoral Dissertation, University of Illinois – Urbana-Champaign. Accessed January 27, 2020. http://hdl.handle.net/2142/95372.

MLA Handbook (7th Edition):

Moore, Brandon Michael. “Coinductive program verification.” 2016. Web. 27 Jan 2020.

Vancouver:

Moore BM. Coinductive program verification. [Internet] [Doctoral dissertation]. University of Illinois – Urbana-Champaign; 2016. [cited 2020 Jan 27]. Available from: http://hdl.handle.net/2142/95372.

Council of Science Editors:

Moore BM. Coinductive program verification. [Doctoral Dissertation]. University of Illinois – Urbana-Champaign; 2016. Available from: http://hdl.handle.net/2142/95372

30. 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 27, 2020. 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. 27 Jan 2020.

Vancouver:

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

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

.