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 394 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 December 15, 2019. 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. 15 Dec 2019.

Vancouver:

Shehata H. Formal Verification of Instruction Dependencies in Microprocessors. [Internet] [Thesis]. University of Waterloo; 2011. [cited 2019 Dec 15]. 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


University of New South Wales

2. 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 December 15, 2019. 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. 15 Dec 2019.

Vancouver:

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

3. 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 December 15, 2019. 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. 15 Dec 2019.

Vancouver:

Vediramana Krishnan HG. Strong Induction in Hardware Model Checking. [Internet] [Thesis]. University of Waterloo; 2019. [cited 2019 Dec 15]. 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

4. 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 December 15, 2019. http://hdl.handle.net/1969.1/165866.

MLA Handbook (7th Edition):

Kottapalli, Venkateshwar. “Formal Verification of a MESI-based Cache Implementation.” 2017. Web. 15 Dec 2019.

Vancouver:

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

5. 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 December 15, 2019. 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. 15 Dec 2019.

Vancouver:

Kattenbelt MA. Automated quantitative software verification. [Internet] [Doctoral dissertation]. University of Oxford; 2010. [cited 2019 Dec 15]. 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

6. 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 December 15, 2019. 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. 15 Dec 2019.

Vancouver:

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


The Ohio State University

7. 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 December 15, 2019. 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. 15 Dec 2019.

Vancouver:

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

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 December 15, 2019. 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. 15 Dec 2019.

Vancouver:

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

9. 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 December 15, 2019. 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. 15 Dec 2019.

Vancouver:

Carter R. Verification of liveness properties on hybrid dynamical systems. [Internet] [Doctoral dissertation]. University of Manchester; 2013. [cited 2019 Dec 15]. 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 Colorado

10. 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 December 15, 2019. https://scholar.colorado.edu/ecen_gradetds/86.

MLA Handbook (7th Edition):

Hassan, Zyad. “Incremental, Inductive Model Checking.” 2014. Web. 15 Dec 2019.

Vancouver:

Hassan Z. Incremental, Inductive Model Checking. [Internet] [Doctoral dissertation]. University of Colorado; 2014. [cited 2019 Dec 15]. 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 Sydney

11. 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 December 15, 2019. 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. 15 Dec 2019.

Vancouver:

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

12. 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 December 15, 2019. https://tigerprints.clemson.edu/all_dissertations/1132.

MLA Handbook (7th Edition):

Smith, Hampton. “Engineering Specifications and Mathematics for Verified Software.” 2013. Web. 15 Dec 2019.

Vancouver:

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

13. 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 December 15, 2019. 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. 15 Dec 2019.

Vancouver:

Sistany B. A Certified Core Policy Language . [Internet] [Thesis]. University of Ottawa; 2016. [cited 2019 Dec 15]. 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

14. 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 December 15, 2019. http://hdl.handle.net/11244/42982.

MLA Handbook (7th Edition):

Ralston, Ryan. “Translating Clojure to ACL2 for Verification.” 2016. Web. 15 Dec 2019.

Vancouver:

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

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 December 15, 2019. 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. 15 Dec 2019.

Vancouver:

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

16. 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 December 15, 2019. http://hdl.handle.net/2097/32880.

MLA Handbook (7th Edition):

Zhang, Zhi. “A formal approach to contract verification for high-integrity applications.” 2016. Web. 15 Dec 2019.

Vancouver:

Zhang Z. A formal approach to contract verification for high-integrity applications. [Internet] [Doctoral dissertation]. Kansas State University; 2016. [cited 2019 Dec 15]. 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

17. 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 December 15, 2019. 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. 15 Dec 2019.

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 2019 Dec 15]. 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

18. 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 December 15, 2019. 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. 15 Dec 2019.

Vancouver:

Joshaghani R. UNICORN Framework: A User-Centric Approach Toward Formal Verification of Privacy Norms. [Internet] [Thesis]. Boise State University; 2019. [cited 2019 Dec 15]. 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 Illinois – Urbana-Champaign

19. 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 December 15, 2019. http://hdl.handle.net/2142/29614.

MLA Handbook (7th Edition):

Katelman, Michael. “A meta-language for functional verification.” 2012. Web. 15 Dec 2019.

Vancouver:

Katelman M. A meta-language for functional verification. [Internet] [Doctoral dissertation]. University of Illinois – Urbana-Champaign; 2012. [cited 2019 Dec 15]. 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 New South Wales

20. 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 December 15, 2019. 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. 15 Dec 2019.

Vancouver:

Elkaduwe KWHMRDDB. A Principled approach to kernel memory management. [Internet] [Doctoral dissertation]. University of New South Wales; 2010. [cited 2019 Dec 15]. 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

21. 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 December 15, 2019. 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. 15 Dec 2019.

Vancouver:

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

22. -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 December 15, 2019. 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. 15 Dec 2019.

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 2019 Dec 15]. 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

23. 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 December 15, 2019. 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. 15 Dec 2019.

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 2019 Dec 15]. 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

24. 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 December 15, 2019. 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. 15 Dec 2019.

Vancouver:

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

25. 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 December 15, 2019. 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. 15 Dec 2019.

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 2019 Dec 15]. 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

26. 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 December 15, 2019. 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. 15 Dec 2019.

Vancouver:

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

27. 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 December 15, 2019. 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. 15 Dec 2019.

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 2019 Dec 15]. 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

28. 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 December 15, 2019. 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. 15 Dec 2019.

Vancouver:

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

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 December 15, 2019. http://hdl.handle.net/2142/95372.

MLA Handbook (7th Edition):

Moore, Brandon Michael. “Coinductive program verification.” 2016. Web. 15 Dec 2019.

Vancouver:

Moore BM. Coinductive program verification. [Internet] [Doctoral dissertation]. University of Illinois – Urbana-Champaign; 2016. [cited 2019 Dec 15]. 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


Duke University

30. Matthews, Opeoluwa. A Formal Framework for Designing Verifiable Protocols .

Degree: 2017, Duke University

  Protocols play critical roles in computer systems today, including managing resources, facilitating communication, and coordinating actions of components. It is highly desirable to formally… (more)

Subjects/Keywords: Computer engineering; Cache Coherence; Formal Verification; Model Checking; Parameterized verification; Protocols; Verification-aware architecture

Record DetailsSimilar RecordsGoogle PlusoneFacebookTwitterCiteULikeMendeleyreddit

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

APA (6th Edition):

Matthews, O. (2017). A Formal Framework for Designing Verifiable Protocols . (Thesis). Duke University. Retrieved from http://hdl.handle.net/10161/16236

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

Matthews, Opeoluwa. “A Formal Framework for Designing Verifiable Protocols .” 2017. Thesis, Duke University. Accessed December 15, 2019. http://hdl.handle.net/10161/16236.

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

MLA Handbook (7th Edition):

Matthews, Opeoluwa. “A Formal Framework for Designing Verifiable Protocols .” 2017. Web. 15 Dec 2019.

Vancouver:

Matthews O. A Formal Framework for Designing Verifiable Protocols . [Internet] [Thesis]. Duke University; 2017. [cited 2019 Dec 15]. Available from: http://hdl.handle.net/10161/16236.

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

Council of Science Editors:

Matthews O. A Formal Framework for Designing Verifiable Protocols . [Thesis]. Duke University; 2017. Available from: http://hdl.handle.net/10161/16236

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]

.