Michael Sammler
ABSTRACT
Given the central role that C continues to play in systems software, and the difficulty of writing safe and correct C code, it remains a grand challenge to develop effective formal methods for verifying C programs. In this paper, we propose a new approach to this problem: a type system we call RefinedC, which combines ownership types (for modular reasoning about shared state and concurrency) with refinement types (for encoding precise invariants on C data types and Hoare-style specifications for C functions).
RefinedC is both automated (requiring minimal user intervention) and foundational (producing a proof of program correctness in Coq), while at the same time handling a range of low-level programming idioms such as pointer arithmetic. In particular, following the approach of RustBelt, the soundness of the RefinedC type system is justified semantically by interpretation into the Coq-based Iris framework for higher-order concurrent separation logic. However, the typing rules of RefinedC are also designed to be encodable in a new “separation logic programming” language we call Lithium. By restricting to a carefully chosen (yet expressive) fragment of separation logic, Lithium supports predictable, automatic, goal-directed proof search without backtracking. We demonstrate the effectiveness of RefinedC on a range of representative examples of C code.
- Jean-Marc Andreoli. 1992. Logic programming with focusing proofs in linear logic. J. Log. Comput., 2, 3 (1992), 297–347. https://doi.org/10.1093/logcom/2.3.297 Google Scholar
Cross Ref
- Andrew W. Appel. 2014. Program Logics for Certified Compilers. Cambridge University Press. https://www.cambridge.org/de/academic/subjects/computer-science/programming-languages-and-applied-logic/program-logics-certified-compilersGoogle ScholarDigital Library
- Pablo A. Armelín and David J. Pym. 2001. Bunched logic programming. In IJCAR (LNCS, Vol. 2083). Springer, 289–304. https://doi.org/10.1007/3-540-45744-5_21 Google ScholarCross Ref
- Alexander Bakst and Ranjit Jhala. 2016. Predicate abstraction for linked data structures. In VMCAI (LNCS, Vol. 9583). Springer, 65–84. https://doi.org/10.1007/978-3-662-49122-5_3 Google ScholarDigital Library
- Mark Batty, Scott Owens, Susmit Sarkar, Peter Sewell, and Tjark Weber. 2011. Mathematizing C++ concurrency. In POPL. ACM, 55–66. https://doi.org/10.1145/1926385.1926394 Google ScholarDigital Library
- Josh Berdine, Cristiano Calcagno, and Peter W. O’Hearn. 2004. A decidable fragment of separation logic. In FSTTCS (LNCS, Vol. 3328). Springer, 97–109. https://doi.org/10.1007/978-3-540-30538-5_9 Google ScholarDigital Library
- Josh Berdine, Cristiano Calcagno, and Peter W. O’Hearn. 2005. Smallfoot: Modular automatic assertion checking with separation logic. In FMCO (LNCS, Vol. 4111). Springer, 115–137. https://doi.org/10.1007/11804192_6 Google ScholarDigital Library
- Sylvie Boldo and Guillaume Melquiond. 2011. Flocq: A unified library for proving floating-point algorithms in Coq. In ARITH. IEEE Computer Society, 243–252. https://doi.org/10.1109/ARITH.2011.40 Google ScholarDigital Library
- Cristiano Calcagno, Dino Distefano, Peter W. O’Hearn, and Hongseok Yang. 2009. Compositional shape analysis by means of bi-abduction. In POPL. ACM, 289–300. https://doi.org/10.1145/1480881.1480917 Google ScholarDigital Library
- Qinxiang Cao, Lennart Beringer, Samuel Gruetter, Josiah Dodds, and Andrew W. Appel. 2018. VST-Floyd: A separation logic tool to verify correctness of C programs. J. Autom. Reason., 61, 1-4 (2018), 367–422. https://doi.org/10.1007/s10817-018-9457-5 Google ScholarDigital Library
- Qinxiang Cao, Shengyi Wang, Aquinas Hobor, and Andrew W. Appel. 2019. Proof pearl: Magic wand as frame. CoRR, abs/1909.08789 (2019), arxiv:1909.08789Google Scholar
- Arthur Charguéraud. 2016. Higher-order representation predicates in separation logic. In CPP. ACM, 3–14. https://doi.org/10.1145/2854065.2854068 Google ScholarDigital Library
- Adam Chlipala. 2011. Mostly-automated verification of low-level programs in computational separation logic. In PLDI. ACM, 234–245. https://doi.org/10.1145/1993498.1993526 Google ScholarDigital Library
- Adam Chlipala. 2013. The Bedrock structured programming system: Combining generative metaprogramming and Hoare logic in an extensible program verifier. In ICFP. ACM, 391–402. https://doi.org/10.1145/2500365.2500592 Google ScholarDigital Library
- Adam Chlipala. 2015. From network interface to multithreaded web applications: A case study in modular program verification. In POPL. ACM, 609–622. https://doi.org/10.1145/2676726.2677003 Google ScholarDigital Library
- Duc-Hiep Chu, Joxan Jaffar, and Minh-Thai Trinh. 2015. Automatic induction proofs of data-structures in imperative programs. In PLDI. ACM, 457–466. https://doi.org/10.1145/2737924.2737984 Google ScholarDigital Library
- Ernie Cohen, Markus Dahlweid, Mark A. Hillebrand, Dirk Leinenbach, Michal Moskal, Thomas Santen, Wolfram Schulte, and Stephan Tobies. 2009. VCC: A practical system for verifying concurrent C. In TPHOLs (LNCS, Vol. 5674). Springer, 23–42. https://doi.org/10.1007/978-3-642-03359-9_2 Google ScholarDigital Library
- Ernie Cohen, Mark A. Hillebrand, Stephan Tobies, Michał Moskal, and Wolfram Schulte. 2012. Verifying C programs: A VCC tutorial. https://archive.codeplex.com/projects/VCC/fda99f81-18b5-45ae-8f49-5b28c747dcc3Google Scholar
- Jeremy Condit, Brian Hackett, Shuvendu K. Lahiri, and Shaz Qadeer. 2009. Unifying type checking and property checking for low-level code. In POPL. ACM, 302–314. https://doi.org/10.1145/1480881.1480921 Google ScholarDigital Library
- Jeremy Condit, Matthew Harren, Zachary R. Anderson, David Gay, and George C. Necula. 2007. Dependent types for low-level programming. In ESOP (LNCS, Vol. 4421). Springer, 520–535. https://doi.org/10.1007/978-3-540-71316-6_35 Google ScholarCross Ref
- Pascal Cuoq, Florent Kirchner, Nikolai Kosmatov, Virgile Prevosto, Julien Signoles, and Boris Yakobowski. 2012. Frama-C: A software analysis perspective. In SEFM (LNCS, Vol. 7504). Springer, 233–247. https://doi.org/10.1007/978-3-642-33826-7_16 Google ScholarDigital Library
- Hoang-Hai Dang, Jacques-Henri Jourdan, Jan-Oliver Kaiser, and Derek Dreyer. 2020. RustBelt meets relaxed memory. Proc. ACM Program. Lang., 4, POPL (2020), 34:1–34:29. https://doi.org/10.1145/3371102 Google ScholarDigital Library
- David Delahaye. 2000. A tactic language for the system Coq. In LPAR (LNCS, Vol. 1955). Springer, 85–95. https://doi.org/10.1007/3-540-44404-1_7 Google ScholarCross Ref
- Robert DeLine and Manuel Fähndrich. 2001. Enforcing high-level protocols in low-level software. In PLDI. ACM, 59–69. https://doi.org/10.1145/378795.378811 Google ScholarDigital Library
- Archibald Samuel Elliott, Andrew Ruef, Michael Hicks, and David Tarditi. 2018. Checked C: making C safe by extension. In SecDev. IEEE Computer Society, 53–60. https://doi.org/10.1109/SecDev.2018.00015 Google ScholarCross Ref
- Andres Erbsen, Jade Philipoom, Jason Gross, Robert Sloan, and Adam Chlipala. 2019. Simple high-level code for cryptographic arithmetic - with proofs, without compromises. In IEEE Symposium on Security and Privacy. IEEE, 1202–1219. https://doi.org/10.1109/SP.2019.00005 Google ScholarCross Ref
- Xinyu Feng, Zhong Shao, Yu Guo, and Yuan Dong. 2008. Combining domain-specific and foundational logics to verify complete software systems. In VSTTE (LNCS, Vol. 5295). Springer, 54–69. https://doi.org/10.1007/978-3-540-87873-5_8 Google ScholarDigital Library
- Timothy S. Freeman and Frank Pfenning. 1991. Refinement types for ML. In PLDI. ACM, 268–277. https://doi.org/10.1145/113445.113468 Google ScholarDigital Library
- Dan Frumin, Léon Gondelman, and Robbert Krebbers. 2019. Semi-automated reasoning about non-determinism in C expressions. In ESOP (LNCS, Vol. 11423). Springer, 60–87. https://doi.org/10.1007/978-3-030-17184-1_3 Google ScholarCross Ref
- David Greenaway, June Andronick, and Gerwin Klein. 2012. Bridging the gap: Automatic verified abstraction of C. In ITP (LNCS, Vol. 7406). Springer, 99–115. https://doi.org/10.1007/978-3-642-32347-8_8 Google ScholarCross Ref
- David Greenaway, Japheth Lim, June Andronick, and Gerwin Klein. 2014. Don’t sweat the small stuff: formal verification of C code without the pain. In PLDI. ACM, 429–439. https://doi.org/10.1145/2594291.2594296 Google ScholarDigital Library
- Ronghui Gu, Jérémie Koenig, Tahina Ramananandro, Zhong Shao, Xiongnan (Newman) Wu, Shu-Chun Weng, Haozhong Zhang, and Yu Guo. 2015. Deep specifications and certified abstraction layers. In POPL. ACM, 595–608. https://doi.org/10.1145/2676726.2676975 Google ScholarDigital Library
- Ronghui Gu, Zhong Shao, Hao Chen, Jieung Kim, Jérémie Koenig, Xiongnan (Newman) Wu, Vilhelm Sjöberg, and David Costanzo. 2019. Building certified concurrent OS kernels. Commun. ACM, 62, 10 (2019), 89–99. https://doi.org/10.1145/3356903 Google ScholarDigital Library
- Ronghui Gu, Zhong Shao, Jieung Kim, Xiongnan (Newman) Wu, Jérémie Koenig, Vilhelm Sjöberg, Hao Chen, David Costanzo, and Tahina Ramananandro. 2018. Certified concurrent abstraction layers. In PLDI. ACM, 646–661. https://doi.org/10.1145/3192366.3192381 Google ScholarDigital Library
- Hafnium. 2020. Hafnium. https://review.trustedfirmware.org/plugins/gitiles/hafnium/hafnium/+/HEAD/README.mdGoogle Scholar
- James Harland, David J. Pym, and Michael Winikoff. 1996. Programming in Lygon: An overview. In AMAST (LNCS, Vol. 1101). Springer, 391–405. https://doi.org/10.1007/BFb0014329 Google ScholarCross Ref
- Chris Hathhorn, Chucky Ellison, and Grigore Rosu. 2015. Defining the undefinedness of C. In PLDI. ACM, 336–345. https://doi.org/10.1145/2737924.2737979 Google ScholarDigital Library
- Aquinas Hobor, Andrew W. Appel, and Francesco Zappa Nardelli. 2008. Oracle semantics for concurrent separation logic. In ESOP (LNCS, Vol. 4960). Springer, 353–367. https://doi.org/10.1007/978-3-540-78739-6_27 Google ScholarCross Ref
- Joshua S. Hodas and Dale Miller. 1991. Logic programming in a fragment of intuitionistic linear logic. In LICS. IEEE Computer Society, 32–42. https://doi.org/10.1109/LICS.1991.151628 Google ScholarCross Ref
- Bart Jacobs, Jan Smans, Pieter Philippaerts, Frédéric Vogels, Willem Penninckx, and Frank Piessens. 2011. VeriFast: A powerful, sound, predictable, fast verifier for C and Java. In NASA Formal Methods (LNCS, Vol. 6617). Springer, 41–55. https://doi.org/10.1007/978-3-642-20398-5_4 Google ScholarCross Ref
- Trevor Jim, Greg Morrisett, Dan Grossman, Michael W. Hicks, James Cheney, and Yanling Wang. 2002. Cyclone: A safe dialect of C. In USENIX. 275–288. http://www.usenix.org/publications/library/proceedings/usenix02/jim.htmlGoogle Scholar
- Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, and Derek Dreyer. 2018. RustBelt: Securing the foundations of the Rust programming language. Proc. ACM Program. Lang., 2, POPL (2018), 66:1–66:34. https://doi.org/10.1145/3158154 Google ScholarDigital Library
- Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, and Derek Dreyer. 2021. Safe systems programming in Rust. Commun. ACM, 64, 4 (2021), April, 144–152. https://cacm.acm.org/magazines/2021/4/251364-safe-systems-programming-in-rust/fulltextGoogle ScholarDigital Library
- Ralf Jung, Robbert Krebbers, Lars Birkedal, and Derek Dreyer. 2016. Higher-order ghost state. In ICFP. ACM, 256–269. https://doi.org/10.1145/2951913.2951943 Google ScholarDigital Library
- Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Ales Bizjak, Lars Birkedal, and Derek Dreyer. 2018. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. J. Funct. Program., 28 (2018), e20. https://doi.org/10.1017/S0956796818000151 Google ScholarCross Ref
- Ralf Jung, Rodolphe Lepigre, Gaurav Parthasarathy, Marianna Rapoport, Amin Timany, Derek Dreyer, and Bart Jacobs. 2020. The future is ours: Prophecy variables in separation logic. Proc. ACM Program. Lang., 4, POPL (2020), 45:1–45:32. https://doi.org/10.1145/3371113 Google ScholarDigital Library
- Ralf Jung, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon, Lars Birkedal, and Derek Dreyer. 2015. Iris: Monoids and invariants as an orthogonal basis for concurrent reasoning. In POPL. ACM, 637–650. https://doi.org/10.1145/2676726.2676980 Google ScholarDigital Library
- Jan-Oliver Kaiser, Hoang-Hai Dang, Derek Dreyer, Ori Lahav, and Viktor Vafeiadis. 2017. Strong logic for weak memory: Reasoning about release-acquire consistency in iris. In ECOOP (LIPIcs, Vol. 74). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 17:1–17:29. https://doi.org/10.4230/LIPIcs.ECOOP.2017.17 Google ScholarCross Ref
- Jeehoon Kang, Chung-Kil Hur, William Mansky, Dmitri Garbuzov, Steve Zdancewic, and Viktor Vafeiadis. 2015. A formal C memory model supporting integer-pointer casts. In PLDI. ACM, 326–335. https://doi.org/10.1145/2737924.2738005 Google ScholarDigital Library
- Gerwin Klein, June Andronick, Kevin Elphinstone, Toby C. Murray, Thomas Sewell, Rafal Kolanski, and Gernot Heiser. 2014. Comprehensive formal verification of an OS microkernel. ACM Trans. Comput. Syst., 32, 1 (2014), 2:1–2:70. https://doi.org/10.1145/2560537 Google ScholarDigital Library
- Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood. 2009. seL4: Formal verification of an OS kernel. In SOSP. ACM, 207–220. https://doi.org/10.1145/1629575.1629596 Google ScholarDigital Library
- Robbert Krebbers. 2014. An operational and axiomatic semantics for non-determinism and sequence points in C. In POPL. ACM, 101–112. https://doi.org/10.1145/2535838.2535878 Google ScholarDigital Library
- Robbert Krebbers. 2015. The C standard formalized in Coq. Ph.D. Dissertation. Radboud University Nijmegen. https://robbertkrebbers.nl/thesis.htmlGoogle Scholar
- Robbert Krebbers, Jacques-Henri Jourdan, Ralf Jung, Joseph Tassarotti, Jan-Oliver Kaiser, Amin Timany, Arthur Charguéraud, and Derek Dreyer. 2018. MoSeL: A general, extensible modal framework for interactive proofs in separation logic. Proc. ACM Program. Lang., 2, ICFP (2018), 77:1–77:30. https://doi.org/10.1145/3236772 Google ScholarDigital Library
- Robbert Krebbers, Ralf Jung, Ales Bizjak, Jacques-Henri Jourdan, Derek Dreyer, and Lars Birkedal. 2017. The essence of higher-order concurrent separation logic. In ESOP (LNCS, Vol. 10201). Springer, 696–723. https://doi.org/10.1007/978-3-662-54434-1_26 Google ScholarDigital Library
- Robbert Krebbers, Amin Timany, and Lars Birkedal. 2017. Interactive proofs in higher-order concurrent separation logic. In POPL. ACM, 205–217. http://dl.acm.org/citation.cfm?id=3009855Google Scholar
- Robbert Krebbers and Freek Wiedijk. 2013. Separation logic for non-local control flow and block scope variables. In FoSSaCS (LNCS, Vol. 7794). Springer, 257–272. https://doi.org/10.1007/978-3-642-37075-5_17 Google ScholarDigital Library
- Quang Loc Le, Jun Sun, and Shengchao Qin. 2018. Frame inference for inductive entailment proofs in separation logic. In TACAS (1) (LNCS, Vol. 10805). Springer, 41–60. https://doi.org/10.1007/978-3-319-89960-2_3 Google ScholarCross Ref
- Juneyoung Lee, Yoonseung Kim, Youngju Song, Chung-Kil Hur, Sanjoy Das, David Majnemer, John Regehr, and Nuno P. Lopes. 2017. Taming undefined behavior in LLVM. In PLDI. ACM, 633–647. https://doi.org/10.1145/3062341.3062343 Google ScholarDigital Library
- Wonyeol Lee and Sungwoo Park. 2014. A proof system for separation logic with magic wand. In POPL. ACM, 477–490. https://doi.org/10.1145/2535838.2535871 Google ScholarDigital Library
- Xavier Leroy, Andrew Appel, Sandrine Blazy, and Gordon Stewart. 2012. The CompCert memory model, version 2. Inria. https://hal.inria.fr/hal-00703441Google Scholar
- Xavier Leroy and Sandrine Blazy. 2008. Formal verification of a C-like memory model and its uses for verifying program transformations. J. Autom. Reason., 41, 1 (2008), 1–31. https://doi.org/10.1007/s10817-008-9099-0 Google ScholarDigital Library
- Jacob R. Lorch, Yixuan Chen, Manos Kapritsos, Bryan Parno, Shaz Qadeer, Upamanyu Sharma, James R. Wilcox, and Xueyuan Zhao. 2020. Armada: Low-effort verification of high-performance concurrent programs. In PLDI. ACM, 197–210. https://doi.org/10.1145/3385412.3385971 Google ScholarDigital Library
- Gregory Malecha, Adam Chlipala, and Thomas Braibant. 2014. Compositional computational reflection. In ITP (LNCS, Vol. 8558). Springer, 374–389. https://doi.org/10.1007/978-3-319-08970-6_24 Google ScholarCross Ref
- William Mansky, Andrew W. Appel, and Aleksey Nogin. 2017. A verified messaging system. Proc. ACM Program. Lang., 1, OOPSLA (2017), 87:1–87:28. https://doi.org/10.1145/3133911 Google ScholarDigital Library
- Kayvan Memarian, Victor B. F. Gomes, Brooks Davis, Stephen Kell, Alexander Richardson, Robert N. M. Watson, and Peter Sewell. 2019. Exploring C semantics and pointer provenance. Proc. ACM Program. Lang., 3, POPL (2019), 67:1–67:32. https://doi.org/10.1145/3290380 Google ScholarDigital Library
- Kayvan Memarian, Justus Matthiesen, James Lingard, Kyndylan Nienhuis, David Chisnall, Robert N. M. Watson, and Peter Sewell. 2016. Into the depths of C: elaborating the de facto standards. In PLDI. ACM, 1–15. https://doi.org/10.1145/2908080.2908081 Google ScholarDigital Library
- Magnus Oskar Myreen. 2009. Formal verification of machine-code programs. Ph.D. Dissertation. University of Cambridge, UK. http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.611450Google Scholar
- George C. Necula, Scott McPeak, and Westley Weimer. 2002. CCured: Type-safe retrofitting of legacy code. In POPL. ACM, 128–139. https://doi.org/10.1145/503272.503286 Google ScholarDigital Library
- Ruzica Piskac, Thomas Wies, and Damien Zufferey. 2014. Automating separation logic with trees and data. In CAV (LNCS, Vol. 8559). Springer, 711–728. https://doi.org/10.1007/978-3-319-08867-9_47 Google ScholarDigital Library
- François Pottier and Jonathan Protzenko. 2013. Programming with permissions in Mezzo. In ICFP. ACM, 173–184. https://doi.org/10.1145/2500365.2500598 Google ScholarDigital Library
- Jonathan Protzenko, Jean Karim Zinzindohoué, Aseem Rastogi, Tahina Ramananandro, Peng Wang, Santiago Zanella Béguelin, Antoine Delignat-Lavaud, Catalin Hritcu, Karthikeyan Bhargavan, Cédric Fournet, and Nikhil Swamy. 2017. Verified low-level programming embedded in F*. Proc. ACM Program. Lang., 1, ICFP (2017), 17:1–17:29. https://doi.org/10.1145/3110261 Google ScholarDigital Library
- Andrew Reynolds, Radu Iosif, Cristina Serban, and Tim King. 2016. A decision procedure for separation logic in SMT. In ATVA (LNCS, Vol. 9938). 244–261. https://doi.org/10.1007/978-3-319-46520-3_16 Google ScholarCross Ref
- Patrick Maxim Rondon, Ming Kawaguchi, and Ranjit Jhala. 2008. Liquid types. In PLDI. ACM, 159–169. https://doi.org/10.1145/1375581.1375602 Google ScholarDigital Library
- Patrick Maxim Rondon, Ming Kawaguchi, and Ranjit Jhala. 2010. Low-level liquid types. In POPL. ACM, 131–144. https://doi.org/10.1145/1706299.1706316 Google ScholarDigital Library
- Grigore Rosu, Chucky Ellison, and Wolfram Schulte. 2010. Matching logic: An alternative to Hoare/Floyd logic. In AMAST (LNCS, Vol. 6486). Springer, 142–162. https://doi.org/10.1007/978-3-642-17796-5_9 Google ScholarCross Ref
- Grigore Rosu and Traian-Florin Serbanuta. 2010. An overview of the K semantic framework. J. Log. Algebraic Methods Program., 79, 6 (2010), 397–434. https://doi.org/10.1016/j.jlap.2010.03.012 Google ScholarCross Ref
- Grigore Rosu and Andrei Stefanescu. 2012. Checking reachability using matching logic. In OOPSLA. ACM, 555–574. https://doi.org/10.1145/2384616.2384656 Google ScholarDigital Library
- Michael Sammler, Rodolphe Lepigre, Robbert Krebbers, Kayvan Memarian, Derek Dreyer, and Deepak Garg. 2021. RefinedC: Automating the foundational verification of C code with refined ownership types (Artifact and Appendix). https://doi.org/10.5281/zenodo.4646747 Project webpage: Google ScholarCross Ref
- Ilya Sergey, Aleksandar Nanevski, and Anindya Banerjee. 2015. Mechanized verification of fine-grained concurrent programs. In PLDI. ACM, 77–87. https://doi.org/10.1145/2737924.2737964 Google ScholarDigital Library
- Thomas Arthur Leck Sewell, Magnus O. Myreen, and Gerwin Klein. 2013. Translation validation for a verified OS kernel. In PLDI. ACM, 471–482. https://doi.org/10.1145/2491956.2462183 Google ScholarDigital Library
- Zhong Shao, Valery Trifonov, Bratin Saha, and Nikolaos Papaspyrou. 2005. A type system for certified binaries. ACM Trans. Program. Lang. Syst., 27, 1 (2005), 1–45. https://doi.org/10.1145/1053468.1053469 Google ScholarDigital Library
- Frederick Smith, David Walker, and J. Gregory Morrisett. 2000. Alias types. In ESOP (LNCS, Vol. 1782). Springer, 366–381. https://doi.org/10.1007/3-540-46425-5_24 Google ScholarCross Ref
- Matthieu Sozeau and Nicolas Oury. 2008. First-class type classes. In TPHOLs (LNCS, Vol. 5170). Springer, 278–293. https://doi.org/10.1007/978-3-540-71067-7_23 Google ScholarDigital Library
- Simon Spies, Lennard Gäher, Daniel Gratzer, Joseph Tassarotti, Robbert Krebbers, Derek Dreyer, and Lars Birkedal. 2021. Transfinite Iris: Resolving an existential dilemma of step-indexed separation logic. In PLDI. ACM. https://doi.org/10.1145/3453483.3454031Google Scholar
- Andrei Stefanescu. 2014. MatchC: A matching logic reachability verifier using the K framework. Electron. Notes Theor. Comput. Sci., 304 (2014), 183–198. https://doi.org/10.1016/j.entcs.2014.05.010 Google ScholarCross Ref
- Kasper Svendsen and Lars Birkedal. 2014. Impredicative concurrent abstract predicates. In ESOP (LNCS, Vol. 8410). Springer, 149–168. https://doi.org/10.1007/978-3-642-54833-8_9 Google ScholarDigital Library
- Nikhil Swamy, Juan Chen, Cédric Fournet, Pierre-Yves Strub, Karthikeyan Bhargavan, and Jean Yang. 2011. Secure distributed programming with value-dependent types. In ICFP. ACM, 266–278. https://doi.org/10.1145/2034773.2034811 Google ScholarDigital Library
- Nikhil Swamy, Michael W. Hicks, Greg Morrisett, Dan Grossman, and Trevor Jim. 2006. Safe manual memory management in Cyclone. Sci. Comput. Program., 62, 2 (2006), 122–144. https://doi.org/10.1016/j.scico.2006.02.003 Google ScholarDigital Library
- Quang-Trung Ta, Ton Chanh Le, Siau-Cheng Khoo, and Wei-Ngan Chin. 2018. Automated lemma synthesis in symbolic-heap separation logic. Proc. ACM Program. Lang., 2, POPL (2018), 9:1–9:29. https://doi.org/10.1145/3158097 Google ScholarDigital Library
- The Bedrock Team. 2015. Verification of a singly linked list. https://github.com/mit-plv/bedrock/blob/e3ff3c2cba9976ac4351caaabb4bf/Bedrock/Examples/SinglyLinkedList.vGoogle Scholar
- The Coq-std++ Team. 2020. An extended “standard library” for Coq. https://gitlab.mpi-sws.org/iris/stdppGoogle Scholar
- The Rust Team. 2020. The Rust programming language. https://rust-lang.orgGoogle Scholar
- The Tokei Team. 2020. Tokei. https://github.com/XAMPPRocky/tokeiGoogle Scholar
- The VCC Team. 2016. Verification of a singly linked list. https://github.com/microsoft/vcc/blob/47f3f33d459f5fd9233203ec3d5d2fc803/vcc/Docs/Tutorial/c/7.2.list.cGoogle Scholar
- The Verifast Team. 2019. Verification of a binary search tree. https://github.com/verifast/verifast/blob/8bc966726de829749eaf916ec3863bf294/examples/sorted_bintree.cGoogle Scholar
- The VST Team. 2020. Verification of Binary Search Tree. https://github.com/PrincetonUniversity/VST/blob/14e6b3a79a9685a478786436c6f0a45dc44c3d52/progs/verif_bst.vGoogle Scholar
- John Toman, Ren Siqi, Kohei Suenaga, Atsushi Igarashi, and Naoki Kobayashi. 2020. ConSORT: Context- and flow-sensitive ownership refinement types for imperative programs. In ESOP (LNCS, Vol. 12075). Springer, 684–714. https://doi.org/10.1007/978-3-030-44914-8_25 Google ScholarDigital Library
- Frédéric Vogels, Bart Jacobs, and Frank Piessens. 2015. Featherweight VeriFast. Log. Methods Comput. Sci., 11, 3 (2015), https://doi.org/10.2168/LMCS-11(3:19)2015 Google ScholarCross Ref
- Frédéric Vogels, Bart Jacobs, Frank Piessens, and Jan Smans. 2011. Annotation inference for separation logic based verifiers. In FMOODS/FORTE (LNCS, Vol. 6722). Springer, 319–333. https://doi.org/10.1007/978-3-642-21461-5_21 Google ScholarCross Ref
- David Walker and J. Gregory Morrisett. 2000. Alias types for recursive data structures. In TIC (LNCS, Vol. 2071). Springer, 177–206. https://doi.org/10.1007/3-540-45332-6_7 Google ScholarCross Ref
- Qinshi Wang and Qinxiang Cao. 2019. VST-A: A foundationally sound annotation verifier. CoRR, abs/1909.00097 (2019), arxiv:1909.00097Google Scholar
- Xi Wang, Haogang Chen, Alvin Cheung, Zhihao Jia, Nickolai Zeldovich, and M. Frans Kaashoek. 2012. Undefined behavior: What happened to my code? In APSys. ACM, 9. https://doi.org/10.1145/2349896.2349905 Google ScholarDigital Library
- Simon Winwood, Gerwin Klein, Thomas Sewell, June Andronick, David Cock, and Michael Norrish. 2009. Mind the gap. In TPHOLs (LNCS, Vol. 5674). Springer, 500–515. https://doi.org/10.1007/978-3-642-03359-9_34 Google ScholarDigital Library
- Hongwei Xi. 2007. Dependent ML: An approach to practical programming with dependent types. J. Funct. Program., 17, 2 (2007), 215–286. https://doi.org/10.1017/S0956796806006216 Google ScholarDigital Library
- Hongseok Yang, Oukseh Lee, Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, and Peter W. O’Hearn. 2008. Scalable shape analysis for systems code. In CAV (LNCS, Vol. 5123). Springer, 385–398. https://doi.org/10.1007/978-3-540-70545-1_36 Google ScholarDigital Library
- Jean Karim Zinzindohoué, Karthikeyan Bhargavan, Jonathan Protzenko, and Benjamin Beurdouche. 2017. HACL*: A verified modern cryptographic library. In CCS. ACM, 1789–1806. https://doi.org/10.1145/3133956.3134043 Google ScholarDigital Library
Index Terms
- RefinedC: automating the foundational verification of C code with refined ownership types
Recommendations
Beyond Backtracking: Connections in Fine-Grained Concurrent Separation Logic
Concurrent separation logic has been responsible for major advances in the formal verification of fine-grained concurrent algorithms and data structures such as locks, barriers, queues, and reference counters. The key ingredient of the verification of ...
Proof Automation for Linearizability in Separation Logic
Recent advances in concurrent separation logic enabled the formal verification of increasingly sophisticated fine-grained (i.e., lock-free) concurrent programs. For such programs, the golden standard of correctness is linearizability, which expresses ...
Practical Proof Search for Coq by Type Inhabitation
Automated ReasoningAbstractWe present a practical proof search procedure for Coq based on a direct search for type inhabitants in an appropriate normal form. The procedure is more general than any of the automation tactics natively available in Coq. It aims to handle as ...
Comments