subject:(Model checking)

Università della Svizzera italiana

1. de Sá Alt, Leonardo. Controlled and effective interpolation.

Degree: 2016, Università della Svizzera italiana

► Model checking is a well established technique to verify systems, exhaustively and automatically. The state space explosion, known as the main difficulty in model checking… (more)

▼ Model checking is a well established technique to verify systems, exhaustively and automatically. The state space explosion, known as the main difficulty in model checking scalability, has been successfully approached by symbolic model checking which represents programs using logic, usually at the propositional or first order theories level. Craig interpolation is one of the most successful abstraction techniques used in symbolic methods. Interpolants can be efficiently generated from proofs of unsatisfiability, and have been used as means of over-approximation to generate inductive invariants, refinement predicates, and function summaries. However, interpolation is still not fully understood. For several theories it is only possible to generate one interpolant, giving the interpolation-based application no chance of further optimization via interpolation. For the theories that have interpolation systems that are able to generate different interpolants, it is not understood what makes one interpolant better than another, and how to generate the most suitable ones for a particular verification task. The goal of this thesis is to address the problems of how to generate multiple interpolants for theories that still lack this flexibility in their interpolation algorithms, and how to aim at good interpolants. This thesis extends the state-of-the-art by introducing novel interpolation frameworks for different theories. For propositional logic, this work provides a thorough theoretical analysis showing which properties are desirable in a labeling function for the Labeled Interpolation Systems framework (LIS). The Proof-Sensitive labeling function is presented, and we prove that it generates interpolants with the smallest number of Boolean connectives in the entire LIS framework. Two variants that aim at controlling the logical strength of propositional interpolants while maintaining a small size are given. The new interpolation algorithms are compared to previous ones from the literature in different model checking settings, showing that they consistently lead to a better overall verification performance. The Equalities and Uninterpreted Functions (EUF)-interpolation system, presented in this thesis, is a duality-based interpolation framework capable of generating multiple interpolants for a single proof of unsatisfiability, and provides control over the logical strength of the interpolants it generates using labeling functions. The labeling functions can be theoretically compared with respect to their strength, and we prove that two of them generate the interpolants with the smallest number of equalities. Our experiments follow the theory, showing that the generated interpolants indeed have different logical strength. We combine propositional and EUF interpolation in a model checking setting, and show that the strength of the interpolation algorithms for different theories has to be aligned in order to generate smaller interpolants. This work also introduces the Linear Real Arithmetic (LRA)-interpolation system, an… Advisors/Committee Members: Natasha (Dir.).

Subjects/Keywords: Model checking

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

de Sá Alt, L. (2016). Controlled and effective interpolation. (Thesis). Università della Svizzera italiana. Retrieved from http://doc.rero.ch/record/309121

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

de Sá Alt, Leonardo. “Controlled and effective interpolation.” 2016. Thesis, Università della Svizzera italiana. Accessed January 19, 2020. http://doc.rero.ch/record/309121.

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

MLA Handbook (7^th Edition):

de Sá Alt, Leonardo. “Controlled and effective interpolation.” 2016. Web. 19 Jan 2020.

Vancouver:

de Sá Alt L. Controlled and effective interpolation. [Internet] [Thesis]. Università della Svizzera italiana; 2016. [cited 2020 Jan 19]. Available from: http://doc.rero.ch/record/309121.

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

Council of Science Editors:

de Sá Alt L. Controlled and effective interpolation. [Thesis]. Università della Svizzera italiana; 2016. Available from: http://doc.rero.ch/record/309121

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

2. Pellegrino, Giancarlo. Détection d'anomalies logiques dans les logiciels d'entreprise multi-partis à travers des tests de sécurité : Detection of logic flaws in multi-party business applications via security testing.

Degree: Docteur es, Informatique et réseaux, 2013, Paris, ENST

URL: http://www.theses.fr/2013ENST0064

►

Les logiciels multi-partis sont des applications distribuées sur le web qui mettent en oeuvre des fonctions collaboratives. Ces applications sont les principales cibles des attaquants… (more)

▼

Les logiciels multi-partis sont des applications distribuées sur le web qui mettent en oeuvre des fonctions collaboratives. Ces applications sont les principales cibles des attaquants qui exploitent des vulnérabilités logicielles dans le cadre d'activités malveillantes. Récemment, un type moins connu de vulnérabilité, les anomalies logiques, a attiré l'attention des chercheurs. Sur la base d'informations tirées de la documentation des applications, il est possible d'appliquer deux techniques de test: la vérification du modèle, autrement appelé ``model checking'', et les tests de sécurité de type ``boîte noire''. Le champs d'application du model checking ne prend pas en suffisamment en compte les implémentations actuelles, tandis que les tests de type boîte noire ne sont pas assez sophistiqués pour découvrir les vulnérabilités logique. Dans cette thèse, nous présentons deux techniques d'analyse modernes visant à résoudre les inconvénients de l'état de l'art. Pour commencer, nous présentons la vérification de deux protocoles de sécurité utilisant la technique du model checking. Ensuite, nous nous concentrons sur l'extension du model checking pour soutenir les tests automatisés d'implémentations. La seconde technique consiste en une analyse boîte noire qui combine l'inférence du modèle, l'extraction du processus et du flot de donnée, ainsi qu'une génération de tests basés sur les modèles d'attaque d'une application. En conclusion, nous discutons de l'application de techniques développées au cours de cette thèse sur des applications issues d'un contexte industrielle.

Multi-party business applications are distributed computer programs implementing collaborative business functions. These applications are one of the main target of attackers who exploit vulnerabilities in order to perform malicious activities. The most prevalent classes of vulnerabilities are the consequence of insufficient validation of the user-provided input. However, the less-known class of logic vulnerabilities recently attracted the attention of researcher. According to the availability of software documentation, two testing techniques can be used: design verification via model checking, and black-box security testing. However, the former offers no support to test real implementations and the latter lacks the sophistication to detect logic flaws. In this thesis, we present two novel security testing techniques to detect logic flaws in multi-party business applicatons that tackle the shortcomings of the existing techniques. First, we present the verification via model checking of two security protocols. We then address the challenge of extending the results of the model checker to automatically test protocol implementations. Second, we present a novel black-box security testing technique that combines model inference, extraction of workflow and data flow patterns, and an attack pattern-based test case generation algorithm. Finally, we discuss the application of the technique developed in this thesis in an industrial setting. We used these techniques…

Advisors/Committee Members: Balzarotti, Davide (thesis director).

Subjects/Keywords: Authentification unique; Model checking; SSO; Model checking

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Pellegrino, G. (2013). Détection d'anomalies logiques dans les logiciels d'entreprise multi-partis à travers des tests de sécurité : Detection of logic flaws in multi-party business applications via security testing. (Doctoral Dissertation). Paris, ENST. Retrieved from http://www.theses.fr/2013ENST0064

Chicago Manual of Style (16^th Edition):

Pellegrino, Giancarlo. “Détection d'anomalies logiques dans les logiciels d'entreprise multi-partis à travers des tests de sécurité : Detection of logic flaws in multi-party business applications via security testing.” 2013. Doctoral Dissertation, Paris, ENST. Accessed January 19, 2020. http://www.theses.fr/2013ENST0064.

MLA Handbook (7^th Edition):

Pellegrino, Giancarlo. “Détection d'anomalies logiques dans les logiciels d'entreprise multi-partis à travers des tests de sécurité : Detection of logic flaws in multi-party business applications via security testing.” 2013. Web. 19 Jan 2020.

Vancouver:

Pellegrino G. Détection d'anomalies logiques dans les logiciels d'entreprise multi-partis à travers des tests de sécurité : Detection of logic flaws in multi-party business applications via security testing. [Internet] [Doctoral dissertation]. Paris, ENST; 2013. [cited 2020 Jan 19]. Available from: http://www.theses.fr/2013ENST0064.

Council of Science Editors:

Pellegrino G. Détection d'anomalies logiques dans les logiciels d'entreprise multi-partis à travers des tests de sécurité : Detection of logic flaws in multi-party business applications via security testing. [Doctoral Dissertation]. Paris, ENST; 2013. Available from: http://www.theses.fr/2013ENST0064

Brno University of Technology

3. Chalk, Matěj. Nástroj pro abstraktní regulární model checking .

Degree: 2018, Brno University of Technology

URL: http://hdl.handle.net/11012/84907

► Metody formální verifikace mohou poskytnout automatizované ověření korektnosti softwaru (stavěné na matematických základech), což je velmi důležité. Jednou z těchto metod je abstraktní regulární model… (more)

▼ Metody formální verifikace mohou poskytnout automatizované ověření korektnosti softwaru (stavěné na matematických základech), což je velmi důležité. Jednou z těchto metod je abstraktní regulární model checking, jenž používá konečné automaty a převodníky pro reprezentaci množiny dosažitelných konfigurací, respektive jednokrokového přechodu mezi těmito konfiguracemi. Přestože tato metoda řeší obecně nerozhodnutelné problémy, umožňuje terminaci v mnoha praktických případech a navíc výrazně zmírňuje problém stavové exploze. Tohoto dosahuje urychlením výpočtu dosažitelných stavů pomocí inkrementálního zjemňování abstrakcí, k odstranění neplatných protipříkladů vzniklých nadaproximací pak slouží technika zjemňování abstrakce založená na protipříkladech. Cílem této práce je vytvořit dobře navržený nástroj pro abstraktní regulární model checking, jenž byl dosud implementován pouze v prototypech. Nový nástroj bude systémy modelovat pomocí symbolických automatů a převodníků namísto jejich (méně stručných) klasických alternativ.; Formal verification methods offer a large potential to provide automated software correctness checking (based on sound mathematical roots), which is of vital importance. One such technique is abstract regular model checking, which encodes sets of reachable configurations and one-step transitions between them using finite automata and transducers, respectively. Though this method addresses problems that are undecidable in general, it facilitates termination in many practical cases, while also significantly reducing the state space explosion problem. This is achieved by accelerating the computation of reachability sets using incrementally refinable abstractions, while eliminating spurious counterexamples caused by overapproximation using a counterexample-guided abstraction refinement technique. The aim of this thesis is to create a well designed tool for abstract regular model checking, which has so far only been implemented in prototypes. The new tool will model systems using symbolic automata and transducers instead of their (less concise) classic alternatives. Advisors/Committee Members: Hruška, Martin (advisor).

Subjects/Keywords: formální verifikace; model checking; regulární model checking; abstraktní regulární model checking; automaty; převodníky; symbolické automaty; formal verification; model checking; regular model checking; abstract regular model checking; automata; transducers; symbolic automata

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Chalk, M. (2018). Nástroj pro abstraktní regulární model checking . (Thesis). Brno University of Technology. Retrieved from http://hdl.handle.net/11012/84907

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

Chalk, Matěj. “Nástroj pro abstraktní regulární model checking .” 2018. Thesis, Brno University of Technology. Accessed January 19, 2020. http://hdl.handle.net/11012/84907.

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

MLA Handbook (7^th Edition):

Chalk, Matěj. “Nástroj pro abstraktní regulární model checking .” 2018. Web. 19 Jan 2020.

Vancouver:

Chalk M. Nástroj pro abstraktní regulární model checking . [Internet] [Thesis]. Brno University of Technology; 2018. [cited 2020 Jan 19]. Available from: http://hdl.handle.net/11012/84907.

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

Council of Science Editors:

Chalk M. Nástroj pro abstraktní regulární model checking . [Thesis]. Brno University of Technology; 2018. Available from: http://hdl.handle.net/11012/84907

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

Université Catholique de Louvain

4. Nauw, Olivier. A framework for visualizing and manipulating structured execution graphs.

Degree: 2015, Université Catholique de Louvain

URL: http://hdl.handle.net/2078.1/thesis:3128

►

Ce travail présente un outil qui permet d'afficher et de manipuler des graphes d’exécutions structurées. Ceux-ci représentent des chemins possibles dans un système et ils… (more)

Subjects/Keywords: Graphes; Model Checking; Visualisation

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Nauw, O. (2015). A framework for visualizing and manipulating structured execution graphs. (Thesis). Université Catholique de Louvain. Retrieved from http://hdl.handle.net/2078.1/thesis:3128

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

Nauw, Olivier. “A framework for visualizing and manipulating structured execution graphs.” 2015. Thesis, Université Catholique de Louvain. Accessed January 19, 2020. http://hdl.handle.net/2078.1/thesis:3128.

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

MLA Handbook (7^th Edition):

Nauw, Olivier. “A framework for visualizing and manipulating structured execution graphs.” 2015. Web. 19 Jan 2020.

Vancouver:

Nauw O. A framework for visualizing and manipulating structured execution graphs. [Internet] [Thesis]. Université Catholique de Louvain; 2015. [cited 2020 Jan 19]. Available from: http://hdl.handle.net/2078.1/thesis:3128.

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

Council of Science Editors:

Nauw O. A framework for visualizing and manipulating structured execution graphs. [Thesis]. Université Catholique de Louvain; 2015. Available from: http://hdl.handle.net/2078.1/thesis:3128

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

Virginia Tech

5. Adhikari, Kiran. Verifying a Quantitative Relaxation of Linearizability via Refinement.

Degree: MS, Electrical and Computer Engineering, 2013, Virginia Tech

URL: http://hdl.handle.net/10919/23222

► Concurrent data structures have found increasingly widespread use in both multicore and distributed computing environments, thereby escalating the priority for verifying their correctness. The thread… (more)

Subjects/Keywords: Quasi Linearizability; Refinement; Model Checking

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Adhikari, K. (2013). Verifying a Quantitative Relaxation of Linearizability via Refinement. (Masters Thesis). Virginia Tech. Retrieved from http://hdl.handle.net/10919/23222

Chicago Manual of Style (16^th Edition):

Adhikari, Kiran. “Verifying a Quantitative Relaxation of Linearizability via Refinement.” 2013. Masters Thesis, Virginia Tech. Accessed January 19, 2020. http://hdl.handle.net/10919/23222.

MLA Handbook (7^th Edition):

Adhikari, Kiran. “Verifying a Quantitative Relaxation of Linearizability via Refinement.” 2013. Web. 19 Jan 2020.

Vancouver:

Adhikari K. Verifying a Quantitative Relaxation of Linearizability via Refinement. [Internet] [Masters thesis]. Virginia Tech; 2013. [cited 2020 Jan 19]. Available from: http://hdl.handle.net/10919/23222.

Council of Science Editors:

Adhikari K. Verifying a Quantitative Relaxation of Linearizability via Refinement. [Masters Thesis]. Virginia Tech; 2013. Available from: http://hdl.handle.net/10919/23222

6. Kang, Eun-Young. Abstractions booléennes pour la vérification des systèmes temps-réel : Tools supported real-time system verification with combination of abstraction/deduction and Model checking.

Degree: Docteur es, Informatique, 2007, Université Henri Poincaré – Nancy I

URL: http://www.theses.fr/2007NAN10089

►

Cette thèse présente un schéma formel et efficace pour la vérification de systèmes temps-réel. Ce schéma repose sur la combinaison par abstraction de techniques déductives… (more)

▼

Cette thèse présente un schéma formel et efficace pour la vérification de systèmes temps-réel. Ce schéma repose sur la combinaison par abstraction de techniques déductives et de model checking, et cette combinaison permet de contourner les limites de chacune de ces techniques. La méthode utilise le raffinement itératif abstrait (IAR) pour le calcul d'abstractions finies. Etant donné un système de transitions et un ensemble fini de prédicats, la méthode détermine une abstraction booléenne dont les états correspondent à des ensembles de prédicats. La correction de l'abstraction par rapport au système d'origine est garantie en établissant un ensemble de conditions de vérification, issues de la procédure IAR. Ces conditions sont à démontrer à l'aide d'un prouveur de théorèmes. Les propriétés de sûreté et de vivacité sont ensuite vérifiées par rapport au modèle abstrait. La procédure IAR termine lorsque toutes les conditions sont vérifiées. Dans le cas contraire, une analyse plus fine détermine si le modèle abstrait doit être affiné en considérant davantage de prédicats. Nous identifions une classe de diagrammes de prédicats appelés PDT (predicate diagram for timed system) qui décrivent l'abstraction et qui peuvent être utilisés pour la vérification de systèmes temporisés et paramétrés.

This thesis provides an efficient formal scheme for the tool-supported real-time system verification by combination of abstraction-based deductive and model checking techniques in order to handle the limitations of the applied verification techniques. This method is based on IAR (Iterative Abstract Refinement) to compute finite state abstractions. Given a transition system and a finite set of predicates, this method determines a finite abstraction, where each state of the abstract state space is a true assignment to the abstraction predicates. A theorem prover can be used to verify that the finite abstract model is a correct abstraction of a given system by checking conformance between an abstract and a concrete model by establishing/proving that a set of verification conditions are obtained during the IAR procedure. Then the safety/liveness properties are checked over the abstract model. If the verification condition holds successfully, IAR terminates its procedure. Otherwise more analysis is applied to identify if the abstract model needs to be more precise by adding extra predicates. As abstraction form, we adopt a class of predicate diagrams and define a variant of predicate diagram PDT (Predicate Diagram for Timed systems) that can be used to verify real-time and parameterized systems.

Advisors/Committee Members: Merz, Stephan (thesis director).

Subjects/Keywords: Model checking

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Kang, E. (2007). Abstractions booléennes pour la vérification des systèmes temps-réel : Tools supported real-time system verification with combination of abstraction/deduction and Model checking. (Doctoral Dissertation). Université Henri Poincaré – Nancy I. Retrieved from http://www.theses.fr/2007NAN10089

Chicago Manual of Style (16^th Edition):

Kang, Eun-Young. “Abstractions booléennes pour la vérification des systèmes temps-réel : Tools supported real-time system verification with combination of abstraction/deduction and Model checking.” 2007. Doctoral Dissertation, Université Henri Poincaré – Nancy I. Accessed January 19, 2020. http://www.theses.fr/2007NAN10089.

MLA Handbook (7^th Edition):

Kang, Eun-Young. “Abstractions booléennes pour la vérification des systèmes temps-réel : Tools supported real-time system verification with combination of abstraction/deduction and Model checking.” 2007. Web. 19 Jan 2020.

Vancouver:

Kang E. Abstractions booléennes pour la vérification des systèmes temps-réel : Tools supported real-time system verification with combination of abstraction/deduction and Model checking. [Internet] [Doctoral dissertation]. Université Henri Poincaré – Nancy I; 2007. [cited 2020 Jan 19]. Available from: http://www.theses.fr/2007NAN10089.

Council of Science Editors:

Kang E. Abstractions booléennes pour la vérification des systèmes temps-réel : Tools supported real-time system verification with combination of abstraction/deduction and Model checking. [Doctoral Dissertation]. Université Henri Poincaré – Nancy I; 2007. Available from: http://www.theses.fr/2007NAN10089

University of Waterloo

7. Taleghani, Ali. Using Software Model Checking for Software Certification.

Degree: 2010, University of Waterloo

URL: http://hdl.handle.net/10012/5484

► Software certification is defined as the process of independently confirming that a system or component complies with its specified requirements and is acceptable for use.… (more)

▼ Software certification is defined as the process of independently confirming that a system or component complies with its specified requirements and is acceptable for use. It consists of the following steps: (1) the software producer subjects her software to rigorous testing and submits for certification, among other documents, evidence that the software has been thoroughly verified, and (2) the certifier evaluates the completeness of the verification and confirms that the software meets its specifications. The certification process is typically a manual evaluation of thousands of pages of documents that the software producer submits. Moreover, most of the current certification techniques focus on certifying testing results, but there is an increase in using formal methods to verify software. Model checking is a formal verification method that systematically explores the entire execution state space of a software program to ensure that a property is satisfied in every program state. As the field of model checking matures, there is a growing interest in its use for verification. In fact, several industrial-sized software projects have used model checking for verification, and there has been an increased push for techniques, preferably automated, to certify model checking results. Motivated by these challenges in certification, we have developed a set of automated techniques to certify model-checking results. One technique, called search-carrying code (SCC), uses information collected by a model checker during the verification of a program to speed up the certification of that program. In SCC, the software producer's model checker performs an exhaustive search of a program's state space and creates a search script that acts as a certificate of verification. The certifier's model checker uses the search script to partition its search task into a number of smaller, roughly balanced tasks that can be distributed to parallel model checkers, thereby using parallelization to speed up certification. When memory resources are limited, the producer's model checker can reduce its memory requirements by caching only a subset of the model-checking-search results. Caching increases the likelihood that an SCC verification task runs to completion and produces a search script that represents the program's entire state space. The downside of caching is that it can result in an increase in search time. We introduce cost-based caching, that achieves an exhaustive search faster than existing caching techniques. Finally, for cases when an exhaustive search is not possible, we present a novel method for estimating the state-space coverage of a partial model checking run. The coverage estimation can help the certifier to determine whether the partial model-checking results are adequate for certification.

Subjects/Keywords: Model Checking; Software Certification

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Taleghani, A. (2010). Using Software Model Checking for Software Certification. (Thesis). University of Waterloo. Retrieved from http://hdl.handle.net/10012/5484

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

Taleghani, Ali. “Using Software Model Checking for Software Certification.” 2010. Thesis, University of Waterloo. Accessed January 19, 2020. http://hdl.handle.net/10012/5484.

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

MLA Handbook (7^th Edition):

Taleghani, Ali. “Using Software Model Checking for Software Certification.” 2010. Web. 19 Jan 2020.

Vancouver:

Taleghani A. Using Software Model Checking for Software Certification. [Internet] [Thesis]. University of Waterloo; 2010. [cited 2020 Jan 19]. Available from: http://hdl.handle.net/10012/5484.

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

Council of Science Editors:

Taleghani A. Using Software Model Checking for Software Certification. [Thesis]. University of Waterloo; 2010. Available from: http://hdl.handle.net/10012/5484

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

Princeton University

8. Ahn, Sunha. AUTOMATED FIRMWARE VERIFICATION USING FIRMWARE-HARDWARE INTERACTION PATTERNS .

Degree: PhD, 2016, Princeton University

URL: http://arks.princeton.edu/ark:/88435/dsp01s4655k00v

► Firmware refers to low-level software that is tied to a specific hardware platform. For instance, low-level drivers that physically interface with the peripherals are an… (more)

▼ Firmware refers to low-level software that is tied to a specific hardware platform. For instance, low-level drivers that physically interface with the peripherals are an example of firmware. An emerging trend in system design is to implement complex system management functions in firmware rather than hardware. For example, firmware has grown to include software that manages critical hardware platform functions such as power management. As the scale and the importance of firmware is increasing, its validation becomes a critical part of system validation. Firmware validation relies on having good models of the interacting hardware components because firmware needs to be shipped with the hardware and shares many of the same critical design concerns as the hardware. This is generally addressed through co-simulating C/C++ based firmware code and HDL~(including SystemC) hardware models, which are usually not available until the late design stages. However, co-simulation tends to be slow, and is further exacerbated by the large number of possible interleavings between the concurrent firmware and hardware threads. Typically, in co-simulation, the thread scheduler, such as the SystemC scheduler, only explores a small number of possible firmware-hardware interleavings and thus may miss critical bugs. A firmware function is mostly reactive: it continuously provides a service, with a clear start and end, in response to inputs from its interacting software or hardware layer~(i.e., the environment). Thus, a firmware function is often inherently associated with an infinite loop structure. This often makes it impossible to guarantee the completeness of the verification results. To this end, I address two key problems in this thesis. First, I describe how to co-design firmware with the system components at the service function level, also referred to as the transaction level. Second, I discuss how to validate firmware interactions with their connected hardware modules while pruning the verification search space and ensuring complete verification. To solve these problems, this thesis first introduces a specific Service-Function Transaction-Level Model (TLM) for modeling firmware and interacting hardware components. I capture the particular structure of the proposed TLMs through cross-transaction interaction patterns, such as statelessness, i.e., when variable values are not retained between transaction executions, or producer-consumer relationships. Using the TLM, this thesis presents a scalable firmware validation approach that is based on automatically generating a test set with the goal of complete path coverage for firmware. Instead of explicitly exploring all the interleavings of the concurrent transactions, this thesis exploits the interaction patterns to automatically generate a sequential program, which is test-equivalent to the target firmware transaction and can be used with a standard single-threaded concolic test generator. The tests generated can… Advisors/Committee Members: Malik, Sharad (advisor).

Subjects/Keywords: Firmware; Model checking; Testing; Verifiation

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Ahn, S. (2016). AUTOMATED FIRMWARE VERIFICATION USING FIRMWARE-HARDWARE INTERACTION PATTERNS . (Doctoral Dissertation). Princeton University. Retrieved from http://arks.princeton.edu/ark:/88435/dsp01s4655k00v

Chicago Manual of Style (16^th Edition):

Ahn, Sunha. “AUTOMATED FIRMWARE VERIFICATION USING FIRMWARE-HARDWARE INTERACTION PATTERNS .” 2016. Doctoral Dissertation, Princeton University. Accessed January 19, 2020. http://arks.princeton.edu/ark:/88435/dsp01s4655k00v.

MLA Handbook (7^th Edition):

Ahn, Sunha. “AUTOMATED FIRMWARE VERIFICATION USING FIRMWARE-HARDWARE INTERACTION PATTERNS .” 2016. Web. 19 Jan 2020.

Vancouver:

Ahn S. AUTOMATED FIRMWARE VERIFICATION USING FIRMWARE-HARDWARE INTERACTION PATTERNS . [Internet] [Doctoral dissertation]. Princeton University; 2016. [cited 2020 Jan 19]. Available from: http://arks.princeton.edu/ark:/88435/dsp01s4655k00v.

Council of Science Editors:

Ahn S. AUTOMATED FIRMWARE VERIFICATION USING FIRMWARE-HARDWARE INTERACTION PATTERNS . [Doctoral Dissertation]. Princeton University; 2016. Available from: http://arks.princeton.edu/ark:/88435/dsp01s4655k00v

University of Limerick

9. Pantelic, Vera. Inspection of concurrent systems: combining tables, theorem proving and model checking.

Degree: 2006, University of Limerick

URL: http://hdl.handle.net/10344/159

► A process for rigorous inspection of concurrent systems using tabular specification was developed and applied to the classic Readers/Writers concurrent program by Jin in [15].… (more)

Subjects/Keywords: model checking

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Pantelic, V. (2006). Inspection of concurrent systems: combining tables, theorem proving and model checking. (Thesis). University of Limerick. Retrieved from http://hdl.handle.net/10344/159

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

Pantelic, Vera. “Inspection of concurrent systems: combining tables, theorem proving and model checking.” 2006. Thesis, University of Limerick. Accessed January 19, 2020. http://hdl.handle.net/10344/159.

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

MLA Handbook (7^th Edition):

Pantelic, Vera. “Inspection of concurrent systems: combining tables, theorem proving and model checking.” 2006. Web. 19 Jan 2020.

Vancouver:

Pantelic V. Inspection of concurrent systems: combining tables, theorem proving and model checking. [Internet] [Thesis]. University of Limerick; 2006. [cited 2020 Jan 19]. Available from: http://hdl.handle.net/10344/159.

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

Council of Science Editors:

Pantelic V. Inspection of concurrent systems: combining tables, theorem proving and model checking. [Thesis]. University of Limerick; 2006. Available from: http://hdl.handle.net/10344/159

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

10. Bozianu, Rodica. Synthesis of Interactive Reactive Systems : Synthèse des systèmes réactifs interactifs.

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

URL: http://www.theses.fr/2016PESC1026

►

Nous étudions le problème de la synthèse automatique de programmes dans des architectures multi-composants tels qu'elles respectent les spécifications par construction. Le principal objectif de… (more)

▼

Nous étudions le problème de la synthèse automatique de programmes dans des architectures multi-composants tels qu'elles respectent les spécifications par construction. Le principal objectif de cette thèse est de développer des procédures pour résoudre le problème de synthèse qui peut conduire à des implémentations efficaces. Chaque composant a une observation partielle sur l'état global du système multi-composants. Le problème est alors de fournir des protocoles basés sur les observations tel que les composants synthétisés assurent les spécifications pour tout le comportement de leur environnement. L'environnement peut être antagoniste, ou peut avoir ses propres objectifs et se comporter de façon rationnelle. Nous étudions d'abord le problème de synthèse lorsque l'environnement est présumé antagoniste. Pour ce contexte, nous proposons une procédure "Safraless" pour la synthèse d'un composant partiellement informé et un environnement omniscient à partir de spécications KLTL+. Elle est implémentée dans l'outil Acacia-K. Ensuite, nous étudions le problème de synthèse lorsque les composants de l'environnement ont leurs propres objectifs et sont rationnels. Pour le cadre plus simple de l'information parfaite, nous fournissons des complexités serrées pour des objectifs omega-réguliers particuliers. Pour le cas de l'information imparfaite, nous prouvons que le problème de la synthèse rationnelle est indécidable en général, mais nous regagnons la décidabilité si on demande à synthétiser un composant avec observation partielle contre un environnement multi-composante, omniscient et rationnel

We study the problem of automatic synthesis of programs in multi-component architectures such that they satisfy the specifications by construction. The main goal of the thesis is to develop procedures to solve the synthesis problem that may lead to efficient implementations.Each component may have partial observation on the global state of the multi-component system.Therefore, the synthesis problem asks to provide observation-based protocols for the components that have to be synthesized that ensure that specifications hold on all interactions with their environment.The environment may be antagonist, or may have its own objectives and behave rationally.We first study the synthesis problem when the environment is presumed to be completely antagonist. For this setting, we propose a "Safraless" procedure for the synthesis of one partially informed component and an omniscient environment from KLTL+ specifications. It is implemented in the tool Acacia-K. Secondly, we study the synthesis problem when the components in the environment have their own objectives and are rational. For the more relaxed setting of perfect information, we provide tight complexities for particular omega-regular objectives. Then, for the case of imperfect information, we prove that the rational synthesis problem is undecidable in general, but we gain decidability if is asked to synthesize only one component against a rational omniscient environment

Advisors/Committee Members: Dima, Catalin (thesis director).

Subjects/Keywords: Synthèse; Model Checking; Verification; Jeux; Synthesis; Model Checking; Verification; Games

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Bozianu, R. (2016). Synthesis of Interactive Reactive Systems : Synthèse des systèmes réactifs interactifs. (Doctoral Dissertation). Université Paris-Est. Retrieved from http://www.theses.fr/2016PESC1026

Chicago Manual of Style (16^th Edition):

Bozianu, Rodica. “Synthesis of Interactive Reactive Systems : Synthèse des systèmes réactifs interactifs.” 2016. Doctoral Dissertation, Université Paris-Est. Accessed January 19, 2020. http://www.theses.fr/2016PESC1026.

MLA Handbook (7^th Edition):

Bozianu, Rodica. “Synthesis of Interactive Reactive Systems : Synthèse des systèmes réactifs interactifs.” 2016. Web. 19 Jan 2020.

Vancouver:

Bozianu R. Synthesis of Interactive Reactive Systems : Synthèse des systèmes réactifs interactifs. [Internet] [Doctoral dissertation]. Université Paris-Est; 2016. [cited 2020 Jan 19]. Available from: http://www.theses.fr/2016PESC1026.

Council of Science Editors:

Bozianu R. Synthesis of Interactive Reactive Systems : Synthèse des systèmes réactifs interactifs. [Doctoral Dissertation]. Université Paris-Est; 2016. Available from: http://www.theses.fr/2016PESC1026

11. Sakho, Mouhamadou Tafsir. ⌈-Pomset pour la modélisation et la vérification de systèmes parallèles : ⌈-Pomset for modelling and verifying parallel systems.

Degree: Docteur es, Mathématiques-Informatique, 2014, Orléans; Université polytechnique de l'Ouest Africain (Dakar, Sénégal)

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

►

Un comportement distribué peut être décrit avec un multi-ensemble partiellement ordonné (pomset). Bien que compacts et très intuitifs, ces modèles sont difficiles à vérifier. La… (more)

▼

Un comportement distribué peut être décrit avec un multi-ensemble partiellement ordonné (pomset). Bien que compacts et très intuitifs, ces modèles sont difficiles à vérifier. La principale technique utilisée dans cette thèse est de ramener les problèmes de décision de la logique MSO sur les pomsets à des problèmes de décision sur les mots. Les problèmes considérés sont la satisfiabilité et la vérification. Le problème de la vérification pour une formule donnée et un pomset consiste à décider si une interprétation est vraie, et le problème de satisfiabilité consiste à décider si un pomset répondant à la formule existe. Le problème de satisfiabilité de MSO sur pomsets est indécidable. Une procédure de semi-décision peut apporter des solutions pour de nombreux cas, en dépit du fait qu'elle peut ne pas terminer. Nous proposons un nouveau modèle, que l'on appelle ⌈-Pomset, pouvant rendre l'exploration des pomsets possible. Par conséquent, si une formule est satisfiable alors notre approche mènera éventuellement à la détection d'une solution. De plus, en utilisant les ⌈-Pomsets comme modèles pour systèmes concurrents, le model-checking de formules ordre partiel sur systèmes concurrents est décidable. Certaines expérimentations ont été faites en utilisant l'outil MONA. Nous avons comparé aussi la puissance expressive de certains modèles classiques de la concurrence comme les traces de Mazurkiewicz avec les ⌈-Pomsets.

Multiset of partially ordered events (pomset) can describe distributed behavior. Although very intuitive and compact, these models are difficult to verify. The main technique used in this thesis is to bring back decision problems for MSO over pomsets to problems for MSO over words. The problems considered are satisfiability and verification. The verification problem for a formula and a given pomset consists in deciding whether such an interpretation exists, and the satisfiability problem consists in deciding whether a pomset satisfying the formula exists. The satisfiability problem of MSO over pomsets is undecidable. A semi-decision procedures can provide solutions for many cases despite the fact that they may not terminate. We propose a new model, so called ⌈-Pomset, making the exploration of pomsets space possible. Consequently, if a formula is satisfiable then our approach will eventually lead to the detection of a solution. Moreover, using ⌈-Pomsets as models for concurrent systems, the model checking of partial order formulas on concurrent systems is decidable. Some experiments have been made using MONA. We compare also the expressive power of some classical model of concurrency such as Mazurkiewicz traces with our ⌈-Pomsets.

Advisors/Committee Members: Couvreur, Jean-Michel (thesis director), Seydi, Hamet (thesis director).

Subjects/Keywords: Pomset; Model-checking; Satisfiabilité; Traces; Pomset; Model-checking; Satisfiability; Trace; 004.3

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Sakho, M. T. (2014). ⌈-Pomset pour la modélisation et la vérification de systèmes parallèles : ⌈-Pomset for modelling and verifying parallel systems. (Doctoral Dissertation). Orléans; Université polytechnique de l'Ouest Africain (Dakar, Sénégal). Retrieved from http://www.theses.fr/2014ORLE2068

Chicago Manual of Style (16^th Edition):

Sakho, Mouhamadou Tafsir. “⌈-Pomset pour la modélisation et la vérification de systèmes parallèles : ⌈-Pomset for modelling and verifying parallel systems.” 2014. Doctoral Dissertation, Orléans; Université polytechnique de l'Ouest Africain (Dakar, Sénégal). Accessed January 19, 2020. http://www.theses.fr/2014ORLE2068.

MLA Handbook (7^th Edition):

Sakho, Mouhamadou Tafsir. “⌈-Pomset pour la modélisation et la vérification de systèmes parallèles : ⌈-Pomset for modelling and verifying parallel systems.” 2014. Web. 19 Jan 2020.

Vancouver:

Sakho MT. ⌈-Pomset pour la modélisation et la vérification de systèmes parallèles : ⌈-Pomset for modelling and verifying parallel systems. [Internet] [Doctoral dissertation]. Orléans; Université polytechnique de l'Ouest Africain (Dakar, Sénégal); 2014. [cited 2020 Jan 19]. Available from: http://www.theses.fr/2014ORLE2068.

Council of Science Editors:

Sakho MT. ⌈-Pomset pour la modélisation et la vérification de systèmes parallèles : ⌈-Pomset for modelling and verifying parallel systems. [Doctoral Dissertation]. Orléans; Université polytechnique de l'Ouest Africain (Dakar, Sénégal); 2014. Available from: http://www.theses.fr/2014ORLE2068

12. Fronc, Lukasz. Compilation de réseaux de Petri : modèles haut niveau et symétries de processus : Compilation of Petri nets : high-level models and process symmetries.

Degree: Docteur es, Informatique, 2013, Evry-Val d'Essonne

URL: http://www.theses.fr/2013EVRY0034

►

Cette thèse s'intéresse à la vérification de systèmes automatisables par model-checking. La question sous-jacente autour de laquelle se construit la contribution est la recherche d'un… (more)

▼

Cette thèse s'intéresse à la vérification de systèmes automatisables par model-checking. La question sous-jacente autour de laquelle se construit la contribution est la recherche d'un compromis entre différents objectifs potentiellement contradictoires : la décidabilité des systèmes à vérifier, l'expressivité des formalismes de modélisation, l'efficacité de la vérification, et la certification des outils utilisés. Dans ce but, on choisit de baser la modélisation sur des réseaux de Petri annotés par des langages de programmation réels. Cela implique la semi-décidabilité de la plupart des questions puisque la responsabilité de la terminaison est remise entre les mains du modélisateur (tout comme la terminaison des programmes est de la responsabilité du programmeur). Afin d'exploiter efficacement ces annotations, on choisit ensuite une approche de compilation de modèle qui permet de générer des programmes efficaces dans le langage des annotations, qui sont alors exécutées de la manière la plus efficace. De plus, la compilation est optimisée en tirant partie des spécificités de chaque modèle et nous utilisons l'approche de model-checking explicite qui autorise cette richesse d'annotations tout en facilitant le diagnostique et en restant compatible avec la simulation (les modèles compilés peuvent servir à de la simulation efficace). Enfin, pour combattre l'explosion combinatoire, nous utilisons des techniques de réductions de symétries qui permettent de réduire les temps d'exploration et l'espace mémoire nécessaire.

This work focuses on verification of automated systems using model-checking techniques. We focus on a compromise between potentially contradictory goals: decidability of systems to be verified, expressivity of modeling formalisms, efficiency of verification, and certification of used tools. To do so, we use high level Petri nets annotated by real programming languages. This implies the semi-decidability of most of problems because termination is left to the modeler (like termination of programs is left to the programmer). To handle these models, we choose a compilation approach which produces programs in the model annotation language, this allows to execute them efficiently. Moreover, this compilation is optimizing using model peculiarities. However, this rich expressivity leads to the use of explicit model-checking which allows to have rich model annotations but also allows to easily recover errors from verification, and remains compatible with simulation (these compiled models can be used for efficient simulation). Finally, to tackle the state space explosion problem, we use reduction by symmetries techniques which allow to reduce exploration times and state spaces.

Advisors/Committee Members: Klaudel, Hanna (thesis director), Pommereau, Franck (thesis director).

Subjects/Keywords: Model-checking; Model-checking; High-level Petri nets; Compilation

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Fronc, L. (2013). Compilation de réseaux de Petri : modèles haut niveau et symétries de processus : Compilation of Petri nets : high-level models and process symmetries. (Doctoral Dissertation). Evry-Val d'Essonne. Retrieved from http://www.theses.fr/2013EVRY0034

Chicago Manual of Style (16^th Edition):

Fronc, Lukasz. “Compilation de réseaux de Petri : modèles haut niveau et symétries de processus : Compilation of Petri nets : high-level models and process symmetries.” 2013. Doctoral Dissertation, Evry-Val d'Essonne. Accessed January 19, 2020. http://www.theses.fr/2013EVRY0034.

MLA Handbook (7^th Edition):

Fronc, Lukasz. “Compilation de réseaux de Petri : modèles haut niveau et symétries de processus : Compilation of Petri nets : high-level models and process symmetries.” 2013. Web. 19 Jan 2020.

Vancouver:

Fronc L. Compilation de réseaux de Petri : modèles haut niveau et symétries de processus : Compilation of Petri nets : high-level models and process symmetries. [Internet] [Doctoral dissertation]. Evry-Val d'Essonne; 2013. [cited 2020 Jan 19]. Available from: http://www.theses.fr/2013EVRY0034.

Council of Science Editors:

Fronc L. Compilation de réseaux de Petri : modèles haut niveau et symétries de processus : Compilation of Petri nets : high-level models and process symmetries. [Doctoral Dissertation]. Evry-Val d'Essonne; 2013. Available from: http://www.theses.fr/2013EVRY0034

13. Declerck, David. Vérification par model-checking de programmes concurrents paramétrés sur des modèles mémoires faibles : Verification via Model Checking of Parameterized Concurrent Programs on Weak Memory Models.

Degree: Docteur es, Informatique, 2018, Paris Saclay

URL: http://www.theses.fr/2018SACLS336

►

Les multiprocesseurs et microprocesseurs multicœurs modernes mettent en oeuvre des modèles mémoires dits faibles ou relâchés, dans dans lesquels l'ordre apparent des opérations mémoire ne… (more)

▼

Les multiprocesseurs et microprocesseurs multicœurs modernes mettent en oeuvre des modèles mémoires dits faibles ou relâchés, dans dans lesquels l'ordre apparent des opérations mémoire ne suit pas la cohérence séquentielle (SC) proposée par Leslie Lamport. Tout programme concurrent s'exécutant sur une telle architecture et conçu avec un modèle SC en tête risque de montrer à l'exécution de nouveaux comportements, dont certains sont potentiellement des comportements incorrects. Par exemple, un algorithme d'exclusion mutuelle correct avec une sémantique par entrelacement pourrait ne plus garantir l'exclusion mutuelle lorsqu'il est mis en oeuvre sur une architecture plus relâchée. Raisonner sur la sémantique de tels programmes s'avère très difficile. Par ailleurs, bon nombre d'algorithmes concurrents sont conçus pour fonctionner indépendamment du nombre de processus mis en oeuvre. On voudrait donc pouvoir s'assurer de la correction d'algorithmes concurrents, quel que soit le nombre de processus impliqués. Pour ce faire, on s'appuie sur le cadre du Model Checking Modulo Theories (MCMT), développé par Ghilardi et Ranise, qui permet la vérification de propriétés de sûreté de programmes concurrents paramétrés, c'est-à-dire mettant en oeuvre un nombre arbitraire de processus. On étend cette technologie avec une théorie permettant de raisonner sur des modèles mémoires faibles. Le résultat ce ces travaux est une extension du model checker Cubicle, appelée Cubicle-W, permettant de vérifier des propriétés de systèmes de transitions paramétrés s'exécutant sur un modèle mémoire faible similaire à TSO.

Modern multiprocessors and microprocesseurs implement weak or relaxed memory models, in which the apparent order of memory operation does not follow the sequential consistency (SC) proposed by Leslie Lamport. Any concurrent program running on such architecture and designed with an SC model in mind may exhibit new behaviors during its execution, some of which may potentially be incorrect. For instance, a mutual exclusion algorithm, correct under an interleaving semantics, may no longer guarantee mutual exclusion when implemented on a weaker architecture. Reasoning about the semantics of such programs is a difficult task. Moreover, most concurrent algorithms are designed for an arbitrary number of processus. We would like to ensure the correctness of concurrent algorithms, regardless of the number of processes involved. For this purpose, we rely on the Model Checking Modulo Theories (MCMT) framework, developed by Ghilardi and Ranise, which allows for the verification of safety properties of parameterized concurrent programs, that is to say, programs involving an arbitrary number of processes. We extend this technology with a theory for reasoning about weak memory models. The result of this work is an extension of the Cubicle model checker called Cubicle-W, which allows the verification of safety properties of parameterized transition systems running under a weak memory model similar to TSO.

Advisors/Committee Members: Zaïdi, Fatiha (thesis director).

Subjects/Keywords: Mémoire faible; Model checking; Vérification; Weak memory; Model checking; Verification

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Declerck, D. (2018). Vérification par model-checking de programmes concurrents paramétrés sur des modèles mémoires faibles : Verification via Model Checking of Parameterized Concurrent Programs on Weak Memory Models. (Doctoral Dissertation). Paris Saclay. Retrieved from http://www.theses.fr/2018SACLS336

Chicago Manual of Style (16^th Edition):

Declerck, David. “Vérification par model-checking de programmes concurrents paramétrés sur des modèles mémoires faibles : Verification via Model Checking of Parameterized Concurrent Programs on Weak Memory Models.” 2018. Doctoral Dissertation, Paris Saclay. Accessed January 19, 2020. http://www.theses.fr/2018SACLS336.

MLA Handbook (7^th Edition):

Declerck, David. “Vérification par model-checking de programmes concurrents paramétrés sur des modèles mémoires faibles : Verification via Model Checking of Parameterized Concurrent Programs on Weak Memory Models.” 2018. Web. 19 Jan 2020.

Vancouver:

Declerck D. Vérification par model-checking de programmes concurrents paramétrés sur des modèles mémoires faibles : Verification via Model Checking of Parameterized Concurrent Programs on Weak Memory Models. [Internet] [Doctoral dissertation]. Paris Saclay; 2018. [cited 2020 Jan 19]. Available from: http://www.theses.fr/2018SACLS336.

Council of Science Editors:

Declerck D. Vérification par model-checking de programmes concurrents paramétrés sur des modèles mémoires faibles : Verification via Model Checking of Parameterized Concurrent Programs on Weak Memory Models. [Doctoral Dissertation]. Paris Saclay; 2018. Available from: http://www.theses.fr/2018SACLS336

14. Naujokat, Stefan. Automatische Generierung von Prozessen im jABC.

Degree: 2009, Technische Universität Dortmund

URL: http://hdl.handle.net/2003/29822

► Serviceorientierung ist ein zentrales Element zur Wiederverwendung in der Softwareentwicklung und die Modellierung von ausführbaren Prozessen aus Services (Orchestrierung) ermöglicht auch Anwendungsexperten, die in der… (more)

Subjects/Keywords: Datenflussanalyse; Lose Spezifikation; Model checking; Prozesssynthese; 004

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Naujokat, S. (2009). Automatische Generierung von Prozessen im jABC. (Thesis). Technische Universität Dortmund. Retrieved from http://hdl.handle.net/2003/29822

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

Naujokat, Stefan. “Automatische Generierung von Prozessen im jABC.” 2009. Thesis, Technische Universität Dortmund. Accessed January 19, 2020. http://hdl.handle.net/2003/29822.

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

MLA Handbook (7^th Edition):

Naujokat, Stefan. “Automatische Generierung von Prozessen im jABC.” 2009. Web. 19 Jan 2020.

Vancouver:

Naujokat S. Automatische Generierung von Prozessen im jABC. [Internet] [Thesis]. Technische Universität Dortmund; 2009. [cited 2020 Jan 19]. Available from: http://hdl.handle.net/2003/29822.

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

Council of Science Editors:

Naujokat S. Automatische Generierung von Prozessen im jABC. [Thesis]. Technische Universität Dortmund; 2009. Available from: http://hdl.handle.net/2003/29822

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

15. Oliveira, João Paulo dos Santos. Rabbit: A novel approach to find data-races during state-space exploration .

Degree: 2012, Universidade Federal de Pernambuco

URL: http://repositorio.ufpe.br/handle/123456789/10891

► Data-races are an important kind of error in concurrent shared-memory programs. Software model checking is a popular approach to find them. This research proposes a… (more)

Subjects/Keywords: Concorrency; Software Verification; Model Checking; Race conditions

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Oliveira, J. P. d. S. (2012). Rabbit: A novel approach to find data-races during state-space exploration . (Thesis). Universidade Federal de Pernambuco. Retrieved from http://repositorio.ufpe.br/handle/123456789/10891

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

Oliveira, João Paulo dos Santos. “Rabbit: A novel approach to find data-races during state-space exploration .” 2012. Thesis, Universidade Federal de Pernambuco. Accessed January 19, 2020. http://repositorio.ufpe.br/handle/123456789/10891.

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

MLA Handbook (7^th Edition):

Oliveira, João Paulo dos Santos. “Rabbit: A novel approach to find data-races during state-space exploration .” 2012. Web. 19 Jan 2020.

Vancouver:

Oliveira JPdS. Rabbit: A novel approach to find data-races during state-space exploration . [Internet] [Thesis]. Universidade Federal de Pernambuco; 2012. [cited 2020 Jan 19]. Available from: http://repositorio.ufpe.br/handle/123456789/10891.

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

Council of Science Editors:

Oliveira JPdS. Rabbit: A novel approach to find data-races during state-space exploration . [Thesis]. Universidade Federal de Pernambuco; 2012. Available from: http://repositorio.ufpe.br/handle/123456789/10891

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

University of Edinburgh

16. Lehtinen, Maria Karoliina. Syntactic complexity in the modal μ calculus.

Degree: PhD, 2017, University of Edinburgh

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

► This thesis studies how to eliminate syntactic complexity in Lμ, the modal μ calculus. Lμ is a verification logic in which a least fixpoint operator… (more)

▼ This thesis studies how to eliminate syntactic complexity in Lμ, the modal μ calculus. Lμ is a verification logic in which a least fixpoint operator μ, and its dual v, add recursion to a simple modal logic. The number of alternations between μ and v is a measure of complexity called the formula’s index: the lower the index, the easier a formula is to model-check. The central question of this thesis is a long standing one, the Lμ index problem: given a formula, what is the least index of any equivalent formula, that is to say, its semantic index? I take a syntactic approach, focused on simplifying formulas. The core decidability results are (i) alternative, syntax-focused decidability proofs for ML and Pμ 1 , the low complexity classes of μ; and (ii) a proof that Ʃμ 2 , the fragment of Lμ with one alternation, is decidable for formulas in the dual class Pμ 2 . Beyond its algorithmic contributions, this thesis aims to deepen our understanding of the index problem and the tools at our disposal. I study disjunctive form and related syntactic restrictions, and how they affect the index problem. The main technical results are that the transformation into disjunctive form preserves Pμ 2 -indices but not μ 2 -indices, and that some properties of binary trees are expressible with a lower index using disjunctive formulas than non-deterministic automata. The latter is part of a thorough account of how the Lμ index problem and the Rabin–Mostowski index problem for parity automata are related. In the final part of the thesis, I revisit the relationship between the index problem and parity games. The syntactic index of a formula is an upper bound on the descriptive complexity of its model-checking parity games. I show that the semantic index of a formula Ψ is bounded above by the descriptive complexity of the model-checking games for Ψ. I then study whether this bound is strict: if a formula Ψ is equivalent to a formula in an alternation class C, does a formula of C suffice to describe the winning regions of the model-checking games of Ψ? I prove that this is the case for ML, Pμ 1 , Ʃμ 2 , and the disjunctive fragment of any alternation class. I discuss the practical implications of these results and propose a uniform approach to the index problem, which subsumes the previously described decision procedures for low alternation classes. In brief, this thesis can be read as a guide on how to approach a seemingly complex Lμ formula. Along the way it studies what makes this such a difficult problem and proposes novel approaches to both simplifying individual formulas and deciding further fragments of the alternation hierarchy.

Subjects/Keywords: verification logic; Lµ; model-checking; Lµ formula

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Lehtinen, M. K. (2017). Syntactic complexity in the modal μ calculus. (Doctoral Dissertation). University of Edinburgh. Retrieved from http://hdl.handle.net/1842/29520

Chicago Manual of Style (16^th Edition):

Lehtinen, Maria Karoliina. “Syntactic complexity in the modal μ calculus.” 2017. Doctoral Dissertation, University of Edinburgh. Accessed January 19, 2020. http://hdl.handle.net/1842/29520.

MLA Handbook (7^th Edition):

Lehtinen, Maria Karoliina. “Syntactic complexity in the modal μ calculus.” 2017. Web. 19 Jan 2020.

Vancouver:

Lehtinen MK. Syntactic complexity in the modal μ calculus. [Internet] [Doctoral dissertation]. University of Edinburgh; 2017. [cited 2020 Jan 19]. Available from: http://hdl.handle.net/1842/29520.

Council of Science Editors:

Lehtinen MK. Syntactic complexity in the modal μ calculus. [Doctoral Dissertation]. University of Edinburgh; 2017. Available from: http://hdl.handle.net/1842/29520

Universidade Nova

17. Beyene, Tewodros Awgichew. Constraint-based verification of imperative programs.

Degree: 2011, Universidade Nova

URL: http://www.rcaap.pt/detail.jsp?id=oai:run.unl.pt:10362/7965

►

work presented in the context of the European Master’s program in Computational Logic, as the partial requirement for obtaining Master of Science degree in Computational… (more)

Subjects/Keywords: Program verification; Model checking; Constraint programming

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Beyene, T. A. (2011). Constraint-based verification of imperative programs. (Thesis). Universidade Nova. Retrieved from http://www.rcaap.pt/detail.jsp?id=oai:run.unl.pt:10362/7965

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

Beyene, Tewodros Awgichew. “Constraint-based verification of imperative programs.” 2011. Thesis, Universidade Nova. Accessed January 19, 2020. http://www.rcaap.pt/detail.jsp?id=oai:run.unl.pt:10362/7965.

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

MLA Handbook (7^th Edition):

Beyene, Tewodros Awgichew. “Constraint-based verification of imperative programs.” 2011. Web. 19 Jan 2020.

Vancouver:

Beyene TA. Constraint-based verification of imperative programs. [Internet] [Thesis]. Universidade Nova; 2011. [cited 2020 Jan 19]. Available from: http://www.rcaap.pt/detail.jsp?id=oai:run.unl.pt:10362/7965.

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

Council of Science Editors:

Beyene TA. Constraint-based verification of imperative programs. [Thesis]. Universidade Nova; 2011. Available from: http://www.rcaap.pt/detail.jsp?id=oai:run.unl.pt:10362/7965

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

18. Cordy, Maxime. Model Checking for the Masses.

Degree: 2014, DIAL (Belgium)

URL: http://hdl.handle.net/2078.2/152729

►

The model-checking problem for software product lines is harder than for single systems. Indeed, one has to verify all the software variants of a product… (more)

▼

The model-checking problem for software product lines is harder than for single systems. Indeed, one has to verify all the software variants of a product line, whose number grows exponentially in the number of their differences. Techniques intended for single systems are inefficient in this case, for these can only be applied to all products separately. Variability-aware modelling formalisms and algorithms were designed as a more appropriate answer to that problem. Their strength lies in their ability to check a behaviour common to several products only once, which leads to substantial performance gains. Although they constitute a major step toward the efficient verification of product lines, these techniques are not yet mature enough to truly achieve this objective. They still lack optimisations to verify large models, the expressiveness to represent complex forms of variable behaviour, as well as usable languages and tools required for industrial transfer. This thesis aims at improving product-line model checking in order to provide formalisms, algorithms, and tools that together hold the potential to verify real-world software product lines. We first study the state-of-the-art model-checking approaches for software product lines. We compare them in terms of available formalisms and algorithms, and we determine that the approach based on Featured Transition Systems (FTS) is the most suitable to act as a basis for the design of novel techniques. We then extend its theory along two axes: efficiency and expressiveness. For the former, we propose abstraction methods that can reduce the size of the model to check while maintaining correctness and completeness; they consist of extensions of single-system abstraction techniques applied to FTS, and of new techniques that abstract away from their variability. As for expressiveness, on the one hand we propose featured timed automata as a combination of FTS and real-time behaviour. On the other hand, we analyse how to support in FTS complex forms of variability such as numeric features and multi-features. We implemented our theoretical results into a new model-checking tool named ProVeLines. As all our extensions are based on FTS, they share many commonalities. ProVeLines was therefore designed as a product line whose each variant implements a distinct combination of verification formalisms and algorithms. Finally, we show that the principles we designed for product-line model checking can also be applied to other formal methods, namely the verification of adaptive systems and the synthesis of controllers for product lines.

(DOCSC06) – UNamur, 2014

Advisors/Committee Members: UNamur - INF_PRECISE, UNamur - Ecole doctorale en sciences, Atlee, Joanne, Greenyer, Joel, Heymans, Patrick, Legay, Axel, Petit, Michaël, Schobbens, Pierre-Yves.

Subjects/Keywords: Formal methods; model checking; software product lines

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Cordy, M. (2014). Model Checking for the Masses. (Thesis). DIAL (Belgium). Retrieved from http://hdl.handle.net/2078.2/152729

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

Cordy, Maxime. “Model Checking for the Masses.” 2014. Thesis, DIAL (Belgium). Accessed January 19, 2020. http://hdl.handle.net/2078.2/152729.

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

MLA Handbook (7^th Edition):

Cordy, Maxime. “Model Checking for the Masses.” 2014. Web. 19 Jan 2020.

Vancouver:

Cordy M. Model Checking for the Masses. [Internet] [Thesis]. DIAL (Belgium); 2014. [cited 2020 Jan 19]. Available from: http://hdl.handle.net/2078.2/152729.

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

Council of Science Editors:

Cordy M. Model Checking for the Masses. [Thesis]. DIAL (Belgium); 2014. Available from: http://hdl.handle.net/2078.2/152729

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

19. Evrot, Dominique. Contribution à la vérification d'exigences de sécurité : application au domaine de la machine industrielle : Contribution to safety requirements verification : application to industrial machinery domain.

Degree: Docteur es, Automatique, Traitement du Signal, Génie Informatique, 2008, Université Henri Poincaré – Nancy I

URL: http://www.theses.fr/2008NAN10038

►

L’introduction des nouvelles technologies de l’information et de la communication dans les systèmes automatisés entraîne un accroissement de la complexité des fonctions qu’ils supportent. Cet… (more)

▼

L’introduction des nouvelles technologies de l’information et de la communication dans les systèmes automatisés entraîne un accroissement de la complexité des fonctions qu’ils supportent. Cet accroissement de la complexité a un impact sur la sécurité des systèmes. En effet, leurs propriétés ne sont plus réductibles aux propriétés de leurs constituants pris isolément mais émergent d’un réseau d’interactions entre ces constituants qui peut être à l’origine de comportements néfastes et difficiles à prévoir. Notre conviction est que le développement sûr de ces systèmes doit combiner des approches pragmatiques orientées « système », qui tiennent compte du facteur d'échelle réel d'une automatisation pour appréhender le fonctionnement global du système et son architecture, avec des approches plus formelles qui permettent de s’assurer que les propriétés intrinsèques des constituants contribuent efficacement au respect des exigences « système » formulées par les utilisateurs. Le travail présenté dans ce mémoire définit donc une approche méthodologique basée sur le formalisme SysML (System Modeling Language) permettant l’identification, la formalisation et la structuration d’exigences globales relatives à un système, puis leur projection, sous forme de propriétés invariantes, sur une architecture de composants. La vérification des exigences de sécurité, repose alors, d’une part, sur un raffinement prouvé (par theroem proving) des exigences « système » permettant d’établir leur équivalence avec un ensemble de propriétés intrinsèques relatives à chacun des composants, et d’autre part, sur la vérification formelle (par model checking) de ces propriétés intrinsèques.

Introduction of new information and communication technology in automated systems leads to a growth of safety functions complexity. System properties are not limited to components properties, they issued from an interactions network that can introduces bad behaviour. Our conviction is that a safe development of such system must involve system oriented approaches in order to apprehend system global behaviour and architecture and more formal approaches allowing verifying that components properties satisfy end users system requirements We define a methodological approach based on SysML formalism (System Modelling Language) allowing global system requirements identification; formalisation and structuring in order to project these requirements on the system components architecture and so obtain local components properties. Then safety requirements verification is based in one hand on proved refinement (using theorem proving) of system requirements to components properties; and, in the other hand, on the formal verification (using model checking) of these components properties.

Advisors/Committee Members: Morel, Gérard (thesis director), Petin, Jean-François (thesis director).

Subjects/Keywords: Analyse des exigences; Vérification par model checking

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Evrot, D. (2008). Contribution à la vérification d'exigences de sécurité : application au domaine de la machine industrielle : Contribution to safety requirements verification : application to industrial machinery domain. (Doctoral Dissertation). Université Henri Poincaré – Nancy I. Retrieved from http://www.theses.fr/2008NAN10038

Chicago Manual of Style (16^th Edition):

Evrot, Dominique. “Contribution à la vérification d'exigences de sécurité : application au domaine de la machine industrielle : Contribution to safety requirements verification : application to industrial machinery domain.” 2008. Doctoral Dissertation, Université Henri Poincaré – Nancy I. Accessed January 19, 2020. http://www.theses.fr/2008NAN10038.

MLA Handbook (7^th Edition):

Evrot, Dominique. “Contribution à la vérification d'exigences de sécurité : application au domaine de la machine industrielle : Contribution to safety requirements verification : application to industrial machinery domain.” 2008. Web. 19 Jan 2020.

Vancouver:

Evrot D. Contribution à la vérification d'exigences de sécurité : application au domaine de la machine industrielle : Contribution to safety requirements verification : application to industrial machinery domain. [Internet] [Doctoral dissertation]. Université Henri Poincaré – Nancy I; 2008. [cited 2020 Jan 19]. Available from: http://www.theses.fr/2008NAN10038.

Council of Science Editors:

Evrot D. Contribution à la vérification d'exigences de sécurité : application au domaine de la machine industrielle : Contribution to safety requirements verification : application to industrial machinery domain. [Doctoral Dissertation]. Université Henri Poincaré – Nancy I; 2008. Available from: http://www.theses.fr/2008NAN10038

Université de Bordeaux I

20. Chucri, Farès. Exploiting model structure in CEGAR verification method : Exploiter la structure des modèles pour la vérification par la méthode CEGAR.

Degree: Docteur es, Informatique, 2012, Université de Bordeaux I

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

►

Cette thèse a eu pour but l'étude et la mise en oeuvre des méthodes de vérification par abstraction pour les modèles AltaRica. A cette effet,… (more)

Subjects/Keywords: Verification; Raffinement; Abstraction; Model Checking; Cegar; Abstraction

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Chucri, F. (2012). Exploiting model structure in CEGAR verification method : Exploiter la structure des modèles pour la vérification par la méthode CEGAR. (Doctoral Dissertation). Université de Bordeaux I. Retrieved from http://www.theses.fr/2012BOR14641

Chicago Manual of Style (16^th Edition):

Chucri, Farès. “Exploiting model structure in CEGAR verification method : Exploiter la structure des modèles pour la vérification par la méthode CEGAR.” 2012. Doctoral Dissertation, Université de Bordeaux I. Accessed January 19, 2020. http://www.theses.fr/2012BOR14641.

MLA Handbook (7^th Edition):

Chucri, Farès. “Exploiting model structure in CEGAR verification method : Exploiter la structure des modèles pour la vérification par la méthode CEGAR.” 2012. Web. 19 Jan 2020.

Vancouver:

Chucri F. Exploiting model structure in CEGAR verification method : Exploiter la structure des modèles pour la vérification par la méthode CEGAR. [Internet] [Doctoral dissertation]. Université de Bordeaux I; 2012. [cited 2020 Jan 19]. Available from: http://www.theses.fr/2012BOR14641.

Council of Science Editors:

Chucri F. Exploiting model structure in CEGAR verification method : Exploiter la structure des modèles pour la vérification par la méthode CEGAR. [Doctoral Dissertation]. Université de Bordeaux I; 2012. Available from: http://www.theses.fr/2012BOR14641

21. Lopes, Arnaud Da Costa. Propriétés de jeux multi-agents : Multi-agent games properties.

Degree: Docteur es, Informatique, 2011, Cachan, Ecole normale supérieure

URL: http://www.theses.fr/2011DENS0034

►

Nous etendons les logiques temporelles du temps alternant ATL et ATL* au moyen de contextes strategiques et de contraintes sur la memoire : la premiere… (more)

▼

Nous etendons les logiques temporelles du temps alternant ATL et ATL* au moyen de contextes strategiques et de contraintes sur la memoire : la premiere extension permet aux agents de s'en tenir a leurs strategies lors de l'evaluation des formules, contrairement a ATL ou chaque quantificateur de strategies ecrase les strategies anterieurement selectionnees. La seconde extension permet aux quantificateurs de strategies de se restreindre aux strategies sans memoire ou avec memoire bornee. Nous avons l'etudie l'expressivite de nos logiques. Nous montrons qu'elles expriment des proprietes importantes comme l'exstence d'equilibres, et nous les comparons formellement a d'autres formalismes proches (ATL, ATL*, Game Logic, Strategy Logic, ...). Nous avons aborde les problemes de model-checking. Nous donnons un algorithme PSPACE pour la logique n'impliquant que des strategies sans memoire, et un algorithme EXPSPACE pour le cas des strategies a memoire bornee. Dans le cas general, malgre leur forte expresssivite, nous prouvons que leur model-checking reste decidable par un algorithme a base d'automates d'arbres alternants qui permet d'evaluer une formule sur la classe complete des CGS avec n joueurs.

We extend the alternating-time temporal logics ATL and ATL* with strategy contexts and memory constraints: the first extension make agents commit to their strategies during the evaluation of formulas, contrary to plain ATL where strategy quantifiers reset previously selected strategies. The second extension allows strategy quantifiers to restrict to memoryless or bounded-memory strategies. We consider expressiveness issues. We show that our logics can express important properties such as equilibria, and we formally compare them with other similar formalisms (ATL, ATL*, Game Logic, Strategy Logic, ...). We address the problem of model-checking for our logics, especially we provide a PSPACE algorithm for the sublogics involving only memoryless strategies and an EXPSPACE algorithm for the bounded-memory case. In the general case, despite the high expressiveness of these logics, we prove that their model-checking problems remain decidable by designing a tree-automata-based algorithm for model-checking ATLsc on the full class of n-player concurrent game structures.

Advisors/Committee Members: Zielonka, Wieslaw (thesis director), Laroussinie, François (thesis director).

Subjects/Keywords: Logique temporelle; Vérification formelle; Model-checking

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Lopes, A. D. C. (2011). Propriétés de jeux multi-agents : Multi-agent games properties. (Doctoral Dissertation). Cachan, Ecole normale supérieure. Retrieved from http://www.theses.fr/2011DENS0034

Chicago Manual of Style (16^th Edition):

Lopes, Arnaud Da Costa. “Propriétés de jeux multi-agents : Multi-agent games properties.” 2011. Doctoral Dissertation, Cachan, Ecole normale supérieure. Accessed January 19, 2020. http://www.theses.fr/2011DENS0034.

MLA Handbook (7^th Edition):

Lopes, Arnaud Da Costa. “Propriétés de jeux multi-agents : Multi-agent games properties.” 2011. Web. 19 Jan 2020.

Vancouver:

Lopes ADC. Propriétés de jeux multi-agents : Multi-agent games properties. [Internet] [Doctoral dissertation]. Cachan, Ecole normale supérieure; 2011. [cited 2020 Jan 19]. Available from: http://www.theses.fr/2011DENS0034.

Council of Science Editors:

Lopes ADC. Propriétés de jeux multi-agents : Multi-agent games properties. [Doctoral Dissertation]. Cachan, Ecole normale supérieure; 2011. Available from: http://www.theses.fr/2011DENS0034

University of Colorado

22. Hassan, Zyad. Incremental, Inductive Model Checking.

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

URL: https://scholar.colorado.edu/ecen_gradetds/86

► Model checking has become a widely adopted approach for the verification of hardware designs. The ever increasing complexity of these designs creates a continuous… (more)

▼ Model checking has become a widely adopted approach for the verification of hardware designs. The ever increasing complexity of these designs creates a continuous need for faster model checkers that are capable of verifying designs within reasonable time frames to reduce time to market. IC3, the recently developed, very successful algorithm for model checking safety properties, introduced a new approach to model checking: incremental, inductive verification (IIV). The IIV approach possesses several attractive traits, such as stability and not relying on high-effort reasoning, that make its usage in model checking very appealing, which motivated the development of another algorithm that follows the IIV approach for model checking ω-regular languages. The algorithm, Fair, has been shown to be capable of dealing with designs beyond the reach of its predecessors. This thesis explores IIV as a promising approach to model checking. After identifying IIV's main elements, the thesis presents an IIV-based model checking algorithm for CTL: the first practical SAT-based algorithm for branching time properties. The algorithm, IICTL, is shown to complement state-of-the-art BDD-based CTL algorithms on a large set of benchmarks. In addition to fulfilling the need for a SAT-based CTL algorithm, IICTL highlights ways in which IIV algorithms can be improved; one of these ways is addressing counterexamples to generalization, which is explored in the context of IC3 and is shown to improve the algorithm's performance considerably. The thesis then addresses an important question: for properties that fall into the scope of more than one IIV algorithm, do these algorithms behave identically? The question is answered negatively, pointing out that the IIV framework admits multiple strategies and that there is a wide spectrum of possible algorithms that all follow the IIV approach. For example, all properties in the common fragment of LTL and CTL—an important class of properties—can be checked with Fair and IICTL. However, empirical evidence presented in the thesis suggests that neither algorithm is always superior to the other, which points out the importance of being flexible in deciding the strategy to apply to a given problem. Advisors/Committee Members: Fabio Somenzi, Aaron R. Bradley, Pavol Cerny, Sriram Sankaranarayanan, Niklas Sorensson.

Subjects/Keywords: Formal Verification; Model Checking; Satisfiability; Computer Engineering

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Hassan, Z. (2014). Incremental, Inductive Model Checking. (Doctoral Dissertation). University of Colorado. Retrieved from https://scholar.colorado.edu/ecen_gradetds/86

Chicago Manual of Style (16^th Edition):

Hassan, Zyad. “Incremental, Inductive Model Checking.” 2014. Doctoral Dissertation, University of Colorado. Accessed January 19, 2020. https://scholar.colorado.edu/ecen_gradetds/86.

MLA Handbook (7^th Edition):

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

Vancouver:

Hassan Z. Incremental, Inductive Model Checking. [Internet] [Doctoral dissertation]. University of Colorado; 2014. [cited 2020 Jan 19]. Available from: https://scholar.colorado.edu/ecen_gradetds/86.

Council of Science Editors:

Hassan Z. Incremental, Inductive Model Checking. [Doctoral Dissertation]. University of Colorado; 2014. Available from: https://scholar.colorado.edu/ecen_gradetds/86

University of Waikato

23. Shaw, Adrian Mark. Partial Order Reduction with Compositional Verification .

Degree: 2014, University of Waikato

URL: http://hdl.handle.net/10289/9001

► This thesis expands the usage of partial order reduction methods in reducing the state space of large models in model checking. The work done can… (more)

Subjects/Keywords: Partial order reduction; Model checking; compositional verification

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Shaw, A. M. (2014). Partial Order Reduction with Compositional Verification . (Masters Thesis). University of Waikato. Retrieved from http://hdl.handle.net/10289/9001

Chicago Manual of Style (16^th Edition):

Shaw, Adrian Mark. “Partial Order Reduction with Compositional Verification .” 2014. Masters Thesis, University of Waikato. Accessed January 19, 2020. http://hdl.handle.net/10289/9001.

MLA Handbook (7^th Edition):

Shaw, Adrian Mark. “Partial Order Reduction with Compositional Verification .” 2014. Web. 19 Jan 2020.

Vancouver:

Shaw AM. Partial Order Reduction with Compositional Verification . [Internet] [Masters thesis]. University of Waikato; 2014. [cited 2020 Jan 19]. Available from: http://hdl.handle.net/10289/9001.

Council of Science Editors:

Shaw AM. Partial Order Reduction with Compositional Verification . [Masters Thesis]. University of Waikato; 2014. Available from: http://hdl.handle.net/10289/9001

Vanderbilt University

24. Li, Yi. Linux Device Driver Synthesis and Verification.

Degree: MS, Computer Science, 2015, Vanderbilt University

URL: http://etd.library.vanderbilt.edu/available/etd-11172015-221551/ ;

► The device driver is a program which provides a software interface to a hardware device, enabling operating systems and other computer programs to access hardware… (more)

Subjects/Keywords: driver synthesis; model checking; domain specific language

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Li, Y. (2015). Linux Device Driver Synthesis and Verification. (Masters Thesis). Vanderbilt University. Retrieved from http://etd.library.vanderbilt.edu/available/etd-11172015-221551/ ;

Chicago Manual of Style (16^th Edition):

Li, Yi. “Linux Device Driver Synthesis and Verification.” 2015. Masters Thesis, Vanderbilt University. Accessed January 19, 2020. http://etd.library.vanderbilt.edu/available/etd-11172015-221551/ ;.

MLA Handbook (7^th Edition):

Li, Yi. “Linux Device Driver Synthesis and Verification.” 2015. Web. 19 Jan 2020.

Vancouver:

Li Y. Linux Device Driver Synthesis and Verification. [Internet] [Masters thesis]. Vanderbilt University; 2015. [cited 2020 Jan 19]. Available from: http://etd.library.vanderbilt.edu/available/etd-11172015-221551/ ;.

Council of Science Editors:

Li Y. Linux Device Driver Synthesis and Verification. [Masters Thesis]. Vanderbilt University; 2015. Available from: http://etd.library.vanderbilt.edu/available/etd-11172015-221551/ ;

University of Waterloo

25. Kajarekar, Tejas. Fully Automated Translation of BoxTalk to Promela.

Degree: 2011, University of Waterloo

URL: http://hdl.handle.net/10012/6135

► Telecommunication systems are structured to enable incremental growth, so that new telecommunication features can be added to the set of existing features. With the addition… (more)

Subjects/Keywords: Model checking; Automated translation; SPIN; BoxTalk

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Kajarekar, T. (2011). Fully Automated Translation of BoxTalk to Promela. (Thesis). University of Waterloo. Retrieved from http://hdl.handle.net/10012/6135

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

Kajarekar, Tejas. “Fully Automated Translation of BoxTalk to Promela.” 2011. Thesis, University of Waterloo. Accessed January 19, 2020. http://hdl.handle.net/10012/6135.

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

MLA Handbook (7^th Edition):

Kajarekar, Tejas. “Fully Automated Translation of BoxTalk to Promela.” 2011. Web. 19 Jan 2020.

Vancouver:

Kajarekar T. Fully Automated Translation of BoxTalk to Promela. [Internet] [Thesis]. University of Waterloo; 2011. [cited 2020 Jan 19]. Available from: http://hdl.handle.net/10012/6135.

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

Council of Science Editors:

Kajarekar T. Fully Automated Translation of BoxTalk to Promela. [Thesis]. University of Waterloo; 2011. Available from: http://hdl.handle.net/10012/6135

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

26. Friggens, David. On the Use of Model Checking for the Bounded and Unbounded Verification of Nonblocking Concurrent Data Structures.

Degree: 2013, Victoria University of Wellington

URL: http://hdl.handle.net/10063/2702

► Concurrent data structure algorithms have traditionally been designed using locks to regulate the behaviour of interacting threads, thus restricting access to parts of the shared… (more)

▼ Concurrent data structure algorithms have traditionally been designed using locks to regulate the behaviour of interacting threads, thus restricting access to parts of the shared memory to only one thread at a time. Since locks can lead to issues of performance and scalability, there has been interest in designing so-called nonblocking algorithms that do not use locks. However, designing and reasoning about concurrent systems is difficult, and is even more so for nonblocking systems, as evidenced by the number of incorrect algorithms in the literature. This thesis explores how the technique of model checking can aid the testing and verification of nonblocking data structure algorithms. Model checking is an automated verification method for finite state systems, and is able to produce counterexamples when verification fails. For verification, concurrent data structures are considered to be infinite state systems, as there is no bound on the number of interacting threads, the number of elements in the data structure, nor the number of possible distinct data values. Thus, in order to analyse concurrent data structures with model checking, we must either place finite bounds upon them, or employ an abstraction technique that will construct a finite system with the same properties. First, we discuss how nonblocking data structures can be best represented for model checking, and how to specify the properties we are interested in verifying. These properties are the safety property linearisability, and the progress properties wait-freedom, lock-freedom and obstructionfreedom. Second, we investigate using model checking for exhaustive testing, by verifying bounded (and hence finite state) instances of nonblocking data structures, parameterised by the number of threads, the number of distinct data values, and the size of storage memory (e.g. array length, or maximum number of linked list nodes). It is widely held, based on anecdotal evidence, that most bugs occur in small instances. We investigate the smallest bounds needed to falsify a number of incorrect algorithms, which supports this hypothesis. We also investigate verifying a number of correct algorithms for a range of bounds. If an algorithm can be verified for bounds significantly higher than the minimum bounds needed for falsification, then we argue it provides a high degree of confidence in the general correctness of the algorithm. However, with the available hardware we were not able to verify any of the algorithms to high enough bounds to claim such confidence. Third, we investigate using model checking to verify nonblocking data structures by employing the technique of canonical abstraction to construct finite state representations of the unbounded algorithms. Canonical abstraction represents abstract states as 3-valued logical structures, and allows the initial coarse abstraction to be refined as necessary by adding derived predicates. We introduce several novel derived predicates and show how these allow linearisability to be verified for linked list based… Advisors/Committee Members: Groves, LIndsay.

Subjects/Keywords: Nonblocking algorithms; Model checking; Canonical abstraction

1 more image…

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Friggens, D. (2013). On the Use of Model Checking for the Bounded and Unbounded Verification of Nonblocking Concurrent Data Structures. (Doctoral Dissertation). Victoria University of Wellington. Retrieved from http://hdl.handle.net/10063/2702

Chicago Manual of Style (16^th Edition):

Friggens, David. “On the Use of Model Checking for the Bounded and Unbounded Verification of Nonblocking Concurrent Data Structures.” 2013. Doctoral Dissertation, Victoria University of Wellington. Accessed January 19, 2020. http://hdl.handle.net/10063/2702.

MLA Handbook (7^th Edition):

Friggens, David. “On the Use of Model Checking for the Bounded and Unbounded Verification of Nonblocking Concurrent Data Structures.” 2013. Web. 19 Jan 2020.

Vancouver:

Friggens D. On the Use of Model Checking for the Bounded and Unbounded Verification of Nonblocking Concurrent Data Structures. [Internet] [Doctoral dissertation]. Victoria University of Wellington; 2013. [cited 2020 Jan 19]. Available from: http://hdl.handle.net/10063/2702.

Council of Science Editors:

Friggens D. On the Use of Model Checking for the Bounded and Unbounded Verification of Nonblocking Concurrent Data Structures. [Doctoral Dissertation]. Victoria University of Wellington; 2013. Available from: http://hdl.handle.net/10063/2702

Colorado State University

27. Al Lail, Mustafa. Unified Modeling Language framework for specifying and analyzing temporal properties, A.

Degree: PhD, Computer Science, 2018, Colorado State University

URL: http://hdl.handle.net/10217/191492

► In the context of Model-Driven Engineering (MDE), designers use the Unified Modeling Language (UML) to create models that drive the entire development process. Once UML… (more)

Subjects/Keywords: Properties; Temporal; Verification; Specification; Model Checking; UML

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Al Lail, M. (2018). Unified Modeling Language framework for specifying and analyzing temporal properties, A. (Doctoral Dissertation). Colorado State University. Retrieved from http://hdl.handle.net/10217/191492

Chicago Manual of Style (16^th Edition):

Al Lail, Mustafa. “Unified Modeling Language framework for specifying and analyzing temporal properties, A.” 2018. Doctoral Dissertation, Colorado State University. Accessed January 19, 2020. http://hdl.handle.net/10217/191492.

MLA Handbook (7^th Edition):

Al Lail, Mustafa. “Unified Modeling Language framework for specifying and analyzing temporal properties, A.” 2018. Web. 19 Jan 2020.

Vancouver:

Al Lail M. Unified Modeling Language framework for specifying and analyzing temporal properties, A. [Internet] [Doctoral dissertation]. Colorado State University; 2018. [cited 2020 Jan 19]. Available from: http://hdl.handle.net/10217/191492.

Council of Science Editors:

Al Lail M. Unified Modeling Language framework for specifying and analyzing temporal properties, A. [Doctoral Dissertation]. Colorado State University; 2018. Available from: http://hdl.handle.net/10217/191492

Iowa State University

28. Suvorov, Yuly. A model checking approach for analyzing and identifying intervention policies to counter infection propagation over networks.

Degree: 2011, Iowa State University

URL: https://lib.dr.iastate.edu/etd/10431

► The spread of infections (disease, ideas, fires, etc.) in a network (group of people, electronic network, forest, etc.) can be modeled by the evolution of… (more)

Subjects/Keywords: Disease; Infection; Model Checking; Policies; Computer Sciences

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Suvorov, Y. (2011). A model checking approach for analyzing and identifying intervention policies to counter infection propagation over networks. (Thesis). Iowa State University. Retrieved from https://lib.dr.iastate.edu/etd/10431

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

Suvorov, Yuly. “A model checking approach for analyzing and identifying intervention policies to counter infection propagation over networks.” 2011. Thesis, Iowa State University. Accessed January 19, 2020. https://lib.dr.iastate.edu/etd/10431.

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

MLA Handbook (7^th Edition):

Suvorov, Yuly. “A model checking approach for analyzing and identifying intervention policies to counter infection propagation over networks.” 2011. Web. 19 Jan 2020.

Vancouver:

Suvorov Y. A model checking approach for analyzing and identifying intervention policies to counter infection propagation over networks. [Internet] [Thesis]. Iowa State University; 2011. [cited 2020 Jan 19]. Available from: https://lib.dr.iastate.edu/etd/10431.

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

Council of Science Editors:

Suvorov Y. A model checking approach for analyzing and identifying intervention policies to counter infection propagation over networks. [Thesis]. Iowa State University; 2011. Available from: https://lib.dr.iastate.edu/etd/10431

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

29. Martins, Alexandre Locci. Teste e verificação formal do comportamento excepcional de programas Java.

Degree: Mestrado, Ciência da Computação, 2014, University of São Paulo

URL: http://www.teses.usp.br/teses/disponiveis/45/45134/tde-11082014-150106/ ;

►

Estruturas de tratamento de exceção são extremamente comuns em softwares desenvolvidos em linguagens modernas, como Java, e afetam de forma contundente o comportamento de um… (more)

▼

Estruturas de tratamento de exceção são extremamente comuns em softwares desenvolvidos em linguagens modernas, como Java, e afetam de forma contundente o comportamento de um software quando exercitadas. Apesar destas duas características, as principais técnicas de verificação, teste de software e verificação formal, e as ferramentas a elas vinculadas, tendem a negligenciar o comportamento excepcional. Alguns dos fatores que levam a esta negligência são a não especificação do comportamento excepcional em termos de projeto e a consequente implementação das estruturas de tratamento com base no julgamento individual de cada programador. Isto resulta na não consideração de partes expressivas do código em termos de verificação e, consequentemente, a possibilidade de não serem detectados erros relativos tanto às próprias estruturas de tratamento quanto às estruturas de código vinculadas a estas. A fim de abordar este problema, propomos uma técnica, baseada em model checking, que automatiza o processo de exercício de caminhos excepcionais. Isto permite que seja observado o comportamento de um software quando da ocorrência de uma exceção. Pretendemos, com esta técnica, dar suporte para que seja aplicado aos caminhos que representam o comportamento excepcional de um software as mesmas técnicas de detecção de erros que são aplicadas aos caminhos que representam o comportamento normal e, com isso, agregar um aumento na qualidade do desenvolvimento de software.

Software developed in modern languages, such as Java, commonly present structures of exception handling. These structures, when exercised, may affect the software behavior. Despite these two characteristics, the main verification techniques, software testing and formal verification and the tools related to them, tend to neglect the exceptional behavior. The nonexistent specification of software exceptional behaviors at the design level, and, the subsequent implementation of exception handling based on the judgment of each programmer, are some factors that lead to this neglect. These factors result in the non-consideration of the expressive parts of the code in verification terms and, consequently, the impossibility of errors detection concerning either the exception treatment structures or the code structures linked to them. Taking this fact into consideration, we propose a technique based on the model checking process, which automates the process of exercising exceptional paths to address this problem. This allows the observation of the software behavior when an exception occurs. With this technique, we intend to support the application of the same error detection techniques for program normal behavior paths to the paths that represent the software exceptional behavior. Therefore, using the proposed technique, we aim to increase the software development quality.

Advisors/Committee Members: Melo, Ana Cristina Vieira de.

Subjects/Keywords: comportamento excepcional; exceção; exception; exceptional behavior; Java; Java; model checker; model checker; model checking; model checking

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Martins, A. L. (2014). Teste e verificação formal do comportamento excepcional de programas Java. (Masters Thesis). University of São Paulo. Retrieved from http://www.teses.usp.br/teses/disponiveis/45/45134/tde-11082014-150106/ ;

Chicago Manual of Style (16^th Edition):

Martins, Alexandre Locci. “Teste e verificação formal do comportamento excepcional de programas Java.” 2014. Masters Thesis, University of São Paulo. Accessed January 19, 2020. http://www.teses.usp.br/teses/disponiveis/45/45134/tde-11082014-150106/ ;.

MLA Handbook (7^th Edition):

Martins, Alexandre Locci. “Teste e verificação formal do comportamento excepcional de programas Java.” 2014. Web. 19 Jan 2020.

Vancouver:

Martins AL. Teste e verificação formal do comportamento excepcional de programas Java. [Internet] [Masters thesis]. University of São Paulo; 2014. [cited 2020 Jan 19]. Available from: http://www.teses.usp.br/teses/disponiveis/45/45134/tde-11082014-150106/ ;.

Council of Science Editors:

Martins AL. Teste e verificação formal do comportamento excepcional de programas Java. [Masters Thesis]. University of São Paulo; 2014. Available from: http://www.teses.usp.br/teses/disponiveis/45/45134/tde-11082014-150106/ ;

University of California – Berkeley

30. Sturton, Cynthia. Secure Virtualization with Formal Methods.

Degree: Computer Science, 2013, University of California – Berkeley

URL: http://www.escholarship.org/uc/item/59q2n05r

► Virtualization software is increasingly a part of the infrastructure behind our online activities. Companies and institutions that produce online content are taking advantage of the… (more)

▼ Virtualization software is increasingly a part of the infrastructure behind our online activities. Companies and institutions that produce online content are taking advantage of the "infrastructure as a service" cloud computing model to obtain cheap and reliable computing power. Cloud providers are able to provide this service by letting multiple client operating systems share a single physical machine, and they use virtualization technology to do that. The virtualization layer also provides isolation between guests, protecting each from unwanted access by the co-tenants. Beyond cloud computing, virtualization software has a variety of security-critical applications, including intrusion detection systems, malware analysis, and providing a secure execution environment in end-users' personal machines.In this work, we investigate the verification of isolation properties for virtualization software. Large data structures, such as page tables and caches, are often used to keep track of emulated state and are central to providing correct isolation. We identify these large data structures as one of the biggest challenges in applying traditional formal methods to the verification of isolation properties in virtualization software.We present a new semi-automatic procedure, S2W, to tackle this challenge. Our approach uses a combination of abstraction and bounded model checking and allows for the verification of safety properties of large or unbounded arrays. The key new ideas are a set of heuristics for creating an abstract model and computing a bound on the reachability diameter of its state space. We evaluate this methodology using six case studies, including verification of the address translation logic in the Bochs x86 emulator, and verification of security properties of several hypervisor models. In all of our case studies, we show that our heuristics are effective: we are able to prove the safety property of interest in a reasonable amount of time (the longest verification takes 70 minutes to complete), and our abstraction-based model checking returns no spurious counter-examples.One weakness of using model checking is that the verification result is only as good as the model; if the model does not accurately represent the system under consideration, properties proven true of the model may or may not be true of the system. We present a theoretical framework for describing how to validate a model against the corresponding source code, and an implementation of the framework using symbolic execution and satisfiability modulo theories (SMT) solving. We evaluate our procedure on a number of case studies, including the Bochs address translation logic, a component of the Berkeley Packet Filter, the TCAS suite, the FTP server from GNU Inetutils, and a component of the XMHF hypervisor. Our results show that even for small, well understood code bases, a hand-written model is likely to have errors. For example, in the model for the Bochs address translation logic - a small model of only 300 lines of code that was vigorously used…

Subjects/Keywords: Computer science; Emulators; Hypervisors; Model checking; Model validation; Security

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Sturton, C. (2013). Secure Virtualization with Formal Methods. (Thesis). University of California – Berkeley. Retrieved from http://www.escholarship.org/uc/item/59q2n05r

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

Sturton, Cynthia. “Secure Virtualization with Formal Methods.” 2013. Thesis, University of California – Berkeley. Accessed January 19, 2020. http://www.escholarship.org/uc/item/59q2n05r.

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

MLA Handbook (7^th Edition):

Sturton, Cynthia. “Secure Virtualization with Formal Methods.” 2013. Web. 19 Jan 2020.

Vancouver:

Sturton C. Secure Virtualization with Formal Methods. [Internet] [Thesis]. University of California – Berkeley; 2013. [cited 2020 Jan 19]. Available from: http://www.escholarship.org/uc/item/59q2n05r.

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

Council of Science Editors:

Sturton C. Secure Virtualization with Formal Methods. [Thesis]. University of California – Berkeley; 2013. Available from: http://www.escholarship.org/uc/item/59q2n05r

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