@inproceedings{DBLP:conf/fmcad/LeonFHM18, author = {Ponce de Le{\'{o}}n, Hern{\'{a}}n and Furbach, Florian and Heljanko, Keijo and Meyer, Roland}, title = {{BMC} with Memory Models as Modules}, booktitle = {{FMCAD}}, publisher = {{IEEE}}, pages = {1--9}, year = {2018}, abstract = {This paper reports progress in verification tool engineering for weak memory models. We present two bounded model checking tools for concurrent programs. Their distinguishing feature is modularity: Besides a program, they expect as input a module describing the hardware architecture for which the program should be verified. DARTAGNAN verifies state reachability under the given memory model using a novel SMT encoding. PORTHOS checks state equivalence under two given memory models using a guided search strategy. We have performed experiments to compare our tools against other memory model-aware verifiers and find them very competitive, despite the modularity offered by our approach.}, doi = {10.23919/FMCAD.2018.8603021}, keywords = {Model-based Systems Engineering, MbSE}, }