{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,7]],"date-time":"2026-01-07T07:47:03Z","timestamp":1767772023030,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":74,"publisher":"ACM","license":[{"start":{"date-parts":[[2022,10,23]],"date-time":"2022-10-23T00:00:00Z","timestamp":1666483200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2022,10,23]]},"DOI":"10.1145\/3550355.3552426","type":"proceedings-article","created":{"date-parts":[[2022,10,24]],"date-time":"2022-10-24T22:44:57Z","timestamp":1666651497000},"page":"98-108","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Modelling program verification tools for software engineers"],"prefix":"10.1145","author":[{"given":"Sophie","family":"Lathouwers","sequence":"first","affiliation":[{"name":"University of Twente, Enschede, The Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Vadim","family":"Zaytsev","sequence":"additional","affiliation":[{"name":"University of Twente, Enschede, The Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2022,10,24]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_14"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63387-9_9"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63390-9_1"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96142-2_1"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-72013-1_17"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/11541868_4"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81685-8_42"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17462-0_26"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96142-2_10"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0020949"},{"volume-title":"Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions","author":"Bertot Yves","key":"e_1_3_2_1_11_1","unstructured":"Yves Bertot and Pierre Cast\u00e9ran . 2004. Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions . Springer Berlin , Heidelberg, London . Yves Bertot and Pierre Cast\u00e9ran. 2004. Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions. Springer Berlin, Heidelberg, London."},{"key":"e_1_3_2_1_12_1","volume-title":"Progress on Software Verification: SV-COMP","author":"Beyer Dirk","year":"2022","unstructured":"Dirk Beyer . 2022. Progress on Software Verification: SV-COMP 2022 . In Tools and Algorithms for the Construction and Analysis of Systems, Dana Fisman and Grigore Rosu (Eds.). Springer , Cham, 375--402. Dirk Beyer. 2022. Progress on Software Verification: SV-COMP 2022. In Tools and Algorithms for the Construction and Analysis of Systems, Dana Fisman and Grigore Rosu (Eds.). Springer, Cham, 375--402."},{"volume-title":"CPAchecker: A Tool for Configurable Software Verification","author":"Beyer Dirk","key":"e_1_3_2_1_13_1","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 , 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, 184--190."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-005-0079-4"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/11589976_12"},{"volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Borralleras Cristina","key":"e_1_3_2_1_16_1","unstructured":"Cristina Borralleras , Marc Brockschmidt , Daniel Larraz , Albert Oliveras , Enric Rodr\u00edguez-Carbonell , and Albert Rubio . 2017. Proving Termination Through Conditional Termination . In Tools and Algorithms for the Construction and Analysis of Systems , Axel Legay and Tiziana Margaria (Eds.). Springer , 99--117. Cristina Borralleras, Marc Brockschmidt, Daniel Larraz, Albert Oliveras, Enric Rodr\u00edguez-Carbonell, and Albert Rubio. 2017. Proving Termination Through Conditional Termination. In Tools and Algorithms for the Construction and Analysis of Systems, Axel Legay and Tiziana Margaria (Eds.). Springer, 99--117."},{"volume-title":"MightyL: A Compositional Translation from MITL to Timed Automata","author":"Brihaye Thomas","key":"e_1_3_2_1_17_1","unstructured":"Thomas Brihaye , Gilles Geeraerts , Hsi-Ming Ho , and Benjamin Monmege . 2017. MightyL: A Compositional Translation from MITL to Timed Automata . In Computer Aided Verification, Rupak Majumdar and Viktor Kun\u010dak (Eds.). Springer , 421--440. Thomas Brihaye, Gilles Geeraerts, Hsi-Ming Ho, and Benjamin Monmege. 2017. MightyL: A Compositional Translation from MITL to Timed Automata. In Computer Aided Verification, Rupak Majumdar and Viktor Kun\u010dak (Eds.). Springer, 421--440."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/APSEC.2003.1254357"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/MS.2020.3041522"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/SCAM.2009.22"},{"volume-title":"Tools and Algorithms for the Construction and Analysis of Systems, Marsha Chechik and Jean-Fran\u00e7ois Raskin (Eds.)","author":"Chen Zhe","key":"e_1_3_2_1_21_1","unstructured":"Zhe Chen , Zhemin Wang , Yunlong Zhu , Hongwei Xi , and Zhibin Yang . 2016. Parametric Runtime Verification of C Programs . In Tools and Algorithms for the Construction and Analysis of Systems, Marsha Chechik and Jean-Fran\u00e7ois Raskin (Eds.) . Springer , 299--315. Zhe Chen, Zhemin Wang, Yunlong Zhu, Hongwei Xi, and Zhibin Yang. 2016. Parametric Runtime Verification of C Programs. In Tools and Algorithms for the Construction and Analysis of Systems, Marsha Chechik and Jean-Fran\u00e7ois Raskin (Eds.). Springer, 299--315."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-41010-9_5"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0_17"},{"volume-title":"Permission Inference for Array Programs","author":"Dohrau J\u00e9r\u00f4me","key":"e_1_3_2_1_25_1","unstructured":"J\u00e9r\u00f4me Dohrau , Alexander J. Summers , Caterina Urban , Severin M\u00fcnger , and Peter M\u00fcller . 2018. Permission Inference for Array Programs . In Computer Aided Verification, Hana Chockler and Georg Weissenbacher (Eds.). Springer , 55--74. J\u00e9r\u00f4me Dohrau, Alexander J. Summers, Caterina Urban, Severin M\u00fcnger, and Peter M\u00fcller. 2018. Permission Inference for Array Programs. In Computer Aided Verification, Hana Chockler and Georg Weissenbacher (Eds.). Springer, 55--74."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25540-4_15"},{"volume-title":"SecCSL: Security Concurrent Separation Logic","author":"Ernst Gidon","key":"e_1_3_2_1_27_1","unstructured":"Gidon Ernst and Toby Murray . 2019. SecCSL: Security Concurrent Separation Logic . In Computer Aided Verification, Isil Dillig and Serdar Tasiran (Eds.). Springer , 208--230. Gidon Ernst and Toby Murray. 2019. SecCSL: Security Concurrent Separation Logic. In Computer Aided Verification, Isil Dillig and Serdar Tasiran (Eds.). Springer, 208--230."},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49674-9_34"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-021-00609-z"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3377811.3380373"},{"key":"e_1_3_2_1_31_1","volume-title":"Language Workbenches: The Killer-App for Domain Specific Languages? MartinFowler.com. https:\/\/martinfowler.com\/articles\/languageWorkbench.html","author":"Fowler Martin","year":"2005","unstructured":"Martin Fowler . 2005 . Language Workbenches: The Killer-App for Domain Specific Languages? MartinFowler.com. https:\/\/martinfowler.com\/articles\/languageWorkbench.html Martin Fowler. 2005. Language Workbenches: The Killer-App for Domain Specific Languages? MartinFowler.com. https:\/\/martinfowler.com\/articles\/languageWorkbench.html"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSMC.2000.884356"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/22145.22178"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53291-8_16"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25543-5_28"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17462-0_20"},{"key":"e_1_3_2_1_37_1","volume-title":"Knottenbelt","author":"Harz Dominik","year":"2018","unstructured":"Dominik Harz and William J . Knottenbelt . 2018 . Towards Safer Smart Contracts: A Survey of Languages and Verification Methods. CoRR abs\/1809.09805 (2018), 20 pages. arXiv:1809.09805 http:\/\/arxiv.org\/abs\/1809.09805 Dominik Harz and William J. Knottenbelt. 2018. Towards Safer Smart Contracts: A Survey of Languages and Verification Methods. CoRR abs\/1809.09805 (2018), 20 pages. arXiv:1809.09805 http:\/\/arxiv.org\/abs\/1809.09805"},{"volume-title":"MaxSMT-Based Type Inference for Python 3","author":"Hassan Mostafa","key":"e_1_3_2_1_38_1","unstructured":"Mostafa Hassan , Caterina Urban , Marco Eilers , and Peter M\u00fcller . 2018. MaxSMT-Based Type Inference for Python 3 . In Computer Aided Verification, Hana Chockler and Georg Weissenbacher (Eds.). Springer , 12--19. Mostafa Hassan, Caterina Urban, Marco Eilers, and Peter M\u00fcller. 2018. MaxSMT-Based Type Inference for Python 3. In Computer Aided Verification, Hana Chockler and Georg Weissenbacher (Eds.). Springer, 12--19."},{"key":"e_1_3_2_1_39_1","volume-title":"Forester: From Heap Shapes to Automata Predicates. In Tools and Algorithms for the Construction and Analysis of Systems","author":"Hol\u00edk Luk\u00e1\u0161","year":"2017","unstructured":"Luk\u00e1\u0161 Hol\u00edk , Martin Hru\u0161ka , Ond\u0159ej Leng\u00e1l , Adam Rogalewicz , Ji\u0159\u00ed \u0160im\u00e1\u010dek , and Tom\u00e1\u0161 Vojnar . 2017 . Forester: From Heap Shapes to Automata Predicates. In Tools and Algorithms for the Construction and Analysis of Systems , Axel Legay and Tiziana Margaria (Eds.). Springer , 365--369. Luk\u00e1\u0161 Hol\u00edk, Martin Hru\u0161ka, Ond\u0159ej Leng\u00e1l, Adam Rogalewicz, Ji\u0159\u00ed \u0160im\u00e1\u010dek, and Tom\u00e1\u0161 Vojnar. 2017. Forester: From Heap Shapes to Automata Predicates. In Tools and Algorithms for the Construction and Analysis of Systems, Axel Legay and Tiziana Margaria (Eds.). Springer, 365--369."},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2013.03.017"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49674-9_33"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSM.1999.792600"},{"volume-title":"TarTar: A Timed Automata Repair Tool","author":"K\u00f6lbl Martin","key":"e_1_3_2_1_43_1","unstructured":"Martin K\u00f6lbl , Stefan Leue , and Thomas Wies . 2020. TarTar: A Timed Automata Repair Tool . In Computer Aided Verification, Shuvendu K. Lahiri and Chao Wang (Eds.). Springer , 529--540. Martin K\u00f6lbl, Stefan Leue, and Thomas Wies. 2020. TarTar: A Timed Automata Repair Tool. In Computer Aided Verification, Shuvendu K. Lahiri and Chao Wang (Eds.). Springer, 529--540."},{"volume-title":"First-Order Theorem Proving and Vampire","author":"Kov\u00e1cs Laura","key":"e_1_3_2_1_44_1","unstructured":"Laura Kov\u00e1cs and Andrei Voronkov . 2013. First-Order Theorem Proving and Vampire . In Computer Aided Verification, Natasha Sharygina and Helmut Veith (Eds.). Springer , 1--35. Laura Kov\u00e1cs and Andrei Voronkov. 2013. First-Order Theorem Proving and Vampire. In Computer Aided Verification, Natasha Sharygina and Helmut Veith (Eds.). Springer, 1--35."},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/177492.177726"},{"key":"e_1_3_2_1_46_1","volume-title":"Rozier","author":"Li Jianwen","year":"2019","unstructured":"Jianwen Li , Moshe Y. Vardi , and Kristin Y . Rozier . 2019 . Satisfiability Checking for Mission-Time LTL. In Computer Aided Verification, Isil Dillig and Serdar Tasiran (Eds.). Springer , 3--22. Jianwen Li, Moshe Y. Vardi, and Kristin Y. Rozier. 2019. Satisfiability Checking for Mission-Time LTL. In Computer Aided Verification, Isil Dillig and Serdar Tasiran (Eds.). Springer, 3--22."},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-80223-3_26"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10617-012-9096-8"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-79876-5_37"},{"volume-title":"SymDIVINE: Tool for Control-Explicit Data-Symbolic State Space Exploration","author":"Mr\u00e1zek Jan","key":"e_1_3_2_1_50_1","unstructured":"Jan Mr\u00e1zek , Petr Bauch , Henrich Lauko , and Ji\u0159\u00ed Barnat . 2016. SymDIVINE: Tool for Control-Explicit Data-Symbolic State Space Exploration . In Model Checking Software, Dragan Bo\u0161na\u010dki and Anton Wijs (Eds.). Springer , 208--213. Jan Mr\u00e1zek, Petr Bauch, Henrich Lauko, and Ji\u0159\u00ed Barnat. 2016. SymDIVINE: Tool for Control-Explicit Data-Symbolic State Space Exploration. In Model Checking Software, Dragan Bo\u0161na\u010dki and Anton Wijs (Eds.). Springer, 208--213."},{"key":"e_1_3_2_1_51_1","volume-title":"STAMINA: STochastic Approximate Model-Checker for INfinite-State Analysis","author":"Neupane Thakur","year":"2019","unstructured":"Thakur Neupane , Chris J. Myers , Curtis Madsen , Hao Zheng , and Zhen Zhang . 2019 . STAMINA: STochastic Approximate Model-Checker for INfinite-State Analysis . In Computer Aided Verification, Isil Dillig and Serdar Tasiran (Eds.). Springer , 540--549. Thakur Neupane, Chris J. Myers, Curtis Madsen, Hao Zheng, and Zhen Zhang. 2019. STAMINA: STochastic Approximate Model-Checker for INfinite-State Analysis. In Computer Aided Verification, Isil Dillig and Serdar Tasiran (Eds.). Springer, 540--549."},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9_5"},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/3475716.3475770"},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.infsof.2021.106731"},{"key":"e_1_3_2_1_55_1","unstructured":"T. Parr. 2013. The Definitive ANTLR 4 Reference. Pragmatic Bookshelf. https:\/\/books.google.nl\/books?id=gA9QDwAAQBAJ  T. Parr. 2013. The Definitive ANTLR 4 Reference. Pragmatic Bookshelf. https:\/\/books.google.nl\/books?id=gA9QDwAAQBAJ"},{"key":"e_1_3_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81688-9_16"},{"key":"e_1_3_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Richter Cedric","key":"e_1_3_2_1_59_1","unstructured":"Cedric Richter and Heike Wehrheim . 2019. PeSCo: Predicting Sequential Combinations of Verifiers . In Tools and Algorithms for the Construction and Analysis of Systems , Dirk Beyer, Marieke Huisman, Fabrice Kordon, and Bernhard Steffen (Eds.). Springer , 229--233. Cedric Richter and Heike Wehrheim. 2019. PeSCo: Predicting Sequential Combinations of Verifiers. In Tools and Algorithms for the Construction and Analysis of Systems, Dirk Beyer, Marieke Huisman, Fabrice Kordon, and Bernhard Steffen (Eds.). Springer, 229--233."},{"volume-title":"Must Fault Localization for Program Repair","author":"Rothenberg Bat-Chen","key":"e_1_3_2_1_60_1","unstructured":"Bat-Chen Rothenberg and Orna Grumberg . 2020. Must Fault Localization for Program Repair . In Computer Aided Verification, Shuvendu K. Lahiri and Chao Wang (Eds.). Springer , 658--680. Bat-Chen Rothenberg and Orna Grumberg. 2020. Must Fault Localization for Program Repair. In Computer Aided Verification, Shuvendu K. Lahiri and Chao Wang (Eds.). Springer, 658--680."},{"key":"e_1_3_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81685-8_10"},{"key":"e_1_3_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-03427-6_20"},{"key":"e_1_3_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/3366030.3366070"},{"key":"e_1_3_2_1_64_1","unstructured":"Aleksey Shipil\u00ebv. 2013. Java Concurrency Stress (jcstress). https:\/\/github.com\/openjdk\/jcstress\/.  Aleksey Shipil\u00ebv. 2013. Java Concurrency Stress (jcstress). https:\/\/github.com\/openjdk\/jcstress\/."},{"key":"e_1_3_2_1_65_1","doi-asserted-by":"crossref","unstructured":"Herbert Stachowiak. 1973. Allgemeine Modelltheorie. Springer.  Herbert Stachowiak. 1973. Allgemeine Modelltheorie. Springer.","DOI":"10.1007\/978-3-7091-8327-4"},{"key":"e_1_3_2_1_66_1","volume-title":"Salvatore La Torre, and Gennaro Parlato","author":"Tomasco Ermenegildo","year":"2016","unstructured":"Ermenegildo Tomasco , Truc L. Nguyen , Omar Inverso , Bernd Fischer , Salvatore La Torre, and Gennaro Parlato . 2016 . MU-CSeq 0.4: Individual Memory Location Unwindings. In Tools and Algorithms for the Construction and Analysis of Systems, Marsha Chechik and Jean-Fran\u00e7ois Raskin (Eds.). Springer , 938--941. Ermenegildo Tomasco, Truc L. Nguyen, Omar Inverso, Bernd Fischer, Salvatore La Torre, and Gennaro Parlato. 2016. MU-CSeq 0.4: Individual Memory Location Unwindings. In Tools and Algorithms for the Construction and Analysis of Systems, Marsha Chechik and Jean-Fran\u00e7ois Raskin (Eds.). Springer, 938--941."},{"key":"e_1_3_2_1_67_1","volume-title":"Reflections on the Lack of Adoption of Domain Specific Languages. In STAF Workshop Proceedings (STAF) (CEUR Workshop Proceedings","volume":"94","author":"Tomassetti Federico","year":"2020","unstructured":"Federico Tomassetti and Vadim Zaytsev . 2020 . Reflections on the Lack of Adoption of Domain Specific Languages. In STAF Workshop Proceedings (STAF) (CEUR Workshop Proceedings , Vol. 2707), Loli Burgue\u00f1o and Lars Michael Kristensen (Eds.). CEUR-WS.org, 85-- 94 . http:\/\/ceur-ws.org\/Vol-2707\/oopslepaper5.pdf Federico Tomassetti and Vadim Zaytsev. 2020. Reflections on the Lack of Adoption of Domain Specific Languages. In STAF Workshop Proceedings (STAF) (CEUR Workshop Proceedings, Vol. 2707), Loli Burgue\u00f1o and Lars Michael Kristensen (Eds.). CEUR-WS.org, 85--94. http:\/\/ceur-ws.org\/Vol-2707\/oopslepaper5.pdf"},{"key":"e_1_3_2_1_68_1","volume-title":"P\u0103s\u0103reanu","author":"Usman Muhammad","year":"2021","unstructured":"Muhammad Usman , Divya Gopinath , Youcheng Sun , Yannic Noller , and Corina S . P\u0103s\u0103reanu . 2021 . NNrepair: Constraint- Based Repair of Neural Network Classifiers. In Computer Aided Verification, Alexandra Silva and K. Rustan M. Leino (Eds.). Springer , 3--25. Muhammad Usman, Divya Gopinath, Youcheng Sun, Yannic Noller, and Corina S. P\u0103s\u0103reanu. 2021. NNrepair: Constraint-Based Repair of Neural Network Classifiers. In Computer Aided Verification, Alexandra Silva and K. Rustan M. Leino (Eds.). Springer, 3--25."},{"key":"e_1_3_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89960-2_16"},{"key":"e_1_3_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.1109\/MS.2019.2956701"},{"key":"e_1_3_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36469-2_15"},{"volume-title":"Mathematics and Computation: Ideas Revolutionizing Technology and Science","author":"Wigderson Avi","key":"e_1_3_2_1_72_1","unstructured":"Avi Wigderson . 2019. Mathematics and Computation: Ideas Revolutionizing Technology and Science . Princeton University Press . https:\/\/www.math.ias.edu\/avi\/book Avi Wigderson. 2019. Mathematics and Computation: Ideas Revolutionizing Technology and Science. Princeton University Press. https:\/\/www.math.ias.edu\/avi\/book"},{"key":"e_1_3_2_1_73_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81685-8_17"},{"key":"e_1_3_2_1_74_1","doi-asserted-by":"publisher","DOI":"10.1145\/1592434.1592436"},{"key":"e_1_3_2_1_75_1","doi-asserted-by":"publisher","DOI":"10.1613\/jair.2490"}],"event":{"name":"MODELS '22: ACM\/IEEE 25th International Conference on Model Driven Engineering Languages and Systems","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering","Univ. of Montreal University of Montreal","IEEE CS"],"location":"Montreal Quebec Canada","acronym":"MODELS '22"},"container-title":["Proceedings of the 25th International Conference on Model Driven Engineering Languages and Systems"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3550355.3552426","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3550355.3552426","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T18:08:07Z","timestamp":1750183687000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3550355.3552426"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,10,23]]},"references-count":74,"alternative-id":["10.1145\/3550355.3552426","10.1145\/3550355"],"URL":"https:\/\/doi.org\/10.1145\/3550355.3552426","relation":{},"subject":[],"published":{"date-parts":[[2022,10,23]]},"assertion":[{"value":"2022-10-24","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}