{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T02:09:47Z","timestamp":1776305387193,"version":"3.50.1"},"publisher-location":"Cham","reference-count":17,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031906596","type":"print"},{"value":"9783031906602","type":"electronic"}],"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,5,1]],"date-time":"2025-05-01T00:00:00Z","timestamp":1746057600000},"content-version":"vor","delay-in-days":120,"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>PROTON 2.1 presents (1) a new termination checking technique that uses a fine-tuned local LLM to synthesize ranking functions, and (2) support for multiple SAT solvers for non-termination checking.<\/jats:p>","DOI":"10.1007\/978-3-031-90660-2_19","type":"book-chapter","created":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T09:38:00Z","timestamp":1746005880000},"page":"242-247","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["PROTON 2.1: Synthesizing Ranking Functions via fine-tuned locally Hosted LLM (Competition Contribution)"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0005-0814-3094","authenticated-orcid":false,"given":"Diganta","family":"Mukhopadhyay","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7368-2389","authenticated-orcid":false,"given":"Ravindra","family":"Metta","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9132-8356","authenticated-orcid":false,"given":"Hrishikesh","family":"Karmarkar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5686-9758","authenticated-orcid":false,"given":"Kumar","family":"Madhukar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,5,1]]},"reference":[{"key":"19_CR1","unstructured":"Llama-3.2-1B-Instruct. https:\/\/huggingface.co\/meta-llama\/Llama-3.2-1B-Instruct, accessed: 2024-11-07"},{"key":"19_CR2","unstructured":"llama.cpp. https:\/\/github.com\/ggerganov\/llama.cpp, accessed: 2024-11-07"},{"key":"19_CR3","unstructured":"Meta-Llama-3-70B-Instruct. https:\/\/huggingface.co\/meta-llama\/Meta-Llama-3-70B-Instruct, accessed: 2024-08-14"},{"key":"19_CR4","unstructured":"Python Bindings for llama.cpp. https:\/\/github.com\/abetlen\/llama-cpp-python, accessed: 2024-11-07"},{"key":"19_CR5","doi-asserted-by":"publisher","unstructured":"PROTON SV-COMP 2025 Competition Contribution (Nov 2024). https:\/\/doi.org\/10.5281\/zenodo.14209458","DOI":"10.5281\/zenodo.14209458"},{"key":"19_CR6","doi-asserted-by":"publisher","unstructured":"Training Scripts and Data set of LLM-PROTON (Feb 2025). https:\/\/doi.org\/10.5281\/zenodo.14854742","DOI":"10.5281\/zenodo.14854742"},{"key":"19_CR7","doi-asserted-by":"publisher","unstructured":"Audemard, G., Simon, L.: On the Glucose SAT Solver. Int. J. Artif. Intell. Tools pp. 1840001:1\u20131840001:25 (2018). https:\/\/doi.org\/10.1142\/S0218213018400018","DOI":"10.1142\/S0218213018400018"},{"key":"19_CR8","unstructured":"Baudin, P., Bobot, F., Correnson, L., Dargaye, Z., Blanchard, A.: WP Plug-in Manual, http:\/\/frama-c.com\/download\/frama-c-wp-manual.pdf"},{"key":"19_CR9","unstructured":"Baudin, P., Filli\u00e2tre, J.C., March\u00e9, C., Monate, B., Moy, Y., Prevosto, V.: ACSL: ANSI\/ISO C Specification Language, http:\/\/frama-c.com\/download\/acsl.pdf"},{"key":"19_CR10","unstructured":"Beyer, D., Strej\u010dek, J.: Improvements in software verification and witness validation: SV-COMP 2025. In: Proc. TACAS. LNCS (2025)"},{"key":"19_CR11","doi-asserted-by":"publisher","unstructured":"Beyer, D.: State of the Art in Software Verification and Witness Validation: SV-COMP 2024. In: TACAS. pp. 299\u2013329 (2024). https:\/\/doi.org\/10.1007\/978-3-031-57256-2_15","DOI":"10.1007\/978-3-031-57256-2_15"},{"key":"19_CR12","unstructured":"Biere, A., Fazekas, K., Fleury, M., Heisinger, M.: CaDiCaL, Kissat, Paracooba, Plingeling and Treengeling Entering the SAT Competition 2020. In: Proc.\u00a0of SAT Competition 2020 \u2013 Solver and Benchmark Descriptions. pp. 51\u201353 (2020)"},{"key":"19_CR13","unstructured":"C Bounded Model Checker. https:\/\/github.com\/diffblue\/cbmc"},{"key":"19_CR14","unstructured":"Correnson, L., Cuoq, P., Kirchner, F., Maroneze, A., Prevosto, V., Puccetti, A., Signoles, J., Yakobowski, B.: Frama-C User Manual, http:\/\/frama-c.com\/download\/frama-c-user-manual.pdf"},{"key":"19_CR15","doi-asserted-by":"publisher","unstructured":"Kamath, A., Mohammed, N., Senthilnathan, A., Chakraborty, S., Deligiannis, P., Lahiri, S.K., Lal, A., Rastogi, A., Roy, S., Sharma, R.: Leveraging LLMs for Program Verification. In: FMCAD. pp. 107\u2013118 (2024). https:\/\/doi.org\/10.34727\/2024\/isbn.978-3-85448-065-5_16","DOI":"10.34727\/2024\/isbn.978-3-85448-065-5_16"},{"key":"19_CR16","doi-asserted-by":"publisher","unstructured":"Kamath, A., Senthilnathan, A., Chakraborty, S., Deligiannis, P., Lahiri, S.K., Lal, A., Rastogi, A., Roy, S., Sharma, R.: Finding Inductive Loop Invariants using Large Language Models. CoRR abs\/2311.07948 (2023). https:\/\/doi.org\/10.48550\/ARXIV.2311.07948","DOI":"10.48550\/ARXIV.2311.07948"},{"key":"19_CR17","doi-asserted-by":"publisher","unstructured":"Metta, R., Karmarkar, H., Madhukar, K., Venkatesh, R., Chakraborty, S.: PROTON: PRObes for Termination Or Not (Competition Contribution). In: TACAS. pp. 393\u2013398 (2024). https:\/\/doi.org\/10.1007\/978-3-031-57256-2_27","DOI":"10.1007\/978-3-031-57256-2_27"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-90660-2_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T09:38:07Z","timestamp":1746005887000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-90660-2_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031906596","9783031906602"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-90660-2_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"1 May 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Hamilton, ON","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","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":"3 May 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 May 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2025\/conferences\/tacas\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}