{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,19]],"date-time":"2026-06-19T06:51:06Z","timestamp":1781851866922,"version":"3.54.5"},"reference-count":30,"publisher":"IEEE","license":[{"start":{"date-parts":[[2026,4,27]],"date-time":"2026-04-27T00:00:00Z","timestamp":1777248000000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2026,4,27]],"date-time":"2026-04-27T00:00:00Z","timestamp":1777248000000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026,4,27]]},"DOI":"10.1109\/vts69484.2026.11563380","type":"proceedings-article","created":{"date-parts":[[2026,6,18]],"date-time":"2026-06-18T20:06:49Z","timestamp":1781813209000},"page":"1-5","source":"Crossref","is-referenced-by-count":0,"title":["Automation of Polynomial Formal Verification using Large Language Models"],"prefix":"10.1109","author":[{"given":"Luca","family":"M\u00fcller","sequence":"first","affiliation":[{"name":"DFKI,Cyber-Physical Systems,Bremen,Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Khushboo","family":"Qayyum","sequence":"additional","affiliation":[{"name":"DFKI,Cyber-Physical Systems,Bremen,Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Nele","family":"Hugo","sequence":"additional","affiliation":[{"name":"Institute of Computer Science, University of Bremen,Bremen,Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Muhammad","family":"Hassan","sequence":"additional","affiliation":[{"name":"DFKI,Cyber-Physical Systems,Bremen,Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Rolf","family":"Drechsler","sequence":"additional","affiliation":[{"name":"DFKI,Cyber-Physical Systems,Bremen,Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"263","reference":[{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.1998.658762"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1109\/12.494097"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1016\/B978-0-12-800727-3.00001-0"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1109\/LATS57337.2022.9936904"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1098\/rsta.2023.0390"},{"key":"ref6","first-page":"122","article-title":"Next-generation automatic human-readable proofs enabling polynomial formal verification","volume-title":"Proceedings of the 21st ACM-IEEE International Conference on Formal Methods and Models for System Design","author":"Drechsler"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.18653\/v1\/2021.findings-acl.317"},{"key":"ref8","article-title":"Towards LLM-based generation of human-readable proofs in polynomial formal verification","volume":"abs\/2505.23311","author":"Drechsler","year":"2025","journal-title":"ArXiv"},{"key":"ref9","article-title":"Z3 theorem prover","year":"26"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.48550\/ARXIV.1706.03762"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676819"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1109\/DAC.1990.114826"},{"key":"ref13","article-title":"Polynomial formal verification of area-efficient and fast adders","volume-title":"2021 Reed Mulller Workshop (RM2021)","author":"Mahzoon"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1109\/ATS52891.2021.00027"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1109\/DDECS52668.2021.9417052"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1016\/j.micpro.2025.105199"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1137\/1.9780898719789"},{"key":"ref18","article-title":"Python 3 Reference Manual","author":"Van Rossum","year":"2009"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-35122-8_43"},{"key":"ref20","article-title":"GPT-5.1 instant and GPT-5.1 thinking system card addendum","year":"26"},{"key":"ref21","article-title":"GPT-5 system card","year":"26"},{"key":"ref22","article-title":"A new era of intelligence with Gemini 3","year":"26"},{"key":"ref23","article-title":"Qwen 3","year":"26"},{"key":"ref24","article-title":"Gemma 3","year":"26"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.3390\/electronics14010120"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1109\/fccm62733.2025.00048"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1109\/LAD62341.2024.10691801"},{"key":"ref28","first-page":"1","article-title":"IEEE standard for SystemVerilog\u2013unified hardware design, specification, and verification language","year":"2024","journal-title":"IEEE Std 1800-2023 (Revision of IEEE Std 1800-2017)"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1145\/3658617.3697756"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.23919\/DATE58400.2024.10546729"}],"event":{"name":"2026 IEEE 44th VLSI Test Symposium (VTS)","location":"Napa, CA, USA","start":{"date-parts":[[2026,4,27]]},"end":{"date-parts":[[2026,4,29]]}},"container-title":["2026 IEEE 44th VLSI Test Symposium (VTS)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx8\/11563061\/11563198\/11563380.pdf?arnumber=11563380","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,19]],"date-time":"2026-06-19T05:55:27Z","timestamp":1781848527000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/11563380\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,4,27]]},"references-count":30,"URL":"https:\/\/doi.org\/10.1109\/vts69484.2026.11563380","relation":{},"subject":[],"published":{"date-parts":[[2026,4,27]]}}}