{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T22:31:41Z","timestamp":1767997901739,"version":"3.49.0"},"publisher-location":"Cham","reference-count":29,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030010898","type":"print"},{"value":"9783030010904","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-030-01090-4_6","type":"book-chapter","created":{"date-parts":[[2018,9,29]],"date-time":"2018-09-29T11:23:23Z","timestamp":1538220203000},"page":"91-108","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Robustness Testing of Intermediate Verifiers"],"prefix":"10.1007","author":[{"given":"YuTing","family":"Chen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Carlo A.","family":"Furia","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,9,30]]},"reference":[{"key":"6_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/978-3-319-33693-0_6","volume-title":"Integrated Formal Methods","author":"M Ameri","year":"2016","unstructured":"Ameri, M., Furia, C.A.: Why just Boogie? In: \u00c1brah\u00e1m, E., Huisman, M. (eds.) IFM 2016. LNCS, vol. 9681, pp. 79\u201395. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-33693-0_6"},{"key":"6_CR2","unstructured":"AutoProof verified code repository. http:\/\/tiny.cc\/autoproof-repo"},{"issue":"5","key":"6_CR3","doi-asserted-by":"publisher","first-page":"507","DOI":"10.1109\/TSE.2014.2372785","volume":"41","author":"ET Barr","year":"2015","unstructured":"Barr, E.T., Harman, M., McMinn, P., Shahbaz, M., Yoo, S.: The oracle problem in software testing: a survey. IEEE Trans. Softw. Eng. 41(5), 507\u2013525 (2015)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"6_CR4","unstructured":"Chen, T.Y., Cheung, S.C., Yiu, S.M.: Metamorphic testing: a new approach for generating next test cases. Technical Report HKUST-CS98-01, Department of Computer Science, Hong Kong University of Science and Technology (1998)"},{"key":"6_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1007\/978-3-319-66845-1_19","volume-title":"Integrated Formal Methods","author":"YT Chen","year":"2017","unstructured":"Chen, Y.T., Furia, C.A.: Triggerless happy. In: Polikarpova, N., Schneider, S. (eds.) IFM 2017. LNCS, vol. 10510, pp. 295\u2013311. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66845-1_19"},{"key":"6_CR6","doi-asserted-by":"crossref","unstructured":"Chen, Y.T., Furia, C.A.: Robustness testing of intermediate verifiers. http:\/\/arxiv.org\/abs\/1805.03296 (2018)","DOI":"10.1007\/978-3-030-01090-4_6"},{"key":"6_CR7","doi-asserted-by":"crossref","unstructured":"Claessen, K., Hughes, J.: Quickcheck: a lightweight tool for random testing of Haskell programs. In: ICFP, pp. 268\u2013279. ACM (2000)","DOI":"10.1145\/357766.351266"},{"key":"6_CR8","unstructured":"Dafny examples and tests. https:\/\/github.com\/Microsoft\/dafny\/tree\/master\/Test"},{"key":"6_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/978-3-642-37036-6_8","volume-title":"Programming Languages and Systems","author":"J-C Filli\u00e2tre","year":"2013","unstructured":"Filli\u00e2tre, J.-C., Paskevich, A.: Why3\u2014where programs meet provers. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 125\u2013128. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-37036-6_8"},{"issue":"3","key":"6_CR10","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2506375","volume":"46","author":"Carlo A. Furia","year":"2014","unstructured":"Furia, C.A., Meyer, B., Velder, S.: Loop invariants: analysis, classification, and examples. ACM Comput. Surv. 46(3) (2014)","journal-title":"ACM Computing Surveys"},{"issue":"6","key":"6_CR11","doi-asserted-by":"publisher","first-page":"697","DOI":"10.1007\/s10009-016-0419-0","volume":"19","author":"CA Furia","year":"2016","unstructured":"Furia, C.A., Nordio, M., Polikarpova, N., Tschannen, J.: AutoProof: auto-active functional verification of object-oriented programs. STTT 19(6), 697\u2013716 (2016)","journal-title":"STTT"},{"issue":"3","key":"6_CR12","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1145\/2093548.2093564","volume":"55","author":"P Godefroid","year":"2012","unstructured":"Godefroid, P., Levin, M.Y., Molnar, D.A.: SAGE: whitebox fuzzing for security testing. Commun. ACM 55(3), 40\u201344 (2012)","journal-title":"Commun. ACM"},{"key":"6_CR13","doi-asserted-by":"crossref","unstructured":"Hawblitzel, C., Howell, J., Kapritsos, M., Lorch, J.R., Parno, B., Roberts, M.L., Setty, S.T.V., Zill, B.: IronFleet: proving practical distributed systems correct. In: SOSP, pp. 1\u201317. ACM (2015)","DOI":"10.1145\/2815400.2815428"},{"key":"6_CR14","unstructured":"Hawblitzel, C., Howell, J., Lorch, J.R., Narayan, A., Parno, B., Zhang, D., Zill, B.: Ironclad Apps: end-to-end security via automated full-system verification. In: USENIX OSDI, pp. 165\u2013181. USENIX Association (2014)"},{"issue":"2","key":"6_CR15","doi-asserted-by":"publisher","first-page":"9:1","DOI":"10.1145\/1459352.1459354","volume":"41","author":"RM Hierons","year":"2009","unstructured":"Hierons, R.M., et al.: Using formal specifications to support testing. ACM Comput. Surv. 41(2), 9:1\u20139:76 (2009)","journal-title":"ACM Comput. Surv."},{"issue":"5","key":"6_CR16","doi-asserted-by":"publisher","first-page":"649","DOI":"10.1109\/TSE.2010.62","volume":"37","author":"Y Jia","year":"2011","unstructured":"Jia, Y., Harman, M.: An analysis and survey of the development of mutation testing. IEEE Trans. Softw. Eng. 37(5), 649\u2013678 (2011)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"6_CR17","unstructured":"Leino, K.R.M.: This is Boogie 2 (2008). http:\/\/goo.gl\/QsH6g"},{"key":"6_CR18","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/978-3-642-17511-4_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"K. Rustan M. Leino","year":"2010","unstructured":"Leino, K., Rustan, M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, pp. 348\u2013370. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-17511-4_20"},{"key":"6_CR19","doi-asserted-by":"crossref","first-page":"361","DOI":"10.1007\/978-3-319-41528-4_20","volume-title":"Computer Aided Verification","author":"K. R. M. Leino","year":"2016","unstructured":"Leino, K.R.M., Pit-Claudel, C.: Trigger selection strategies to stabilize program verifiers. In: CAV, pp. 361\u2013381. Springer, Berlin (2016)"},{"issue":"7","key":"6_CR20","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X Leroy","year":"2009","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107\u2013115 (2009)","journal-title":"Commun. ACM"},{"key":"6_CR21","doi-asserted-by":"crossref","unstructured":"Liew, D., Cadar, C., Donaldson, A.F.: Symbooglix: A symbolic execution engine for boogie programs. In: ICST, pp. 45\u201356. IEEE Computer Society (2016)","DOI":"10.1109\/ICST.2016.11"},{"issue":"1","key":"6_CR22","first-page":"100","volume":"10","author":"WM McKeeman","year":"1998","unstructured":"McKeeman, W.M.: Differential testing for software. Digit. Tech. J. 10(1), 100\u2013107 (1998)","journal-title":"Digit. Tech. J."},{"key":"6_CR23","unstructured":"$$\\mu $$\u03bcgie repository. https:\/\/emptylambda.github.io\/mu-gie\/"},{"key":"6_CR24","doi-asserted-by":"crossref","unstructured":"Pacheco, C., Lahiri, S.K., Ernst, M.D., Ball, T.: Feedback-directed random test generation. In: ICSE, pp. 75\u201384. IEEE Computer Society (2007)","DOI":"10.1109\/ICSE.2007.37"},{"key":"6_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1007\/978-3-642-40787-1_15","volume-title":"Runtime Verification","author":"N Polikarpova","year":"2013","unstructured":"Polikarpova, N., Furia, C.A., West, S.: To run what no one has run before: executing an intermediate verification language. In: Legay, A., Bensalem, S. (eds.) RV 2013. LNCS, vol. 8174, pp. 251\u2013268. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-40787-1_15"},{"issue":"9","key":"6_CR26","doi-asserted-by":"publisher","first-page":"805","DOI":"10.1109\/TSE.2016.2532875","volume":"42","author":"S Segura","year":"2016","unstructured":"Segura, S., Fraser, G., Sanchez, A.B., Ruiz-Cort\u00e9s, A.: A survey on metamorphic testing. IEEE Trans. Softw. Eng. 42(9), 805\u2013824 (2016)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"6_CR27","unstructured":"Tange, O.: GNU parallel\u2014the command-line power tool. Login: USENIX Mag. 36, 42\u201347 (2011)"},{"issue":"6","key":"6_CR28","doi-asserted-by":"publisher","first-page":"283","DOI":"10.1145\/1993316.1993532","volume":"46","author":"Xuejun Yang","year":"2011","unstructured":"Yang, X., Chen, Y., Eide, E., Regehr, J.: Finding and understanding bugs in C compilers. ACM SIGPLAN Not. ACM 46, 283\u2013294 (2011)","journal-title":"ACM SIGPLAN Notices"},{"issue":"2","key":"6_CR29","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1109\/32.988498","volume":"28","author":"A Zeller","year":"2002","unstructured":"Zeller, A., Hildebrandt, R.: Simplifying and isolating failure-inducing input. IEEE Trans. Softw. Eng. 28(2), 183\u2013200 (2002)","journal-title":"IEEE Trans. Softw. Eng."}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-01090-4_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,24]],"date-time":"2019-10-24T23:32:16Z","timestamp":1571959936000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-01090-4_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783030010898","9783030010904"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-01090-4_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]},"assertion":[{"value":"ATVA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Automated Technology for Verification and Analysis","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Los Angeles, CA","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2018","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 October 2018","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 October 2018","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"atva2018","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/atva-conference.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}