Parameterized model checking on the TSO weak memory model

DOI10.1007/S10817-020-09565-WzbMATH Open1468.68123OpenAlexW3037684714MaRDI QIDQ2208293FDOQ2208293

Authors: Sylvain Conchon, David Declerck, Fatiha Zaidi 

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

Recommendations

• Cubicle-\(\mathcal{W}\): parameterized model checking on weak memory
• The benefits of duality in verifying concurrent programs under TSO
• On the verification problem for weak memory models
• A load-buffer semantics for total store ordering
• Verification of Concurrent Programs on Weak Memory Models

zbMATH Keywords

SMTpartial order reductionweak memoryMCMTparameterized model checking

Mathematics Subject Classification ID

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

Cites Work

• Cubicle-\(\mathcal{W}\): parameterized model checking on weak memory
• Reasoning about systems with many processes
• Reasoning about networks with many identical finite state processes
• How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs
• Backward reachability of array-based systems by SMT solving: termination and invariant synthesis
• MCMT: a model checker modulo theories
• Software verification for weak memory via program transformation
• Parameterized Verification of Infinite-State Processes with Global Conditions
• 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
• Checking and enforcing robustness against TSO
• Regular Model Checking Without Transducers (On Efficient Verification of Parameterized Systems)
• Title not available (Why is that?)
• The benefits of duality in verifying concurrent programs under TSO

Cited In (5)

• Declarative parameterized verification of distributed protocols via the Cubicle model checker
• Sound verification procedures for temporal properties of infinite-state systems
• Parameterized verification under TSO with data types
• Cubicle-\(\mathcal{W}\): parameterized model checking on weak memory
• The benefits of duality in verifying concurrent programs under TSO

Uses Software

• Memorax
• Mcmt
• Cubicle

This page was built for publication: Parameterized model checking on the TSO weak memory model

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2208293)