RefinedC: Automating the foundational verification of C code with refined ownership types
Michael Sammler, Rodolphe Lepigre, Robbert Krebbers, Kayvan Memarian, Derek Dreyer, Deepak Garg[doi] [ISBN] [Google Scholar] [DBLP] [Citeseer] [url]
Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation
PLDI 2021
Virtual, Canada
Association for Computing Machinery
New York, NY, USA
Pages 158-174
2021
Note(s): coq theorem prover, ownership types, separation logic, refinement types
PLDI 2021
Virtual, Canada
Association for Computing Machinery
New York, NY, USA
Pages 158-174
2021
Note(s): coq theorem prover, ownership types, separation logic, refinement types