Symbolic methods reason about groups of values. The evolution of modern satisfiability modulo theories (SMT) solvers has enabled an increasing variety of symbolic applications that require efficient reasoning in rich logics, such as bit vectors and arrays. SMT solvers remove barriers for employing solver technology in the development of symbolic methods. This dissertation contributes applications of symbolic methods in the areas of stream processing, test generation and software verification.Symbolic automata and transducers are generalizations of their respective classical models that shift reasoning about inputs to an SMT solver, which allows efficient use of very large alphabets. In the areas of stream processing and Big Data analytics, it is desirable to be able to represent computations as pipelines of modular processing stages. Pipelines represented as symbolic transducers can be efficiently fused into a single stage, which reduces communication overhead and enables further reductions.This dissertation presents a tool that applies fusion to pipelines of symbolic transducers specified in a variety of frontend languages. Fusion is supported by further reductions based on reachability analysis and automata minimization. The tool generates efficient fused code, which is shown to provide comparable performance to a sample of real-world, hand-optimized, monolithic code, as well as greater performance than alternative methods of composing modular pipelines of stream computations.Concolic testing is a popular approach for implementing symbolic execution, which commonly uses SMT solvers to efficiently generate test inputs. The Dash algorithm combines concolic testing with a predicate abstraction. This dissertation presents an implementation of Dash for automati- cally verifying sequential C programs on the LLVM compiler framework. A refinement strategy for the LLVM intermediate representation is presented and design considerations for reducing memory usage and improving verification performance are discussed. The resulting tool LCTD shows competitive results on a set of benchmarks drawn from SV-COMP.Partial order reduction is an approach for exploring reduced sets of interleavings between threads in a multi-threaded program. This dissertation presents an improvement to the dynamic partial order reduction (DPOR) algorithm, which exploits the commutativity of read operations to enable more reduction. The new algorithm DPOR-CR is shown to explore significantly fewer tests. Furthermore, a proof is presented that data races can be cheaply checked for during DPOR.
|Tila||Julkaistu - 2017|
|OKM-julkaisutyyppi||G5 Tohtorinväitöskirja (artikkeli)|