{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,30]],"date-time":"2026-01-30T00:18:11Z","timestamp":1769732291305,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":73,"publisher":"ACM","license":[{"start":{"date-parts":[[2024,10,17]],"date-time":"2024-10-17T00:00:00Z","timestamp":1729123200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nd\/4.0\/"}],"funder":[{"name":"NSF (National Science Foundation)","award":["1844964,2220991"],"award-info":[{"award-number":["1844964,2220991"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2024,10,17]]},"DOI":"10.1145\/3689493.3689980","type":"proceedings-article","created":{"date-parts":[[2024,10,17]],"date-time":"2024-10-17T09:12:11Z","timestamp":1729156331000},"page":"98-109","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Mocking Temporal Logic"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9012-4490","authenticated-orcid":false,"given":"Colin S.","family":"Gordon","sequence":"first","affiliation":[{"name":"Drexel University, Philadelphia, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,10,17]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"2017. OMG Unified Modeling Language (OMG UML). https:\/\/www.omg.org\/spec\/UML\/2.5.1\/PDF Version 2.5.1"},{"key":"e_1_3_2_1_2_1","volume-title":"Defining liveness. Information processing letters, 21, 4","author":"Alpern Bowen","year":"1985","unstructured":"Bowen Alpern and Fred B Schneider. 1985. Defining liveness. Information processing letters, 21, 4 (1985), 181\u2013185."},{"key":"e_1_3_2_1_3_1","volume-title":"Hanne Riis Nielson, and Flemming Nielson","author":"Amtoft Torben","year":"1999","unstructured":"Torben Amtoft, Hanne Riis Nielson, and Flemming Nielson. 1999. Type and effect systems: behaviours for concurrency. World Scientific."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1561\/9781680831351"},{"key":"e_1_3_2_1_5_1","volume-title":"Effective Software Testing: A developer\u2019s guide","author":"Aniche Maur\u00edcio","unstructured":"Maur\u00edcio Aniche. 2022. Effective Software Testing: A developer\u2019s guide. Manning Publications."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2015.345"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSTW.2015.7107466"},{"key":"e_1_3_2_1_8_1","volume-title":"Principles of model checking","author":"Baier Christel","unstructured":"Christel Baier and Joost-Pieter Katoen. 2008. Principles of model checking. MIT press."},{"key":"e_1_3_2_1_9_1","unstructured":"Mordechai Ben-Ari. 2006. Principles of concurrent and distributed programming. Pearson Education."},{"key":"e_1_3_2_1_10_1","volume-title":"Mathematical logic for computer science","author":"Ben-Ari Mordechai","unstructured":"Mordechai Ben-Ari. 2012. Mathematical logic for computer science. Springer Science & Business Media."},{"key":"e_1_3_2_1_11_1","volume-title":"Testing object-oriented systems: models, patterns, and tools","author":"Binder Robert","unstructured":"Robert Binder. 2000. Testing object-oriented systems: models, patterns, and tools. Addison-Wesley Professional."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"crossref","unstructured":"J. Richard B\u00fcchi. 1960. Weak Second Order Arithmetic and Finite Automata. Zeitschrift f\u00fcr Math. Log. und Grundl. der Math..","DOI":"10.1002\/malq.19600060105"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.2514\/6.1993-4516"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3550355.3552408"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/351240.351266"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/581690.581696"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/5397.5399"},{"key":"e_1_3_2_1_18_1","volume-title":"Handbook of model checking. 10","author":"Clarke Edmund M","unstructured":"Edmund M Clarke, Thomas A Henzinger, Helmut Veith, and Roderick Bloem. 2018. Handbook of model checking. 10, Springer."},{"key":"e_1_3_2_1_19_1","volume-title":"Foregrounding and temporal relations in narrative discourse. Essays on tensing in English, 2","author":"Couper-Kuhlen Elizabeth","year":"1989","unstructured":"Elizabeth Couper-Kuhlen. 1989. Foregrounding and temporal relations in narrative discourse. Essays on tensing in English, 2 (1989), 7\u201329."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2716316"},{"key":"e_1_3_2_1_21_1","volume-title":"Teaching and assessment of mathematical principles for software correctness using a reasoning concept inventory. Ph. D. Dissertation","author":"Drachova-Strang Svetlana","unstructured":"Svetlana Drachova-Strang. 2013. Teaching and assessment of mathematical principles for software correctness using a reasoning concept inventory. Ph. D. Dissertation. Clemson University. http:\/\/tigerprints.clemson.edu\/all_dissertations\/1095\/"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/302405.302672"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/4904.4999"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.485225"},{"key":"e_1_3_2_1_25_1","volume-title":"Teaching and Learning Formal Methods","author":"Finney Kate M","unstructured":"Kate M Finney and Alex M Fedorec. 1996. An empirical study of specification readability. In Teaching and Learning Formal Methods. Academic Press."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.5555\/519308.786905"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3597503.3639581"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3622758.3622890"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"crossref","unstructured":"Ben Greenman Sam Saarinen Tim Nelson and Shriram Krishnamurthi. 2023. Little Tricky Logic: Misconceptions in the Understanding of LTL. The Art Science and Engineering of Programming.","DOI":"10.22152\/programming-journal.org\/2023\/7\/7"},{"key":"e_1_3_2_1_30_1","volume-title":"Modeling and analysis of communicating systems","author":"Groote Jan Friso","unstructured":"Jan Friso Groote and Mohammad Reza Mousavi. 2014. Modeling and analysis of communicating systems. MIT press."},{"key":"e_1_3_2_1_31_1","volume-title":"25 years of model checking: history, achievements, perspectives. 5000","author":"Grumberg Orna","unstructured":"Orna Grumberg and Helmut Veith. 2008. 25 years of model checking: history, achievements, perspectives. 5000, Springer."},{"key":"e_1_3_2_1_32_1","volume-title":"Second NASA Formal Methods Symposium. 8, 179\u2013195","author":"Harrison John","year":"2010","unstructured":"John Harrison. 2010. Formal methods at Intel\u2014An overview. In Second NASA Formal Methods Symposium. 8, 179\u2013195."},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICST.2016.37"},{"key":"e_1_3_2_1_34_1","volume-title":"Logic in Computer Science: Modelling and reasoning about systems","author":"Huth Michael","unstructured":"Michael Huth and Mark Ryan. 2004. Logic in Computer Science: Modelling and reasoning about systems. Cambridge university press."},{"key":"e_1_3_2_1_35_1","volume-title":"Model-based software testing and analysis with C","author":"Jacky Jonathan","unstructured":"Jonathan Jacky, Margus Veanes, Colin Campbell, and Wolfram Schulte. 2007. Model-based software testing and analysis with C. Cambridge University Press."},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/69575.69577"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04912-5_10"},{"key":"e_1_3_2_1_38_1","volume-title":"Computer Science Curricula","author":"Kumar Amruth N.","year":"2023","unstructured":"Amruth N. Kumar, Rajendra K. Raj, Sherif G. Aly, Monica D. Anderson, Brett A. Becker, Richard L. Blumenthal, Eric Eaton, Susan L. Epstein, Michael Goldweber, Pankaj Jalote, Douglas Lea, Michael Oudshoorn, Marcelo Pias, Susan Reiser, Christian Servin, Rahul Simha, Titus Winters, and Qiao Xiang. 2024. Computer Science Curricula 2023. Association for Computing Machinery, New York, NY, USA. isbn:9798400710339"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-27534-0_5"},{"key":"e_1_3_2_1_40_1","volume-title":"Proceedings of the 7th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 174\u2013185","author":"Lamport Leslie","year":"1980","unstructured":"Leslie Lamport. 1980. \" Sometime\" is sometimes\" not never\" on the temporal logic of programs. In Proceedings of the 7th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 174\u2013185."},{"key":"e_1_3_2_1_41_1","unstructured":"Leslie Lamport. 2002. Specifying systems: the TLA+ language and tools for hardware and software engineers."},{"key":"e_1_3_2_1_42_1","volume-title":"Software engineering 2004: curriculum guidelines for undergraduate degree programs in software engineering","author":"LeBlanc Richard Joseph","unstructured":"Richard Joseph LeBlanc, Ann Sobel, Jorge L Diaz-Herrera, and Thomas B Hilburn. 2006. Software engineering 2004: curriculum guidelines for undergraduate degree programs in software engineering. IEEE Computer Society."},{"key":"e_1_3_2_1_43_1","first-page":"122","article-title":"Temporal logic with past is exponentially more succinct","volume":"79","author":"Markey Nicolas","year":"2003","unstructured":"Nicolas Markey. 2003. Temporal logic with past is exponentially more succinct. Bulletin-European Association for Theoretical Computer Science, 79 (2003), 122\u2013128.","journal-title":"Bulletin-European Association for Theoretical Computer Science"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"crossref","unstructured":"Stephan Merz. 2008. The specification language TLA+. Logics of specification languages 401\u2013451.","DOI":"10.1007\/978-3-540-74107-7_8"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"crossref","unstructured":"Wojciech Mostowski Thomas Arts and John Hughes. 2017. Modelling of Autosar libraries for large scale testing. arXiv preprint arXiv:1703.06574.","DOI":"10.4204\/EPTCS.244.7"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3649833"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/2699417"},{"key":"e_1_3_2_1_48_1","unstructured":"Brian Okken. 2022. Python Testing with pytest. Pragmatic Bookshelf."},{"key":"e_1_3_2_1_49_1","volume-title":"International encyclopedia of education, 2","author":"Perkins David N","year":"1992","unstructured":"David N Perkins and Gavriel Salomon. 1992. Transfer of learning. International encyclopedia of education, 2 (1992), 6452\u20136457."},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2013.6606618"},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"crossref","unstructured":"Amir Pnueli. 1984. In transition from global to modular temporal reasoning about programs. In Logics and models of concurrent systems. Springer 123\u2013144.","DOI":"10.1007\/978-3-642-82453-1_5"},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1109\/40.372360"},{"key":"e_1_3_2_1_54_1","volume-title":"Temporal Logic= Library of Exact Philosophy","author":"Rescher Nicholas","unstructured":"Nicholas Rescher and Alasdair Urquhart. 1971. Temporal Logic= Library of Exact Philosophy, Vol. 3. Springer Verlag."},{"key":"e_1_3_2_1_55_1","volume-title":"Plateau Workshop.","author":"Rothkopf Raven","year":"2023","unstructured":"Raven Rothkopf, Angel Leyi Cui, Hannah Tongxin Zeng, Arya Sinha, and Santolucito Mark. 2023. Towards the usability of reactive synthesis: Building blocks of temporal logic. In Plateau Workshop."},{"key":"e_1_3_2_1_56_1","volume-title":"Rocky roads to transfer: Rethinking mechanism of a neglected phenomenon. Educational psychologist, 24, 2","author":"Salomon Gavriel","year":"1989","unstructured":"Gavriel Salomon and David N Perkins. 1989. Rocky roads to transfer: Rethinking mechanism of a neglected phenomenon. Educational psychologist, 24, 2 (1989), 113\u2013142."},{"key":"e_1_3_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/2483760.2483790"},{"key":"e_1_3_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1109\/MS.2012.13"},{"key":"e_1_3_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.5555\/646130.679472"},{"key":"e_1_3_2_1_60_1","volume-title":"A method for translating natural language program specifications into algebraic specifications. Systems and computers in Japan, 23, 11","author":"Seki Hiroyuki","year":"1992","unstructured":"Hiroyuki Seki, Tadao Kasami, Eiji Nabika, and Takashi Matsumura. 1992. A method for translating natural language program specifications into algebraic specifications. Systems and computers in Japan, 23, 11 (1992), 1\u201316."},{"key":"e_1_3_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796807006466"},{"key":"e_1_3_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0950-5849(00)00166-X"},{"key":"e_1_3_2_1_63_1","volume-title":"Exploring the barriers to formal specification. Ph. D. Dissertation","author":"Snook Colin Frank","unstructured":"Colin Frank Snook. 2001. Exploring the barriers to formal specification. Ph. D. Dissertation. University of Southampton."},{"key":"e_1_3_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1109\/MSR.2017.61"},{"key":"e_1_3_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10664-018-9663-0"},{"key":"e_1_3_2_1_66_1","volume-title":"Typestate: A programming language concept for enhancing software reliability","author":"Strom Robert E","year":"1986","unstructured":"Robert E Strom and Shaula Yemini. 1986. Typestate: A programming language concept for enhancing software reliability. IEEE transactions on software engineering, 157\u2013171."},{"key":"e_1_3_2_1_67_1","volume-title":"JUnit in action","author":"Tahchiev Petar","unstructured":"Petar Tahchiev, Felipe Leme, Vincent Massol, and Gary Gregory. 2010. JUnit in action. Manning Publications."},{"key":"e_1_3_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1145\/1858996.1859053"},{"key":"e_1_3_2_1_69_1","volume-title":"Developer testing: Building quality into software","author":"Tarlinder Alexander","unstructured":"Alexander Tarlinder. 2016. Developer testing: Building quality into software. Addison-Wesley Professional."},{"key":"e_1_3_2_1_70_1","volume-title":"JUnit in action","author":"Tudose Catalin","unstructured":"Catalin Tudose. 2020. JUnit in action. Manning Publications."},{"key":"e_1_3_2_1_71_1","volume-title":"Planning Driven Development","author":"Wayne Hillel","unstructured":"Hillel Wayne. 2018. Practical TLA+: Planning Driven Development. Apress."},{"key":"e_1_3_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.1109\/2.58215"},{"key":"e_1_3_2_1_73_1","volume-title":"Using Relational Problems to Teach Property-Based Testing. The art science and engineering of programming, 5, 2","author":"Wrenn John","year":"2021","unstructured":"John Wrenn, Tim Nelson, and Shriram Krishnamurthi. 2021. Using Relational Problems to Teach Property-Based Testing. The art science and engineering of programming, 5, 2 (2021)."}],"event":{"name":"SPLASH-E '24: 2024 ACM SIGPLAN International Symposium on SPLASH-E","location":"Pasadena CA USA","acronym":"SPLASH-E '24","sponsor":["SIGPLAN SIGPLAN","SIGAda SIGAda"]},"container-title":["Proceedings of the 2024 ACM SIGPLAN International Symposium on SPLASH-E"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3689493.3689980","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3689493.3689980","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T01:09:46Z","timestamp":1750295386000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3689493.3689980"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,10,17]]},"references-count":73,"alternative-id":["10.1145\/3689493.3689980","10.1145\/3689493"],"URL":"https:\/\/doi.org\/10.1145\/3689493.3689980","relation":{},"subject":[],"published":{"date-parts":[[2024,10,17]]},"assertion":[{"value":"2024-10-17","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}