@inproceedings{atig2012detecting,
author = {Atig, Mohamed Faouzi and Bouajjani, Ahmed and Emmi, Michael and Lal, Akash},
title = {Detecting Fair Non-Termination in Multithreaded Programs},
booktitle = {Computer-Aided Verification (CAV)},
year = {2012},
month = {July},
abstract = {We develop compositional analysis algorithms for discovering fair non-terminating executions in multithreaded programs. In particular, our analysis finds fair and ultimately-periodic executions—i.e., those that ultimately repeat the same sequence of actions indefinitely with each enabled thread participating. Further, we limit the number of context-switches each thread is allowed along any repeating sequence of actions; one expects that this number is usually small for bugs in practice. Bounding context-switches leads to a compositional analysis in which each thread is considered separately, in isolation. We implement our analysis by a systematic code-to-code translation from multithreaded programs to sequential programs, such that one requires a safety analysis of the latter to find liveness bugs in the former. Then by using standard sequential analysis tools, we are able to discover fair non-terminating executions in multithreaded programs.},
url = {http://approjects.co.za/?big=en-us/research/publication/detecting-fair-non-termination-in-multithreaded-programs/},
edition = {Computer-Aided Verification (CAV)},
}