Page 118 - 《软件学报》2021年第7期

2036 Journal of Software 软件学报 Vol.32, No.7, July 2021

[46] Wang J, Zhan N, Feng X, Liu Z. Overview of formal methods. Ruan Jian Xue Bao/Journal of Software, 2019,30(1):33–61 (in
Chinese with English abstract). http://www.jos.org.cn/9825-1000/5652.htm [doi: 10.13328/j.cnki.jos.005652]
[47] Owicki S, Gries D. An axiomatic proof technique for parallel programs i. Acta Informatica, 1976,6(4):319–340.
[48] Yang J, Hawblitzel C. Safe to the last instruction: Automated verification of a type-safe operating system. In: Proc. of the 31st
ACM SIGPLAN Conf. on Programming Language Design and Implementation (PLDI). New York: Association for Computing
Machinery, 2010. 99–110. [doi: 10.1145/1806596.1806610]
[49] Boogie: An intermediate verification language. 2020. https://www.microsoft.com/en-us/research/project/boogie-an-intermediate-
verification-language/
[50] Nelson L, Sigurbjarnarson H, Zhang K, Johnson D, Bornholt J, Torlak E, Wang X. Hyperkernel: Push-button verification of an os
kernel. In: Proc. of the 26th Symp. on Operating Systems Principles (SOSP). Shanghai: ACM, 2017. 252–269.
[51] Sigurbjarnarson H, Bornholt J, Torlak E, Wang X. Push-button verification of file systems via crash refinement. In: Proc. of the
12th USENIX Conf. on Operating Systems Design and Implementation. 2016. 1–16. [doi: 10.1145/3132747.3132748]
[52] Xu F, Fu M, Feng X, Zhang X, Zhang H, Li Z. A practical verification framework for preemptive OS kernels. In: Proc. of the Conf.
on Computer Aided Verification. Cham: Springer-Verlag, 2016. 59–79.
[53] Klein G, Andronick J, Elphinstone K, Murray T, Sewell T, Kolanski R, Heiser G. Comprehensive formal verification of an OS
microkernel. ACM Trans. on Computer Systems (TOCS), 2014,32(1):1–70. [doi: 10.1145/2560537]
[54] Merz S. Model checking: A tutorial overview. In: Summer School on Modeling and Verification of Parallel Processes. Berlin,
Heidelberg: Springer-Verlag, 2001. 3–38.
[55] Visser W, Havelund K, Brat G, Park S. Model checking programs. In: Proc. of the Conf. of Automated Software Engineering (ASE).
2003,10(2):203–232.
[56] Kim M, Hong S, Hong C, Kim T. Model-based kernel testing for concurrency bugs through counter example replay. Electronic
Notes in Theoretical Computer Science, 2009,253(2):21–36. [doi: 10.1016/j.entcs.2009.09.049]
[57] Holzmann GJ, Joshi R. Model-driven software verification. ACM Computing Surveys (CSUR), 2009,41(4):1–54. [doi: 10.1145/
1592434.1592438]
[58] Holzmann GJ. The model checker SPIN. IEEE Trans. on Software Engineering, 1997,23(5):279–295. [doi: 10.1109/32.588521]
[59] Flanagan C, Ave L, Freund SN. Type-based race detection for Java. In: Proc. of the ACM SIGPLAN 2000 Conf. on Programming
Language Design and Implementation (PLDI). 2000. 219–232. [doi: 10.1145/349299.349328]
[60] Sasturkar A, Agarwal R, Wang LQ, Stoller SD. Automated type-based analysis of data races and atomicity. In: Proc. of the 10th
ACM SIGPLAN Symp. on Principles and Practice of Parallel Programming. 2005. 83–94. [doi: 10.1145/1065944.1065956]
[61] Vojdani V, Apinis K, Rõtov V, et al. Static race detection for device drivers: The Goblint approach. In: Proc. of the 31st IEEE/ACM
Int’l Conf. on Automated Software Engineering (ASE). Singapore: ACM Press, 2016. 391–402.
[62] Kildall GA. A unified approach to global program optimization. In: Proc. of the 1st Annual ACM SIGACT-SIGPLAN Symp. on
Principles of Programming Languages (POPL). Boston: ACM Press, 1973. 194–206. [doi: 10.1145/512927.512945]
[63] Engler D, Ashcraft K. RacerX: Effective, static detection of race conditions and deadlocks. ACM SIGOPS Operating Systems
Review, 2003,37(5):237–252. [doi: 10.1145/1165389.945468]
[64] Bai JJ, Wang YP, Lawall J, Hu SM. DSAC: Effective static analysis of sleep-in-atomic-context bugs in kernel modules. In: Proc. of
the 2018 USENIX Annual Technical Conf. (USENIX ATC). 2018. 587–600.
[65] King JC. Symbolic execution and program testing. Communications of the ACM, 1976,19(7):385–394. [doi: 10.1145/360248.
360252]
[66] Tan L, Zhou Y, Padioleau Y. aComment: Mining annotations from comments and code to detect interrupt related concurrency bugs.
In: Proc. of the 33rd Int’l Conf. on Software Engineering (ICSE). IEEE, 2011. 11–20. [doi: 10.1145/1985793.1985796]
[67] Breuer PT, Valls MG. Static deadlock detection in the Linux kernel. In: Proc. of the Int’l Conf. on Reliable Software Technologies.
Berlin, Heidelberg: Springer-Verlag, 2004. 52–64.
[68] Hong S, Kim M. Effective pattern-driven concurrency bug detection for operating systems. Journal of Systems and Software, 2013,
86(2):377–388. [doi: 10.1016/j.jss.2012.08.063]