{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T07:23:52Z","timestamp":1760081032773,"version":"3.40.3"},"publisher-location":"Cham","reference-count":28,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031754333"},{"type":"electronic","value":"9783031754340"}],"license":[{"start":{"date-parts":[[2024,12,30]],"date-time":"2024-12-30T00:00:00Z","timestamp":1735516800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,12,30]],"date-time":"2024-12-30T00:00:00Z","timestamp":1735516800000},"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-75434-0_10","type":"book-chapter","created":{"date-parts":[[2024,12,29]],"date-time":"2024-12-29T09:24:31Z","timestamp":1735464271000},"page":"145-166","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Proof Repair Utilizing Large Language Models: A Case Study on\u00a0the\u00a0Copland Remote Attestation Proofbase"],"prefix":"10.1007","author":[{"given":"Amer","family":"Tahat","sequence":"first","affiliation":[]},{"given":"David","family":"Hardin","sequence":"additional","affiliation":[]},{"given":"Adam","family":"Petz","sequence":"additional","affiliation":[]},{"given":"Perry","family":"Alexander","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,12,30]]},"reference":[{"key":"10_CR1","doi-asserted-by":"crossref","unstructured":"Amundson, I., Cofer, D.: Resolute assurance arguments for cyber assured systems engineering. In: Design Automation for Cyber-Physical Systems and Internet of Things (DESTION 2021), May 2021","DOI":"10.1145\/3445034.3460507"},{"key":"10_CR2","doi-asserted-by":"publisher","unstructured":"Belt, J., et al.: Model-driven development for the seL4 microkernel using the HAMR framework. J. Syst. Architect. 134, 102789 (2023). https:\/\/doi.org\/10.1016\/j.sysarc.2022.102789. https:\/\/www.sciencedirect.com\/science\/article\/pii\/S1383762122002740","DOI":"10.1016\/j.sysarc.2022.102789"},{"key":"10_CR3","unstructured":"Chowdhery, A., et al.: PaLM: Scaling language modeling with pathways (2022). https:\/\/arxiv.org\/pdf\/2204.02311.pdf"},{"key":"10_CR4","doi-asserted-by":"publisher","unstructured":"Cofer, D., et al.: Cyber assured systems engineering at scale. In: IEEE Security & Privacy, pp. 52\u201364, May\/June 2022. https:\/\/doi.org\/10.1109\/MSEC.2022.3151733","DOI":"10.1109\/MSEC.2022.3151733"},{"issue":"2","key":"10_CR5","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1007\/s10207-011-0124-7","volume":"10","author":"G Coker","year":"2011","unstructured":"Coker, G., et al.: Principles of remote attestation. Int. J. Inf. Secur. 10(2), 63\u201381 (2011)","journal-title":"Int. J. Inf. Secur."},{"key":"10_CR6","doi-asserted-by":"crossref","unstructured":"First, E., Rabe, M.N., Ringer, T., Brun, Y.: Baldur: Whole-proof generation and repair with large language models (2023). https:\/\/arxiv.org\/pdf\/2303.04910.pdf","DOI":"10.1145\/3611643.3616243"},{"key":"10_CR7","unstructured":"Haldar, V., Chandra, D., Franz, M.: Semantic remote attestation \u2013 a virtual machine directed approach to trusted computing. In: Proceedings of the Third Virtual Machine Research and Technology Symposium. San Jose, CA, May 2004"},{"key":"10_CR8","doi-asserted-by":"crossref","unstructured":"Leino, K.R.M.: Developing verified programs with Dafny. In: Proceedings of the 2013 International Conference on Software Engineering. pp. 1488\u20131490. ICSE \u201913, IEEE Press, Piscataway, NJ, USA (2013), http:\/\/dl.acm.org\/citation.cfm?id=2486788.2487050","DOI":"10.1109\/ICSE.2013.6606754"},{"key":"10_CR9","unstructured":"Lewkowycz, A., et al.: Solving quantitative reasoning problems with language models (2022). https:\/\/arxiv.org\/pdf\/2206.14858.pdf"},{"key":"10_CR10","unstructured":"Megill, N., Wheeler, D.A.: Metamath: A computer language for mathematical proofs (2019), https:\/\/us.metamath.org\/downloads\/metamath.pdf"},{"key":"10_CR11","unstructured":"OpenAI: Evaluation templates (2023). https:\/\/github.com\/openai\/evals\/blob\/main\/docs\/eval-templates.md. Accessed 9 Dec 2023"},{"key":"10_CR12","unstructured":"OpenAI: GPT-4 Technical Report (2023), https:\/\/arxiv.org\/pdf\/2303.08774.pdf"},{"key":"10_CR13","unstructured":"OpenAI: Legacy fine-tuning guide (2023). https:\/\/platform.openai.com\/docs\/guides\/legacy-fine-tuning. Accessed 9 Dec 2023"},{"key":"10_CR14","unstructured":"OpenAI: Prompt engineering strategies (2023). https:\/\/platform.openai.com\/docs\/guides\/prompt-engineering\/strategy-use-external-tools. Accessed 9 Dec 2023"},{"key":"10_CR15","doi-asserted-by":"publisher","unstructured":"Pearce, H., Ahmad, B., Tan, B., Dolan-Gavitt, B., Karri, R.: Asleep at the keyboard? assessing the security of GitHub Copilot\u2019s code contributions. In: 2022 IEEE Symposium on Security and Privacy, pp. 754\u2013768 (2022). https:\/\/doi.org\/10.1109\/SP46214.2022.9833571","DOI":"10.1109\/SP46214.2022.9833571"},{"key":"10_CR16","unstructured":"Pei, K., Bieber, D., Shi, K., Sutton, C., Yin, P.: Can large language models reason about program invariants? In: Krause, A., Brunskill, E., Cho, K., Englehardt, B., Sabato, S., Scarlett, J. (eds.) Proceedings of the 40th International Conference on Machine Learning. Proceedings of Machine Learning Research, vol.\u00a0202, pp. 27496\u201327520. PMLR, July 2023. https:\/\/proceedings.mlr.press\/v202\/pei23a\/pei23a.html"},{"key":"10_CR17","doi-asserted-by":"crossref","unstructured":"Pendergrass, J.A., Helble, S., Clemens, J., Loscocco, P.: Maat: a platform service for measurement and attestation. arXiv preprint arXiv:1709.10147 (2017)","DOI":"10.1109\/MILCOM.2018.8599735"},{"key":"10_CR18","unstructured":"Perry, N., Srivastava, M., Kumar, D., Boneh, D.: Do users write more insecure code with AI assistants? (2022). https:\/\/arxiv.org\/pdf\/2211.03622.pdf"},{"key":"10_CR19","doi-asserted-by":"crossref","unstructured":"Petz, A., Alexander, P.: An Infrastructure for Faithful Execution of Remote Attestation Protocols. Innovations in Systems and Software Engineering (2022)","DOI":"10.1007\/978-3-030-76384-8_17"},{"key":"10_CR20","doi-asserted-by":"crossref","unstructured":"Petz, A., Alexander, P.: An infrastructure for faithful execution of remote attestation protocols. In: Proceedings of the 13th NASA Formal Methods Symposium (NFM 2021) (May 2021)","DOI":"10.1007\/978-3-030-76384-8_17"},{"key":"10_CR21","doi-asserted-by":"crossref","unstructured":"Petz, A., Jurgensen, G., Alexander, P.: Design and formal verification of a Copland-based attestation protocol. In: ACM\/IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE 2021), November 2021","DOI":"10.1145\/3487212.3487340"},{"key":"10_CR22","unstructured":"Polu, S., Sutskever, I.: Generative language modeling for automated theorem proving (2020). https:\/\/arxiv.org\/pdf\/2009.03393.pdf"},{"key":"10_CR23","doi-asserted-by":"crossref","unstructured":"Ramsdell, J., et al.: Orchestrating layered attestations. In: Principles of Security and Trust (POST\u201919). Prague, Czech Republic (April 8-11 2019)","DOI":"10.1007\/978-3-030-17138-4_9"},{"key":"10_CR24","doi-asserted-by":"crossref","unstructured":"Rowe, P.D.: Bundling evidence for layered attestation. In: Trust and Trustworthy Computing, pp. 119\u2013139. Springer, Cham (2016)","DOI":"10.1007\/978-3-319-45572-3_7"},{"key":"10_CR25","doi-asserted-by":"crossref","unstructured":"Sun, C., Sheng, Y., Padon, O., Barrett, C.: Clover: closed-loop verifiable code generation (2024). https:\/\/arxiv.org\/pdf\/2310.17807.pdf","DOI":"10.1007\/978-3-031-65112-0_7"},{"key":"10_CR26","unstructured":"Trusted Computing Group: TCG TPM Specification. Trusted Computing Group, 3885 SW 153rd Drive, Beaverton, OR 97006, version 1.2 revision 103 edn., July 2007. https:\/\/www.trustedcomputinggroup.org\/resources\/tpm_main_specification\/"},{"key":"10_CR27","unstructured":"Wu, H., Barrett, C., Narodytska, N.: Lemur: Integrating large language models in automated program verification (2023). https:\/\/arxiv.org\/pdf\/2310.04870.pdf"},{"key":"10_CR28","unstructured":"Zhang, S.D., First, E., Ringer, T.: Getting more out of large language models for proofs (2023). https:\/\/arxiv.org\/pdf\/2305.04369.pdf"}],"container-title":["Lecture Notes in Computer Science","Bridging the Gap Between AI and Reality"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-75434-0_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,12,29]],"date-time":"2024-12-29T10:02:42Z","timestamp":1735466562000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-75434-0_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,12,30]]},"ISBN":["9783031754333","9783031754340"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-75434-0_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024,12,30]]},"assertion":[{"value":"30 December 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"AISoLA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Bridging the Gap between AI and Reality","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Crete","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Greece","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":"30 October 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 November 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"aisola2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/2023-aisola.isola-conference.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}