Global ETD Search
Search theses and dissertations gathered from participating repositories worldwide. Every result links back to the library that holds it. No account is needed.
Results
Showing 1 to 11 of 11 for “"Hoare logic"”.
-
USIMPL: An Extension of Isabelle/UTP with Simpl-like Control Flow
… proofs of program correctness utilizing Hoare logic and Hoare-style algebraic laws of programming.
-
Policy-Based Pervasive Systems Management Using Specification-Enhanced Rules
… formally state the effect of an action using Hoare logic as pre- and post-conditions. This framework facilitates advanced conflict and cycle analysis, determines enforcement order when multiple rules are simultaneously triggered, supports policy exception handling and provides reasoning …
-
Certifying a crash-safe file system
… state FSCQ's theorems, FSCQ introduces the Crash Hoare Logic (CHL), which extends traditional Hoare logic with a crash condition, a recovery procedure, and logical address spaces for specifying disk states at different abstraction levels. CHL also reduces the proof effort for developers through …
-
Forward with separation logic
The use of Hoare logic in combination with weakest preconditions and strongest postconditions is a standard tool for program verification, known as backward and forward reasoning. Separation logic, an extension of Hoare logic, finds countless applications in the areas of program verification, but …
-
An Interactive Theorem Prover for First-Order Dynamic Logic
Dynamic logic is an extension of modal logic originally intended for reasoning about computer programs. The method of proving correctness of properties of a computer program using the well-known Hoare Logic can be implemented by utilizing the robustness of dynamic logic. For a very broad range of …
-
Symbolic semantics for CSP
… transition semantics has been given by Brookes, Hoare and Roscoe. In this thesis, we present a generalized transition semantics of CSP, which we call HCSP, that merges the original transition system with ideas from Floyd-Hoare logic and symbolic computation. This generalized semantics is shown to …
-
Certificação de composições de serviços web semânticos
… This dimension is formalized by a Hoare logic based calculus. Partial correctness specifications involving compositions of semantic web services can be derived from the deductive system proposed. Our work is also characterized by exploiting the use of a fragment of description …
-
Formally Verified Code Obfuscation in the Coq Proof Assistant
… transformations. Along the way, we also employ Hoare logic as an alternative to state equivalence, as well as augment the IMP program with Switch statements. We also define a lower-level flowchart language to wrap around IMP for modelling certain flattening transformations, treating blocks of …
-
A Language and Logic for Programming and Reasoning with Partial Observability
… for the MPL. I will also present Epistemic Hoare Logic (EHL), a program logic for belief programs that enables developers to reason about properties of the resulting state estimators. I have used EHL to prove that the BLIMP version of the MPL does not have the error that caused the original …
-
FORMAL VERIFICATION-BASED PROGRAM REPAIR
Automated program repair has been an active research field in software engineering in the last decade. It aims to help developers automatically localize and fix program bugs, consequently reducing debugging efforts. Automated repair tools have been incorporated into continuous integration and code …
-
Automatic techniques for proving correctness of heap-manipulating programs
… verification. This dissertation presents two logic-based automatic software verification systems, namely Strand and Dryad, that help in the task of verification of heap-manipulating programs, which is one of the most complex aspects of modern software that eludes automatic verification. Strand …