Model checking parameterized by the semantics in Maude

DOI10.1007/978-3-319-90686-7_13MaRDI QIDQ1648886zbMATH OpenOpenAlexFDO

Authors Adrián Riesco

Publication date 9 July 2018

Full work available at URL https://doi.org/10.1007/978-3-319-90686-7_13

zbMATH Keywords

Maudemessage passingmodel checkingsemanticsshared memory

Mathematics Subject Classification ID

Theory of programming languages (68N15) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• The Maude LTL model checker
• scientific article; zbMATH DE number 1982209
• scientific article; zbMATH DE number 910719
• Can we efficiently check concurrent programs under relaxed memory models in Maude?
• scientific article; zbMATH DE number 1543047

Cited in

(4)

• Proving VLRL action properties with the Maude model checker
• Moving Arrows and Four Model Checking Results
• Model Checking Value-Passing Modal Specifications
• Strategies, Model Checking and Branching-Time Properties in Maude

This page was built for publication: Model checking parameterized by the semantics in Maude

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