UMM: an operational memory model specification framework with integrated model checking capability

2005 ◽  
Vol 17 (5-6) ◽  
pp. 465-487 ◽  
Author(s):  
Yue Yang ◽  
Ganesh Gopalakrishnan ◽  
Gary Lindstrom
Keyword(s):  
Model Checking ◽  
Integrated Model ◽  
Model Specification ◽  
Memory Model ◽  
Operational Memory

scholarly journals An Integrated Model Checking Toolset for Kernel P Systems

2015 ◽  
pp. 153-170 ◽  
Author(s):  
Marian Gheorghe ◽  
Savas Konur ◽  
Florentin Ipate ◽  
Laurentiu Mierla ◽  
Mehmet E. Bakir ◽  
...  
Keyword(s):  
Model Checking ◽  
Integrated Model ◽  
P Systems

scholarly journals Improvement of a Library for Model Checking under Weakly Ordered Memory Model with SPIN

2018 ◽  
Vol 26 (0) ◽  
pp. 314-326
Author(s):  
Kosuke Matsumoto ◽  
Tomoharu Ugawa ◽  
Tatsuya Abe
Keyword(s):  
Model Checking ◽  
Memory Model

scholarly journals Dartagnan: Bounded Model Checking for Weak Memory Models (Competition Contribution)

2020 ◽  
pp. 378-382
Author(s):  
Hernán Ponce-de-León ◽  
Florian Furbach ◽  
Keijo Heljanko ◽  
Roland Meyer
Keyword(s):  
Model Checking ◽  
Bounded Model Checking ◽  
Memory Models ◽  
Memory Model ◽  
Complete Analysis ◽  
Concurrent Programs ◽  
Sequential Consistency ◽  
Model Checker ◽  
Safety Properties ◽  
C Programs

Abstract Dartagnanis a bounded model checker for concurrent programs under weak memory models. What makes it different from other tools is that the memory model is not hard-coded inside Dartagnanbut taken as part of the input. For SV-COMP’20, we take as input sequential consistency (i.e. the standard interleaving memory model) extended by support for atomic blocks. Our point is to demonstrate that a universal tool can be competitive and perform well in SV-COMP. Being a bounded model checker, Dartagnan’s focus is on disproving safety properties by finding counterexample executions. For programs with bounded loops, Dartagnanperforms an iterative unwinding that results in a complete analysis. The SV-COMP’20 version of Dartagnanworks on Boogiecode. The C programs of the competition are translated internally to Boogieusing SMACK.

Parameterized Model Checking on the TSO Weak Memory Model

2020 ◽  
Vol 64 (7) ◽  
pp. 1307-1330
Author(s):  
Sylvain Conchon ◽  
David Declerck ◽  
Fatiha Zaïdi
Keyword(s):  
Model Checking ◽  
Memory Model ◽  
Parameterized Model

JRF-E: using model checking to give advice on eliminating memory model-related bugs

2012 ◽  
Vol 19 (4) ◽  
pp. 491-530 ◽  
Author(s):  
Kyung Hee Kim ◽  
Tuba Yavuz-Kahveci ◽  
Beverly A. Sanders
Keyword(s):  
Model Checking ◽  
Memory Model
Sign in / Sign up

Export Citation Format

Share Document