{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,19]],"date-time":"2025-10-19T00:13:12Z","timestamp":1760832792546,"version":"build-2065373602"},"publisher-location":"Cham","reference-count":17,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031986673"},{"type":"electronic","value":"9783031986680"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,7,22]],"date-time":"2025-07-22T00:00:00Z","timestamp":1753142400000},"content-version":"vor","delay-in-days":202,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>This paper presents a modular approach to verifying the vector module of PETSc, a widely used library in scientific computing, using the CIVL model checker. Our approach relies on the creation of stub functions, which serve a dual purpose of specifying the intended behavior of individual PETSc functions and providing an abstraction for called functions to allow efficient verification of callers. This facilitates the use of symbolic execution and model checking to establish the correctness of isolated functions. Our work contributes to the ongoing effort to enhance the reliability of high-performance computing libraries and proposes an effective verification strategy for complex scientific software.<\/jats:p>","DOI":"10.1007\/978-3-031-98668-0_7","type":"book-chapter","created":{"date-parts":[[2025,7,21]],"date-time":"2025-07-21T20:46:11Z","timestamp":1753130771000},"page":"148-161","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Verifying PETSc Vector Components Using CIVL"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0001-5036-8968","authenticated-orcid":false,"given":"Venkata","family":"Dhavala","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3479-6361","authenticated-orcid":false,"given":"Jan","family":"H\u00fcckelheim","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0907-2567","authenticated-orcid":false,"given":"Paul D.","family":"Hovland","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9359-3332","authenticated-orcid":false,"given":"Stephen F.","family":"Siegel","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,7,22]]},"reference":[{"key":"7_CR1","doi-asserted-by":"publisher","unstructured":"Balay, S., et al.: PETSc\/TAO users manual. Technical report, ANL-21\/39 - Revision 3.21, Argonne National Laboratory (2024). https:\/\/doi.org\/10.2172\/2205494","DOI":"10.2172\/2205494"},{"key":"7_CR2","unstructured":"Balay, S., et al.: PETSc Web page (2024). https:\/\/petsc.org\/"},{"key":"7_CR3","doi-asserted-by":"publisher","unstructured":"Balay, S., Gropp, W.D., McInnes, L.C., Smith, B.F.: Efficient management of parallelism in object-oriented numerical software libraries. In: Modern Software Tools for Scientific Computing, pp. 163\u2013202. Springer, Cham (1997). https:\/\/doi.org\/10.1007\/978-1-4612-1986-6_8","DOI":"10.1007\/978-1-4612-1986-6_8"},{"key":"7_CR4","doi-asserted-by":"publisher","unstructured":"Barrett, C., et al.: CVC4. In: Computer Aided Verification: 23rd International Conference (CAV 2011). Lecture Notes in Computer Science, vol.\u00a06806, pp. 171\u2013177. Springer, Cham (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_14","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"7_CR5","unstructured":"Baudin, P., et al.: ACSL: ANSI\/ISO C Specification Language, version 1.16 (2020). http:\/\/frama-c.com\/download\/acsl-1.16.pdf"},{"key":"7_CR6","doi-asserted-by":"publisher","unstructured":"Chong, N., et al.: Code-level model checking in the software development workflow. In: Proceedings of the ACM\/IEEE 42nd International Conference on Software Engineering: Software Engineering in Practice. ICSE-SEIP \u201920, pp. 11\u201320. Association for Computing Machinery, New York, NY, USA (2020). https:\/\/doi.org\/10.1145\/3377813.3381347","DOI":"10.1145\/3377813.3381347"},{"key":"7_CR7","unstructured":"CIVL: The Concurrency Intermediate Verification Language. https:\/\/civl.dev. Accessed 20 May 2024"},{"key":"7_CR8","unstructured":"Clarke Jr., E.M., Grumberg, O., Kroening, D., Peled, D., Veith, H.: Model Checking. MIT Press, Cambridge, MA, USA, 2 edn (2018). https:\/\/mitpress.mit.edu\/books\/model-checking-second-edition"},{"key":"7_CR9","doi-asserted-by":"publisher","unstructured":"De\u00a0Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: International conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2008). Lecture Notes in Computer Science, vol.\u00a04963, pp. 337\u2013340. Springer, Cham (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"7_CR10","doi-asserted-by":"publisher","unstructured":"Kellison, A.E., Appel, A.W., Tekriwal, M., Bindel, D.: LAProof: a library of formal proofs of accuracy and correctness for linear algebra programs. In: 2023 IEEE 30th Symposium on Computer Arithmetic (ARITH), pp. 36\u201343. IEEE (2023). https:\/\/doi.org\/10.1109\/ARITH58626.2023.00021","DOI":"10.1109\/ARITH58626.2023.00021"},{"issue":"7","key":"7_CR11","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1145\/360248.360252","volume":"19","author":"JC King","year":"1976","unstructured":"King, J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385\u2013394 (1976). https:\/\/doi.org\/10.1145\/360248.360252","journal-title":"Commun. ACM"},{"key":"7_CR12","unstructured":"Message Passing Interface Forum: MPI: A Message-Passing Interface Standard Version 4.1 (2023). https:\/\/www.mpi-forum.org\/docs\/mpi-4.1\/mpi41-report.pdf"},{"key":"7_CR13","doi-asserted-by":"publisher","unstructured":"Meyer, B.: Applying \u201cdesign by contract.\u201d IEEE Comput. 25(10), 40\u201351 (1992). https:\/\/doi.org\/10.1109\/2.161279","DOI":"10.1109\/2.161279"},{"key":"7_CR14","unstructured":"OpenMP Architecture Review Board: OpenMP Application Programming Interface, version 6.0 (2024). https:\/\/www.openmp.org\/wp-content\/uploads\/OpenMP-API-Specification-6-0.pdf"},{"key":"7_CR15","doi-asserted-by":"publisher","unstructured":"Siegel, S.F., et al.: CIVL: the concurrency intermediate verification language. In: SC15: Proceedings of the International Conference for High Performance Computing, Networking, Storage and Analysis. ACM, New York (2015). https:\/\/doi.org\/10.1145\/2807591.2807635, Article No. 61, pp. 1\u201312","DOI":"10.1145\/2807591.2807635"},{"issue":"4","key":"7_CR16","doi-asserted-by":"publisher","first-page":"395","DOI":"10.1007\/s11786-011-0100-7","volume":"5","author":"SF Siegel","year":"2011","unstructured":"Siegel, S.F., Zirkel, T.K.: TASS: the toolkit for accurate scientific software. Math. Comput. Sci. 5(4), 395\u2013426 (2011). https:\/\/doi.org\/10.1007\/s11786-011-0100-7","journal-title":"Math. Comput. Sci."},{"key":"7_CR17","doi-asserted-by":"publisher","unstructured":"Zheng, M., Rogers, M.S., Luo, Z., Dwyer, M.B., Siegel, S.F.: CIVL: formal verification of parallel programs. In: Proceedings of the 30th ACM\/IEEE International Conference on Automated Software Engineering (ASE\u201915), pp. 830\u2013835. ACM, New York, NY, USA (2015). https:\/\/doi.org\/10.1109\/ASE.2015.99","DOI":"10.1109\/ASE.2015.99"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-98668-0_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,18]],"date-time":"2025-10-18T05:38:38Z","timestamp":1760765918000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-98668-0_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031986673","9783031986680"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-98668-0_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"22 July 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Zagreb","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Croatia","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 July 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 July 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"37","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conferences.i-cav.org\/2025\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}