Symboliset metodit muuntimille ja testaukseen

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.Symboliset metodit päättelevät joukoilla arvoja. Modernien satisfiability modulo theories (SMT) -ratkaisimien evoluutio on mahdollistanut kasvavan valikoiman symbolisia sovelluksia, jotka vaativat päättelyä rikkailla logiikoilla, kuten bittivektoreilla ja taulukoilla. SMT-ratkaisimet helpottavat ratkaisinteknologian käyttöä symbolisten metodien kehityksessä. Tämä väitöskirja edistää symbolisten metodien sovelluksia tietovirtojen käsittelyssä, testien generoinnissa ja ohjelmistojen verifioinnissa.Symboliset automaatit ja muuntimet ovat vastaavien klassisten mallien yleistyksiä, jotka siirtävät syötteisiin liittyvää päättelyä SMT-ratkaisimelle, mikä mahdollistaa erittäin suurten aakkostojen tehokkaan käytön. Tietovirtojen käsittelyssä ja suuren datan analytiikassa on hyödyllistä pystyä esittämään laskentaa sarjana modulaarisia vaiheita. Sarjana symbolisia muuntimia esitetty ohjelma on mahdollista tehokkaasti yhdistää yhdeksi vaiheeksi, mikä vähentää ylimääräistä kommunikaatiota. Tätä kutsutaan fuusioksi. Lisäksi näin yhdistettyjä muuntimia voidaan edelleen supistaa.Tämä väitöskirja esittelee työkalun, joka soveltaa fuusiota erinäisillä ohjelmointikielillä esitettyjen symbolisien muuntimien sarjoista koostuviin ohjelmiin. Fuusiota täydentävät saavutettavuusanalyysiin ja automaattien minimointiin perustuvat supistusmenetelmät. Työkalu tuottaa tehokasta koodia, jonka näytetään olevan suorituskyvyltään vertailukelpoista näytteeseen käsin optimoitua ei-modulaarista koodia, sekä tehokkaampaa kuin vaihtoehtoisilla menetelmillä fuusioidut ohjelmat.Dynaaminen symbolinen suoritus käyttää SMT-ratkaisimia generoidakseen tehokkaasti syötteitä testaukseen. Dash-algoritmi yhdistää dynaamisen symbolisen suorituksen ja predikaattiabstraktion. Tämä väitöskirja esittelee LLVM kääntäjäkirjastoa käyttävän toteutuksen Dash-algoritmista C-ohjelmien automaattista verifiointia varten. Tämä sisältää selityksen siitä, miten Dash-algoritmi toteutetaan LLVM:n välikielelle, sekä tavan parantaa verifoinnin suorituskykyä. Toteutettu työkalu LCTD on kilpailukykyinen vertailtuna joukolla SV-COMP-kilpailusta haettuja ohjelmia.Osittaisjärjestysreduktio on lähestymistapa, jolla voidaan käydä läpi supistettuja joukkoja rinnakkaisten ohjelmien testisuorituksia menettämättä virheiden saavutettavuutta. Tämä väitöskirja esittelee uuden version dynaamisesta osittaisjärjestysreduktiosta (DPOR), joka mahdollistaa lukuoperaatioiden kommutatiivisuuden hyödyntämisen. Uuden algoritmin DPOR-CR:n näytetään käyvän läpi huomattavasti vähemmän testisuorituksia kuin alkuperäinen. Lisäksi todistetaan, että synkronoimaton jaetun muistin käyttö voidaan tarkistaa edullisesti DPOR:n aikana