subject:(proof checking)

1. Radhouani, Amira. Méthodes formelles pour l'extraction d'attaques internes des Systèmes d'Information : Formal methods for extracting insider attacks from Information Systems.

Degree: Docteur es, Informatique, 2017, Université Grenoble Alpes (ComUE); Université de Tunis. Faculté des sciences de Tunis

URL: http://www.theses.fr/2017GREAM025

►

La sécurité des Systèmes d’Information (SI) constitue un défi majeur car elle conditionne amplement la future exploitation d’un SI. C’est pourquoi l’étude des vulnérabilités d’un… (more)

▼

La sécurité des Systèmes d’Information (SI) constitue un défi majeur car elle conditionne amplement la future exploitation d’un SI. C’est pourquoi l’étude des vulnérabilités d’un SI dès les phases conceptuelles est cruciale. Il s’agit d’étudier la validation de politiques de sécurité, souvent exprimées par des règles de contrôle d’accès, et d’effectuer des vérifications automatisées sur des modèles afin de garantir une certaine confiance dans le SI avant son opérationnalisation. Notre intérêt porte plus particulièrement sur la détection des vulnérabilités pouvant être exploitées par des utilisateurs internes afin de commettre des attaques, appelées attaques internes, en profitant de leur accès légitime au système. Pour ce faire, nous exploitons des spécifications formelles B générées, par la plateforme B4MSecure, à partir de modèles fonctionnels UML et d’une description Secure UML des règles de contrôle d’accès basées sur les rôles. Ces vulnérabilités étant dues à l’évolution dynamique de l’état fonctionnel du système, nous proposons d’étudier l’atteignabilité des états, dits indésirables, donnant lieu à des attaques potentielles, à partir d’un état normal du système. Les techniques proposées constituent une alternative aux techniques de model-checking. En effet, elles mettent en œuvre une recherche symbolique vers l’arrière fondée sur des approches complémentaires : la preuve et la résolution de contraintes. Ce processus de recherche est entièrement automatisé grâce à notre outil GenISIS qui a montré, sur la base d’études de cas disponibles dans la littérature, sa capacité à retrouver des attaques déjà publiées mais aussi des attaques nouvelles.

The early detection of potential threats during the modelling phase of a Secure Information System (IS) is required because it favours the design of a robust access control policy and the prevention of malicious behaviours during the system execution. This involves studying the validation of access control rules and performing vulnerabilities automated checks before the IS operationalization. We are particularly interested in detecting vulnerabilities that can be exploited by internal trusted users to commit attacks, called insider attacks, by taking advantage of their legitimate access to the system. To do so, we use formal B specifications which are generated by the B4MSecure platform from UML functional models and a SecureUML modelling of role-based access control rules. Since these vulnerabilities are due to the dynamic evolution of the functional state, we propose to study the reachability of someundesirable states starting from a normal state of the system. The proposed techniques are an alternative to model-checking techniques. Indeed, they implement symbolic backward search algorithm based on complementary approaches: proof and constraint solving. This rich technical background allowed the development of the GenISIS tool which automates our approach and which was successfully experimented on several case studies available in the literature. These experiments…

Advisors/Committee Members: Ledru, Yves (thesis director), Idani, Akram (thesis director).

Subjects/Keywords: Attaques internes; B; Preuve; Résolution de contraintes; Model-Checking; Atteignabilité; Insider attacks; B-Method; Proof; Constraint solving; Model-Checking; Reachability; 004

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Radhouani, A. (2017). Méthodes formelles pour l'extraction d'attaques internes des Systèmes d'Information : Formal methods for extracting insider attacks from Information Systems. (Doctoral Dissertation). Université Grenoble Alpes (ComUE); Université de Tunis. Faculté des sciences de Tunis. Retrieved from http://www.theses.fr/2017GREAM025

Chicago Manual of Style (16^th Edition):

Radhouani, Amira. “Méthodes formelles pour l'extraction d'attaques internes des Systèmes d'Information : Formal methods for extracting insider attacks from Information Systems.” 2017. Doctoral Dissertation, Université Grenoble Alpes (ComUE); Université de Tunis. Faculté des sciences de Tunis. Accessed February 28, 2021. http://www.theses.fr/2017GREAM025.

MLA Handbook (7^th Edition):

Radhouani, Amira. “Méthodes formelles pour l'extraction d'attaques internes des Systèmes d'Information : Formal methods for extracting insider attacks from Information Systems.” 2017. Web. 28 Feb 2021.

Vancouver:

Radhouani A. Méthodes formelles pour l'extraction d'attaques internes des Systèmes d'Information : Formal methods for extracting insider attacks from Information Systems. [Internet] [Doctoral dissertation]. Université Grenoble Alpes (ComUE); Université de Tunis. Faculté des sciences de Tunis; 2017. [cited 2021 Feb 28]. Available from: http://www.theses.fr/2017GREAM025.

Council of Science Editors:

Radhouani A. Méthodes formelles pour l'extraction d'attaques internes des Systèmes d'Information : Formal methods for extracting insider attacks from Information Systems. [Doctoral Dissertation]. Université Grenoble Alpes (ComUE); Université de Tunis. Faculté des sciences de Tunis; 2017. Available from: http://www.theses.fr/2017GREAM025

University of Illinois – Chicago

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

Degree: 2016, University of Illinois – Chicago

URL: http://hdl.handle.net/10027/20884

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

▼ 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 behind by this quickly changing practice. Advances in verification techniques have been considerable in the past years, and feasibility has been achieved on always greater systems. Nevertheless, we believe that verification and modern development processes are still not going at the same pace in terms of incrementality. Classical verification algorithms are applied when a complete specification of the model is available, and several development costs and efforts have been already spent. Today more than ever, the description of a system changes continuously during the phase of analysis, asking for periodical adjustments in its specifications. Various parts are often only sketched awaiting further enrichment, which is sometimes delegated to third parties. The classical scenario is, therefore, not applicable anymore: it becomes essential to come up with light iterative methods of verification that can be applied also to incomplete models at each stage of the design and development phases, contributing more incisively to developers choices. With particular focus on two main verification techniques, model checking and deductive verification, we study a way integrating them into this incremental context. The idea is to supply each step of the design phase with a way to prove behaviors of incomplete systems or only single components. Step-wise model checking can be augmented by a simple incremental deductive system generator that justifies why the system meets some requested temporal specification. This kind of infrastructure can bring a useful contribution in cases and refinements where safety, starvation or liveness are critical, and, in general, guide the choices of the developer that faces different designs. The main idea is to combine two approaches presented in literature: we would like to exploit a procedure of model checking that supports incompletely specified systems and we study a mechanism to build deductive proofs using information gathered during model checking. This thesis deals with the construction of these incremental deductive proofs of linear temporal logic properties in incomplete systems that are completed progressively when the system gets refined. Advisors/Committee Members: Zuck, Lenore D. (advisor), Sistla, Prasad (committee member), Lanzi, Pier Luca (committee member).

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

Record Details Similar Records Cite « Share

❌

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

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

Bernasconi, Anna. “Building Deductive Proofs of LTL Properties for Iteratively Refined Systems.” 2016. Thesis, University of Illinois – Chicago. Accessed February 28, 2021. 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 (7^th Edition):

Bernasconi, Anna. “Building Deductive Proofs of LTL Properties for Iteratively Refined Systems.” 2016. Web. 28 Feb 2021.

Vancouver:

Bernasconi A. Building Deductive Proofs of LTL Properties for Iteratively Refined Systems. [Internet] [Thesis]. University of Illinois – Chicago; 2016. [cited 2021 Feb 28]. 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 Minnesota

3. Ghassabani, Elaheh. Inductive Validity Cores.

Degree: PhD, Computer Science, 2018, University of Minnesota

URL: http://hdl.handle.net/11299/201700

► Symbolic model checkers can construct proofs of properties over very complex models. However, the results reported by the tool when a proof succeeds do not… (more)

Subjects/Keywords: Inductive proofs; Proof-cores; SMAT solving; Symbolic model checking; Traceability; Unsat-cores

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Ghassabani, E. (2018). Inductive Validity Cores. (Doctoral Dissertation). University of Minnesota. Retrieved from http://hdl.handle.net/11299/201700

Chicago Manual of Style (16^th Edition):

Ghassabani, Elaheh. “Inductive Validity Cores.” 2018. Doctoral Dissertation, University of Minnesota. Accessed February 28, 2021. http://hdl.handle.net/11299/201700.

MLA Handbook (7^th Edition):

Ghassabani, Elaheh. “Inductive Validity Cores.” 2018. Web. 28 Feb 2021.

Vancouver:

Ghassabani E. Inductive Validity Cores. [Internet] [Doctoral dissertation]. University of Minnesota; 2018. [cited 2021 Feb 28]. Available from: http://hdl.handle.net/11299/201700.

Council of Science Editors:

Ghassabani E. Inductive Validity Cores. [Doctoral Dissertation]. University of Minnesota; 2018. Available from: http://hdl.handle.net/11299/201700

4. Todorov, Vassil. Automotive embedded software design using formal methods : Intégration de méthodes formelles dans la conception des fonctions logicielles automobiles.

Degree: Docteur es, Informatique, 2020, université Paris-Saclay

URL: http://www.theses.fr/2020UPASG026

►

La part croissante des fonctions d'assistance à la conduite, leur criticité, ainsi que la perspective d'une certification de ces fonctions, rendent nécessaire leur vérification et… (more)

▼

La part croissante des fonctions d'assistance à la conduite, leur criticité, ainsi que la perspective d'une certification de ces fonctions, rendent nécessaire leur vérification et leur validation avec un niveau d'exigence que le test seul ne peut assurer.Depuis quelques années déjà d’autres domaines comme l’aéronautique ou le ferroviaire sont soumis à des contextes équivalents. Pour répondre à certaines contraintes ils ont localement mis en place des méthodes formelles. Nous nous intéressons aux motivations et aux critères qui ont conduit à l’utilisation des méthodes formelles dans ces domaines afin de les transposer sur des scénarios automobiles et identifier le périmètre potentiel d'application.Dans cette thèse, nous présentons nos études de cas et proposons des méthodologies pour l'usage de méthodes formelles par des ingénieurs non-experts. Le model checking inductif pour un processus de développement utilisant des modèles, l'interprétation abstraite pour démontrer l'absence d'erreurs d'exécution du code et la preuve déductive pour des cas de fonctions critiques de librairie.Enfin, nous proposons de nouveaux algorithmes pour résoudre les problèmes identifiés lors de nos expérimentations. Il s'agit d'une part d'un générateur d'invariants et d'une méthode utilisant la sémantique des données pour traiter efficacement des propriétés comportant du temps long, et d'autre part d'un algorithme efficace pour mesurer la couverture du modèle par les propriétés en utilisant des techniques de mutation.

The growing share of driver assistance functions, their criticality, as well as the prospect of certification of these functions, make their verification and validation necessary with a level of requirement that testing alone cannot ensure. For several years now, other industries such as aeronautics and railways have been subject to equivalent contexts. To respond to certain constraints, they have locally implemented formal methods. We are interested in the motivations and criteria that led to the use of formal methods in these industries in order to transpose them to automotive scenarios and identify the potential scope of application.In this thesis, we present our case studies and propose methodologies for the use of formal methods by non-expert engineers. Inductive model checking for a model-driven development process, abstract interpretation to demonstrate the absence of run-time errors in the code and deductive proof for critical library functions.Finally, we propose new algorithms to solve the problems identified during our experiments. These are, firstly, an invariant generator and a method using the semantics of data to process properties involving long-running timers in an efficient way, and secondly, an efficient algorithm to measure the coverage of the model by the properties using mutation techniques.

Advisors/Committee Members: Boulanger, Frédéric (thesis director).

Subjects/Keywords: Génie logiciel; Vérification de logiciel; Méthodes formelles; Model checking; Interprétation abstraite; Preuve déductive; Software engineering; Software verification; Formal methods; Model checking; Abstract interpretation; Deductive proof

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Todorov, V. (2020). Automotive embedded software design using formal methods : Intégration de méthodes formelles dans la conception des fonctions logicielles automobiles. (Doctoral Dissertation). université Paris-Saclay. Retrieved from http://www.theses.fr/2020UPASG026

Chicago Manual of Style (16^th Edition):

Todorov, Vassil. “Automotive embedded software design using formal methods : Intégration de méthodes formelles dans la conception des fonctions logicielles automobiles.” 2020. Doctoral Dissertation, université Paris-Saclay. Accessed February 28, 2021. http://www.theses.fr/2020UPASG026.

MLA Handbook (7^th Edition):

Todorov, Vassil. “Automotive embedded software design using formal methods : Intégration de méthodes formelles dans la conception des fonctions logicielles automobiles.” 2020. Web. 28 Feb 2021.

Vancouver:

Todorov V. Automotive embedded software design using formal methods : Intégration de méthodes formelles dans la conception des fonctions logicielles automobiles. [Internet] [Doctoral dissertation]. université Paris-Saclay; 2020. [cited 2021 Feb 28]. Available from: http://www.theses.fr/2020UPASG026.

Council of Science Editors:

Todorov V. Automotive embedded software design using formal methods : Intégration de méthodes formelles dans la conception des fonctions logicielles automobiles. [Doctoral Dissertation]. université Paris-Saclay; 2020. Available from: http://www.theses.fr/2020UPASG026

Université de Grenoble

5. Muhammad, Humayoun. Développement du système MathNat pour la formalisation automatique des textes mathématiques : Developing System MathNat for Automatic Formalization of Mathematical texts.

Degree: Docteur es, Mathématiques, 2012, Université de Grenoble

URL: http://www.theses.fr/2012GRENM001

► Le langage mathématique courant et les langages mathématiques formelssont très éloignés. Par <<langage mathématique courant>> nousentendons la prose que le mathématicien utilise tous les jours… (more)

▼ Le langage mathématique courant et les langages mathématiques formelssont très éloignés. Par <<langage mathématique courant>> nousentendons la prose que le mathématicien utilise tous les jours dansses articles et ses livres. C'est une langue naturelle avec desexpressions symboliques et des notations spécifiques. Cette langue està la fois flexible et structurée mais reste sémantiquementintelligible par tous les mathématiciens.Cependant, il est très difficile de formaliser automatiquement cettelangue. Les raisons principales sont: la complexité et l'ambiguïté deslangues naturelles en général, le mélange inhabituel entre languenaturelle et notations symboliques tout aussi ambiguë et les sautsdans le raisonnement qui sont pour l'instant bien au-delà descapacités des prouveurs de théorèmes automatiques ou interactifs.Pour contourner ce problème, les assistants de preuves actuelsutilisent des langages formels précis dans un système logique biendéterminé, imposant ainsi de fortes restrictions par rapport auxlangues naturelles. En général ces langages ressemblent à des langagesde programmation avec un nombre limité de constructions possibles etune absence d'ambiguïté.Ainsi, le monde des mathématiques est séparé en deux, la vastemajorité qui utilise la langue naturelle et un petit nombre utilisantaussi des méthodes formelles. Cette seconde communauté est elle-mêmesubdivisée en autant de groupes qu'il y a d'assistants de preuves. Onperd alors l'intelligibilité des preuves pour tous les mathématiciens.Pour résoudre ce problème, on peut se demander:est-il possible d'écrire un programme qui comprend la langue naturellemathématique et qui la traduit vers un langage formel afin depermettre sa validation?Ce problème se subdivise naturellement en deux sous-problèmes tous lesdeux très difficiles:1. l'analyse grammaticale des textes mathématiques et leur traductiondans un langage formel,2. la validation des preuves écrites dans ce langage formel.Le but du projet MathNat (Mathematics in controlled Natural languages)est de faire un premier pas pour répondre à cette question trèsdifficile, en se concentrant essentiellement sur la première question.Pour cela, nous développons CLM (Controlled Language for Mathematics)qui est un sous-ensemble de l'anglais avec une grammaire et un lexiquerestreint, mais qui inclut tout de même quelques ingrédientsimportants des langues naturelles comme les pronoms anaphoriques, lesréférences, la possibilité d'écrire la même chose de plusieursmanières, des adjectifs distributifs ou non, ...Le second composant de MathNath est MathAbs (Mathematical Abstractlanguage). C'est un langage formel, indépendant du choix d'un systèmelogique permettant de représenter la sémantique des textes enpréservant leur structure et le fil du raisonnement. MathAbs est conçucomme un langage intermédiaire entre CLM et un système logique formelpermettant la vérification des preuves.Nous proposons un système qui permet de traduire CLM vers MathAbsdonnant ainsi une sémantique précise à CLM. Nous considèrons que cetravail est déjà un… Advisors/Committee Members: Raffalli, Christophe (thesis director), Ranta, Aarne (thesis director).

Subjects/Keywords: Linguistique informatique; Langage contrôlé; Systèmes formels; Vérification de preuves; Computational linguistics; Language technology; Controlled languages; The language of mathematics; Formalization; Formal systems; Validation; Proof checking

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Muhammad, H. (2012). Développement du système MathNat pour la formalisation automatique des textes mathématiques : Developing System MathNat for Automatic Formalization of Mathematical texts. (Doctoral Dissertation). Université de Grenoble. Retrieved from http://www.theses.fr/2012GRENM001

Chicago Manual of Style (16^th Edition):

Muhammad, Humayoun. “Développement du système MathNat pour la formalisation automatique des textes mathématiques : Developing System MathNat for Automatic Formalization of Mathematical texts.” 2012. Doctoral Dissertation, Université de Grenoble. Accessed February 28, 2021. http://www.theses.fr/2012GRENM001.

MLA Handbook (7^th Edition):

Muhammad, Humayoun. “Développement du système MathNat pour la formalisation automatique des textes mathématiques : Developing System MathNat for Automatic Formalization of Mathematical texts.” 2012. Web. 28 Feb 2021.

Vancouver:

Muhammad H. Développement du système MathNat pour la formalisation automatique des textes mathématiques : Developing System MathNat for Automatic Formalization of Mathematical texts. [Internet] [Doctoral dissertation]. Université de Grenoble; 2012. [cited 2021 Feb 28]. Available from: http://www.theses.fr/2012GRENM001.

Council of Science Editors:

Muhammad H. Développement du système MathNat pour la formalisation automatique des textes mathématiques : Developing System MathNat for Automatic Formalization of Mathematical texts. [Doctoral Dissertation]. Université de Grenoble; 2012. Available from: http://www.theses.fr/2012GRENM001

6. Davis, Jared Curran. A self-verifying theorem prover.

Degree: PhD, Computer Sciences, 2009, University of Texas – Austin

URL: http://hdl.handle.net/2152/ETD-UT-2009-12-435

► Programs have precise semantics, so we can use mathematical proof to establish their properties. These proofs are often too large to validate with the usual… (more)

▼ Programs have precise semantics, so we can use mathematical proof to establish their properties. These proofs are often too large to validate with the usual "social process" of mathematics, so instead we create and check them with theorem-proving software. This software must be advanced enough to make the proof process tractable, but this very sophistication casts doubt upon the whole enterprise: who verifies the verifier? We begin with a simple proof checker, Level 1, that only accepts proofs composed of the most primitive steps, like Instantiation and Cut. This program is so straightforward the ordinary, social process can establish its soundness and the consistency of the logical theory it implements (so we know theorems are "always true"). Next, we develop a series of increasingly capable proof checkers, Level 2, Level 3, etc. Each new proof checker accepts new kinds of proof steps which were not accepted in the previous levels. By taking advantage of these new proof steps, higher-level proofs can be written more concisely than lower-level proofs, and can take less time to construct and check. Our highest-level proof checker, Level 11, can be thought of as a simplified version of the ACL2 or NQTHM theorem provers. One contribution of this work is to show how such systems can be verified. To establish that the Level 11 proof checker can be trusted, we first use it, without trusting it, to prove the fidelity of every Level n to Level 1: whenever Level n accepts a proof of some phi, there exists a Level 1 proof of phi. We then mechanically translate the Level 11 proof for each Level n into a Level n - 1 proof – that is, we create a Level 1 proof of Level 2's fidelity, a Level 2 proof of Level 3's fidelity, and so on. This layering shows that each level can be trusted, and allows us to manage the sizes of these proofs. In this way, our system proves its own fidelity, and trusting Level 11 only requires us to trust Level 1. Advisors/Committee Members: Moore, J Strother, 1947- (advisor), Emerson, E. Allen (committee member), Harrison, John (committee member), Hunt, Jr., Warren A. (committee member), Kaufmann, Matt (committee member), Lifschitz, Vladimir (committee member).

Subjects/Keywords: Milawa; mathematical logic; formal verification; Lisp; proof checking; theorem proving; automated reasoning; reflection; soundness; fidelity; faithfulness; rewriting; proof building; tactics; first-order logic; verified verifier

…Terms . . . . . Formulas . . . . Appeals . . . . Step Checking . Proof Checking Provability… …Proof-Checking Support Rewriter Debugging . . Parallelism… …format makes checking each individual step of a formal proof quite easy, which allows proof… …the proof has been constructed, we check it with our simple proof-checking program, on a… …statement is true from the engineering task of constructing and checking such a large formal proof…

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Davis, J. C. (2009). A self-verifying theorem prover. (Doctoral Dissertation). University of Texas – Austin. Retrieved from http://hdl.handle.net/2152/ETD-UT-2009-12-435

Chicago Manual of Style (16^th Edition):

Davis, Jared Curran. “A self-verifying theorem prover.” 2009. Doctoral Dissertation, University of Texas – Austin. Accessed February 28, 2021. http://hdl.handle.net/2152/ETD-UT-2009-12-435.

MLA Handbook (7^th Edition):

Davis, Jared Curran. “A self-verifying theorem prover.” 2009. Web. 28 Feb 2021.

Vancouver:

Davis JC. A self-verifying theorem prover. [Internet] [Doctoral dissertation]. University of Texas – Austin; 2009. [cited 2021 Feb 28]. Available from: http://hdl.handle.net/2152/ETD-UT-2009-12-435.

Council of Science Editors:

Davis JC. A self-verifying theorem prover. [Doctoral Dissertation]. University of Texas – Austin; 2009. Available from: http://hdl.handle.net/2152/ETD-UT-2009-12-435

University of Queensland

7. Watson, Geoffrey Norman. A Generic Proof Checker.

Degree: School of Computer Science and Electrical Engineering, 2001, University of Queensland

URL: http://espace.library.uq.edu.au/view/UQ:10603

► The use of formal methods in software development seeks to increase our confidence in the resultant system. Their use often requires tool support, so the… (more)

▼ The use of formal methods in software development seeks to increase our confidence in the resultant system. Their use often requires tool support, so the integrity of a development using formal methods is dependent on the integrity of the tool-set used. Specifically its integrity depends on the theorem prover, since in a typical formal development system the theorem prover is used to establish the validity of the proof obligations incurred by all the steps in the design and refinement process. In this thesis we are concerned with tool-based formal development systems that are used to develop high-integrity software. Since the theorem prover program is a critical part of such a system, it should ideally have been itself formally verified. Unfortunately, most theorem provers are too complex to be verified formally using currently available techniques. An alternative approach, which has many advantages, is to include a proof checker as an extra component in the system, and to certify this. A proof checker is a program which reads and checks the proofs produced by a theorem prover. Proof checkers are inherently simpler than theorem provers, since they only process actual proofs, whereas much of the code of a theorem prover is concerned with searching the space of possible proofs to find the required one. They are also free from all but the simplest user interface concerns, since their input is a proof produced by another program, and their output may be as simple as a `yes/no' reply to the question: Is this a valid proof? plus a list of assumptions on which this judgement is based. When included in a formal development system a stand-alone proof checker is, in one sense, superfluous, since it does not produce any proofs – the theorem prover does this. Instead its importance is in establishing the integrity of the results of the system – it provides extra assurance. A proof checker provides extra assurance simply by checking the proofs, since all proofs have then been validated by two independent programs. However a proof checker can provide an extra, and higher, level of assurance if it has been formally verified. In order for formal verification to be feasible the proof checker must be as simple as possible. In turn the simplicity of a proof checker is dependent on the complexity of the data which it processes, that is, the representation of the proofs that it checks. This thesis develops a representation of proofs that is simple and generic. The aim is to produce a generic representation that is applicable to the proofs produced by a variety of theorem provers. Simplicity facilitates verification, while genericity maximises the return on the effort of verification. Using a generic representation places obligations on the theorem provers to produce a proof record in this format. A flexible recorder/translator architecture is proposed which allows proofs to be recorded by existing theorem provers with minimal changes to the original code. The prover is extended with a recorder module whose output is then, if necessary,…

Subjects/Keywords: Software verification; theorem proving; proof checking; 280403 Logics and Meanings of Programs; 280499 Computation Theory and Mathematics not elsewhere classified; 700102 Application tools and system utilities

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Watson, G. N. (2001). A Generic Proof Checker. (Thesis). University of Queensland. Retrieved from http://espace.library.uq.edu.au/view/UQ:10603

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

Watson, Geoffrey Norman. “A Generic Proof Checker.” 2001. Thesis, University of Queensland. Accessed February 28, 2021. http://espace.library.uq.edu.au/view/UQ:10603.

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

MLA Handbook (7^th Edition):

Watson, Geoffrey Norman. “A Generic Proof Checker.” 2001. Web. 28 Feb 2021.

Vancouver:

Watson GN. A Generic Proof Checker. [Internet] [Thesis]. University of Queensland; 2001. [cited 2021 Feb 28]. Available from: http://espace.library.uq.edu.au/view/UQ:10603.

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

Council of Science Editors:

Watson GN. A Generic Proof Checker. [Thesis]. University of Queensland; 2001. Available from: http://espace.library.uq.edu.au/view/UQ:10603

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

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

Open Access Theses and Dissertations