Efficient testing of concurrent programs with abstraction-guided symbolic execution

Simple item page
dc.contributor.authorRungta N.
dc.contributor.authorMercer E.G.
dc.contributor.authorVisser W.
dc.date.accessioned2011-05-15T16:02:05Z
dc.date.available2011-05-15T16:02:05Z
dc.date.issued2009
dc.description.abstractIn this work we present an abstraction-guided symbolic execution technique that quickly detects errors in concurrent programs. The input to the technique is a set of target locations that represent a possible error in the program. We generate an abstract system from a backward slice for each target location. The backward slice contains program locations relevant in testing the reachability of the target locations. The backward slice only considers sequential execution and does not capture any inter-thread dependencies. A combination of heuristics are to guide a symbolic execution along locations in the abstract system in an effort to generate a corresponding feasible execution trace to the target locations. When the symbolic execution is unable to make progress, we refine the abstraction by adding locations to handle inter-thread dependencies. We demonstrate empirically that abstraction-guided symbolic execution generates feasible execution paths in the actual system to find concurrency errors in a few seconds where exhaustive symbolic execution fails to find the same errors in an hour. © 2009 Springer Berlin Heidelberg.
dc.description.versionConference Paper
dc.identifier.citationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
dc.identifier.citation5578 LNCS
dc.identifier.issn3029743
dc.identifier.other10.1007/978-3-642-02652-2_16
dc.identifier.urihttp://hdl.handle.net/10019.1/12303
dc.subjectAbstract systems
dc.subjectActual system
dc.subjectConcurrency errors
dc.subjectConcurrent program
dc.subjectExecution paths
dc.subjectExecution trace
dc.subjectReachability
dc.subjectSequential execution
dc.subjectSymbolic execution
dc.subjectTarget location
dc.subjectAbstracting
dc.subjectComputer software
dc.subjectErrors
dc.subjectLocation
dc.subjectSpin dynamics
dc.subjectTargets
dc.subjectModel checking
dc.titleEfficient testing of concurrent programs with abstraction-guided symbolic execution
dc.typeConference Paper
Files
Collections
Stellenbosch University - Scopus Publications