subject:(Formal verification)

University of Waterloo

1. Shehata, Hazem. Formal Verification of Instruction Dependencies in Microprocessors.

Degree: 2011, University of Waterloo

► 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

❌

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

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

Shehata, Hazem. “Formal Verification of Instruction Dependencies in Microprocessors.” 2011. Thesis, University of Waterloo. Accessed December 15, 2019. 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 (7^th Edition):

Shehata, Hazem. “Formal Verification of Instruction Dependencies in Microprocessors.” 2011. Web. 15 Dec 2019.

Vancouver:

Shehata H. Formal Verification of Instruction Dependencies in Microprocessors. [Internet] [Thesis]. University of Waterloo; 2011. [cited 2019 Dec 15]. 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

University of New South Wales

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

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

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

► Before software can be formally reasoned about, it must first be represented in some form of logic. There are two approaches to carrying out this… (more)

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

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

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Greenaway, D. (2014). Automated proof-producing abstraction of C code. (Doctoral Dissertation). University of New South Wales. Retrieved from http://handle.unsw.edu.au/1959.4/54260 ; https://unsworks.unsw.edu.au/fapi/datastream/unsworks:13743/SOURCE02?view=true

Chicago Manual of Style (16^th Edition):

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

MLA Handbook (7^th Edition):

Greenaway, David. “Automated proof-producing abstraction of C code.” 2014. Web. 15 Dec 2019.

Vancouver:

Greenaway D. Automated proof-producing abstraction of C code. [Internet] [Doctoral dissertation]. University of New South Wales; 2014. [cited 2019 Dec 15]. Available from: http://handle.unsw.edu.au/1959.4/54260 ; https://unsworks.unsw.edu.au/fapi/datastream/unsworks:13743/SOURCE02?view=true.

Council of Science Editors:

Greenaway D. Automated proof-producing abstraction of C code. [Doctoral Dissertation]. University of New South Wales; 2014. Available from: http://handle.unsw.edu.au/1959.4/54260 ; https://unsworks.unsw.edu.au/fapi/datastream/unsworks:13743/SOURCE02?view=true

University of Waterloo

3. Vediramana Krishnan, Hari Govind. Strong Induction in Hardware Model Checking.

Degree: 2019, University of Waterloo

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

► Symbolic Model checking is a widely used technique for automated verification of both hardware and software systems. Unbounded SAT-based Symbolic Model Checking (SMC) algorithms are… (more)

Subjects/Keywords: model checking; formal methods; formal verification; hardware verification

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Vediramana Krishnan, H. G. (2019). Strong Induction in Hardware Model Checking. (Thesis). University of Waterloo. Retrieved from http://hdl.handle.net/10012/14885

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

Chicago Manual of Style (16^th Edition):

Vediramana Krishnan, Hari Govind. “Strong Induction in Hardware Model Checking.” 2019. Thesis, University of Waterloo. Accessed December 15, 2019. http://hdl.handle.net/10012/14885.

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

MLA Handbook (7^th Edition):

Vediramana Krishnan, Hari Govind. “Strong Induction in Hardware Model Checking.” 2019. Web. 15 Dec 2019.

Vancouver:

Vediramana Krishnan HG. Strong Induction in Hardware Model Checking. [Internet] [Thesis]. University of Waterloo; 2019. [cited 2019 Dec 15]. Available from: http://hdl.handle.net/10012/14885.

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

Council of Science Editors:

Vediramana Krishnan HG. Strong Induction in Hardware Model Checking. [Thesis]. University of Waterloo; 2019. Available from: http://hdl.handle.net/10012/14885

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

Texas A&M University

4. 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

❌

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

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

Kottapalli, Venkateshwar. “Formal Verification of a MESI-based Cache Implementation.” 2017. Masters Thesis, Texas A&M University. Accessed December 15, 2019. http://hdl.handle.net/1969.1/165866.

MLA Handbook (7^th Edition):

Kottapalli, Venkateshwar. “Formal Verification of a MESI-based Cache Implementation.” 2017. Web. 15 Dec 2019.

Vancouver:

Kottapalli V. Formal Verification of a MESI-based Cache Implementation. [Internet] [Masters thesis]. Texas A&M University; 2017. [cited 2019 Dec 15]. 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 Oxford

5. Kattenbelt, Mark Alex. Automated quantitative software verification.

Degree: PhD, 2010, University of Oxford

URL: http://ora.ox.ac.uk/objects/uuid:62430df4-7fdf-4c4f-b3cd-97ba8912c9f5 ; https://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.540281

► Many software systems exhibit probabilistic behaviour, either added explicitly, to improve performance or to break symmetry, or implicitly, through interaction with unreliable networks or faulty… (more)

▼ Many software systems exhibit probabilistic behaviour, either added explicitly, to improve performance or to break symmetry, or implicitly, through interaction with unreliable networks or faulty hardware. When employed in safety-critical applications, it is important to rigorously analyse the behaviour of these systems. This can be done with a formal verification technique called model checking, which establishes properties of systems by algorithmically considering all execution scenarios. In the presence of probabilistic behaviour, we consider quantitative properties such as "the worst-case probability that the airbag fails to deploy within 10ms", instead of qualitative properties such as "the airbag eventually deploys". Although many model checking techniques exist to verify qualitative properties of software, quantitative model checking techniques typically focus on manually derived models of systems and cannot directly verify software. In this thesis, we present two quantitative model checking techniques for probabilistic software. The first is a quantitative adaptation of a successful model checking technique called counter-example guided abstraction refinement which uses stochastic two-player games as abstractions of probabilistic software. We show how to achieve abstraction and refinement in a probabilistic setting and investigate theoretical extensions of stochastic two-player game abstractions. Our second technique instruments probabilistic software in such a way that existing, non-probabilistic software verification methods can be used to compute bounds on quantitative properties of the original, uninstrumented software. Our techniques are the first to target real, compilable software in a probabilistic setting. We present an experimental evaluation of both approaches on a large range of case studies and evaluate several extensions and heuristics. We demonstrate that, with our methods, we can successfully compute quantitative properties of real network clients comprising approximately 1,000 lines of complex ANSI-C code — the verification of such software is far beyond the capabilities of existing quantitative model checking techniques.

Subjects/Keywords: 005.3; Theory and automated verification; model checking; quantitative; verification; software; formal methods; formal verification; software verification

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Kattenbelt, M. A. (2010). Automated quantitative software verification. (Doctoral Dissertation). University of Oxford. Retrieved from http://ora.ox.ac.uk/objects/uuid:62430df4-7fdf-4c4f-b3cd-97ba8912c9f5 ; https://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.540281

Chicago Manual of Style (16^th Edition):

Kattenbelt, Mark Alex. “Automated quantitative software verification.” 2010. Doctoral Dissertation, University of Oxford. Accessed December 15, 2019. http://ora.ox.ac.uk/objects/uuid:62430df4-7fdf-4c4f-b3cd-97ba8912c9f5 ; https://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.540281.

MLA Handbook (7^th Edition):

Kattenbelt, Mark Alex. “Automated quantitative software verification.” 2010. Web. 15 Dec 2019.

Vancouver:

Kattenbelt MA. Automated quantitative software verification. [Internet] [Doctoral dissertation]. University of Oxford; 2010. [cited 2019 Dec 15]. Available from: http://ora.ox.ac.uk/objects/uuid:62430df4-7fdf-4c4f-b3cd-97ba8912c9f5 ; https://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.540281.

Council of Science Editors:

Kattenbelt MA. Automated quantitative software verification. [Doctoral Dissertation]. University of Oxford; 2010. Available from: http://ora.ox.ac.uk/objects/uuid:62430df4-7fdf-4c4f-b3cd-97ba8912c9f5 ; https://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.540281

University of Utah

6. 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

❌

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

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

Xu, Yang. “Algorithms for automatic generation of relative timing constraints.” 2011. Doctoral Dissertation, University of Utah. Accessed December 15, 2019. http://content.lib.utah.edu/cdm/singleitem/collection/etd3/id/197/rec/177.

MLA Handbook (7^th Edition):

Xu, Yang. “Algorithms for automatic generation of relative timing constraints.” 2011. Web. 15 Dec 2019.

Vancouver:

Xu Y. Algorithms for automatic generation of relative timing constraints. [Internet] [Doctoral dissertation]. University of Utah; 2011. [cited 2019 Dec 15]. 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

The Ohio State University

7. 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

❌

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

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

Zaccai, Diego Sebastian. “A Balanced Verification Effort for the Java Language.” 2016. Doctoral Dissertation, The Ohio State University. Accessed December 15, 2019. http://rave.ohiolink.edu/etdc/view?acc_num=osu1461243619.

MLA Handbook (7^th Edition):

Zaccai, Diego Sebastian. “A Balanced Verification Effort for the Java Language.” 2016. Web. 15 Dec 2019.

Vancouver:

Zaccai DS. A Balanced Verification Effort for the Java Language. [Internet] [Doctoral dissertation]. The Ohio State University; 2016. [cited 2019 Dec 15]. 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

8. 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)

Subjects/Keywords: 004.2; hybrid systems; ODEs; formal verification

11 more images…

Record Details Similar Records Cite « Share

❌

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

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

Sogokon, Andrew. “Direct methods for deductive verification of temporal properties in continuous dynamical systems.” 2016. Doctoral Dissertation, University of Edinburgh. Accessed December 15, 2019. http://hdl.handle.net/1842/20952.

MLA Handbook (7^th Edition):

Sogokon, Andrew. “Direct methods for deductive verification of temporal properties in continuous dynamical systems.” 2016. Web. 15 Dec 2019.

Vancouver:

Sogokon A. Direct methods for deductive verification of temporal properties in continuous dynamical systems. [Internet] [Doctoral dissertation]. University of Edinburgh; 2016. [cited 2019 Dec 15]. 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

University of Manchester

9. 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

❌

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

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

Carter, Rebekah. “Verification of liveness properties on hybrid dynamical systems.” 2013. Doctoral Dissertation, University of Manchester. Accessed December 15, 2019. 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 (7^th Edition):

Carter, Rebekah. “Verification of liveness properties on hybrid dynamical systems.” 2013. Web. 15 Dec 2019.

Vancouver:

Carter R. Verification of liveness properties on hybrid dynamical systems. [Internet] [Doctoral dissertation]. University of Manchester; 2013. [cited 2019 Dec 15]. 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 Colorado

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

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

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

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

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

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

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

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

Chicago Manual of Style (16^th Edition):

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

MLA Handbook (7^th Edition):

Hassan, Zyad. “Incremental, Inductive Model Checking.” 2014. Web. 15 Dec 2019.

Vancouver:

Hassan Z. Incremental, Inductive Model Checking. [Internet] [Doctoral dissertation]. University of Colorado; 2014. [cited 2019 Dec 15]. 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 Sydney

11. 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)

Subjects/Keywords: Static Analysis; Abstract Interpretation; Formal Verification; LLVM

Record Details Similar Records Cite « Share

❌

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

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

Subotic, Pavle. “Applying Elimination-Based Algorithms to Abstract Interpretation .” 2014. Thesis, University of Sydney. Accessed December 15, 2019. 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 (7^th Edition):

Subotic, Pavle. “Applying Elimination-Based Algorithms to Abstract Interpretation .” 2014. Web. 15 Dec 2019.

Vancouver:

Subotic P. Applying Elimination-Based Algorithms to Abstract Interpretation . [Internet] [Thesis]. University of Sydney; 2014. [cited 2019 Dec 15]. 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

Clemson University

12. 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

❌

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

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

Smith, Hampton. “Engineering Specifications and Mathematics for Verified Software.” 2013. Doctoral Dissertation, Clemson University. Accessed December 15, 2019. https://tigerprints.clemson.edu/all_dissertations/1132.

MLA Handbook (7^th Edition):

Smith, Hampton. “Engineering Specifications and Mathematics for Verified Software.” 2013. Web. 15 Dec 2019.

Vancouver:

Smith H. Engineering Specifications and Mathematics for Verified Software. [Internet] [Doctoral dissertation]. Clemson University; 2013. [cited 2019 Dec 15]. 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

University of Ottawa

13. 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

❌

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

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

Sistany, Bahman. “A Certified Core Policy Language .” 2016. Thesis, University of Ottawa. Accessed December 15, 2019. 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 (7^th Edition):

Sistany, Bahman. “A Certified Core Policy Language .” 2016. Web. 15 Dec 2019.

Vancouver:

Sistany B. A Certified Core Policy Language . [Internet] [Thesis]. University of Ottawa; 2016. [cited 2019 Dec 15]. 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 Oklahoma

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

Degree: PhD, 2016, University of Oklahoma

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

► Software spends a significant portion of its life-cycle in the maintenance phase and over 20% of the maintenance effort is fixing defects. Formal methods, including… (more)

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

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

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Ralston, R. (2016). Translating Clojure to ACL2 for Verification. (Doctoral Dissertation). University of Oklahoma. Retrieved from http://hdl.handle.net/11244/42982

Chicago Manual of Style (16^th Edition):

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

MLA Handbook (7^th Edition):

Ralston, Ryan. “Translating Clojure to ACL2 for Verification.” 2016. Web. 15 Dec 2019.

Vancouver:

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

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)

Subjects/Keywords: Formal Semantics; P4; K Framework; Network Verification

Record Details Similar Records Cite « Share

❌

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

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

Kheradmand, Ali. “A formal semantics of P4 and applications.” 2018. Thesis, University of Illinois – Urbana-Champaign. Accessed December 15, 2019. 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 (7^th Edition):

Kheradmand, Ali. “A formal semantics of P4 and applications.” 2018. Web. 15 Dec 2019.

Vancouver:

Kheradmand A. A formal semantics of P4 and applications. [Internet] [Thesis]. University of Illinois – Urbana-Champaign; 2018. [cited 2019 Dec 15]. 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

Kansas State University

16. 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)

Subjects/Keywords: Formal Methods; Language Semantics; Program Verification

Record Details Similar Records Cite « Share

❌

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

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

Zhang, Zhi. “A formal approach to contract verification for high-integrity applications.” 2016. Doctoral Dissertation, Kansas State University. Accessed December 15, 2019. http://hdl.handle.net/2097/32880.

MLA Handbook (7^th Edition):

Zhang, Zhi. “A formal approach to contract verification for high-integrity applications.” 2016. Web. 15 Dec 2019.

Vancouver:

Zhang Z. A formal approach to contract verification for high-integrity applications. [Internet] [Doctoral dissertation]. Kansas State University; 2016. [cited 2019 Dec 15]. 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 New South Wales

17. 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

❌

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

APA (6^th 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 (16^th 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 December 15, 2019. http://handle.unsw.edu.au/1959.4/53099 ; https://unsworks.unsw.edu.au/fapi/datastream/unsworks:11785/SOURCE01?view=true.

MLA Handbook (7^th Edition):

von Tessin, Michael. “The clustered multikernel: an approach to formal verification of multiprocessor operating-system kernels.” 2013. Web. 15 Dec 2019.

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 2019 Dec 15]. 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

Boise State University

18. 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)

Subjects/Keywords: privacy; formal verification; Other Computer Engineering

Record Details Similar Records Cite « Share

❌

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

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

Joshaghani, Rezvan. “UNICORN Framework: A User-Centric Approach Toward Formal Verification of Privacy Norms.” 2019. Thesis, Boise State University. Accessed December 15, 2019. 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 (7^th Edition):

Joshaghani, Rezvan. “UNICORN Framework: A User-Centric Approach Toward Formal Verification of Privacy Norms.” 2019. Web. 15 Dec 2019.

Vancouver:

Joshaghani R. UNICORN Framework: A User-Centric Approach Toward Formal Verification of Privacy Norms. [Internet] [Thesis]. Boise State University; 2019. [cited 2019 Dec 15]. 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

University of Illinois – Urbana-Champaign

19. 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)

Subjects/Keywords: Programming Languages; Formal Methods; Hardware Verification

Record Details Similar Records Cite « Share

❌

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

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

Katelman, Michael. “A meta-language for functional verification.” 2012. Doctoral Dissertation, University of Illinois – Urbana-Champaign. Accessed December 15, 2019. http://hdl.handle.net/2142/29614.

MLA Handbook (7^th Edition):

Katelman, Michael. “A meta-language for functional verification.” 2012. Web. 15 Dec 2019.

Vancouver:

Katelman M. A meta-language for functional verification. [Internet] [Doctoral dissertation]. University of Illinois – Urbana-Champaign; 2012. [cited 2019 Dec 15]. 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 New South Wales

20. Elkaduwe, Karunadipathi Wasala H. M. R. D. D. B. A Principled approach to kernel memory management.

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

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

► Small kernels are a promising approach to secure and reliable system construction. These systems reduce the size of the kernel to a point where it… (more)

▼ Small kernels are a promising approach to secure and reliable system construction. These systems reduce the size of the kernel to a point where it is feasible to formally verify the implementation correctness of the kernel with respect to an abstract formal model of the kernel's behaviour. The system is composed of user-level components, isolated from one another using the kernel-provided mechanisms. The abstract formal model facilitates the enforcement, and reasoning about the enforcement of different policies between these user-level components. However, existing formal models only capture the application-level interface of a small kernel with no clear relationship between the externally visible access control model and the kernel's low-level management of physical memory. In this work, a model for managing the in-kernel memory of a formally verified, small kernel is designed and evaluated for its formal and empirical characteristics. The design eliminates all implicit memory allocations within the kernel by promoting all dynamically allocated kernel memory into first-class, explicitly allocated kernel objects. This reduces the problem of physical memory management within the kernel to that of controlling the authority to perform these explicit allocations and controlling the dissemination of authority over already allocated objects. A formal protection model that unifies in-kernel management of physical memory with access control is developed by extending the take-grant model. A formal analysis carried out on the above developed model demonstrates that the model is capable of enforcing spatial partitioning and isolation. The extension preserves the decidability of the original take-grant model while providing the ability to reason about kernel memory consumption of components which is not feasible in the original model. Performance of the model is evaluated using a prototype implementation based on an L4 microkernel. The analysis shows no significant performance degradation due to exporting all in-kernel memory allocations to user-level. When enforcing spatial partitioning to a para-virtualised Linux kernel the model shows performance improvements compared to a L4 based system enforcing a similar policy by run-time monitoring and shows similar performance to a L4 system that attempts no control over memory consumption and a Xen based system. This work demonstrates the feasibility of exporting all in-kernel memory allocations to user-level resource managers through a capability-based, decidable, protection model. The model shows no performance degradation in the scenarios examined and can be used to make strong formal guarantees on memory consumption of components. Advisors/Committee Members: Elphinstone, Kevin, Computer Science & Engineering, Faculty of Engineering, UNSW, Heiser, Gernot, Computer Science & Engineering, Faculty of Engineering, UNSW.

Subjects/Keywords: Kernel memory management; Microkernels; Security; Formal verification

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Elkaduwe, K. W. H. M. R. D. D. B. (2010). A Principled approach to kernel memory management. (Doctoral Dissertation). University of New South Wales. Retrieved from http://handle.unsw.edu.au/1959.4/45068 ; https://unsworks.unsw.edu.au/fapi/datastream/unsworks:8363/SOURCE02?view=true

Chicago Manual of Style (16^th Edition):

Elkaduwe, Karunadipathi Wasala H M R D D B. “A Principled approach to kernel memory management.” 2010. Doctoral Dissertation, University of New South Wales. Accessed December 15, 2019. http://handle.unsw.edu.au/1959.4/45068 ; https://unsworks.unsw.edu.au/fapi/datastream/unsworks:8363/SOURCE02?view=true.

MLA Handbook (7^th Edition):

Elkaduwe, Karunadipathi Wasala H M R D D B. “A Principled approach to kernel memory management.” 2010. Web. 15 Dec 2019.

Vancouver:

Elkaduwe KWHMRDDB. A Principled approach to kernel memory management. [Internet] [Doctoral dissertation]. University of New South Wales; 2010. [cited 2019 Dec 15]. Available from: http://handle.unsw.edu.au/1959.4/45068 ; https://unsworks.unsw.edu.au/fapi/datastream/unsworks:8363/SOURCE02?view=true.

Council of Science Editors:

Elkaduwe KWHMRDDB. A Principled approach to kernel memory management. [Doctoral Dissertation]. University of New South Wales; 2010. Available from: http://handle.unsw.edu.au/1959.4/45068 ; https://unsworks.unsw.edu.au/fapi/datastream/unsworks:8363/SOURCE02?view=true

University of New South Wales

21. 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)

Subjects/Keywords: Formal verification; Separation logic; Virtual memory

Record Details Similar Records Cite « Share

❌

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

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

Kolanski, Rafal Michal. “Verification of programs in virtual memory using separation logic.” 2011. Doctoral Dissertation, University of New South Wales. Accessed December 15, 2019. http://handle.unsw.edu.au/1959.4/51288 ; https://unsworks.unsw.edu.au/fapi/datastream/unsworks:9969/SOURCE02?view=true.

MLA Handbook (7^th Edition):

Kolanski, Rafal Michal. “Verification of programs in virtual memory using separation logic.” 2011. Web. 15 Dec 2019.

Vancouver:

Kolanski RM. Verification of programs in virtual memory using separation logic. [Internet] [Doctoral dissertation]. University of New South Wales; 2011. [cited 2019 Dec 15]. 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

University of Texas – Austin

22. -4047-4940. Extending capability of formal tools : applying semiformal verification on large design.

Degree: MSin Engineering, Electrical and Computer Engineering, 2019, University of Texas – Austin

URL: http://dx.doi.org/10.26153/tsw/5533

► Simulation and formal verification are the two most commonly used techniques for verifying a digital design described at the Register-Transfer Level (RTL). Compared to simulation,… (more)

Subjects/Keywords: Formal engine; Semiformal verification; Waypoint; Neural network

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

-4047-4940. (2019). Extending capability of formal tools : applying semiformal verification on large design. (Masters Thesis). University of Texas – Austin. Retrieved from http://dx.doi.org/10.26153/tsw/5533

Note: this citation may be lacking information needed for this citation format:
Author name may be incomplete

Chicago Manual of Style (16^th Edition):

-4047-4940. “Extending capability of formal tools : applying semiformal verification on large design.” 2019. Masters Thesis, University of Texas – Austin. Accessed December 15, 2019. http://dx.doi.org/10.26153/tsw/5533.

Note: this citation may be lacking information needed for this citation format:
Author name may be incomplete

MLA Handbook (7^th Edition):

-4047-4940. “Extending capability of formal tools : applying semiformal verification on large design.” 2019. Web. 15 Dec 2019.

Note: this citation may be lacking information needed for this citation format:
Author name may be incomplete

Vancouver:

-4047-4940. Extending capability of formal tools : applying semiformal verification on large design. [Internet] [Masters thesis]. University of Texas – Austin; 2019. [cited 2019 Dec 15]. Available from: http://dx.doi.org/10.26153/tsw/5533.

Note: this citation may be lacking information needed for this citation format:
Author name may be incomplete

Council of Science Editors:

-4047-4940. Extending capability of formal tools : applying semiformal verification on large design. [Masters Thesis]. University of Texas – Austin; 2019. Available from: http://dx.doi.org/10.26153/tsw/5533

Note: this citation may be lacking information needed for this citation format:
Author name may be incomplete

University of Newcastle

23. 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

❌

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

APA (6^th 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 (16^th 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 December 15, 2019. http://hdl.handle.net/1959.13/1397849.

MLA Handbook (7^th Edition):

Hogavanaghatta Kumaraswamy, Jnanamurthy. “Model-driven engineering to enhance the reliability of software development by verifying system properties and detecting clones.” 2019. Web. 15 Dec 2019.

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 2019 Dec 15]. 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

24. Bockenek, Joshua A. USIMPL: An Extension of Isabelle/UTP with Simpl-like Control Flow.

Degree: MS, Electrical and 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)

Subjects/Keywords: Formal Verification; Formal Methods; Isabelle; Unifying Theories of Programming; Verification Condition Generation

1 more image…

Record Details Similar Records Cite « Share

❌

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

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

Bockenek, Joshua A. “USIMPL: An Extension of Isabelle/UTP with Simpl-like Control Flow.” 2017. Masters Thesis, Virginia Tech. Accessed December 15, 2019. http://hdl.handle.net/10919/81710.

MLA Handbook (7^th Edition):

Bockenek, Joshua A. “USIMPL: An Extension of Isabelle/UTP with Simpl-like Control Flow.” 2017. Web. 15 Dec 2019.

Vancouver:

Bockenek JA. USIMPL: An Extension of Isabelle/UTP with Simpl-like Control Flow. [Internet] [Masters thesis]. Virginia Tech; 2017. [cited 2019 Dec 15]. 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

Universitat Politècnica de València

25. 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

❌

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

APA (6^th 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 (16^th 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 December 15, 2019. http://hdl.handle.net/10251/63152.

MLA Handbook (7^th Edition):

Peiró Frasquet, Salvador. “Metodología para hipervisores seguros utilizando técnicas de validación formal .” 2016. Web. 15 Dec 2019.

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 2019 Dec 15]. 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

University of Utah

26. 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

❌

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

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

Pruss, Tim. “Word-level abstraction from combinational circuits using algebraic geometry.” 2015. Doctoral Dissertation, University of Utah. Accessed December 15, 2019. http://content.lib.utah.edu/cdm/singleitem/collection/etd3/id/3965/rec/2938.

MLA Handbook (7^th Edition):

Pruss, Tim. “Word-level abstraction from combinational circuits using algebraic geometry.” 2015. Web. 15 Dec 2019.

Vancouver:

Pruss T. Word-level abstraction from combinational circuits using algebraic geometry. [Internet] [Doctoral dissertation]. University of Utah; 2015. [cited 2019 Dec 15]. 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

Université de Grenoble

27. 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

❌

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

APA (6^th 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 (16^th 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 December 15, 2019. http://www.theses.fr/2012GRENT065.

MLA Handbook (7^th 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. 15 Dec 2019.

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 2019 Dec 15]. 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

28. 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)

Subjects/Keywords: Formal Verification; Relational Model Transformations; Intermediate Verification Language

Record Details Similar Records Cite « Share

❌

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

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

Cheng, Zheng. “Formal Verification of Relational Model Transformations using an Intermediate Verification Language.” 2016. Thesis, RIAN. Accessed December 15, 2019. 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 (7^th Edition):

Cheng, Zheng. “Formal Verification of Relational Model Transformations using an Intermediate Verification Language.” 2016. Web. 15 Dec 2019.

Vancouver:

Cheng Z. Formal Verification of Relational Model Transformations using an Intermediate Verification Language. [Internet] [Thesis]. RIAN; 2016. [cited 2019 Dec 15]. 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

29. Moore, Brandon Michael. Coinductive program verification.

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

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

► We present a program-verification approach based on coinduction, which makes it feasible to verify programs given an operational semantics of a programming language, without constructing… (more)

Subjects/Keywords: Program Verification; Coinduction; Operational Semantics; Formal Methods; Software Verification

1 more image…

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Moore, B. M. (2016). Coinductive program verification. (Doctoral Dissertation). University of Illinois – Urbana-Champaign. Retrieved from http://hdl.handle.net/2142/95372

Chicago Manual of Style (16^th Edition):

Moore, Brandon Michael. “Coinductive program verification.” 2016. Doctoral Dissertation, University of Illinois – Urbana-Champaign. Accessed December 15, 2019. http://hdl.handle.net/2142/95372.

MLA Handbook (7^th Edition):

Moore, Brandon Michael. “Coinductive program verification.” 2016. Web. 15 Dec 2019.

Vancouver:

Moore BM. Coinductive program verification. [Internet] [Doctoral dissertation]. University of Illinois – Urbana-Champaign; 2016. [cited 2019 Dec 15]. Available from: http://hdl.handle.net/2142/95372.

Council of Science Editors:

Moore BM. Coinductive program verification. [Doctoral Dissertation]. University of Illinois – Urbana-Champaign; 2016. Available from: http://hdl.handle.net/2142/95372

Duke University

30. Matthews, Opeoluwa. A Formal Framework for Designing Verifiable Protocols .

Degree: 2017, Duke University

URL: http://hdl.handle.net/10161/16236

► Protocols play critical roles in computer systems today, including managing resources, facilitating communication, and coordinating actions of components. It is highly desirable to formally… (more)

▼ Protocols play critical roles in computer systems today, including managing resources, facilitating communication, and coordinating actions of components. It is highly desirable to formally verify protocols, to provide a mathematical guarantee that they behave correctly. Ideally, one would pass a model of a protocol into a formal verification tool, push a button, and the tool uncovers bugs or certifies that the protocol behaves correctly. Unfortunately, as a result of the state explosion problem, automated formal verification tools struggle to verify the increasingly complex protocols that appear in computer systems today. We observe that design decisions have a significant impact on the scalability of verifying a protocol in a formal verification tool. Hence, we present a formal framework that guides architects in designing protocols specifically to be verifiable with state of the art formal verification tools. If architects design protocols to fit our framework, the protocols inherit scalable automated verification. Key to our framework is a modular approach to constructing protocols from pre-verified subprotocols. We formulate properties that can be proven in automated tools to hold on these subprotocols, guaranteeing that any arbitrary composition of the subprotocols behaves correctly. The result is that we can design complex hierarchical (tree) protocols that are formally verified, using fully automated tools, for any number of nodes or any configuration of the tree. Our framework is applicable to a large class of protocols, including power management, cache coherence, and distributed lock management protocols. To demonstrate the efficacy of our framework, we design and verify a realistic hierarchical (tree) coherence protocol, using a fully automated tool to prove that it behaves correctly for any configuration of the tree. We identify certain protocol optimizations prohibited by our framework or the state of the art verification tools and we evaluate our verified protocol against unverifiable protocols that feature these optimizations. We find that these optimizations have a negligible impact on performance. We hope that our framework can be used to design a wide variety of protocols that are verifiable, high-performing, and architecturally flexible. Advisors/Committee Members: Sorin, Daniel J (advisor).

Subjects/Keywords: Computer engineering; Cache Coherence; Formal Verification; Model Checking; Parameterized verification; Protocols; Verification-aware architecture

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Matthews, O. (2017). A Formal Framework for Designing Verifiable Protocols . (Thesis). Duke University. Retrieved from http://hdl.handle.net/10161/16236

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

Chicago Manual of Style (16^th Edition):

Matthews, Opeoluwa. “A Formal Framework for Designing Verifiable Protocols .” 2017. Thesis, Duke University. Accessed December 15, 2019. http://hdl.handle.net/10161/16236.

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

MLA Handbook (7^th Edition):

Matthews, Opeoluwa. “A Formal Framework for Designing Verifiable Protocols .” 2017. Web. 15 Dec 2019.

Vancouver:

Matthews O. A Formal Framework for Designing Verifiable Protocols . [Internet] [Thesis]. Duke University; 2017. [cited 2019 Dec 15]. Available from: http://hdl.handle.net/10161/16236.

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

Council of Science Editors:

Matthews O. A Formal Framework for Designing Verifiable Protocols . [Thesis]. Duke University; 2017. Available from: http://hdl.handle.net/10161/16236

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

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

Open Access Theses and Dissertations