Parameterized Verification under TSO with Data Types
Parosh Aziz Abdulla, Mohamad Faouzi Atig, Florian Furbach, Adwait Godbole, Yacoub Hendi, Shankara Narayanan Krishna, Stephan Spengler · Lecture notes in computer science · 2023
Abstract We consider parameterized verification of systems executing according to the total store ordering (TSO) semantics. The processes manipulate abstract data types over potentially infinite domains. We present a framework that translates the reachability problem for such systems to the reachability problem for register machines enriched with the given abstract data type.