To the top

Page Manager: Webmaster
Last update: 9/11/2012 3:13 PM

Tell a friend about this page
Print version

Can we efficiently check … - University of Gothenburg, Sweden Till startsida
To content Read more about how we use cookies on

Can we efficiently check concurrent programs under relaxed memory models in Maude?

Journal article
Authors Yehia Abd Alrahman
Marina Andric
Alessandro Beggiato
Alberto Lluch Lafuente
Published in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume 8663
Pages 21-41
ISSN 03029743
Publication year 2014
Published at Department of Computer Science and Engineering, Computing Science (GU)
Pages 21-41
Language en
Subject categories Theoretical computer science


© Springer International Publishing Switzerland 2014. Relaxed memory models offer suitable abstractions of the actual optimizations offered by multi-core architectures and by compilers of concurrent programming languages. Using such abstractions for verification purposes is challenging in part due to their inherent non-determinism which contributes to the state space explosion. Several techniques have been proposed to mitigate those problems so to make verification under relaxed memory models feasible. We discuss how to adopt some of those techniques in a Maude-based approach to language prototyping, and suggest the use of other techniques that have been shown successful for similar verification purposes.

Page Manager: Webmaster|Last update: 9/11/2012

The University of Gothenburg uses cookies to provide you with the best possible user experience. By continuing on this website, you approve of our use of cookies.  What are cookies?