Symbolic Methods for Transducers and Testing

 |  Login

Show simple item record

dc.contributor Aalto-yliopisto fi
dc.contributor Aalto University en
dc.contributor.advisor Heljanko, Keijo, Assoc. Prof., Aalto University, Department of Computer Science, Finland
dc.contributor.author Saarikivi, Olli
dc.date.accessioned 2018-01-31T10:02:44Z
dc.date.available 2018-01-31T10:02:44Z
dc.date.issued 2017
dc.identifier.isbn 978-952-60-7787-1 (electronic)
dc.identifier.isbn 978-952-60-7786-4 (printed)
dc.identifier.issn 1799-4942 (electronic)
dc.identifier.issn 1799-4934 (printed)
dc.identifier.issn 1799-4934 (ISSN-L)
dc.identifier.uri https://aaltodoc.aalto.fi/handle/123456789/29705
dc.description.abstract 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. en
dc.description.abstract 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. fi
dc.format.extent 81 + app. 111
dc.format.mimetype application/pdf en
dc.language.iso en en
dc.publisher Aalto University en
dc.publisher Aalto-yliopisto fi
dc.relation.ispartofseries Aalto University publication series DOCTORAL DISSERTATIONS en
dc.relation.ispartofseries 255/2017
dc.relation.haspart [Publication 1]: Olli Saarikivi, Margus Veanes, Todd Mytkowicz, Madan Musuvathi. Fusing effectful comprehensions. In Proceedings of the 38th Conference on Programming Language Design and Implementation (PLDI 2017), pages 17–32. June 2017. DOI: 10.1145/3062341.3062362
dc.relation.haspart [Publication 2]: Olli Saarikivi, Margus Veanes. Minimization of symbolic transducers. In Proceedings of the 29th International Conference on Computer Aided Verification (CAV 2017), Part II, LNCS 10427, pages 176–196. July 2017. DOI: 10.1007/978-3-319-63390-9_10
dc.relation.haspart [Publication 3]: Olli Saarikivi, Margus Veanes. Translating C# to branching symbolic transducers. In 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-21), Short Presentations, pages 86–99, May 2017.
dc.relation.haspart [Publication 4]: Olli Saarikivi, Keijo Heljanko. LCTD: test-guided proofs for C programs on LLVM. Journal of Logic and Algebraic Methods in Programming (JLAMP), 85(6), pages 1292–1317. October 2016. DOI: 10.1016/j.jlamp.2015.10.010
dc.relation.haspart [Publication 5]: Olli Saarikivi, Kari Kahkonen, Keijo Heljanko. Improving dynamic partial order reductions for concolic testing. In Proceedings of the 12th International Conference on Application of Concurrency to System Design (ACSD 2012), pages 132–141. June2012. DOI: 10.1109/ACSD.2012.18
dc.relation.haspart [Publication 6]: Olli Saarikivi, Keijo Heljanko. Reporting races in dynamic partial order reduction. In Proceedings of NASA Formal Methods - 7th International Symposium (NFM 2015), LNCS 9058, pages 450–456, April 2015. DOI: 10.1007/978-3-319-17524-9_35
dc.subject.other Computer science en
dc.title Symbolic Methods for Transducers and Testing en
dc.title Symboliset metodit muuntimille ja testaukseen fi
dc.type G5 Artikkeliväitöskirja fi
dc.contributor.school Perustieteiden korkeakoulu fi
dc.contributor.school School of Science en
dc.contributor.department Tietotekniikan laitos fi
dc.contributor.department Department of Computer Science en
dc.subject.keyword symbolic methods en
dc.subject.keyword symbolic transducers en
dc.subject.keyword stream processing en
dc.subject.keyword stream fusion en
dc.subject.keyword test generation en
dc.subject.keyword software verification en
dc.subject.keyword partial order reduction en
dc.subject.keyword race detection en
dc.subject.keyword symboliset metodit fi
dc.subject.keyword symboliset muuntimet fi
dc.subject.keyword tietovirtojen prosessointi fi
dc.subject.keyword tietovirtojen fuusio fi
dc.subject.keyword testigenerointi fi
dc.subject.keyword ohjelmistojen verifiointi fi
dc.subject.keyword osittaisjärjestysreduktio fi
dc.identifier.urn URN:ISBN:978-952-60-7787-1
dc.type.dcmitype text en
dc.type.ontasot Doctoral dissertation (article-based) en
dc.type.ontasot Väitöskirja (artikkeli) fi
dc.contributor.supervisor Heljanko, Keijo, Assoc. Prof., Aalto University, Department of Computer Science, Finland
dc.opn Majumdar, Rupak, Adj. Prof., University of California, USA
dc.rev Aziz Abdulla, Parosh, Prof., Uppsala University, Sweden
dc.rev van de Pol, Jaco, Prof., University of Twente, The Netherlands
dc.date.defence 2018-02-16


Files in this item

This item appears in the following Collection(s)

Show simple item record

Search archive


Advanced Search

article-iconSubmit a publication

Browse

My Account