{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,8]],"date-time":"2025-09-08T06:16:37Z","timestamp":1757312197607,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":66,"publisher":"ACM","license":[{"start":{"date-parts":[[2022,11,29]],"date-time":"2022-11-29T00:00:00Z","timestamp":1669680000000},"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,11,29]]},"DOI":"10.1145\/3567512.3567520","type":"proceedings-article","created":{"date-parts":[[2022,12,1]],"date-time":"2022-12-01T21:22:55Z","timestamp":1669929775000},"page":"84-97","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Property-Based Testing: Climbing the Stairway to Verification"],"prefix":"10.1145","author":[{"given":"Zilin","family":"Chen","sequence":"first","affiliation":[{"name":"UNSW, Australia"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christine","family":"Rizkallah","sequence":"additional","affiliation":[{"name":"University of Melbourne, Australia"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Liam","family":"O'Connor","sequence":"additional","affiliation":[{"name":"University of Edinburgh, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Partha","family":"Susarla","sequence":"additional","affiliation":[{"name":"Independent, Australia"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gerwin","family":"Klein","sequence":"additional","affiliation":[{"name":"Proofcraft, Australia \/ UNSW, Australia"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gernot","family":"Heiser","sequence":"additional","affiliation":[{"name":"UNSW, Australia"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gabriele","family":"Keller","sequence":"additional","affiliation":[{"name":"Utrecht University, Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2022,12]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"2022. ACL2. http:\/\/www.cs.utexas.edu\/users\/moore\/acl2\/ \t\t\t\t  2022. ACL2. http:\/\/www.cs.utexas.edu\/users\/moore\/acl2\/"},{"key":"e_1_3_2_1_2_1","unstructured":"AdaCore. 2022. SPARK Pro. https:\/\/www.adacore.com\/sparkpro\/ \t\t\t\t  AdaCore. 2022. SPARK Pro. https:\/\/www.adacore.com\/sparkpro\/"},{"volume-title":"A Methodology for Trustworthy File Systems. CSE","author":"Amani Sidney","key":"e_1_3_2_1_3_1","unstructured":"Sidney Amani . 2016. A Methodology for Trustworthy File Systems. CSE , UNSW. Sydney, Australia . Sidney Amani. 2016. A Methodology for Trustworthy File Systems. CSE, UNSW. Sydney, Australia."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2872362.2872404"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.196.1"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSTW.2015.7107466"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00291051"},{"key":"e_1_3_2_1_8_1","volume-title":"Conventional and Uniqueness Typing in Graph Rewrite Systems. In Foundations of Software Technology and Theoretical Computer Science (Lecture Notes in Computer Science","volume":"51","author":"Barendsen Erik","year":"1993","unstructured":"Erik Barendsen and Sjaak Smetsers . 1993 . Conventional and Uniqueness Typing in Graph Rewrite Systems. In Foundations of Software Technology and Theoretical Computer Science (Lecture Notes in Computer Science , Vol. 761). 41\u2013 51 . Erik Barendsen and Sjaak Smetsers. 1993. Conventional and Uniqueness Typing in Graph Rewrite Systems. In Foundations of Software Technology and Theoretical Computer Science (Lecture Notes in Computer Science, Vol. 761). 41\u201351."},{"key":"e_1_3_2_1_9_1","unstructured":"Brian Behlendorf. 2011. POSIX Filesystem Test Suite. https:\/\/github.com\/zfsonlinux\/fstest \t\t\t\t  Brian Behlendorf. 2011. POSIX Filesystem Test Suite. https:\/\/github.com\/zfsonlinux\/fstest"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/SEFM.2004.36"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158093"},{"volume-title":"Programming Languages and Systems","author":"Bernardy Jean-Philippe","key":"e_1_3_2_1_12_1","unstructured":"Jean-Philippe Bernardy , Patrik Jansson , and Koen Claessen . 2010. Testing Polymorphic Properties . In Programming Languages and Systems . Springer Berlin Heidelberg , Berlin, Heidelberg . 125\u2013144. Jean-Philippe Bernardy, Patrik Jansson, and Koen Claessen. 2010. Testing Polymorphic Properties. In Programming Languages and Systems. Springer Berlin Heidelberg, Berlin, Heidelberg. 125\u2013144."},{"volume-title":"Interactive Theorem Proving and Program Development. Coq\u2019Art: The Calculus of Inductive Constructions","author":"Bertot Yves","key":"e_1_3_2_1_13_1","unstructured":"Yves Bertot and Pierre Cast\u00e9ran . 2004. Interactive Theorem Proving and Program Development. Coq\u2019Art: The Calculus of Inductive Constructions . Springer . Yves Bertot and Pierre Cast\u00e9ran. 2004. Interactive Theorem Proving and Program Development. Coq\u2019Art: The Calculus of Inductive Constructions. Springer."},{"key":"e_1_3_2_1_14_1","volume-title":"ICFP","author":"Breitner Joachim","year":"2018","unstructured":"Joachim Breitner , Antal Spector-Zabusky , Yao Li , Christine Rizkallah , John Wiegley , and Stephanie Weirich . 2018. Ready , set, verify! applying hs-to-coq to real-world Haskell code (experience report). PACMPL, 2 , ICFP ( 2018 ), 89:1\u201389:16. Joachim Breitner, Antal Spector-Zabusky, Yao Li, Christine Rizkallah, John Wiegley, and Stephanie Weirich. 2018. Ready, set, verify! applying hs-to-coq to real-world Haskell code (experience report). PACMPL, 2, ICFP (2018), 89:1\u201389:16."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35308-6_10"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/10722298_8"},{"key":"e_1_3_2_1_17_1","unstructured":"Zilin Chen. 2022. Cogent property-based testing case studies. https:\/\/github.com\/au-ts\/cogent\/tree\/master\/impl\/fs\/bilby\/quickcheck \t\t\t\t  Zilin Chen. 2022. Cogent property-based testing case studies. https:\/\/github.com\/au-ts\/cogent\/tree\/master\/impl\/fs\/bilby\/quickcheck"},{"key":"e_1_3_2_1_18_1","volume-title":"The Cogent Case for Property-Based Testing. In Workshop on Programming Languages and Operating Systems (PLOS). ACM","author":"Chen Zilin","year":"2017","unstructured":"Zilin Chen , Liam O\u2019Connor , Gabriele Keller , Gerwin Klein , and Gernot Heiser . 2017 . The Cogent Case for Property-Based Testing. In Workshop on Programming Languages and Operating Systems (PLOS). ACM , Shanghai, China. 1\u20137. Zilin Chen, Liam O\u2019Connor, Gabriele Keller, Gerwin Klein, and Gernot Heiser. 2017. The Cogent Case for Property-Based Testing. In Workshop on Programming Languages and Operating Systems (PLOS). ACM, Shanghai, China. 1\u20137."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3497775.3503686"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/351240.351266"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1596550.1596574"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71067-7_16"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535839"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511663079"},{"key":"e_1_3_2_1_25_1","volume-title":"Abrahamson","author":"de Vries Edsko","year":"2008","unstructured":"Edsko de Vries , Rinus Plasmeijer , and David M . Abrahamson . 2008 . Uniqueness Typing Simplified. In Implementation and Application of Functional Languages (Lecture Notes in Computer Science , Vol. 5083). Springer, 201\u2013 218 . Edsko de Vries, Rinus Plasmeijer, and David M. Abrahamson. 2008. Uniqueness Typing Simplified. In Implementation and Application of Functional Languages (Lecture Notes in Computer Science, Vol. 5083). Springer, 201\u2013218."},{"volume-title":"Proceedings of the ACM SIGPLAN Haskell Workshop","author":"Derrin Philip","key":"e_1_3_2_1_26_1","unstructured":"Philip Derrin , Kevin Elphinstone , Gerwin Klein , David Cock , and Manuel M. T. Chakravarty . 2006. Running the Manual: An Approach to High-Assurance Microkernel Development . In Proceedings of the ACM SIGPLAN Haskell Workshop . Portland, OR, USA. Philip Derrin, Kevin Elphinstone, Gerwin Klein, David Cock, and Manuel M. T. Chakravarty. 2006. Running the Manual: An Approach to High-Assurance Microkernel Development. In Proceedings of the ACM SIGPLAN Haskell Workshop. Portland, OR, USA."},{"volume-title":"Enhancements to the Cogent Property-Based Testing Framework. CSE","author":"Downing Oscar","key":"e_1_3_2_1_27_1","unstructured":"Oscar Downing . 2021. Enhancements to the Cogent Property-Based Testing Framework. CSE , UNSW. Sydney, Australia . https:\/\/people.eng.unimelb.edu.au\/rizkallahc\/theses\/oscar-downing-honours-thesis.pdf Oscar Downing. 2021. Enhancements to the Cogent Property-Based Testing Framework. CSE, UNSW. Sydney, Australia. https:\/\/people.eng.unimelb.edu.au\/rizkallahc\/theses\/oscar-downing-honours-thesis.pdf"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2364506.2364515"},{"volume-title":"Theorem Proving in Higher Order Logics","author":"Dybjer Peter","key":"e_1_3_2_1_29_1","unstructured":"Peter Dybjer , Haiyan Qiao , and Makoto Takeyama . 2003. Combining Testing and Proving in Dependent Type Theory . In Theorem Proving in Higher Order Logics . Springer Berlin Heidelberg , Berlin, Heidelberg . 188\u2013203. Peter Dybjer, Haiyan Qiao, and Makoto Takeyama. 2003. Combining Testing and Proving in Dependent Type Theory. In Theorem Proving in Higher Order Logics. Springer Berlin Heidelberg, Berlin, Heidelberg. 188\u2013203."},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1637837.1637844"},{"key":"e_1_3_2_1_31_1","unstructured":"2022. The FUSE Project. https:\/\/github.com\/libfuse\/libfuse \t\t\t\t  2022. The FUSE Project. https:\/\/github.com\/libfuse\/libfuse"},{"key":"e_1_3_2_1_32_1","unstructured":"2022. GHC User\u2019s Guide. https:\/\/downloads.haskell.org\/ghc\/latest\/docs\/users_guide\/ \t\t\t\t  2022. GHC User\u2019s Guide. https:\/\/downloads.haskell.org\/ghc\/latest\/docs\/users_guide\/"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11219-017-9386-2"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/1086365.1086380"},{"key":"e_1_3_2_1_35_1","unstructured":"2018. The Haskell Lightweight Virtual Machine (HaLVM) source archive. https:\/\/github.com\/GaloisInc\/HaLVM \t\t\t\t  2018. The Haskell Lightweight Virtual Machine (HaLVM) source archive. https:\/\/github.com\/GaloisInc\/HaLVM"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/1867635.1867638"},{"key":"e_1_3_2_1_37_1","volume-title":"Quickly. In International Conference on Functional Programming. 455\u2013468","author":"Hri\u0163cu C\u0103t\u0103lin","year":"2013","unstructured":"C\u0103t\u0103lin Hri\u0163cu , John Hughes , Benjamin C. Pierce , Antal Spector-Zabusky , Dimitrios Vytiniotis , Arthur Azevedo de Amorim , and Leonidas Lampropoulos . 2013 . Testing Noninterference , Quickly. In International Conference on Functional Programming. 455\u2013468 . C\u0103t\u0103lin Hri\u0163cu, John Hughes, Benjamin C. Pierce, Antal Spector-Zabusky, Dimitrios Vytiniotis, Arthur Azevedo de Amorim, and Leonidas Lampropoulos. 2013. Testing Noninterference, Quickly. In International Conference on Functional Programming. 455\u2013468."},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-30936-1_9"},{"key":"e_1_3_2_1_39_1","unstructured":"Steve Klabnik and Carol Nichols. 2017. The Rust Programming Language. No Starch Press. \t\t\t\t  Steve Klabnik and Carol Nichols. 2017. The Rust Programming Language. No Starch Press."},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2560537"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_3_2_1_42_1","unstructured":"Edward A. Kmett. 2022. lens: Lenses Folds and Traversals. https:\/\/hackage.haskell.org\/package\/lens \t\t\t\t  Edward A. Kmett. 2022. lens: Lenses Folds and Traversals. https:\/\/hackage.haskell.org\/package\/lens"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/10722298"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39634-2_9"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-018-9461-9"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009868"},{"key":"e_1_3_2_1_47_1","volume-title":"Pierce","author":"Lampropoulos Leonidas","year":"2022","unstructured":"Leonidas Lampropoulos and Benjamin C . Pierce . 2022 . QuickChick: Property- Based Testing in Coq . https:\/\/softwarefoundations.cis.upenn.edu\/qc-current\/index.html Leonidas Lampropoulos and Benjamin C. Pierce. 2022. QuickChick: Property-Based Testing in Coq. https:\/\/softwarefoundations.cis.upenn.edu\/qc-current\/index.html"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/325694.325708"},{"key":"e_1_3_2_1_49_1","unstructured":"David R. MacIver. 2016. Integrated vs Type-based Shrinking. http:\/\/hypothesis.works\/articles\/integrated-shrinking \t\t\t\t  David R. MacIver. 2016. Integrated vs Type-based Shrinking. http:\/\/hypothesis.works\/articles\/integrated-shrinking"},{"key":"e_1_3_2_1_50_1","unstructured":"David R. MacIver. 2016. QuickCheck in Every Language. https:\/\/hypothesis.works\/articles\/quickcheck-in-every-language \t\t\t\t  David R. MacIver. 2016. QuickCheck in Every Language. https:\/\/hypothesis.works\/articles\/quickcheck-in-every-language"},{"key":"e_1_3_2_1_51_1","unstructured":"Toshiyuki Maeda. 2015. Kernel Mode Linux: Execute user processes in kernel mode. http:\/\/web.yl.is.s.u-tokyo.ac.jp\/~tosh\/kml\/ \t\t\t\t  Toshiyuki Maeda. 2015. Kernel Mode Linux: Execute user processes in kernel mode. http:\/\/web.yl.is.s.u-tokyo.ac.jp\/~tosh\/kml\/"},{"key":"e_1_3_2_1_52_1","volume-title":"Programming from Specifications","author":"Morgan Carroll","unstructured":"Carroll Morgan . 1990. Programming from Specifications ( 2 nd ed.). Prentice Hall . Carroll Morgan. 1990. Programming from Specifications (2nd ed.). Prentice Hall.","edition":"2"},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.244.7"},{"volume-title":"Concrete Semantics with Isabelle\/HOL","author":"Nipkow Tobias","key":"e_1_3_2_1_54_1","unstructured":"Tobias Nipkow and Gerwin Klein . 2014. Concrete Semantics with Isabelle\/HOL . Springer . Tobias Nipkow and Gerwin Klein. 2014. Concrete Semantics with Isabelle\/HOL. Springer."},{"key":"e_1_3_2_1_55_1","volume-title":"Type Systems for Systems Types. Ph. D. Dissertation","author":"O\u2019Connor Liam","year":"1959","unstructured":"Liam O\u2019Connor . 2019. Type Systems for Systems Types. Ph. D. Dissertation . UNSW . Sydney, Australia . http:\/\/handle.unsw.edu.au\/ 1959 .4\/64238 Liam O\u2019Connor. 2019. Type Systems for Systems Types. Ph. D. Dissertation. UNSW. Sydney, Australia. http:\/\/handle.unsw.edu.au\/1959.4\/64238"},{"key":"e_1_3_2_1_56_1","volume-title":"Refinement Through Restraint: Bringing Down the Cost of Verification. In International Conference on Functional Programming","author":"O\u2019Connor Liam","year":"2016","unstructured":"Liam O\u2019Connor , Zilin Chen , Christine Rizkallah , Sidney Amani , Japheth Lim , Toby Murray , Yutaka Nagashima , Thomas Sewell , and Gerwin Klein . 2016 . Refinement Through Restraint: Bringing Down the Cost of Verification. In International Conference on Functional Programming . Nara, Japan. Liam O\u2019Connor, Zilin Chen, Christine Rizkallah, Sidney Amani, Japheth Lim, Toby Murray, Yutaka Nagashima, Thomas Sewell, and Gerwin Klein. 2016. Refinement Through Restraint: Bringing Down the Cost of Verification. In International Conference on Functional Programming. Nara, Japan."},{"key":"e_1_3_2_1_57_1","unstructured":"Bryan O\u2019Sullivan. 2022. aeson: Fast JSON parsing and encoding. https:\/\/hackage.haskell.org\/package\/aeson \t\t\t\t  Bryan O\u2019Sullivan. 2022. aeson: Fast JSON parsing and encoding. https:\/\/hackage.haskell.org\/package\/aeson"},{"key":"e_1_3_2_1_58_1","volume-title":"Cogent: uniqueness types and certifying compilation. Journal of Functional Programming, 31","author":"O\u2019Connor Liam","year":"2021","unstructured":"Liam O\u2019Connor , Zilin Chen , Christine Rizkallah , Vincent Jackson , Sidney Amani , Gerwin Klein , Toby Murray , Thomas Sewell , and Gabriele Keller . 2021. Cogent: uniqueness types and certifying compilation. Journal of Functional Programming, 31 ( 2021 ). Liam O\u2019Connor, Zilin Chen, Christine Rizkallah, Vincent Jackson, Sidney Amani, Gerwin Klein, Toby Murray, Thomas Sewell, and Gabriele Keller. 2021. Cogent: uniqueness types and certifying compilation. Journal of Functional Programming, 31 (2021)."},{"key":"e_1_3_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-43144-4_20"},{"key":"e_1_3_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411286.1411292"},{"key":"e_1_3_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/3167092"},{"key":"e_1_3_2_1_62_1","unstructured":"Jacob Stanley. 2022. Hedgehog will eat all your bugs. https:\/\/github.com\/hedgehogqa\/haskell-hedgehog \t\t\t\t  Jacob Stanley. 2022. Hedgehog will eat all your bugs. https:\/\/github.com\/hedgehogqa\/haskell-hedgehog"},{"key":"e_1_3_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-21455-4_9"},{"key":"e_1_3_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1002\/stvr.456"},{"key":"e_1_3_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1145\/1217975.1217999"},{"key":"e_1_3_2_1_66_1","unstructured":"Philip Wadler. 1990. Linear types can change the world!. In Programming Concepts and Methods. \t\t\t\t  Philip Wadler. 1990. Linear types can change the world!. In Programming Concepts and Methods."}],"event":{"name":"SLE '22: 15th ACM SIGPLAN International Conference on Software Language Engineering","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"],"location":"Auckland New Zealand","acronym":"SLE '22"},"container-title":["Proceedings of the 15th ACM SIGPLAN International Conference on Software Language Engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3567512.3567520","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3567512.3567520","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T22:43:47Z","timestamp":1750286627000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3567512.3567520"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,11,29]]},"references-count":66,"alternative-id":["10.1145\/3567512.3567520","10.1145\/3567512"],"URL":"https:\/\/doi.org\/10.1145\/3567512.3567520","relation":{},"subject":[],"published":{"date-parts":[[2022,11,29]]},"assertion":[{"value":"2022-12-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}