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

Search Limiters

Last 2 Years | English Only

No search limiters apply to these results.

▼ Search Limiters


University of Illinois – Chicago

1. Bernasconi, Anna. Building Deductive Proofs of LTL Properties for Iteratively Refined Systems.

Degree: 2016, University of Illinois – Chicago

 Modern software development processes are evolving from sequential to increasingly agile and incremental paradigms. Verification, unavoidable step of a correct software production, cannot get left… (more)

Subjects/Keywords: formal software verification; model checking; deductive verification; requirements; incremental; deductive proof; deductive system

Record DetailsSimilar RecordsGoogle PlusoneFacebookTwitterCiteULikeMendeleyreddit

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

APA (6th Edition):

Bernasconi, A. (2016). Building Deductive Proofs of LTL Properties for Iteratively Refined Systems. (Thesis). University of Illinois – Chicago. Retrieved from http://hdl.handle.net/10027/20884

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

Bernasconi, Anna. “Building Deductive Proofs of LTL Properties for Iteratively Refined Systems.” 2016. Thesis, University of Illinois – Chicago. Accessed March 30, 2020. http://hdl.handle.net/10027/20884.

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

MLA Handbook (7th Edition):

Bernasconi, Anna. “Building Deductive Proofs of LTL Properties for Iteratively Refined Systems.” 2016. Web. 30 Mar 2020.

Vancouver:

Bernasconi A. Building Deductive Proofs of LTL Properties for Iteratively Refined Systems. [Internet] [Thesis]. University of Illinois – Chicago; 2016. [cited 2020 Mar 30]. Available from: http://hdl.handle.net/10027/20884.

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

Council of Science Editors:

Bernasconi A. Building Deductive Proofs of LTL Properties for Iteratively Refined Systems. [Thesis]. University of Illinois – Chicago; 2016. Available from: http://hdl.handle.net/10027/20884

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


University of Illinois – Urbana-Champaign

2. Pek, Edgar. Automated deductive verification of systems software.

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

 Software has become an integral part of our everyday lives, and so is our reliance on his correct functioning. Systems software lies at the heart… (more)

Subjects/Keywords: software verification; software security; automated deductive reasoning

Record DetailsSimilar RecordsGoogle PlusoneFacebookTwitterCiteULikeMendeleyreddit

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

APA (6th Edition):

Pek, E. (2015). Automated deductive verification of systems software. (Doctoral Dissertation). University of Illinois – Urbana-Champaign. Retrieved from http://hdl.handle.net/2142/88993

Chicago Manual of Style (16th Edition):

Pek, Edgar. “Automated deductive verification of systems software.” 2015. Doctoral Dissertation, University of Illinois – Urbana-Champaign. Accessed March 30, 2020. http://hdl.handle.net/2142/88993.

MLA Handbook (7th Edition):

Pek, Edgar. “Automated deductive verification of systems software.” 2015. Web. 30 Mar 2020.

Vancouver:

Pek E. Automated deductive verification of systems software. [Internet] [Doctoral dissertation]. University of Illinois – Urbana-Champaign; 2015. [cited 2020 Mar 30]. Available from: http://hdl.handle.net/2142/88993.

Council of Science Editors:

Pek E. Automated deductive verification of systems software. [Doctoral Dissertation]. University of Illinois – Urbana-Champaign; 2015. Available from: http://hdl.handle.net/2142/88993

3. Blatter, Lionel. Relational properties for specification and verification of C programs in Frama-C : Propriétés relationnnelles pour la spécification et la vérification de programmes C avec Frama-C.

Degree: Docteur es, Informatique, 2019, Université Paris-Saclay (ComUE)

Les techniques de vérification déductive fournissent des méthodes puissantes pour la vérification formelle des propriétés exprimées dans la Logique de Hoare. Dans cette formalisation, également… (more)

Subjects/Keywords: Propriétés relationnelles; Frama-C; Verification deductive; Relational properties; Frama-C; Deductive Verification

Record DetailsSimilar RecordsGoogle PlusoneFacebookTwitterCiteULikeMendeleyreddit

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

APA (6th Edition):

Blatter, L. (2019). Relational properties for specification and verification of C programs in Frama-C : Propriétés relationnnelles pour la spécification et la vérification de programmes C avec Frama-C. (Doctoral Dissertation). Université Paris-Saclay (ComUE). Retrieved from http://www.theses.fr/2019SACLC065

Chicago Manual of Style (16th Edition):

Blatter, Lionel. “Relational properties for specification and verification of C programs in Frama-C : Propriétés relationnnelles pour la spécification et la vérification de programmes C avec Frama-C.” 2019. Doctoral Dissertation, Université Paris-Saclay (ComUE). Accessed March 30, 2020. http://www.theses.fr/2019SACLC065.

MLA Handbook (7th Edition):

Blatter, Lionel. “Relational properties for specification and verification of C programs in Frama-C : Propriétés relationnnelles pour la spécification et la vérification de programmes C avec Frama-C.” 2019. Web. 30 Mar 2020.

Vancouver:

Blatter L. Relational properties for specification and verification of C programs in Frama-C : Propriétés relationnnelles pour la spécification et la vérification de programmes C avec Frama-C. [Internet] [Doctoral dissertation]. Université Paris-Saclay (ComUE); 2019. [cited 2020 Mar 30]. Available from: http://www.theses.fr/2019SACLC065.

Council of Science Editors:

Blatter L. Relational properties for specification and verification of C programs in Frama-C : Propriétés relationnnelles pour la spécification et la vérification de programmes C avec Frama-C. [Doctoral Dissertation]. Université Paris-Saclay (ComUE); 2019. Available from: http://www.theses.fr/2019SACLC065


University of California – San Diego

4. Ricketts, Daniel. Verification of Sampled-Data Systems using Coq.

Degree: Computer Science, 2017, University of California – San Diego

 Due to their safety-critical nature, cyber-physical systems (CPS) demand the most rigorous verification techniques. However, the complexity of the domain puts many cyber-physical systems outside… (more)

Subjects/Keywords: Computer science; Control theory; Coq; Deductive; Hybrid systems; Verification

Record DetailsSimilar RecordsGoogle PlusoneFacebookTwitterCiteULikeMendeleyreddit

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

APA (6th Edition):

Ricketts, D. (2017). Verification of Sampled-Data Systems using Coq. (Thesis). University of California – San Diego. Retrieved from http://www.escholarship.org/uc/item/5n1899s2

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

Ricketts, Daniel. “Verification of Sampled-Data Systems using Coq.” 2017. Thesis, University of California – San Diego. Accessed March 30, 2020. http://www.escholarship.org/uc/item/5n1899s2.

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

MLA Handbook (7th Edition):

Ricketts, Daniel. “Verification of Sampled-Data Systems using Coq.” 2017. Web. 30 Mar 2020.

Vancouver:

Ricketts D. Verification of Sampled-Data Systems using Coq. [Internet] [Thesis]. University of California – San Diego; 2017. [cited 2020 Mar 30]. Available from: http://www.escholarship.org/uc/item/5n1899s2.

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

Council of Science Editors:

Ricketts D. Verification of Sampled-Data Systems using Coq. [Thesis]. University of California – San Diego; 2017. Available from: http://www.escholarship.org/uc/item/5n1899s2

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

5. Fortin, Jean. BSP-Why, un outil pour la vérification déductive de programmes BSP : machine-checked semantics and application to distributed state-space algorithms : BSP-Why, a tool for deductive verification of BSP programs : sémantiques mécanisées et application aux algorithmes d'espace d'états distribués.

Degree: Docteur es, Informatique, 2013, Université Paris-Est

Cette thèse s'inscrit dans le domaine de la vérification formelle de programmes parallèles. L'enjeu de la vérification formelle est de s'assurer qu'un programme va bien… (more)

Subjects/Keywords: Bsp; Sémantiques; Vérification déductive; Bsp; Semantics; Deductive Verification

Record DetailsSimilar RecordsGoogle PlusoneFacebookTwitterCiteULikeMendeleyreddit

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

APA (6th Edition):

Fortin, J. (2013). BSP-Why, un outil pour la vérification déductive de programmes BSP : machine-checked semantics and application to distributed state-space algorithms : BSP-Why, a tool for deductive verification of BSP programs : sémantiques mécanisées et application aux algorithmes d'espace d'états distribués. (Doctoral Dissertation). Université Paris-Est. Retrieved from http://www.theses.fr/2013PEST1084

Chicago Manual of Style (16th Edition):

Fortin, Jean. “BSP-Why, un outil pour la vérification déductive de programmes BSP : machine-checked semantics and application to distributed state-space algorithms : BSP-Why, a tool for deductive verification of BSP programs : sémantiques mécanisées et application aux algorithmes d'espace d'états distribués.” 2013. Doctoral Dissertation, Université Paris-Est. Accessed March 30, 2020. http://www.theses.fr/2013PEST1084.

MLA Handbook (7th Edition):

Fortin, Jean. “BSP-Why, un outil pour la vérification déductive de programmes BSP : machine-checked semantics and application to distributed state-space algorithms : BSP-Why, a tool for deductive verification of BSP programs : sémantiques mécanisées et application aux algorithmes d'espace d'états distribués.” 2013. Web. 30 Mar 2020.

Vancouver:

Fortin J. BSP-Why, un outil pour la vérification déductive de programmes BSP : machine-checked semantics and application to distributed state-space algorithms : BSP-Why, a tool for deductive verification of BSP programs : sémantiques mécanisées et application aux algorithmes d'espace d'états distribués. [Internet] [Doctoral dissertation]. Université Paris-Est; 2013. [cited 2020 Mar 30]. Available from: http://www.theses.fr/2013PEST1084.

Council of Science Editors:

Fortin J. BSP-Why, un outil pour la vérification déductive de programmes BSP : machine-checked semantics and application to distributed state-space algorithms : BSP-Why, a tool for deductive verification of BSP programs : sémantiques mécanisées et application aux algorithmes d'espace d'états distribués. [Doctoral Dissertation]. Université Paris-Est; 2013. Available from: http://www.theses.fr/2013PEST1084

6. Carloto, Carlos José Abreu Dias da Silva. Towards a formally verified microkernel using the Frama-C toolset.

Degree: 2010, RCAAP

 This dissertation is included in the MSc course in Computer Science of the University of Beira Interior. It is a Formal Method’s related dissertation, where… (more)

Subjects/Keywords: Design by contract; Formal verification; xLuna; Formal methods; Frama-C; Hoare logic; Static verification; Deductive verification; Separation Kernel

Record DetailsSimilar RecordsGoogle PlusoneFacebookTwitterCiteULikeMendeleyreddit

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

APA (6th Edition):

Carloto, C. J. A. D. d. S. (2010). Towards a formally verified microkernel using the Frama-C toolset. (Thesis). RCAAP. Retrieved from http://www.rcaap.pt/detail.jsp?id=oai:ubibliorum.ubi.pt:10400.6/3716

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

Carloto, Carlos José Abreu Dias da Silva. “Towards a formally verified microkernel using the Frama-C toolset.” 2010. Thesis, RCAAP. Accessed March 30, 2020. http://www.rcaap.pt/detail.jsp?id=oai:ubibliorum.ubi.pt:10400.6/3716.

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

MLA Handbook (7th Edition):

Carloto, Carlos José Abreu Dias da Silva. “Towards a formally verified microkernel using the Frama-C toolset.” 2010. Web. 30 Mar 2020.

Vancouver:

Carloto CJADdS. Towards a formally verified microkernel using the Frama-C toolset. [Internet] [Thesis]. RCAAP; 2010. [cited 2020 Mar 30]. Available from: http://www.rcaap.pt/detail.jsp?id=oai:ubibliorum.ubi.pt:10400.6/3716.

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

Council of Science Editors:

Carloto CJADdS. Towards a formally verified microkernel using the Frama-C toolset. [Thesis]. RCAAP; 2010. Available from: http://www.rcaap.pt/detail.jsp?id=oai:ubibliorum.ubi.pt:10400.6/3716

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


University of Colorado

7. Han, Hyojung. Increasing The Effectiveness of Deduction in Propositional SAT Solvers.

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

  The satisfiability (SAT) of a propositional formula is the decision problem to determine whether there is a satisfying assignment that can make the formula… (more)

Subjects/Keywords: CNF; Deductive Power; Dominators; DPLL; Formal Verification; SAT solvers; Computer Sciences; Electrical and Computer Engineering

Record DetailsSimilar RecordsGoogle PlusoneFacebookTwitterCiteULikeMendeleyreddit

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

APA (6th Edition):

Han, H. (2011). Increasing The Effectiveness of Deduction in Propositional SAT Solvers. (Doctoral Dissertation). University of Colorado. Retrieved from https://scholar.colorado.edu/ecen_gradetds/22

Chicago Manual of Style (16th Edition):

Han, Hyojung. “Increasing The Effectiveness of Deduction in Propositional SAT Solvers.” 2011. Doctoral Dissertation, University of Colorado. Accessed March 30, 2020. https://scholar.colorado.edu/ecen_gradetds/22.

MLA Handbook (7th Edition):

Han, Hyojung. “Increasing The Effectiveness of Deduction in Propositional SAT Solvers.” 2011. Web. 30 Mar 2020.

Vancouver:

Han H. Increasing The Effectiveness of Deduction in Propositional SAT Solvers. [Internet] [Doctoral dissertation]. University of Colorado; 2011. [cited 2020 Mar 30]. Available from: https://scholar.colorado.edu/ecen_gradetds/22.

Council of Science Editors:

Han H. Increasing The Effectiveness of Deduction in Propositional SAT Solvers. [Doctoral Dissertation]. University of Colorado; 2011. Available from: https://scholar.colorado.edu/ecen_gradetds/22

8. Clochard, Martin. Méthodes et outils pour la spécification et la preuve de propriétés difficiles de programmes séquentiels : Methods and tools for specification and proof of difficult properties of sequential programs.

Degree: Docteur es, Informatique, 2018, Université Paris-Saclay (ComUE)

Cette thèse se positionne dans le domaine de la vérification déductive de programmes, qui consiste à transformer une propriété à vérifier sur un programme en… (more)

Subjects/Keywords: Vérification déductive; Calcul symbolique; Preuve formelle; Deductive verification; Symbolic computations; Formal proof

Record DetailsSimilar RecordsGoogle PlusoneFacebookTwitterCiteULikeMendeleyreddit

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

APA (6th Edition):

Clochard, M. (2018). Méthodes et outils pour la spécification et la preuve de propriétés difficiles de programmes séquentiels : Methods and tools for specification and proof of difficult properties of sequential programs. (Doctoral Dissertation). Université Paris-Saclay (ComUE). Retrieved from http://www.theses.fr/2018SACLS071

Chicago Manual of Style (16th Edition):

Clochard, Martin. “Méthodes et outils pour la spécification et la preuve de propriétés difficiles de programmes séquentiels : Methods and tools for specification and proof of difficult properties of sequential programs.” 2018. Doctoral Dissertation, Université Paris-Saclay (ComUE). Accessed March 30, 2020. http://www.theses.fr/2018SACLS071.

MLA Handbook (7th Edition):

Clochard, Martin. “Méthodes et outils pour la spécification et la preuve de propriétés difficiles de programmes séquentiels : Methods and tools for specification and proof of difficult properties of sequential programs.” 2018. Web. 30 Mar 2020.

Vancouver:

Clochard M. Méthodes et outils pour la spécification et la preuve de propriétés difficiles de programmes séquentiels : Methods and tools for specification and proof of difficult properties of sequential programs. [Internet] [Doctoral dissertation]. Université Paris-Saclay (ComUE); 2018. [cited 2020 Mar 30]. Available from: http://www.theses.fr/2018SACLS071.

Council of Science Editors:

Clochard M. Méthodes et outils pour la spécification et la preuve de propriétés difficiles de programmes séquentiels : Methods and tools for specification and proof of difficult properties of sequential programs. [Doctoral Dissertation]. Université Paris-Saclay (ComUE); 2018. Available from: http://www.theses.fr/2018SACLS071

9. Parreira Pereira, Mário José. Tools and Techniques for the Verification of Modular Stateful Code : Outils et techniques pour la vérification de programmes impératives modulaires.

Degree: Docteur es, Informatique, 2018, Université Paris-Saclay (ComUE)

Cette thèse se place dans le cadre des méthodes formelles et plus précisément dans celui de la vérification déductive et du système Why3. Ce dernier… (more)

Subjects/Keywords: Vérification déductive; Why3; Effets; Bibliothèque OCaml; OCaml; Modulaire; Deductive verification; Why3; Efects; OCaml library; OCaml; Modularity

Record DetailsSimilar RecordsGoogle PlusoneFacebookTwitterCiteULikeMendeleyreddit

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

APA (6th Edition):

Parreira Pereira, M. J. (2018). Tools and Techniques for the Verification of Modular Stateful Code : Outils et techniques pour la vérification de programmes impératives modulaires. (Doctoral Dissertation). Université Paris-Saclay (ComUE). Retrieved from http://www.theses.fr/2018SACLS605

Chicago Manual of Style (16th Edition):

Parreira Pereira, Mário José. “Tools and Techniques for the Verification of Modular Stateful Code : Outils et techniques pour la vérification de programmes impératives modulaires.” 2018. Doctoral Dissertation, Université Paris-Saclay (ComUE). Accessed March 30, 2020. http://www.theses.fr/2018SACLS605.

MLA Handbook (7th Edition):

Parreira Pereira, Mário José. “Tools and Techniques for the Verification of Modular Stateful Code : Outils et techniques pour la vérification de programmes impératives modulaires.” 2018. Web. 30 Mar 2020.

Vancouver:

Parreira Pereira MJ. Tools and Techniques for the Verification of Modular Stateful Code : Outils et techniques pour la vérification de programmes impératives modulaires. [Internet] [Doctoral dissertation]. Université Paris-Saclay (ComUE); 2018. [cited 2020 Mar 30]. Available from: http://www.theses.fr/2018SACLS605.

Council of Science Editors:

Parreira Pereira MJ. Tools and Techniques for the Verification of Modular Stateful Code : Outils et techniques pour la vérification de programmes impératives modulaires. [Doctoral Dissertation]. Université Paris-Saclay (ComUE); 2018. Available from: http://www.theses.fr/2018SACLS605


Université Paris-Sud – Paris XI

10. Bobot, François. Logique de séparation et vérification déductive : Separation logic and deductive verification.

Degree: Docteur es, Informatique, 2011, Université Paris-Sud – Paris XI

Cette thèse s'inscrit dans la démarche de preuve de programmes à l'aide de vérification déductive. La vérification déductive consiste à produire, à partir des sources… (more)

Subjects/Keywords: Sureté des programmes; Vérification de programmes; Démonstrateur automatique; Encodage; Vérification deductive; Modèle mémoire; Automatisation; Polymorphisme; Structure de donnée; Logique de séparation; Program safety; Program verification; Automatic provers; Encoding; Deductive verification; Memory model; Automatisation; Polymorphisme; Datastructure; Separation logic

Record DetailsSimilar RecordsGoogle PlusoneFacebookTwitterCiteULikeMendeleyreddit

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

APA (6th Edition):

Bobot, F. (2011). Logique de séparation et vérification déductive : Separation logic and deductive verification. (Doctoral Dissertation). Université Paris-Sud – Paris XI. Retrieved from http://www.theses.fr/2011PA112332

Chicago Manual of Style (16th Edition):

Bobot, François. “Logique de séparation et vérification déductive : Separation logic and deductive verification.” 2011. Doctoral Dissertation, Université Paris-Sud – Paris XI. Accessed March 30, 2020. http://www.theses.fr/2011PA112332.

MLA Handbook (7th Edition):

Bobot, François. “Logique de séparation et vérification déductive : Separation logic and deductive verification.” 2011. Web. 30 Mar 2020.

Vancouver:

Bobot F. Logique de séparation et vérification déductive : Separation logic and deductive verification. [Internet] [Doctoral dissertation]. Université Paris-Sud – Paris XI; 2011. [cited 2020 Mar 30]. Available from: http://www.theses.fr/2011PA112332.

Council of Science Editors:

Bobot F. Logique de séparation et vérification déductive : Separation logic and deductive verification. [Doctoral Dissertation]. Université Paris-Sud – Paris XI; 2011. Available from: http://www.theses.fr/2011PA112332

11. Gondelman, Léon. Un système de types pragmatique pour la vérification déductive des programmes : A Pragmatic Type System for Deductive Software Verification.

Degree: Docteur es, Informatique, 2016, Paris Saclay

Cette thèse se place dans le contexte de la vérification déductive des programmes et a pour objectif de formaliser un certain nombre de concepts qui… (more)

Subjects/Keywords: Vérification déductive des programmes; Why3; Raffinement de données; Système de types; Code fantôme; Deductive Software Verification; Why3; Data refinement; Type systems; Ghost code

Record DetailsSimilar RecordsGoogle PlusoneFacebookTwitterCiteULikeMendeleyreddit

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

APA (6th Edition):

Gondelman, L. (2016). Un système de types pragmatique pour la vérification déductive des programmes : A Pragmatic Type System for Deductive Software Verification. (Doctoral Dissertation). Paris Saclay. Retrieved from http://www.theses.fr/2016SACLS583

Chicago Manual of Style (16th Edition):

Gondelman, Léon. “Un système de types pragmatique pour la vérification déductive des programmes : A Pragmatic Type System for Deductive Software Verification.” 2016. Doctoral Dissertation, Paris Saclay. Accessed March 30, 2020. http://www.theses.fr/2016SACLS583.

MLA Handbook (7th Edition):

Gondelman, Léon. “Un système de types pragmatique pour la vérification déductive des programmes : A Pragmatic Type System for Deductive Software Verification.” 2016. Web. 30 Mar 2020.

Vancouver:

Gondelman L. Un système de types pragmatique pour la vérification déductive des programmes : A Pragmatic Type System for Deductive Software Verification. [Internet] [Doctoral dissertation]. Paris Saclay; 2016. [cited 2020 Mar 30]. Available from: http://www.theses.fr/2016SACLS583.

Council of Science Editors:

Gondelman L. Un système de types pragmatique pour la vérification déductive des programmes : A Pragmatic Type System for Deductive Software Verification. [Doctoral Dissertation]. Paris Saclay; 2016. Available from: http://www.theses.fr/2016SACLS583


Université Paris-Sud – Paris XI

12. Bardou, Romain. Vérification de programmes avec pointeurs à l'aide de régions et de permissions : Verification of Pointer Programs Using Regions and Permissions.

Degree: Docteur es, Informatique, 2011, Université Paris-Sud – Paris XI

La vérification déductive de programmes consiste à annoter des programmes par une spécification, c'est-à-dire un ensemble de formules logiques décrivant le comportement du programme, et… (more)

Subjects/Keywords: Typage; Langage de programmation; Vérification déductive; Logique; Alias de pointeurs; Régions; Permissions; Séparation; Modèle mémoire; Typing; Programming languages; Deductive verification; Logic; Pointer aliases; Regions; Permissions; Separation; Memory model

Record DetailsSimilar RecordsGoogle PlusoneFacebookTwitterCiteULikeMendeleyreddit

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

APA (6th Edition):

Bardou, R. (2011). Vérification de programmes avec pointeurs à l'aide de régions et de permissions : Verification of Pointer Programs Using Regions and Permissions. (Doctoral Dissertation). Université Paris-Sud – Paris XI. Retrieved from http://www.theses.fr/2011PA112220

Chicago Manual of Style (16th Edition):

Bardou, Romain. “Vérification de programmes avec pointeurs à l'aide de régions et de permissions : Verification of Pointer Programs Using Regions and Permissions.” 2011. Doctoral Dissertation, Université Paris-Sud – Paris XI. Accessed March 30, 2020. http://www.theses.fr/2011PA112220.

MLA Handbook (7th Edition):

Bardou, Romain. “Vérification de programmes avec pointeurs à l'aide de régions et de permissions : Verification of Pointer Programs Using Regions and Permissions.” 2011. Web. 30 Mar 2020.

Vancouver:

Bardou R. Vérification de programmes avec pointeurs à l'aide de régions et de permissions : Verification of Pointer Programs Using Regions and Permissions. [Internet] [Doctoral dissertation]. Université Paris-Sud – Paris XI; 2011. [cited 2020 Mar 30]. Available from: http://www.theses.fr/2011PA112220.

Council of Science Editors:

Bardou R. Vérification de programmes avec pointeurs à l'aide de régions et de permissions : Verification of Pointer Programs Using Regions and Permissions. [Doctoral Dissertation]. Université Paris-Sud – Paris XI; 2011. Available from: http://www.theses.fr/2011PA112220

13. Andreescu, Oana Fabiana. Static analysis of functional programs with an application to the frame problem in deductive verification : Analyse statique de programmes fonctionnels avec une application au problème du frame dans le domaine de la vérification déductive.

Degree: Docteur es, Informatique, 2017, Rennes 1

Dans le domaine de la vérification formelle de logiciels, il est impératif d'identifier les limites au sein desquelles les éléments ou fonctions opèrent. Ces limites… (more)

Subjects/Keywords: Vérification formelle de logiciels; Analyse statique; Problème du frame; Invariants; Vérification déductive; Analyse de dépendances; Analyse de corrélations; Formal verification; Static analysis; Frame problem; Invariants; Frame properties; Deductive verification; Interactive theorem provers; Dependency analysis; Correlation analysis

Record DetailsSimilar RecordsGoogle PlusoneFacebookTwitterCiteULikeMendeleyreddit

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

APA (6th Edition):

Andreescu, O. F. (2017). Static analysis of functional programs with an application to the frame problem in deductive verification : Analyse statique de programmes fonctionnels avec une application au problème du frame dans le domaine de la vérification déductive. (Doctoral Dissertation). Rennes 1. Retrieved from http://www.theses.fr/2017REN1S047

Chicago Manual of Style (16th Edition):

Andreescu, Oana Fabiana. “Static analysis of functional programs with an application to the frame problem in deductive verification : Analyse statique de programmes fonctionnels avec une application au problème du frame dans le domaine de la vérification déductive.” 2017. Doctoral Dissertation, Rennes 1. Accessed March 30, 2020. http://www.theses.fr/2017REN1S047.

MLA Handbook (7th Edition):

Andreescu, Oana Fabiana. “Static analysis of functional programs with an application to the frame problem in deductive verification : Analyse statique de programmes fonctionnels avec une application au problème du frame dans le domaine de la vérification déductive.” 2017. Web. 30 Mar 2020.

Vancouver:

Andreescu OF. Static analysis of functional programs with an application to the frame problem in deductive verification : Analyse statique de programmes fonctionnels avec une application au problème du frame dans le domaine de la vérification déductive. [Internet] [Doctoral dissertation]. Rennes 1; 2017. [cited 2020 Mar 30]. Available from: http://www.theses.fr/2017REN1S047.

Council of Science Editors:

Andreescu OF. Static analysis of functional programs with an application to the frame problem in deductive verification : Analyse statique de programmes fonctionnels avec une application au problème du frame dans le domaine de la vérification déductive. [Doctoral Dissertation]. Rennes 1; 2017. Available from: http://www.theses.fr/2017REN1S047


Université Paris-Sud – Paris XI

14. Tafat, Asma. Preuves par raffinement de programmes avec pointeurs : Proofs by refinement of programs with pointers.

Degree: Docteur es, Informatique, 2013, Université Paris-Sud – Paris XI

Le but de cette thèse est de spécifier et prouver des programmes avec pointeurs, tels que des programmes C, en utilisant des techniques de raffinement.… (more)

Subjects/Keywords: Méthodes formelles; Vérification déductive; Preuve de programmes; Raffinement; Programmes avec pointeurs; Preuves modulaires; Abstraction de données; Invariants de données; Framac; Formal methods; Deductive verification; Refinement; Modular proofs; Programs with pointers; Data abstraction; Data invariants; Proofs modularity; Framac

Record DetailsSimilar RecordsGoogle PlusoneFacebookTwitterCiteULikeMendeleyreddit

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

APA (6th Edition):

Tafat, A. (2013). Preuves par raffinement de programmes avec pointeurs : Proofs by refinement of programs with pointers. (Doctoral Dissertation). Université Paris-Sud – Paris XI. Retrieved from http://www.theses.fr/2013PA112141

Chicago Manual of Style (16th Edition):

Tafat, Asma. “Preuves par raffinement de programmes avec pointeurs : Proofs by refinement of programs with pointers.” 2013. Doctoral Dissertation, Université Paris-Sud – Paris XI. Accessed March 30, 2020. http://www.theses.fr/2013PA112141.

MLA Handbook (7th Edition):

Tafat, Asma. “Preuves par raffinement de programmes avec pointeurs : Proofs by refinement of programs with pointers.” 2013. Web. 30 Mar 2020.

Vancouver:

Tafat A. Preuves par raffinement de programmes avec pointeurs : Proofs by refinement of programs with pointers. [Internet] [Doctoral dissertation]. Université Paris-Sud – Paris XI; 2013. [cited 2020 Mar 30]. Available from: http://www.theses.fr/2013PA112141.

Council of Science Editors:

Tafat A. Preuves par raffinement de programmes avec pointeurs : Proofs by refinement of programs with pointers. [Doctoral Dissertation]. Université Paris-Sud – Paris XI; 2013. Available from: http://www.theses.fr/2013PA112141

15. Roux, Mattias. Extensions de l’algorithme d’atteignabilité arrière dans le cadre de la vérification de modèles modulo théories : Extensions of the backward reachability algorithm in the model checking modulo theories framework.

Degree: Docteur es, Informatique, 2019, Université Paris-Saclay (ComUE)

Cette thèse se propose de présenter plusieurs extensions ayant été ajoutées au vérificateur de modèles Cubicle.Cubicle est un logiciel permettant de vérifier automatiquement la sûreté… (more)

Subjects/Keywords: Vérification de modèles; Vérification de modèles modulo theories; Vérification déductive; Satisfiabilité modulo théories; Systèmes distribués; Apprentissage non supervisé; Model Checking; Model Checking Modulo Theories; Deductive Verification; Satisfiability Modulo Theories; Distributed Systems; Unsupervised learning

Record DetailsSimilar RecordsGoogle PlusoneFacebookTwitterCiteULikeMendeleyreddit

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

APA (6th Edition):

Roux, M. (2019). Extensions de l’algorithme d’atteignabilité arrière dans le cadre de la vérification de modèles modulo théories : Extensions of the backward reachability algorithm in the model checking modulo theories framework. (Doctoral Dissertation). Université Paris-Saclay (ComUE). Retrieved from http://www.theses.fr/2019SACLS582

Chicago Manual of Style (16th Edition):

Roux, Mattias. “Extensions de l’algorithme d’atteignabilité arrière dans le cadre de la vérification de modèles modulo théories : Extensions of the backward reachability algorithm in the model checking modulo theories framework.” 2019. Doctoral Dissertation, Université Paris-Saclay (ComUE). Accessed March 30, 2020. http://www.theses.fr/2019SACLS582.

MLA Handbook (7th Edition):

Roux, Mattias. “Extensions de l’algorithme d’atteignabilité arrière dans le cadre de la vérification de modèles modulo théories : Extensions of the backward reachability algorithm in the model checking modulo theories framework.” 2019. Web. 30 Mar 2020.

Vancouver:

Roux M. Extensions de l’algorithme d’atteignabilité arrière dans le cadre de la vérification de modèles modulo théories : Extensions of the backward reachability algorithm in the model checking modulo theories framework. [Internet] [Doctoral dissertation]. Université Paris-Saclay (ComUE); 2019. [cited 2020 Mar 30]. Available from: http://www.theses.fr/2019SACLS582.

Council of Science Editors:

Roux M. Extensions de l’algorithme d’atteignabilité arrière dans le cadre de la vérification de modèles modulo théories : Extensions of the backward reachability algorithm in the model checking modulo theories framework. [Doctoral Dissertation]. Université Paris-Saclay (ComUE); 2019. Available from: http://www.theses.fr/2019SACLS582

16. 中野, 昌弘. モデル検査を用いたシステム検証の支援に関する研究.

Degree: Japan Advanced Institute of Science and Technology / 北陸先端科学技術大学院大学

Supervisor:二木 厚吉

情報科学研究科

修士

Subjects/Keywords: 形式仕様, 証明論的手法, モデル検査, 振舞仕様, 仕様変換; Formal Specification, Deductive Verification, Mode

Record DetailsSimilar RecordsGoogle PlusoneFacebookTwitterCiteULikeMendeleyreddit

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

APA (6th Edition):

中野, . (n.d.). モデル検査を用いたシステム検証の支援に関する研究. (Thesis). Japan Advanced Institute of Science and Technology / 北陸先端科学技術大学院大学. Retrieved from http://hdl.handle.net/10119/1680

Note: this citation may be lacking information needed for this citation format:
No year of publication.
Not specified: Masters Thesis or Doctoral Dissertation

Chicago Manual of Style (16th Edition):

中野, 昌弘. “モデル検査を用いたシステム検証の支援に関する研究.” Thesis, Japan Advanced Institute of Science and Technology / 北陸先端科学技術大学院大学. Accessed March 30, 2020. http://hdl.handle.net/10119/1680.

Note: this citation may be lacking information needed for this citation format:
No year of publication.
Not specified: Masters Thesis or Doctoral Dissertation

MLA Handbook (7th Edition):

中野, 昌弘. “モデル検査を用いたシステム検証の支援に関する研究.” Web. 30 Mar 2020.

Note: this citation may be lacking information needed for this citation format:
No year of publication.

Vancouver:

中野 . モデル検査を用いたシステム検証の支援に関する研究. [Internet] [Thesis]. Japan Advanced Institute of Science and Technology / 北陸先端科学技術大学院大学; [cited 2020 Mar 30]. Available from: http://hdl.handle.net/10119/1680.

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
No year of publication.

Council of Science Editors:

中野 . モデル検査を用いたシステム検証の支援に関する研究. [Thesis]. Japan Advanced Institute of Science and Technology / 北陸先端科学技術大学院大学; Available from: http://hdl.handle.net/10119/1680

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
No year of publication.

.