{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,25]],"date-time":"2025-07-25T10:29:47Z","timestamp":1753439387484,"version":"3.37.3"},"reference-count":23,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2020,10,23]],"date-time":"2020-10-23T00:00:00Z","timestamp":1603411200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,10,23]],"date-time":"2020-10-23T00:00:00Z","timestamp":1603411200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100001824","name":"Grantov\u00e1 Agentura Cesk\u00e9 Republiky","doi-asserted-by":"publisher","award":["18-02177S"],"award-info":[{"award-number":["18-02177S"]}],"id":[{"id":"10.13039\/501100001824","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Softw Syst Model"],"published-print":{"date-parts":[[2021,4]]},"DOI":"10.1007\/s10270-020-00837-y","type":"journal-article","created":{"date-parts":[[2020,10,23]],"date-time":"2020-10-23T04:02:40Z","timestamp":1603425760000},"page":"363-382","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Reproducible execution of POSIX programs with DiOS"],"prefix":"10.1007","volume":"20","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8484-1063","authenticated-orcid":false,"given":"Petr","family":"Ro\u010dkai","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zuzana","family":"Baranov\u00e1","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jan","family":"Mr\u00e1zek","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Katar\u00edna","family":"Kejstov\u00e1","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ji\u0159\u00ed\u00ed","family":"Barnat","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,10,23]]},"reference":[{"key":"837_CR1","doi-asserted-by":"crossref","unstructured":"Baranov\u00e1, Z., Barnat, J., Kejstov\u00e1, K., Ku\u010dera, T., Lauko, H., Mr\u00e1zek, J., Ro\u010dkai, P., \u0160till, V.: Model checking of C and C++ with DIVINE 4. In: ATVA 2017, Volume 10482 of LNCS, pp. 201\u2013207. Springer. https:\/\/divine.fi.muni.cz\/2017\/divine4 (2017)","DOI":"10.1007\/978-3-319-68167-2_14"},{"key":"837_CR2","doi-asserted-by":"publisher","unstructured":"Beyer, D.: Reliable and reproducible competition results with BenchExec and witnesses report on SV-COMP 2016. In: TACAS, pp. 887\u2013904. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-662-49674-9_55","DOI":"10.1007\/978-3-662-49674-9_55"},{"key":"837_CR3","unstructured":"Cadar, C., Dunbar, D., Engler, D.R.: KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. In: OSDI, pp. 209\u2013224. USENIX Association (2008)"},{"issue":"1","key":"837_CR4","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2110356.2110358","volume":"30","author":"V Chipounov","year":"2012","unstructured":"Chipounov, V., Kuznetsov, V., Candea, G.: The S2E platform: design, implementation, and applications. ACM Trans. Comput. Syst. 30(1), 1\u201349 (2012). https:\/\/doi.org\/10.1145\/2110356.2110358","journal-title":"ACM Trans. Comput. Syst."},{"key":"837_CR5","unstructured":"Chirigati, F., Shasha, D., Freire, J.: Reprozip: using provenance to support computational reproducibility. In: Theory and Practice of Provenance, pp. 1:1\u20131:4. USENIX Association, Berkeley (2013). http:\/\/dl.acm.org\/citation.cfm?id=2482949.2482951"},{"key":"837_CR6","doi-asserted-by":"publisher","unstructured":"Daum, M., Schirmer, N., Schmidt, M.: From operating-system correctness to pervasively veried applications. In: Integrated Formal Methods, vol. 10, pp. 105\u2013120 (2010). https:\/\/doi.org\/10.1007\/978-3-642-16265-7_9","DOI":"10.1007\/978-3-642-16265-7_9"},{"issue":"5","key":"837_CR7","doi-asserted-by":"publisher","first-page":"485","DOI":"10.1002\/cpe.v20:5","volume":"20","author":"J Frew","year":"2008","unstructured":"Frew, J., Metzger, D., Slaughter, P.: Automatic capture and reconstruction of computational provenance. Concurr. Comput. Pract. Exp. 20(5), 485\u2013496 (2008). https:\/\/doi.org\/10.1002\/cpe.v20:5","journal-title":"Concurr. Comput. Pract. Exp."},{"key":"837_CR8","doi-asserted-by":"crossref","unstructured":"Goel, S., Hunt, W.A., Kaufmann, M., Ghosh, S.: Simulation and formal verification of x86 machine-code programs that make system calls. In: 2014 Formal Methods in Computer-Aided Design (FMCAD), pp. 91\u201398 (2014)","DOI":"10.1109\/FMCAD.2014.6987600"},{"key":"837_CR9","doi-asserted-by":"publisher","unstructured":"Inverso, O., Nguyen, T.L., Fischer, B., Torre, S.L., Parlato, G.: Lazy-CSeq: a context-bounded model checking tool for multi-threaded C-programs. In: Automated Software Engineering, pp. 807\u2013812 (2015). https:\/\/doi.org\/10.1109\/ASE.2015.108","DOI":"10.1109\/ASE.2015.108"},{"key":"837_CR10","doi-asserted-by":"publisher","unstructured":"Joshi, S., Orso, A.: SCARPE: a technique and tool for selective capture and replay of program executions. In: International Conference on Software Maintenance, pp. 234\u2013243 (2007). ISBN 978-1-4244-1256-3, https:\/\/doi.org\/10.1109\/ICSM.2007.4362636","DOI":"10.1109\/ICSM.2007.4362636"},{"key":"837_CR11","unstructured":"Kejstov\u00e1, K.: Model Checking with System Call Traces. Master\u2019s Thesis, Masarykova univerzita, Fakulta informatiky, Brno (2019). http:\/\/is.muni.cz\/th\/tukvk\/"},{"key":"837_CR12","doi-asserted-by":"publisher","unstructured":"Kejstov\u00e1, K., Ro\u010dkai, P., Barnat, J.: From model checking to runtime verification and back. In: Runtime Verification, Volume 10548 of LNCS, pp. 225\u2013240. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-67531-2_14","DOI":"10.1007\/978-3-319-67531-2_14"},{"key":"837_CR13","doi-asserted-by":"publisher","unstructured":"Kong, S., Tillmann, N., de\u00a0Halleux, J.: Automated testing of environment-dependent programs: a case study of modeling the file system for Pex. In: International Conference on Information Technology: New Generations, pp. 758\u2013762 (2009). https:\/\/doi.org\/10.1109\/ITNG.2009.80","DOI":"10.1109\/ITNG.2009.80"},{"key":"837_CR14","unstructured":"Krekel, H., Oliveira, B., Pfannschmidt, R., Bruynooghe, F., Laugher, B., Bruhin, F.: pytest 4.5 (2004). https:\/\/github.com\/pytest-dev\/pytest"},{"key":"837_CR15","doi-asserted-by":"crossref","unstructured":"Lauko, H., \u0160till, V., Ro\u010dkai, P., Barnat, J.: Extending DIVINE with symbolic verification using SMT. In: TACAS, pp. 204\u2013208. Springer, Cham (2019)","DOI":"10.1007\/978-3-030-17502-3_14"},{"key":"837_CR16","doi-asserted-by":"publisher","first-page":"483","DOI":"10.1109\/TSE.2013.49","volume":"40","author":"W Leungwattanakit","year":"2014","unstructured":"Leungwattanakit, W., Artho, C., Hagiya, M., Tanabe, Y., Yamamoto, M., Takahashi, K.: Modular software model checking for distributed systems. IEEE Trans. Softw. Eng. 40, 483\u2013501 (2014). https:\/\/doi.org\/10.1109\/TSE.2013.49","journal-title":"IEEE Trans. Softw. Eng."},{"key":"837_CR17","unstructured":"Mackinnon, T., Freeman, S., Craig, P.: Extreme programming examined. In: Chapter Endo-Testing: Unit Testing with Mock Objects, pp. 287\u2013301. Addison-Wesley Longman Publishing Co., Inc., Boston (2001). ISBN 0-201-71040-4. http:\/\/dl.acm.org\/citation.cfm?id=377517.377534"},{"key":"837_CR18","doi-asserted-by":"publisher","unstructured":"Mostafa, S., Wang, X.: An empirical study on the usage of mocking frameworks in software testing. In: International Conference on Quality Software, pp. 127\u2013132 (2014). https:\/\/doi.org\/10.1109\/QSIC.2014.19","DOI":"10.1109\/QSIC.2014.19"},{"key":"837_CR19","unstructured":"Musuvathi, M., Qadeer, S., Ball, T., Basler, G., Nainar, P.A., Neamtiu, I.: Finding and reproducing Heisenbugs in concurrent programs. In: Symposium on Operating Systems Design and Implementation. USENIX (2008)"},{"key":"837_CR20","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.jss.2018.04.026","volume":"143","author":"P Ro\u010dkai","year":"2018","unstructured":"Ro\u010dkai, P., \u0160till, V., \u010cern\u00e1, I., Barnat, J.: DiVM: model checking with LLVM and graph memory. J. Syst. Softw. 143, 1\u201313 (2018). https:\/\/doi.org\/10.1016\/j.jss.2018.04.026","journal-title":"J. Syst. Softw."},{"key":"837_CR21","doi-asserted-by":"publisher","unstructured":"\u0160till, V., Ro\u010dkai, P., Barnat, J.: Using off-the-shelf exception support components in C++ verification. In: Software Quality, Reliability and Security, pp. 54\u201364. IEEE (2017). https:\/\/doi.org\/10.1109\/QRS.2017.15","DOI":"10.1109\/QRS.2017.15"},{"key":"837_CR22","doi-asserted-by":"publisher","unstructured":"Wachter, B., Kroening, D., Ouaknine, J.: Verifying multi-threaded software with Impact. In: Formal Methods in Computer-Aided Design, pp. 210\u2013217. IEEE (2013). https:\/\/doi.org\/10.1109\/FMCAD.2013.6679412","DOI":"10.1109\/FMCAD.2013.6679412"},{"key":"837_CR23","unstructured":"Yang, Y., Chen, X., Gopalakrishnan, G.: A Runtime Model Checker for Multithreaded C Programs. Technical Report, Inspect (2008)"}],"container-title":["Software and Systems Modeling"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-020-00837-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10270-020-00837-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-020-00837-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,10,22]],"date-time":"2021-10-22T19:22:05Z","timestamp":1634930525000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10270-020-00837-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,10,23]]},"references-count":23,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2021,4]]}},"alternative-id":["837"],"URL":"https:\/\/doi.org\/10.1007\/s10270-020-00837-y","relation":{},"ISSN":["1619-1366","1619-1374"],"issn-type":[{"type":"print","value":"1619-1366"},{"type":"electronic","value":"1619-1374"}],"subject":[],"published":{"date-parts":[[2020,10,23]]},"assertion":[{"value":"1 March 2020","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"17 July 2020","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"5 October 2020","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"23 October 2020","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}