Physical Sciences and Mathematics Commons^™

Using Formal Methods To Verify Transactional Abstract Concurrency Control, Trek S. Palmer

Doctoral Dissertations

Concurrent application design and implementation is more important than ever in today's multi-core processor world. Transactional Memory (TM) Concurrent application design and implementation is more important than ever in today's multi-core processor world. Transactional Memory (TM). Each has its own particular advantages and disadvantages. However, these techniques each need some extra information to `glue' the non-transactional operation into a transactional context. At the most general level, non-transactional code must be decorated in such a way that the TM run-time can determine how those non-transactional operations commute with one another, and how to `undo' the non-transactional operations in case the run-time …

Program Analysis : Termination Proofs For Linear Simple Loops, Hongyi Chen

LSU Doctoral Dissertations

Termination proof synthesis for simple loops, i.e., loops with only conjoined constraints in the loop guard and variable updates in the loop body, is the building block of termination analysis, as well as liveness analysis, for large complex imperative systems. In particular, we consider a subclass of simple loops which contain only linear constraints in the loop guard and linear updates in the loop body. We call them Linear Simple Loops (LSLs). LSLs are particularly interesting because most loops in practice are indeed linear; more importantly, since we allow the update statements to handle nondeterminism, LSLs are expressive enough to …

Unification Modulo Theories Of Blind Signatures, Serdar Erbatur

Legacy Theses & Dissertations (2009 - 2024)

This thesis is concerned with equational unification problems that are relevant in formal verification of cryptographic protocols which deploy blind signature schemes. Blind signatures are signature schemes that keep the content confidential and have applications in modern cryptography for electronic voting and digital cash schemes. Equational unification problems studied here originate from blind RSA signatures and El Gamal encryption.

Behavioral Signature-Based Framework For Identifying Unsatisfiable Variable Mappings Between Digital Designs, Vaibhav Uday Tendulkar

Browse all Theses and Dissertations

Throughout its design process (from specification to implementation) a digital circuit goes through a variety of structural changes. These changes are introduced primarily due to the use of automated tools in the design process. Checking whether the Boolean functions representing the two designs are equivalent is thus necessary to verify if a design implementation adheres to its specification. Combinational Equivalence Checking (CEC) - a process of determining whether two combinational design functions are equiv-alent, has been one of the most researched Boolean matching problems. The well-known CEC techniques that have been proposed adopt some kind of a formal approach such …

Deductive Formal Verification Of Embedded Systems, Zheng Lu

LSU Doctoral Dissertations

We combine static analysis techniques with model-based deductive verification using SMT solvers to provide a framework that, given an analysis aspect of the source code, automatically generates an analyzer capable of inferring information about that aspect.

The analyzer is generated by translating the collecting semantics of a program to a formula in first order logic over multiple underlying theories. We import the semantics of the API invocations as first order logic assertions. These assertions constitute the models used by the analyzer. Logical specification of the desired program behavior is incorporated as a first order logic formula. An SMT-LIB solver treats …