subject:(theorem proving)

1. Scott, Phil. Ordered geometry in Hilbert's Grundlagen der Geometrie.

Degree: PhD, 2015, University of Edinburgh

► The Grundlagen der Geometrie brought Euclid’s ancient axioms up to the standards of modern logic, anticipating a completely mechanical verification of their theorems. There are… (more)

Subjects/Keywords: 516.2; geometry; theorem proving; proofs

1 more image…

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Scott, P. (2015). Ordered geometry in Hilbert's Grundlagen der Geometrie. (Doctoral Dissertation). University of Edinburgh. Retrieved from http://hdl.handle.net/1842/15948

Chicago Manual of Style (16^th Edition):

Scott, Phil. “Ordered geometry in Hilbert's Grundlagen der Geometrie.” 2015. Doctoral Dissertation, University of Edinburgh. Accessed March 05, 2021. http://hdl.handle.net/1842/15948.

MLA Handbook (7^th Edition):

Scott, Phil. “Ordered geometry in Hilbert's Grundlagen der Geometrie.” 2015. Web. 05 Mar 2021.

Vancouver:

Scott P. Ordered geometry in Hilbert's Grundlagen der Geometrie. [Internet] [Doctoral dissertation]. University of Edinburgh; 2015. [cited 2021 Mar 05]. Available from: http://hdl.handle.net/1842/15948.

Council of Science Editors:

Scott P. Ordered geometry in Hilbert's Grundlagen der Geometrie. [Doctoral Dissertation]. University of Edinburgh; 2015. Available from: http://hdl.handle.net/1842/15948

University of Kansas

2. Austin, Evan Christopher. HaskHOL: A Haskell Hosted Domain Specific Language for Higher-Order Logic Theorem Proving.

Degree: MS, Electrical Engineering & Computer Science, 2011, University of Kansas

URL: http://hdl.handle.net/1808/8037

► HaskHOL is an implementation of a HOL theorem proving capability in Haskell. Motivated by a need to integrate theorem proving capabilities into a Haskell-based tool… (more)

Subjects/Keywords: Computer science; Haskell; Hol; Theorem proving

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Austin, E. C. (2011). HaskHOL: A Haskell Hosted Domain Specific Language for Higher-Order Logic Theorem Proving. (Masters Thesis). University of Kansas. Retrieved from http://hdl.handle.net/1808/8037

Chicago Manual of Style (16^th Edition):

Austin, Evan Christopher. “HaskHOL: A Haskell Hosted Domain Specific Language for Higher-Order Logic Theorem Proving.” 2011. Masters Thesis, University of Kansas. Accessed March 05, 2021. http://hdl.handle.net/1808/8037.

MLA Handbook (7^th Edition):

Austin, Evan Christopher. “HaskHOL: A Haskell Hosted Domain Specific Language for Higher-Order Logic Theorem Proving.” 2011. Web. 05 Mar 2021.

Vancouver:

Austin EC. HaskHOL: A Haskell Hosted Domain Specific Language for Higher-Order Logic Theorem Proving. [Internet] [Masters thesis]. University of Kansas; 2011. [cited 2021 Mar 05]. Available from: http://hdl.handle.net/1808/8037.

Council of Science Editors:

Austin EC. HaskHOL: A Haskell Hosted Domain Specific Language for Higher-Order Logic Theorem Proving. [Masters Thesis]. University of Kansas; 2011. Available from: http://hdl.handle.net/1808/8037

University of Manchester

3. Hoder, Krystof. Practical aspects of automated first-order reasoning.

Degree: PhD, 2012, University of Manchester

URL: https://www.research.manchester.ac.uk/portal/en/theses/practical-aspects-of-automated-firstorder-reasoning(1331ec1f-802c-4aeb-9265-1248d8db2a8e).html ; http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.558052

► Our work focuses on bringing the first-order reasoning closer to practicalapplications, particularly in software and hardware verification. The aim is to develop techniques that make… (more)

Subjects/Keywords: 006.3; First-Order Reasoning; Automated Theorem Proving

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Hoder, K. (2012). Practical aspects of automated first-order reasoning. (Doctoral Dissertation). University of Manchester. Retrieved from https://www.research.manchester.ac.uk/portal/en/theses/practical-aspects-of-automated-firstorder-reasoning(1331ec1f-802c-4aeb-9265-1248d8db2a8e).html ; http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.558052

Chicago Manual of Style (16^th Edition):

Hoder, Krystof. “Practical aspects of automated first-order reasoning.” 2012. Doctoral Dissertation, University of Manchester. Accessed March 05, 2021. https://www.research.manchester.ac.uk/portal/en/theses/practical-aspects-of-automated-firstorder-reasoning(1331ec1f-802c-4aeb-9265-1248d8db2a8e).html ; http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.558052.

MLA Handbook (7^th Edition):

Hoder, Krystof. “Practical aspects of automated first-order reasoning.” 2012. Web. 05 Mar 2021.

Vancouver:

Hoder K. Practical aspects of automated first-order reasoning. [Internet] [Doctoral dissertation]. University of Manchester; 2012. [cited 2021 Mar 05]. Available from: https://www.research.manchester.ac.uk/portal/en/theses/practical-aspects-of-automated-firstorder-reasoning(1331ec1f-802c-4aeb-9265-1248d8db2a8e).html ; http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.558052.

Council of Science Editors:

Hoder K. Practical aspects of automated first-order reasoning. [Doctoral Dissertation]. University of Manchester; 2012. Available from: https://www.research.manchester.ac.uk/portal/en/theses/practical-aspects-of-automated-firstorder-reasoning(1331ec1f-802c-4aeb-9265-1248d8db2a8e).html ; http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.558052

4. Meikle, Laura Isabel. Intuition in formal proof : a novel framework for combining mathematical tools.

Degree: PhD, 2014, University of Edinburgh

URL: http://hdl.handle.net/1842/9663

► This doctoral thesis addresses one major difficulty in formal proof: removing obstructions to intuition which hamper the proof endeavour. We investigate this in the context… (more)

Subjects/Keywords: 006.3; theorem proving; automated reasoning; computational geometry

10 more images…

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Meikle, L. I. (2014). Intuition in formal proof : a novel framework for combining mathematical tools. (Doctoral Dissertation). University of Edinburgh. Retrieved from http://hdl.handle.net/1842/9663

Chicago Manual of Style (16^th Edition):

Meikle, Laura Isabel. “Intuition in formal proof : a novel framework for combining mathematical tools.” 2014. Doctoral Dissertation, University of Edinburgh. Accessed March 05, 2021. http://hdl.handle.net/1842/9663.

MLA Handbook (7^th Edition):

Meikle, Laura Isabel. “Intuition in formal proof : a novel framework for combining mathematical tools.” 2014. Web. 05 Mar 2021.

Vancouver:

Meikle LI. Intuition in formal proof : a novel framework for combining mathematical tools. [Internet] [Doctoral dissertation]. University of Edinburgh; 2014. [cited 2021 Mar 05]. Available from: http://hdl.handle.net/1842/9663.

Council of Science Editors:

Meikle LI. Intuition in formal proof : a novel framework for combining mathematical tools. [Doctoral Dissertation]. University of Edinburgh; 2014. Available from: http://hdl.handle.net/1842/9663

Loughborough University

5. Okoli, Ifeyinwa. A novel term rewriting strategy for certain hierarchical AC-algebraic systems.

Degree: PhD, 1989, Loughborough University

URL: http://hdl.handle.net/2134/10641

Subjects/Keywords: 510; Theorem proving

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Okoli, I. (1989). A novel term rewriting strategy for certain hierarchical AC-algebraic systems. (Doctoral Dissertation). Loughborough University. Retrieved from http://hdl.handle.net/2134/10641

Chicago Manual of Style (16^th Edition):

Okoli, Ifeyinwa. “A novel term rewriting strategy for certain hierarchical AC-algebraic systems.” 1989. Doctoral Dissertation, Loughborough University. Accessed March 05, 2021. http://hdl.handle.net/2134/10641.

MLA Handbook (7^th Edition):

Okoli, Ifeyinwa. “A novel term rewriting strategy for certain hierarchical AC-algebraic systems.” 1989. Web. 05 Mar 2021.

Vancouver:

Okoli I. A novel term rewriting strategy for certain hierarchical AC-algebraic systems. [Internet] [Doctoral dissertation]. Loughborough University; 1989. [cited 2021 Mar 05]. Available from: http://hdl.handle.net/2134/10641.

Council of Science Editors:

Okoli I. A novel term rewriting strategy for certain hierarchical AC-algebraic systems. [Doctoral Dissertation]. Loughborough University; 1989. Available from: http://hdl.handle.net/2134/10641

University of British Columbia

6. LeQuesne, Peter Neave. A unit resolution theorem proving system.

Degree: MS- MSc, Computer Science, 1972, University of British Columbia

URL: http://hdl.handle.net/2429/33349

A unit resolution theorem proving system is developed and compared with the previous work of C.L. Chang. This thesis includes a description of a particular approach to unit resolution and a description of the resulting program and its effectiveness.

Subjects/Keywords: Automatic theorem proving.

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

LeQuesne, P. N. (1972). A unit resolution theorem proving system. (Masters Thesis). University of British Columbia. Retrieved from http://hdl.handle.net/2429/33349

Chicago Manual of Style (16^th Edition):

LeQuesne, Peter Neave. “A unit resolution theorem proving system.” 1972. Masters Thesis, University of British Columbia. Accessed March 05, 2021. http://hdl.handle.net/2429/33349.

MLA Handbook (7^th Edition):

LeQuesne, Peter Neave. “A unit resolution theorem proving system.” 1972. Web. 05 Mar 2021.

Vancouver:

LeQuesne PN. A unit resolution theorem proving system. [Internet] [Masters thesis]. University of British Columbia; 1972. [cited 2021 Mar 05]. Available from: http://hdl.handle.net/2429/33349.

Council of Science Editors:

LeQuesne PN. A unit resolution theorem proving system. [Masters Thesis]. University of British Columbia; 1972. Available from: http://hdl.handle.net/2429/33349

University of British Columbia

7. Minicozzi, Eliana. On the completeness of linear strategies in automatic consequence finding.

Degree: MS- MSc, Computer Science, 1972, University of British Columbia

URL: http://hdl.handle.net/2429/33572

► The problem of the automatic generation of logical consequences of a set of axioms is examined. The merging subsumption linear strategy has been shown complete… (more)

Subjects/Keywords: Automatic theorem proving.

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Minicozzi, E. (1972). On the completeness of linear strategies in automatic consequence finding. (Masters Thesis). University of British Columbia. Retrieved from http://hdl.handle.net/2429/33572

Chicago Manual of Style (16^th Edition):

Minicozzi, Eliana. “On the completeness of linear strategies in automatic consequence finding.” 1972. Masters Thesis, University of British Columbia. Accessed March 05, 2021. http://hdl.handle.net/2429/33572.

MLA Handbook (7^th Edition):

Minicozzi, Eliana. “On the completeness of linear strategies in automatic consequence finding.” 1972. Web. 05 Mar 2021.

Vancouver:

Minicozzi E. On the completeness of linear strategies in automatic consequence finding. [Internet] [Masters thesis]. University of British Columbia; 1972. [cited 2021 Mar 05]. Available from: http://hdl.handle.net/2429/33572.

Council of Science Editors:

Minicozzi E. On the completeness of linear strategies in automatic consequence finding. [Masters Thesis]. University of British Columbia; 1972. Available from: http://hdl.handle.net/2429/33572

University of New South Wales

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

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

URL: http://handle.unsw.edu.au/1959.4/54260 ; https://unsworks.unsw.edu.au/fapi/datastream/unsworks:13743/SOURCE02?view=true

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

▼ 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 translation: the first is to generate an idealised representation of the program, convenient for reasoning about. The second, safer approach is to perform a precise, conservative translation, at the cost of burdening verification efforts with low-level implementation details. In this thesis, we present methods for bridging the gap between these two approaches. In particular, we describe algorithms for automatically abstracting low-level C code semantics into a higher level representation. These translations include simplifying program control flow, converting finite machine arithmetic into idealised integers, and translating the byte-level C memory model to a split heap model. The generated abstractions are easier to reason about than the input representations, which in turn increases the productivity of formal verification techniques. Critically, we guarantee soundness by automatically generating proofs that our abstractions are correct. Previous work carrying out such transformations has either done so using unverified translations, or required significant manual proof engineering effort. Our algorithms are implemented in a new tool named AutoCorres, built on the Isabelle/HOL interactive theorem prover. We demonstrate the effectiveness of our abstractions in a number of case studies, and show the scalability of AutoCorres by translating real-world programs consisting of tens of thousands of lines of code. While our work focuses on a subset of the C programming language, we believe most of our algorithms are also applicable to other imperative languages, such as Java or C#. Advisors/Committee Members: Klein, Gerwin, University of New South Wales and NICTA, Andronick, June, University of New South Wales and NICTA, Elphinstone, Kevin, University of New South Wales and NICTA.

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

Record Details Similar Records Cite « Share

❌

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

APA (6^th 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 (16^th Edition):

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

MLA Handbook (7^th Edition):

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

Vancouver:

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

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

Degree: PhD, 2016, University of Oklahoma

URL: http://hdl.handle.net/11244/42982

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

▼ 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 verification, can reduce the number of defects in software and lower corrective maintenance, but their industrial adoption has been underwhelming. A significant barrier to adoption is the overhead of converting imperative programming languages, which are common in industry, into the declarative programming languages that are used by formal methods tools. In comparison, the verification of software written in declarative programming languages is much easier because the conversion into a formal methods tool is easier. The growing popularity of declarative programming – evident from the rise of multi-paradigm languages such as Javascript, Ruby, and Scala – affords us the opportunity to verify the correctness of software more easily. Clojure is a declarative language released in 2007 that compiles to bytecode that executes on the Java Virtual Machine (JVM). Despite being a newer, declarative programming language, several companies have already used it to develop commercial products. Clojure shares a Lisp syntax with ACL2, an interactive theorem prover that is used to verify the correctness of software. Since both languages are based on Lisp, code written in either Clojure or ACL2 is easily converted to the other. Therefore, Clojure can conceivably be verified by ACL2 with limited overhead assuming that the underlying behavior of Clojure code matches that of ACL2. ACL2 has been previously used to reason about Java programs through the use of formal models of the JVM. Since Clojure compiles to JVM bytecode, a similar approach is taken in this dissertation to verify the underlying implementation of Clojure. The research presented in this dissertation advances techniques to verify Clojure code in ACL2. Clojure and ACL2 are declarative, but they are specifically functional programming languages so the research focuses on two important concepts in functional programming and verification: arbitrary-precision numbers ("bignums") and lists. For bignums, the correctness of a model of addition is verified that addresses issues that arise from the unique representation of bignums in Clojure. Lists, in Clojure, are implemented as a type of sequence. This dissertation demonstrates an abstraction that equates Clojure sequences to ACL2 lists. In support of the research, an existing ACL2 model of the JVM is modified to address specific aspects of compiled Clojure code and the new model is used to verify the correctness of core Clojure functions with respect to corresponding ACL2 functions. The results support the ideas that ACL2 can be used to reason about Clojure code and that formal methods can be integrated more easily in industrial software development when the implementation corresponds semantically to the verification model. Advisors/Committee Members: Page, Rex (advisor), Hougen, Dean (advisor), Miller, David (committee member), Jensen, Matthew (committee member), Weaver, Christopher (committee member).

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

Record Details Similar Records Cite « Share

❌

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

APA (6^th 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 (16^th Edition):

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

MLA Handbook (7^th Edition):

Ralston, Ryan. “Translating Clojure to ACL2 for Verification.” 2016. Web. 05 Mar 2021.

Vancouver:

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

Univerzitet u Beogradu

10. Stojanović, Sana. 1981-. Формализација и аутоматско доказивање теорема еуклидске геометрије.

Degree: Matematički fakultet, 2018, Univerzitet u Beogradu

URL: https://fedorabg.bg.ac.rs/fedora/get/o:15164/bdef:Content/get

►

Рачунарство - Вештачка интелигенција / Computer Science - Artificial intelligence

Напредак геометрије кроз векове се може разматрати кроз развој различитих аксиоматских система који је описују.… (more)

Subjects/Keywords: coherent logic; formalization of geometry; automated theorem proving; interactive theorem proving; automated generation of readable proofs

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Stojanović, S. 1. (2018). Формализација и аутоматско доказивање теорема еуклидске геометрије. (Thesis). Univerzitet u Beogradu. Retrieved from https://fedorabg.bg.ac.rs/fedora/get/o:15164/bdef:Content/get

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

Chicago Manual of Style (16^th Edition):

Stojanović, Sana 1981-. “Формализација и аутоматско доказивање теорема еуклидске геометрије.” 2018. Thesis, Univerzitet u Beogradu. Accessed March 05, 2021. https://fedorabg.bg.ac.rs/fedora/get/o:15164/bdef:Content/get.

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

MLA Handbook (7^th Edition):

Stojanović, Sana 1981-. “Формализација и аутоматско доказивање теорема еуклидске геометрије.” 2018. Web. 05 Mar 2021.

Vancouver:

Stojanović S1. Формализација и аутоматско доказивање теорема еуклидске геометрије. [Internet] [Thesis]. Univerzitet u Beogradu; 2018. [cited 2021 Mar 05]. Available from: https://fedorabg.bg.ac.rs/fedora/get/o:15164/bdef:Content/get.

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

Council of Science Editors:

Stojanović S1. Формализација и аутоматско доказивање теорема еуклидске геометрије. [Thesis]. Univerzitet u Beogradu; 2018. Available from: https://fedorabg.bg.ac.rs/fedora/get/o:15164/bdef:Content/get

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

Universiteit Utrecht

11. Bitane, Y. On Formalizing Decreasing Proof Orders.

Degree: 2015, Universiteit Utrecht

URL: http://dspace.library.uu.nl:8080/handle/1874/321339

► Confluence is an important property of term rewriting systems. Since any algorithm can be modelled as such, the decreasing diagrams technique is very useful for… (more)

Subjects/Keywords: term rewriting; coq; automated theorem proving; decreasing diagrams

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Bitane, Y. (2015). On Formalizing Decreasing Proof Orders. (Masters Thesis). Universiteit Utrecht. Retrieved from http://dspace.library.uu.nl:8080/handle/1874/321339

Chicago Manual of Style (16^th Edition):

Bitane, Y. “On Formalizing Decreasing Proof Orders.” 2015. Masters Thesis, Universiteit Utrecht. Accessed March 05, 2021. http://dspace.library.uu.nl:8080/handle/1874/321339.

MLA Handbook (7^th Edition):

Bitane, Y. “On Formalizing Decreasing Proof Orders.” 2015. Web. 05 Mar 2021.

Vancouver:

Bitane Y. On Formalizing Decreasing Proof Orders. [Internet] [Masters thesis]. Universiteit Utrecht; 2015. [cited 2021 Mar 05]. Available from: http://dspace.library.uu.nl:8080/handle/1874/321339.

Council of Science Editors:

Bitane Y. On Formalizing Decreasing Proof Orders. [Masters Thesis]. Universiteit Utrecht; 2015. Available from: http://dspace.library.uu.nl:8080/handle/1874/321339

University of Tasmania

12. Stokes, T E(Timothy Edward). On the algebraic and algorithmic properties of some generalised algebras.

Degree: 1990, University of Tasmania

URL: https://eprints.utas.edu.au/21929/1/whole_StokesTimothyEdward1991_thesis.pdf

Subjects/Keywords: Geometry; Algebraic; Automatic theorem proving

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Stokes, T. E. E. (1990). On the algebraic and algorithmic properties of some generalised algebras. (Thesis). University of Tasmania. Retrieved from https://eprints.utas.edu.au/21929/1/whole_StokesTimothyEdward1991_thesis.pdf

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

Chicago Manual of Style (16^th Edition):

Stokes, T E(Timothy Edward). “On the algebraic and algorithmic properties of some generalised algebras.” 1990. Thesis, University of Tasmania. Accessed March 05, 2021. https://eprints.utas.edu.au/21929/1/whole_StokesTimothyEdward1991_thesis.pdf.

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

MLA Handbook (7^th Edition):

Stokes, T E(Timothy Edward). “On the algebraic and algorithmic properties of some generalised algebras.” 1990. Web. 05 Mar 2021.

Vancouver:

Stokes TEE. On the algebraic and algorithmic properties of some generalised algebras. [Internet] [Thesis]. University of Tasmania; 1990. [cited 2021 Mar 05]. Available from: https://eprints.utas.edu.au/21929/1/whole_StokesTimothyEdward1991_thesis.pdf.

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

Council of Science Editors:

Stokes TEE. On the algebraic and algorithmic properties of some generalised algebras. [Thesis]. University of Tasmania; 1990. Available from: https://eprints.utas.edu.au/21929/1/whole_StokesTimothyEdward1991_thesis.pdf

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

Univerzitet u Beogradu

13. Nikolić, Mladen S. Usmeravanje pretrage u automatskom dokazivanju teorema.

Degree: Matematički fakultet, 2015, Univerzitet u Beogradu

URL: https://fedorabg.bg.ac.rs/fedora/get/o:8050/bdef:Content/get

►

Računarstvo-Automatsko dokazivanje teorema / computer science-Automated theorem proving

U ovom radu se razmatra problem usmeravanja pretrage u automatskom dokazivanju teorema. Rad se sastoji od dva… (more)

▼

Računarstvo-Automatsko dokazivanje teorema / computer science-Automated theorem proving

U ovom radu se razmatra problem usmeravanja pretrage u automatskom dokazivanju teorema. Rad se sastoji od dva dela čija je dodirna tačka CDCL sistem pretrage, koji se intenzivno koristi kod modernih SAT rešavača. U prvom delu rada razmatran je problem jednostavnog usmeravanja pretrage | izborom rešavača, njegovih heuristika i njihovih parametara, a u zavisnosti od svojstava instance koju je potrebno rešiti. Osnova predloženih metoda za izbor algoritama je sintaksna sličnost formula koja se odražava na njihovu grafovsku strukturu. Ova sličnost je prvi put pouzdano ustanovljena i analizirana pomoću originalne mere sličnosti grafova (koja se pokazala korisnom i u drugim domenima). Praktični pristupi merenju sličnosti formula se zbog računske efikasnosti ipak zasnivaju na numeričkim atributima iskaznih formula. Predložene su dve jednostavne metode izbora algoritma zasnovane na algoritmu k najbližih suseda. Prva tehnika, ArgoSmArT se zasniva na klasifikaciji instance u jednu od unapred zadatih familija za koje su poznati algoritmi koji ih efikasno rešavaju. Instanca se rešava algoritmom koji odgovara familiji u koju je instanca klasifikovana. Druga tehnika, ArgoSmArT k-NN se zasniva na nalaženju nekoliko sličnih instanci u trening skupu za koje je poznato vreme rešavanja pomoću svih algoritama kojima sistem raspolaže. Instanca se rešava algoritmom koji se najbolje ponaša na pronađenim instancama. Tehnika ArgoSmArT je pogodnija za izbor konfiguracije SAT rešavača, a ArgoSmArT k-NN za izbor samog SAT rešavača. Tehnika ArgoSmArT k-NN se pokazala značajno efikasnijom od najvažnijeg i pritom vrlo složenog sistema za izbor SAT rešavača i sistema SATzilla. Pored problema izbora KNF SAT rešavača i njihovih heuristika, razmatran je i problem izbora ne-KNF SAT rešavača u kojem fokus nije bio na tehnikama izbora rešavača, pošto se predložene tehnike direktno primenjuju i na taj problem, već na atributima kojima se ne-KNF instance mogu opisati, a koji do sad nisu predloženi. Rezultati u ovom domenu su pozitivni, ali za sada ograničeni. Osnovni razlog za to je nedostatak veceg broja ne-KNF resavaca raznovrsnog ponasanja, sto ne iznenaduje s obzirom da je ova vrsta resavaca tek u svom povoju. Pored konstrukcije ekasnog sistema za izbor SAT resavaca, prikazana je i metodologija poredenja SAT resavaca zasnovana na statistickom testiranju hipoteza. Potreba za ovakvom metodologijom proizilazi iz velike varijacije vremena resavanja jedne formule od strane jednog SAT resavaca, sto moze dovesti do razlicitih redosleda SAT resavaca prilikom poredenja njihovih performansi ili rangiranja, sto je i eksperimentalno demonstrirano. Predlozena metodologija pruza ocenu statisti cke znacajnosti testiranja i ocenu velicine efekta, poput verovatnoce da jedan SAT resavac bude brzi od drugog...

Advisors/Committee Members: Janičić, Predrag, 1968-.

Subjects/Keywords: automated theorem proving; search; SAT solvers; coherent logic; data mining

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Nikolić, M. S. (2015). Usmeravanje pretrage u automatskom dokazivanju teorema. (Thesis). Univerzitet u Beogradu. Retrieved from https://fedorabg.bg.ac.rs/fedora/get/o:8050/bdef:Content/get

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

Chicago Manual of Style (16^th Edition):

Nikolić, Mladen S. “Usmeravanje pretrage u automatskom dokazivanju teorema.” 2015. Thesis, Univerzitet u Beogradu. Accessed March 05, 2021. https://fedorabg.bg.ac.rs/fedora/get/o:8050/bdef:Content/get.

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

MLA Handbook (7^th Edition):

Nikolić, Mladen S. “Usmeravanje pretrage u automatskom dokazivanju teorema.” 2015. Web. 05 Mar 2021.

Vancouver:

Nikolić MS. Usmeravanje pretrage u automatskom dokazivanju teorema. [Internet] [Thesis]. Univerzitet u Beogradu; 2015. [cited 2021 Mar 05]. Available from: https://fedorabg.bg.ac.rs/fedora/get/o:8050/bdef:Content/get.

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

Council of Science Editors:

Nikolić MS. Usmeravanje pretrage u automatskom dokazivanju teorema. [Thesis]. Univerzitet u Beogradu; 2015. Available from: https://fedorabg.bg.ac.rs/fedora/get/o:8050/bdef:Content/get

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

University of Cambridge

14. Li, Wenda. Towards justifying computer algebra algorithms in Isabelle/HOL.

Degree: PhD, 2019, University of Cambridge

URL: https://www.repository.cam.ac.uk/handle/1810/289389

► As verification efforts using interactive theorem proving grow, we are in need of certified algorithms in computer algebra to tackle problems over the real numbers.… (more)

Subjects/Keywords: formal verification; theorem proving; Isabelle/HOL; computer algebra; cylindrical algebraic decomposition

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Li, W. (2019). Towards justifying computer algebra algorithms in Isabelle/HOL. (Doctoral Dissertation). University of Cambridge. Retrieved from https://www.repository.cam.ac.uk/handle/1810/289389

Chicago Manual of Style (16^th Edition):

Li, Wenda. “Towards justifying computer algebra algorithms in Isabelle/HOL.” 2019. Doctoral Dissertation, University of Cambridge. Accessed March 05, 2021. https://www.repository.cam.ac.uk/handle/1810/289389.

MLA Handbook (7^th Edition):

Li, Wenda. “Towards justifying computer algebra algorithms in Isabelle/HOL.” 2019. Web. 05 Mar 2021.

Vancouver:

Li W. Towards justifying computer algebra algorithms in Isabelle/HOL. [Internet] [Doctoral dissertation]. University of Cambridge; 2019. [cited 2021 Mar 05]. Available from: https://www.repository.cam.ac.uk/handle/1810/289389.

Council of Science Editors:

Li W. Towards justifying computer algebra algorithms in Isabelle/HOL. [Doctoral Dissertation]. University of Cambridge; 2019. Available from: https://www.repository.cam.ac.uk/handle/1810/289389

University of Oxford

15. Boehm, Peter. Incremental modelling for verified communication architectures.

Degree: PhD, 2011, University of Oxford

URL: http://ora.ox.ac.uk/objects/uuid:ec6c9e06-7395-4af4-b961-b2ed837fda89 ; https://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.559739

► Modern computer systems are advancing from multi-core to many-core designs and System-on-chips (SoC) are becoming increasingly complex while integrating a great variety of components, thus… (more)

Subjects/Keywords: 004.62; Theory and automated verification; communication protocols; verification; theorem proving

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Boehm, P. (2011). Incremental modelling for verified communication architectures. (Doctoral Dissertation). University of Oxford. Retrieved from http://ora.ox.ac.uk/objects/uuid:ec6c9e06-7395-4af4-b961-b2ed837fda89 ; https://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.559739

Chicago Manual of Style (16^th Edition):

Boehm, Peter. “Incremental modelling for verified communication architectures.” 2011. Doctoral Dissertation, University of Oxford. Accessed March 05, 2021. http://ora.ox.ac.uk/objects/uuid:ec6c9e06-7395-4af4-b961-b2ed837fda89 ; https://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.559739.

MLA Handbook (7^th Edition):

Boehm, Peter. “Incremental modelling for verified communication architectures.” 2011. Web. 05 Mar 2021.

Vancouver:

Boehm P. Incremental modelling for verified communication architectures. [Internet] [Doctoral dissertation]. University of Oxford; 2011. [cited 2021 Mar 05]. Available from: http://ora.ox.ac.uk/objects/uuid:ec6c9e06-7395-4af4-b961-b2ed837fda89 ; https://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.559739.

Council of Science Editors:

Boehm P. Incremental modelling for verified communication architectures. [Doctoral Dissertation]. University of Oxford; 2011. Available from: http://ora.ox.ac.uk/objects/uuid:ec6c9e06-7395-4af4-b961-b2ed837fda89 ; https://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.559739

University of Edinburgh

16. Duncan, Hazel. The use of data-mining for the automatic formation of tactics.

Degree: PhD, 2007, University of Edinburgh

URL: http://hdl.handle.net/1842/1768

► As functions which further the state of a proof in automated theorem proving, tactics are an important development in automated deduction. This thesis describes a… (more)

Subjects/Keywords: 005.3; Tactics; Theorem Proving

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Duncan, H. (2007). The use of data-mining for the automatic formation of tactics. (Doctoral Dissertation). University of Edinburgh. Retrieved from http://hdl.handle.net/1842/1768

Chicago Manual of Style (16^th Edition):

Duncan, Hazel. “The use of data-mining for the automatic formation of tactics.” 2007. Doctoral Dissertation, University of Edinburgh. Accessed March 05, 2021. http://hdl.handle.net/1842/1768.

MLA Handbook (7^th Edition):

Duncan, Hazel. “The use of data-mining for the automatic formation of tactics.” 2007. Web. 05 Mar 2021.

Vancouver:

Duncan H. The use of data-mining for the automatic formation of tactics. [Internet] [Doctoral dissertation]. University of Edinburgh; 2007. [cited 2021 Mar 05]. Available from: http://hdl.handle.net/1842/1768.

Council of Science Editors:

Duncan H. The use of data-mining for the automatic formation of tactics. [Doctoral Dissertation]. University of Edinburgh; 2007. Available from: http://hdl.handle.net/1842/1768

University of Edinburgh

17. Raggi, Daniel. Searching the space of representations : reasoning through transformations for mathematical problem solving.

Degree: PhD, 2016, University of Edinburgh

URL: http://hdl.handle.net/1842/22936

► The role of representation in reasoning has been long and widely regarded as crucial. It has remained one of the fundamental considerations in the design… (more)

Subjects/Keywords: 511; automated reasoning; representation; transformation; interactive theorem proving

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Raggi, D. (2016). Searching the space of representations : reasoning through transformations for mathematical problem solving. (Doctoral Dissertation). University of Edinburgh. Retrieved from http://hdl.handle.net/1842/22936

Chicago Manual of Style (16^th Edition):

Raggi, Daniel. “Searching the space of representations : reasoning through transformations for mathematical problem solving.” 2016. Doctoral Dissertation, University of Edinburgh. Accessed March 05, 2021. http://hdl.handle.net/1842/22936.

MLA Handbook (7^th Edition):

Raggi, Daniel. “Searching the space of representations : reasoning through transformations for mathematical problem solving.” 2016. Web. 05 Mar 2021.

Vancouver:

Raggi D. Searching the space of representations : reasoning through transformations for mathematical problem solving. [Internet] [Doctoral dissertation]. University of Edinburgh; 2016. [cited 2021 Mar 05]. Available from: http://hdl.handle.net/1842/22936.

Council of Science Editors:

Raggi D. Searching the space of representations : reasoning through transformations for mathematical problem solving. [Doctoral Dissertation]. University of Edinburgh; 2016. Available from: http://hdl.handle.net/1842/22936

Hong Kong University of Science and Technology

18. Wang, Jianwei CSE. Find closed form solutions to recurrences using theorem discovery.

Degree: 2019, Hong Kong University of Science and Technology

URL: http://repository.ust.hk/ir/Record/1783.1-100110 ; https://doi.org/10.14711/thesis-991012730263703412 ; http://repository.ust.hk/ir/bitstream/1783.1-100110/1/th_redirect.html

► Recent years, program verification has become a more and more key problem in computer science. Solving recurrences, as a vital part of program verification system,… (more)

Subjects/Keywords: Automatic theorem proving ; Computer programs ; Verification ; Machine learning ; Computer algorithms

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Wang, J. C. (2019). Find closed form solutions to recurrences using theorem discovery. (Thesis). Hong Kong University of Science and Technology. Retrieved from http://repository.ust.hk/ir/Record/1783.1-100110 ; https://doi.org/10.14711/thesis-991012730263703412 ; http://repository.ust.hk/ir/bitstream/1783.1-100110/1/th_redirect.html

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

Chicago Manual of Style (16^th Edition):

Wang, Jianwei CSE. “Find closed form solutions to recurrences using theorem discovery.” 2019. Thesis, Hong Kong University of Science and Technology. Accessed March 05, 2021. http://repository.ust.hk/ir/Record/1783.1-100110 ; https://doi.org/10.14711/thesis-991012730263703412 ; http://repository.ust.hk/ir/bitstream/1783.1-100110/1/th_redirect.html.

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

MLA Handbook (7^th Edition):

Wang, Jianwei CSE. “Find closed form solutions to recurrences using theorem discovery.” 2019. Web. 05 Mar 2021.

Vancouver:

Wang JC. Find closed form solutions to recurrences using theorem discovery. [Internet] [Thesis]. Hong Kong University of Science and Technology; 2019. [cited 2021 Mar 05]. Available from: http://repository.ust.hk/ir/Record/1783.1-100110 ; https://doi.org/10.14711/thesis-991012730263703412 ; http://repository.ust.hk/ir/bitstream/1783.1-100110/1/th_redirect.html.

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

Council of Science Editors:

Wang JC. Find closed form solutions to recurrences using theorem discovery. [Thesis]. Hong Kong University of Science and Technology; 2019. Available from: http://repository.ust.hk/ir/Record/1783.1-100110 ; https://doi.org/10.14711/thesis-991012730263703412 ; http://repository.ust.hk/ir/bitstream/1783.1-100110/1/th_redirect.html

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

Georgia Tech

19. Goble, Tiffany Danielle. Automate Reasoning: Computer Assisted Proofs in Set Theory Using Godel's Algorithm for Class Formation.

Degree: MS, Mathematics, 2004, Georgia Tech

URL: http://hdl.handle.net/1853/4767

► Automated reasoning, and in particular automated theorem proving, has become a very important research field within the world of mathematics. Besides being used to verify… (more)

Subjects/Keywords: Automated reasoning; Automated theorem proving

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Goble, T. D. (2004). Automate Reasoning: Computer Assisted Proofs in Set Theory Using Godel's Algorithm for Class Formation. (Masters Thesis). Georgia Tech. Retrieved from http://hdl.handle.net/1853/4767

Chicago Manual of Style (16^th Edition):

Goble, Tiffany Danielle. “Automate Reasoning: Computer Assisted Proofs in Set Theory Using Godel's Algorithm for Class Formation.” 2004. Masters Thesis, Georgia Tech. Accessed March 05, 2021. http://hdl.handle.net/1853/4767.

MLA Handbook (7^th Edition):

Goble, Tiffany Danielle. “Automate Reasoning: Computer Assisted Proofs in Set Theory Using Godel's Algorithm for Class Formation.” 2004. Web. 05 Mar 2021.

Vancouver:

Goble TD. Automate Reasoning: Computer Assisted Proofs in Set Theory Using Godel's Algorithm for Class Formation. [Internet] [Masters thesis]. Georgia Tech; 2004. [cited 2021 Mar 05]. Available from: http://hdl.handle.net/1853/4767.

Council of Science Editors:

Goble TD. Automate Reasoning: Computer Assisted Proofs in Set Theory Using Godel's Algorithm for Class Formation. [Masters Thesis]. Georgia Tech; 2004. Available from: http://hdl.handle.net/1853/4767

University of Illinois – Urbana-Champaign

20. Popescu, Andrei. Contributions to the theory of syntax with bindings and to process algebra.

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

URL: http://hdl.handle.net/2142/18477

► We develop a theory of syntax with bindings, focusing on: - methodological issues concerning the convenient representation of syntax; - techniques for recursive definitions and… (more)

▼ We develop a theory of syntax with bindings, focusing on: - methodological issues concerning the convenient representation of syntax; - techniques for recursive definitions and inductive reasoning. Our approach consists of a combination of FOAS (First-Order Abstract Syntax) and HOAS (Higher-Order Abstract Syntax) and tries to take advantage of the best of both worlds. The connection between FOAS and HOAS follows some general patterns and is presented as a (formally certified) statement of adequacy. We also develop a general technique for proving bisimilarity in process algebra. Our technique, presented as a formal proof system, is applicable to a wide range of process algebras. The proof system is incremental, in that it allows building incrementally an a priori unknown bisimulation, and pattern-based, in that it works on equalities of process patterns (i.e., universally quantified equations of process terms containing process variables), thus taking advantage of equational reasoning in a "circular" manner, inside coinductive proof loops. All the work presented here has been formalized in the Isabelle theorem prover. The formalization is performed in a general setting: arbitrary many-sorted syntax with bindings and arbitrary SOS-specified process algebra in de Simone format. The usefulness of our techniques is illustrated by several formalized case studies: - a development of call-by-name and call-by-value lambda-calculus with constants, including Church-Rosser theorems, connection with de Bruijn representation, connection with other Isabelle formalizations, HOAS representation, and contituation-passing-style (CPS) transformation; - a proof in HOAS of strong normalization for the polymorphic second-order lambda-calculus (a.k.a. System F). We also indicate the outline and some details of the formal development. Advisors/Committee Members: Gunter, Elsa L. (advisor), Gunter, Elsa L. (Committee Chair), Agha, Gul A. (committee member), Rosu, Grigore (committee member), Felty, Amy (committee member).

Subjects/Keywords: Syntax with Bindings; Lambda Calculus; Coinduction; Theorem proving; Isabelle

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Popescu, A. (2011). Contributions to the theory of syntax with bindings and to process algebra. (Doctoral Dissertation). University of Illinois – Urbana-Champaign. Retrieved from http://hdl.handle.net/2142/18477

Chicago Manual of Style (16^th Edition):

Popescu, Andrei. “Contributions to the theory of syntax with bindings and to process algebra.” 2011. Doctoral Dissertation, University of Illinois – Urbana-Champaign. Accessed March 05, 2021. http://hdl.handle.net/2142/18477.

MLA Handbook (7^th Edition):

Popescu, Andrei. “Contributions to the theory of syntax with bindings and to process algebra.” 2011. Web. 05 Mar 2021.

Vancouver:

Popescu A. Contributions to the theory of syntax with bindings and to process algebra. [Internet] [Doctoral dissertation]. University of Illinois – Urbana-Champaign; 2011. [cited 2021 Mar 05]. Available from: http://hdl.handle.net/2142/18477.

Council of Science Editors:

Popescu A. Contributions to the theory of syntax with bindings and to process algebra. [Doctoral Dissertation]. University of Illinois – Urbana-Champaign; 2011. Available from: http://hdl.handle.net/2142/18477

Georgia Tech

21. Jobredeaux, Romain J. Formal verification of control software.

Degree: PhD, Aerospace Engineering, 2015, Georgia Tech

URL: http://hdl.handle.net/1853/53841

► In a context of heightened requirements for safety-critical embedded systems and ever-increasing costs of verification and validation, this research proposes to advance the state of… (more)

▼ In a context of heightened requirements for safety-critical embedded systems and ever-increasing costs of verification and validation, this research proposes to advance the state of formal analysis for control software. Formal methods are a field of computer science that uses mathematical techniques and formalisms to rigorously analyze the behavior of programs. This research develops a framework and tools to express and prove high level properties of control law implementations. One goal is to bridge the gap between control theory and computer science. An annotation language is extended with symbols and axioms to describe control-related concepts at the code level. Libraries of theorems, along with their proofs, are developed to enable an interactive proof assistant to verify control-related properties. Through integration in a prototype tool, the process of verification is made automatic, and applied to several example systems.In a context of heightened requirements for safety-critical embedded systems and ever-increasing costs of verification and validation, this research proposes to advance the state of formal analysis for control software. Formal methods are a field of computer science that uses mathematical techniques and formalisms to rigorously analyze the behavior of programs. This research develops a framework and tools to express and prove high level properties of control law implementations. One goal is to bridge the gap between control theory and computer science. An annotation language is extended with symbols and axioms to describe control-related concepts at the code level. Libraries of theorems, along with their proofs, are developed to enable an interactive proof assistant to verify control-related properties. Through integration in a prototype tool, the process of verification is made automatic, and applied to several example systems. Advisors/Committee Members: Feron, Eric M. (advisor), Garoche, Pierre Loic (committee member), Goodloe, Alwyn (committee member), Holzinger, Marcus (committee member), Johnson, Eric (committee member).

Subjects/Keywords: Formal methods; LMI; Lyapunov; Static analysis; Control software; Theorem proving

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Jobredeaux, R. J. (2015). Formal verification of control software. (Doctoral Dissertation). Georgia Tech. Retrieved from http://hdl.handle.net/1853/53841

Chicago Manual of Style (16^th Edition):

Jobredeaux, Romain J. “Formal verification of control software.” 2015. Doctoral Dissertation, Georgia Tech. Accessed March 05, 2021. http://hdl.handle.net/1853/53841.

MLA Handbook (7^th Edition):

Jobredeaux, Romain J. “Formal verification of control software.” 2015. Web. 05 Mar 2021.

Vancouver:

Jobredeaux RJ. Formal verification of control software. [Internet] [Doctoral dissertation]. Georgia Tech; 2015. [cited 2021 Mar 05]. Available from: http://hdl.handle.net/1853/53841.

Council of Science Editors:

Jobredeaux RJ. Formal verification of control software. [Doctoral Dissertation]. Georgia Tech; 2015. Available from: http://hdl.handle.net/1853/53841

Louisiana State University

22. Lu, Zheng. Deductive formal verification of embedded systems.

Degree: PhD, Computer Sciences, 2012, Louisiana State University

URL: etd-11102012-171915 ; https://digitalcommons.lsu.edu/gradschool_dissertations/1525

► <div align = "justify"> We combine static analysis techniques with model-based deductive verification using SMT solvers to provide a framework that, given an analysis aspect… (more)

Subjects/Keywords: Coq; Static Code Analysis; Theorem Proving; Android; Formal Verification; SMT

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Lu, Z. (2012). Deductive formal verification of embedded systems. (Doctoral Dissertation). Louisiana State University. Retrieved from etd-11102012-171915 ; https://digitalcommons.lsu.edu/gradschool_dissertations/1525

Chicago Manual of Style (16^th Edition):

Lu, Zheng. “Deductive formal verification of embedded systems.” 2012. Doctoral Dissertation, Louisiana State University. Accessed March 05, 2021. etd-11102012-171915 ; https://digitalcommons.lsu.edu/gradschool_dissertations/1525.

MLA Handbook (7^th Edition):

Lu, Zheng. “Deductive formal verification of embedded systems.” 2012. Web. 05 Mar 2021.

Vancouver:

Lu Z. Deductive formal verification of embedded systems. [Internet] [Doctoral dissertation]. Louisiana State University; 2012. [cited 2021 Mar 05]. Available from: etd-11102012-171915 ; https://digitalcommons.lsu.edu/gradschool_dissertations/1525.

Council of Science Editors:

Lu Z. Deductive formal verification of embedded systems. [Doctoral Dissertation]. Louisiana State University; 2012. Available from: etd-11102012-171915 ; https://digitalcommons.lsu.edu/gradschool_dissertations/1525

23. RICART, JUAN. Hopster: Automated discovery of mathematical properties in HOL .

Degree: Chalmers tekniska högskola / Institutionen för data och informationsteknik, 2019, Chalmers University of Technology

URL: http://hdl.handle.net/20.500.12380/300420

► A new tactic for HOL is proposed that is suitable for proving equational properties of functional programs. HOL has numerous tactics that automate the process… (more)

Subjects/Keywords: theory exploration; automated theorem proving; hopster; hol; quickspec

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

RICART, J. (2019). Hopster: Automated discovery of mathematical properties in HOL . (Thesis). Chalmers University of Technology. Retrieved from http://hdl.handle.net/20.500.12380/300420

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

Chicago Manual of Style (16^th Edition):

RICART, JUAN. “Hopster: Automated discovery of mathematical properties in HOL .” 2019. Thesis, Chalmers University of Technology. Accessed March 05, 2021. http://hdl.handle.net/20.500.12380/300420.

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

MLA Handbook (7^th Edition):

RICART, JUAN. “Hopster: Automated discovery of mathematical properties in HOL .” 2019. Web. 05 Mar 2021.

Vancouver:

RICART J. Hopster: Automated discovery of mathematical properties in HOL . [Internet] [Thesis]. Chalmers University of Technology; 2019. [cited 2021 Mar 05]. Available from: http://hdl.handle.net/20.500.12380/300420.

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

Council of Science Editors:

RICART J. Hopster: Automated discovery of mathematical properties in HOL . [Thesis]. Chalmers University of Technology; 2019. Available from: http://hdl.handle.net/20.500.12380/300420

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

University of New South Wales

24. Syeda, Hira. Low-level program verification under cached address translation.

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

URL: http://handle.unsw.edu.au/1959.4/63277 ; https://unsworks.unsw.edu.au/fapi/datastream/unsworks:60079/SOURCE02?view=true

► Operating system (OS) kernels achieve isolation between user-level processes using multi-level page tables. The hardware-implemented translation lookaside buffer (TLB) caches page table walks, and therefore… (more)

▼ Operating system (OS) kernels achieve isolation between user-level processes using multi-level page tables. The hardware-implemented translation lookaside buffer (TLB) caches page table walks, and therefore the TLB and its consistency with memory are security critical for OS kernels, including formally verified kernels such as seL4. If performance is paramount, this consistency can be subtle to achieve; yet, all major formally verified kernels currently leave the TLB as an assumption. They assume correct TLB management because faithfully modeling the hardware details of a TLB would significantly complicate the program logic used to verify the OS code. For instance, a simple memory read operation would now change the state of the program. In this thesis, we present a formal model of the memory management unit (MMU) in the interactive proof assistant Isabelle/HOL for the ARMv7-A architecture which includes the TLB, its maintenance operations, and its derived properties. We integrate this specification into the Cambridge ARM model. We derive sufficient conditions for TLB consistency, and we abstract away the functional details of the MMU using data refinement for simpler reasoning about executions in the presence of cached address translation, including complete and partial walks. Based on the verified abstraction of the MMU model of the ARMv7-A architecture, we present a logic in Isabelle/HOL for reasoning about low-level programs in the presence of cached address translation. We extract invariants and necessary conditions for correct TLB operation that mirror the informal reasoning of OS engineers. We show that our program logic reduces to a standard logic for user-level reasoning, reduces to side-condition checks for kernel-level reasoning, and can handle typical OS kernel tasks such as context switching and page table manipulations. This research removes the unnecessary TLB complexities from program reasoning, and provides a reasoning framework for validating TLB management in OS kernel verification. Advisors/Committee Members: Klein, Gerwin, Computer Science & Engineering, Faculty of Engineering, UNSW, Elphinstone, Kevin, Computer Science & Engineering, Faculty of Engineering, UNSW.

Subjects/Keywords: Theorem proving; Operating system verification; Cached address translation

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Syeda, H. (2019). Low-level program verification under cached address translation. (Doctoral Dissertation). University of New South Wales. Retrieved from http://handle.unsw.edu.au/1959.4/63277 ; https://unsworks.unsw.edu.au/fapi/datastream/unsworks:60079/SOURCE02?view=true

Chicago Manual of Style (16^th Edition):

Syeda, Hira. “Low-level program verification under cached address translation.” 2019. Doctoral Dissertation, University of New South Wales. Accessed March 05, 2021. http://handle.unsw.edu.au/1959.4/63277 ; https://unsworks.unsw.edu.au/fapi/datastream/unsworks:60079/SOURCE02?view=true.

MLA Handbook (7^th Edition):

Syeda, Hira. “Low-level program verification under cached address translation.” 2019. Web. 05 Mar 2021.

Vancouver:

Syeda H. Low-level program verification under cached address translation. [Internet] [Doctoral dissertation]. University of New South Wales; 2019. [cited 2021 Mar 05]. Available from: http://handle.unsw.edu.au/1959.4/63277 ; https://unsworks.unsw.edu.au/fapi/datastream/unsworks:60079/SOURCE02?view=true.

Council of Science Editors:

Syeda H. Low-level program verification under cached address translation. [Doctoral Dissertation]. University of New South Wales; 2019. Available from: http://handle.unsw.edu.au/1959.4/63277 ; https://unsworks.unsw.edu.au/fapi/datastream/unsworks:60079/SOURCE02?view=true

University of New South Wales

25. Boyton, Andrew. Secure architectures on a verified microkernel.

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

URL: http://handle.unsw.edu.au/1959.4/55628 ; https://unsworks.unsw.edu.au/fapi/datastream/unsworks:38182/SOURCE02?view=true

► The safety and security of software systems depends on how they are initially configured. Manually writing program codethat establishes such an initial configuration is a… (more)

Subjects/Keywords: Separation logic; Interactive Theorem Proving; Microkernels; Separation logic

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Boyton, A. (2014). Secure architectures on a verified microkernel. (Doctoral Dissertation). University of New South Wales. Retrieved from http://handle.unsw.edu.au/1959.4/55628 ; https://unsworks.unsw.edu.au/fapi/datastream/unsworks:38182/SOURCE02?view=true

Chicago Manual of Style (16^th Edition):

Boyton, Andrew. “Secure architectures on a verified microkernel.” 2014. Doctoral Dissertation, University of New South Wales. Accessed March 05, 2021. http://handle.unsw.edu.au/1959.4/55628 ; https://unsworks.unsw.edu.au/fapi/datastream/unsworks:38182/SOURCE02?view=true.

MLA Handbook (7^th Edition):

Boyton, Andrew. “Secure architectures on a verified microkernel.” 2014. Web. 05 Mar 2021.

Vancouver:

Boyton A. Secure architectures on a verified microkernel. [Internet] [Doctoral dissertation]. University of New South Wales; 2014. [cited 2021 Mar 05]. Available from: http://handle.unsw.edu.au/1959.4/55628 ; https://unsworks.unsw.edu.au/fapi/datastream/unsworks:38182/SOURCE02?view=true.

Council of Science Editors:

Boyton A. Secure architectures on a verified microkernel. [Doctoral Dissertation]. University of New South Wales; 2014. Available from: http://handle.unsw.edu.au/1959.4/55628 ; https://unsworks.unsw.edu.au/fapi/datastream/unsworks:38182/SOURCE02?view=true

University of New South Wales

26. Matichuk, Daniel. Automation for Proof Engineering: Machine-Checked Proofs At Scale.

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

URL: http://handle.unsw.edu.au/1959.4/60290 ; https://unsworks.unsw.edu.au/fapi/datastream/unsworks:51703/SOURCE2?view=true

► Formal proofs, interactively developed and machine-checked, are a means to achieve the highest level of assurance in the correctness of software. In larger verification projects,… (more)

▼ Formal proofs, interactively developed and machine-checked, are a means to achieve the highest level of assurance in the correctness of software. In larger verification projects, with multi-year timelines and hundreds of thousands of lines of proof text, the emerging discipline of proof engineering plays a critical role in minimizing both the cost and effort of developing formal proofs. The work presented in this thesis targets the scalability challenges present in such projects. In a systematic analysis of several large software verification projects in the interactive proof assistant Isabelle, we demonstrate that in these projects, as the size of a formal specification increases, the required effort for its corresponding proof grows quadratically. Proof engineering encompasses both authoring proofs, and developing the necessary infrastructure to make those proofs tractable, scalable and robust against specification changes. Proof automation plays a key role here. However, in the context of Isabelle, many advanced features, such as developing custom automated reasoning procedures, are outside the standard repertoire of the majority of proof authors. To address this problem, we present Eisbach: an extension to Isabelle's formal proof document language Isar. Eisbach allows proof authors to write automated reasoning procedures, known as proof methods, at the familiar level of abstraction provided by Isar. Additionally, Eisbach is extensible through specialized methods that act as general language constructs, providing high-level access to advanced features of Isabelle, such as subgoal matching. We show how Eisbach provides a framework for extending Isar with more automation than was previously possible, by allowing proof methods to be treated as first-class language elements. Today, Eisbach is already used in many Isabelle proof developments. We further demonstrate its effectiveness by implementing several language extensions, together with a collection of proof methods for performing program refinement proofs. By applying these to proofs from the L4.verified project, the one of the largest formal proof projects in history, we show that effective use of Eisbach results in a reduction in the overall proof size and required effort for a given specification. Advisors/Committee Members: Klein, Gerwin, Computer Science & Engineering, Faculty of Engineering, UNSW, Murray, Toby, Computer Science & Engineering, Faculty of Engineering, UNSW, Chakravarty, Manuel M T, Computer Science & Engineering, Faculty of Engineering, UNSW.

Subjects/Keywords: Automated reasoning; Interactive theorem proving; Proof engineering; Machine-checked proof

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Matichuk, D. (2018). Automation for Proof Engineering: Machine-Checked Proofs At Scale. (Doctoral Dissertation). University of New South Wales. Retrieved from http://handle.unsw.edu.au/1959.4/60290 ; https://unsworks.unsw.edu.au/fapi/datastream/unsworks:51703/SOURCE2?view=true

Chicago Manual of Style (16^th Edition):

Matichuk, Daniel. “Automation for Proof Engineering: Machine-Checked Proofs At Scale.” 2018. Doctoral Dissertation, University of New South Wales. Accessed March 05, 2021. http://handle.unsw.edu.au/1959.4/60290 ; https://unsworks.unsw.edu.au/fapi/datastream/unsworks:51703/SOURCE2?view=true.

MLA Handbook (7^th Edition):

Matichuk, Daniel. “Automation for Proof Engineering: Machine-Checked Proofs At Scale.” 2018. Web. 05 Mar 2021.

Vancouver:

Matichuk D. Automation for Proof Engineering: Machine-Checked Proofs At Scale. [Internet] [Doctoral dissertation]. University of New South Wales; 2018. [cited 2021 Mar 05]. Available from: http://handle.unsw.edu.au/1959.4/60290 ; https://unsworks.unsw.edu.au/fapi/datastream/unsworks:51703/SOURCE2?view=true.

Council of Science Editors:

Matichuk D. Automation for Proof Engineering: Machine-Checked Proofs At Scale. [Doctoral Dissertation]. University of New South Wales; 2018. Available from: http://handle.unsw.edu.au/1959.4/60290 ; https://unsworks.unsw.edu.au/fapi/datastream/unsworks:51703/SOURCE2?view=true

Simon Fraser University

27. Mitchell, David G. An empirical study of random SAT.

Degree: 1993, Simon Fraser University

URL: http://summit.sfu.ca/item/5624

Subjects/Keywords: Automatic theorem proving.; Artificial intelligence.

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Mitchell, D. G. (1993). An empirical study of random SAT. (Thesis). Simon Fraser University. Retrieved from http://summit.sfu.ca/item/5624

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

Chicago Manual of Style (16^th Edition):

Mitchell, David G. “An empirical study of random SAT.” 1993. Thesis, Simon Fraser University. Accessed March 05, 2021. http://summit.sfu.ca/item/5624.

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

MLA Handbook (7^th Edition):

Mitchell, David G. “An empirical study of random SAT.” 1993. Web. 05 Mar 2021.

Vancouver:

Mitchell DG. An empirical study of random SAT. [Internet] [Thesis]. Simon Fraser University; 1993. [cited 2021 Mar 05]. Available from: http://summit.sfu.ca/item/5624.

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

Council of Science Editors:

Mitchell DG. An empirical study of random SAT. [Thesis]. Simon Fraser University; 1993. Available from: http://summit.sfu.ca/item/5624

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

Univerzitet u Beogradu

28. Marinković, Vesna, 1982-. Аутоматско решавање конструктивних проблема у геометрији.

Degree: Matematički fakultet, 2016, Univerzitet u Beogradu

URL: https://fedorabg.bg.ac.rs/fedora/get/o:11479/bdef:Content/get

►

Рачунарство - Вештачка интелигенција / Artificial Intelligence

Проблеми геометријских конструкција уз помоћ лењира и шестара представљају један од најстаријих и најизазовнијих проблема у елементарној математици.… (more)

Subjects/Keywords: automated reasoning; automated theorem proving; interactive theorem proving; automated generation of readable proofs; coherent logic; geometry construction problems; constructions by ruler and compass

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Marinković, Vesna, 1. (2016). Аутоматско решавање конструктивних проблема у геометрији. (Thesis). Univerzitet u Beogradu. Retrieved from https://fedorabg.bg.ac.rs/fedora/get/o:11479/bdef:Content/get

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

Chicago Manual of Style (16^th Edition):

Marinković, Vesna, 1982-. “Аутоматско решавање конструктивних проблема у геометрији.” 2016. Thesis, Univerzitet u Beogradu. Accessed March 05, 2021. https://fedorabg.bg.ac.rs/fedora/get/o:11479/bdef:Content/get.

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

MLA Handbook (7^th Edition):

Marinković, Vesna, 1982-. “Аутоматско решавање конструктивних проблема у геометрији.” 2016. Web. 05 Mar 2021.

Vancouver:

Marinković, Vesna 1. Аутоматско решавање конструктивних проблема у геометрији. [Internet] [Thesis]. Univerzitet u Beogradu; 2016. [cited 2021 Mar 05]. Available from: https://fedorabg.bg.ac.rs/fedora/get/o:11479/bdef:Content/get.

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

Council of Science Editors:

Marinković, Vesna 1. Аутоматско решавање конструктивних проблема у геометрији. [Thesis]. Univerzitet u Beogradu; 2016. Available from: https://fedorabg.bg.ac.rs/fedora/get/o:11479/bdef:Content/get

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

Indian Institute of Science

29. Prathamesh, Turga Venkata Hanumantha. Mechanising knot Theory.

Degree: PhD, Faculty of Science, 2018, Indian Institute of Science

URL: http://etd.iisc.ac.in/handle/2005/3052

► Mechanisation of Mathematics refers to use of computers to generate or check proofs in Mathematics. It involves translation of relevant mathematical theories from one system… (more)

Subjects/Keywords: Knot Theory; Theorem Proving; Formal Theorem Proving; Kauffman Bracket; Link Theory; First Order Logic; Tangles; Matrices; Formalising Knot Theory; Symbolic and Mathematical Logic; Knots; Braids; Mathematics

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Prathamesh, T. V. H. (2018). Mechanising knot Theory. (Doctoral Dissertation). Indian Institute of Science. Retrieved from http://etd.iisc.ac.in/handle/2005/3052

Chicago Manual of Style (16^th Edition):

Prathamesh, Turga Venkata Hanumantha. “Mechanising knot Theory.” 2018. Doctoral Dissertation, Indian Institute of Science. Accessed March 05, 2021. http://etd.iisc.ac.in/handle/2005/3052.

MLA Handbook (7^th Edition):

Prathamesh, Turga Venkata Hanumantha. “Mechanising knot Theory.” 2018. Web. 05 Mar 2021.

Vancouver:

Prathamesh TVH. Mechanising knot Theory. [Internet] [Doctoral dissertation]. Indian Institute of Science; 2018. [cited 2021 Mar 05]. Available from: http://etd.iisc.ac.in/handle/2005/3052.

Council of Science Editors:

Prathamesh TVH. Mechanising knot Theory. [Doctoral Dissertation]. Indian Institute of Science; 2018. Available from: http://etd.iisc.ac.in/handle/2005/3052

30. Mohand Oussaïd, Linda. Conception et vérification formelles des interfaces homme-machine multimodales : applications à la multimodalité en sortie : Formal modelling and verification of multimodal human computer interfaces : output multimodality.

Degree: Docteur es, Informatique et applications, 2014, Chasseneuil-du-Poitou, Ecole nationale supérieure de mécanique et d'aérotechnique

URL: http://www.theses.fr/2014ESMA0022

►

Les interfaces homme-machine (IHM) multimodales offrent à l’utilisateur la possibilité de combiner les modalités d’interaction afin d’augmenter la robustesse et l’utilisabilité de l’interface utilisateur d’un… (more)

▼

Les interfaces homme-machine (IHM) multimodales offrent à l’utilisateur la possibilité de combiner les modalités d’interaction afin d’augmenter la robustesse et l’utilisabilité de l’interface utilisateur d’un système. Plus particulièrement, en sortie, les IHM multimodales permettent au système de restituer à l’utilisateur, l’information produite par le noyau fonctionnel en combinant sémantiquement plusieurs modalités. Dans l’optique de concevoir de telles interfaces pour des systèmes critiques, nous avons proposé un modèle formel de conception des interfaces multimodales en sortie. Le modèle proposé se décompose en deux modèles : le modèle de fission sémantique qui décrit la décomposition de l’information à restituer en informations élémentaires, et le modèle d’allocation qui spécifie l’allocation des modalités et médias aux informations élémentaires. Nous avons également développé une formalisation B Événementiel détaillée des deux modèles : fission sémantique et allocation. Cette formalisation a été instanciée sur des études de cas puis généralisée dans un processus de développement B Événementiel cadre dans lequel s’inscrivent les modèles de fission sémantique et d’allocation. Cette formalisation a permis de procéder à la vérification de propriétés de sûreté, de vivacité et d’utilisabilité.

Multimodal Human-Computer Interfaces (HCI) offer to users the possibility to combine interaction modalities in order to increase user interface robustness and usability. Specifically, output multimodal HCI allow system to return to the user, the information generated by the functional core by combining semantically different modalities. In order to design such interfaces for critical systems, we proposed a formal model for the design of output multimodal interfaces. The proposed model consists of two models: the semantic fission model describes the decomposition of the information to return into elementary information and the allocation model specifies the allocation of the elementary information with modalities and media. We have also developed a detailed Event B formalization for the two models: semantic fission and allocation. This formalization has been instantiated on case studies and generalized in an Event B development process framework including semantic fission and allocation models. This formalization allows to carry out safety, liveness and usability properties verification.

Advisors/Committee Members: Aït-Ameur, Yamine (thesis director), Aït-Sadoune, Idir (thesis director).

Subjects/Keywords: Multimodalité en sortie; Raffinement; Preuve de théorème; Output multimodality; Refinement; Theorem proving

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Mohand Oussaïd, L. (2014). Conception et vérification formelles des interfaces homme-machine multimodales : applications à la multimodalité en sortie : Formal modelling and verification of multimodal human computer interfaces : output multimodality. (Doctoral Dissertation). Chasseneuil-du-Poitou, Ecole nationale supérieure de mécanique et d'aérotechnique. Retrieved from http://www.theses.fr/2014ESMA0022

Chicago Manual of Style (16^th Edition):

Mohand Oussaïd, Linda. “Conception et vérification formelles des interfaces homme-machine multimodales : applications à la multimodalité en sortie : Formal modelling and verification of multimodal human computer interfaces : output multimodality.” 2014. Doctoral Dissertation, Chasseneuil-du-Poitou, Ecole nationale supérieure de mécanique et d'aérotechnique. Accessed March 05, 2021. http://www.theses.fr/2014ESMA0022.

MLA Handbook (7^th Edition):

Mohand Oussaïd, Linda. “Conception et vérification formelles des interfaces homme-machine multimodales : applications à la multimodalité en sortie : Formal modelling and verification of multimodal human computer interfaces : output multimodality.” 2014. Web. 05 Mar 2021.

Vancouver:

Mohand Oussaïd L. Conception et vérification formelles des interfaces homme-machine multimodales : applications à la multimodalité en sortie : Formal modelling and verification of multimodal human computer interfaces : output multimodality. [Internet] [Doctoral dissertation]. Chasseneuil-du-Poitou, Ecole nationale supérieure de mécanique et d'aérotechnique; 2014. [cited 2021 Mar 05]. Available from: http://www.theses.fr/2014ESMA0022.

Council of Science Editors:

Mohand Oussaïd L. Conception et vérification formelles des interfaces homme-machine multimodales : applications à la multimodalité en sortie : Formal modelling and verification of multimodal human computer interfaces : output multimodality. [Doctoral Dissertation]. Chasseneuil-du-Poitou, Ecole nationale supérieure de mécanique et d'aérotechnique; 2014. Available from: http://www.theses.fr/2014ESMA0022

		in
And / Or
		in
And / Or
		in
And / Or
		in

Open Access Theses and Dissertations