{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,30]],"date-time":"2026-01-30T03:45:32Z","timestamp":1769744732507,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":40,"publisher":"ACM","license":[{"start":{"date-parts":[[2022,5,18]],"date-time":"2022-05-18T00:00:00Z","timestamp":1652832000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"National Research, Development and Innovation Fund","award":["2019-2.1.3- NEMZ ECSEL-2019-00003"],"award-info":[{"award-number":["2019-2.1.3- NEMZ ECSEL-2019-00003"]}]},{"name":"European Commission","award":["826452"],"award-info":[{"award-number":["826452"]}]},{"name":"Ministry for Innovation and Technology","award":["\u00daNKP-21-2-I-BME-142"],"award-info":[{"award-number":["\u00daNKP-21-2-I-BME-142"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2022,5,18]]},"DOI":"10.1145\/3524482.3527646","type":"proceedings-article","created":{"date-parts":[[2022,7,21]],"date-time":"2022-07-21T22:06:57Z","timestamp":1658441217000},"page":"1-11","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["C for yourself"],"prefix":"10.1145","author":[{"given":"Levente","family":"Bajczi","sequence":"first","affiliation":[{"name":"Budapest University of Technology and Economics, Budapest, Hungary"}]},{"given":"Zs\u00f3fia","family":"\u00c1d\u00e1m","sequence":"additional","affiliation":[{"name":"Budapest University of Technology and Economics, Budapest, Hungary"}]},{"given":"Vince","family":"Moln\u00e1r","sequence":"additional","affiliation":[{"name":"Budapest University of Technology and Economics, Budapest, Hungary"}]}],"member":"320","published-online":{"date-parts":[[2022,7,21]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"\u00c1d\u00e1m Zs\u00f3fia","unstructured":"Zs\u00f3fia \u00c1d\u00e1m , Gyula Sallai , and \u00c1kos Hajdu . 2021. Gazer-Theta: LLVM-based Verifier Portfolio with BMC\/CEGAR (Competition Contribution) . In Tools and Algorithms for the Construction and Analysis of Systems , Jan Friso Groote and Kim Guldstrand Larsen (Eds.). Springer International Publishing , Cham , 433--437. Zs\u00f3fia \u00c1d\u00e1m, Gyula Sallai, and \u00c1kos Hajdu. 2021. Gazer-Theta: LLVM-based Verifier Portfolio with BMC\/CEGAR (Competition Contribution). In Tools and Algorithms for the Construction and Analysis of Systems, Jan Friso Groote and Kim Guldstrand Larsen (Eds.). Springer International Publishing, Cham, 433--437."},{"key":"e_1_3_2_1_2_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Andrianov Pavel","unstructured":"Pavel Andrianov , Karlheinz Friedberger , Mikhail Mandrykin , Vadim Mutilin , and Anton Volkov . 2017. CPA-BAM-BnB: Block-Abstraction Memoization and Region-Based Memory Models for Predicate Abstractions . In Tools and Algorithms for the Construction and Analysis of Systems , Axel Legay and Tiziana Margaria (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg , 355--359. Pavel Andrianov, Karlheinz Friedberger, Mikhail Mandrykin, Vadim Mutilin, and Anton Volkov. 2017. CPA-BAM-BnB: Block-Abstraction Memoization and Region-Based Memory Models for Predicate Abstractions. In Tools and Algorithms for the Construction and Analysis of Systems, Axel Legay and Tiziana Margaria (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 355--359."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1134\/S0361768820080022"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-03077-7_18"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.5281\/ZENODO.5920382"},{"key":"e_1_3_2_1_6_1","volume-title":"Automated Technology for Verification and Analysis, Deepak D'Souza and K","author":"Baranov\u00e1 Zuzana","unstructured":"Zuzana Baranov\u00e1 , Ji\u0159\u00ed Barnat , Katar\u00edna Kejstov\u00e1 , Tade\u00e1\u0161 Ku\u010dera , Henrich Lauko , Jan Mr\u00e1zek , Petr Ro\u010dkai , and Vladim\u00edr \u0160till . 2017. Model Checking of C and C++ with DIVINE 4 . In Automated Technology for Verification and Analysis, Deepak D'Souza and K . Narayan Kumar (Eds.). Springer International Publishing , Cham , 201--207. Zuzana Baranov\u00e1, Ji\u0159\u00ed Barnat, Katar\u00edna Kejstov\u00e1, Tade\u00e1\u0161 Ku\u010dera, Henrich Lauko, Jan Mr\u00e1zek, Petr Ro\u010dkai, and Vladim\u00edr \u0160till. 2017. Model Checking of C and C++ with DIVINE 4. In Automated Technology for Verification and Analysis, Deepak D'Souza and K. Narayan Kumar (Eds.). Springer International Publishing, Cham, 201--207."},{"key":"e_1_3_2_1_7_1","volume-title":"Robert DeLine, Bart Jacobs, and K. Rustan M. Leino.","author":"Barnett Mike","year":"2006","unstructured":"Mike Barnett , Bor-Yuh Evan Chang , Robert DeLine, Bart Jacobs, and K. Rustan M. Leino. 2006 . Boogie : A Modular Reusable Verifier for Object-Oriented Programs. In Formal Methods for Components and Objects, Frank S. de Boer, Marcello M. Bonsangue, Susanne Graf, and Willem-Paul de Roever (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg, 364--387. Mike Barnett, Bor-Yuh Evan Chang, Robert DeLine, Bart Jacobs, and K. Rustan M. Leino. 2006. Boogie: A Modular Reusable Verifier for Object-Oriented Programs. In Formal Methods for Components and Objects, Frank S. de Boer, Marcello M. Bonsangue, Susanne Graf, and Willem-Paul de Roever (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 364--387."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-72013-1_24"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2009.5351147"},{"key":"e_1_3_2_1_10_1","volume-title":"Combining k-Induction with Continuously-Refined Invariants. CoRR abs\/1502.00096","author":"Beyer Dirk","year":"2015","unstructured":"Dirk Beyer , Matthias Dangl , and Philipp Wendler . 2015. Combining k-Induction with Continuously-Refined Invariants. CoRR abs\/1502.00096 ( 2015 ). arXiv:1502.00096 http:\/\/arxiv.org\/abs\/1502.00096 Dirk Beyer, Matthias Dangl, and Philipp Wendler. 2015. Combining k-Induction with Continuously-Refined Invariants. CoRR abs\/1502.00096 (2015). arXiv:1502.00096 http:\/\/arxiv.org\/abs\/1502.00096"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-007-0044-z"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73368-3_51"},{"key":"e_1_3_2_1_13_1","volume-title":"CPAchecker: A Tool for Configurable Software Verification","author":"Beyer Dirk","unstructured":"Dirk Beyer and M. Erkan Keremoglu . 2011. CPAchecker: A Tool for Configurable Software Verification . In Computer Aided Verification, Ganesh Gopalakrishnan and Shaz Qadeer (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg , 184--190. Dirk Beyer and M. Erkan Keremoglu. 2011. CPAchecker: A Tool for Configurable Software Verification. In Computer Aided Verification, Ganesh Gopalakrishnan and Shaz Qadeer (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 184--190."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-017-0469-y"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/s0065-2458(03)58003-2"},{"key":"e_1_3_2_1_16_1","volume-title":"Safety Verification and Refutation by k-Invariants and k-Induction","author":"Brain Martin","unstructured":"Martin Brain , Saurabh Joshi , Daniel Kroening , and Peter Schrammel . 2015. Safety Verification and Refutation by k-Invariants and k-Induction . In Static Analysis, Sandrine Blazy and Thomas Jensen (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg , 145--161. Martin Brain, Saurabh Joshi, Daniel Kroening, and Peter Schrammel. 2015. Safety Verification and Refutation by k-Invariants and k-Induction. In Static Analysis, Sandrine Blazy and Thomas Jensen (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 145--161."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00768-2_16"},{"key":"e_1_3_2_1_18_1","volume-title":"Model Checking Software, Mar\u00eda del Mar Gallardo and Pedro Merino (Eds.)","author":"Chalupa Marek","unstructured":"Marek Chalupa , Jan Strej\u010dek , and Martina Vitovsk\u00e1 . 2018. Joint Forces for Memory Safety Checking . In Model Checking Software, Mar\u00eda del Mar Gallardo and Pedro Merino (Eds.) . Springer International Publishing , Cham , 115--132. Marek Chalupa, Jan Strej\u010dek, and Martina Vitovsk\u00e1. 2018. Joint Forces for Memory Safety Checking. In Model Checking Software, Mar\u00eda del Mar Gallardo and Pedro Merino (Eds.). Springer International Publishing, Cham, 115--132."},{"key":"e_1_3_2_1_19_1","volume-title":"Pinaka: Symbolic Execution Meets Incremental Solving. In Tools and Algorithms for the Construction and Analysis of Systems","author":"Chaudhary Eti","year":"2019","unstructured":"Eti Chaudhary and Saurabh Joshi . 2019 . Pinaka: Symbolic Execution Meets Incremental Solving. In Tools and Algorithms for the Construction and Analysis of Systems , Dirk Beyer, Marieke Huisman, Fabrice Kordon, and Bernhard Steffen (Eds.). Springer International Publishing , Cham , 234--238. Eti Chaudhary and Saurabh Joshi. 2019. Pinaka: Symbolic Execution Meets Incremental Solving. In Tools and Algorithms for the Construction and Analysis of Systems, Dirk Beyer, Marieke Huisman, Fabrice Kordon, and Bernhard Steffen (Eds.). Springer International Publishing, Cham, 234--238."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/876638.876643"},{"key":"e_1_3_2_1_21_1","volume-title":"Model checking","author":"Clarke Edmund M.","unstructured":"Edmund M. Clarke , Orna Grumberg , and Doron Peled . 1999. Model checking . MIT Press . Edmund M. Clarke, Orna Grumberg, and Doron Peled. 1999. Model checking. MIT Press."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1985793.1985839"},{"key":"e_1_3_2_1_23_1","volume-title":"Frama-C","author":"Cuoq Pascal","unstructured":"Pascal Cuoq , Florent Kirchner , Nikolai Kosmatov , Virgile Prevosto , Julien Signoles , and Boris Yakobowski . 2012. Frama-C . In Software Engineering and Formal Methods, George Eleftherakis, Mike Hinchey, and Mike Holcombe (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg , 233--247. Pascal Cuoq, Florent Kirchner, Nikolai Kosmatov, Virgile Prevosto, Julien Signoles, and Boris Yakobowski. 2012. Frama-C. In Software Engineering and Formal Methods, George Eleftherakis, Mike Hinchey, and Mike Holcombe (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 233--247."},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/fmcad.2013.6679414"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-23702-7_26"},{"key":"e_1_3_2_1_26_1","volume-title":"Splitting via Interpolants","author":"Ermis Evren","unstructured":"Evren Ermis , Jochen Hoenicke , and Andreas Podelski . 2012. Splitting via Interpolants . In Verification, Model Checking, and Abstract Interpretation, Viktor Kuncak and Andrey Rybalchenko (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg , 186--201. Evren Ermis, Jochen Hoenicke, and Andreas Podelski. 2012. Splitting via Interpolants. In Verification, Model Checking, and Abstract Interpretation, Viktor Kuncak and Andrey Rybalchenko (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 186--201."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-015-0407-9"},{"key":"e_1_3_2_1_28_1","volume-title":"Florian Furbach, Keijo Heljanko, and Roland Meyer.","author":"Gavrilenko Natalia","year":"2019","unstructured":"Natalia Gavrilenko , Hern\u00e1n Ponce-de Le\u00f3n , Florian Furbach, Keijo Heljanko, and Roland Meyer. 2019 . BMC for Weak Memory Models: Relation Analysis for Compact SMT Encodings. In Computer Aided Verification, Isil Dillig and Serdar Tasiran (Eds.). Springer International Publishing , Cham, 355--365. Natalia Gavrilenko, Hern\u00e1n Ponce-de Le\u00f3n, Florian Furbach, Keijo Heljanko, and Roland Meyer. 2019. BMC for Weak Memory Models: Relation Analysis for Compact SMT Encodings. In Computer Aided Verification, Isil Dillig and Serdar Tasiran (Eds.). Springer International Publishing, Cham, 355--365."},{"key":"e_1_3_2_1_29_1","volume-title":"Loop Invariants from Counterexamples","author":"Greitschus Marius","unstructured":"Marius Greitschus , Daniel Dietsch , and Andreas Podelski . 2017. Loop Invariants from Counterexamples . In Static Analysis, Francesco Ranzato (Ed.). Springer International Publishing , Cham , 128--147. Marius Greitschus, Daniel Dietsch, and Andreas Podelski. 2017. Loop Invariants from Counterexamples. In Static Analysis, Francesco Ranzato (Ed.). Springer International Publishing, Cham, 128--147."},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-019-09535-x"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-019-09535-x"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.infsof.2003.09.016"},{"key":"e_1_3_2_1_33_1","volume-title":"Software Model Checking for People Who Love Automata","author":"Heizmann Matthias","unstructured":"Matthias Heizmann , Jochen Hoenicke , and Andreas Podelski . 2013. Software Model Checking for People Who Love Automata . In Computer Aided Verification, Natasha Sharygina and Helmut Veith (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg , 36--52. Matthias Heizmann, Jochen Hoenicke, and Andreas Podelski. 2013. Software Model Checking for People Who Love Automata. In Computer Aided Verification, Natasha Sharygina and Helmut Veith (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 36--52."},{"key":"e_1_3_2_1_34_1","volume-title":"International Standard","author":"IEC","unstructured":"ISO\/ IEC 9899:201x 2010. Programming languages --- C . International Standard . International Organization for Standardization , International Electrotechnical Commission. ISO\/IEC 9899:201x 2010. Programming languages --- C. International Standard. International Organization for Standardization, International Electrotechnical Commission."},{"key":"e_1_3_2_1_35_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems, Erika \u00c1brah\u00e1m and Klaus Havelund (Eds.)","author":"Kroening Daniel","unstructured":"Daniel Kroening and Michael Tautschnig . 2014. CBMC - C Bounded Model Checker . In Tools and Algorithms for the Construction and Analysis of Systems, Erika \u00c1brah\u00e1m and Klaus Havelund (Eds.) . Springer Berlin Heidelberg, Berlin , Heidelberg , 389--391. Daniel Kroening and Michael Tautschnig. 2014. CBMC - C Bounded Model Checker. In Tools and Algorithms for the Construction and Analysis of Systems, Erika \u00c1brah\u00e1m and Klaus Havelund (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 389--391."},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/CGO.2004.1281665"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993548"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_7"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/73560.73562"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.23919\/FMCAD.2017.8102257"}],"event":{"name":"FormaliSE '22: International Conference on Formal Methods in Software Engineering","location":"Pittsburgh Pennsylvania","acronym":"FormaliSE '22","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering","IEEE CS"]},"container-title":["Proceedings of the IEEE\/ACM 10th International Conference on Formal Methods in Software Engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3524482.3527646","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3524482.3527646","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T17:50:59Z","timestamp":1750182659000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3524482.3527646"}},"subtitle":["comparison of front-end techniques for formal verification"],"short-title":[],"issued":{"date-parts":[[2022,5,18]]},"references-count":40,"alternative-id":["10.1145\/3524482.3527646","10.1145\/3524482"],"URL":"https:\/\/doi.org\/10.1145\/3524482.3527646","relation":{},"subject":[],"published":{"date-parts":[[2022,5,18]]},"assertion":[{"value":"2022-07-21","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}