Parameterized model checking on the TSO weak memory model

DOI10.1007/S10817-020-09565-WMaRDI QIDQ2208293zbMATH OpenOpenAlexFDO

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

zbMATH Keywords

SMTpartial order reductionweak memoryMCMTparameterized model checking

Mathematics Subject Classification ID

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

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

Cites work

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

Describes a project that uses

Uses Software

• Cubicle
• Mcmt
• Memorax

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)