Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Quantitative Analysis of Exploration Schedules for Symbolic Execution
KTH, School of Computer Science and Communication (CSC).
2017 (English)Independent thesis Advanced level (degree of Master (Two Years)), 20 credits / 30 HE creditsStudent thesisAlternative title
Kvantitativ analys av utforskningsscheman för Symbolisk Exekvering (Swedish)
Abstract [en]

Due to complexity in software, manual testing is not enough to cover all relevant behaviours of it. A different approach to this problem is Symbolic Execution.

Symbolic Execution is a software testing technique that tests all possible inputs of a program in the hopes of finding all bugs. Due to the often exponential increase in possible program paths, Symbolic Execution usually cannot exhaustively test a program. To nevertheless cover the most important or error prone areas of a program, search strategies that prioritize these areas are used. Such search strategies navigate the program execution tree, analysing which paths seem interesting enough to execute and which to prune. These strategies are typically grouped into two categories, general purpose searchers, with no specific target but the aim to cover the whole program and targeted searchers which can be directed towards specific areas of interest.

To analyse how different searching strategies in Symbolic Execution affect the finding of errors and how they can be combined to improve the general outcome, the experiments conducted consist of several different searchers and combinations of them, each run on the same set of test targets. This set of test targets contains amongst others one of the most heavily tested sets of open source tools, the GNU Coreutils. With these, the different strategies are compared in distinct categories like the total number of errors found or the percentage of covered code.

With the results from this thesis the potential of targeted searchers is shown, with an example implementation of the Pathscore-Relevance strategy. Further, the results obtained from the conducted experiments endorse the use of combinations of search strategies. It is also shown that, even simple combinations of strategies can be highly effective. For example, interleaving strategies can provide good results even if the underlying searchers might not perform well by themselves.

Abstract [sv]

På grund av programvarukomplexitet är manuell testning inte tillräcklig för att täcka alla relevanta beteenden av programvaror. Ett annat tillvägagångssätt till detta problem är Symbolisk Exekvering (Symbolic Execution).

Symbolisk Exekvering är en mjukvarutestningsteknik som testar alla möjliga inmatningari ett program i hopp om att hitta alla buggar. På grund av den ofta exponentiella ökningeni möjliga programsökvägar kan Symbolisk Exekvering vanligen inte uttömmande testa ettprogram. För att ändå täcka de viktigaste eller felbenägna områdena i ett program, används sökstrategier som prioriterar dessa områden. Sådana sökstrategier navigerar i programexekveringsträdet genom att analysera vilka sökvägar som verkar intressanta nog att utföra och vilka att beskära. Dessa strategier grupperas vanligtvis i två kategorier, sökare med allmänt syfte, utan något specifikt mål förutom att täcka hela programmet, och riktade sökare som kan riktas mot specifika intresseområden.

För att analysera hur olika sökstrategier i Symbolisk Exekvering påverkar upptäckandetav fel och hur de kan kombineras för att förbättra det allmänna utfallet, bestod de experimentsom utfördes av flera olika sökare och kombinationer av dem, som alla kördes på samma uppsättning av testmål. Denna uppsättning av testmål innehöll bland annat en av de mest testade uppsättningarna av öppen källkod-verktyg, GNU Coreutils. Med dessa jämfördes de olika strategierna i distinkta kategorier såsom det totala antalet fel som hittats eller procenttalet av täckt kod.

Med resultaten från denna avhandling visas potentialen hos riktade sökare, med ett exempeli form av implementeringen av Pathscore-Relevance strategin. Vidare stöder resultaten som erhållits från de utförda experimenten användningen av sökstrategikombinationer. Det visas också att även enkla kombinationer av strategier kan vara mycket effektiva.Interleaving-strategier kan till exempel ge bra resultat även om de underliggande sökarna kanske inte fungerar bra själva.

Place, publisher, year, edition, pages
2017. , p. 71
Keyword [en]
symbolic execution, bug finding, test case generation
National Category
Computer Sciences
Identifiers
URN: urn:nbn:se:kth:diva-216671OAI: oai:DiVA.org:kth-216671DiVA, id: diva2:1151605
External cooperation
Communication and Distributed Systems, RWTH Aachen University, Germany
Educational program
Master of Science - Computer Science
Supervisors
Examiners
Available from: 2017-10-25 Created: 2017-10-23 Last updated: 2018-01-13Bibliographically approved

Open Access in DiVA

fulltext(1715 kB)36 downloads
File information
File name FULLTEXT01.pdfFile size 1715 kBChecksum SHA-512
03706181c6e64ce699a4d3a196ac1d8ea0e438bc1ac49c09bd9d414f3eda9c48ded8b387d62aa57011fb88519af859a44d0e85d25069eb298fc8a8e47a3abea8
Type fulltextMimetype application/pdf

By organisation
School of Computer Science and Communication (CSC)
Computer Sciences

Search outside of DiVA

GoogleGoogle Scholar
Total: 36 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

urn-nbn

Altmetric score

urn-nbn
Total: 53 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf