You searched for subject:(Formal verification).
Showing records 1 – 30 of
469 total matches.
◁ [1] [2] [3] [4] [5] … [16] ▶
University of Waterloo
1.
Shehata, Hazem.
Formal Verification of Instruction Dependencies in Microprocessors.
Degree: 2011, University of Waterloo
URL: http://hdl.handle.net/10012/6102 
► In microprocessors, achieving an efficient utilization of the execution units is a key factor in improving performance. However, maintaining an uninterrupted flow of instructions is…
(more)
▼ In microprocessors, achieving an efficient utilization of the execution units is a key factor in improving performance. However, maintaining an uninterrupted flow of instructions is a challenge due to the data and control dependencies between instructions of a program. Modern microprocessors employ aggressive optimizations trying to keep their execution units busy without violating inter-instruction dependencies. Such complex optimizations may cause subtle implementation flaws that can be hard to detect using conventional simulation-based verification techniques.
Formal verification is known for its ability to discover design flaws that may go undetected using conventional verification techniques. However, with formal verification come two major challenges. First, the correctness of the implementation needs to be defined formally. Second, formal verification is often hard to apply at the scale of realistic implementations.
In this thesis, we present a formal verification strategy to guarantee that a microprocessor implementation preserves both data and control dependencies among instructions. Throughout our strategy, we address the two major challenges associated with formal verification: correctness and scalability.
We address the correctness challenge by specifying our correctness in the context of generic pipelines. Unlike conventional pipeline hazard rules, we make no distinction between the data and control aspects. Instead, we describe the relationship between a producer instruction and a consumer instruction in a way such that both instructions can speculatively read their source operands, speculatively write their results, and go out of their program order during execution. In addition to supporting branch and value prediction, our correctness criteria allow the implementation to discard (squash) or replay instructions while being executed.
We address the scalability challenge in three ways: abstraction, decomposition, and induction. First, we state our inter-instruction dependency correctness criteria in terms of read and write operations without making reference to data values. Consequently, our correctness criteria can be verified for implementations with abstract datapaths. Second, we decompose our correctness criteria into a set of smaller obligations that are easier to verify. All these obligations can be expressed as properties within the Syntactically-Safe fragment of Linear Temporal Logic (SSLTL). Third, we introduce a technique to verify SSLTL properties by induction, and prove its soundness and completeness.
To demonstrate our overall strategy, we verified a term-level model of an out-of-order speculative processor. The processor model implements register renaming using a P6-style reorder buffer and branch prediction with a hybrid (discard-replay) recovery mechanism. The verification obligations (expressed in SSLTL) are checked using a tool implementing our inductive technique. Our tool, named Tahrir, is built on top of a generic interface to SMT solvers and can be generally used for…
Subjects/Keywords: Formal Verification; Microprocessors
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Shehata, H. (2011). Formal Verification of Instruction Dependencies in Microprocessors. (Thesis). University of Waterloo. Retrieved from http://hdl.handle.net/10012/6102
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
Chicago Manual of Style (16th Edition):
Shehata, Hazem. “Formal Verification of Instruction Dependencies in Microprocessors.” 2011. Thesis, University of Waterloo. Accessed January 17, 2021.
http://hdl.handle.net/10012/6102.
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
MLA Handbook (7th Edition):
Shehata, Hazem. “Formal Verification of Instruction Dependencies in Microprocessors.” 2011. Web. 17 Jan 2021.
Vancouver:
Shehata H. Formal Verification of Instruction Dependencies in Microprocessors. [Internet] [Thesis]. University of Waterloo; 2011. [cited 2021 Jan 17].
Available from: http://hdl.handle.net/10012/6102.
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
Council of Science Editors:
Shehata H. Formal Verification of Instruction Dependencies in Microprocessors. [Thesis]. University of Waterloo; 2011. Available from: http://hdl.handle.net/10012/6102
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
Texas A&M University
2.
Zheng, Qingran.
Hybrid Verification for Analog and Mixed-signal Circuits.
Degree: MS, Computer Engineering, 2017, Texas A&M University
URL: http://hdl.handle.net/1969.1/173237
► With increasing design complexity and reliability requirements, analog and mixedsignal (AMS) verification manifests itself as a key bottleneck. While formal methods and machine learning have…
(more)
▼ With increasing design complexity and reliability requirements, analog and mixedsignal
(AMS)
verification manifests itself as a key bottleneck. While
formal methods and
machine learning have been proposed for AMS
verification, these two types of techniques
suffer from their own limitations, with the former being specifically limited by scalability
and the latter by inherent errors in learning-based models.
We present a new direction in AMS
verification by proposing a hybrid
formal/machinelearning-
based
verification technique (HFMV) to combine the best of the two worlds.
HFMV builds formalism on the top of a machine learning model to verify AMS circuits
efficiently while meeting a user-specified confidence level. Guided by
formal checks,
HFMV intelligently explores the high-dimensional parameter space of a given design by
iteratively improving the machine learning model. As a result, it leads to accurate failure
prediction in the case of a failing circuit or a reliable pass decision in the case of a good
circuit. Our experimental results demonstrate that the proposed HFMV approach is capable
of identifying hard-to-find failures which are completely missed by a huge number
of random simulation samples while significantly cutting down training sample size and
verification cycle time.
Advisors/Committee Members: Li, Peng (advisor), Choi, Gwan S. (committee member), Hoyos, Sebastian (committee member), Huang, Jianhua (committee member).
Subjects/Keywords: AMS Verification; Formal Verification; Machine Learning
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Zheng, Q. (2017). Hybrid Verification for Analog and Mixed-signal Circuits. (Masters Thesis). Texas A&M University. Retrieved from http://hdl.handle.net/1969.1/173237
Chicago Manual of Style (16th Edition):
Zheng, Qingran. “Hybrid Verification for Analog and Mixed-signal Circuits.” 2017. Masters Thesis, Texas A&M University. Accessed January 17, 2021.
http://hdl.handle.net/1969.1/173237.
MLA Handbook (7th Edition):
Zheng, Qingran. “Hybrid Verification for Analog and Mixed-signal Circuits.” 2017. Web. 17 Jan 2021.
Vancouver:
Zheng Q. Hybrid Verification for Analog and Mixed-signal Circuits. [Internet] [Masters thesis]. Texas A&M University; 2017. [cited 2021 Jan 17].
Available from: http://hdl.handle.net/1969.1/173237.
Council of Science Editors:
Zheng Q. Hybrid Verification for Analog and Mixed-signal Circuits. [Masters Thesis]. Texas A&M University; 2017. Available from: http://hdl.handle.net/1969.1/173237
University of New South Wales
3.
Greenaway, David.
Automated proof-producing abstraction of C code.
Degree: Computer Science & Engineering, 2014, University of New South Wales
URL: http://handle.unsw.edu.au/1959.4/54260
;
https://unsworks.unsw.edu.au/fapi/datastream/unsworks:13743/SOURCE02?view=true
► Before software can be formally reasoned about, it must first be represented in some form of logic. There are two approaches to carrying out this…
(more)
▼ Before software can be formally reasoned about, it must first be represented in some form of logic. There are two approaches to carrying out this translation: the first is to generate an idealised representation of the program, convenient for reasoning about. The second, safer approach is to perform a precise, conservative translation, at the cost of burdening
verification efforts with low-level implementation details. In this thesis, we present methods for bridging the gap between these two approaches. In particular, we describe algorithms for automatically abstracting low-level C code semantics into a higher level representation. These translations include simplifying program control flow, converting finite machine arithmetic into idealised integers, and translating the byte-level C memory model to a split heap model. The generated abstractions are easier to reason about than the input representations, which in turn increases the productivity of
formal verification techniques. Critically, we guarantee soundness by automatically generating proofs that our abstractions are correct. Previous work carrying out such transformations has either done so using unverified translations, or required significant manual proof engineering effort. Our algorithms are implemented in a new tool named AutoCorres, built on the Isabelle/HOL interactive theorem prover. We demonstrate the effectiveness of our abstractions in a number of case studies, and show the scalability of AutoCorres by translating real-world programs consisting of tens of thousands of lines of code. While our work focuses on a subset of the C programming language, we believe most of our algorithms are also applicable to other imperative languages, such as Java or C#.
Advisors/Committee Members: Klein, Gerwin, University of New South Wales and NICTA, Andronick, June, University of New South Wales and NICTA, Elphinstone, Kevin, University of New South Wales and NICTA.
Subjects/Keywords: Interactive Theorem Proving; Formal Verification; Program Verification
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Greenaway, D. (2014). Automated proof-producing abstraction of C code. (Doctoral Dissertation). University of New South Wales. Retrieved from http://handle.unsw.edu.au/1959.4/54260 ; https://unsworks.unsw.edu.au/fapi/datastream/unsworks:13743/SOURCE02?view=true
Chicago Manual of Style (16th Edition):
Greenaway, David. “Automated proof-producing abstraction of C code.” 2014. Doctoral Dissertation, University of New South Wales. Accessed January 17, 2021.
http://handle.unsw.edu.au/1959.4/54260 ; https://unsworks.unsw.edu.au/fapi/datastream/unsworks:13743/SOURCE02?view=true.
MLA Handbook (7th Edition):
Greenaway, David. “Automated proof-producing abstraction of C code.” 2014. Web. 17 Jan 2021.
Vancouver:
Greenaway D. Automated proof-producing abstraction of C code. [Internet] [Doctoral dissertation]. University of New South Wales; 2014. [cited 2021 Jan 17].
Available from: http://handle.unsw.edu.au/1959.4/54260 ; https://unsworks.unsw.edu.au/fapi/datastream/unsworks:13743/SOURCE02?view=true.
Council of Science Editors:
Greenaway D. Automated proof-producing abstraction of C code. [Doctoral Dissertation]. University of New South Wales; 2014. Available from: http://handle.unsw.edu.au/1959.4/54260 ; https://unsworks.unsw.edu.au/fapi/datastream/unsworks:13743/SOURCE02?view=true
Rice University
4.
Song, Daniel W.
The Design and Implementation of a Verified File System with End-to-End Data Integrity.
Degree: PhD, Engineering, 2020, Rice University
URL: http://hdl.handle.net/1911/108425
► Despite significant research and engineering efforts, many of today's important computer systems suffer from bugs. To increase the reliability of software systems, recent work has…
(more)
▼ Despite significant research and engineering efforts, many of today's
important computer systems suffer from bugs.
To increase the reliability of software systems, recent work has
applied
formal verification to certify the correctness of
such systems, with recent successes including certified file systems
and certified cryptographic protocols, albeit using quite different
proof tactics and toolchains. Unifying these concepts, we present the
first certified file system that uses cryptographic primitives to
protect itself against tampering. Our certified file system defends
against adversaries that might wish to tamper with the raw disk. Such
an ``untrusted storage'' threat model captures the behavior of storage
devices that might silently return erroneous bits as well as
adversaries who might have limited access to a disk, perhaps while in
transit.
In this paper, we present IFSCQ, a certified cryptographic file system with strong integrity guarantees.
IFSCQ combines and extends work on cryptographic file systems and formally certified file systems to prove that our design is correct.
It is the first certified file system that is secure against strong adversaries that can maliciously corrupt on-disk data and metadata, including attempting to roll back the disk to earlier versions of valid data.
IFSCQ achieves this by constructing a Merkle hash tree of the whole disk, and by proving that tampered disk blocks will always be detected if they ever occur.
We demonstrate that IFSCQ runs with reasonable overhead while detecting several kinds of attacks.
Advisors/Committee Members: Wallach, Dan S (advisor).
Subjects/Keywords: software security; systems; formal verification
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Song, D. W. (2020). The Design and Implementation of a Verified File System with End-to-End Data Integrity. (Doctoral Dissertation). Rice University. Retrieved from http://hdl.handle.net/1911/108425
Chicago Manual of Style (16th Edition):
Song, Daniel W. “The Design and Implementation of a Verified File System with End-to-End Data Integrity.” 2020. Doctoral Dissertation, Rice University. Accessed January 17, 2021.
http://hdl.handle.net/1911/108425.
MLA Handbook (7th Edition):
Song, Daniel W. “The Design and Implementation of a Verified File System with End-to-End Data Integrity.” 2020. Web. 17 Jan 2021.
Vancouver:
Song DW. The Design and Implementation of a Verified File System with End-to-End Data Integrity. [Internet] [Doctoral dissertation]. Rice University; 2020. [cited 2021 Jan 17].
Available from: http://hdl.handle.net/1911/108425.
Council of Science Editors:
Song DW. The Design and Implementation of a Verified File System with End-to-End Data Integrity. [Doctoral Dissertation]. Rice University; 2020. Available from: http://hdl.handle.net/1911/108425
Georgia Tech
5.
Bobek, Jan.
Hidden fallacies in formally verified systems.
Degree: MS, Computer Science, 2020, Georgia Tech
URL: http://hdl.handle.net/1853/62855
► Formal verification or formal methods represent a rising trend in approaches to correct software construction, i.e. they help us answer the question of how to…
(more)
▼ Formal verification or
formal methods represent a rising trend in approaches to correct software construction, i.e. they help us answer the question of how to build software that contains no errors, colloquially known as “bugs.” They achieve their goal by providing means for stating theorems about the program under test, and for proving such theorems by methods well-known in mathematics, specifically in mathematical logic. Of course,
formal methods are no silver bullet and come with their own set of limitations, the most significant of which is extremely difficult scalability with software size. In spite of the limitations, there have been important breakthroughs in their applications over the last 10–15 years, e.g. Leroy’s CompCert (verified C compiler) or Klein’s seL4 (verified implementation of the L4 microkernel). However, how bug-free is verified software in reality?
Formal methods make a bold claim that there are indeed no bugs in verified software, or more formally, that the software precisely implements its specification. Unfortunately, as an empirical study from 2017 by Fonseca et al. shows, it may be just too easy to introduce errors into the specification itself, either in form of mistakes (“specification bugs”), or in form of unanticipated assumptions. This thesis aims to take a broader look at formally verified software and
formal verification systems, and identify the most common problems in
formal methods’ applications, leading to bugs still being present in verified software. In particular, the main contribution of this thesis is an overview of several software projects employing
formal methods at their core; an empirical study of “real-world” guarantees that the
formal verification systems afford them; and, consequently, showcases of different approaches to verified software, along with their strengths and weaknesses. We believe that understanding how
formal methods succeed and fail (or rather, how they can be misused) will be helpful in determining when they become an attractive and worthwhile choice for more ordinary (as opposed to top mission-critical) software. Indeed, we hope that this thesis may serve as an introductory guide for new projects to the guarantees provided by
formal verification; correctness guarantees much stronger than those given by software testing. We hope that in long-term, entry barrier to
formal verification will become sufficiently low for
formal methods to enter mainstream software development, making developers more confident about their programs, and hopefully ridding our world of “buggy” software once and for all.
Advisors/Committee Members: Kim, Taesoo (advisor), Saltaformaggio, Brendan (committee member), Pu, Calton (committee member), Gavrilovska, Ada (committee member).
Subjects/Keywords: Formal verification; Fuzzing; File systems
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Bobek, J. (2020). Hidden fallacies in formally verified systems. (Masters Thesis). Georgia Tech. Retrieved from http://hdl.handle.net/1853/62855
Chicago Manual of Style (16th Edition):
Bobek, Jan. “Hidden fallacies in formally verified systems.” 2020. Masters Thesis, Georgia Tech. Accessed January 17, 2021.
http://hdl.handle.net/1853/62855.
MLA Handbook (7th Edition):
Bobek, Jan. “Hidden fallacies in formally verified systems.” 2020. Web. 17 Jan 2021.
Vancouver:
Bobek J. Hidden fallacies in formally verified systems. [Internet] [Masters thesis]. Georgia Tech; 2020. [cited 2021 Jan 17].
Available from: http://hdl.handle.net/1853/62855.
Council of Science Editors:
Bobek J. Hidden fallacies in formally verified systems. [Masters Thesis]. Georgia Tech; 2020. Available from: http://hdl.handle.net/1853/62855
University of Edinburgh
6.
Butler, David Thomas.
Formalising cryptography using CryptHOL.
Degree: PhD, 2020, University of Edinburgh
URL: https://doi.org/10.7488/era/510
;
https://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.814924
► Security proofs are now a cornerstone of modern cryptography. Provable security has greatly increased the level of rigour of the security statements, however proofs of…
(more)
▼ Security proofs are now a cornerstone of modern cryptography. Provable security has greatly increased the level of rigour of the security statements, however proofs of these statements often present informal or incomplete arguments. In fact, many proofs are still considered to be unverifiable due to their complexity and length. Formal methods offers one way to establish far higher levels of rigour and confidence in proofs and tools have been developed to formally reason about cryptography and obtain machine-checked proof of security statements. In this thesis we use the CryptHOL framework, embedded inside Isabelle/HOL, to reason about cryptography. First we consider two fundamental cryptographic primitives: Σ-protocols and Commitment Schemes. Σ-protocols allow a Prover to convince a Verifier that they know a value x without revealing anything beyond that the fact they know x. Commitment Schemes allow a Committer to commit to a chosen value while keeping it hidden, and be able to reveal the value at a later time. We first formalise abstract definitions for both primitives and then prove multiple case studies and general constructions secure. A highlight of this part of the work is our general proof of the construction of commitment schemes from Σ-protocols. This result means that within our framework for every Σ-protocol proven secure we obtain, for free, a new commitment scheme that is secure also. We also consider compound Σ-protocols that allow for the proof of AND and OR statements. As a result of our formalisation effort here we are able to highlight which of the different definitions of Σ-protocols from the literature is the correct one; in particular we show that the most widely used definition of Σ-protocols is not sufficient for the OR construction. To show our frameworks are usable we also formalise numerous other case studies of Σ-protocols and commitment schemes, namely: the Σ-protocols by Schnorr, Chaum-Pedersen, and Okamoto; and the commitment schemes by Rivest and Pedersen. Second, we consider Multi-Party Computation (MPC). MPC allows for multiple distrusting parties to jointly compute functions over their inputs while keeping their inputs private. We formalise frameworks to abstractly reason about two party security in both the semi-honest and malicious adversary models and then instantiate them for numerous case studies and examples. A particularly important two party MPC protocol is Oblivious Transfer} (OT) which, in its simplest form, allows the Receiver to choose one of two messages from the other party, the Sender; the Receiver learns nothing of the other message held by the sender and the Sender does not learn which message the Receiver chose. Due to OTs fundamental importance we choose to focus much of our formalisation here, a highlight of this section of our work is our general proof of security of a 1-out-of-2 OT (OT21) protocol in the semi-honest model that relies on Extended Trapdoor Permutations (ETPs). We formalise the construction assuming only that an ETP exists meaning any…
Subjects/Keywords: formal verification; cryptography; Isabelle/HOL
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Butler, D. T. (2020). Formalising cryptography using CryptHOL. (Doctoral Dissertation). University of Edinburgh. Retrieved from https://doi.org/10.7488/era/510 ; https://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.814924
Chicago Manual of Style (16th Edition):
Butler, David Thomas. “Formalising cryptography using CryptHOL.” 2020. Doctoral Dissertation, University of Edinburgh. Accessed January 17, 2021.
https://doi.org/10.7488/era/510 ; https://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.814924.
MLA Handbook (7th Edition):
Butler, David Thomas. “Formalising cryptography using CryptHOL.” 2020. Web. 17 Jan 2021.
Vancouver:
Butler DT. Formalising cryptography using CryptHOL. [Internet] [Doctoral dissertation]. University of Edinburgh; 2020. [cited 2021 Jan 17].
Available from: https://doi.org/10.7488/era/510 ; https://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.814924.
Council of Science Editors:
Butler DT. Formalising cryptography using CryptHOL. [Doctoral Dissertation]. University of Edinburgh; 2020. Available from: https://doi.org/10.7488/era/510 ; https://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.814924
Texas A&M University
7.
Kottapalli, Venkateshwar.
Formal Verification of a MESI-based Cache Implementation.
Degree: MS, Computer Engineering, 2017, Texas A&M University
URL: http://hdl.handle.net/1969.1/165866
► Cache coherency is crucial to multi-core systems with a shared memory programming model. Coherency protocols have been formally verified at the architectural level with relative…
(more)
▼ Cache coherency is crucial to multi-core systems with a shared memory programming model. Coherency protocols have been formally verified at the architectural level with relative ease. However, several subtle issues creep into the hardware realization of cache in a multi-processor environment. The assumption, made in the abstract model, that state transitions are atomic, is invalid for the HDL implementation. Each transition is composed of many concurrent multi-core operations. As a result, even with a blocking bus, several transient states come into existence. Most modern processors optimize communication with a split-transaction bus, this results in further transient states and race conditions. Therefore, the design and
verification of cache coherency is increasingly complex and challenging.
Simulation techniques are insufficient to ensure memory consistency and the absence of deadlock, livelock, and starvation. At best, it is tediously complex and time consuming to reach confidence in functionality with simulation.
Formal methods are ideally suited to identify the numerous race conditions and subtle failures. In this study, we perform
formal property
verification on the RTL of a multi-core level-1 cache design based on snooping MESI protocol. We demonstrate full-proof
verification of the coherence module in JasperGold using complexity reduction techniques through parameterization. We verify that the assumptions needed to constrain inputs of the stand-alone cache coherence module are satisfied as valid assertions in the instantiation environment. We compare results obtained from
formal property
verification against a state-of-the-art UVM environment. We highlight the benefits of a synergistic collaboration between simulation and
formal techniques. We present
formal analysis as a generic toolkit with numerous usage models in the digital design process.
Advisors/Committee Members: Tyagi, Aakash (advisor), Walker, Duncan M (committee member), Hu, Jiang (committee member).
Subjects/Keywords: Verification; Cache; Coherence; Memory Consistency; Formal Verification; Model Checking; RTL; Formal Property Verification; UVM; MESI
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Kottapalli, V. (2017). Formal Verification of a MESI-based Cache Implementation. (Masters Thesis). Texas A&M University. Retrieved from http://hdl.handle.net/1969.1/165866
Chicago Manual of Style (16th Edition):
Kottapalli, Venkateshwar. “Formal Verification of a MESI-based Cache Implementation.” 2017. Masters Thesis, Texas A&M University. Accessed January 17, 2021.
http://hdl.handle.net/1969.1/165866.
MLA Handbook (7th Edition):
Kottapalli, Venkateshwar. “Formal Verification of a MESI-based Cache Implementation.” 2017. Web. 17 Jan 2021.
Vancouver:
Kottapalli V. Formal Verification of a MESI-based Cache Implementation. [Internet] [Masters thesis]. Texas A&M University; 2017. [cited 2021 Jan 17].
Available from: http://hdl.handle.net/1969.1/165866.
Council of Science Editors:
Kottapalli V. Formal Verification of a MESI-based Cache Implementation. [Masters Thesis]. Texas A&M University; 2017. Available from: http://hdl.handle.net/1969.1/165866
University of Utah
8.
Xu, Yang.
Algorithms for automatic generation of relative timing constraints.
Degree: PhD, Electrical & Computer Engineering, 2011, University of Utah
URL: http://content.lib.utah.edu/cdm/singleitem/collection/etd3/id/197/rec/177
► Asynchronous circuits exhibit impressive power and performance benefits over its synchronous counterpart. Asynchronous system design, however, is not widely adopted due to the fact that…
(more)
▼ Asynchronous circuits exhibit impressive power and performance benefits over its synchronous counterpart. Asynchronous system design, however, is not widely adopted due to the fact that it lacks an equivalent support of CAD tools and requires deep expertise in asynchronous circuit design. A relative timing (RT) based asynchronous asynchronous commercial CAD tools was recently proposed. This design flow enables engineers who are proficient in using synchronous design and CAD flow to more easily switch to asynchronous design without asynchronous experience while retaining the asynchronous benefits of power and performance. Relative timing constraints are the key step to this design flow, and were generated manually by the designer based on his/her intuition and understanding of the circuit logic and structure. This process was quite time-consuming and error-prone. This dissertation presents an algorithm that automatically generates a set of relative timing constraints to guarantee the correctness of a circuit with the aid of a formal verification engine – Analyze. The algorithms have been implemented in a tool called ARTIST (Automatic Relative Timing Identifier based on Signal Traces). Automatic generation of relative timing constraints relies on manipulation, such as searching and backtracking, of a trace status tableau that is built based on the counter example signal trace returned from the formal verification engine. The underlying mechanism of relative timing is to force signal ordering on the labeled transition graph of the system to restrict its reachability to failure states such that the circuit implementation conforms to the specification. Examples from a simple C-Element to complex six-four GasP circuits are demonstrated to show how this technique is applied to real problems. The set of relative timing constraints generated by ARTIST is compared against the set of hand generated constraints in terms of efficiency and quality. Over 100 four-phase handshake controller protocols have been verified through ARTIST and Analyze. ARTSIT vastly reduces the design time as compared to hand generation which may take days or even months to achieve a solution set of RT constraints. The quality of ARTIST generated constraints is also shown to be as good as hand generation.
Subjects/Keywords: Asynchronous circuits; Formal verification; Relative timing
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Xu, Y. (2011). Algorithms for automatic generation of relative timing constraints. (Doctoral Dissertation). University of Utah. Retrieved from http://content.lib.utah.edu/cdm/singleitem/collection/etd3/id/197/rec/177
Chicago Manual of Style (16th Edition):
Xu, Yang. “Algorithms for automatic generation of relative timing constraints.” 2011. Doctoral Dissertation, University of Utah. Accessed January 17, 2021.
http://content.lib.utah.edu/cdm/singleitem/collection/etd3/id/197/rec/177.
MLA Handbook (7th Edition):
Xu, Yang. “Algorithms for automatic generation of relative timing constraints.” 2011. Web. 17 Jan 2021.
Vancouver:
Xu Y. Algorithms for automatic generation of relative timing constraints. [Internet] [Doctoral dissertation]. University of Utah; 2011. [cited 2021 Jan 17].
Available from: http://content.lib.utah.edu/cdm/singleitem/collection/etd3/id/197/rec/177.
Council of Science Editors:
Xu Y. Algorithms for automatic generation of relative timing constraints. [Doctoral Dissertation]. University of Utah; 2011. Available from: http://content.lib.utah.edu/cdm/singleitem/collection/etd3/id/197/rec/177
Tampere University
9.
Biswas, Prasun.
Model-to-Model Transformation Of Nuclear Industry I&C Logic To Assist Model Checking
.
Degree: 2020, Tampere University
URL: https://trepo.tuni.fi/handle/10024/121539
► The demand for electricity has increased proportionately with massive urbanisation and in-dustrialisation. Nuclear energy is a strong candidate which can be one of the solutions…
(more)
▼ The demand for electricity has increased proportionately with massive urbanisation and in-dustrialisation. Nuclear energy is a strong candidate which can be one of the solutions to ca-ter to this massive demand for energy. Nuclear resources have the benefit of enormous ener-gy density, low carbon footprint, cheap operating cost and production reliability. Even though it is deemed as a dependable and economically viable option, it is limited by safety concerns, unfortunate accidents can cause monumental and long-lasting consequences. On the other hand, if critically examined, thoroughly tested and flawlessly implemented, the decision-makers can opt for nuclear source. Thus utilising nuclear resources will call for an error-proof instrumentation and control system to observe and ensure safe operation. Model verification plays a vital role in critical analysis of I & C system, it checks all the possibilities the system may reach, and thus provide a model to develop an I&C safety system.
An industrial operation may suffer from unknown component failure and design error, but its safety-critical system must be able to strictly prohibit these undesired events in the system before causing any major accident. “Model Checking” is a mathematical deterministic tool for logic design verification, which has been proven to be effective for detecting design errors in the system. Granted that, Instrumentation and control system starts with logic design at the preliminary phase, a model checking tool can efficiently identify design faults by exhaustive analysis. NuSMV is such a tool, which provides simpler syntax, that can represent the system as logical states with simple data structures. Analysts write SMV files to represent the system available as proprietary non-standard machine-readable diagrams. This thesis proposes an automation step towards diagram import in a verification tool and implements an intermediate data representation.
This thesis provides a perception of various technologies relevant to broader authentication process of a safety system covering from design to verification tools. The state-of-the-art model-checking practice is discussed briefly. Subsequently, a number of logical instrumenta-tion and control diagrams, drawn in Microsoft VISIO tool, are analysed and processed to au-tomatically create an intermediate component network consisting of Function Block elements. A significant effort is spent to partially generate NuSMV code from the retrieved component data to assist the model checking of the system. Finally, the thesis is concluded with a synop-sis of the work done and future development scope.
Subjects/Keywords: Model Transformation
;
Formal Verification
;
Model Checking
;
NuSMV
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Biswas, P. (2020). Model-to-Model Transformation Of Nuclear Industry I&C Logic To Assist Model Checking
. (Masters Thesis). Tampere University. Retrieved from https://trepo.tuni.fi/handle/10024/121539
Chicago Manual of Style (16th Edition):
Biswas, Prasun. “Model-to-Model Transformation Of Nuclear Industry I&C Logic To Assist Model Checking
.” 2020. Masters Thesis, Tampere University. Accessed January 17, 2021.
https://trepo.tuni.fi/handle/10024/121539.
MLA Handbook (7th Edition):
Biswas, Prasun. “Model-to-Model Transformation Of Nuclear Industry I&C Logic To Assist Model Checking
.” 2020. Web. 17 Jan 2021.
Vancouver:
Biswas P. Model-to-Model Transformation Of Nuclear Industry I&C Logic To Assist Model Checking
. [Internet] [Masters thesis]. Tampere University; 2020. [cited 2021 Jan 17].
Available from: https://trepo.tuni.fi/handle/10024/121539.
Council of Science Editors:
Biswas P. Model-to-Model Transformation Of Nuclear Industry I&C Logic To Assist Model Checking
. [Masters Thesis]. Tampere University; 2020. Available from: https://trepo.tuni.fi/handle/10024/121539
University of Ottawa
10.
Sistany, Bahman.
A Certified Core Policy Language
.
Degree: 2016, University of Ottawa
URL: http://hdl.handle.net/10393/34865
► We present the design and implementation of a Certified Core Policy Language (ACCPL) that can be used to express access-control rules and policies. Although full-blown…
(more)
▼ We present the design and implementation of a Certified Core Policy Language (ACCPL) that can be used to express access-control rules and policies. Although full-blown access-control policy languages such as eXtensible Access Control Markup Language (XACML) [OAS13] already exist, because access rules in such languages are often expressed in a declarative manner using fragments of a natural language like English, it isn’t alwaysclear what the intended behaviour of the system encoded in these access rules should be. To remedy this ambiguity, formal specification of how an access-control mechanism should behave, is typically given in some sort of logic, often a subset of first order logic. To show that an access-control system actually behaves correctly with respect to its specification,
proofs are needed, however the proofs that are often presented in the literature are hard or impossible to formally verify. The verification difficulty is partly due to the fact that the language used to do the proofs while mathematical in nature, utilizes intuitive justifications to derive the proofs. Intuitive language in proofs means that the proofs could be incomplete and/or contain subtle errors.
ACCPL is small by design. By small we refer to the size of the language; the syntax,
auxiliary definitions and the semantics of ACCPL only take a few pages to describe. This compactness allows us to concentrate on the main goal of this thesis which is the ability to reason about the policies written in ACCPL with respect to specific questions. By making the language compact, we have stayed away from completeness and expressive power in several directions. For example, ACCPL uses only a single policy combinator, the conjunction policy combinator. The design of ACCPL is therefore a trade-off between ease of formal proof of correctness and expressive power. We also consider ACCPL a core policy access-control language since we have retained the core features of many access-control policy languages. For instance ACCPL employs a single condition type called a “prerequisite” where other languages may have very expressive and rich sets of conditions.
Subjects/Keywords: access-control;
formal verification;
proofs;
policy language
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Sistany, B. (2016). A Certified Core Policy Language
. (Thesis). University of Ottawa. Retrieved from http://hdl.handle.net/10393/34865
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
Chicago Manual of Style (16th Edition):
Sistany, Bahman. “A Certified Core Policy Language
.” 2016. Thesis, University of Ottawa. Accessed January 17, 2021.
http://hdl.handle.net/10393/34865.
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
MLA Handbook (7th Edition):
Sistany, Bahman. “A Certified Core Policy Language
.” 2016. Web. 17 Jan 2021.
Vancouver:
Sistany B. A Certified Core Policy Language
. [Internet] [Thesis]. University of Ottawa; 2016. [cited 2021 Jan 17].
Available from: http://hdl.handle.net/10393/34865.
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
Council of Science Editors:
Sistany B. A Certified Core Policy Language
. [Thesis]. University of Ottawa; 2016. Available from: http://hdl.handle.net/10393/34865
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
University of Newcastle
11.
Hogavanaghatta Kumaraswamy, Jnanamurthy.
Model-driven engineering to enhance the reliability of software development by verifying system properties and detecting clones.
Degree: PhD, 2019, University of Newcastle
URL: http://hdl.handle.net/1959.13/1397849
► Research Doctorate - Doctor of Philosophy (PhD)
Computer software is used in almost every facet of day-to-day life, such as air conditioners, refrigerators, washing machines,…
(more)
▼ Research Doctorate - Doctor of Philosophy (PhD)
Computer software is used in almost every facet of day-to-day life, such as air conditioners, refrigerators, washing machines, transport systems, medical systems, and banking. This dependency gives rise to advantages, such as reductions in manual work and improvements in the quality of work. It is essential to ensure that the software that is used in the above-mentioned applications is correct, to avoid catastrophic failures. The aim of this research is twofold, as outlined below. Firstly, formal methods are used to ensure that the software specification for a system is accurate before implementation of that system. The use of formal methods in model-driven development requires a complete transformation of model-driven engineering (MDE) models to a formal model, and also a need to state specifications for verification after the transformation. There are several techniques to transform MDE models into formal models, but the model transformation is not enough to verify the system unless the specification is stated at the model level. Otherwise, the model designer has to know a formal specification language to specify the properties for verification. Additionally, existing modelling frameworks consume additional time during manual inputting of formal specifications to formal verification tools. Furthermore, existing methods achieve less in accuracy (percentage of specifications specified against required specifications during verification) and may require additional documentation of specifications due to, a designer may forget to include all required specifications in the verification tools for verification due to the larger application.To solve this problem, we use domain-specific modelling techniques to design a modelling framework that allows the specification of formal properties at the model level. The model and specifications are then extracted and transformed into a formal model and formal specifications for verification. The designed modelling framework also provides semantics to derive test cases. The framework performs well in coverage criteria during model-based development, and reduces the time and cost of verification by enabling automation. Secondly, software program classification plays a vital role in the identification of similar functionality, which can be considered as software clones, for re-usability, code optimisation and to avoid bug traversal. There are many existing methods for identifying software clones; however, these methods focus on structure-based analysis to detect clones at the code level. We consider the clone detection process at two levels: model and code (considering MDE models and IEC 61131-3 programs). Furthermore, we present a novel approach to detecting clones at model level using semantic-based analysis. Our method is based on model checking that involves mathematical analysis. Our process is tested with control-flow-based models and yields good results in the detection of model clones. To identify clones in IEC 61131-3…
Advisors/Committee Members: University of Newcastle. Faculty of Engineering & Built Environment, School of Electrical Engineering and Computing.
Subjects/Keywords: formal verification; model-driven engineering; software clones
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Hogavanaghatta Kumaraswamy, J. (2019). Model-driven engineering to enhance the reliability of software development by verifying system properties and detecting clones. (Doctoral Dissertation). University of Newcastle. Retrieved from http://hdl.handle.net/1959.13/1397849
Chicago Manual of Style (16th Edition):
Hogavanaghatta Kumaraswamy, Jnanamurthy. “Model-driven engineering to enhance the reliability of software development by verifying system properties and detecting clones.” 2019. Doctoral Dissertation, University of Newcastle. Accessed January 17, 2021.
http://hdl.handle.net/1959.13/1397849.
MLA Handbook (7th Edition):
Hogavanaghatta Kumaraswamy, Jnanamurthy. “Model-driven engineering to enhance the reliability of software development by verifying system properties and detecting clones.” 2019. Web. 17 Jan 2021.
Vancouver:
Hogavanaghatta Kumaraswamy J. Model-driven engineering to enhance the reliability of software development by verifying system properties and detecting clones. [Internet] [Doctoral dissertation]. University of Newcastle; 2019. [cited 2021 Jan 17].
Available from: http://hdl.handle.net/1959.13/1397849.
Council of Science Editors:
Hogavanaghatta Kumaraswamy J. Model-driven engineering to enhance the reliability of software development by verifying system properties and detecting clones. [Doctoral Dissertation]. University of Newcastle; 2019. Available from: http://hdl.handle.net/1959.13/1397849
University of Colorado
12.
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 »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Hassan, Z. (2014). Incremental, Inductive Model Checking. (Doctoral Dissertation). University of Colorado. Retrieved from https://scholar.colorado.edu/ecen_gradetds/86
Chicago Manual of Style (16th Edition):
Hassan, Zyad. “Incremental, Inductive Model Checking.” 2014. Doctoral Dissertation, University of Colorado. Accessed January 17, 2021.
https://scholar.colorado.edu/ecen_gradetds/86.
MLA Handbook (7th Edition):
Hassan, Zyad. “Incremental, Inductive Model Checking.” 2014. Web. 17 Jan 2021.
Vancouver:
Hassan Z. Incremental, Inductive Model Checking. [Internet] [Doctoral dissertation]. University of Colorado; 2014. [cited 2021 Jan 17].
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 Manchester
13.
Carter, Rebekah.
Verification of liveness properties on hybrid dynamical systems.
Degree: PhD, 2013, University of Manchester
URL: https://www.research.manchester.ac.uk/portal/en/theses/verification-of-liveness-properties-on-hybrid-dynamical-systems(8817319c-a63f-4cf3-927d-a2ddf69139b4).html
;
http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.576886
► A hybrid dynamical system is a mathematical model for a part of the real world where discrete and continuous parts interact with each other. Typically…
(more)
▼ A hybrid dynamical system is a mathematical model for a part of the real world where discrete and continuous parts interact with each other. Typically such systems are complex, and it is difficult to know how they will behave for general parameters and initial conditions. However, the method of formal verification gives us the ability to prove automatically that certain behaviour does or does not happen for a range of parameters in a system. The challenge is then to define suitable methods for proving properties on hybrid systems.This thesis looks at using formal verification for proving liveness properties on hybrid systems: a liveness property says that something good eventually happens in the system. This work presents the theoretical background and practical application of various methods for proving and disproving inevitability properties (a type of liveness) in different classes of hybrid systems. The methods combine knowledge of dynamical behaviour of a system with the brute-force approach of model checking, in order to make the most of the benefits of both sides. The work on proving liveness properties is based on abstraction of dynamical systems to timed automata. This thesis explores the limits of a pre-defined abstraction method, adds some dynamical knowledge to the method, and shows that this improvement makes liveness properties provable in certain continuous dynamical systems. The limits are then pushed further to see how this method can be used for piecewise-continuous dynamical systems. The resulting algorithms are implemented for both classes of systems.In order to disprove liveness properties in hybrid systems a novel framework is proposed, using a new property called deadness. Deadness is a dynamically-aware property of the hybrid system which, if true, disproves the liveness property by means of a finite execution: we usually require an infinite execution to disprove a liveness property. An algorithm is proposed which uses dynamical properties of hybrid systems to derive deadness properties automatically, and the implementation of this algorithm is discussed and applied to a simplified model of an oilwell drillstring.
Subjects/Keywords: 511; Hybrid systems; Formal verification; Liveness
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Carter, R. (2013). Verification of liveness properties on hybrid dynamical systems. (Doctoral Dissertation). University of Manchester. Retrieved from https://www.research.manchester.ac.uk/portal/en/theses/verification-of-liveness-properties-on-hybrid-dynamical-systems(8817319c-a63f-4cf3-927d-a2ddf69139b4).html ; http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.576886
Chicago Manual of Style (16th Edition):
Carter, Rebekah. “Verification of liveness properties on hybrid dynamical systems.” 2013. Doctoral Dissertation, University of Manchester. Accessed January 17, 2021.
https://www.research.manchester.ac.uk/portal/en/theses/verification-of-liveness-properties-on-hybrid-dynamical-systems(8817319c-a63f-4cf3-927d-a2ddf69139b4).html ; http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.576886.
MLA Handbook (7th Edition):
Carter, Rebekah. “Verification of liveness properties on hybrid dynamical systems.” 2013. Web. 17 Jan 2021.
Vancouver:
Carter R. Verification of liveness properties on hybrid dynamical systems. [Internet] [Doctoral dissertation]. University of Manchester; 2013. [cited 2021 Jan 17].
Available from: https://www.research.manchester.ac.uk/portal/en/theses/verification-of-liveness-properties-on-hybrid-dynamical-systems(8817319c-a63f-4cf3-927d-a2ddf69139b4).html ; http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.576886.
Council of Science Editors:
Carter R. Verification of liveness properties on hybrid dynamical systems. [Doctoral Dissertation]. University of Manchester; 2013. Available from: https://www.research.manchester.ac.uk/portal/en/theses/verification-of-liveness-properties-on-hybrid-dynamical-systems(8817319c-a63f-4cf3-927d-a2ddf69139b4).html ; http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.576886
University of Illinois – Urbana-Champaign
14.
Katelman, Michael.
A meta-language for functional verification.
Degree: PhD, 0112, 2012, University of Illinois – Urbana-Champaign
URL: http://hdl.handle.net/2142/29614
► This dissertation perceives a similarity between two activities: that of coordinating the search for simulation traces toward reaching verification closure, and that of coordinating the…
(more)
▼ This dissertation perceives a similarity between two activities: that of coordinating the search for simulation traces toward reaching
verification closure, and that of coordinating the search for a proof within a theorem prover. The programmatic coordination of simulation is difficult with existing tools for digital circuit
verification because stimuli generation, simulation execution, and analysis of simulation results are all decoupled. A new programming language to address this problem, analogous to the mechanism for orchestrating proof search tactics within a theorem prover, is defined wherein device simulation is made a first-class notion. This meta-language for functional
verification is first formalized in a parametric way over hardware description languages using rewriting logic, and subsequently a more richly featured software tool for Verilog designs, implemented as an embedded domain-specific language in Haskell, is described and used to demonstrate the novelty of the programming language and to conduct two case studies. Additionally, three hardware description languages are given
formal semantics using rewriting logic and we demonstrate the use of executable rewriting logic tools to formally analyze devices implemented in those languages.
Advisors/Committee Members: Meseguer, Jos?? (advisor), Arvind (committee member), Rosu, Grigore (committee member), Torrellas, Josep (committee member).
Subjects/Keywords: Programming Languages; Formal Methods; Hardware Verification
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Katelman, M. (2012). A meta-language for functional verification. (Doctoral Dissertation). University of Illinois – Urbana-Champaign. Retrieved from http://hdl.handle.net/2142/29614
Chicago Manual of Style (16th Edition):
Katelman, Michael. “A meta-language for functional verification.” 2012. Doctoral Dissertation, University of Illinois – Urbana-Champaign. Accessed January 17, 2021.
http://hdl.handle.net/2142/29614.
MLA Handbook (7th Edition):
Katelman, Michael. “A meta-language for functional verification.” 2012. Web. 17 Jan 2021.
Vancouver:
Katelman M. A meta-language for functional verification. [Internet] [Doctoral dissertation]. University of Illinois – Urbana-Champaign; 2012. [cited 2021 Jan 17].
Available from: http://hdl.handle.net/2142/29614.
Council of Science Editors:
Katelman M. A meta-language for functional verification. [Doctoral Dissertation]. University of Illinois – Urbana-Champaign; 2012. Available from: http://hdl.handle.net/2142/29614
University of Illinois – Urbana-Champaign
15.
Kheradmand, Ali.
A formal semantics of P4 and applications.
Degree: MS, Computer Science, 2018, University of Illinois – Urbana-Champaign
URL: http://hdl.handle.net/2142/102486
► Programmable packet processors and P4 as a programming language for such devices have gained significant interest, because their flexibility enables rapid development of a diverse…
(more)
▼ Programmable packet processors and P4 as a programming language for such devices have gained significant interest, because their flexibility enables rapid development of a diverse set of applications that work at line rate. However, this flexibility, combined with the complexity of devices and networks, increases the chance of introducing subtle bugs that are hard to discover manually. Worse, this is a domain where bugs can have catastrophic consequences, yet
formal analysis tools for P4 programs and networks are missing.
We argue that
formal analysis tools must be based on a
formal semantics of the target language, rather than on its informal specification. To this end, we provide an executable
formal semantics of the P4 language in the K framework. Based on this semantics, K provides an interpreter and various analysis tools including a symbolic model checker and a deductive program verifier.
This thesis overviews our
formal K semantics of P4, as well as several P4 language design issues that we found during our formalization process. We also discuss some applications resulting from the tools provided by K for P4 programmers and network administrators as well as language designers and compiler developers, such as detection of unportable code, state space exploration of P4 programs and networks, bug finding using symbolic execution, data plane
verification, program
verification, and translation validation.
Advisors/Committee Members: Rosu, Grigore (advisor).
Subjects/Keywords: Formal Semantics; P4; K Framework; Network Verification
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Kheradmand, A. (2018). A formal semantics of P4 and applications. (Thesis). University of Illinois – Urbana-Champaign. Retrieved from http://hdl.handle.net/2142/102486
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
Chicago Manual of Style (16th Edition):
Kheradmand, Ali. “A formal semantics of P4 and applications.” 2018. Thesis, University of Illinois – Urbana-Champaign. Accessed January 17, 2021.
http://hdl.handle.net/2142/102486.
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
MLA Handbook (7th Edition):
Kheradmand, Ali. “A formal semantics of P4 and applications.” 2018. Web. 17 Jan 2021.
Vancouver:
Kheradmand A. A formal semantics of P4 and applications. [Internet] [Thesis]. University of Illinois – Urbana-Champaign; 2018. [cited 2021 Jan 17].
Available from: http://hdl.handle.net/2142/102486.
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
Council of Science Editors:
Kheradmand A. A formal semantics of P4 and applications. [Thesis]. University of Illinois – Urbana-Champaign; 2018. Available from: http://hdl.handle.net/2142/102486
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
Boise State University
16.
Joshaghani, Rezvan.
UNICORN Framework: A User-Centric Approach Toward Formal Verification of Privacy Norms.
Degree: 2019, Boise State University
URL: https://scholarworks.boisestate.edu/td/1526
► In the development of complex systems, such as user-centric privacy management systems with multiple components and attributes, it is important to formalize the process and…
(more)
▼ In the development of complex systems, such as user-centric privacy management systems with multiple components and attributes, it is important to formalize the process and develop mathematical models that can be utilized to automatically make decisions on the information sharing actions of users. While valuable, the current state-of-the-art models are mostly based on enterprise/organizational privacy perspectives and leave the main actor, i.e., the user, uninvolved or with limited ability to control information sharing actions. These approaches cannot be applied to a user-centric environment since user privacy policies are dynamic because they change based on the information sharing context and environment. In this thesis, we focused on developing the main core of the framework which is the privacy formalization and verification engine that allows for the guided and flexible specification of user’s privacy policies. The formalization and verification engine reasons about the user’s privacy rules to find privacy violating information sharing actions and ensure that the privacy norms are unambiguous and consistent. Utilizing these privacy norms, the framework monitors user’s information sharing actions to detect privacy violations. In cases that an action is not compliant with the privacy norms, the framework utilizes a game theoretic approach to generate a privacy decision model. This model enables the users to proceed with the violating action without compromising their privacy by suggesting an information negotiation protocol based on the information sensitivity, users trust, and the reward of information sharing action.
Subjects/Keywords: privacy; formal verification; Other Computer Engineering
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Joshaghani, R. (2019). UNICORN Framework: A User-Centric Approach Toward Formal Verification of Privacy Norms. (Thesis). Boise State University. Retrieved from https://scholarworks.boisestate.edu/td/1526
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
Chicago Manual of Style (16th Edition):
Joshaghani, Rezvan. “UNICORN Framework: A User-Centric Approach Toward Formal Verification of Privacy Norms.” 2019. Thesis, Boise State University. Accessed January 17, 2021.
https://scholarworks.boisestate.edu/td/1526.
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
MLA Handbook (7th Edition):
Joshaghani, Rezvan. “UNICORN Framework: A User-Centric Approach Toward Formal Verification of Privacy Norms.” 2019. Web. 17 Jan 2021.
Vancouver:
Joshaghani R. UNICORN Framework: A User-Centric Approach Toward Formal Verification of Privacy Norms. [Internet] [Thesis]. Boise State University; 2019. [cited 2021 Jan 17].
Available from: https://scholarworks.boisestate.edu/td/1526.
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
Council of Science Editors:
Joshaghani R. UNICORN Framework: A User-Centric Approach Toward Formal Verification of Privacy Norms. [Thesis]. Boise State University; 2019. Available from: https://scholarworks.boisestate.edu/td/1526
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
Clemson University
17.
Smith, Hampton.
Engineering Specifications and Mathematics for Verified Software.
Degree: PhD, Computer Science, 2013, Clemson University
URL: https://tigerprints.clemson.edu/all_dissertations/1132
► Developing a verifying compiler – a compiler that proves that components are correct with respect to their specifications – is a grand challenge for the computing community.…
(more)
▼ Developing a verifying compiler – a compiler that proves that components are correct with respect to their specifications – is a grand challenge for the computing community. The prevailing view of the software engineering community is that this problem is necessarily difficult because, to-date, the resultant
verification conditions necessary to prove software correctness have required powerful automated provers and deep mathematical insight to dispatch. This seems counter-intuitive, however, since human programmers only rarely resort to deep mathematics to assure themselves that their code works. In this work, we show that well-specified and well-engineered software supported by a flexible, extensible mathematical system can yield
verification conditions that are sufficiently straightforward to be dispatched by a minimalist rewrite prover. We explore techniques for making such a system both powerful and user-friendly, and for tuning an automated prover to the
verification task. In addition to influencing the design of our own system, RESOLVE, this exploration benefits the greater
verification community by informing specification and theory design and encouraging greater integration between nuanced mathematical systems and powerful programming languages. This dissertation presents the design and an implementation of a minimalist rewrite prover tuned for the software
verification task. It supports the prover with the design and implementation of a flexible, extensible mathematical system suitable for use with an industrial-strength programming language. This system is employed within a well-integrated specification framework. The dissertation validates the central thesis that
verification conditions for well-engineered software can be dispatched easily by applying these tools and methods to a number of benchmark components and collecting and analyzing the resulting data.
Advisors/Committee Members: Sitaraman, Murali, Dean , Brian C, Hallstrom , Jason O, Pargas , Roy P.
Subjects/Keywords: Formal Methods; Specficiation; Verification; Computer Sciences
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Smith, H. (2013). Engineering Specifications and Mathematics for Verified Software. (Doctoral Dissertation). Clemson University. Retrieved from https://tigerprints.clemson.edu/all_dissertations/1132
Chicago Manual of Style (16th Edition):
Smith, Hampton. “Engineering Specifications and Mathematics for Verified Software.” 2013. Doctoral Dissertation, Clemson University. Accessed January 17, 2021.
https://tigerprints.clemson.edu/all_dissertations/1132.
MLA Handbook (7th Edition):
Smith, Hampton. “Engineering Specifications and Mathematics for Verified Software.” 2013. Web. 17 Jan 2021.
Vancouver:
Smith H. Engineering Specifications and Mathematics for Verified Software. [Internet] [Doctoral dissertation]. Clemson University; 2013. [cited 2021 Jan 17].
Available from: https://tigerprints.clemson.edu/all_dissertations/1132.
Council of Science Editors:
Smith H. Engineering Specifications and Mathematics for Verified Software. [Doctoral Dissertation]. Clemson University; 2013. Available from: https://tigerprints.clemson.edu/all_dissertations/1132
18.
Sogokon, Andrew.
Direct methods for deductive verification of temporal properties in continuous dynamical systems.
Degree: PhD, 2016, University of Edinburgh
URL: http://hdl.handle.net/1842/20952
► This thesis is concerned with the problem of formal verification of correctness specifications for continuous and hybrid dynamical systems. Our main focus will be on…
(more)
▼ This thesis is concerned with the problem of formal verification of correctness specifications for continuous and hybrid dynamical systems. Our main focus will be on developing and automating general proof principles for temporal properties of systems described by non-linear ordinary differential equations (ODEs) under evolution constraints. The proof methods we consider will work directly with the differential equations and will not rely on the explicit knowledge of solutions, which are in practice rarely available. Our ultimate goal is to increase the scope of formal deductive verification tools for hybrid system designs. We give a comprehensive survey and comparison of available methods for checking set invariance in continuous systems, which provides a foundation for safety verification using inductive invariants. Building on this, we present a technique for constructing discrete abstractions of continuous systems in which spurious transitions between discrete states are entirely eliminated, thereby extending previous work. We develop a method for automatically generating inductive invariants for continuous systems by efficiently extracting reachable sets from their discrete abstractions. To reason about liveness properties in ODEs, we introduce a new proof principle that extends and generalizes methods that have been reported previously and is highly amenable to use as a rule of inference in a deductive verification calculus for hybrid systems. We will conclude with a summary of our contributions and directions for future work.
Subjects/Keywords: 004.2; hybrid systems; ODEs; formal verification
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Sogokon, A. (2016). Direct methods for deductive verification of temporal properties in continuous dynamical systems. (Doctoral Dissertation). University of Edinburgh. Retrieved from http://hdl.handle.net/1842/20952
Chicago Manual of Style (16th Edition):
Sogokon, Andrew. “Direct methods for deductive verification of temporal properties in continuous dynamical systems.” 2016. Doctoral Dissertation, University of Edinburgh. Accessed January 17, 2021.
http://hdl.handle.net/1842/20952.
MLA Handbook (7th Edition):
Sogokon, Andrew. “Direct methods for deductive verification of temporal properties in continuous dynamical systems.” 2016. Web. 17 Jan 2021.
Vancouver:
Sogokon A. Direct methods for deductive verification of temporal properties in continuous dynamical systems. [Internet] [Doctoral dissertation]. University of Edinburgh; 2016. [cited 2021 Jan 17].
Available from: http://hdl.handle.net/1842/20952.
Council of Science Editors:
Sogokon A. Direct methods for deductive verification of temporal properties in continuous dynamical systems. [Doctoral Dissertation]. University of Edinburgh; 2016. Available from: http://hdl.handle.net/1842/20952
Kansas State University
19.
Zhang, Zhi.
A formal
approach to contract verification for high-integrity
applications.
Degree: PhD, Department of Computing and
Information Sciences, 2016, Kansas State University
URL: http://hdl.handle.net/2097/32880
► High-integrity applications are safety- and security-critical applications developed for a variety of critical tasks. The correctness of these applications must be thoroughly tested or formally…
(more)
▼ High-integrity applications are safety- and
security-critical applications developed for a variety of critical
tasks. The correctness of these applications must be thoroughly
tested or formally verified to ensure their reliability and
robustness. The major properties to be verified for the correctness
of applications include: (1) functional properties, capturing the
expected behaviors of a software, (2) dataflow property, tracking
data dependency and preventing secret data from leaking to the
public, and (3) robustness property, the ability of a program to
deal with errors during execution.
This dissertation presents and
explores
formal verification and proof technique, a promising
technique using rigorous mathematical methods, to verify critical
applications from the above three aspects. Our research is carried
out in the context of SPARK, a programming language designed for
development of safety- and security-critical applications.
First,
we have formalized in the Coq proof assistant the dynamic semantics
for a significant subset of the SPARK 2014 language, which includes
run-time checks as an integral part of the language, as any
formal
methods for program specification and
verification depend on the
unambiguous semantics of the language.
Second, we have formally
defined and proved the correctness of run-time checks generation
and optimization based on SPARK reference semantics, and have built
the certifying tools within the mechanized proof infrastructure to
certify the run-time checks inserted by the GNAT compiler frontend
to guarantee the absence of run-time errors.
Third, we have
proposed a language-based information security policy framework and
the associated enforcement algorithm, which is proved to be sound
with respect to the formalized program semantics. We have shown how
the policy framework can be integrated into SPARK 2014 for more
advanced information security analysis.
Advisors/Committee Members: John M. Hatcliff.
Subjects/Keywords: Formal
Methods; Language
Semantics; Program
Verification
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Zhang, Z. (2016). A formal
approach to contract verification for high-integrity
applications. (Doctoral Dissertation). Kansas State University. Retrieved from http://hdl.handle.net/2097/32880
Chicago Manual of Style (16th Edition):
Zhang, Zhi. “A formal
approach to contract verification for high-integrity
applications.” 2016. Doctoral Dissertation, Kansas State University. Accessed January 17, 2021.
http://hdl.handle.net/2097/32880.
MLA Handbook (7th Edition):
Zhang, Zhi. “A formal
approach to contract verification for high-integrity
applications.” 2016. Web. 17 Jan 2021.
Vancouver:
Zhang Z. A formal
approach to contract verification for high-integrity
applications. [Internet] [Doctoral dissertation]. Kansas State University; 2016. [cited 2021 Jan 17].
Available from: http://hdl.handle.net/2097/32880.
Council of Science Editors:
Zhang Z. A formal
approach to contract verification for high-integrity
applications. [Doctoral Dissertation]. Kansas State University; 2016. Available from: http://hdl.handle.net/2097/32880
University of Sydney
20.
Subotic, Pavle.
Applying Elimination-Based Algorithms to Abstract Interpretation
.
Degree: 2014, University of Sydney
URL: http://hdl.handle.net/2123/12052
► Unbounded abstract domains are used in static program analysis frameworks for representing ranges of variables, and their applications include elimination of assertions in programs, automatically…
(more)
▼ Unbounded abstract domains are used in static program analysis frameworks for representing ranges of variables, and their applications include elimination of assertions in programs, automatically deducing numerical stability, and eliminating array bounds checking. Unbounded abstract domains impose a major challenge in static program analysis because the termination of the analysis may not be guaranteed in the presence of program loops. To overcome the problem of termination, extrapolation techniques are applied to programs loops. State-of-the-art work proposes the use of cumbersome techniques to mark loop headers or relies on structurally composed programs, e.g., programs that consists of while and if statements but do not have goto statements. In this thesis we present a novel program analysis technique that applies abstract interpretation to low-level intermediate languages with unbounded abstract domains. Our work adapts methods of elimination-based data flow analysis to abstract interpretation. The proposed technique has several advantages over the state-of-the-art, most importantly, its ability to detect strongly connected components automatically. We have implemented a prototype of our proposed framework in the LLVM compiler infrastructure and have conducted experiments with a suite of test programs to show the viability of our approach.
Subjects/Keywords: Static Analysis;
Abstract Interpretation;
Formal Verification;
LLVM
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Subotic, P. (2014). Applying Elimination-Based Algorithms to Abstract Interpretation
. (Thesis). University of Sydney. Retrieved from http://hdl.handle.net/2123/12052
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
Chicago Manual of Style (16th Edition):
Subotic, Pavle. “Applying Elimination-Based Algorithms to Abstract Interpretation
.” 2014. Thesis, University of Sydney. Accessed January 17, 2021.
http://hdl.handle.net/2123/12052.
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
MLA Handbook (7th Edition):
Subotic, Pavle. “Applying Elimination-Based Algorithms to Abstract Interpretation
.” 2014. Web. 17 Jan 2021.
Vancouver:
Subotic P. Applying Elimination-Based Algorithms to Abstract Interpretation
. [Internet] [Thesis]. University of Sydney; 2014. [cited 2021 Jan 17].
Available from: http://hdl.handle.net/2123/12052.
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
Council of Science Editors:
Subotic P. Applying Elimination-Based Algorithms to Abstract Interpretation
. [Thesis]. University of Sydney; 2014. Available from: http://hdl.handle.net/2123/12052
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
University of New South Wales
21.
von Tessin, Michael.
The clustered multikernel: an approach to formal verification of multiprocessor operating-system kernels.
Degree: Computer Science & Engineering, 2013, University of New South Wales
URL: http://handle.unsw.edu.au/1959.4/53099
;
https://unsworks.unsw.edu.au/fapi/datastream/unsworks:11785/SOURCE01?view=true
► The key software component of a computer system is the operating-system kernel. Italways needs to be trusted because it runs in the CPU’s privileged mode…
(more)
▼ The key software component of a computer system is the operating-system kernel. Italways needs to be trusted because it runs in the CPU’s privileged mode and therefore hasaccess to all system components. Consequently, kernel correctness is crucial for secure,safe and reliable computer systems. Correctness can be improved by careful design,development and testing. However, this is not enough for kernels of high-assurancecomputer systems used in defence, aviation and the like.Much stronger correctness guarantees can be obtained by
formal verification of akernel’s implementation. In order to keep
verification complexity at a manageable level,prior kernel
verification research only targeted uniprocessor kernels. In other words,the current state of research restricts computer systems that require a verified kernelto running on one CPU/core. This is a problem because manufacturers are increasingcomputing power of their systems by adding more CPUs and cores.In this thesis, we demonstrate that it is possible to extend a verified uniprocessorkernel to utilise multiple CPUs/cores and leverage the existing proofs to obtain a verifiedmultiprocessor version of that kernel (under certain assumptions).To this end, we introduce the clustered multikernel, a point in the design space ofmultiprocessor kernels. The main feature of this design is that it reduces concurrentdata access to a minimum while offering a configurable trade-off between scalability andflexibility. Furthermore, we present a conversion scheme to convert a uniprocessor kernelinto a clustered multikernel.Based on this design, we contribute a refinement lifting framework, which lifts theconverted kernel’s functional-correctness proof such that it applies to the clusteredmultikernelversion. The support for handling the introduced concurrency is added to theexisting
verification framework in a non-intrusive way and accounts for total-store-orderweak memory ordering.We demonstrate the practicability of our approach by successfully applying it to seL4,a formally verified general-purpose microkernel. We show that this requires relatively loweffort, compared to the kernel’s initial
verification.All
formal specifications and proofs are machine-checked in the theorem prover Isabelle/HOL.
Advisors/Committee Members: Elphinstone, Kevin, Computer Science & Engineering, Faculty of Engineering, UNSW.
Subjects/Keywords: Microkernel; Formal verification; Multiprocessor; seL4; Isabelle/HOL
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
von Tessin, M. (2013). The clustered multikernel: an approach to formal verification of multiprocessor operating-system kernels. (Doctoral Dissertation). University of New South Wales. Retrieved from http://handle.unsw.edu.au/1959.4/53099 ; https://unsworks.unsw.edu.au/fapi/datastream/unsworks:11785/SOURCE01?view=true
Chicago Manual of Style (16th Edition):
von Tessin, Michael. “The clustered multikernel: an approach to formal verification of multiprocessor operating-system kernels.” 2013. Doctoral Dissertation, University of New South Wales. Accessed January 17, 2021.
http://handle.unsw.edu.au/1959.4/53099 ; https://unsworks.unsw.edu.au/fapi/datastream/unsworks:11785/SOURCE01?view=true.
MLA Handbook (7th Edition):
von Tessin, Michael. “The clustered multikernel: an approach to formal verification of multiprocessor operating-system kernels.” 2013. Web. 17 Jan 2021.
Vancouver:
von Tessin M. The clustered multikernel: an approach to formal verification of multiprocessor operating-system kernels. [Internet] [Doctoral dissertation]. University of New South Wales; 2013. [cited 2021 Jan 17].
Available from: http://handle.unsw.edu.au/1959.4/53099 ; https://unsworks.unsw.edu.au/fapi/datastream/unsworks:11785/SOURCE01?view=true.
Council of Science Editors:
von Tessin M. The clustered multikernel: an approach to formal verification of multiprocessor operating-system kernels. [Doctoral Dissertation]. University of New South Wales; 2013. Available from: http://handle.unsw.edu.au/1959.4/53099 ; https://unsworks.unsw.edu.au/fapi/datastream/unsworks:11785/SOURCE01?view=true
University of Texas – Austin
22.
Yang, Hongkun.
Efficient verification of packet networks.
Degree: PhD, Computer science, 2015, University of Texas – Austin
URL: http://hdl.handle.net/2152/33271
► Network management will benefit from automated tools based upon formal methods. In these tools, the algorithm for computing reachability is the core algorithm for verifying…
(more)
▼ Network management will benefit from automated tools based upon
formal methods. In these tools, the algorithm for computing reachability is the core algorithm for verifying network properties in the data plane. This dissertation presents efficient algorithms for computing reachability and verifying network properties for a single network with both packet filters and transformers, and for interconnected networks.
For computing port to port reachability in a network, we present a new
formal method for a new tool, Atomic Predicates (AP) Verifier, which is much more time and space efficient than existing tools. Given a set of predicates representing packet filters, AP Verifier computes a set of atomic predicates, which is minimum and unique. The use of atomic predicates dramatically speeds up computation of network reachability. AP Verifier also includes algorithms to process network update events and check compliance with network policies and properties in real time.
Packet transformers are widely used in Internet service provider networks, datacenter infrastructures, and layer-2 networks. Existing network
verification tools do not scale to such networks with large numbers of different transformers. We present a new tool, AP+ Verifier, based upon a new algorithm for computing atomic predicates for networks with both packet filters and transformers. For performance evaluation, we use network datasets with different types of transformers (i.e., MPLS tunnels, IP-in-IP tunnels, and NATs). We found that AP+ Verifier is more time and space efficient than prior tools by orders of magnitude.
The Internet consists a large collection of networks. To debug reachability problems, a network operator often asks operators of other networks for help by telephone or email. We present a new protocol, COVE, and an efficient data structure for automating the exchange of data plane reachability information between networks in a business relationship. COVE is designed to improve a network's views of forward and reverse reachability with partial deployment in mind. COVE is scalable to very large networks in the Internet. We illustrate applications of COVE to perform useful network management tasks, which cannot be done effectively using existing methods and tools.
Advisors/Committee Members: Lam, Simon S., 1947- (advisor), Emerson, Ernest A. (committee member), Garg, Vijay K. (committee member), Gouda, Mohamed G. (committee member), Mok, Aloysius K. (committee member).
Subjects/Keywords: Network verification; Formal methods; Automated tools
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Yang, H. (2015). Efficient verification of packet networks. (Doctoral Dissertation). University of Texas – Austin. Retrieved from http://hdl.handle.net/2152/33271
Chicago Manual of Style (16th Edition):
Yang, Hongkun. “Efficient verification of packet networks.” 2015. Doctoral Dissertation, University of Texas – Austin. Accessed January 17, 2021.
http://hdl.handle.net/2152/33271.
MLA Handbook (7th Edition):
Yang, Hongkun. “Efficient verification of packet networks.” 2015. Web. 17 Jan 2021.
Vancouver:
Yang H. Efficient verification of packet networks. [Internet] [Doctoral dissertation]. University of Texas – Austin; 2015. [cited 2021 Jan 17].
Available from: http://hdl.handle.net/2152/33271.
Council of Science Editors:
Yang H. Efficient verification of packet networks. [Doctoral Dissertation]. University of Texas – Austin; 2015. Available from: http://hdl.handle.net/2152/33271
University of New South Wales
23.
Kolanski, Rafal Michal.
Verification of programs in virtual memory using separation logic.
Degree: Computer Science & Engineering, 2011, University of New South Wales
URL: http://handle.unsw.edu.au/1959.4/51288
;
https://unsworks.unsw.edu.au/fapi/datastream/unsworks:9969/SOURCE02?view=true
► Formal reasoning about programs executing in virtual memory is a difficult problem, as it is an environment in which writing to memory can change its…
(more)
▼ Formal reasoning about programs executing in virtual memory is a difficult problem, as it is an environment in which writing to memory can change its layout. At the same time, correctly reasoning about virtual memory is essential to operating system
verification, a field we are very much interested in. Current approaches rely on entering special modes or making high-level assertions about the nature of virtual memory which may or may not be correct.In this thesis, we examine the problems created by virtual memory and develop a unified view of memory, both physical and virtual, based on separation logic. We first develop this model for a simple programming language on a simplified architecture with a one-level page table, taking care to prove it constitutes a separation logic. We then extend the framework to deal with low-level C programs executing in a virtual memory environment of the ARMv6 architecture with a two-level page table. We perform two case studies involving mapping in of a new page into the current address space: first for the simple version of our logic, and finally for our full framework. The case studies demonstrate that separation logic style modular reasoning via the frame rule can be used in a unified model which encompasses virtual memory, even in the presence of page table writes.To our knowledge, we present the first model offering a unified view of virtual and physical memory, the first separation logic involving an address translation mechanism, as well as the first published model of a functional subset of ARM memory management unit. Our memory models, framework, proofs and all results are formalised in the Isabelle/HOL interactive theorem prover.
Advisors/Committee Members: Klein, Gerwin, National ICT Australia, Elphinstone, Kevin, Computer Science & Engineering, Faculty of Engineering, UNSW.
Subjects/Keywords: Formal verification; Separation logic; Virtual memory
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Kolanski, R. M. (2011). Verification of programs in virtual memory using separation logic. (Doctoral Dissertation). University of New South Wales. Retrieved from http://handle.unsw.edu.au/1959.4/51288 ; https://unsworks.unsw.edu.au/fapi/datastream/unsworks:9969/SOURCE02?view=true
Chicago Manual of Style (16th Edition):
Kolanski, Rafal Michal. “Verification of programs in virtual memory using separation logic.” 2011. Doctoral Dissertation, University of New South Wales. Accessed January 17, 2021.
http://handle.unsw.edu.au/1959.4/51288 ; https://unsworks.unsw.edu.au/fapi/datastream/unsworks:9969/SOURCE02?view=true.
MLA Handbook (7th Edition):
Kolanski, Rafal Michal. “Verification of programs in virtual memory using separation logic.” 2011. Web. 17 Jan 2021.
Vancouver:
Kolanski RM. Verification of programs in virtual memory using separation logic. [Internet] [Doctoral dissertation]. University of New South Wales; 2011. [cited 2021 Jan 17].
Available from: http://handle.unsw.edu.au/1959.4/51288 ; https://unsworks.unsw.edu.au/fapi/datastream/unsworks:9969/SOURCE02?view=true.
Council of Science Editors:
Kolanski RM. Verification of programs in virtual memory using separation logic. [Doctoral Dissertation]. University of New South Wales; 2011. Available from: http://handle.unsw.edu.au/1959.4/51288 ; https://unsworks.unsw.edu.au/fapi/datastream/unsworks:9969/SOURCE02?view=true
The Ohio State University
24.
Zaccai, Diego Sebastian.
A Balanced Verification Effort for the Java Language.
Degree: PhD, Computer Science and Engineering, 2016, The Ohio State University
URL: http://rave.ohiolink.edu/etdc/view?acc_num=osu1461243619
► Current tools used to verify software in languages with reference semantics, such as Java, are hampered by the possibility of aliases. Existing approaches to addressing…
(more)
▼ Current tools used to verify software in languages
with reference semantics, such as Java, are hampered by the
possibility of aliases. Existing approaches to addressing this
long-standing
verification problem try not to sacrifice modularity
because modular reasoning is what makes
verification tractable. To
achieve this, these approaches treat the value of a reference
variable as a memory address in the heap. A serious problem with
this decision is that it severely limits the usefulness of generic
collections because they must be specified as collections of
references, and components of this kind are fundamentally flawed in
design and implementation. The limitations become clear when
attempting to verify clients of generic collections.The first step
in rectifying the situation is to redefine the "value" of a
reference variable in terms of the abstract value of the object it
references. A careful analysis of what the "value" of a reference
variable might mean leads inevitably to this conclusion, which is
consistent with the denotation of a variable in languages with
value semantics, such as RESOLVE.
Verification in languages with
value semantics is straightforward compared to
verification in
languages with reference semantics precisely because of the lack of
concern with heap properties. However, there is still a nagging
problem: aliasing can occur in legal programs in languages with
reference semantics, such as Java, and it must be handled when it
does occur. The crux of the issue is not in-your-face assignment
statements that copy references but rather aliasing arising within
(hidden) method bodies. The reason is that the effects of calls to
these methods in client code must be summarized in their
specifications in order to preserve modularity.So, the second step
is the introduction of a discipline restricting what a client can
do with a reference that is aliased within a method. The discipline
advertises the creation of such aliases in method specifications
and prevents a client from engaging in behavior that would break
the abstractions of the objects being referenced, as this would
also prevent modular
verification. These restrictions allow code to
be specified in terms of the abstract values of objects instead of
treating the values of references as memory addresses in the heap.
Even though the discipline prevents some programming idioms, it
remains flexible enough to allow for most common programs,
including the use of iterators, without the need for workarounds.A
tool can verify that a program satisfies the provisions of this
discipline. Further, it can generate
verification conditions that
rely only on abstract object values to demonstrate a program's
correctness. These
verification conditions can be discharged by the
theorem-proving tools currently used to verify RESOLVE
programs.
Advisors/Committee Members: Weide, Bruce W. (Advisor).
Subjects/Keywords: Computer Science; Formal Methods; Software Verification
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Zaccai, D. S. (2016). A Balanced Verification Effort for the Java Language. (Doctoral Dissertation). The Ohio State University. Retrieved from http://rave.ohiolink.edu/etdc/view?acc_num=osu1461243619
Chicago Manual of Style (16th Edition):
Zaccai, Diego Sebastian. “A Balanced Verification Effort for the Java Language.” 2016. Doctoral Dissertation, The Ohio State University. Accessed January 17, 2021.
http://rave.ohiolink.edu/etdc/view?acc_num=osu1461243619.
MLA Handbook (7th Edition):
Zaccai, Diego Sebastian. “A Balanced Verification Effort for the Java Language.” 2016. Web. 17 Jan 2021.
Vancouver:
Zaccai DS. A Balanced Verification Effort for the Java Language. [Internet] [Doctoral dissertation]. The Ohio State University; 2016. [cited 2021 Jan 17].
Available from: http://rave.ohiolink.edu/etdc/view?acc_num=osu1461243619.
Council of Science Editors:
Zaccai DS. A Balanced Verification Effort for the Java Language. [Doctoral Dissertation]. The Ohio State University; 2016. Available from: http://rave.ohiolink.edu/etdc/view?acc_num=osu1461243619
University of Oklahoma
25.
Ralston, Ryan.
Translating Clojure to ACL2 for Verification.
Degree: PhD, 2016, University of Oklahoma
URL: http://hdl.handle.net/11244/42982
► Software spends a significant portion of its life-cycle in the maintenance phase and over 20% of the maintenance effort is fixing defects. Formal methods, including…
(more)
▼ Software spends a significant portion of its life-cycle in the maintenance phase and over 20% of the maintenance effort is fixing defects.
Formal methods, including
verification, can reduce the number of defects in software and lower corrective maintenance, but their industrial adoption has been underwhelming. A significant barrier to adoption is the overhead of converting imperative programming languages, which are common in industry, into the declarative programming languages that are used by
formal methods tools. In comparison, the
verification of software written in declarative programming languages is much easier because the conversion into a
formal methods tool is easier. The growing popularity of declarative programming – evident from the rise of multi-paradigm languages such as Javascript, Ruby, and Scala – affords us the opportunity to verify the correctness of software more easily.
Clojure is a declarative language released in 2007 that compiles to bytecode that executes on the Java Virtual Machine (JVM). Despite being a newer, declarative programming language, several companies have already used it to develop commercial products. Clojure shares a Lisp syntax with ACL2, an interactive theorem prover that is used to verify the correctness of software. Since both languages are based on Lisp, code written in either Clojure or ACL2 is easily converted to the other. Therefore, Clojure can conceivably be verified by ACL2 with limited overhead assuming that the underlying behavior of Clojure code matches that of ACL2. ACL2 has been previously used to reason about Java programs through the use of
formal models of the JVM. Since Clojure compiles to JVM bytecode, a similar approach is taken in this dissertation to verify the underlying implementation of Clojure.
The research presented in this dissertation advances techniques to verify Clojure code in ACL2. Clojure and ACL2 are declarative, but they are specifically functional programming languages so the research focuses on two important concepts in functional programming and
verification: arbitrary-precision numbers ("bignums") and lists. For bignums, the correctness of a model of addition is verified that addresses issues that arise from the unique representation of bignums in Clojure. Lists, in Clojure, are implemented as a type of sequence. This dissertation demonstrates an abstraction that equates Clojure sequences to ACL2 lists. In support of the research, an existing ACL2 model of the JVM is modified to address specific aspects of compiled Clojure code and the new model is used to verify the correctness of core Clojure functions with respect to corresponding ACL2 functions. The results support the ideas that ACL2 can be used to reason about Clojure code and that
formal methods can be integrated more easily in industrial software development when the implementation corresponds semantically to the
verification model.
Advisors/Committee Members: Page, Rex (advisor), Hougen, Dean (advisor), Miller, David (committee member), Jensen, Matthew (committee member), Weaver, Christopher (committee member).
Subjects/Keywords: Software Verification; Formal Methods; Theorem Proving
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Ralston, R. (2016). Translating Clojure to ACL2 for Verification. (Doctoral Dissertation). University of Oklahoma. Retrieved from http://hdl.handle.net/11244/42982
Chicago Manual of Style (16th Edition):
Ralston, Ryan. “Translating Clojure to ACL2 for Verification.” 2016. Doctoral Dissertation, University of Oklahoma. Accessed January 17, 2021.
http://hdl.handle.net/11244/42982.
MLA Handbook (7th Edition):
Ralston, Ryan. “Translating Clojure to ACL2 for Verification.” 2016. Web. 17 Jan 2021.
Vancouver:
Ralston R. Translating Clojure to ACL2 for Verification. [Internet] [Doctoral dissertation]. University of Oklahoma; 2016. [cited 2021 Jan 17].
Available from: http://hdl.handle.net/11244/42982.
Council of Science Editors:
Ralston R. Translating Clojure to ACL2 for Verification. [Doctoral Dissertation]. University of Oklahoma; 2016. Available from: http://hdl.handle.net/11244/42982
Universitat Politècnica de València
26.
Peiró Frasquet, Salvador.
Metodología para hipervisores seguros utilizando técnicas de validación formal
.
Degree: 2016, Universitat Politècnica de València
URL: http://hdl.handle.net/10251/63152
► [EN] The availability of new processors with more processing power for embedded systems has raised the development of applications that tackle problems of greater complexity.…
(more)
▼ [EN] The availability of new processors with more processing power for embedded systems has raised
the development of applications that tackle problems of greater complexity. Currently, the
embedded applications have more features, and as a consequence, more complexity. For this
reason, there exists a growing interest in allowing the secure execution of multiple applications
that share a single processor and memory. In this context, partitioned system architectures based
on hypervisors have evolved as an adequate solution to build secure systems.
One of the main challenges in the construction of secure partitioned systems is the
verification of
the correct operation of the hypervisor, since, the hypervisor is the critical component on which
rests the security of the partitioned system. Traditional approaches for Validation and
Verification
(V&V), such as testing, inspection and analysis, present limitations for the exhaustive validation
and
verification of the system operation, due to the fact that the input space to validate grows
exponentially with respect to the number of inputs to validate. Given this limitations,
verification
techniques based in
formal methods arise as an alternative to complement the traditional validation
techniques.
This dissertation focuses on the application of
formal methods to validate the correctness of the
partitioned system, with a special focus on the XtratuM hypervisor. The proposed methodology
is evaluated through its application to the hypervisor validation. To this end, we propose a
formal
model of the hypervisor based in Finite State Machines (FSM), this model enables the definition
of the correctness properties that the hypervisor design must fulfill. In addition, this dissertation
studies how to ensure the functional correctness of the hypervisor implementation by means of
deductive code
verification techniques.
Last, we study the vulnerabilities that result of the loss of confidentiality (CWE-200 [CWE08b]) of
the information managed by the partitioned system. In this context, the vulnerabilities (infoleaks)
are modeled, static code analysis techniques are applied to the detection of the vulnerabilities,
and last the proposed techniques are validated by means of a practical case study on the Linux
kernel that is a component of the partitioned system.; [ES] La disponibilidad de nuevos procesadores más potentes para aplicaciones empotradas ha permitido
el desarrollo de aplicaciones que abordan problemas de mayor complejidad. Debido a esto, las
aplicaciones empotradas actualmente tienen más funciones y prestaciones, y como consecuencia de
esto, una mayor complejidad. Por este motivo, existe un interés creciente en permitir la ejecución
de múltiples aplicaciones de forma segura y sin interferencias en un mismo procesador y memoria.
En este marco surgen las arquitecturas de sistemas particionados basados en hipervisores como
una solución apropiada para construir sistemas seguros.
Uno de los principales retos en la construcción de sistemas particionados, es la verificación del…
Advisors/Committee Members: Crespo Lorente, Alfons (advisor), Masmano Tello, Miguel Ángel (advisor), Simó Ten, José Enrique (advisor).
Subjects/Keywords: Secure Hypervisor construction using formal verification;
Partitioned system;
Hypervisor;
Formal methods;
Security;
Validation and verification
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Peiró Frasquet, S. (2016). Metodología para hipervisores seguros utilizando técnicas de validación formal
. (Doctoral Dissertation). Universitat Politècnica de València. Retrieved from http://hdl.handle.net/10251/63152
Chicago Manual of Style (16th Edition):
Peiró Frasquet, Salvador. “Metodología para hipervisores seguros utilizando técnicas de validación formal
.” 2016. Doctoral Dissertation, Universitat Politècnica de València. Accessed January 17, 2021.
http://hdl.handle.net/10251/63152.
MLA Handbook (7th Edition):
Peiró Frasquet, Salvador. “Metodología para hipervisores seguros utilizando técnicas de validación formal
.” 2016. Web. 17 Jan 2021.
Vancouver:
Peiró Frasquet S. Metodología para hipervisores seguros utilizando técnicas de validación formal
. [Internet] [Doctoral dissertation]. Universitat Politècnica de València; 2016. [cited 2021 Jan 17].
Available from: http://hdl.handle.net/10251/63152.
Council of Science Editors:
Peiró Frasquet S. Metodología para hipervisores seguros utilizando técnicas de validación formal
. [Doctoral Dissertation]. Universitat Politècnica de València; 2016. Available from: http://hdl.handle.net/10251/63152
27.
Bockenek, Joshua A.
USIMPL: An Extension of Isabelle/UTP with Simpl-like Control Flow.
Degree: MS, Computer Engineering, 2017, Virginia Tech
URL: http://hdl.handle.net/10919/81710
► Writing bug-free code is fraught with difficulty, and existing tools for the formal verification of programs do not scale well to large, complicated codebases such…
(more)
▼ Writing bug-free code is fraught with difficulty, and existing tools for the
formal verification of programs do not scale well to large, complicated codebases such as that of systems software (OSes, compilers, and similar programs that have a high level of complexity but work on a lower level than typical user applications such as text editors, image viewers, and the like). This thesis presents USIMPL, a component of the Orca project for
formal verification that builds on an existing framework for computer-aided, deductive mathematical proofs (Foster’s Isabelle/UTP) with features inspired by a simple but featureful language used for
verification (Schirmer’s Simpl) in order to achieve a modular, scalable framework for proofs of program correctness utilizing the rule-based mathematical representation of program behavior known as Hoare logic and Hoare-style algebraic laws of programming, which provide a
formal methodology for transforming programs to equivalent formulations.
Advisors/Committee Members: Ravindran, Binoy (committeechair), Lammich, Peter (committee member), Broadwater, Robert P. (committee member).
Subjects/Keywords: Formal Verification; Formal Methods; Isabelle; Unifying Theories of Programming; Verification Condition Generation
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Bockenek, J. A. (2017). USIMPL: An Extension of Isabelle/UTP with Simpl-like Control Flow. (Masters Thesis). Virginia Tech. Retrieved from http://hdl.handle.net/10919/81710
Chicago Manual of Style (16th Edition):
Bockenek, Joshua A. “USIMPL: An Extension of Isabelle/UTP with Simpl-like Control Flow.” 2017. Masters Thesis, Virginia Tech. Accessed January 17, 2021.
http://hdl.handle.net/10919/81710.
MLA Handbook (7th Edition):
Bockenek, Joshua A. “USIMPL: An Extension of Isabelle/UTP with Simpl-like Control Flow.” 2017. Web. 17 Jan 2021.
Vancouver:
Bockenek JA. USIMPL: An Extension of Isabelle/UTP with Simpl-like Control Flow. [Internet] [Masters thesis]. Virginia Tech; 2017. [cited 2021 Jan 17].
Available from: http://hdl.handle.net/10919/81710.
Council of Science Editors:
Bockenek JA. USIMPL: An Extension of Isabelle/UTP with Simpl-like Control Flow. [Masters Thesis]. Virginia Tech; 2017. Available from: http://hdl.handle.net/10919/81710
University of Utah
28.
Pruss, Tim.
Word-level abstraction from combinational circuits using algebraic geometry.
Degree: PhD, Electrical & Computer Engineering, 2015, University of Utah
URL: http://content.lib.utah.edu/cdm/singleitem/collection/etd3/id/3965/rec/2938
► Abstraction plays an important role in digital design, analysis, and verification, as it allows for the refinement of functions through different levels of conceptualization. This…
(more)
▼ Abstraction plays an important role in digital design, analysis, and verification, as it allows for the refinement of functions through different levels of conceptualization. This dissertation introduces a new method to compute a symbolic, canonical, word-level abstraction of the function implemented by a combinational logic circuit. This abstraction provides a representation of the function as a polynomial Z = F(A) over the Galois field F2k , expressed over the k-bit input to the circuit, A. This representation is easily utilized for formal verification (equivalence checking) of combinational circuits. The approach to abstraction is based upon concepts from commutative algebra and algebraic geometry, notably the Grobner basis theory. It is shown that the polynomial F(A) can be derived by computing a Grobner basis of the polynomials corresponding to the circuit, using a specific elimination term order based on the circuits topology. However, computing Grobner bases using elimination term orders is infeasible for large circuits. To overcome these limitations, this work introduces an efficient symbolic computation to derive the word-level polynomial. The presented algorithms exploit i) the structure of the circuit, ii) the properties of Grobner bases, iii) characteristics of Galois fields F2k , and iv) modern algorithms from symbolic computation. A custom abstraction tool is designed to efficiently implement the abstraction procedure. While the concept is applicable to any arbitrary combinational logic circuit, it is particularly powerful in verification and equivalence checking of hierarchical, custom designed and structurally dissimilar Galois field arithmetic circuits. In most applications, the field size and the datapath size k in the circuits is very large, up to 1024 bits. The proposed abstraction procedure can exploit the hierarchy of the given Galois field arithmetic circuits. Our experiments show that, using this approach, our tool can abstract and verify Galois field arithmetic circuits up to 1024 bits in size. Contemporary techniques fail to verify these types of circuits beyond 163 bits and cannot abstract a canonical representation beyond 32 bits.
Subjects/Keywords: Abstraction; Digital Design; Formal Verification; Grobner Basis; Hardware Verification
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Pruss, T. (2015). Word-level abstraction from combinational circuits using algebraic geometry. (Doctoral Dissertation). University of Utah. Retrieved from http://content.lib.utah.edu/cdm/singleitem/collection/etd3/id/3965/rec/2938
Chicago Manual of Style (16th Edition):
Pruss, Tim. “Word-level abstraction from combinational circuits using algebraic geometry.” 2015. Doctoral Dissertation, University of Utah. Accessed January 17, 2021.
http://content.lib.utah.edu/cdm/singleitem/collection/etd3/id/3965/rec/2938.
MLA Handbook (7th Edition):
Pruss, Tim. “Word-level abstraction from combinational circuits using algebraic geometry.” 2015. Web. 17 Jan 2021.
Vancouver:
Pruss T. Word-level abstraction from combinational circuits using algebraic geometry. [Internet] [Doctoral dissertation]. University of Utah; 2015. [cited 2021 Jan 17].
Available from: http://content.lib.utah.edu/cdm/singleitem/collection/etd3/id/3965/rec/2938.
Council of Science Editors:
Pruss T. Word-level abstraction from combinational circuits using algebraic geometry. [Doctoral Dissertation]. University of Utah; 2015. Available from: http://content.lib.utah.edu/cdm/singleitem/collection/etd3/id/3965/rec/2938
29.
Cheng, Zheng.
Formal Verification of Relational Model
Transformations using an Intermediate
Verification Language.
Degree: 2016, RIAN
URL: http://eprints.maynoothuniversity.ie/7089/
► Model-driven engineering has been recognised as an effective way to manage the complexity of software development. Model transformation is widely acknowledged as one of its…
(more)
▼ Model-driven engineering has been recognised as an effective way to manage the complexity
of software development. Model transformation is widely acknowledged as one of its
central ingredients. Among different paradigms of model transformations, we are specifically
interested in relational model transformations.
Proving the correctness of relational model transformations is our major concern. Typically
“correctness” is specified by MTr developers using contracts. Contracts are the annotations
on the MTr which express constraints under which the MTr are considered to be
correct. Our main objective is to develop an approach to designing a deductive verifier in a
modular and sound way for a given target relational model transformation language, which
enables formal verification of the correctness of MTr.
To this end, we have developed the VeriMTLr framework. Its role is to assist in designing
verifiers that allow verification (via automatic theorem proving) of the correctness
of relational model transformations. VeriMTLr draws on the Boogie intermediate verification
language to systematically design modular and reusable verifiers for a target relational
model transformation language. Our framework encapsulates an EMF metamodels library
and an OCL library within Boogie. The result is reduced cost and time required for a verifier’s
construction. Furthermore, VeriMTLr includes an ASM and EMFTVM bytecode
library, enabling an automated translation validation approach to ensuring the soundness of
the verification of the designed verifier. We demonstrate our VeriMTLr framework with the
design of verifiers for the Atlas Transformation Language and the SimpleGT graph transformation
language.
Subjects/Keywords: Formal Verification; Relational Model Transformations; Intermediate Verification Language
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Cheng, Z. (2016). Formal Verification of Relational Model
Transformations using an Intermediate
Verification Language. (Thesis). RIAN. Retrieved from http://eprints.maynoothuniversity.ie/7089/
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
Chicago Manual of Style (16th Edition):
Cheng, Zheng. “Formal Verification of Relational Model
Transformations using an Intermediate
Verification Language.” 2016. Thesis, RIAN. Accessed January 17, 2021.
http://eprints.maynoothuniversity.ie/7089/.
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
MLA Handbook (7th Edition):
Cheng, Zheng. “Formal Verification of Relational Model
Transformations using an Intermediate
Verification Language.” 2016. Web. 17 Jan 2021.
Vancouver:
Cheng Z. Formal Verification of Relational Model
Transformations using an Intermediate
Verification Language. [Internet] [Thesis]. RIAN; 2016. [cited 2021 Jan 17].
Available from: http://eprints.maynoothuniversity.ie/7089/.
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
Council of Science Editors:
Cheng Z. Formal Verification of Relational Model
Transformations using an Intermediate
Verification Language. [Thesis]. RIAN; 2016. Available from: http://eprints.maynoothuniversity.ie/7089/
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
Université de Grenoble
30.
Damri, Laila.
Génération de séquences de test pour l'accélération d'assertions : Generation of test sequences for accelerating assertions.
Degree: Docteur es, Sciences et technologie industrielles, 2012, Université de Grenoble
URL: http://www.theses.fr/2012GRENT065
► Avec la complexité croissante des systèmes sur puce, le processus de vérification devient une tâche de plus en plus cruciale à tous les niveaux du…
(more)
▼ Avec la complexité croissante des systèmes sur puce, le processus de vérification devient une tâche de plus en plus cruciale à tous les niveaux du cycle de conception, et monopolise une part importante du temps de développement. Dans ce contexte, l'assertion-based verification (ABV) a considérablement gagné en popularité ces dernières années. Il s'agit de spécifier le comportement attendu du système par l'intermédiaire de propriétés logico-temporelles, et de vérifier ces propriétés par des méthodes semi-formelles ou formelles. Des langages de spécification comme PSL ou SVA (standards IEEE) sont couramment utilisés pour exprimer ces propriétés. Des techniques de vérification statiques (model checking) ou dynamiques (validation en cours de simulation) peuvent être mises en œuvre. Nous nous plaçons dans le contexte de la vérification dynamique. A partir d'assertions exprimées en PSL ou SVA, des descriptions VHDL ou Verilog synthétisables de moniteurs matériels de surveillance peuvent être produites (outil Horus). Ces composants peuvent être utilisés pendant la conception (en simulation et/ou émulation pour le débug et la validation de circuits), ou comme composants embarqués, pour la surveillance du comportement de systèmes critiques. Pour l'analyse en phase de conception, que ce soit en simulation ou en émulation, le problème de la génération des séquences de test se pose. En effet, des séquences de test générées aléatoirement peuvent conduire à un faible taux de couverture des conditions d'activation des moniteurs et, de ce fait, peuvent être peu révélatrices de la satisfaction des assertions. Les méthodes de génération de séquences de test sous contraintes n'apportent pas de réelle solution car les contraintes ne peuvent pas être liées à des conditions temporelles. De nouvelles méthodes doivent être spécifiées et implémentées, c'est ce que nous nous proposons d'étudier dans cette thèse.
With the increasing complexity of SoC, the verification process becomes a task more crucial at all levels of the design cycle, and monopolize a large share of development time. In this context, the assertion-based verification (ABV) has gained considerable popularity in recent years. This is to specify the behavior of the system through logico-temporal properties and check these properties by semiformal or formal methods. Specification languages such as PSL or SVA (IEEE) are commonly used to express these properties. Static verification techniques (model checking) or dynamic (during simulation) can be implemented. We are placed in the context of dynamic verification. Our assertions are expressed in PSL or SVA, and synthesizable descriptions VHDL or Verilog hardware surveillance monitors can be produced (Horus tool). These components can be used for design (simulation and/or emulation for circuit debug and validation) or as embedded components for monitoring the behavior of critical systems. For analysis in the design phase, either in simulation or emulation, the problem of generating test sequences arises. In effect, sequences of…
Advisors/Committee Members: Pierre, Laurence (thesis director).
Subjects/Keywords: Vérification formelle; Vérification à base d'assertions; Formal verification; Assertion-based verification
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Damri, L. (2012). Génération de séquences de test pour l'accélération d'assertions : Generation of test sequences for accelerating assertions. (Doctoral Dissertation). Université de Grenoble. Retrieved from http://www.theses.fr/2012GRENT065
Chicago Manual of Style (16th Edition):
Damri, Laila. “Génération de séquences de test pour l'accélération d'assertions : Generation of test sequences for accelerating assertions.” 2012. Doctoral Dissertation, Université de Grenoble. Accessed January 17, 2021.
http://www.theses.fr/2012GRENT065.
MLA Handbook (7th Edition):
Damri, Laila. “Génération de séquences de test pour l'accélération d'assertions : Generation of test sequences for accelerating assertions.” 2012. Web. 17 Jan 2021.
Vancouver:
Damri L. Génération de séquences de test pour l'accélération d'assertions : Generation of test sequences for accelerating assertions. [Internet] [Doctoral dissertation]. Université de Grenoble; 2012. [cited 2021 Jan 17].
Available from: http://www.theses.fr/2012GRENT065.
Council of Science Editors:
Damri L. Génération de séquences de test pour l'accélération d'assertions : Generation of test sequences for accelerating assertions. [Doctoral Dissertation]. Université de Grenoble; 2012. Available from: http://www.theses.fr/2012GRENT065
◁ [1] [2] [3] [4] [5] … [16] ▶
. 
Open Access Theses and Dissertations
