Model Checking One Million Lines of C Code.

作者: Drew Dean , David A. Wagner , Hao Chen

DOI:

关键词:

摘要:

参考文章(21)
Dawson Engler, Madanlal Musuvathi, Static Analysis versus Software Model Checking for Bug Finding verification model checking and abstract interpretation. pp. 191- 210 ,(2004) , 10.1007/978-3-540-24622-0_17
David Wagner, Kunal Talwar, Jeffrey S. Foster, Umesh Shankar, Detecting format string vulnerabilities with type qualifiers usenix security symposium. pp. 16- 16 ,(2001)
Eric A. Brewer, Alexander Aiken, David A. Wagner, Jeffrey S. Foster, A First Step Towards Automated Detection of Buffer Overrun Vulnerabilities. network and distributed system security symposium. ,(2000)
Antony Edwards, Trent Jaeger, Xiaolan Zhang, Using CQUAL for Static Analysis of Authorization Hook Placement usenix security symposium. pp. 33- 48 ,(2002)
Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, Grégoire Sutre, Software verification with BLAST international workshop on model checking software. pp. 235- 239 ,(2003) , 10.1007/3-540-44829-2_17
K. Ashcraft, D. Engler, Using programmer-written compiler extensions to catch security holes ieee symposium on security and privacy. pp. 143- 159 ,(2002) , 10.1109/SECPRI.2002.1004368
Daniel Jackson, Lightweight Formal Methods formal methods. pp. 1- 1 ,(2001) , 10.1007/3-540-45251-6_1
Jeffrey S. Foster, Manuel Fähndrich, Alexander Aiken, A theory of type qualifiers Proceedings of the ACM SIGPLAN 1999 conference on Programming language design and implementation - PLDI '99. ,vol. 34, pp. 192- 203 ,(1999) , 10.1145/301618.301665
Seth Hallem, Benjamin Chelf, Andy Chou, Dawson Engler, Checking system rules using system-specific, programmer-written compiler extensions operating systems design and implementation. pp. 1- 16 ,(2000) , 10.5555/1251229.1251230
Thomas Ball, Sriram K. Rajamani, The SLAM project Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages - POPL '02. ,vol. 37, pp. 1- 3 ,(2002) , 10.1145/503272.503274