形式化方法概貌
|
摘要
形式化方法是基于严格数学基础,对计算机硬件和软件系统进行描述、开发和验证的技术.其数学基础建立在形式语言、语义和推理证明三位一体的形式逻辑系统之上.形式化方法已经以不同程度和不同方式愈来愈多地应用在计算系统生命周期的各个阶段.介绍了形式化方法的发展历程和基本方法体系;以形式规约和形式验证为主线,综述了形式化方法的理论、方法、工具和应用的现状,展示了形式化方法与软件学科其他领域的交叉和融合;分析了形式化方法的启示,并展望了其面临的发展机遇和未来趋势.形式化方法的发展和研究现状表明:其应用已经取得了长足的进步,在提高计算系统的可靠性和安全性方面发挥了重要作用.在当今软件日益成为社会基础设施的时代,形式化方法将与人工智能、网络空间安全、量子计算、生物计算等领域和方向交叉融合,得到更加广阔的应用.研究和建立这种交叉融合的理论和方法不仅重要,而且具有挑战性.
Formal methods are techniques with mathematical foundations for specifying, developing, and verifying computer software and hardware systems. Their mathematical foundations lie in formal logic systems, consisting of formal languages, semantics, and proof systems. Formal methods have been increasingly applied in different stages of the lifecycle of a computing system with appropriate levels of rigor. This paper reviews the historic development of formal methods. Focusing on specification and verification, the paper discusses and introduces the state-of-the-art mainstream formal methods in details, including their theories, techniques, tools, and applications. It is also shown that the relation between formal methods and other fields of computer science. Finally, the opportunities, trends, and challenges of formal methods are forseen. Formal methods have made significant progresses and played crucial roles to guarantee the safety and security of computing systems. Now software is becoming a fundamental infrastructure, it is believed that formal methods will gain much wider applications, especially when they are used in combination with other theories and methods such as those in artificial intelligence, cyber security, quantum computing, and bioinformatics. Research to achieving such seamless combinations is, however, both challenging and important.
Formal methods are techniques with mathematical foundations for specifying, developing, and verifying computer software and hardware systems. Their mathematical foundations lie in formal logic systems, consisting of formal languages, semantics, and proof systems. Formal methods have been increasingly applied in different stages of the lifecycle of a computing system with appropriate levels of rigor. This paper reviews the historic development of formal methods. Focusing on specification and verification, the paper discusses and introduces the state-of-the-art mainstream formal methods in details, including their theories, techniques, tools, and applications. It is also shown that the relation between formal methods and other fields of computer science. Finally, the opportunities, trends, and challenges of formal methods are forseen. Formal methods have made significant progresses and played crucial roles to guarantee the safety and security of computing systems. Now software is becoming a fundamental infrastructure, it is believed that formal methods will gain much wider applications, especially when they are used in combination with other theories and methods such as those in artificial intelligence, cyber security, quantum computing, and bioinformatics. Research to achieving such seamless combinations is, however, both challenging and important.
引文
[1] CCF Formal Methods Technical Committee. Advances and trends on formal methods. In:The Progress Report of Computer Science and Technology in China from 2017 to 2018. Beijing:China Machine Press, 2018. 1-68(in Chinese with English abstract).
[2] CCF Software Engineering Technical Committee. Software analysis:techniques, applications and trends. In:The Progress Report of Computer Science and Technology in China from 2015 to 2016. Beijing:China Machine Press, 2016. 56-114(in Chinese with English abstract).
[3] Zhang J, Zhang C, Xuan JF, Xiong YF, Wang QX, Liang B, Li L, Dou WS, Chen ZB, Chen LQ, Cai Y. Recent progress in program analysis. Ruan Jian Xue Bao/Journal of Software, 2019,30(1):80-109(in Chinese with English abstract). http://www.jos.org.cn/1000-9825/5651.htm[doi:10.13328/j.cnki.jos.005651]
[4] Ma XX, Liu XZ, Xie B, Yu P, Zhang T, Bu L, Jin Z, Li XD. Software development methods:Review and outlook. Ruan Jian Xue Bao/Journal of Software, 2019,30(1):3-21(in Chinese with English abstract). http://www.jos.org.cn/1000-9825/5650.htm[doi:10.13328/j.cnki.jos.005650]
[5] Turing A. Checking a large routine. Report of a Conf. on High Speed Automatic Calculating Machines, Cambridge University Math.Lab., 1949. 67-69.
[6] McCarthy J. Towards a mathematical science of computation. In:Proc. of the IFIP Congress. 1962. 21-28.
[7] Church A. A set of postulates for the foundation of logic. Annals of Mathematics, 1932,33(2):346-366.[doi:10.2307/1968337]
[8] Church A. An unsolvable problem of elementary number theory. American Journal of Mathematics, 1936,58(2):345-363.[doi:10.2307/2371045]
[9] Tygert M. Formal methods. http://www.princeton.edu/~hos/frs122/unixhist/formal.htm
[10] Floyd RW. Assigning meaning to programs. In:Schwartz JT, ed. Proc. of the Symp. on Applied Mathematics.A.M.S., 1967.19-32.
[11] McCarthy J. Recursive functions of symbolic expressions and their computation by machine, Part I. Communications of the ACM,1960,3(4):184-219.
[12] Petri CA, Reisig W. Petri net. Scholarpedia, 2008,3(4):6477.
[13] Hoare CAR. Communicating sequential processes. Communications of the ACM, 1978,21(8):666-677.
[14] Hoare CAR. Communicating sequential processes. In:Int'l Series in Computer Science. Prentice-Hall, 1985.
[15] Milner R. A Calculus of Communicating Systems. Springer-Verlag, 1980.
[16] Milner R. Communication and concurrency. In:Int'l Series in Computer Science. Prentice Hall, 1989.
[17] Hennessy M, Lin H. Symbolic bisimulations. Theoretical Computer Science, 1995,138(2):353-389.
[18] Pnueli A. The temporal logic of programs. In:Proc. of the 18th IEEE Symp. on Foundations of Computer. 1977. 46-57.
[19] Clarke EM, Emerson EA. Design and synthesis of synchronization skeletons using branching time temporal logic. In:Proc. of the Logic of Programs:Workshop. LNCS 131, Springer-Verlag, 1981. 52-71.
[20] Alur R, Henzinger TA. A really temporal logic. Journal of the ACM, 1994,41:181-204.
[21] Alur R, Dill D. A theory of timed automata. Theoretical Computer Science, 1994,126(2):183-235.
[22] Asarin E, Caspi P, Maler O. Timed regular expressions. Journal of the ACM, 2002,49(2):172-206.
[23] Reed GM, Roscoe AW. A timed model for communicating squential processes. In:Proc. of the Int'l Colloquium on Automata,Languages, and Programming. 1986. 314-323.
[24] Yi W. CCS+Time=An interleaving model for real time systems. In:Proc. of the Int'l Conf. on Automata, Languages and Programming. LNCS 510, Springer-Verlag, 1991. 217-228.
[25] Bjorner D, Jone CB. The Vienna development methods:The meta language. LNCS 61, Springer-Verlag, 1978.
[26] Bjorner D, Jone CB. Formal Specification and Software Developemnt. Prentice-Hall, 1982.
[27] Jones CB. Systematic Software Development Using VDM. 2nd ed., Prentice-Hall, 1990.
[28] Woodcock JCP, Davies J. Using Z:Specification, Proof and Fefinement. Prentice Hall, 1996.
[29] Abrial JR. Modeling in Event-B:System and Software Engineering. Cambridge University Press, 2009.
[30] George CW, Haff P, Havelund K, Haxthausen AE, Milne R, Nielsen CB, Prehn S, Wagner KR. The RAISE Specification Language.Prentice-Hall, 1992.
[31] George CW, Haxthausen AE, Hughes S, Milne R, Prehn S, Pedersen JS. The RAISE Development Method. Prentice-Hall, 1995.
[32] Futatsugi K, Diaconescu R. CafeOBJ Report the Language, Proof Techniques, and Methodologies for Object-Oriented Algebraic Specification. World Scientific, 1998.
[33] Lamport L. Specifying Systems:The TLA+Language and Tools for Hardware and Software Engineers. Addison-Wesley, 2002.
[34] He J, Li X, Liu Z. rCOS:A refinement calculus for object systems. Theoretical Computer Science, 2006,365(1-2):109-142.
[35] Liu SY, Offutt AJ, Ho-Stuart C, Sun Y, Ohba M. SOFL:A formal engineering methodology for industrial applications. IEEE Trans.on Software Engineering, 1998,24(1):24-45.
[36] CZT:Community Z tools. http://czt.sourceforge.net/eclipse/zeves/
[37] Event-B/Rodin. http://www.event-b.org/
[38] Tang ZS, et al. Temporal Logic Programming and Software Engineering. Beijing:Science Press, 2002(in Chinese).
[39] Goguen JA, Burstall RM. Institutions:Abstract model theory for specification and programming. Journal of the Association for Computing Machinery, 1992,39(1):95-146.
[40] Hoare CAR, He J. Unifying Theories of Programming. Prentice Hall, 1998,14:184-203.
[41] Chaff. https://www.princeton.edu/~chaff/software.html
[42] Z3. https://github.com/Z3Prover/z3
[43] CVC4. http://cvc4.cs.stanford.edu/web/
[44] ACL2. http://www.cs.utexas.edu/users/moore/acl2/
[45] The Isabelle proof assistant. https://isabelle.in.tum.de/
[46] The Coq proof assistant. https://coq.inria.fr/
[47] PVS specification and verification system. http://pvs.csl.sri.com/
[48] SMV. http://nusmv.fbk.eu/
[49] Holzmann GJ. The SPIN Model Checker, Primer and Reference Manual. Reading:Addison-Wesley, 2003.
[50] UPPAAL. http://www.uppaal.org/
[51] PRISM. https://www.prismmodelchecker.org
[52] Sun J, Liu Y, Dong JS. Model checking CSP revisited:Introducing a process analysis toolkit. In:Proc. of the Int'l Symp. on Leveraging Applications of Formal Methods, Verification and Validation. Springer-Verlag, 2008. 307-322.
[53] Pnueli A. Verification engineering:A future profession. In:Proc. of the Annual ACM Symp. on Principles of Distributed Computing. 1997. 7.
[54] Hoare CAR, Misra J, Leavens GT, Shankar N. The verified software initiaive:A manifesto. ACM Computing Surveys, 2009,41(4):22-31.
[55] He JF, Shan ZG, Wang J, Pu GG, Fang YF, Liu K, Zhao RZ, Zhang ZT. Review of the achievements of major research plan on“Trustworthy Software”. Science Foundation in China, 2018,32(3):291-296(in Chinese with English abstract).
[56] Liu K, Shan ZG, Wang J, He JF, Zhang ZT, Qin YW. Overview on major research plan of trustworthy software. Science Foundation in China, 2008,22(3):145-151(in Chinese with English abstract).
[57] Dong W, Chen L. Recent advances on trusted computing in China. Chinese Science Bulletin, 2012,57(35):4529-4532.
[58] Leroy X. A formally verified compiler back-end. Journal of Automated Reasoning, 2009,43(4):363-446.
[59] 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, 2014,32(1):2:1-2:70.
[60] CMACS. http://cmacs.cs.cmu.edu/
[61] EXCAPE. https://excape.cis.upenn.edu/
[62] DeepSpec. https://deepspec.org/main
[63] Fisher K, Launchbury J, Richards R. The HACMS program:Using formal methods to eliminate exploitable bugs. Philosophical Trans. on Mathematical, Physical, and Engineering Sciences, 2017,375(2104).[doi:10.1098/rsta.2015.0401]
[64] Wing JM. A specifier's introduction to formal methods. IEEE Computer, 1990,23(9):8-22.
[65] Astesiano E, Bidoit M, Kirchner H, Krieg-Brückner B, Mosses PD, Sannella D, Tarlecki A. CASL:The common algebraic specification language. Theoretical Computer Science, 2002,286(2):153-196.
[66] Futatsugi K, Goguen JA, Jouannaud JP, Meseguer J. Principles of OBJ2. In:Proc. of the 12th ACM SIGACT-SIGPLAN Symp. on Principles of Programming Languages. 1985. 52-66.
[67] Gaudel MC. Structuring and modularizing algebraic specifications:The PLUSS specification language, evolutions and perspectives.In:Proc. of the Annual Symp. on Theoretical Aspects of Computer Science. Springer-Verlag, 1992. 1-18.
[68] Guttag JV, Horning J. LARCH:Languages and Tools for Formal Specification. Springer-Verlag, 1993.
[69] Liskov B, Zilles S. Specification techniques for data abstractions. IEEE Trans. on Software Engineering, 1975,1(1):7-18.
[70] Meyer B. Object-Oriented Software Construction. Prentice Hall, 1988.
[71] Abadi M, Cardelli L. A Theory of Objects. Springer-Verlag, 2012.
[72] Paulson L. ML for the Working Programmer. Cambridge University Press, 1996.
[73] Abrial JR. The specification language Z:Syntax and semantics. Technical Report, Programming Research Group, Oxford University, 1980.
[74] Durr E, Van KJ. VDM++, a formal specification language for object-oriented designs. In:Proc. of the Computer Systems and Software Engineering. IEEE, 1992. 214-219.
[75] Smith G. The Object-Z Specification Language. Springer-Verlag, 2000.
[76] Abrial JR. The B-Book:Assigning Programs to Meanings. Cambridge University Press, 1996.
[77] Jackson D. Software Abstractions:Logic, Language, and Analysis. MIT Press, 2006.
[78] Gary T, Leavens AL, Baker CR. Preliminary design of JML:A behavioral interface specification language for Java. ACM SIGSOFT Software Engineering Notes, 2006,31(3):1-38.
[79] Bergstra JA, Klop JW. Algebra of communicating processes with abstraction. Theoretical Computer Science, 1985,37(85):77-121.
[80] He J. From CSP to hybrid systems. In:Classical Mind. Prentice Hall, 1994. 171-189.
[81] Zhou CC, Wang J, Ravn AP. A formal description of hybrid systems. In:Proc. of the Int'l Hybrid Systems Workshop.Springer-Verlag, 1995. 511-530.
[82] Zhan N, Wang S, Zhao H. Formal modelling, analysis and verification of hybrid systems. In:Proc. of the Unifying Theories of Programming and Formal Engineering Methods. Springer-Verlag, 2013. 207-281.
[83] Milner R. Communicating and Mobile Systems—The Pi-Calculus. Cambridge:Cambridge University Press, 1999.
[84] Cardelli L, Gordon AD. Mobile ambients. Theoretical Computer Science, 1998,240(1):177-213.
[85] Abadi M, Gordon AD. A calculus for cryptographic protocols:The Spi calculus. Information Computation, 1999,148(1):1-70.
[86] Jensen OH, Milner R. Bigraphs and transitions. In:Proc. of the ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages. ACM Press, 2003,38(1):38-49.
[87] Harel D. Statecharts:A visual formalism for complex systems. Science of Computer Programming, 1987,8(3):231-274.
[88] Alur R, Courcoubetis C, Halbwachs N, Henzinger T, Ho PH, Nicollin X, Olivero A, Sifakis J, Yovine S. The algorithmic analysis of hybrid systems. Theoretical Computer Science, 1995,138(1):3-34.
[89] Alur R, Courcoubetis C, Dill D. Model-Checking for probabilistic real-time systems. In:Proc of the Int'l Colloquium on Automata,Languages, and Programming. Springer-Verlag, 1991. 115-126.
[90] Pola G, Bujorianu M, Lygeros J, Benedetto MD. Stochastic hybrid models:An overview. In:Proc. of the Conf. on Analysis and Design of Hybrid Systems. Elsevier, 2003. 45-50.
[91] Lamport L. Proving the correctness of multiprocess programs. IEEE Trans. on Software Engineering, 1977,3(2):125-143.
[92] Alpern B, Schneider F. Recongnizing safety and liveness. Distributed Computing, 1987,2(3):117-126.
[93] Hoare CAR. An axiomatic basis for computer programming. Communications of the ACM, 1969,12(10):576-580.
[94] Dijkstra EW. A Discipline of Programming. Prentice Hall, 1976.
[95] Reynolds JC. Separation logic:A logic for shared mutable data structures. In:Proc. of the 17th IEEE Symp. on Logic in Computer Science. IEEE, 2002. 55-74.
[96] Owicki S, Gries D. An axiomatic proof technique for parallel programs I. Acta Informatica, 1976,6(4):319-340.
[97] Owicki S, Gries D. Verifying properties of parallel programs:An axiomatic approach. Communications of the ACM, 1976,19(5):279-285.
[98] Jones CB. Tentative steps toward a development method for interfering programs. ACM Trans. on Programming Languages and Systems, 1983,5(4):596-619.
[99] Xu Q, de Roever WP, He J. The rely-guarantee method for verifying shared variable concurrent programs. Formal Aspects of Computing, 1997,9(2):149-174.
[100] O'hearn PW. Resources, concurrency and local reasoning. In:Proc. of the Int'l Conf. on Concurrency Theory. Springer-Verlag,2004. 49-67.
[101] Brookes S, O'Hearn PW. Concurrent separation logic. ACM SIGLOG News, 2016,3(3):47-65.
[102] Svendsen K, Pichon-Pharabod J, Doko M, Lahav O, Vafeiadis V. A separation logic for a promising semantics. In:Proc. of the European Symp. on Programming. Springer-Verlag, 2018. 357-384.
[103] Pratt VR. Semantical consideration on Floyo-Hoare logic. In:Proc. of the Annual Symp. on Foundations of Computer Science.IEEE, 1976. 109-121.
[104] Kozen D. Results on the propositional mu-calculus. Theoretical Computer Science, 1983,27(3):333-354.
[105] Emerson A, Lei CL. Efficient model checking in fragments of the propositional mu-calculus. In:Proc of the Symp. on Logic in Computer Science. IEEE, 1986. 267-278.
[106] Janin D, Walukiewicz I. On the expressive completeness of the propositional mu-calculus with respect to monadic second order logic. In:Proc. of the Int'l Conf. on Concurrency Theory. 1996. 263-277.
[107] Manna Z, Pnueli A. The Temporal Logic of Reactive and Concurrent Systems:Specification. Springer-verlag, 1991.
[108] Emerson EA. Temporal and modal logic. In:Formal Models and Semantics. 1990. 995-1072.
[109] Clarke E, Emerson A. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. on Programming Languages and Systems, 1986,8(2):244-263.
[110] Lamport L. The temporal logic of actions. ACM Trans. on Programming Languages and Systems, 1994,16(3):872-923.
[111] Halpern J, Manna Z, Moszkowski B. A hardware semantics based on temporal intervals. In:Proc. of the Int'l Colloquium on Automata, Languages,&Programming. 1983. 278-291.
[112] Platzer A. Logical Analysis of Hybrid Systems—Proving Theorems for Complex Dynamics. Springer-Verlag, 2010.
[113] Koymans R. Specifying Message Passing and Time-Critical Systems with Temporal Logic. Springer-Verlag, 1992.
[114] Ognjanovic Z. Discrete linear-time probabilistic logics:Completeness, decidability and complexity. Journal of Logic and Computation, 2006,16(2):257-285.
[115] Hansson H, Jonsson B. A logic for reasoning about time and reliability. Formal Aspects of Computing, 1994,6(5):102-111.
[116] Zhou C, Hoare CAR, Anders PR. A calculus of durations. Information Processing Letters, 1991,40(5):269-276.
[117] Zhou C, Hansen M. Duration calculus:A formal approach to real-time systems. In:Proc. of the Monographs in Theoretical Computer Science. Springer-Verlag, 2004.
[118] Lu RQ. The formal semantics of computer languages. Beijing:Science Press, 1992(in Chinese).
[119] Zhou CC, Zhan NJ. Introduction to formal semantics. 2nd ed., Beijing:Science Press, 2017(in Chinese).
[120] Plotkin G. A structural approach to operational semantics. Journal of Logic and Algebraic Programming, 1981,60-61:17-139.
[121] O'Hearn PW, Yang H, Reynolds JC. Separation and information hiding. In:Proc. of the ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages. 2004. 268-280.
[122] Olmedo F, Kaminski BL, Katoen JP, et al. Reasoning about recursive probabilistic programs. In:Proc. of the 31st Annual ACM/IEEE Symp. on Logic in Computer Science. 2016. 672-681.
[123] Fiore M, Jung A, Moggi E, et al. Domains and denotational semantics:History, accomplishments and open problems. Bulletin of EATCS, 1996,59:227-256.
[124] Roscoe AW. Understanding Concurrent Systems. Springer-Verlag, 2010.
[125] Zhan NJ, Wang SL, Zhao HJ. Formal Verification of Simulink/Stateflow Diagrams:A Deductive Way. Springer-verlag, 2017.
[126] Smyth MB. Power domains and predicate transformers:A topological view. In:Proc. of the Int'l Colloquium on Automata,Languages,&Programming. 1983. 662-675.
[127] Lin HM. Characterization of relative completeness and abstract data type. Science in China Series A—Mathematics, Physics,Astronomy&Technological Science, 1998,18(6):658-664(in Chinese with English abstract).
[128] Rosu G, Serbanuta TF. An overview of the K semantic framework. Journal of Logic&Algebraic Programming, 2010,79(6):397-434.
[129] Bogdanas D, Rosu G. K-Java:A complete semantics of Java. In:Proc. of the ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages. ACM Press, 2015. 445-456.
[130] Rabin M. Automata on infinite objects and Church's problem. In:CBMS Regional Conf. Series in Mathematics. 1972.
[131] Liu Z, Chen X. Model-Driven design of object and component systems. In:Proc. of the Int'l School on Engineering Trustworthy Software Systems. Springer-Verlag, 2014. 152-255.
[132] Back, RJ, von Wright J. Refinement Calculus. Springer-Verlag, 1998.
[133] Morgan C. Programming from Specifications. 2nd ed., Prentice-Hall, 1998.
[134] Preoteasa V, Tripakis S. Refinement calculus of reactive systems. In:Proc. of the 14th Int'l Conf. on Embedded Software. ACM Press, 2014. 2:1-2:10.
[135] Dragomir I, Preoteasa V, Tripakis S. The refinement calculus of reactive systems toolset. In:Proc. of the Int'l Conf. on Tools and Algorithms for the Construction and Analysis of Systems. Springer-Verlag, 2018. 201-208.
[136] Liu Z, Joseph M. Specification and verification of fault-tolerance, timing, and scheduling. ACM Trans. on Programming Languages and Systems, 1999,21(1):46-89.
[137] Brooks FP. No silver bullet:Essence and accidents of software engineering. IEEE Computer, 1987,20(4):10-19.
[138] Church A. Logic, arithmetic and automata. In:Proc. of the Int'l Congress of Mathematicians. 1962. 23-35.
[139] Pnueli A, Rosner R. On the synthesis of a reactive module. In:Proc. of the 16th ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages. ACM Press, 1989. 179-190.
[140] Manna Z, Waldinger RJ. Knowledge and reasoning in program synthesis. Artificial Intelligence, 1975,6(2):175-208.
[141] Büchi JR, Landweber LH. Solving sequential conditions by finite-state strategies. Trans. of the American Mathematical Society,1969,138(1):295-311.
[142] Kolmogorov AN. Zur deutung der intuitionistischen logik. Mathematische Zeitschrift, 1932,35(1):58-65.
[143] Green C. Application of theorem proving to problem solving. In:Readings in Artificial Intelligence. 1981. 202-222.
[144] Manna Z, Waldinger RJ. Toward automatic program synthesis. Communications of the ACM, 1971,14(3):151-165.
[145] Waldinger RJ, Lee RC. PROW:A step toward automatic program writing. In:Proc. of the 1st Int'l Joint Conf. on Artificial Intelligence. Morgan Kaufmann Publishers, 1969. 241-252.
[146] Howard WA. The formulae-as-types notion of construction. To HB Curry:Essays on Combinatory Logic, Lambda Calculus and Formalism, 1980,44:479-490.
[147] Shaw D, Wartout W, Green C. Inferring LISP programs from examples. In:Proc. of the 4th Int'l Joint Conf. on Artificial Intelligence. Morgan Kaufmann Publishers, 1975. 260-267.
[148] Summers PD. A methodology for LISP program construction from examples. Journal of the ACM, 1977,24(1):161-175.
[149] Biermann AW. The inference of regular LISP programs from examples. IEEE Trans. on Systems, Man, and Cybernetics, 1978,8(8):585-600.
[150] Smith DC. Pygmalion:A creative programming environment[Ph.D. Thesis]. Stanford University, 1975.
[151] Koza JR. Genetic programming as a means for programming computers by natural selection. Statistics and Computing, 1994,4(2):87-112.
[152] Lezama SA, Bodik R. Program Synthesis by Sketching. Berkeley:University of California, 2008.
[153] Gulwani S. Automating string processing in spreadsheets using input-output examples. In:Proc. of the 38th ACM SIGPLANSIGACT Symp. on Principles of Programming Languages. ACM Press, 2011. 317-330.
[154] Gulwani S, Harris WR, Singh R. Spreadsheet data manipulation using examples. Communications of the ACM, 2012,55(8):97-105.
[155] Polozov O, Gulwani S. FlashMeta:A framework for inductive programsynthesis. In:Proc. of the 2015 ACM SIGPLAN Int'l Conf.on Object-Oriented Programming, Systems, Languages, and Applications. 2015. 107-126.
[156] Torlak E, Bodik R. Growing solver-aided languages with Rosette. In:Proc. of the 2013 ACM Int'l Symp. on New Ideas, New Paradigms, and Reflections on Programming&Software. ACM Press, 2013. 135-152.
[157] Gu R, Shao Z, Chen H, Wu X, Kim J, Sj(o|¨)berg V, Costanzo D. CertiKOS:An extensible architecture for building certified concurrent OS kernels. In:Proc. of the USENIX Symp. on Operating Systems Design and Implementation. 2016. 653-669.
[158] Benton N. Simple relational correctness proofs for static analyses and program transformations. In:Proc. of the ACM SIGPLANSIGACT Symp. on Principles of Programming Languages. ACM Press, 2004. 14-25.
[159] Yang H. Relational separation logic. Theoretical Computer Science, 2007,375(1-3):308-334.
[160] Beringer L, Hofmann M. Secure information flow and program logics. In:Proc. of the Computer Security Foundations Symp. IEEE,2007. 233-248.
[161] Aguirre A, Barthe G, Gaboardi M, Garg D, Strub PY. A relational logic for higher-order programs. In:Proc. of the ACM on Programming Languages. 2017. 21:1-21:29.
[162] Turon A, Dreyer D, Birkedal L. Unifying refinement and hoare-style reasoning in a logic for higher-order concurrency. In:Proc. of the Conf. on Functional Programming. 2013. 377-390.
[163] Liang H, Feng X. Modular verification of linearizability with non-fixed linearization points. In:Proc. of the ACM SIGPLAN Conf.on Programming Language Design and Implementation. ACM Press, 2013. 459-470.
[164] Sousa M, Dillig I. Cartesian Hoare logic for verifying k-safety properties. In:Proc. of the ACM SIGPLAN Conf. on Programming Language Design and Implementation. ACM Press, 2016. 57-69.
[165] Dafny. https://rise4fun.com/dafny
[166] Why3. http://why3.lri.fr/
[167] Verifast. https://github.com/verifast/verifast
[168] Berdine J, Calcagno C, O'Hearn PW. Smallfoot:Modular automatic assertion checking with separation logic. In:Proc. of the Int'l Symp. on Formal Methods for Components and Objects. 2005. 115-137.
[169] Yices 2. http://yices.csl.sri.com/
[170] Yang J, Hawblitzel C. Safe to the last instruction:Automated verification of a type-safe operating system. In:Proc. of the ACM SIGPLAN Conf. on Programming Language Design and Implementation. ACM Press, 2010. 99-110.
[171] Hawblitzel C, Howell J, Kapritsos M, Lorch JR, Parno B, Roberts ML, Setty S, Zill B. IronFleet:Proving practical distributed systems correct. In:Proc. of the Symp. on Operating Systems Principles. ACM Press, 2015. 1-17.
[172] Boogie. https://www.microsoft.com/en-us/research/project/boogie-an-intermediate-verification-language/
[173] 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 Symp. on Operating Systems Principles. ACM Press, 2017. 252-269.
[174] Sigurbjarnarson H, Bornholt J, Christin N, Cranor LF. Push-Button verification of file systems via crash refinement. In:Proc. of the USENIX Annual Technical Conf. 2017.
[175] Clarke EM, Emerson EA, Sistla AP. Automatic verification of finite-state concurrent systems using temporal logic specifications.ACM Trans. on Programming Languages and Systems. 1986,8(2):244-263.
[176] Queille JP, Sifakis J. Specification and verification of concurrent systems in CESAR. In:Proc. of the Int'l Symp. on Programming.Springer-Verlag, 1982. 337-351.
[177] Clarke EM, Grumberg O, Peled D. Model Checking. MIT Press, 1999.
[178] Clarke EM. The birth of model checking. In:Proc. of the 25 Years of Model Checking. Spinger-Verlag, 2008. 1-26.
[179] Clarke EM, Henzinger TA, Veith H, Bloem R. Handbook of Model Checking. Springer-Verlag, 2016.
[180] Clarke EM, Filkorn T, Jha S. Exploiting symmetry in temporal logic model checking. In:Proc. of the Formal Methods in System Design. Springer-Verlag, 1996,9(1-2):77-104.
[181] Emerson EA, Sistla AP. Symmetry and model checking. In:Proc. of the Formal Methods in System Design. Springer-Verlag, 1996,9(1-2):105-131.
[182] Ip CW, Dill DL. Better verification through symmetry. In:Proc. of the Formal Methods in System Design. Springer-Verlag, 1996,9(1-2):41-75.
[183] Gerth R, Peled D, Vardi M, Wolper P. Simple on-the-fly automatic verification of linear temporal logic. In:Dembinski P,Sredniawa M, eds. Proc. of the Int'l Symp. on Protocol Specification, Testing and Verification. 1995. 3-18.
[184] Vardi MY, Wolper P. An automata-theoretic approach to automatic program verification. In:Proc. of the Symp. on Logic in Computer Science. IEEE Computer Society, 1986. 322-331.
[185] Peled D. All from one, one for all:on model checking using representatives. In:Proc. of the Int'l Conf. on Computer Aided Verification. Springer-Verlag, 1993. 409-423.
[186] Valmari A. A stubborn attack on the state explosion problem. In:Proc. of the Formal Methods in System Design. Springer-Verlag,1992,1(4):297-322.
[187] Godefroid P. Using partial orders to improve automatic verification methods. In:Proc. of the Int'l Conf. on Computer Aided Verification. LNCS 531, Springer-Verlag, 1990. 176-185.
[188] Clarke EM, Grumberg O, Browne MC. Reasoning about networks with many identical finite-state processes. In:Proc. of the 5th Annual ACM Symp. on Principles of Distributed Computing. ACM Press, 1986. 240-248.
[189] German SM, Sistla AP. Reasoning about systems with many processes. Journal of the ACM, 1992,39(3):675-735.
[190] Burch JR, Clarke EM, McMillan KL, Dill DL, Hwang LJ. Symbolic model checking:1020 states and beyond. Information and Computation, 1992,98(2):142-170.
[191] Biere A, Cimatti A, Clarke E, Zhu Y. Symbolic model checking without BDDs. In:Proc. of the Int'l Conf. on Tools and Algorithms for the Construction and Analysis of Systems. Springer-Verlag, 1999. 193-207.
[192] Armando A, Mantovani J, Platania L. Bounded model checking of software using SMT solvers instead of SAT solvers. In:Proc. of the Workshop on Model Checking Software(SPIN). Springer-Verlag, 2006. 146-162.
[193] Clarke EM, Grumberg O, Long DE. Model checking and abstraction. ACM Trans. on Programming Languages and Systems,1994,16(5):1512-1542.
[194] Cousot P, Cousot R. Abstract interpretation:A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In:Proc. of the ACM SIGACT-SIGPLAN Symp. on Principles of Programming Languages. ACM Press,1977. 238-252.
[195] Cousot P, Cousot R. Abstract interpretation:Past, present and future. In:Proc. of the Joint Meeting of the 23rd EACSL Annual Conf. on Computer Science Logic and the 29th Annual ACM/IEEE Symp. on Logic in Computer Science. ACM Press, 2014.2:1-2:10.
[196] Bouajjani A, Esparza J, Maler O. Reachability analysis of pushdown automata:Application to model-checking. In:Proc. of the Int'l Conf. on Concurrency Theory. Springer-Verlag, 1997. 135-150.
[197] Alur R, Courcourbetis C, Dill D. Model-Checking for real-time systems. In:Proc. of the 5th Symp. on Logic in Computer Science.IEEE, 1990. 414-425.
[198] Henzinger TA, Kopke PW, Puri A, Varaiya P. What's decidable about hybrid automata? In:Proc. of the 27th Annual Symp. on Theory of Computing. ACM Press, 1995. 373-382.
[199] Alur R, Dill DL. Automata-Theoretic verification of real-time systems. In:Formal Methods for Real-Time Computing. 1996.55-82.
[200] Larsen KG, Pettersson P, Yi W. Uppaal in a nutshell. Int'l Journal on Software Tools for Technology Transfer, 1997,1(1-2):134-152.
[201] Forejt V, Kwiatkowska M, Norman G, Parker D. Automated verification techniques for probabilistic systems. In:Formal Methods for Eternal Networked Software Systems. Springer-Verlag, 2011. 53-113.
[202] Kwiatkowska M, Norman G, Parker D. PRISM 4.0:Verification of probabilistic real-time systems. In:Proc. of the 23rd Int'l Conf.on Computer Aided Verification(CAV 2011). Springer-Verlag, 2011. 585-591.
[203] Younes HL, Simmons RG. Probabilistic verification of discrete event systems using acceptance sampling. In:Proc. of the Int'l Conf. on Computer Aided Verification. Springer-Verlag, 2002. 223-235.
[204] Sen K, Viswanathan M, Agha G. On statistical model checking of stochastic systems. In:Proc. of the Int'l Conf. on Computer Aided Verification. Springer-Verlag, 2005. 266-280.
[205] Clarke E, Grumberg O, Jha S, Lu Y, Veith H. Counterexample-Guided abstraction refinement for symbolic model checking.Journal of the ACM, 2003,50(5):752-794.
[206] Ball T, Majumdar R, Millstein TD, Rajamani S. Automatic predicate abstraction of C programs. In:Proc. of the ACM SIGPLAN2001 Conf. on Programming Language Design and Implementation. ACM Press, 2001. 203-213.
[207] Thomas B, Cook B, Levin V, Rajamani SK. SLAM and static driver verifier:Technology transfer of formal methods inside Microsoft. In:Proc. of the Int'l Conf. on Integrated Formal Methods. Springer-Verlag, 2004. 1-20.
[208] Daniel K, Tautschnig M. CBMC—C bounded model checker. In:Proc. of the Int'l Conf. on Tools and Algorithms for the Construction and Analysis of Systems. Springer-Verlag, 2014. 389-391.
[209] Dirk B, Keremoglu ME. CPAchecker:A tool for configurable software verification. In:Proc. of the Int'l Conf. on Computer Aided Verification. Springer-Verlag, 2011. 184-190.
[210] Grebenshchikov S, Lopes NP, Popeea C, Rybalchenko A. Synthesize software verifiers from proof rules. In:Proc. of the PLDI2012. ACM Press, 2012. 405-416.
[211] Bjorner N, Gurfinkel A, McMillan K, Rybalchenko A. Horn clause solvers for program verification. In:Fields of Logic and Computation II:Essays Dedicated to Yuri Gurevich on the Occasion of His 75th Birthday. Springer-Verlag, 2015. 24-51.
[212] Clarke EM, Biere A, Raimi A, Zhu Y. Bounded model checking using satisfiability solving. Formal Methods in System Design,2001,19(1):7-34.
[213] Biere A, Cimatti A, Clarke EM, Strichman O, Zhu Y. Bounded model checking. Advances in Computers, 2003,58(11):117-148.
[214] Yin L, Dong W, Liu W, Wang J. On scheduling constraint abstraction for multi-threaded program verification. IEEE Trans. on Software Engineering. 2018.
[215] Clarke EM, Grumberg O, Hiraishi H, Jha S, Long DE, McMillan KL, Ness LA. Verification of the Futurebus+cache coherence protocol. In:Proc. of the Computer Hardware Description Languages and Their Applications. 1993. 15-30.
[216] Miller SP, Srivas M. Formal verification of the AAMP5 microprocessor. In:Proc. of the Workshop on Industrial—Strength Formal Specification Techniques Boca Raton. 1995. 125-180.
[217] Kaivola R, Ghughal R, Narasimhan N, Telfer A, Whittemore J, Pandav S, Slobodova A, Taylor C, Frolov V, Reeber E, Naik A.Replacing testing with formal verification in Intel CoreTM i7 processor execution engine validation. In:Proc. of the Int'l Conf. on Computer Aided Verification. Springer-Verlag, 2009. 414-429.
[218] Hinchey M, Bowen JP, Vassev E. Formal methods. In:Laplante PA, ed. Proc. of the Encyclopaedia of Software Engineering. 2010.308-320.
[219] Bjorner D, Havelund K. 40 years of formal methods. In:Proc. of the Int'l Symp. on Formal Methods. Springer-Verlag, 2014.42-61.
[220] Woodcock J, Larsen PG, Bicarregui J, Fitzgerald J. Formal methods:Practive and experience. ACM Computing Surveys, 2009,41(4):19:1-19:36.
[221] Moy Y, Wallenburg A. Tokeneer:Beyond formal program verification. In:Proc. of the Embedded Real Time Software and Systems.2010.
[222] Holzmann GJ. Mars code. Communications of the ACM, 2014,57(2):64-73.
[223] Zhao Y, Yang Z, Sanan D, Liu Y. Event-Based formalization of safety-critical operating system standards:An experience report on arinc 653 using event-b. In:Proc. of the IEEE Int'l Symp. on Software Reliability Engineering. IEEE, 2015. 281-292.
[224] Subramanyan P, Sinha R, Lebedev I, Devadas S, Seshia SA. A formal foundation for secure remote execution of enclaves. In:Proc.of the ACM SIGSAC Conf. on Computer and Communications Security. ACM Press, 2017. 2435-2450.
[225] Moore JS. System verification. Journal of Automated Reasoning, 1989.
[226] Xu F, Fu M, Feng X, Zhang X, Zhang H, Li Z. A practical verification framework for preemptive OS kernels. In:Proc. of the Int'l Conf. on Computer Aided Verification. Springer-Verlag, 2016. 59-79.
[227] Lesani M, Bell CJ, Chlipala A. Chapar:Certified causally consistent distributed key-value stores. In:Proc. of the ACM SIGPLANSIGACT Symp. on Principles of Programming Languages. ACM Press, 2016. 357-370.
[228] Appel AW. Verification of a cryptographic primitive:SHA-256. ACM Trans. on Programming Languages and Systems, 2015,37(2):7:1-7:31.
[229] Ye KQ, Green M, Sanguansin N, Beringer L, Petcher A, Appel AW. Verified correctness and security of mbedTLS HMAC-DRBG.In:Proc. of the ACM SIGSAC Conf. on Computer and Communications Security. ACM Press, 2017. 2007-2020.
[230] Chen H, Ziegler D, Chajed T, Chlipala A, Kaashoek MF, Zeldovich N. Using Crash Hoare logic for certifying the FSCQ file system.In:Proc. of the Symp. on Operating Systems Principles. ACM Press, 2015. 18-37.
[231] Chen H, Chajed T, Konradi A, Wang S, Ileri A, Chlipala A, Kaashoek MF, Zeldovich N. Verifying a high-performance crash-safe file system using a tree specification. In:Proc. of the Symp. on Operating Systems Principles. ACM Press, 2017. 270-286.
[232] Hunt GC, Larus JR. Singularity:Rethinking the software stack. Operating Systems Review, 2007,41(2):37-49.
[233] Larus JR, Hunt GC. The singularity system. Communications of the ACM, 2010,53(8):72-79.
[234] Necula G. Proof-Carrying code. In:Proc. of the ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages. ACM Press, 1997. 106-119.
[235] Morrisett G. Typed assembly language. In:Proc. of the Advanced Topics in Types and Programming Languages. 2002. 137-176.
[236] The rust language. https://www.rust-lang.org/
[237] Klein G, Andronick J, Fernandez M, Kuz I, Murray T, Heiser G. Fromally verified software in the real world. Communications of the ACM, 2018,61(10):68-77.
[238] Wang Y. Towards customizable CPS:Composability, efficiency and predictability. In:Proc. of the Int'l Conf. on Formal Engineering Methods. Springer-Verlag, 2017. 3-15.
[239] Seshia SA, Hu S, Li W, Zhu Q. Design automation of cyber-physical systems:Challenges, advances, and opportunities. IEEE Trans.on Computer-Aided Design of Integrated Circuits and Systems, 2017,36(9):1421-1434.
[240] Newcombe C, Rath T, Zhang F, Munteanu B, Brooker M, Deardeuff M. How Amazon Web services uses formal methods.Communications of the ACM, 2015,58(4):66-73.
[241] Formal verification might be built-in linux kernel in the future, message from linux foundation. https://linuxstory.org/en/tag/formalverification/
[242] Chong S, Guttman J, Datta A, Myers A, Pierce B, Schaumont P, Sherwood T, Zeldovich N. Report on the NSF Workshop on Formal Methods for Security, 2016.
[243] Ruso G. Formal design, implementation and verification of blockchain languages. In:Kirchner H, ed. Proc. of the Int'l Conf. on Formal Structures for Computation and Deduction. 2018. 2:1-2:6.
[244] Luu L, Chu DH, Olickel H, Saxena P, Hobor A. Making smart contracts smarter. In:Proc. of the ACM SIGSAC Conf. on Computer and Communications Security. ACM Press, 2016. 254-269.
[245] Gonthier G. Formal proof—The four-color theorem. Notices of the AMS, 2008,55(11):1382-1393.
[246] Dahn BI. Robbins algebras are Boolean:A revision of McCune's computer-generated solution of robbins problem. Journal of Algebra, 1998,208(2):526-532.
[247] Hales TC, Ferguson SP. A formulation of the Kepler conjecture. Discrete&Computational Geometry, 2006,36(1):21-69.
[248] Hales TC. A proof of the Kepler conjecture. Annals of Mathematics(2nd. Series), 2005,162(3):1065-1185.
[249] ALEXANDRIA. http://www.cl.cam.ac.uk/~1p15/Grants/Alexandria/
[250] Seshia SA, Sadigh D, Sastry SS. Towards verified artificial intelligence. arXiv Preprint arXiv:1606.08514. 2016.
[251] Selsam D, Liang P, Dill DL. Formal methods for probabilistic programming. In:Proc. of the Probabilistic Programming Languages,Semantics, and Systems. 2018.
[252] Ying M. Foundations of Quantum Programming. Morgan Kaufmann Publishers, 2016.
[253] Fisher J, Harel D, Henzinger TA. Biology as reactivity. Communications of the ACM, 2011,54(10):72-82.
[254] Miskov-Zivanov N, Zuliani P, Wang Q, Clarke EM, Faeder JR. High-Level modeling and verification of cellular signaling. In:Proc.of the Int'l High Level Design Validation and Test Workshop. IEEE, 2016. 162-169.
[255] Islam MA, Lim H, Paoletti N, Abbas H, Jiang Z, Cyranka J, Cleaveland R, Gao S, Clarke E, Grosu R,Mangharam R.CyberCardia project:Modeling, verification and validation of implantable cardiac devices. In:Proc. of the IEEE Int'l Conf. on Bioinformatics and Biomedicine. IEEE, 2016. 1445-1452.
[256] Joint Task Force on Computing Curricula(ACM and IEEE). Software Engineering 2014:Curriculum Guidelines for Undergraduate Degree Programs in Software Engineering. ACM Press, 2014. 10-19.
[257] Joint Task Force on Computing Curricula(ACM and IEEE). Computer Science Curricula 2013:Curriculum Guidelines for Undergraduate Degree Programs in Computer Science. New York:ACM Press, 2013.27-38.
[258] Liu B, Liu ZM, Qiu ZY, Qin X.On computer science education of undergraduate students to improve their understanding of program correctness and to develop their skills in developing correct programs. Computer Education, 2018(in Chinese).
[259] Hoare CAR. How did software get so reliable without proof? In:Proc. of the Int'l Symp. of Formal Methods Europe.Springer-Verlag, 1996. 1-17.
[1] CCF形式化方法专业委员会.形式化方法的研究进展与趋势.2017~2018中国计算机科学技术发展报告.北京:机械工业出版社,2018.1-68.
[2] CCF软件工程专业委员会.软件分析:技术、应用与趋势.2015-2016中国计算机科学技术发展报告.北京:机械工业出版社,2016.56-114.
[3]张健,张超,玄跻峰,熊英飞,王千祥,梁彬,李炼,窦文生,陈振邦,陈立前,蔡彦.程序分析研究进展.软件学报,2019,30(1):80-109.http://www.jos.org.cn/1000-9825/5651.htm[doi:10.13328/j.cnki.jos.005651]
[4]马晓星,刘譞哲,谢冰,余萍,张天,卜磊,李宣东.软件开法方法发展回顾与展望.软件学报,2019,30(1):3-21. http://www.jos.org.cn/1000-9825/5650.htm[doi:10.13328/j.cnki.jos.005650]
[38]唐稚松,等.时序逻辑程序设计与软件工程.北京:科学出版社,2002.
[55]何积丰,单志广,王戟,蒲戈光,房毓菲,刘克,赵瑞珍,张兆田.“可信软件基础研究”重大研究计划结题综述.中国科学基金,2018,32(3):291-296.
[57]刘克,单志广,王戟,何积丰,张兆田,秦玉文.“可信软件基础研究”重大研究计划综述.中国科学基金,2008,22(3):145-151.
[118]陆汝钤.计算机语言的形式语义.北京:科学出版社,1992.
[119]周巢尘,詹乃军.形式语义学引论.第2版,北京:科学出版社,2017.
[127]林惠民.相对完备性与抽象数据类型的描述.中国科学(A辑),1998,18(6):658-664.
[258]刘波,刘志明,裘宗燕,秦晓.加强计算机本科专业程序正确性知识教育与能力培养.计算机教育,2018.
[2] CCF Software Engineering Technical Committee. Software analysis:techniques, applications and trends. In:The Progress Report of Computer Science and Technology in China from 2015 to 2016. Beijing:China Machine Press, 2016. 56-114(in Chinese with English abstract).
[3] Zhang J, Zhang C, Xuan JF, Xiong YF, Wang QX, Liang B, Li L, Dou WS, Chen ZB, Chen LQ, Cai Y. Recent progress in program analysis. Ruan Jian Xue Bao/Journal of Software, 2019,30(1):80-109(in Chinese with English abstract). http://www.jos.org.cn/1000-9825/5651.htm[doi:10.13328/j.cnki.jos.005651]
[4] Ma XX, Liu XZ, Xie B, Yu P, Zhang T, Bu L, Jin Z, Li XD. Software development methods:Review and outlook. Ruan Jian Xue Bao/Journal of Software, 2019,30(1):3-21(in Chinese with English abstract). http://www.jos.org.cn/1000-9825/5650.htm[doi:10.13328/j.cnki.jos.005650]
[5] Turing A. Checking a large routine. Report of a Conf. on High Speed Automatic Calculating Machines, Cambridge University Math.Lab., 1949. 67-69.
[6] McCarthy J. Towards a mathematical science of computation. In:Proc. of the IFIP Congress. 1962. 21-28.
[7] Church A. A set of postulates for the foundation of logic. Annals of Mathematics, 1932,33(2):346-366.[doi:10.2307/1968337]
[8] Church A. An unsolvable problem of elementary number theory. American Journal of Mathematics, 1936,58(2):345-363.[doi:10.2307/2371045]
[9] Tygert M. Formal methods. http://www.princeton.edu/~hos/frs122/unixhist/formal.htm
[10] Floyd RW. Assigning meaning to programs. In:Schwartz JT, ed. Proc. of the Symp. on Applied Mathematics.A.M.S., 1967.19-32.
[11] McCarthy J. Recursive functions of symbolic expressions and their computation by machine, Part I. Communications of the ACM,1960,3(4):184-219.
[12] Petri CA, Reisig W. Petri net. Scholarpedia, 2008,3(4):6477.
[13] Hoare CAR. Communicating sequential processes. Communications of the ACM, 1978,21(8):666-677.
[14] Hoare CAR. Communicating sequential processes. In:Int'l Series in Computer Science. Prentice-Hall, 1985.
[15] Milner R. A Calculus of Communicating Systems. Springer-Verlag, 1980.
[16] Milner R. Communication and concurrency. In:Int'l Series in Computer Science. Prentice Hall, 1989.
[17] Hennessy M, Lin H. Symbolic bisimulations. Theoretical Computer Science, 1995,138(2):353-389.
[18] Pnueli A. The temporal logic of programs. In:Proc. of the 18th IEEE Symp. on Foundations of Computer. 1977. 46-57.
[19] Clarke EM, Emerson EA. Design and synthesis of synchronization skeletons using branching time temporal logic. In:Proc. of the Logic of Programs:Workshop. LNCS 131, Springer-Verlag, 1981. 52-71.
[20] Alur R, Henzinger TA. A really temporal logic. Journal of the ACM, 1994,41:181-204.
[21] Alur R, Dill D. A theory of timed automata. Theoretical Computer Science, 1994,126(2):183-235.
[22] Asarin E, Caspi P, Maler O. Timed regular expressions. Journal of the ACM, 2002,49(2):172-206.
[23] Reed GM, Roscoe AW. A timed model for communicating squential processes. In:Proc. of the Int'l Colloquium on Automata,Languages, and Programming. 1986. 314-323.
[24] Yi W. CCS+Time=An interleaving model for real time systems. In:Proc. of the Int'l Conf. on Automata, Languages and Programming. LNCS 510, Springer-Verlag, 1991. 217-228.
[25] Bjorner D, Jone CB. The Vienna development methods:The meta language. LNCS 61, Springer-Verlag, 1978.
[26] Bjorner D, Jone CB. Formal Specification and Software Developemnt. Prentice-Hall, 1982.
[27] Jones CB. Systematic Software Development Using VDM. 2nd ed., Prentice-Hall, 1990.
[28] Woodcock JCP, Davies J. Using Z:Specification, Proof and Fefinement. Prentice Hall, 1996.
[29] Abrial JR. Modeling in Event-B:System and Software Engineering. Cambridge University Press, 2009.
[30] George CW, Haff P, Havelund K, Haxthausen AE, Milne R, Nielsen CB, Prehn S, Wagner KR. The RAISE Specification Language.Prentice-Hall, 1992.
[31] George CW, Haxthausen AE, Hughes S, Milne R, Prehn S, Pedersen JS. The RAISE Development Method. Prentice-Hall, 1995.
[32] Futatsugi K, Diaconescu R. CafeOBJ Report the Language, Proof Techniques, and Methodologies for Object-Oriented Algebraic Specification. World Scientific, 1998.
[33] Lamport L. Specifying Systems:The TLA+Language and Tools for Hardware and Software Engineers. Addison-Wesley, 2002.
[34] He J, Li X, Liu Z. rCOS:A refinement calculus for object systems. Theoretical Computer Science, 2006,365(1-2):109-142.
[35] Liu SY, Offutt AJ, Ho-Stuart C, Sun Y, Ohba M. SOFL:A formal engineering methodology for industrial applications. IEEE Trans.on Software Engineering, 1998,24(1):24-45.
[36] CZT:Community Z tools. http://czt.sourceforge.net/eclipse/zeves/
[37] Event-B/Rodin. http://www.event-b.org/
[38] Tang ZS, et al. Temporal Logic Programming and Software Engineering. Beijing:Science Press, 2002(in Chinese).
[39] Goguen JA, Burstall RM. Institutions:Abstract model theory for specification and programming. Journal of the Association for Computing Machinery, 1992,39(1):95-146.
[40] Hoare CAR, He J. Unifying Theories of Programming. Prentice Hall, 1998,14:184-203.
[41] Chaff. https://www.princeton.edu/~chaff/software.html
[42] Z3. https://github.com/Z3Prover/z3
[43] CVC4. http://cvc4.cs.stanford.edu/web/
[44] ACL2. http://www.cs.utexas.edu/users/moore/acl2/
[45] The Isabelle proof assistant. https://isabelle.in.tum.de/
[46] The Coq proof assistant. https://coq.inria.fr/
[47] PVS specification and verification system. http://pvs.csl.sri.com/
[48] SMV. http://nusmv.fbk.eu/
[49] Holzmann GJ. The SPIN Model Checker, Primer and Reference Manual. Reading:Addison-Wesley, 2003.
[50] UPPAAL. http://www.uppaal.org/
[51] PRISM. https://www.prismmodelchecker.org
[52] Sun J, Liu Y, Dong JS. Model checking CSP revisited:Introducing a process analysis toolkit. In:Proc. of the Int'l Symp. on Leveraging Applications of Formal Methods, Verification and Validation. Springer-Verlag, 2008. 307-322.
[53] Pnueli A. Verification engineering:A future profession. In:Proc. of the Annual ACM Symp. on Principles of Distributed Computing. 1997. 7.
[54] Hoare CAR, Misra J, Leavens GT, Shankar N. The verified software initiaive:A manifesto. ACM Computing Surveys, 2009,41(4):22-31.
[55] He JF, Shan ZG, Wang J, Pu GG, Fang YF, Liu K, Zhao RZ, Zhang ZT. Review of the achievements of major research plan on“Trustworthy Software”. Science Foundation in China, 2018,32(3):291-296(in Chinese with English abstract).
[56] Liu K, Shan ZG, Wang J, He JF, Zhang ZT, Qin YW. Overview on major research plan of trustworthy software. Science Foundation in China, 2008,22(3):145-151(in Chinese with English abstract).
[57] Dong W, Chen L. Recent advances on trusted computing in China. Chinese Science Bulletin, 2012,57(35):4529-4532.
[58] Leroy X. A formally verified compiler back-end. Journal of Automated Reasoning, 2009,43(4):363-446.
[59] 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, 2014,32(1):2:1-2:70.
[60] CMACS. http://cmacs.cs.cmu.edu/
[61] EXCAPE. https://excape.cis.upenn.edu/
[62] DeepSpec. https://deepspec.org/main
[63] Fisher K, Launchbury J, Richards R. The HACMS program:Using formal methods to eliminate exploitable bugs. Philosophical Trans. on Mathematical, Physical, and Engineering Sciences, 2017,375(2104).[doi:10.1098/rsta.2015.0401]
[64] Wing JM. A specifier's introduction to formal methods. IEEE Computer, 1990,23(9):8-22.
[65] Astesiano E, Bidoit M, Kirchner H, Krieg-Brückner B, Mosses PD, Sannella D, Tarlecki A. CASL:The common algebraic specification language. Theoretical Computer Science, 2002,286(2):153-196.
[66] Futatsugi K, Goguen JA, Jouannaud JP, Meseguer J. Principles of OBJ2. In:Proc. of the 12th ACM SIGACT-SIGPLAN Symp. on Principles of Programming Languages. 1985. 52-66.
[67] Gaudel MC. Structuring and modularizing algebraic specifications:The PLUSS specification language, evolutions and perspectives.In:Proc. of the Annual Symp. on Theoretical Aspects of Computer Science. Springer-Verlag, 1992. 1-18.
[68] Guttag JV, Horning J. LARCH:Languages and Tools for Formal Specification. Springer-Verlag, 1993.
[69] Liskov B, Zilles S. Specification techniques for data abstractions. IEEE Trans. on Software Engineering, 1975,1(1):7-18.
[70] Meyer B. Object-Oriented Software Construction. Prentice Hall, 1988.
[71] Abadi M, Cardelli L. A Theory of Objects. Springer-Verlag, 2012.
[72] Paulson L. ML for the Working Programmer. Cambridge University Press, 1996.
[73] Abrial JR. The specification language Z:Syntax and semantics. Technical Report, Programming Research Group, Oxford University, 1980.
[74] Durr E, Van KJ. VDM++, a formal specification language for object-oriented designs. In:Proc. of the Computer Systems and Software Engineering. IEEE, 1992. 214-219.
[75] Smith G. The Object-Z Specification Language. Springer-Verlag, 2000.
[76] Abrial JR. The B-Book:Assigning Programs to Meanings. Cambridge University Press, 1996.
[77] Jackson D. Software Abstractions:Logic, Language, and Analysis. MIT Press, 2006.
[78] Gary T, Leavens AL, Baker CR. Preliminary design of JML:A behavioral interface specification language for Java. ACM SIGSOFT Software Engineering Notes, 2006,31(3):1-38.
[79] Bergstra JA, Klop JW. Algebra of communicating processes with abstraction. Theoretical Computer Science, 1985,37(85):77-121.
[80] He J. From CSP to hybrid systems. In:Classical Mind. Prentice Hall, 1994. 171-189.
[81] Zhou CC, Wang J, Ravn AP. A formal description of hybrid systems. In:Proc. of the Int'l Hybrid Systems Workshop.Springer-Verlag, 1995. 511-530.
[82] Zhan N, Wang S, Zhao H. Formal modelling, analysis and verification of hybrid systems. In:Proc. of the Unifying Theories of Programming and Formal Engineering Methods. Springer-Verlag, 2013. 207-281.
[83] Milner R. Communicating and Mobile Systems—The Pi-Calculus. Cambridge:Cambridge University Press, 1999.
[84] Cardelli L, Gordon AD. Mobile ambients. Theoretical Computer Science, 1998,240(1):177-213.
[85] Abadi M, Gordon AD. A calculus for cryptographic protocols:The Spi calculus. Information Computation, 1999,148(1):1-70.
[86] Jensen OH, Milner R. Bigraphs and transitions. In:Proc. of the ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages. ACM Press, 2003,38(1):38-49.
[87] Harel D. Statecharts:A visual formalism for complex systems. Science of Computer Programming, 1987,8(3):231-274.
[88] Alur R, Courcoubetis C, Halbwachs N, Henzinger T, Ho PH, Nicollin X, Olivero A, Sifakis J, Yovine S. The algorithmic analysis of hybrid systems. Theoretical Computer Science, 1995,138(1):3-34.
[89] Alur R, Courcoubetis C, Dill D. Model-Checking for probabilistic real-time systems. In:Proc of the Int'l Colloquium on Automata,Languages, and Programming. Springer-Verlag, 1991. 115-126.
[90] Pola G, Bujorianu M, Lygeros J, Benedetto MD. Stochastic hybrid models:An overview. In:Proc. of the Conf. on Analysis and Design of Hybrid Systems. Elsevier, 2003. 45-50.
[91] Lamport L. Proving the correctness of multiprocess programs. IEEE Trans. on Software Engineering, 1977,3(2):125-143.
[92] Alpern B, Schneider F. Recongnizing safety and liveness. Distributed Computing, 1987,2(3):117-126.
[93] Hoare CAR. An axiomatic basis for computer programming. Communications of the ACM, 1969,12(10):576-580.
[94] Dijkstra EW. A Discipline of Programming. Prentice Hall, 1976.
[95] Reynolds JC. Separation logic:A logic for shared mutable data structures. In:Proc. of the 17th IEEE Symp. on Logic in Computer Science. IEEE, 2002. 55-74.
[96] Owicki S, Gries D. An axiomatic proof technique for parallel programs I. Acta Informatica, 1976,6(4):319-340.
[97] Owicki S, Gries D. Verifying properties of parallel programs:An axiomatic approach. Communications of the ACM, 1976,19(5):279-285.
[98] Jones CB. Tentative steps toward a development method for interfering programs. ACM Trans. on Programming Languages and Systems, 1983,5(4):596-619.
[99] Xu Q, de Roever WP, He J. The rely-guarantee method for verifying shared variable concurrent programs. Formal Aspects of Computing, 1997,9(2):149-174.
[100] O'hearn PW. Resources, concurrency and local reasoning. In:Proc. of the Int'l Conf. on Concurrency Theory. Springer-Verlag,2004. 49-67.
[101] Brookes S, O'Hearn PW. Concurrent separation logic. ACM SIGLOG News, 2016,3(3):47-65.
[102] Svendsen K, Pichon-Pharabod J, Doko M, Lahav O, Vafeiadis V. A separation logic for a promising semantics. In:Proc. of the European Symp. on Programming. Springer-Verlag, 2018. 357-384.
[103] Pratt VR. Semantical consideration on Floyo-Hoare logic. In:Proc. of the Annual Symp. on Foundations of Computer Science.IEEE, 1976. 109-121.
[104] Kozen D. Results on the propositional mu-calculus. Theoretical Computer Science, 1983,27(3):333-354.
[105] Emerson A, Lei CL. Efficient model checking in fragments of the propositional mu-calculus. In:Proc of the Symp. on Logic in Computer Science. IEEE, 1986. 267-278.
[106] Janin D, Walukiewicz I. On the expressive completeness of the propositional mu-calculus with respect to monadic second order logic. In:Proc. of the Int'l Conf. on Concurrency Theory. 1996. 263-277.
[107] Manna Z, Pnueli A. The Temporal Logic of Reactive and Concurrent Systems:Specification. Springer-verlag, 1991.
[108] Emerson EA. Temporal and modal logic. In:Formal Models and Semantics. 1990. 995-1072.
[109] Clarke E, Emerson A. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. on Programming Languages and Systems, 1986,8(2):244-263.
[110] Lamport L. The temporal logic of actions. ACM Trans. on Programming Languages and Systems, 1994,16(3):872-923.
[111] Halpern J, Manna Z, Moszkowski B. A hardware semantics based on temporal intervals. In:Proc. of the Int'l Colloquium on Automata, Languages,&Programming. 1983. 278-291.
[112] Platzer A. Logical Analysis of Hybrid Systems—Proving Theorems for Complex Dynamics. Springer-Verlag, 2010.
[113] Koymans R. Specifying Message Passing and Time-Critical Systems with Temporal Logic. Springer-Verlag, 1992.
[114] Ognjanovic Z. Discrete linear-time probabilistic logics:Completeness, decidability and complexity. Journal of Logic and Computation, 2006,16(2):257-285.
[115] Hansson H, Jonsson B. A logic for reasoning about time and reliability. Formal Aspects of Computing, 1994,6(5):102-111.
[116] Zhou C, Hoare CAR, Anders PR. A calculus of durations. Information Processing Letters, 1991,40(5):269-276.
[117] Zhou C, Hansen M. Duration calculus:A formal approach to real-time systems. In:Proc. of the Monographs in Theoretical Computer Science. Springer-Verlag, 2004.
[118] Lu RQ. The formal semantics of computer languages. Beijing:Science Press, 1992(in Chinese).
[119] Zhou CC, Zhan NJ. Introduction to formal semantics. 2nd ed., Beijing:Science Press, 2017(in Chinese).
[120] Plotkin G. A structural approach to operational semantics. Journal of Logic and Algebraic Programming, 1981,60-61:17-139.
[121] O'Hearn PW, Yang H, Reynolds JC. Separation and information hiding. In:Proc. of the ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages. 2004. 268-280.
[122] Olmedo F, Kaminski BL, Katoen JP, et al. Reasoning about recursive probabilistic programs. In:Proc. of the 31st Annual ACM/IEEE Symp. on Logic in Computer Science. 2016. 672-681.
[123] Fiore M, Jung A, Moggi E, et al. Domains and denotational semantics:History, accomplishments and open problems. Bulletin of EATCS, 1996,59:227-256.
[124] Roscoe AW. Understanding Concurrent Systems. Springer-Verlag, 2010.
[125] Zhan NJ, Wang SL, Zhao HJ. Formal Verification of Simulink/Stateflow Diagrams:A Deductive Way. Springer-verlag, 2017.
[126] Smyth MB. Power domains and predicate transformers:A topological view. In:Proc. of the Int'l Colloquium on Automata,Languages,&Programming. 1983. 662-675.
[127] Lin HM. Characterization of relative completeness and abstract data type. Science in China Series A—Mathematics, Physics,Astronomy&Technological Science, 1998,18(6):658-664(in Chinese with English abstract).
[128] Rosu G, Serbanuta TF. An overview of the K semantic framework. Journal of Logic&Algebraic Programming, 2010,79(6):397-434.
[129] Bogdanas D, Rosu G. K-Java:A complete semantics of Java. In:Proc. of the ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages. ACM Press, 2015. 445-456.
[130] Rabin M. Automata on infinite objects and Church's problem. In:CBMS Regional Conf. Series in Mathematics. 1972.
[131] Liu Z, Chen X. Model-Driven design of object and component systems. In:Proc. of the Int'l School on Engineering Trustworthy Software Systems. Springer-Verlag, 2014. 152-255.
[132] Back, RJ, von Wright J. Refinement Calculus. Springer-Verlag, 1998.
[133] Morgan C. Programming from Specifications. 2nd ed., Prentice-Hall, 1998.
[134] Preoteasa V, Tripakis S. Refinement calculus of reactive systems. In:Proc. of the 14th Int'l Conf. on Embedded Software. ACM Press, 2014. 2:1-2:10.
[135] Dragomir I, Preoteasa V, Tripakis S. The refinement calculus of reactive systems toolset. In:Proc. of the Int'l Conf. on Tools and Algorithms for the Construction and Analysis of Systems. Springer-Verlag, 2018. 201-208.
[136] Liu Z, Joseph M. Specification and verification of fault-tolerance, timing, and scheduling. ACM Trans. on Programming Languages and Systems, 1999,21(1):46-89.
[137] Brooks FP. No silver bullet:Essence and accidents of software engineering. IEEE Computer, 1987,20(4):10-19.
[138] Church A. Logic, arithmetic and automata. In:Proc. of the Int'l Congress of Mathematicians. 1962. 23-35.
[139] Pnueli A, Rosner R. On the synthesis of a reactive module. In:Proc. of the 16th ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages. ACM Press, 1989. 179-190.
[140] Manna Z, Waldinger RJ. Knowledge and reasoning in program synthesis. Artificial Intelligence, 1975,6(2):175-208.
[141] Büchi JR, Landweber LH. Solving sequential conditions by finite-state strategies. Trans. of the American Mathematical Society,1969,138(1):295-311.
[142] Kolmogorov AN. Zur deutung der intuitionistischen logik. Mathematische Zeitschrift, 1932,35(1):58-65.
[143] Green C. Application of theorem proving to problem solving. In:Readings in Artificial Intelligence. 1981. 202-222.
[144] Manna Z, Waldinger RJ. Toward automatic program synthesis. Communications of the ACM, 1971,14(3):151-165.
[145] Waldinger RJ, Lee RC. PROW:A step toward automatic program writing. In:Proc. of the 1st Int'l Joint Conf. on Artificial Intelligence. Morgan Kaufmann Publishers, 1969. 241-252.
[146] Howard WA. The formulae-as-types notion of construction. To HB Curry:Essays on Combinatory Logic, Lambda Calculus and Formalism, 1980,44:479-490.
[147] Shaw D, Wartout W, Green C. Inferring LISP programs from examples. In:Proc. of the 4th Int'l Joint Conf. on Artificial Intelligence. Morgan Kaufmann Publishers, 1975. 260-267.
[148] Summers PD. A methodology for LISP program construction from examples. Journal of the ACM, 1977,24(1):161-175.
[149] Biermann AW. The inference of regular LISP programs from examples. IEEE Trans. on Systems, Man, and Cybernetics, 1978,8(8):585-600.
[150] Smith DC. Pygmalion:A creative programming environment[Ph.D. Thesis]. Stanford University, 1975.
[151] Koza JR. Genetic programming as a means for programming computers by natural selection. Statistics and Computing, 1994,4(2):87-112.
[152] Lezama SA, Bodik R. Program Synthesis by Sketching. Berkeley:University of California, 2008.
[153] Gulwani S. Automating string processing in spreadsheets using input-output examples. In:Proc. of the 38th ACM SIGPLANSIGACT Symp. on Principles of Programming Languages. ACM Press, 2011. 317-330.
[154] Gulwani S, Harris WR, Singh R. Spreadsheet data manipulation using examples. Communications of the ACM, 2012,55(8):97-105.
[155] Polozov O, Gulwani S. FlashMeta:A framework for inductive programsynthesis. In:Proc. of the 2015 ACM SIGPLAN Int'l Conf.on Object-Oriented Programming, Systems, Languages, and Applications. 2015. 107-126.
[156] Torlak E, Bodik R. Growing solver-aided languages with Rosette. In:Proc. of the 2013 ACM Int'l Symp. on New Ideas, New Paradigms, and Reflections on Programming&Software. ACM Press, 2013. 135-152.
[157] Gu R, Shao Z, Chen H, Wu X, Kim J, Sj(o|¨)berg V, Costanzo D. CertiKOS:An extensible architecture for building certified concurrent OS kernels. In:Proc. of the USENIX Symp. on Operating Systems Design and Implementation. 2016. 653-669.
[158] Benton N. Simple relational correctness proofs for static analyses and program transformations. In:Proc. of the ACM SIGPLANSIGACT Symp. on Principles of Programming Languages. ACM Press, 2004. 14-25.
[159] Yang H. Relational separation logic. Theoretical Computer Science, 2007,375(1-3):308-334.
[160] Beringer L, Hofmann M. Secure information flow and program logics. In:Proc. of the Computer Security Foundations Symp. IEEE,2007. 233-248.
[161] Aguirre A, Barthe G, Gaboardi M, Garg D, Strub PY. A relational logic for higher-order programs. In:Proc. of the ACM on Programming Languages. 2017. 21:1-21:29.
[162] Turon A, Dreyer D, Birkedal L. Unifying refinement and hoare-style reasoning in a logic for higher-order concurrency. In:Proc. of the Conf. on Functional Programming. 2013. 377-390.
[163] Liang H, Feng X. Modular verification of linearizability with non-fixed linearization points. In:Proc. of the ACM SIGPLAN Conf.on Programming Language Design and Implementation. ACM Press, 2013. 459-470.
[164] Sousa M, Dillig I. Cartesian Hoare logic for verifying k-safety properties. In:Proc. of the ACM SIGPLAN Conf. on Programming Language Design and Implementation. ACM Press, 2016. 57-69.
[165] Dafny. https://rise4fun.com/dafny
[166] Why3. http://why3.lri.fr/
[167] Verifast. https://github.com/verifast/verifast
[168] Berdine J, Calcagno C, O'Hearn PW. Smallfoot:Modular automatic assertion checking with separation logic. In:Proc. of the Int'l Symp. on Formal Methods for Components and Objects. 2005. 115-137.
[169] Yices 2. http://yices.csl.sri.com/
[170] Yang J, Hawblitzel C. Safe to the last instruction:Automated verification of a type-safe operating system. In:Proc. of the ACM SIGPLAN Conf. on Programming Language Design and Implementation. ACM Press, 2010. 99-110.
[171] Hawblitzel C, Howell J, Kapritsos M, Lorch JR, Parno B, Roberts ML, Setty S, Zill B. IronFleet:Proving practical distributed systems correct. In:Proc. of the Symp. on Operating Systems Principles. ACM Press, 2015. 1-17.
[172] Boogie. https://www.microsoft.com/en-us/research/project/boogie-an-intermediate-verification-language/
[173] 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 Symp. on Operating Systems Principles. ACM Press, 2017. 252-269.
[174] Sigurbjarnarson H, Bornholt J, Christin N, Cranor LF. Push-Button verification of file systems via crash refinement. In:Proc. of the USENIX Annual Technical Conf. 2017.
[175] Clarke EM, Emerson EA, Sistla AP. Automatic verification of finite-state concurrent systems using temporal logic specifications.ACM Trans. on Programming Languages and Systems. 1986,8(2):244-263.
[176] Queille JP, Sifakis J. Specification and verification of concurrent systems in CESAR. In:Proc. of the Int'l Symp. on Programming.Springer-Verlag, 1982. 337-351.
[177] Clarke EM, Grumberg O, Peled D. Model Checking. MIT Press, 1999.
[178] Clarke EM. The birth of model checking. In:Proc. of the 25 Years of Model Checking. Spinger-Verlag, 2008. 1-26.
[179] Clarke EM, Henzinger TA, Veith H, Bloem R. Handbook of Model Checking. Springer-Verlag, 2016.
[180] Clarke EM, Filkorn T, Jha S. Exploiting symmetry in temporal logic model checking. In:Proc. of the Formal Methods in System Design. Springer-Verlag, 1996,9(1-2):77-104.
[181] Emerson EA, Sistla AP. Symmetry and model checking. In:Proc. of the Formal Methods in System Design. Springer-Verlag, 1996,9(1-2):105-131.
[182] Ip CW, Dill DL. Better verification through symmetry. In:Proc. of the Formal Methods in System Design. Springer-Verlag, 1996,9(1-2):41-75.
[183] Gerth R, Peled D, Vardi M, Wolper P. Simple on-the-fly automatic verification of linear temporal logic. In:Dembinski P,Sredniawa M, eds. Proc. of the Int'l Symp. on Protocol Specification, Testing and Verification. 1995. 3-18.
[184] Vardi MY, Wolper P. An automata-theoretic approach to automatic program verification. In:Proc. of the Symp. on Logic in Computer Science. IEEE Computer Society, 1986. 322-331.
[185] Peled D. All from one, one for all:on model checking using representatives. In:Proc. of the Int'l Conf. on Computer Aided Verification. Springer-Verlag, 1993. 409-423.
[186] Valmari A. A stubborn attack on the state explosion problem. In:Proc. of the Formal Methods in System Design. Springer-Verlag,1992,1(4):297-322.
[187] Godefroid P. Using partial orders to improve automatic verification methods. In:Proc. of the Int'l Conf. on Computer Aided Verification. LNCS 531, Springer-Verlag, 1990. 176-185.
[188] Clarke EM, Grumberg O, Browne MC. Reasoning about networks with many identical finite-state processes. In:Proc. of the 5th Annual ACM Symp. on Principles of Distributed Computing. ACM Press, 1986. 240-248.
[189] German SM, Sistla AP. Reasoning about systems with many processes. Journal of the ACM, 1992,39(3):675-735.
[190] Burch JR, Clarke EM, McMillan KL, Dill DL, Hwang LJ. Symbolic model checking:1020 states and beyond. Information and Computation, 1992,98(2):142-170.
[191] Biere A, Cimatti A, Clarke E, Zhu Y. Symbolic model checking without BDDs. In:Proc. of the Int'l Conf. on Tools and Algorithms for the Construction and Analysis of Systems. Springer-Verlag, 1999. 193-207.
[192] Armando A, Mantovani J, Platania L. Bounded model checking of software using SMT solvers instead of SAT solvers. In:Proc. of the Workshop on Model Checking Software(SPIN). Springer-Verlag, 2006. 146-162.
[193] Clarke EM, Grumberg O, Long DE. Model checking and abstraction. ACM Trans. on Programming Languages and Systems,1994,16(5):1512-1542.
[194] Cousot P, Cousot R. Abstract interpretation:A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In:Proc. of the ACM SIGACT-SIGPLAN Symp. on Principles of Programming Languages. ACM Press,1977. 238-252.
[195] Cousot P, Cousot R. Abstract interpretation:Past, present and future. In:Proc. of the Joint Meeting of the 23rd EACSL Annual Conf. on Computer Science Logic and the 29th Annual ACM/IEEE Symp. on Logic in Computer Science. ACM Press, 2014.2:1-2:10.
[196] Bouajjani A, Esparza J, Maler O. Reachability analysis of pushdown automata:Application to model-checking. In:Proc. of the Int'l Conf. on Concurrency Theory. Springer-Verlag, 1997. 135-150.
[197] Alur R, Courcourbetis C, Dill D. Model-Checking for real-time systems. In:Proc. of the 5th Symp. on Logic in Computer Science.IEEE, 1990. 414-425.
[198] Henzinger TA, Kopke PW, Puri A, Varaiya P. What's decidable about hybrid automata? In:Proc. of the 27th Annual Symp. on Theory of Computing. ACM Press, 1995. 373-382.
[199] Alur R, Dill DL. Automata-Theoretic verification of real-time systems. In:Formal Methods for Real-Time Computing. 1996.55-82.
[200] Larsen KG, Pettersson P, Yi W. Uppaal in a nutshell. Int'l Journal on Software Tools for Technology Transfer, 1997,1(1-2):134-152.
[201] Forejt V, Kwiatkowska M, Norman G, Parker D. Automated verification techniques for probabilistic systems. In:Formal Methods for Eternal Networked Software Systems. Springer-Verlag, 2011. 53-113.
[202] Kwiatkowska M, Norman G, Parker D. PRISM 4.0:Verification of probabilistic real-time systems. In:Proc. of the 23rd Int'l Conf.on Computer Aided Verification(CAV 2011). Springer-Verlag, 2011. 585-591.
[203] Younes HL, Simmons RG. Probabilistic verification of discrete event systems using acceptance sampling. In:Proc. of the Int'l Conf. on Computer Aided Verification. Springer-Verlag, 2002. 223-235.
[204] Sen K, Viswanathan M, Agha G. On statistical model checking of stochastic systems. In:Proc. of the Int'l Conf. on Computer Aided Verification. Springer-Verlag, 2005. 266-280.
[205] Clarke E, Grumberg O, Jha S, Lu Y, Veith H. Counterexample-Guided abstraction refinement for symbolic model checking.Journal of the ACM, 2003,50(5):752-794.
[206] Ball T, Majumdar R, Millstein TD, Rajamani S. Automatic predicate abstraction of C programs. In:Proc. of the ACM SIGPLAN2001 Conf. on Programming Language Design and Implementation. ACM Press, 2001. 203-213.
[207] Thomas B, Cook B, Levin V, Rajamani SK. SLAM and static driver verifier:Technology transfer of formal methods inside Microsoft. In:Proc. of the Int'l Conf. on Integrated Formal Methods. Springer-Verlag, 2004. 1-20.
[208] Daniel K, Tautschnig M. CBMC—C bounded model checker. In:Proc. of the Int'l Conf. on Tools and Algorithms for the Construction and Analysis of Systems. Springer-Verlag, 2014. 389-391.
[209] Dirk B, Keremoglu ME. CPAchecker:A tool for configurable software verification. In:Proc. of the Int'l Conf. on Computer Aided Verification. Springer-Verlag, 2011. 184-190.
[210] Grebenshchikov S, Lopes NP, Popeea C, Rybalchenko A. Synthesize software verifiers from proof rules. In:Proc. of the PLDI2012. ACM Press, 2012. 405-416.
[211] Bjorner N, Gurfinkel A, McMillan K, Rybalchenko A. Horn clause solvers for program verification. In:Fields of Logic and Computation II:Essays Dedicated to Yuri Gurevich on the Occasion of His 75th Birthday. Springer-Verlag, 2015. 24-51.
[212] Clarke EM, Biere A, Raimi A, Zhu Y. Bounded model checking using satisfiability solving. Formal Methods in System Design,2001,19(1):7-34.
[213] Biere A, Cimatti A, Clarke EM, Strichman O, Zhu Y. Bounded model checking. Advances in Computers, 2003,58(11):117-148.
[214] Yin L, Dong W, Liu W, Wang J. On scheduling constraint abstraction for multi-threaded program verification. IEEE Trans. on Software Engineering. 2018.
[215] Clarke EM, Grumberg O, Hiraishi H, Jha S, Long DE, McMillan KL, Ness LA. Verification of the Futurebus+cache coherence protocol. In:Proc. of the Computer Hardware Description Languages and Their Applications. 1993. 15-30.
[216] Miller SP, Srivas M. Formal verification of the AAMP5 microprocessor. In:Proc. of the Workshop on Industrial—Strength Formal Specification Techniques Boca Raton. 1995. 125-180.
[217] Kaivola R, Ghughal R, Narasimhan N, Telfer A, Whittemore J, Pandav S, Slobodova A, Taylor C, Frolov V, Reeber E, Naik A.Replacing testing with formal verification in Intel CoreTM i7 processor execution engine validation. In:Proc. of the Int'l Conf. on Computer Aided Verification. Springer-Verlag, 2009. 414-429.
[218] Hinchey M, Bowen JP, Vassev E. Formal methods. In:Laplante PA, ed. Proc. of the Encyclopaedia of Software Engineering. 2010.308-320.
[219] Bjorner D, Havelund K. 40 years of formal methods. In:Proc. of the Int'l Symp. on Formal Methods. Springer-Verlag, 2014.42-61.
[220] Woodcock J, Larsen PG, Bicarregui J, Fitzgerald J. Formal methods:Practive and experience. ACM Computing Surveys, 2009,41(4):19:1-19:36.
[221] Moy Y, Wallenburg A. Tokeneer:Beyond formal program verification. In:Proc. of the Embedded Real Time Software and Systems.2010.
[222] Holzmann GJ. Mars code. Communications of the ACM, 2014,57(2):64-73.
[223] Zhao Y, Yang Z, Sanan D, Liu Y. Event-Based formalization of safety-critical operating system standards:An experience report on arinc 653 using event-b. In:Proc. of the IEEE Int'l Symp. on Software Reliability Engineering. IEEE, 2015. 281-292.
[224] Subramanyan P, Sinha R, Lebedev I, Devadas S, Seshia SA. A formal foundation for secure remote execution of enclaves. In:Proc.of the ACM SIGSAC Conf. on Computer and Communications Security. ACM Press, 2017. 2435-2450.
[225] Moore JS. System verification. Journal of Automated Reasoning, 1989.
[226] Xu F, Fu M, Feng X, Zhang X, Zhang H, Li Z. A practical verification framework for preemptive OS kernels. In:Proc. of the Int'l Conf. on Computer Aided Verification. Springer-Verlag, 2016. 59-79.
[227] Lesani M, Bell CJ, Chlipala A. Chapar:Certified causally consistent distributed key-value stores. In:Proc. of the ACM SIGPLANSIGACT Symp. on Principles of Programming Languages. ACM Press, 2016. 357-370.
[228] Appel AW. Verification of a cryptographic primitive:SHA-256. ACM Trans. on Programming Languages and Systems, 2015,37(2):7:1-7:31.
[229] Ye KQ, Green M, Sanguansin N, Beringer L, Petcher A, Appel AW. Verified correctness and security of mbedTLS HMAC-DRBG.In:Proc. of the ACM SIGSAC Conf. on Computer and Communications Security. ACM Press, 2017. 2007-2020.
[230] Chen H, Ziegler D, Chajed T, Chlipala A, Kaashoek MF, Zeldovich N. Using Crash Hoare logic for certifying the FSCQ file system.In:Proc. of the Symp. on Operating Systems Principles. ACM Press, 2015. 18-37.
[231] Chen H, Chajed T, Konradi A, Wang S, Ileri A, Chlipala A, Kaashoek MF, Zeldovich N. Verifying a high-performance crash-safe file system using a tree specification. In:Proc. of the Symp. on Operating Systems Principles. ACM Press, 2017. 270-286.
[232] Hunt GC, Larus JR. Singularity:Rethinking the software stack. Operating Systems Review, 2007,41(2):37-49.
[233] Larus JR, Hunt GC. The singularity system. Communications of the ACM, 2010,53(8):72-79.
[234] Necula G. Proof-Carrying code. In:Proc. of the ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages. ACM Press, 1997. 106-119.
[235] Morrisett G. Typed assembly language. In:Proc. of the Advanced Topics in Types and Programming Languages. 2002. 137-176.
[236] The rust language. https://www.rust-lang.org/
[237] Klein G, Andronick J, Fernandez M, Kuz I, Murray T, Heiser G. Fromally verified software in the real world. Communications of the ACM, 2018,61(10):68-77.
[238] Wang Y. Towards customizable CPS:Composability, efficiency and predictability. In:Proc. of the Int'l Conf. on Formal Engineering Methods. Springer-Verlag, 2017. 3-15.
[239] Seshia SA, Hu S, Li W, Zhu Q. Design automation of cyber-physical systems:Challenges, advances, and opportunities. IEEE Trans.on Computer-Aided Design of Integrated Circuits and Systems, 2017,36(9):1421-1434.
[240] Newcombe C, Rath T, Zhang F, Munteanu B, Brooker M, Deardeuff M. How Amazon Web services uses formal methods.Communications of the ACM, 2015,58(4):66-73.
[241] Formal verification might be built-in linux kernel in the future, message from linux foundation. https://linuxstory.org/en/tag/formalverification/
[242] Chong S, Guttman J, Datta A, Myers A, Pierce B, Schaumont P, Sherwood T, Zeldovich N. Report on the NSF Workshop on Formal Methods for Security, 2016.
[243] Ruso G. Formal design, implementation and verification of blockchain languages. In:Kirchner H, ed. Proc. of the Int'l Conf. on Formal Structures for Computation and Deduction. 2018. 2:1-2:6.
[244] Luu L, Chu DH, Olickel H, Saxena P, Hobor A. Making smart contracts smarter. In:Proc. of the ACM SIGSAC Conf. on Computer and Communications Security. ACM Press, 2016. 254-269.
[245] Gonthier G. Formal proof—The four-color theorem. Notices of the AMS, 2008,55(11):1382-1393.
[246] Dahn BI. Robbins algebras are Boolean:A revision of McCune's computer-generated solution of robbins problem. Journal of Algebra, 1998,208(2):526-532.
[247] Hales TC, Ferguson SP. A formulation of the Kepler conjecture. Discrete&Computational Geometry, 2006,36(1):21-69.
[248] Hales TC. A proof of the Kepler conjecture. Annals of Mathematics(2nd. Series), 2005,162(3):1065-1185.
[249] ALEXANDRIA. http://www.cl.cam.ac.uk/~1p15/Grants/Alexandria/
[250] Seshia SA, Sadigh D, Sastry SS. Towards verified artificial intelligence. arXiv Preprint arXiv:1606.08514. 2016.
[251] Selsam D, Liang P, Dill DL. Formal methods for probabilistic programming. In:Proc. of the Probabilistic Programming Languages,Semantics, and Systems. 2018.
[252] Ying M. Foundations of Quantum Programming. Morgan Kaufmann Publishers, 2016.
[253] Fisher J, Harel D, Henzinger TA. Biology as reactivity. Communications of the ACM, 2011,54(10):72-82.
[254] Miskov-Zivanov N, Zuliani P, Wang Q, Clarke EM, Faeder JR. High-Level modeling and verification of cellular signaling. In:Proc.of the Int'l High Level Design Validation and Test Workshop. IEEE, 2016. 162-169.
[255] Islam MA, Lim H, Paoletti N, Abbas H, Jiang Z, Cyranka J, Cleaveland R, Gao S, Clarke E, Grosu R,Mangharam R.CyberCardia project:Modeling, verification and validation of implantable cardiac devices. In:Proc. of the IEEE Int'l Conf. on Bioinformatics and Biomedicine. IEEE, 2016. 1445-1452.
[256] Joint Task Force on Computing Curricula(ACM and IEEE). Software Engineering 2014:Curriculum Guidelines for Undergraduate Degree Programs in Software Engineering. ACM Press, 2014. 10-19.
[257] Joint Task Force on Computing Curricula(ACM and IEEE). Computer Science Curricula 2013:Curriculum Guidelines for Undergraduate Degree Programs in Computer Science. New York:ACM Press, 2013.27-38.
[258] Liu B, Liu ZM, Qiu ZY, Qin X.On computer science education of undergraduate students to improve their understanding of program correctness and to develop their skills in developing correct programs. Computer Education, 2018(in Chinese).
[259] Hoare CAR. How did software get so reliable without proof? In:Proc. of the Int'l Symp. of Formal Methods Europe.Springer-Verlag, 1996. 1-17.
[1] CCF形式化方法专业委员会.形式化方法的研究进展与趋势.2017~2018中国计算机科学技术发展报告.北京:机械工业出版社,2018.1-68.
[2] CCF软件工程专业委员会.软件分析:技术、应用与趋势.2015-2016中国计算机科学技术发展报告.北京:机械工业出版社,2016.56-114.
[3]张健,张超,玄跻峰,熊英飞,王千祥,梁彬,李炼,窦文生,陈振邦,陈立前,蔡彦.程序分析研究进展.软件学报,2019,30(1):80-109.http://www.jos.org.cn/1000-9825/5651.htm[doi:10.13328/j.cnki.jos.005651]
[4]马晓星,刘譞哲,谢冰,余萍,张天,卜磊,李宣东.软件开法方法发展回顾与展望.软件学报,2019,30(1):3-21. http://www.jos.org.cn/1000-9825/5650.htm[doi:10.13328/j.cnki.jos.005650]
[38]唐稚松,等.时序逻辑程序设计与软件工程.北京:科学出版社,2002.
[55]何积丰,单志广,王戟,蒲戈光,房毓菲,刘克,赵瑞珍,张兆田.“可信软件基础研究”重大研究计划结题综述.中国科学基金,2018,32(3):291-296.
[57]刘克,单志广,王戟,何积丰,张兆田,秦玉文.“可信软件基础研究”重大研究计划综述.中国科学基金,2008,22(3):145-151.
[118]陆汝钤.计算机语言的形式语义.北京:科学出版社,1992.
[119]周巢尘,詹乃军.形式语义学引论.第2版,北京:科学出版社,2017.
[127]林惠民.相对完备性与抽象数据类型的描述.中国科学(A辑),1998,18(6):658-664.
[258]刘波,刘志明,裘宗燕,秦晓.加强计算机本科专业程序正确性知识教育与能力培养.计算机教育,2018.