{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,28]],"date-time":"2025-09-28T04:10:51Z","timestamp":1759032651300,"version":"3.37.3"},"reference-count":43,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2017,4,4]],"date-time":"2017-04-04T00:00:00Z","timestamp":1491264000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100004359","name":"Vetenskapsr\u00e5det","doi-asserted-by":"publisher","award":["2012-4499"],"award-info":[{"award-number":["2012-4499"]}],"id":[{"id":"10.13039\/501100004359","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000921","name":"European Cooperation in Science and Technology","doi-asserted-by":"publisher","award":["IC1402"],"award-info":[{"award-number":["IC1402"]}],"id":[{"id":"10.13039\/501100000921","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2017,8]]},"DOI":"10.1007\/s10703-017-0274-y","type":"journal-article","created":{"date-parts":[[2017,4,5]],"date-time":"2017-04-05T07:23:19Z","timestamp":1491376999000},"page":"200-265","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":27,"title":["Verifying data- and control-oriented properties combining static and runtime verification: theory and tools"],"prefix":"10.1007","volume":"51","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5671-2555","authenticated-orcid":false,"given":"Wolfgang","family":"Ahrendt","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jes\u00fas Mauricio","family":"Chimento","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gordon J.","family":"Pace","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gerardo","family":"Schneider","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,4,4]]},"reference":[{"key":"274_CR1","unstructured":"Apache Tomcat. http:\/\/tomcat.apache.org\/"},{"key":"274_CR2","doi-asserted-by":"crossref","unstructured":"Ahrendt W, Beckert B, Bubel R, H\u00e4hnle R, Schmitt PH, Ulbrich M (eds) (2016) Deductive software verification\u2014the KeY book (LNCS), vol 10001. Springer, Berlin","DOI":"10.1007\/978-3-319-49812-6"},{"key":"274_CR3","doi-asserted-by":"crossref","unstructured":"Ahrendt W, Chimento JM, Pace GJ, Schneider G (2015) A specification language for static and runtime verification of data and control properties. In: FM\u201915 (LNCS), vol 9109. Springer, Berlin","DOI":"10.1007\/978-3-319-19249-9_8"},{"key":"274_CR4","doi-asserted-by":"crossref","first-page":"1289","DOI":"10.1016\/j.scico.2010.08.003","volume":"77","author":"W Ahrendt","year":"2012","unstructured":"Ahrendt W, Dylla M (2012) A system for compositional verification of asynchronous objects. Sci Comput Program 77:1289\u20131309","journal-title":"Sci Comput Program"},{"key":"274_CR5","doi-asserted-by":"crossref","unstructured":"Ahrendt W, Pace G, Schneider G (2012) A unified approach for static and runtime verification: framework and applications. In: ISoLA\u201912 (LNCS), vol 7609. Springer, Berlin","DOI":"10.1007\/978-3-642-34026-0_24"},{"key":"274_CR6","doi-asserted-by":"crossref","unstructured":"Ahrendt W, Pace GJ, Schneider G (2016) StaRVOOrS\u2014episode II: strengthen and distribute the force. In: ISoLA\u201916 (1) (LNCS), vol 9952. Springer, Berlin","DOI":"10.1007\/978-3-319-47166-2_28"},{"issue":"2\u20133","key":"274_CR7","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1016\/j.tcs.2004.11.007","volume":"336","author":"C Artho","year":"2005","unstructured":"Artho C, Barringer H, Goldberg A, Havelund K, Khurshid S, Lowry M, Pasareanu C, Rosu G, Sen K, Visser W et al (2005) Combining test case generation and runtime verification. Theor Comput Sci 336(2\u20133):209\u2013234","journal-title":"Theor Comput Sci"},{"key":"274_CR8","unstructured":"Artho C, Biere A (2015) Combined static and dynamic analysis. In: AIOOL\u201905 (ENTCS) vol 131, pp 3\u201314"},{"key":"274_CR9","unstructured":"Barnes J (2012) SPARK: the proven approach to high integrity software. Altran Praxis. http:\/\/www.altran.co.uk"},{"key":"274_CR10","doi-asserted-by":"crossref","unstructured":"Barnett M, Rustan K, Leino M, Schulte W (2005) The Spec# programming system: an overview. In: CASSIS\u201905 (LNCS) vol 3362. Springer, Berlin, pp 49\u201369","DOI":"10.1007\/978-3-540-30569-9_3"},{"key":"274_CR11","doi-asserted-by":"crossref","unstructured":"Barringer H, Goldberg A, Havelund K, Sen K (2004) Rule-based runtime verification. In: VMCAI\u201904, pp 44\u201357","DOI":"10.1007\/978-3-540-24622-0_5"},{"key":"274_CR12","doi-asserted-by":"crossref","unstructured":"Bodden E, Hendren LJ, Lhot\u00e1k O (2007) A staged static program analysis to improve the performance of runtime monitoring. In: ECOOP\u201907 (LNCS), vol 4609","DOI":"10.1007\/978-3-540-73589-2_25"},{"key":"274_CR13","unstructured":"Bodden E, Lam P (2010) Clara: partially evaluating runtime monitors at compile time\u2014tutorial supplement. In: RV\u201910 (LNCS) vol 6418, pp 74\u201388"},{"issue":"3","key":"274_CR14","doi-asserted-by":"crossref","first-page":"212","DOI":"10.1007\/s10009-004-0167-4","volume":"7","author":"L Burdy","year":"2005","unstructured":"Burdy L, Cheon Y, Cok DR, Ernst MD, Kiniry JR, Leavens GT, Rustan K, Leino M, Poll E (2005) An overview of JML tools and applications. Int J Softw Tools Technol Transf 7(3):212\u2013232","journal-title":"Int J Softw Tools Technol Transf"},{"key":"274_CR15","doi-asserted-by":"crossref","unstructured":"Chen F, Ro\u015fu G (2005) Java-MOP: a monitoring oriented programming environment for Java. In: TACAS\u201905 (LNCS), vol 3440. Springer, Berlin, pp 546\u2013550","DOI":"10.1007\/978-3-540-31980-1_36"},{"key":"274_CR16","doi-asserted-by":"crossref","unstructured":"Chimento JM, Ahrendt W, Pace GJ, Schneider G (2015) StaRVOOrS: a tool for combined static and runtime verification of Java. In: Bartocci E, Majumdar R (eds) Runtime verification (LNCS), vol 9333. Springer, Berlin, pp 297\u2013305","DOI":"10.1007\/978-3-319-23820-3_21"},{"key":"274_CR17","doi-asserted-by":"crossref","unstructured":"Christakis M, M\u00fcller P, W\u00fcstholz V (2012) Collaborative verification and testing with explicit assumptions. In: FM\u201912: formal methods - 18th international symposium, Paris, France, August 27-31, 2012. Proceedings, pp 132\u2013146","DOI":"10.1007\/978-3-642-32759-9_13"},{"key":"274_CR18","doi-asserted-by":"crossref","unstructured":"Colombo C, Pace GJ, Schneider G (2009) Dynamic event-based runtime monitoring of real-time and contextual properties. In: FMICS\u201908 (LNCS), vol 5596. Springer, Berlin, pp 135\u2013149","DOI":"10.1007\/978-3-642-03240-0_13"},{"key":"274_CR19","unstructured":"Colombo C, Pace GJ, Schneider G (2009) LARVA: a tool for runtime monitoring of Java programs. In: SEFM\u201909, IEEE Computer Society, pp 33\u201337"},{"key":"274_CR20","doi-asserted-by":"crossref","unstructured":"Csallner C, Smaragdakis Y(2005) Check \u2019n\u2019 crash: combining static checking and testing. In: 27th International Conference on Software Engineering (ICSE 2005), 15-21 May 2005, St. Louis, Missouri, USA, pp 422\u2013431","DOI":"10.1145\/1062455.1062533"},{"key":"274_CR21","unstructured":"de Boer FS, de Gouw S, Johnsen EB, Wong PYH (2013) Run-time checking of data- and protocol-oriented properties of Java programs: an industrial case study. In: Shin Sung Y, Maldonado Jos C (eds) SAC. ACM, pp 1573\u20131578"},{"key":"274_CR22","doi-asserted-by":"crossref","unstructured":"Decker N, Leucker M, Thoma D (2013) jUnitRV\u2014adding runtime verification to JUnit. In: NASA formal methods (LNCS), vol 7871. Springer, Berlin","DOI":"10.1007\/978-3-642-38088-4_34"},{"issue":"6","key":"274_CR23","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1007\/s10009-014-0308-3","volume":"17","author":"G Ernst","year":"2015","unstructured":"Ernst G, Pf\u00e4hler J, Schellhorn G, Haneberg D, Reif W (2015) KIV: overview and verifythis competition. Int J Softw Tools Technol Transf 17(6):677\u2013694","journal-title":"Int J Softw Tools Technol Transf"},{"key":"274_CR24","unstructured":"Falzon K, Pace G (2012) Combining testing and runtime verification techniques. In Model-based methodologies for pervasive and embedded software, 8th international workshop, MOMPES 2012, Essen, Germany, September 4, 2012, pp 38\u201357"},{"key":"274_CR25","doi-asserted-by":"crossref","unstructured":"Flanagan Cormac, Leino K Rustan M, Lillibridge Mark, Nelson Greg, Saxe James B, Stata Raymie (2002) Extended Static Checking for Java. In Knoop Jens, Hendren Laurie J , editors, PLDI\u201902, pages 234\u2013245. ACM","DOI":"10.1145\/512557.512558"},{"key":"274_CR26","doi-asserted-by":"crossref","unstructured":"Ge X, Taneja K, Xie T, Tillmann N (2011) DyTa: dynamic symbolic execution guided with static verification results. In: Proceedings of the 33rd international conference on software engineering, ICSE 2011, Waikiki, Honolulu , HI, USA, May 21\u201328, 2011, pp 992\u2013994","DOI":"10.1145\/1985793.1985971"},{"key":"274_CR27","volume-title":"The science of programming","author":"D Gries","year":"1987","unstructured":"Gries D (1987) The science of programming, 1st edn. Springer, Berlin","edition":"1"},{"key":"274_CR28","doi-asserted-by":"crossref","unstructured":"Jacobs B, Smans J, Philippaerts P, Vogels F, Penninckx W, Piessens F (2011) Verifast: a powerful, sound, predictable, fast verifier for C and Java. In: NASA formal methods (LNCS), vol 6617. Springer, pp 41\u201355","DOI":"10.1007\/978-3-642-20398-5_4"},{"key":"274_CR29","unstructured":"Leavens GT, Poll E, Clifton C, Cheon Y, Ruby C, Cok D, M\u00fcller P, Kiniry J, Chalin P (2007) JML reference manual. Draft 1.200"},{"key":"274_CR30","doi-asserted-by":"crossref","unstructured":"Leino K Rustan M (2010) Dafny: an automatic program verifier for functional correctness. In: Clarke EM, Voronkov A (eds) Logic for programming, artificial intelligence, and reasoning (LPAR-16) (LNCS), vol 6355. Springer, Berlin","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"274_CR31","doi-asserted-by":"crossref","unstructured":"Maraninchi F, R\u00e9mond Y (2000) Running-modes of real-time systems: a case-study with mode-automata. In: Proceedings of 12th euromicro conference on real-time systems (ECRTS 2000), 19\u201321 June 2000, Stockholm, Sweden, pp 257\u2013264","DOI":"10.1109\/EMRTS.2000.854014"},{"key":"274_CR32","unstructured":"MasterCard International Inc. Mondex web page. http:\/\/www.mondexusa.com\/"},{"key":"274_CR33","doi-asserted-by":"crossref","unstructured":"Reger G (2016) An overview of MarQ. In: Proceedings of runtime verification\u201416th international conference, RV 2016 (LNCS), vol 10012. Springer","DOI":"10.1007\/978-3-319-46982-9_34"},{"issue":"10","key":"274_CR34","doi-asserted-by":"crossref","first-page":"1359","DOI":"10.1002\/spe.2287","volume":"45","author":"H S\u00f6zer","year":"2015","unstructured":"S\u00f6zer H (2015) Integrated static code analysis and runtime verification. Softw Pract Exp 45(10):1359\u20131373","journal-title":"Softw Pract Exp"},{"key":"274_CR35","volume-title":"The Z notation: a reference manual","author":"JM Spivey","year":"1989","unstructured":"Spivey JM (1989) The Z notation: a reference manual. Prentice-Hall Inc, Upper Saddle River"},{"key":"274_CR36","unstructured":"SoftSlate Commerce. www.softslate.com\/"},{"key":"274_CR37","unstructured":"Stepney S, Cooper D, Woodcock J (2000) An electronic purse: specification, refinement and proof. Technical monograph PRG-126, Oxford University Computing Laboratory"},{"key":"274_CR38","unstructured":"StaRVOOrS web page. http:\/\/cse-212294.cse.chalmers.se\/starvoors\/"},{"key":"274_CR39","doi-asserted-by":"crossref","unstructured":"Tillmann N, Halleux Jonathan de (2008) Pex-white box test generation for .nET. In: Beckert B, H\u00e4hnle R (eds) Tests and proofs (LNCS), vol 4966. Springer, Berlin, pp 134\u2013153","DOI":"10.1007\/978-3-540-79124-9_10"},{"key":"274_CR40","unstructured":"Tonin I (2007) Verifying the mondex case study. The KeY approach. Technical Report 2007-4, Universit\u00e4t Karlsruhe"},{"key":"274_CR41","doi-asserted-by":"crossref","unstructured":"Wonisch D, Schremmer A, Wehrheim H (2013) Zero overhead runtime monitoring. In: SEFM\u201913 (LNCS), vol 8137. Springer, Berlin, pp 244\u2013258","DOI":"10.1007\/978-3-642-40561-7_17"},{"key":"274_CR42","doi-asserted-by":"crossref","unstructured":"Woodcock J (2006) First steps in the verified software grand challenge. In: SEW\u201906. IEEE Computer Society, pp 203\u2013206","DOI":"10.1109\/SEW.2006.17"},{"key":"274_CR43","doi-asserted-by":"crossref","unstructured":"Zee K, Kuncak V, Taylor M, Rinard MC (2007) Runtime checking for program verification. In: RV\u201907 (LNCS), vol 4839. Springer, Berlin, pp 202\u2013213","DOI":"10.1007\/978-3-540-77395-5_17"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-017-0274-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-017-0274-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-017-0274-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,20]],"date-time":"2019-09-20T12:52:51Z","timestamp":1568983971000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-017-0274-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,4,4]]},"references-count":43,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2017,8]]}},"alternative-id":["274"],"URL":"https:\/\/doi.org\/10.1007\/s10703-017-0274-y","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2017,4,4]]}}}