{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:46:55Z","timestamp":1750308415960,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":42,"publisher":"ACM","license":[{"start":{"date-parts":[[2018,6,2]],"date-time":"2018-06-02T00:00:00Z","timestamp":1527897600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2018,6,2]]},"DOI":"10.1145\/3193992.3194000","type":"proceedings-article","created":{"date-parts":[[2018,7,19]],"date-time":"2018-07-19T13:05:12Z","timestamp":1532005512000},"page":"30-39","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":8,"title":["Testing meets static and runtime verification"],"prefix":"10.1145","author":[{"given":"Jes\u00fas Mauricio","family":"Chimento","sequence":"first","affiliation":[{"name":"Chalmers University of Technology, Gothenburg, Sweden"}]},{"given":"Wolfgang","family":"Ahrendt","sequence":"additional","affiliation":[{"name":"Chalmers University of Technology, Gothenburg, Sweden"}]},{"given":"Gerardo","family":"Schneider","sequence":"additional","affiliation":[{"name":"University of Gothenburg, Gothenburg, Sweden"}]}],"member":"320","published-online":{"date-parts":[[2018,6,2]]},"reference":[{"volume-title":"Quviq AB: QuickCheck Documentation v1.26.2. (June","year":"2012","key":"e_1_3_2_1_1_1","unstructured":"2012. Quviq AB: QuickCheck Documentation v1.26.2. (June 2012 ). 2012. Quviq AB: QuickCheck Documentation v1.26.2. (June 2012)."},{"volume-title":"Bank system repository. github.com\/mchimento\/Bank. (January","year":"2018","key":"e_1_3_2_1_2_1","unstructured":"2018. Bank system repository. github.com\/mchimento\/Bank. (January 2018 ). 2018. Bank system repository. github.com\/mchimento\/Bank. (January 2018)."},{"key":"e_1_3_2_1_3_1","unstructured":"2018. SeleniumHQ. http:\/\/www.seleniumhq.org\/. (2018). Accessed: 2018-01-25.  2018. SeleniumHQ. http:\/\/www.seleniumhq.org\/. (2018). Accessed: 2018-01-25."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"crossref","unstructured":"Wolfgang Ahrendt Bernhard Beckert Richard Bubel Reiner H\u00e4hnle Peter H. Schmitt and Mattias Ulbrich (Eds.). 2016. Deductive Software Verification---The KeY Book. Springer.  Wolfgang Ahrendt Bernhard Beckert Richard Bubel Reiner H\u00e4hnle Peter H. Schmitt and Mattias Ulbrich (Eds.). 2016. Deductive Software Verification---The KeY Book. Springer.","DOI":"10.1007\/978-3-319-49812-6"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-19249-9_8"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-017-0274-y"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"crossref","unstructured":"Wolfgang Ahrendt Christoph Gladisch and Mihai Herda. 2016. Proof-based Test Case Generation 415--452. In Ahrendt et al. {4}.  Wolfgang Ahrendt Christoph Gladisch and Mihai Herda. 2016. Proof-based Test Case Generation 415--452. In Ahrendt et al. {4}.","DOI":"10.1007\/978-3-319-49812-6_12"},{"key":"e_1_3_2_1_8_1","unstructured":"Micael Andersson. 2014. Test Driven Development and Automated Testin. Course given at Chalmers reporting on his experience teaching TDD to Volvo software developers. (2014).  Micael Andersson. 2014. Test Driven Development and Automated Testin. Course given at Chalmers reporting on his experience teaching TDD to Volvo software developers. (2014)."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSTW.2013.29"},{"volume-title":"Test Driven Development: A Practical Guide","author":"Astels D.","key":"e_1_3_2_1_10_1","unstructured":"D. Astels . 2003. Test Driven Development: A Practical Guide . Prentice Hall PTR. D. Astels. 2003. Test Driven Development: A Practical Guide. Prentice Hall PTR."},{"key":"e_1_3_2_1_11_1","unstructured":"Stefan Bechtold Sam Brannen Johannes Link Matthias Merdes Marc Philipp and Christian Stein. 2018. JUnit 5 User Guide (version 5.0.3).  Stefan Bechtold Sam Brannen Johannes Link Matthias Merdes Marc Philipp and Christian Stein. 2018. JUnit 5 User Guide (version 5.0.3)."},{"volume-title":"the calculus of inductive constructions","author":"Bertot Yves","key":"e_1_3_2_1_12_1","unstructured":"Yves Bertot , Pierre Cast\u00e9ran , G\u00e8rard Huet , and Christine Paulin-Mohring . 2004. Coq'Art : the calculus of inductive constructions . Springer . Yves Bertot, Pierre Cast\u00e9ran, G\u00e8rard Huet, and Christine Paulin-Mohring. 2004. Coq'Art : the calculus of inductive constructions. Springer."},{"key":"e_1_3_2_1_13_1","volume-title":"Program Slicing and Test Generation for C Program Debugging. In TAP'11","author":"Chebaro Omar","year":"2011","unstructured":"Omar Chebaro , Nikolai Kosmatov , Alain Giorgetti , and Jacques Julliand . 2011 . The SANTE Tool: Value Analysis , Program Slicing and Test Generation for C Program Debugging. In TAP'11 . 78--83. Omar Chebaro, Nikolai Kosmatov, Alain Giorgetti, and Jacques Julliand. 2011. The SANTE Tool: Value Analysis, Program Slicing and Test Generation for C Program Debugging. In TAP'11. 78--83."},{"key":"e_1_3_2_1_14_1","unstructured":"David Chelimsky. 2010. The RSpec Book. Behaviour-Driven Development with RSpec Cucumber and Friends. The Pragmatic Bookshelf.   David Chelimsky. 2010. The RSpec Book. Behaviour-Driven Development with RSpec Cucumber and Friends. The Pragmatic Bookshelf."},{"volume-title":"OpenJML: JML for Java 7 by Extending OpenJDK","author":"Cok David R.","key":"e_1_3_2_1_15_1","unstructured":"David R. Cok . 2011. OpenJML: JML for Java 7 by Extending OpenJDK . Springer . David R. Cok. 2011. OpenJML: JML for Java 7 by Extending OpenJDK. Springer."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.141.2"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03240-0_13"},{"key":"e_1_3_2_1_18_1","volume-title":"LARVA - A Tool for Runtime Monitoring of Java Programs. In SEFM'09","author":"Colombo Christian","year":"2009","unstructured":"Christian Colombo , Gordon J. Pace , and Gerardo Schneider . 2009 . LARVA - A Tool for Runtime Monitoring of Java Programs. In SEFM'09 . Christian Colombo, Gordon J. Pace, and Gerardo Schneider. 2009. LARVA - A Tool for Runtime Monitoring of Java Programs. In SEFM'09."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1062455.1062533"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21690-4_16"},{"key":"e_1_3_2_1_21_1","volume-title":"de Moura and Nikolaj Bj\u00f8rner","author":"Leonardo","year":"2008","unstructured":"Leonardo M. de Moura and Nikolaj Bj\u00f8rner . 2008 . Z3: An Efficient SMT Solver.. In TACAS (LNCS), Vol. 4963 . Springer , 337--340. Leonardo M. de Moura and Nikolaj Bj\u00f8rner. 2008. Z3: An Efficient SMT Solver.. In TACAS (LNCS), Vol. 4963. Springer, 337--340."},{"key":"e_1_3_2_1_22_1","volume-title":"Model-based Methodologies for Pervasive and Embedded Software","volume":"7706","author":"Falzon Kevin","year":"2012","unstructured":"Kevin Falzon and Gordon Pace . 2012 . Combining Testing and Runtime Verification Techniques . In Model-based Methodologies for Pervasive and Embedded Software , Vol. LNCS 7706 . Kevin Falzon and Gordon Pace. 2012. Combining Testing and Runtime Verification Techniques. In Model-based Methodologies for Pervasive and Embedded Software, Vol. LNCS 7706."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.5555\/3220907.3221159"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"crossref","unstructured":"A. Francalanza L. Aceto A. Achilleos D. P. Attard I. Cassar D. Della Monica and A. Ing\u00f3lfsd\u00f3ttir. 2017. A Foundation for Runtime Monitoring. In RV'17. 8--29.  A. Francalanza L. Aceto A. Achilleos D. P. Attard I. Cassar D. Della Monica and A. Ing\u00f3lfsd\u00f3ttir. 2017. A Foundation for Runtime Monitoring. In RV'17. 8--29.","DOI":"10.1007\/978-3-319-67531-2_2"},{"volume-title":"Computer Aided Verification (CAV'01) satellite workshop (ENTCS)","author":"Havelund Klaus","key":"e_1_3_2_1_25_1","unstructured":"Klaus Havelund and Grigore Ro\u015fu . 2001. Runtime Verification . In Computer Aided Verification (CAV'01) satellite workshop (ENTCS) , Vol. 55 . Klaus Havelund and Grigore Ro\u015fu. 2001. Runtime Verification. In Computer Aided Verification (CAV'01) satellite workshop (ENTCS), Vol. 55."},{"key":"e_1_3_2_1_26_1","unstructured":"Martin Hentschel Reiner H\u00e4hnle and Richard Bubel. 2016. Symbolic Execution 385--389. In Ahrendt et al. {4}.  Martin Hentschel Reiner H\u00e4hnle and Richard Bubel. 2016. Symbolic Execution 385--389. In Ahrendt et al. {4}."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"crossref","unstructured":"Marieke Huisman Wolfgang Ahrendt Daniel Grahl and Martin Hentschel. 2016. Formal Specification with the Java Modeling Language 193--241. In Ahrendt et al. {4}.  Marieke Huisman Wolfgang Ahrendt Daniel Grahl and Martin Hentschel. 2016. Formal Specification with the Java Modeling Language 193--241. In Ahrendt et al. {4}.","DOI":"10.1007\/978-3-319-49812-6_7"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/360248.360252"},{"volume-title":"Software Safety and Security. NATO Science for Peace and Security Series - D: Information and Communication Security","author":"Koenig Jason","key":"e_1_3_2_1_30_1","unstructured":"Jason Koenig and K. Rustan M. Leino . 2012. Getting Started with Dafny: A Guide . In Software Safety and Security. NATO Science for Peace and Security Series - D: Information and Communication Security , Vol. 33 . IOS Press , 152--181. Jason Koenig and K. Rustan M. Leino. 2012. Getting Started with Dafny: A Guide. In Software Safety and Security. NATO Science for Peace and Security Series - D: Information and Communication Security, Vol. 33. IOS Press, 152--181."},{"key":"e_1_3_2_1_31_1","unstructured":"G. T. Leavens E. Poll C. Clifton Y. Cheon C. Ruby D. Cok P. M\u00fcller J. Kiniry and P. Chalin. 2007. JML Reference Manual.  G. T. Leavens E. Poll C. Clifton Y. Cheon C. Ruby D. Cok P. M\u00fcller J. Kiniry and P. Chalin. 2007. JML Reference Manual."},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2008.08.004"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/SCAM.2014.19"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0_55"},{"volume-title":"Theories of Programming Languages","author":"Reynolds J. C.","key":"e_1_3_2_1_36_1","unstructured":"J. C. Reynolds . 2009. Theories of Programming Languages . Cambridge University Press . J. C. Reynolds. 2009. Theories of Programming Languages. Cambridge University Press."},{"volume-title":"TAP (LNCS)","author":"Tillmann Nikolai","key":"e_1_3_2_1_37_1","unstructured":"Nikolai Tillmann and Jonathan de Halleux . 2008. Pex-White Box Test Generation for .NET .. In TAP (LNCS) , Vol. 4966 . Springer , 134--153. Nikolai Tillmann and Jonathan de Halleux. 2008. Pex-White Box Test Generation for .NET.. In TAP (LNCS), Vol. 4966. Springer, 134--153."},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"crossref","unstructured":"J. Tschannen C. A. Furia M. Nordio and B. Meyer. 2011. Usable Verification of Object-Oriented Programs by Combining Static and Dynamic Techniques. In SEFM (LNCS). 382--398.   J. Tschannen C. A. Furia M. Nordio and B. Meyer. 2011. Usable Verification of Object-Oriented Programs by Combining Static and Dynamic Techniques. In SEFM (LNCS). 382--398.","DOI":"10.1007\/978-3-642-24690-6_26"},{"key":"e_1_3_2_1_39_1","unstructured":"Mark Utting and Bruno Legeard. 2007. Practical Model-Based Testing - A Tools Approach. Morgan Kaufmann. I--XIX 1--433 pages.   Mark Utting and Bruno Legeard. 2007. Practical Model-Based Testing - A Tools Approach. Morgan Kaufmann. I--XIX 1--433 pages."},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1002\/stvr.456"},{"key":"e_1_3_2_1_41_1","unstructured":"Makarius Wenzel. 2016. The Isabelle\/Isar Reference Manual.  Makarius Wenzel. 2016. The Isabelle\/Isar Reference Manual."},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/11408901_21"}],"event":{"name":"ICSE '18: 40th International Conference on Software Engineering","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering","IEEE-CS Computer Society"],"location":"Gothenburg Sweden","acronym":"ICSE '18"},"container-title":["Proceedings of the 6th Conference on Formal Methods in Software Engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3193992.3194000","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3193992.3194000","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T17:49:15Z","timestamp":1750268955000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3193992.3194000"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,6,2]]},"references-count":42,"alternative-id":["10.1145\/3193992.3194000","10.1145\/3193992"],"URL":"https:\/\/doi.org\/10.1145\/3193992.3194000","relation":{},"subject":[],"published":{"date-parts":[[2018,6,2]]},"assertion":[{"value":"2018-06-02","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}