Parameterized model checking on the TSO weak memory model
From MaRDI portal
Publication:2208293
DOI10.1007/s10817-020-09565-wzbMath1468.68123OpenAlexW3037684714MaRDI QIDQ2208293
Fatiha Zaïdi, David Declerck, Sylvain Conchon
Publication date: 2 November 2020
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-020-09565-w
Related Items (1)
Uses Software
Cites Work
- Unnamed Item
- Fundamental approaches to software engineering. 18th international conference, FASE 2015, held as part of the European joint conferences on theory and practice of software, ETAPS 2015, London, UK, April 11--18, 2015. Proceedings
- Reasoning about networks with many identical finite state processes
- Cubicle-\(\mathcal{W}\): parameterized model checking on weak memory
- Backward Reachability of Array-based Systems by SMT solving: Termination and Invariant Synthesis
- How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs
- Reasoning about systems with many processes
- The Benefits of Duality in Verifying Concurrent Programs under TSO
- Software Verification for Weak Memory via Program Transformation
- Checking and Enforcing Robustness against TSO
- Parameterized Verification of Infinite-State Processes with Global Conditions
- MCMT: A Model Checker Modulo Theories
- Regular Model Checking Without Transducers (On Efficient Verification of Parameterized Systems)
This page was built for publication: Parameterized model checking on the TSO weak memory model
