D 2012

Abstracting Path Conditions

STREJČEK, Jan a Marek TRTÍK

Základní údaje

Originální název

Abstracting Path Conditions

Autoři

STREJČEK, Jan (203 Česká republika, garant, domácí) a Marek TRTÍK (203 Česká republika, domácí)

Vydání

New York, NY, USA, Proceedings of the 2012 International Symposium on Software Testing and Analysis, ISSTA 2012, od s. 155-165, 11 s. 2012

Nakladatel

ACM

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Česká republika

Utajení

není předmětem státního či obchodního tajemství

Forma vydání

tištěná verze "print"

Odkazy

Kód RIV

RIV/00216224:14330/12:00057592

Organizační jednotka

Fakulta informatiky

ISBN

978-1-4503-1454-1

DOI

Klíčová slova anglicky

Symbolic execution; Path conditions; Program location reachability; Tests generation

Příznaky

Mezinárodní význam, Recenzováno
Změněno: 7. 1. 2016 22:12, prof. RNDr. Jan Strejček, Ph.D.

Anotace

ORIG CZ

V originále

We present a symbolic-execution-based algorithm that for a given program and a given program location in it produces a nontrivial necessary condition on input values to drive the program execution to the given location. The algorithm is based on computation of loop summaries for loops along acyclic paths leading to the target location. We also propose an application of necessary conditions in contemporary bug-finding and test-generation tools. Experimental results on several small benchmarks show that the presented technique can in some cases significantly improve performance of the tools.

Česky

Představujeme algoritmus založený na symbolické exekuci, který pro daný program a daný bod v programu vytvoří netriviální nutnou podmínku na vstupní hodnoty programu, aby běh programu nad těmito hodnotami navštívil daný bod. Hlavní myšlenkou algoritmu je výpočet sumární informace pro cykly přiléhající k acyklickým cestám vedoucím do daného bodu. Dále navrhujeme využití nutných podmínek v současných nástrojích pro hledání chyb či generování testů. Experimentální výsledky na několika malých příkladech ukazují, že představená technika současné může v některých případech podstatně zlepšit výkonnost zmíněných nástrojů.

Návaznosti

GBP202/12/G061, projekt VaV
Název: Centrum excelence - Institut teoretické informatiky (CE-ITI) (Akronym: CE-ITI)
Investor: Grantová agentura ČR, Centrum excelence - Institut teoretické informatiky
MUNI/A/0758/2011, interní kód MU
Název: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity (Akronym: SKOMU)
Investor: Masarykova univerzita, Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity, DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty
MUNI/A/0914/2009, interní kód MU
Název: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace (Akronym: SV-FI MAV)
Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace, DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty