Coq's Vibrant Ecosystem for Verification Engineering (Invited Talk)

被引：7
作者：
Appel, Andrew W. [1 ]
机构：
[1] Princeton Univ, Princeton, NJ 08544 USA
来源：
PROCEEDINGS OF THE 11TH ACM SIGPLAN INTERNATIONAL CONFERENCE ON CERTIFIED PROGRAMS AND PROOFS (CPP '22) | 2022年
关键词：
VST;
D O I：
10.1145/3497775.3503951
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
Program verification in the large is not only a matter of mechanizing a program logic to handle the semantics of your programming language. You must reason in the mathematics of your application domain-and there are many application domains, each with their own community of domain experts. So you will need to import mechanized proof theories from many domains, and they must all interoperate. Such an ecosystem is not only a matter of mathematics, it is a matter of software process engineering and social engineering. Coq's ecosystem has been maturing nicely in these senses.
引用
收藏
页码：2 / 11
页数：10
相关论文
共 48 条
[1]  
[Anonymous], 1998, 25 YEARS CONSTRUCTIV
[2]   Verified Sequential Malloc/Free [J].
Appel, Andrew W. ;
Naumann, David A. .
PROCEEDINGS OF THE 2020 ACM SIGPLAN INTERNATIONAL SYMPOSIUM ON MEMORY MANAGEMENT, ISMM 2020, 2020, :48-59
[3]  
Appel AW, 2020, J FORMALIZ REASON, V13, P1
[4]   Modular Verification for Computer Security [J].
Appel, Andrew W. .
2016 IEEE 29TH COMPUTER SECURITY FOUNDATIONS SYMPOSIUM (CSF 2016), 2016, :1-8
[5]   Verification of a Cryptographic Primitive: SHA-256 [J].
Appel, Andrew W. .
ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2015, 37 (02)
[6]  
Appel AW, 2011, LECT NOTES COMPUT SC, V6602, P1, DOI 10.1007/978-3-642-19718-5_1
[7]  
Appel AW, 2007, CONFERENCE RECORD OF POPL 2007: THE 34TH ACM SIGPLAN SIGACT SYMPOSIUM ON PRINCIPLES OF PROGAMMING LANGUAGES, P109
[8]  
Appel Andrew W., 2014, Program Logics-for Certified Compilers
[9]  
Appel Andrew W., SOFTWARE FDN, V3
[10]   ISA Semantics for ARMv8-A, RISC-V, and CHERI-MIPS [J].
Armstrong, Alasdair ;
Bauereiss, Thomas ;
Campbell, Brian ;
Reid, Alastair ;
Gray, Kathryn E. ;
Norton, Robert M. ;
Mundkur, Prashanth ;
Wassell, Mark ;
French, Jon ;
Pulte, Christopher ;
Flur, Shaked ;
Stark, Ian ;
Krishnaswami, Neel ;
Sewell, Peter .
PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2019, 3 (POPL)
12345