search query: @keyword automated testing / total: 16
reference: 3 / 16
« previous | next »
Author:Saarikivi, Olli
Title:Test-guided proofs for C programs on LLVM
Testiohjatut todistukset C-ohjelmille LLVM-järjestelmässä
Publication type:Master's thesis
Publication year:2013
Pages:61      Language:   eng
Department/School:Perustieteiden korkeakoulu
Main subject:Tietojenkäsittelyteoria   (T-79)
Supervisor:Heljanko, Keijo
Instructor:Kähkönen, Kari
OEVS:
Electronic archive copy is available via Aalto Thesis Database.
Instructions

Reading digital theses in the closed network of the Aalto University Harald Herlin Learning Centre

In the closed network of Learning Centre you can read digital and digitized theses not available in the open network.

The Learning Centre contact details and opening hours: https://learningcentre.aalto.fi/en/harald-herlin-learning-centre/

You can read theses on the Learning Centre customer computers, which are available on all floors.

Logging on to the customer computers

  • Aalto University staff members log on to the customer computer using the Aalto username and password.
  • Other customers log on using a shared username and password.

Opening a thesis

  • On the desktop of the customer computers, you will find an icon titled:

    Aalto Thesis Database

  • Click on the icon to search for and open the thesis you are looking for from Aaltodoc database. You can find the thesis file by clicking the link on the OEV or OEVS field.

Reading the thesis

  • You can either print the thesis or read it on the customer computer screen.
  • You cannot save the thesis file on a flash drive or email it.
  • You cannot copy text or images from the file.
  • You cannot edit the file.

Printing the thesis

  • You can print the thesis for your personal study or research use.
  • Aalto University students and staff members may print black-and-white prints on the PrintingPoint devices when using the computer with personal Aalto username and password. Color printing is possible using the printer u90203-psc3, which is located near the customer service. Color printing is subject to a charge to Aalto University students and staff members.
  • Other customers can use the printer u90203-psc3. All printing is subject to a charge to non-University members.
Location:P1 Ark Aalto     | Archive
Keywords:automated testing
verification
dynamic symbolic execution
abstraction refinement
automaattinen testaus
verifiointi
dynaaminen symbolinen suoritus
abstraktion hienontaminen
Abstract (eng): Software defects can be very expensive, especially when encountered in economically critical or safety critical systems.
Many of these defects can be avoided if it can be ensured that a program meets its specification.
When the specification is given formally, for example with assertions embedded in the source code, automated software verification methods can be applied to determine whether a program complies with its specification.

Recently there has been much interest in combining under approximation and over approximation based approaches to software verification.
Such a technique is employed by the DASH algorithm originally developed at Microsoft, which generates tests to improve an under approximation of the program under test.
Simultaneously, an over approximating abstraction of the program is refined with information gathered from test generation.

We present an open source implementation of the DASH algorithm for the verification of C programs compiled on the LLVM compiler framework.
Our implementation is an extension of the dynamic symbolic execution tool LCT.
We also present a detailed method for constructing the weakest precondition based refinement operator employed by DASH for instructions of the LLVM internal representation.

To maintain a mapping between concrete executions and the abstraction DASH needs to evaluate predicates on the concrete states visited during test executions.
A straightforward implementation might store the complete concrete states of each executed test or might employ expensive re-executions to recover the concrete states.
We present a technique which allows only the concrete values of pointer variables to be stored while still requiring no re-executions.

Finally we present a case study to show the viability of our tool.
We also document a more powerful abstraction refinement method used in DASH and evaluate its effect.
Abstract (fin): Ohjelmistovirheet voivat olla hyvin kalliita, varsinkin turvallisuus- ja talouskriittisissä järjestelmissä.
Monet näistä virheistä voidaan välttää jos voidaan varmistaa että ohjelmistot täyttävät niille annetut spesifikaatiot.
Kun spesifikaatio on annettu formaalisti, esimerkiksi lähdekoodiin kirjoitetuilla assertioilla, voidaan automaattisilla ohjelmiston verifiointimenetelmillä tarkastaa että ohjelmisto täyttää sen spesifikaation.

Viime aikoina on ollut paljon kiinnostusta yhdistää yli- ja aliapproksimoivia lähestymistapoja ohjelmistojen verifiointiin.
DASH algoritmi toteuttaa tällaisen menetelmän.
Se generoi testejä parantaakseen aliapproksimaatiota verifioitavasta ohjelmasta.
Samanaikaisesti DASH hienontaa ohjelmaa yliapproksimoivaa abstraktiota testien generoinnista kerätyllä informaatiolla.

Esittelemme avoimen lähdekoodin työkalun, joka toteuttaa DASH algoritmin LLVM kääntäjäkirjastolla käännettyjen C ohjelmien verifiointiin.
Toteutuksemme perustuu dynaamisen symbolisen suorituksen työkaluun LCT:hen.
Annamme myös yksityiskohtaisen menetelmän tuottaa DASH:n vaatima heikoimpiin esiehtoihin perustuva abstraktion hienonnusoperaattori LLVM:n välikielen käskyille.

DASH evaluoi predikaatteja testien aikana nähdyille konkreettisille tiloille ylläpitääkseen kuvausta testiajojen ja abstraktion välillä.
Suoraviivainen toteutus saattaisi tallentaa jokaisen ajetun testin kokonaiset konkreettiset tilat tai ajaa testejä toistamiseen konkreettisten tilojen uudelleenkonstruoimiseksi.
Esittelemme menetelmän jolla ainoastaan osoittimia sisältävien muuttujien arvot tallennetaan ilman että testejä pitää uudelleenajaa.

Lopuksi näytämme työkalumme käyttökelpoisuuden kokeiden avulla.
Dokumentoimme myös DASH algoritmissa käytetyn tehokkaamman abstraktion hienonnusoperaattorin sekä esittelemme sen vaikutuksen kokeellisesti.
ED:2013-08-06
INSSI record number: 47021
+ add basket
« previous | next »
INSSI