{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,30]],"date-time":"2026-04-30T04:55:42Z","timestamp":1777524942945,"version":"3.51.4"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031773815","type":"print"},{"value":"9783031773822","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,11,26]],"date-time":"2024-11-26T00:00:00Z","timestamp":1732579200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,11,26]],"date-time":"2024-11-26T00:00:00Z","timestamp":1732579200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"DOI":"10.1007\/978-3-031-77382-2_21","type":"book-chapter","created":{"date-parts":[[2024,11,25]],"date-time":"2024-11-25T19:26:39Z","timestamp":1732562799000},"page":"366-384","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Unlocking the\u00a0Power of\u00a0Environment Assumptions for\u00a0Unit Proofs"],"prefix":"10.1007","author":[{"given":"Siddharth","family":"Priya","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Temesghen","family":"Kahsai","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Arie","family":"Gurfinkel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,11,26]]},"reference":[{"key":"21_CR1","unstructured":"Crux (2023). https:\/\/crux.galois.com\/"},{"key":"21_CR2","unstructured":"Authors, T.: Introducing \u201cTesting on the Toilet\u201d (2007). https:\/\/testing.googleblog.com\/2007\/01\/introducing-testing-on-toilet.html"},{"key":"21_CR3","unstructured":"Authors, T.: Tott: partial mocks using forwarding objects (2009). https:\/\/testing.googleblog.com\/2009\/02\/tott-partial-mocks-using-forwarding_19.html"},{"key":"21_CR4","unstructured":"Authors, T.: Testing on the toilet: Don\u2019t mock types you don\u2019t own (2020). https:\/\/testing.googleblog.com\/2020\/07\/testing-on-toilet-dont-mock-types-you.html"},{"key":"21_CR5","doi-asserted-by":"publisher","unstructured":"Ball, T., et al.: Thorough static analysis of device drivers. In: Berbers, Y., Zwaenepoel, W. (eds.) 2006 EuroSys Conference, Leuven, Belgium, April 18-21, 2006, Proceedings, pp. 73\u201385. ACM (2006). https:\/\/doi.org\/10.1145\/1217935.1217943","DOI":"10.1145\/1217935.1217943"},{"key":"21_CR6","unstructured":"Beck, K.: Test-driven development: by example. Addison-Wesley Professional (2003)"},{"key":"21_CR7","unstructured":"Boeira, M.: Using sourcery to automatically generate mocks (2019). https:\/\/medium.com\/@mdboeira\/using-sourcery-to-automatically-generate-mocks-73ced75b2863"},{"key":"21_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"808","DOI":"10.1007\/978-3-030-81685-8_38","volume-title":"Computer Aided Verification","author":"NFF Bragg","year":"2021","unstructured":"Bragg, N.F.F., Foster, J.S., Roux, C., Solar-Lezama, A.: Program sketching by automatically generating mocks from tests. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12759, pp. 808\u2013831. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81685-8_38"},{"key":"21_CR9","unstructured":"Cadar, C., Dunbar, D., Engler, D.R.: KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In: Draves, R., van Renesse, R. (eds.) 8th USENIX Symposium, OSDI 2008, December 8-10, 2008, San Diego, California, USA, Proceedings, pp. 209\u2013224. USENIX Association (2008). https:\/\/dl.acm.org\/doi\/10.5555\/1855741.1855756"},{"issue":"4","key":"21_CR10","doi-asserted-by":"publisher","first-page":"772","DOI":"10.1002\/spe.2949","volume":"51","author":"N Chong","year":"2021","unstructured":"Chong, N., Cook, B., Eidelman, J., Kallas, K., Khazem, K., Monteiro, F.R., Schwartz-Narbonne, D., Tasiran, S., Tautschnig, M., Tuttle, M.R.: Code-level model checking in the software development workflow at amazon web services. Softw. Pract. Exp. 51(4), 772\u2013797 (2021). https:\/\/doi.org\/10.1002\/spe.2949","journal-title":"Softw. Pract. Exp."},{"key":"21_CR11","unstructured":"jMock Developers: jmock (2019). http:\/\/jmock.org\/"},{"key":"21_CR12","unstructured":"cmocka Developers.: cmocka website (2023). https:\/\/cmocka.org\/"},{"key":"21_CR13","unstructured":"mbedTLS Developers: mbedtls project (2023). https:\/\/github.com\/Mbed-TLS\/mbedtls"},{"key":"21_CR14","unstructured":"Developers, A.: Trusty tee (2023), https:\/\/source.android.com\/docs\/security\/features\/trusty"},{"key":"21_CR15","unstructured":"Developers, B.H.: Boost.hana (2023). https:\/\/boostorg.github.io\/hana\/index.html"},{"key":"21_CR16","unstructured":"Developers, E.: Easymock (2022). https:\/\/easymock.org\/"},{"key":"21_CR17","unstructured":"Developers., K.: Using kani to validate security boundaries in aws firecracker (2024). https:\/\/model-checking.github.io\/kani-verifier-blog\/2023\/08\/31\/using-kani-to-validate-security-boundaries-in-aws-firecracker.html"},{"key":"21_CR18","doi-asserted-by":"publisher","unstructured":"Freeman, S., Mackinnon, T., Pryce, N., Walnes, J.: Mock roles, objects. In: Vlissides, J.M., Schmidt, D.C. (eds.) OOPSLA 2004, Vancouver, BC, Canada, pp. 236\u2013246. ACM (2004). https:\/\/doi.org\/10.1145\/1028664.1028765","DOI":"10.1145\/1028664.1028765"},{"key":"21_CR19","doi-asserted-by":"publisher","unstructured":"Freeman, S., Pryce, N.: Evolving an embedded domain-specific language in java. In: Tarr, P.L., Cook, W.R. (eds.) OOPSLA 2006, Portland, Oregon, USA, pp. 855\u2013865. ACM (2006). https:\/\/doi.org\/10.1145\/1176617.1176735","DOI":"10.1145\/1176617.1176735"},{"key":"21_CR20","doi-asserted-by":"publisher","unstructured":"Hamza, J., Felix, S., Kuncak, V., Nussbaumer, I., Schramka, F.: From verified scala to STIX file system embedded code using stainless. In: Deshmukh, J.V., Havelund, K., Perez, I. (eds.) NFM 2022, Pasadena, CA, USA. LNCS, vol. 13260, pp. 393\u2013410. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-06773-0_21","DOI":"10.1007\/978-3-031-06773-0_21"},{"key":"21_CR21","unstructured":"Kraus, S.: Using sourcery to automatically generate mocks (2019). https:\/\/medium.com\/iqoqo-engineering\/this-library-uses-your-jest-tests-to-generate-mocks-c07c322c58e3"},{"key":"21_CR22","doi-asserted-by":"publisher","unstructured":"Lahiri, S.K., Lal, A., Gopinath, S., Nutz, A., Levin, V., Kumar, R., Deisinger, N., Lichtenberg, J., Bansal, C.: Angelic checking within static driver verifier: Towards high-precision defects without (modeling) cost. In: FMCAD 2020, Haifa, Israel, pp. 169\u2013178. IEEE (2020). https:\/\/doi.org\/10.34727\/2020\/isbn.978-3-85448-042-6_24","DOI":"10.34727\/2020\/isbn.978-3-85448-042-6_24"},{"key":"21_CR23","doi-asserted-by":"crossref","unstructured":"Lattner, C., Adve, V.: LLVM: a compilation framework for lifelong program analysis and transformation, pp. 75\u201388. San Jose, CA, USA, March 2004","DOI":"10.1109\/CGO.2004.1281665"},{"key":"21_CR24","unstructured":"LLC., G.: Googletest user\u2019s guide (2023). https:\/\/google.github.io\/googletest\/"},{"key":"21_CR25","doi-asserted-by":"publisher","unstructured":"Munir, H., Wnuk, K., Petersen, K., Moayyed, M.: An experimental evaluation of test driven development vs. test-last development with industry professionals. In: Shepperd, M.J., Hall, T., Myrtveit, I. (eds.) EASE \u201914, London, United Kingdom, May 13-14, 2014, pp. 50:1\u201350:10. ACM (2014). https:\/\/doi.org\/10.1145\/2601248.2601267","DOI":"10.1145\/2601248.2601267"},{"issue":"3","key":"21_CR26","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1007\/s10664-008-9062-z","volume":"13","author":"N Nagappan","year":"2008","unstructured":"Nagappan, N., Maximilien, E.M., Bhat, T., Williams, L.A.: Realizing quality improvement through test driven development: results and experiences of four industrial teams. Empir. Softw. Eng. 13(3), 289\u2013302 (2008). https:\/\/doi.org\/10.1007\/s10664-008-9062-z","journal-title":"Empir. Softw. Eng."},{"key":"21_CR27","doi-asserted-by":"publisher","unstructured":"Priya, S., Gurfinkel, A., Kahsai, T.: verify-mbedtls-artifact, June 2024. https:\/\/doi.org\/10.6084\/m9.figshare.26122222. https:\/\/figshare.com\/articles\/dataset\/verify-mbedtls-artifact\/26122222\/1","DOI":"10.6084\/m9.figshare.26122222"},{"key":"21_CR28","unstructured":"Priya, S., Kahsai, T., Gurfinkel, A.: Unlocking the power of environment assumptions for unit proofs (extended) (2024). https:\/\/github.com\/seahorn\/seamock\/blob\/main\/paper.md"},{"key":"21_CR29","doi-asserted-by":"publisher","unstructured":"Priya, S., Su, Y., Bao, Y., Zhou, X., Vizel, Y., Gurfinkel, A.: Bounded model checking for LLVM. In: Griggio, A., Rungta, N. (eds.) FMCAD 2022, Trento, Italy, pp. 214\u2013224. IEEE (2022). https:\/\/doi.org\/10.34727\/2022\/isbn.978-3-85448-053-2_28","DOI":"10.34727\/2022\/isbn.978-3-85448-053-2_28"},{"issue":"3","key":"21_CR30","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1007\/s11334-022-00443-9","volume":"18","author":"S Priya","year":"2022","unstructured":"Priya, S., Zhou, X., Su, Y., Vizel, Y., Bao, Y., Gurfinkel, A.: Verifying verified code. Innov. Syst. Softw. Eng. 18(3), 335\u2013346 (2022). https:\/\/doi.org\/10.1007\/s11334-022-00443-9","journal-title":"Innov. Syst. Softw. Eng."},{"key":"21_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"106","DOI":"10.1007\/978-3-319-08867-9_7","volume-title":"Computer Aided Verification","author":"Z Rakamari\u0107","year":"2014","unstructured":"Rakamari\u0107, Z., Emmi, M.: SMACK: decoupling source language details from verifier implementations. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 106\u2013113. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_7"},{"key":"21_CR32","doi-asserted-by":"publisher","unstructured":"Romano, S., Zampetti, F., Baldassarre, M.T., Penta, M.D., Scanniello, G.: Do static analysis tools affect software quality when using test-driven development? In: Madeiral, F., Lassenius, C., Conte, T., M\u00e4nnist\u00f6, T. (eds.) ESEM \u201922: ACM\/IEEE Helsinki, Finland, pp. 80\u201391. ACM (2022). https:\/\/doi.org\/10.1145\/3544902.3546233","DOI":"10.1145\/3544902.3546233"},{"key":"21_CR33","unstructured":"Wright, H., Winters, T.D., Manshreck, T.: Software Engineering at Google. O\u2019Reilly (2020)"}],"container-title":["Lecture Notes in Computer Science","Software Engineering and Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-77382-2_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,25]],"date-time":"2024-11-25T20:03:30Z","timestamp":1732565010000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-77382-2_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,11,26]]},"ISBN":["9783031773815","9783031773822"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-77382-2_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,11,26]]},"assertion":[{"value":"26 November 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SEFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Software Engineering and Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Aveiro","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"4 November 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 November 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"sefm2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/sefm-conference.github.io\/2024\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}