@inproceedings{21aa52ee5ab143c9a799baf2d248838b,
title = "Boosting Sequential Consistency Checking Using Saturation",
abstract = "We address the problem of checking that an execution of a shared memory concurrent program is sequentially consistent (SC). This problem is NP-hard due to the necessity of finding a total order between the write operations that induces an acyclic happen-before relation. We propose an approach allowing to avoid falling systematically in the worst case, and to check SCness in polynomial-time in most cases in practice. The approach is based on a simple yet powerful saturation-based procedure for computing write constraints that must hold for SCness, allowing on one hand fast detection of SC violations, and on the other hand reducing drastically the search space for a total order witnessing SCness.",
author = "Rachid Zennou and Atig, \{Mohamed Faouzi\} and Ranadeep Biswas and Ahmed Bouajjani and Constantin Enea and Mohammed Erradi",
note = "Publisher Copyright: {\textcopyright} 2020, Springer Nature Switzerland AG.; 18th International Symposium on Automated Technology for Verification and Analysis, ATVA 2020 ; Conference date: 19-10-2020 Through 23-10-2020",
year = "2020",
month = jan,
day = "1",
doi = "10.1007/978-3-030-59152-6\_20",
language = "English",
isbn = "9783030591519",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Science and Business Media Deutschland GmbH",
pages = "360--376",
editor = "Hung, \{Dang Van\} and Oleg Sokolsky",
booktitle = "Automated Technology for Verification and Analysis - 18th International Symposium, ATVA 2020, Proceedings",
}