共 22 条
[1]
Besson Frederic, 2014, Programming Languages and Systems. 12th Asian Symposium (APLAS 2014), Proceedings: LNCS 8858, P449, DOI 10.1007/978-3-319-12736-1_24
[3]
CompCertS: A Memory-Aware Verified C Compiler Using Pointer as Integer Semantics
[J].
INTERACTIVE THEOREM PROVING (ITP 2017),
2017, 10499
:81-97
[5]
Chisnall David, 2016, C MEMORY OBJECT VALU
[6]
A Context-Sensitive Memory Model for Verification of C/C plus plus Programs
[J].
STATIC ANALYSIS (SAS 2017),
2017, 10422
:148-168
[7]
Hathhorn C, 2015, ACM SIGPLAN NOTICES, V50, P336, DOI [10.1145/2737924.2737979, 10.1145/2813885.2737979]
[8]
Kang J, 2015, ACM SIGPLAN NOTICES, V50, P326, DOI [10.1145/2813885.2738005, 10.1145/2737924.2738005]
[9]
A Typed C11 Semantics for Interactive Theorem Proving
[J].
CPP'15: PROCEEDINGS OF THE 2015 ACM CONFERENCE ON CERTIFIED PROGRAMS AND PROOFS,
2015,
:15-27
[10]
Krebbers Robbert, 2013, ALIASING RESTRICTION, DOI [10.1007/978-3-319-03545-1_4, DOI 10.1007/978-3-319-03545-1_4]