{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,30]],"date-time":"2025-08-30T16:48:51Z","timestamp":1756572531623,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":77,"publisher":"ACM","license":[{"start":{"date-parts":[[2020,12,21]],"date-time":"2020-12-21T00:00:00Z","timestamp":1608508800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"EPSRC","award":["EP\/N023978\/2"],"award-info":[{"award-number":["EP\/N023978\/2"]}]},{"name":"DFG","award":["FR 2955\/3-1"],"award-info":[{"award-number":["FR 2955\/3-1"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2020,12,21]]},"DOI":"10.1145\/3324884.3416554","type":"proceedings-article","created":{"date-parts":[[2021,1,27]],"date-time":"2021-01-27T23:38:56Z","timestamp":1611790736000},"page":"150-162","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["Verified from scratch"],"prefix":"10.1145","author":[{"given":"Andreas","family":"Stahlbauer","sequence":"first","affiliation":[{"name":"University of Passau, Germany"}]},{"given":"Christoph","family":"Fr\u00e4drich","sequence":"additional","affiliation":[{"name":"University of Passau, Germany"}]},{"given":"Gordon","family":"Fraser","sequence":"additional","affiliation":[{"name":"University of Passau, Germany"}]}],"member":"320","published-online":{"date-parts":[[2021,1,27]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Plotkin","author":"Abadi Mart\u00edn","year":"2010","unstructured":"Mart\u00edn Abadi and Gordon D. Plotkin. 2010. A Model of Cooperative Threads. Log. Methods Comput. Sci. 6, 4 (2010)."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-16042-6_2"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2960310.2960325"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"crossref","unstructured":"Sven Apel Dirk Beyer Vitaly O. Mordan Vadim S. Mutilin and Andreas Stahlbauer. 2016. On-the-fly decomposition of specifications in software model checking. In SIGSOFT FSE. ACM 349--361.","DOI":"10.1145\/2950290.2950349"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/278283.278285"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36135-9_16"},{"key":"e_1_3_2_1_7_1","volume-title":"Rajamani","author":"Ball Thomas","year":"2001","unstructured":"Thomas Ball and Sriram K. Rajamani. 2001. The SLAM Toolkit. In CAV (Lecture Notes in Computer Science, Vol. 2102). Springer, 260--264."},{"volume-title":"Verification of Distributed Embedded Real-Time Systems and their Low-Level Implementations Using Timed CSP","author":"Bartels Bj\u00f6rn","key":"e_1_3_2_1_8_1","unstructured":"Bj\u00f6rn Bartels and Sabine Glesner. 2011. Verification of Distributed Embedded Real-Time Systems and their Low-Level Implementations Using Timed CSP. In APSEC. IEEE Computer Society, 195--202."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2771839.2771875"},{"volume-title":"Generating Tests from Counterexamples","author":"Beyer Dirk","key":"e_1_3_2_1_10_1","unstructured":"Dirk Beyer, Adam Chlipala, Thomas A. Henzinger, Ranjit Jhala, and Rupak Majumdar. 2004. Generating Tests from Counterexamples. In ICSE. IEEE Computer Society, 326--335."},{"key":"e_1_3_2_1_11_1","volume-title":"Software Model Checking via Large-Block Encoding. CoRR abs\/0904.4709","author":"Beyer Dirk","year":"2009","unstructured":"Dirk Beyer, Alessandro Cimatti, Alberto Griggio, M. Erkan Keremoglu, and Roberto Sebastiani. 2009. Software Model Checking via Large-Block Encoding. CoRR abs\/0904.4709 (2009)."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8_16"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73368-3_51"},{"key":"e_1_3_2_1_14_1","volume-title":"CPAchecker: A Tool for Configurable Software Verification. CoRR abs\/0902.0019","author":"Beyer Dirk","year":"2009","unstructured":"Dirk Beyer and M. Erkan Keremoglu. 2009. CPAchecker: A Tool for Configurable Software Verification. CoRR abs\/0902.0019 (2009)."},{"volume-title":"Mathematical proceedings of the Cambridge philosophical society","author":"Birkhoff Garrett","key":"e_1_3_2_1_15_1","unstructured":"Garrett Birkhoff. 1935. On the structure of abstract algebras. In Mathematical proceedings of the Cambridge philosophical society, Vol. 31. Cambridge University Press, 433--454."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2445196.2445265"},{"key":"e_1_3_2_1_17_1","volume-title":"IF: An Intermediate Representation and Validation Environment for Timed Asynchronous Systems. In World Congress on Formal Methods (Lecture Notes in Computer Science","volume":"327","author":"Bozga Marius","year":"1999","unstructured":"Marius Bozga, Jean-Claude Fernandez, Lucian Ghirvu, Susanne Graf, Jean-Pierre Krimm, and Laurent Mounier. 1999. IF: An Intermediate Representation and Validation Environment for Timed Asynchronous Systems. In World Congress on Formal Methods (Lecture Notes in Computer Science, Vol. 1708). Springer, 307--327."},{"key":"e_1_3_2_1_18_1","volume-title":"Brat and Willem Visser","author":"Guillaume","year":"2001","unstructured":"Guillaume P. Brat and Willem Visser. 2001. Combining Static Analysis and Model Checking for Software Analysis. In ASE. IEEE Computer Society, 262."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/IWCMC.2018.8450296"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1011276507260"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/10722167_15"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/186025.186051"},{"volume-title":"Journal of computing sciences in colleges","author":"Cooper Stephen","key":"e_1_3_2_1_23_1","unstructured":"Stephen Cooper, Wanda Dann, Randy Pausch, and Randy Pausch. 2000. Alice: a 3-D tool for introductory programming concepts. In Journal of computing sciences in colleges, Vol. 15. Consortium for Computing Sciences in Colleges, 107--116."},{"volume-title":"Verification: Theory and Practice","author":"Cousot P.","key":"e_1_3_2_1_24_1","unstructured":"P. Cousot. 2003. Verification by abstract interpretation. In Verification: Theory and Practice. Springer, 243--268."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/2.4.511"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-19805-2_31"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/360933.360975"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2670757.2670774"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1080\/10494820903520040"},{"key":"e_1_3_2_1_30_1","volume-title":"Heitmeyer","author":"Gargantini Angelo","year":"1999","unstructured":"Angelo Gargantini and Constance L. Heitmeyer. 1999. Using Model Checking to Generate Tests from Requirements Specifications. In ESEC \/ SIGSOFT FSE (Lecture Notes in Computer Science, Vol. 1687). Springer, 146--162."},{"key":"e_1_3_2_1_31_1","volume-title":"ISSEP","author":"Geldreich Katharina","year":"2016","unstructured":"Katharina Geldreich, Alexandra Funke, and Peter Hubwieser. 2016. A programming circus for primary schools. In ISSEP 2016. 49--50."},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2325296.2325346"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-63166-6_10"},{"volume-title":"Proc. PLDI. ACM, 376--386","author":"Gulwani S.","key":"e_1_3_2_1_34_1","unstructured":"S. Gulwani and A. Tiwari. 2006. Combining abstract interpreters. In Proc. PLDI. ACM, 376--386."},{"volume-title":"Proceeding of the 44th ACM technical symposium on Computer science education. 759--759.","author":"Harvey Brian","key":"e_1_3_2_1_35_1","unstructured":"Brian Harvey, Daniel D Garcia, Tiffany Barnes, Nathaniel Titterton, Daniel Armendariz, Luke Segars, Eugene Lemon, Sean Morris, and Josh Paley. 2013. Snap!(build your own blocks). In Proceeding of the 44th ACM technical symposium on Computer science education. 759--759."},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"crossref","unstructured":"Sarah Smith Heckman and Laurie Williams. 2008. On establishing a benchmark for evaluating static analysis alert prioritization and classification techniques. In ESEM. ACM 41--50.","DOI":"10.1145\/1414004.1414013"},{"key":"e_1_3_2_1_37_1","volume-title":"Plotkin","author":"Hennessy Matthew","year":"1979","unstructured":"Matthew Hennessy and Gordon D. Plotkin. 1979. Full Abstraction for a Simple Parallel Programming Language. In MFCS (Lecture Notes in Computer Science, Vol. 74). Springer, 108--120."},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICPC.2016.7503706"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1109\/VLHCC.2016.7739666"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/10722468_8"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/1592434.1592438"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/2839509.2844600"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/1089733.1089734"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-55092-5_32"},{"key":"e_1_3_2_1_45_1","volume-title":"Tom Van Cutsem, and Wolfgang De Meuter","author":"Koster Joeri De","year":"2016","unstructured":"Joeri De Koster, Tom Van Cutsem, and Wolfgang De Meuter. 2016. 43 years of actors: a taxonomy of actor models and their key properties. In AGERE!@SPLASH. ACM, 31--40."},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/1868358.1868363"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/1868358.1868363"},{"key":"e_1_3_2_1_48_1","volume-title":"GRAIL: A Zeroth Programming Language. In Advanced Research in Computers and Communications in Education New Human Abilities for the Networked Society","author":"McIver Linda","year":"1999","unstructured":"Linda McIver and Damian M Conway. 1999. GRAIL: A Zeroth Programming Language. In Advanced Research in Computers and Communications in Education New Human Abilities for the Networked Society. IOS Press, Netherlands, 43 -- 50."},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/1999747.1999796"},{"key":"e_1_3_2_1_50_1","series-title":"Lecture Notes in Computer Science","volume-title":"A Calculus of Communicating Systems","author":"Milner Robin","unstructured":"Robin Milner. 1980. A Calculus of Communicating Systems. Lecture Notes in Computer Science, Vol. 92. Springer."},{"key":"e_1_3_2_1_51_1","volume-title":"Symbolic Methods to Enhance the Precision of Numerical Abstract Domains. CoRR abs\/cs\/0703076","author":"Min\u00e9 Antoine","year":"2007","unstructured":"Antoine Min\u00e9. 2007. Symbolic Methods to Enhance the Precision of Numerical Abstract Domains. CoRR abs\/cs\/0703076 (2007)."},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/2818314.2818338"},{"key":"e_1_3_2_1_53_1","volume-title":"Shree Prakash Rahul, and Westley Weimer","author":"Necula George C.","year":"2002","unstructured":"George C. Necula, Scott McPeak, Shree Prakash Rahul, and Westley Weimer. 2002. CIL: Intermediate Language and Tools for Analysis and Transformation of C Programs. In CC (Lecture Notes in Computer Science, Vol. 2304). Springer, 213--228."},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1002\/spe.4380250705"},{"key":"e_1_3_2_1_55_1","volume-title":"A structural approach to operational semantics. J. Log. Algebr. Program. 60--61","author":"Plotkin Gordon D.","year":"2004","unstructured":"Gordon D. Plotkin. 2004. A structural approach to operational semantics. J. Log. Algebr. Program. 60--61 (2004), 17--139."},{"key":"e_1_3_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69850-0_11"},{"key":"e_1_3_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/3017680.3017762"},{"key":"e_1_3_2_1_58_1","volume-title":"A survey on visual programming languages in internet of things. Scientific Programming 2017","author":"Ray Partha Pratim","year":"2017","unstructured":"Partha Pratim Ray. 2017. A survey on visual programming languages in internet of things. Scientific Programming 2017 (2017)."},{"key":"e_1_3_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0950-5849(98)00093-7"},{"key":"e_1_3_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9947-1953-0053041-6"},{"key":"e_1_3_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1109\/IWSC.2017.7880506"},{"volume-title":"Global Value Numbers and Redundant Computations","author":"Rosen Barry K.","key":"e_1_3_2_1_62_1","unstructured":"Barry K. Rosen, Mark N. Wegman, and F. Kenneth Zadeck. 1988. Global Value Numbers and Redundant Computations. In POPL. ACM Press, 12--27."},{"key":"e_1_3_2_1_63_1","unstructured":"Koushik Sen. 2007. Concolic testing. In ASE. ACM 571--572."},{"key":"e_1_3_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)80523-1"},{"key":"e_1_3_2_1_65_1","doi-asserted-by":"crossref","unstructured":"Andreas Stahlbauer Marvin Kreis and Gordon Fraser. 2019. Testing scratch programs automatically. In ESEC\/SIGSOFT FSE. ACM 165--175.","DOI":"10.1145\/3338906.3338910"},{"key":"e_1_3_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-54415-1_54"},{"key":"e_1_3_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1145\/2534973"},{"key":"e_1_3_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0020-0190(02)00286-7"},{"key":"e_1_3_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1109\/VLHCC.2017.8103498"},{"key":"e_1_3_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.1109\/VLHCC.2017.8103449"},{"key":"e_1_3_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.1109\/VLHCC.2019.8818950"},{"key":"e_1_3_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676723.2691871"},{"key":"e_1_3_2_1_73_1","doi-asserted-by":"publisher","DOI":"10.15388\/infedu.2018.08"},{"key":"e_1_3_2_1_74_1","doi-asserted-by":"publisher","DOI":"10.1109\/BLOCKS.2017.8120406"},{"key":"e_1_3_2_1_75_1","doi-asserted-by":"publisher","DOI":"10.1145\/2771839.2771860"},{"key":"e_1_3_2_1_76_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00264291"},{"volume-title":"Software Pioneers","author":"Wirth Niklaus","key":"e_1_3_2_1_77_1","unstructured":"Niklaus Wirth. 2002. Pascal and Its Successors. In Software Pioneers. Springer Berlin Heidelberg, 108--119."}],"event":{"name":"ASE '20: 35th IEEE\/ACM International Conference on Automated Software Engineering","sponsor":["SIGAI ACM Special Interest Group on Artificial Intelligence","SIGSOFT ACM Special Interest Group on Software Engineering","IEEE CS"],"location":"Virtual Event Australia","acronym":"ASE '20"},"container-title":["Proceedings of the 35th IEEE\/ACM International Conference on Automated Software Engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3324884.3416554","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3324884.3416554","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:01:37Z","timestamp":1750197697000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3324884.3416554"}},"subtitle":["program analysis for learners' programs"],"short-title":[],"issued":{"date-parts":[[2020,12,21]]},"references-count":77,"alternative-id":["10.1145\/3324884.3416554","10.1145\/3324884"],"URL":"https:\/\/doi.org\/10.1145\/3324884.3416554","relation":{},"subject":[],"published":{"date-parts":[[2020,12,21]]},"assertion":[{"value":"2021-01-27","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}