Parameterized model checking on the TSO weak memory model

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

zbMATH Keywords

SMTpartial order reductionweak memoryMCMTparameterized model checking

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (1)

Sound verification procedures for temporal properties of infinite-state systems

Uses Software

• Memorax
• Mcmt
• Cubicle

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