程序分析研究进展
|
摘要
在信息化时代,人们对软件的质量要求越来越高.程序分析是保障软件质量的重要手段之一,日益受到学术界和产业界的重视.介绍了若干基本程序分析技术(抽象解释、数据流分析、基于摘要的分析、符号执行、动态分析、基于机器学习的程序分析等),特别是最近10余年的研究进展.进而介绍了针对不同类型软件(移动应用、并发软件、分布式系统、二进制代码等)的分析方法.最后展望了程序分析未来的研究方向和所面临的挑战.
In the information age, people are increasingly demanding high quality of software systems. Program analysis is one of the important approaches to guarantee the quality of software, and has been receiving attentions from academia and industry. This article mainly focuses on the research progress in program analysis in the last decade. First, the article introduces the basic program analysis techniques, including abstract interpretation, data flow analysis, summary-based analysis, symbolic execution, dynamic analysis, machine learning-based program analysis, etc. Then, it summarizes program analysis approaches for different types of software systems, including mobile applications, concurrent software, distributed systems, binary code, etc. Finally, the article discusses potential research directions and challenges of program analysis in the future.
In the information age, people are increasingly demanding high quality of software systems. Program analysis is one of the important approaches to guarantee the quality of software, and has been receiving attentions from academia and industry. This article mainly focuses on the research progress in program analysis in the last decade. First, the article introduces the basic program analysis techniques, including abstract interpretation, data flow analysis, summary-based analysis, symbolic execution, dynamic analysis, machine learning-based program analysis, etc. Then, it summarizes program analysis approaches for different types of software systems, including mobile applications, concurrent software, distributed systems, binary code, etc. Finally, the article discusses potential research directions and challenges of program analysis in the future.
引文
[1] Mei H, Wang QX, Zhang L, Wang J. Software analysis:A road map. Chinese Journal of Computers, 2009,32(9):1697-1710(in Chinese with English abstract).
[2] Nielson F, Nielson HR, Hankin C. Principles of Program Analysis. Springer-Verlag, 1999.
[3] Rice HG. Classes of recursively enumerable sets and their decision problems. Trans. of the American Mathematical Society, 1952,74(2):358-366.
[4] Zhang J, Wang X. A constraint solver and its application to path feasibility analysis. Int'l Journal of Software Engineering and Knowledge Engineering, 2001,11(2):139-156.
[5] Cousot P, Giacobazzi R, Ranzato F. Program analysis is harder than verification:A computability perspective. In:Proc. of the CAV.2018. 75-95.
[6] Li Z, Lu S, Myagmar S, Zhou Y. CP-Miner:Finding copy-paste and related bugs in large-scale software code. IEEE Trans. on Software Engineering, 2006,32(3):176-192.
[7] Cousot P, Cousot R. Abstract interpretation:A unified lattice mode for static analysis of programs by construction or approximation of fixpoints. In:Proc. of the POPL. 1977. 238-252.
[8] Cousot P, Cousot R. Systematic design of program analysis frameworks. In:Proc. of the POPL. 1979. 269-282.
[9] Jeannet B, Min A. Apron:A library of numerical abstract domains for static analysis. In:Proc. of the CAV. 2009. 661-667.
[10] Singh G, Schel MP, Vechev MT. A practical construction for decomposing numerical abstract domains. In:Proc. of the POPL.2018. 1-28.
[11] Bagnara R, Hill PM, Zaffanella E. The parma polyhedra library:Toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems. Science of Computer Programming, 2008,72:3-21.
[12] Polyspace code prover. 2018. https://www.mathworks.com/products/polyspace-code-prover.html
[13] Astree runtime error analyzer. 2018. https://www.absint.com/astree/index.htm
[14] Kirchner F, Kosmatov N, Prevosto V, Signoles J, Yakobowski B. Frama-C:A software analysis perspective. Formal Aspects of Computing, 2015,27(3):573-609.
[15] Logozzo F. Practical verification for the working programmer with code contracts and abstract interpretation. In:Proc. of the VMCAI. 2011. 19-22.
[16] Interproc. 2018. http://pop-art.inrialpes.fr/people/bjeannet/bjeannet-forge/interproc/
[17] Blanchet B, Cousot P, Cousot R, Feret J, Mauborgne L, Mine A, Monniaux D, Rival X. A static analyzer for large safety-critical software. In:Proc. of the PLDI. 2003. 196-207.
[18] Mine A, Delmas D. Towards an industrial use of sound static analysis for the verification of concurrent embedded avionics software. In:Proc. of the EMSOFT. 2015. 65-74.
[19] Roux P, Garoche PL. Practical policy iterations-a practical use of policy iterations for static analysis:The quadratic case. Formal Methods in System Design, 2015,46(2):163-196.
[20] Jeannet B, Schrammel P, Sankaranarayanan S. Abstract acceleration of general linear loops. In:Proc. of the POPL. 2013. 529-540.
[21] Amato G, Scozzari F, Seidl H, Apinis K, Vojdani V. Efficiently intertwining widening and narrowing. Science of Computer Programming, 2016,120:1-24.
[22] Li Y, Albarghouthi A, Kincaid Z, Gurfinkel A, Chechik M. Symbolic optimization with SMT solvers. In:Proc. of the POPL. 2014.607-618.
[23] Jiang J, Chen L, Wu X, Wang J. Block-Wise abstract interpretation by combining abstract domains with SMT. In:Proc. of the VMCAI. 2017. 310-329.
[24] Cousot P. Abstracting induction by extrapolation and interpolation. In:Proc. of the VMCAI. 2015. 19-42.
[25] Chen L, Liu J, Mine A, Kapur D, Wang J. An abstract domain to infer octagonal constraints with absolute value. In:Proc. of the SAS. 2014. 101-117.
[26] Chen J, Cousot P. A binary decision tree abstract domain functor. In:Proc. of the SAS. 2015. 36-53.
[27] Kincaid Z, Breck J, Reps T. Compositional recurrence analysis revisited. In:Proc. of the PLDI. 2017. 248-262.
[28] Kincaid Z, Cyphert J, Breck J, Reps T. Non-Linear reasoning for invariant synthesis. In:Proc. of the POPL. 2017. 1-33.
[29] Allamigeon X, Gaubert S, Goubault E, Putot S, Stott N. A fast method to compute disjunctive quadratic invariants of numerical programs. Trans. on Embedded Computing Systems, 2017,16(5):1-19.
[30] Oh H, Heo K, Lee W, Lee W, Park D, Kang J, Yi K. Global sparse analysis framework. Trans. on Programming Languages and Systems, 2014,36(3):1-44.
[31] Oh H, Lee W, Heo K, Yang H, Yi K. Selective x-sensitive analysis guided by impact pre-analysis. Trans. on Programming Languages and Systems, 2015,38(2):1-45.
[32] Singh G, Püschel M, Vechev M. Making numerical program analysis fast. In:Proc. of the PLDI. 2015. 303-313.
[33] Singh G, Püschel M, Vechev M. Fast polyhedra abstract domain. In:Proc. of the POPL. 2017. 46-59.
[34] Singh G, Püschel M, Vechev M. A practical construction for decomposing numerical abstract domains. In:Proc. of the POPL. 2018.46-59.
[35] Singh G, Püschel M, Vechev M. Fast numerical program analysis with reinforcement learning. In:Proc. of the CAV. 2018.211-229.
[36] Becchi A, Zaffanella E. A direct encoding for NNC polyhedra. In:Proc. of the CAV. 2018. 230-248.
[37] Liu J, Rival X. Abstraction of arrays based on non contiguous partitions. In:Proc. of the VMCAI. 2015. 282-299.
[38] Liu J, Rival X, Chen L. Automatic verification of embedded manipulating dynamic structures stored in system code contiguous regions. In:Proc. of the EMSOFT. 2018.
[39] Chen L, Mine A, Wang J, Cousot P. An abstract domain to discover interval linear equalities. In:Proc. of the VMCAI. 2010.112-128.
[40] Fu Z. Modularly combining numeric abstract domains with points-to analysis, and a scalable static numeric analyzer for Java. In:Proc. of the VMCAI. 2014. 282-301.
[41] Illous H, Lemerre M, Rival X. A relational shape abstract domain. In:Proc. of the NFM. 2013. 212-229.
[42] Wu X, Chen L, Mine A, Dong W, Wang J. Static analysis of runtime errors in interrupt-driven programs via sequentialization.ACM Trans. on Embedded Computing Systems, 2016,15(4):1-26.
[43] Sung C, Kusano M, Wang C. Modular verification of interrupt-driven software. In:Proc. of the ASE. 2017. 206-216.
[44] Chakarov A, Sankaranarayanan S. Expectation invariants for probabilistic program loops as fixed points. In:Proc. of the SAS. 2014.85-100.
[45] Wang D, Hoffmann J, Reps T. PMAF:An algebraic framework for static analysis of probabilistic programs. In:Proc. of the PLDI.2018. 513-528.
[46] Ouadjaout A, Mine A, Lasla N, Badache N. Static analysis by abstract interpretation of functional properties of device drivers in TinyOS. Journal of Systems and Software, 2016,120:114-132.
[47] Cox A, Chang BE, Rival X. Desynchronized multi-state abstractions for open programs in dynamic languages. In:Proc. of the ESOP. 2015. 483-509.
[48] Lim J, Reps T. TSL:A system for generating abstract interpreters and its application to machine-code analysis. Trans. on Programming Languages and Systems, 2013,35(1):1-59.
[49] Tripp O, Pistoia M, Cousot P, Cousot R, Guarnieri S. Andromeda:Accurate and scalable security analysis of Web applications. In:Proc. of the FASE. 2013. 210-225.
[50] Urban C, Mine A. Proving guarantee and recurrence temporal properties by abstract interpretation. In:Proc. of the VMCAI. 2015.190-208.
[51] Urban C. FuncTion:An abstract domain functor for termination. In:Proc. of the TACAS. 2015. 464-466.
[52] Gonnord L, Monniaux D, Radanne G. Synthesis of ranking functions using extremal counterexamples. In:Proc. of the PLDI. 2015.608-618.
[53] Dan A, Meshman Y, Vechev M, Yahav E. Effective abstractions for verification under relaxed memory models. In:Proc. of the VMCAI. 2017. 62-76.
[54] Alglave J, Cousot P. Ogre and Pythia:An invariance proof method for weak consistency models. In:Proc. of the PLDI. 2017. 3-18.
[55] Gehr T, Mirman M, Drachsler-Cohen D, Tsankov P, Chaudhuri S, Vechev M. AI2:Safety and robustness certification of neural networks with abstract interpretation. In:Proc. of the IEEE S&P. 2018. 3-18.
[56] Wang S, Pei K, Whitehouse J, Yang J, Jana S. Formal security analysis of neural networks using symbolic intervals. Technical Report, 1804.10829, 2018.
[57] Urban C, Muller P. An abstract interpretation framework for input data usage. In:Proc. of the ESOP. 2018. 683-710.
[58] Fromherz A, Ouadjaout A, Mine A. Static value analysis of python programs by abstract interpretation. In:Proc. of the NFM. 2018.185-202.
[59] Chae K, Oh H, Heo K, Yang H. Automatically generating features for learning program analysis heuristics for C-like languages. In:Proc. of the OOPSLA. 2017. 1-25.
[60] Seladji Y. Finding relevant templates via the principal component analysis. In:Proc. of the VMCAI. 2017. 483-499.
[61] Cousot P, Cousot R. Abstract interpretation:Past, present and future. In:Proc. of the CSL-LICS. 2014. 1-10.
[62] Aho AV, Sethi R, Ullman JD, et al. Compilers:Principles, Techniques, and Tools. Pearson Education Singapore, 1986.
[63] Reps T, Horwitz S, Sagiv M. Precise interprocedural dataflow analysis via graph reachability. In:Proc. of the POPL. 1995. 49-61.
[64] Bodden E. Inter-Procedural data-flow analysis with IFDS/IDE and Soot. In:Proc. of the SOAP. 2012. 3-8.
[65] Dolby J. Watson libraries for analysis(WALA). 2018. https://github.com/wala/WALA
[66] Arzt S, Rasthofer S, Fritz C, Bodden E, Bartel A, Klein J, Traon YL, Octeau D, McDaniel P. FlowDroid:Precise context, flow,field, object-sensitive and lifecycle-aware taint analysis for Android apps. In:Proc. of the PLDI. 2014. 259-269.
[67] Reps T. Program analysis via graph reachability. Information and Software Technology, 1998,40(11-12):701-726.
[68] Sridharan M, Bodik R. Refinement-Based context-sensitive points-to analysis for Java. In:Proc. of the PLDI. 2006. 387-400.
[69] Sui Y, Li Y, Xue J. Query-Directed adaptive heap cloning for optimizing compilers. In:Proc. of the CGO. 2013. 1-11.
[70] Pratikakis P, Foster JS, Hicks M. LOCKSMITH:Context-Sensitive correlation analysis for race detection. In:Proc. of the PLDI.2006. 320-331.
[71] Zhou Q, Li L, Wang L, Xue J, Feng X. May-Happen-in-Parallel analysis with static vector clocks. In:Proc. of the CGO. 2018.228-240.
[72] Li L, Cifuentes C, Keynes N. Boosting the performance of flow-sensitive points-to analysis using value flow. In:Proc. of the FSE.2011. 343-353.
[73] Sui Y, Xue J. On-Demand strong update analysis via value-flow refinement. In:Proc. of the FSE. 2016. 460-473.
[74] Yu H, Xue J, Huo W, Feng X, Zhang Z. Level by level:Making flow-and context-sensitive pointer analysis scalable for millions of lines of code. In:Proc. of the CGO. 2010. 218-229.
[75] Hardekopf B, Lin C. Flow-Sensitive pointer analysis for millions of lines of code. In:Proc. of the CGO. 2011. 289-298.
[76] Li L, Cifuentes C, Keynes N. Precise and scalable context-sensitive pointer analysis via value flow graph. In:Proc. of the ISMM.2013. 85-96.
[77] Ali K, Lhotak O. Application-Only call graph construction. In:Proc. of the ECOOP. 2012. 688-712.
[78] Ali K, Lhotak O. Averroes:Whole-Program analysis without the whole program. In:Proc. of the ECOOP. 2013. 378-400.
[79] Dillig I, Dillig T, Aiken A. Reasoning about the unknown in static analysis. Communications of the ACM, 2010,53(8):115-123.
[80] Cousot P, Cousot R. Modular static program analysis. In:Proc. of the CC. 2002. 159-179.
[81] Smaragdakis Y, Balatsouras G, Kastrinis G. Set-Based pre-processing for points-to analysis. In:Proc. of the OOPSLA. 2013.253-270.
[82] Rountev A, Ryder BG. Points-To and side-effect analyses for programs built with precompiled libraries. In:Proc. of the CC. 2001.20-36.
[83] Rountev A, Kagan S, Marlowe T. Interprocedural dataflow analysis in the presence of large libraries. In:Proc. of the CC. 2006.2-16.
[84] Rountev A, Sharp M, Xu G. IDE dataflow analysis in the presence of large object-oriented libraries. In:Proc. of the CC. 2008.53-68.
[85] Sharir M, Pnueli A. Two approaches to interprocedural data flow analysis. Computer Science Department, Courant Institute of Mathematical Sciences, New York University, 1978. http://www.rw.cdl.uni-saarland.de/teaching/spa10/slides/kboesche.pdf
[86] Arzt S, Bodden E. StubDroid:Automatic inference of precise data-flow summaries for the Android framework. In:Proc. of the ICSE. 2016. 725-735.
[87] Tang H, Wang X, Zhang L, Xie B, Zhang L, Mei H. Summary-Based context-sensitive data-dependence analysis in presence of callbacks. In:Proc. of the POPL. 2015. 83-95.
[88] Tang H, Wang D, Xiong Y, Zhang L, Wang X, Zhang L. Conditional DYCK-CFL reachability analysis for complete and efficient library summarization. In:Proc. of the ESOP. 2017. 880-908.
[89] Palepu VK, Xu G, Jones JA. Improving efficiency of dynamic analysis with dynamic dependence summaries. In:Proc. of the ASE.2013. 59-69.
[90] Kulkarni S, Mangal R, Zhang X, Naik M. Accelerating program analyses by cross-program training. In:Proc. of the OOPSLA.2016. 359-377.
[91] Yorsh G, Yahav E, Chandra S. Generating precise and concise procedure summaries. In:Proc. of the POPL. 2008. 221-234.
[92] Strom RE, Yemini S. Typestate:A programming language concept for enchancing software reliability. IEEE Trans. on Software Engineering, 1986,12(1):157-171.
[93] Dillig I, Dillig T, Aiken A, Sagiv M. Precise and compact modular procedure summaries for heap manipulating programs. In:Proc.of the PLDI. 2011. 567-577.
[94] Boyer RS, Elspas B, Levitt KN. SELECT—A formal system for testing and debugging programs by symbolic execution. ACM SIGPLAN Notices, 1975,10(6):234-245.
[95] Clarke LA. A program testing system. In:Proc. of the Annual Conf. 1976. 488-491.
[96] King JC. Symbolic execution and program testing. Communications of the ACM, 1976,19(7):385-394.
[97] Zhang J. Sharp static analysis of programs. Chinese Journal of Computers, 2008,31(9):1549-1553(in Chinese with English abstract).
[98] Zhang J. Constraint solving and symbolic execution. In:Proc. of the VSTTE. 2008. 539-544.
[99] De Moura L, Bjφrner N. Z3:An efficient SMT solver. In:Proc. of the TACAS. 2008. 337-340.
[100] Ganesh V, Dill DL. A decision procedure for bit-vectors and arrays. In:Proc. of the CAV. 2007. 519-531.
[101] Dutertre B, de Moura L. A fast linear-arithmetic solver for DPLL(T). In:Proc. of the CAV. 2016. 81-94.
[102] Godefroid P, Klarlund N, Sen K. DART:Directed automated random testing. In:Proc. of the PLDI. 2005. 213-223.
[103] Sen K, Marinov D, Agha G. CUTE:A concolic unit testing engine for C. In:Proc. of the FSE. 2005. 263-272.
[104] Godefroid P, Levin MY, Molnar D. Automated whitebox fuzz testing. In:Proc. of the NDSS. 2008. 151-166.
[105] Cadar C, Dunbar D, Engler D. KLEE:Unassisted and automatic generation of high-coverage tests for complex systems programs.In:Proc. of the OSDI. 2008. 209-224.
[106] Pǎsǎreanu CS, Mehlitz PC, Bushnell DH, Gundy-Burlet K, Lowry M, Person S, Pape M. Combining unit-level symbolic execution and system-level concrete execution for testing NASA software. In:Proc. of the ISSTA. 2008. 15-26.
[107] Tillmann N, de Halleux J. Pex-White box test generation for.NET. In:Proc. of the TAP. 2008. 134-153.
[108] Chipounov V, Kuznetsov V, Candea G. S2E:A platform for in-vivo multi-path analysis of software systems. In:Proc. of the ASPLOS. 2011. 265-278.
[109] Xie T, Tillmann N, de Halleux J, Schulte W. Fitness-Guided path exploration in dynamic symbolic execution. In:Proc. of the DSN.2009. 359-368.
[110] Li Y, Su Z, Wang L, Li X. Steering symbolic execution to less traveled paths. In:Proc. of the OOPSLA. 2013. 19-32.
[111] Seo H, Kim S. How we get there:A context-guided search strategy in concolic testing. In:Proc. of the FSE. 2014. 413-424.
[112] Ma KK, Khoo YP, Foster JS, Hicks M. Directed symbolic execution. In:Proc. of the SAS. 2011. 95-111.
[113] Zhang Y, Chen Z, Wang J, Dong W, Liu Z. Regular property guided dynamic symbolic execution. In:Proc. of the ICSE. 2015.643-653.
[114] Person S, Yang G, Rungta N, Khurshid S. Directed incremental symbolic execution. In:Proc. of the PLDI. 2011. 504-515.
[115] Dan Marinescu P, Cadar C. Make test-zesti:A symbolic execution solution for improving regression testing. In:Proc. of the ICSE.2012. 716-726.
[116] Godefroid P, Kiezun A, Levin MY. Grammar-Based whitebox fuzzing. In:Proc. of the PLDI. 2008. 206-215.
[117] Siddiqui JH, Khurshid S. Scaling symbolic execution using ranged analysis. In:Proc. of the OOPSLA. 2012. 523-536.
[118] Slaby J, Strejcek J, Trtik M. Checking properties described by state machines:On synergy of instrumentation, slicing, and symbolic execution. In:Proc. of the FMICS. 2012. 207-221.
[119] Cui H, Hu G, Wu J, Yang J. Verifying systems rules using rule-directed symbolic execution. In:Proc. of the ASPLOS. 2013.329-342.
[120] Trabish D, Mattavelli A, Rinetzky N, Cadar C. Chopped symbolic execution. In:Proc. of the ICSE. 2018. 350-360.
[121] Yu H, Chen Z, Wang J, Su Z, Dong W. Symbolic verification of regular properties. In:Proc. of the ICSE. 2018. 871-881.
[122] Boonstoppel P, Cadar C, Engler D. RWset:Attacking path explosion in constraint-based test generation. In:Proc. of the TACAS.2008. 351-366.
[123] Jaffar J, Murali V, Navas JA. Boosting concolic testing via interpolation. In:Proc. of the FSE. 2013. 48-58.
[124] Godefroid P. Compositional dynamic test generation. In:Proc. of the POPL. 2007. 47-54.
[125] Saxena P, Poosankam P, McCamant S, Song D. Loop-Extended symbolic execution on binary programs. In:Proc. of the ISSTA.2009. 225-236.
[126] Godefroid P, Luchaup D. Automatic partial loop summarization in dynamic test generation. In:Proc. of the ISSTA. 2011. 23-33.
[127] Strejcek J, Trtik M. Abstracting path conditions. In:Proc. of the ISSTA. 2012. 155-165.
[128] Qiu R, Yang G, Pasareanu CS, Khurshid S. Compositional symbolic execution with memoized replay. In:Proc. of the ICSE. 2015.632-642.
[129] Yi Q, Yang Z, Guo S, Wang C, Liu J, Zhao C. Eliminating path redundancy via postconditioned symbolic execution. IEEE Trans.on Software Engineering, 2018,44(1):25-43.
[130] Sen K. Scalable automated methods for dynamic program analysis[Ph.D. Thesis]. University of Illinois at Urbana-Champaign,2006.
[131] Wang C, Yang Z, Kahlon V, Gupta A. Peephole partial order reduction. In:Proc. of the TACAS. 2008. 382-396.
[132] Kuznetsov V, Kinder J, Bucur S, Candea G. Efficient state merging in symbolic execution. ACM SIGPLAN Notices, 2012,47(6):193-204.
[133] Avgerinos T, Rebert A, Sang KC, Brumley D. Enhancing symbolic execution with veritesting. In:Proc. of the ICSE. 2014.1083-1094.
[134] Qi D, Nguyen HDT, Roychoudhury A. Path exploration based on symbolic output. ACM Trans. on Software Engineering and Methodology, 2013,22(4):32.
[135] Guo S, Kusano M, Wang C, Yang Z, Gupta A. Assertion guided symbolic execution of multithreaded programs. In:Proc. of the FSE. 2015. 854-865.
[136] Wang H, Liu T, Guan X, Shen C, Zheng Q, Yang Z. Dependence guided symbolic execution. IEEE Trans. on Software Engineering,2017,43(3):252-271.
[137] Visser W, Geldenhuys J, Dwyer MB. Green:Reducing, reusing and recycling constraints in program analysis. In:Proc. of the FSE.2012. 58.
[138] Aquino A, Bianchi FA, Chen M, Denaro G, Pezze M. Reusing constraint proofs in program analysis. In:Proc. of the ISSTA. 2015.305-315.
[139] Jia X, Ghezzi C, Ying S. Enhancing reuse of constraint solutions to improve symbolic execution. In:Proc. of the ISSTA. 2015.177-187.
[140] Zhang Y, Chen Z, Wang J. Speculative symbolic execution. In:Proc. of the ISSRE. 2012. 101-110.
[141] Barr ET, Vo T, Le V, Su Z. Automatic detection of floating-point exceptions. In:Proc. of the POPL. 2013. 549-560.
[142] Lakhotia K, Tillmann N, Harman M, de Halleux J. FloPSy-Search-Based floating point constraint solving for symbolic execution.In:Proc. of the ICTSS. 2010. 142-157.
[143] Romano A. Practical floating-point tests with integer code. In:Proc. of the VMCAI. 2014. 337-356.
[144] Li X, Liang Y, Qian H, Hu YQ, Bu L, Yu Y, Chen X, Li X. Symbolic execution of complex program driven by machine learning based constraint solving. In:Proc. of the ASE. 2016. 554-559.
[145] Fu Z, Su Z. XSat:A fast floating-point satisfiability solver. In:Proc. of the CAV. 2016. 187-209.
[146] Bjorner N, Tillmann N, Voronkov A. Path feasibility analysis for string-manipulating programs. In:Proc. of the TACAS. 2009.307-321.
[147] Khurshid S, Pasareanu CS, Visser W. Generalized symbolic execution for model checking and testing. In:Proc. of the TACAS.2003. 553-568.
[148] Ramos DA, Engler D. Under-Constrained symbolic execution:Correctness checking for real code. In:Proc. of the USENIX Security. 2015. 49-64.
[149] Rosner N, Geldenhuys J, Aguirre NM, Visser W, Frias MF. BLISS:Improved symbolic execution by bounded lazy initialization with SAT support. IEEE Trans. on Software Engineering, 2015,41(7):639-660.
[150] Jeon J, Qiu X, Fetter-Degges J, Foster JS, Solar-Lezama A. Synthesizing framework models for symbolic execution. In:Proc. of the ICSE. 2016. 156-167.
[151] Cha SK, Avgerinos T, Rebert A, Brumley D. Unleashing mayhem on binary code. In:Proc. of the IEEE S&P. 2012. 380-394.
[152] Shoshitaishvili Y, Wang R, Salls C, Stephens N, Polino M, Dutcher A, Grosen J, Feng S, Hauser C, Kruegel C, Vigna G. SOK:(state of)the art of war:Offensive techniques in binary analysis. In:Proc. of the IEEE S&P. 2016. 138-157.
[153] Banabic R, Candea G, Guerraoui R. Finding trojan message vulnerabilities in distributed systems. In:Proc. of the ASPLOS. 2014.113-126.
[154] Bucur S, Kinder J, Candea G. Prototyping symbolic execution engines for interpreted languages. In:Proc. of the ASPLOS. 2014.239-253.
[155] Emmi M, Majumdar R, Sen K. Dynamic test input generation for database applications. In:Proc. of the ISSTA. 2007. 151-162.
[156] Sasnauskas R, Landsiedel O, Alizai MH, Weise C, Kowalewski S, Wehrle K. KleeNet:Discovering insidious interaction bugs in wireless sensor networks before deployment. In:Proc. of the IPSN. 2010. 186-196.
[157] Fu X, Chen Z, Yu H, Huang C, Dong W, Wang J. Poster:Symbolic execution of MPI programs. In:Proc. of the ICSE. 2015.809-810.
[158] Yu H. Combining symbolic execution and model checking to verify MPI programs. In:Proc. of the ICSE. 2018. 527-529.
[159] Davidson D, Moench B, Jha S, Ristenpart T. FIE on firmware:Finding vulnerabilities in embedded systems using symbolic execution. In:Proc. of the USENIX Security. 2013. 463-478.
[160] Guo S, Wu M, Wang C. Symbolic execution of programmable logic controller code. In:Proc. of the FSE. 2017. 326-336.
[161] Liu S, Zhang J. Program analysis:From qualitative analysis to quantitative analysis. In:Proc. of the ICSE. 2011. 956-959.
[162] Geldenhuys J, Dwyer MB, Visser W. Probabilistic symbolic execution. In:Proc. of the ISSTA. 2012. 166-176.
[163] Filieri A, Pasareanu CS, Visser W. Reliability analysis in symbolic pathFinder. In:Proc. of the ICSE. 2013. 622-631.
[164] Chen B, Liu Y, Le W. Generating performance distributions via probabilistic symbolic execution. In:Proc. of the ICSE. 2016.49-60.
[165] Filieri A, Pasareanu CS, Yang G. Quantification of software changes through probabilistic symbolic execution. In:Proc. of the ASE. 2015. 703-708.
[166] Godefroid P, Levin MY, Molnar D. SAGE:Whitebox fuzzing for security testing. Communications of the ACM, 2012,10(3):40-44.
[167] Miscrosfot. Visual studio 2015 RTM. 2018. https://www.visualstudio.com/news/vs2015-vs#Testing
[168] Xu Z, Zhang J, Wang J. Canalyze:A static bug-finding tool for C programs. In:Proc. of the ISSTA. 2014. 425-428.
[169] Cha S, Hong S, Lee J, Oh H. Automatically generating search heuristics for concolic testing. In:Proc. of the ICSE. 2018.1244-1254.
[170] Su T, Fu Z, Pu G, He J, Su Z. Combining symbolic execution and model checking for data flow testing. In:Proc. of the ICSE. 2015.654-665.
[171] Christakis M, Müller P, Wüstholz V. Guiding dynamic symbolic execution toward unverified program executions. In:Proc. of the ICSE. 2016. 144-155.
[172] Wang X, Sun J, Chen Z, Zhang P, Wang J, Lin Y. Towards optimal concolic testing. In:Proc. of the ICSE. 2018. 291-302.
[173] Stephens N, Grosen J, Salls C, Dutcher A, Wang R, Corbetta J, Shoshitaishvili Y, Kruegel C, Vigna G. Driller:Augmenting fuzzing through selective symbolic execution. In:Proc. of the NDSS. 2016. 21-24.
[174] Gosain A, Sharma G. A survey of dynamic program analysis techniques and tools. In:Proc. of the FICTA. 2014. 113-122.
[175] Kong P, Li Y, Chen X, Sun J, Sun M, Wang J. Towards concolic testing for hybrid systems. In:Proc. of the FM. 2016. 460-478.
[176] Chen Y, Poskitt CM, Sun J. Learning from mutants:Using code mutation to learn and monitor invariants of a cyber-physical system. In:Proc. of the SP. 2018. 648-660.
[177] Xiong Y, Wang B, Fu G, Zang L. Learning to synthesize. In:Proc. of the GI. 2018. 37-44.
[178] Heo K, Oh H, Yi K. Machine-Learning-Guided selectively unsound static analysis. In:Proc. of the ICSE. 2017. 519-529.
[179] Oh H, Yang H, Yi K. Learning a strategy for adapting a program analysis via Bayesian optimisation. In:Proc. of the OOPSLA.2015. 572-588.
[180] Heo K, Oh H, Yang H, Yi K. Adapting static analysis via learning with bayesian optimization. ACM Trans. on Programming Languages and Systems, 2018.
[181] Jeong S, Jeon M, Cha S, Oh H. Data-Driven context-sensitivity for points-to analysis. In:Proc. of the OOPSLA. 2017. 1-28.
[182] Enck W, Gilbert P, Chun BG, Cox LP, Jung J, McDaniel P, Sheth AN. TaintDroid:An information-flow tracking system for realtime privacy monitoring on smartphones. In:Proc. of the USENIX Security. 2014. 393-407.
[183] Hornyack P, Han S, Jung J, Schechter S, Wetherall D. These aren't the Droids you're looking for:Retrofitting Android to protect data from imperious applications. In:Proc. of the CCS. 2011. 639-652.
[184] DroidBox:Android application sandbox. 2018. http://code.google.com/p/droidbox/
[185] Yan LK, Yin H. DroidScope:Seamlessly reconstructing the OS and Dalvik semantic views for dynamic Android malware analysis.In:Proc. of the USENIX Security. 2014. 569-584.
[186] Bellard F. QEMU, a fast and portable dynamic translator. In:Proc. of the ATEC. 2005. 41-46.
[187] TEMU:The BitBlaze dynamic analysis component. 2018. http://bitblaze.cs.berkeley.edu/temu.html
[188] Gibler C, Crussell J, Erickson J, Chen H. AndroidLeaks:Automatically detecting potential privacy leaks in Android applications on a large scale. In:Proc. of the TRUST. 2012. 291-307.
[189] Feng Y, Anand S, Dillig I, Aiken A. Apposcopy:Semantics-Based detection of Android malware through static analysis. In:Proc.of the FSE. 2014. 576-587.
[190] Gordon MI, Kim D, Perkins J, Gilham L, Nguyen N, Rinard M. Information-Flow analysis of Android applications in DroidSafe. In:Proc. of the NDSS. 2015. 8-11.
[191] Jin X, Hu X, Ying K, Du W, Yin H, Peri GN. Code injection attacks on HTML5-based mobile apps:Characterization, detection and mitigation. In:Proc. of the CCS. 2014. 66-77.
[192] Egele M, Kruegel C, Kirda E, Vigna G. PiOS:Detecting privacy leaks in iOS applications. In:Proc. of the NDSS. 2011. 11.
[193] Octeau D, McDaniel P, Jha S, Bartel A, Bodden E, Klein J, Traon YL. Effective inter-component communication mapping in Android with Epicc:An essential step towards holistic security analysis. In:Proc. of the USENIX Security. 2013. 543-558.
[194] Wu T, Liu J, Xu Z, Guo C, Zhang Y, Yan J, Zhang J. Light-Weight, inter-procedural and callback-aware resource leak detection for Android apps. IEEE Trans. on Software Engineering, 2016,42(11):1054-1076.
[195] Chan PPF, Hui LCK, Yiu SM. DroidChecker:Analyzing Android applications for capability leak categories. In:Proc. of the WISEC. 2012. 125-136.
[196] Felt AP, Wang HJ, Moshchuk A, Hanna S, Chin E. Permission re-delegation:Attacks and defenses. In:Proc. of the USENIX Security. 2011. 22-22.
[197] Amalfitano D, Fasolino AR, Tramontana P, De Carmine S, Memon AM. Using GUI ripping for automated testing of Android applications. In:Proc. of the ASE. 2012. 258-261.
[198] Machiry A, Tahiliani R, Naik M. Dynodroid:An input generation system for Android apps. In:Proc. of the FSE. 2013. 224-234.
[199] Hu G, Yuan X, Tang Y, Yang J. Efficiently, effectively detecting mobile app bugs with AppDoctor. In:Proc. of the EuroSys. 2014.1-15.
[200] Mahmood R, Mirzaei N, Malek S. EvoDroid:Segmented evolutionary testing of Android apps. In:Proc. of the FSE. 2014.599-609.
[201] Mirzaei N, Garcia J, Bagheri H, Sadeghi A, Malek S. Reducing combinatorics in GUI testing of Android applications. In:Proc. of the ICSE. 2016. 559-570.
[202] You W, Liang B, Shi W, Zhu S, Wang P, Xie S, Zhang X. Reference hijacking:Patching, protecting and analyzing on unmodified and non-rooted Android devices. In:Proc. of the ICSE. 2016. 959-970.
[203] Au KWY, Zhou YF, Huang Z, Lie D. PScout:Analyzing the Android permission specification. In:Proc. of the CCS. 2012.217-228.
[204] Cao Y, Fratantonio Y, Bianchi A, Egele M, Kruegel C, Vigna G, Chen Y. EdgeMiner:Automatically detecting implicit control flow transitions through the Android framework. In:Proc. of the NDSS. 2015. 8-11.
[205] Rasthofer S, Arzt S, Bodden E. A machine-learning approach for classifying and categorizing Android sources and sinks. In:Proc.of the NDSS. 2014. 23-26.
[206] Zhang Y, Luo X, Yin H. DexHunter:Toward extracting hidden code from packed Android applications. In:Proc. of the ESORICS.2015. 293-311.
[207] Xue L, Luo X, Yu L, Wang S, Wu D. Adaptive unpacking of Android apps. In:Proc. of the ICSE. 2017. 358-369.
[208] Clarke EM, Emerson EA, Sistla AP. Automatic verification of finite-state concurrent systems using temporal logic specifications.Trans. on Programming Languages and Systems, 1986,8(2):244-263.
[209] Bron A, Farchi E, Magid Y, Nir Y, Ur S. Applications of synchronization coverage. In:Proc. of the PPoPP. 2005. 206-212.
[210] Krena B, Letko Z, Vojnar T. Coverage metrics for saturation-based and search-based testing of concurrent software. In:Proc. of the RV. 2011. 177-192.
[211] Sorrentino F, Farzan A, Madhusudan P. PENELOPE:Weaving threads to expose atomicity violations. In:Proc. of the FSE. 2010.37-46.
[212] Wang C, Said M, Gupta A. Coverage guided systematic concurrency testing. In:Proc. of the ICSE. 2011. 221-230.
[213] Musuvathi M, Qadeer S, Ball T, Basler G, Nainar PA, Neamtiu I. Finding and reproducing heisenbugs in concurrent programs. In:Proc. of the OSDI. 2008. 267-280.
[214] Kahlon V, Sinha N, Kruus E, Zhang Y. Static data race detection for concurrent programs with asynchronous calls. In:Proc. of the FSE. 2009. 13-22.
[215] Naik M, Aiken A, Whaley J. Effective static race detection for Java. In:Proc. of the PLDI. 2006. 308-319.
[216] Voung JW, Ranjit J, Lerner S. RELAY:Static race detection on millions of lines of code. In:Proc. of the FSE. 2007. 205-214.
[217] Cai Y, Wu S, Chan WK. ConLock:A constraint-based approach to dynamic checking on deadlocks in multithreaded programs. In:Proc. of the ICSE. 2014. 491-502.
[218] Pozniansky E, Schuster A. Efficient on-the-fly data race detection in multihreaded C++programs. In:Proc. of the PPoPP. 2003.179-190.
[219] Savage S, Burrows M, Nelson G, Sobalvarro P, Anderson T. Eraser:A dynamic data race detector for multithreaded programs.ACM Trans. on Computer Systems, 1997,15(4):391-411.
[220] Yu Y, Rodeheffer T, Chen W. RaceTrack:Efficient detection of data race conditions via adaptive tracking. In:Proc. of the SOSP.2005. 221-234.
[221] Xie X, Xue J. Acculock:Accurate and efficient detection of data races. In:Proc. of the CGO. 2011. 201-212.
[222] Kasikci B, Zamfir C, Candea G. RaceMob:Crowdsourced data race detection. In:Proc. of the SOSP. 2013. 406-422.
[223] Williams A, Thies W, Ernst M. Static deadlock detection for Java libraries. In:Proc. of the ECOOP. 2005. 602-629.
[224] Clarke EM, Emerson EA. Design and synthesis of synchronization skeletons using branching time temporal logic. In:Proc. of the Logic of Programs. 1981. 52-71.
[225] Bach M, Charney M, Cohn R, Demikhovsky E, Devor T, Hazelwood K, Jaleel A, Luk C, Lyons G, Patil H, Tal A. Analyzing parallel programs with pin. IEEE Computer, 2010,43(3):34-41.
[226] Eslamimehr M, Palsberg J. Race directed scheduling of concurrent programs. In:Proc. of the PPoPP. 2014. 301-314.
[227] Edelstein O, Farchi E, Nir Y, Ratsaby G, Ur S. Multithreaded Java program test generation. IBM Systems Journal, 2002,41(1):111-125.
[228] Burckhardt S, Kothari P, Musuvathi M, Nagarakatte S. A randomized scheduler with probabilistic guarantees of finding bugs. In:Proc. of the ASPLOS. 2010. 167-178.
[229] Cai Y, Yang Z. Radius aware probabilistic testing of deadlocks with guarantees. In:Proc. of the ASE. 2016. 356-367.
[230] Fonseca P, Rodrigues R, B.Brandenburg B. SKI:Exposing kernel concurrency bugs through systematic schedule exploration. In:Proc. of the OSDI. 2014. 415-431.
[231] Yu J, Narayanasamy S, Pereira C, Pokam G. Maple:A coverage-driven testing tool for multithreaded programs. In:Proc. of the OOPSLA. 2012.
[232] Abdelrasoul M. Promoting secondary orders of event pairs in randomized scheduling using a randomized stride. In:Proc. of the ASE. 2017. 741-752.
[233] Lu S, Park S, Seo E, Zhou Y. Learning from mistakes—A comprehensive study on real world concurrency bug characteristics. In:Proc. of the ASPLOS. 2008. 329-339.
[234] Flanagan C, Freund SN. FastTrack:Efficient and precise dynamic race detection. Communications of the ACM, 2010,53(11):93-101.
[235] Cai Y, Cao L. Effective and precise dynamic detection of hidden races for Java programs. In:Proc. of the FSE. 2015. 450-461.
[236] Smaragdakis Y, Evans JM, Sadowski C, Yi J, Flanagan C. Sound predictive race detection in polynomial time. In:Proc. of the POPL. 2012. 387-400.
[237] Marino D, Musuvathi M, Narayanasamy S. LiteRace:Effective sampling for lightweight data-race detection. In:Proc. of the PLDI.2009. 134-143.
[238] Bond MD, Coons KE, Mckinley KS. PACER:Proportional detection of data races. In:Proc. of the PLDI. 2010. 255-268.
[239] Zhai K, Xu B, Chan WK, Tse TH. CARISMA:A context-sensitive approach to race-condition sample-instance selection for multithreaded applications. In:Proc. of the ISSTA. 2012. 221-231.
[240] Erickson J, Musuvathi M, Burckhardt S, Olynyk K. Effective data-race detection for the kernel. In:Proc. of the OSDI. 2010. 1-16.
[241] Sen K. Race directed random testing of concurrent programs. In:Proc. of the PLDI. 2008. 11-21.
[242] Joshi P, Park CS, Sen K, Naik M. A randomized dynamic program analysis technique for detecting real deadlocks. In:Proc. of the PLDI. 2009. 110-120.
[243] Huang J, Meredith PO, Rosu G. Maximal sound predictive race detection with control flow abstraction. In:Proc. of the PLDI. 2013.337-348.
[244] Cai Y, Zhang J, Cao L, Liu J. A deployable sampling strategy for data race detection. In:Proc. of the PLDI. 2016. 810-821.
[245] Guo Y, Cai Y, Yang Z. AtexRace:Across thread and execution sampling for in-house race detection. In:Proc. of the FSE. 2017.315-325.
[246] Lu S, Tucek J, Qin F, Zhou Y. AVIO:Detecting atomicity violations via access-interleaving invariants. In:Proc. of the ASPLOS.2006. 37-48.
[247] Lu S, Park S, Hu C, Ma X, Jiang W, Li Z, Popa RA, Zhou Y. MUVI:Automatically inferring multi-variable access correlations and detecting related semantic and concurrency bugs. In:Proc. of the SOSP. 2007. 103-116.
[248] Park CS, Sen K. Randomized active atomicity violation detection in concurrent programs. In:Proc. of the FSE. 2008. 135-145.
[249] Muzahid A, Otsuki N, Torrellas J. AtomTracker:A comprehensive approach to atomic region inference and violation detection. In:Proc. of the MICRO. 2010. 287-297.
[250] Cai Y, Chan WK. MagicFuzzer:Scalable deadlock detection for large-scale applications. In:Proc. of the ICSE. 2012. 606-616.
[251] Cai Y, Chan WK. Magiclock:Scalable detection of potential deadlocks in large-scale multithreaded programs. IEEE Trans, on Software Engineering, 2014,40(3):266-281.
[252] Cai Y, Lu Q. Dynamic testing for deadlocks via constraints. IEEE Trans, on Software Engineering, 2016,42(9):825-842.
[253] Cai Y, Jia C, Wu S, Zhai K, Chan WK. ASN:A dynamic barrier-based approach to confirmation of deadlocks from warnings for large-scale multithreaded programs. IEEE Trans. on Parallel and Distributed Systems, 2015,26(1):13-23.
[254] Pradel M, Gross TR. Fully automatic and precise detection of thread safety violations. In:Proc. of the PLDI. 2012. 521-530.
[255] Choudhary A, Lu S, Pradel M. Efficient detection of thread safety violations via coverage-guided generation of concurrent tests. In:Proc. of the ICSE. 2017. 266-277.
[256] The 10 biggest cloud outages of 2014. 2018. http://www.crn.com/slide-shows/cloud/300075204/the-10-biggest-cloud-outages-of-2014.html
[257] Gunawi HS, Hao M, Leesatapornwongsa T, Patana-anake T, Do T, Adityatama J, Eliazar KJ, Laksono A, Lukman JF, Martin V,Satria AD. What bugs live in the cloud? A study of 3000+issues in cloud systems. In:Proc. of the SOCC. 2014. 1-14.
[258] Leesatapornwongsa T, Lukman JF, Lu S, Gunawi HS. TaxDC:A taxonomy of non-deterministic concurrency bugs in datacenter distributed systems. In:Proc. of the ASPLOS. 2016. 517-530.
[259] Dai T, He J, Gu X, Lu S. Understanding real-world timeout problems in cloud server systems. In:Proc. of the IC2E. 2018. 1-11.
[260] Gao Y, Dou W, Qin F, Gao C, Wang D, Wei J, Huang R, Zhou L, Wu Y. An empirical study on crash recovery bugs in large-scale distributed systems. In:Proc. of the FSE. 2018. 539-550.
[261] Guo Z, McDirmid S, Yang M, Zhuang L, Zhang P, Luo Y, Bergan T, Bodik P, Musuvathi M, Zhang Z, Zhou L. Failure recovery:When the cure is worse than the disease. In:Proc. of the HotOS. 2013. 1-6.
[262] Yuan D, Luo Y, Zhuang X, Rodrigues GR, Zhao X, Zhang Y, Jain PU, Stumm M. Simple testing can prevent most critical failures:An analysis of production failures in distributed data-intensive systems. In:Proc. of the OSDI. 2014. 249-265.
[263] Wang G, Zhang L, Xu W. What can we learn from four years of data center hardware failures? In:Proc. of the DSN. 2017. 25-36.
[264] Liu H, Li G, Lukman JF, Li J, Lu S, Gunawi HS, Tian C. DCatch:Automatically detecting distributed concurrency bugs in cloud systems cloud systems. In:Proc. of the ASPLOS. 2017. 677-691.
[265] Liu H, Wang X, Li G, Lu S, Ye F, Tian C. FCatch:Automatically detecting time-of-fault bugs in cloud systems. In:Proc. of the ASPLOS. 2018. 1-11.
[266] Liu X, Guo Z, Wang X, Chen F, Lian X, Tang J, Wu M, Kaashoek MF, Zhang Z. D3S:Debugging deployed distributed systems. In:Proc. of the NSDI. 2008. 423-437.
[267] Xu W, Huang L, Fox A, Patterson D, Jordan MI. Detecting large-scale system problems by mining console logs. In:Proc. of the SOSP. 2009. 117-132.
[268] Grant S, Cech H, Beschastnikh I. Inferring and asserting distributed system invariants. In:Proc. of the ICSE. 2018. 1149-1159.
[269] Scott C, Panda A, Brajkovic V, Necula G, Krishnamurthy A, Shenker S. Minimizing faulty executions of distributed systems. In:Proc. of the NSDI. 2016. 291-309.
[270] Flanagan C, Godefroid P. Dynamic partial-order reduction for model checking software. In:Proc. of the POPL. 2005. 110-121.
[271] Zeller A, Hildebrandt R. Simplifying and isolating failure-inducing input. IEEE Trans. on Software Engineering, 2002,28(2):183-200.
[272] Wilcox JR, Woos D, Panchekha P, Tatlock Z, Wang X, Ernst MD, Anderson T. Verdi:A framework for implementing and formally verifying distributed systems. In:Proc. of the PLDI. 2015. 357-368.
[273] 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 SOSP. 2015. 1-17.
[274] Lesani M, Bell CJ, Chlipala A. Chapar:Certified causally consistent distributed key-value stores. In:Proc. of the POPL. 2016.357-370.
[275] Fonseca P, Zhang K, Wang X, Krishnamurthy A. An empirical study on the correctness of formally verified distributed systems. In:Proc. of the EuroSys. 2017. 328-343.
[276] Yang J, Chen T, Wu M, Xu Z, Liu X, Lin H, Yang M, Long F, Zhang L, Zhou L. MODIST:Transparent model checking of unmodified distributed systems. In:Proc. of the NSDI. 2009. 213-228.
[277] Guo H, Wu M, Zhou L, Hu G, Yang J, Zhang L. Practical software model checking via dynamic interface reduction. In:Proc. of the SOSP. 2011. 265-278.
[278] Leesatapornwongsa T, Hao M, Joshi P, Lukman JF, Gunawi HS. SAMC:Semantic-Aware model checking for fast discovery of deep bugs in cloud systems. In:Proc. of the OSDI. 2014. 399-414.
[279] Sasnauskas R, Dustmann OS, Kaminski BL, Wehrle K, Weise C, Kowalewski S. Scalable symbolic execution of distributed systems. In:Proc. of the ICDCS. 2011. 333-342.
[280] Joahi P, Ganai M, Balakrishnan G, Gupta A, Papakonstantinou N. SETSUDO:Perturbation-Based testing framework for scalable distributed systems pallavi. In:Proc. of the TRIOS. 2013. 1-14.
[281] Joshi P, Gunawi HS, Sen K. PREFAIL:A programmable tool for multiple-failure injection. In:Proc. of the OOPSLA. 2011.171-188.
[282] Gunawi HS, Do T, Joshi P, Alvaro P, Hellerstein JM, Arpaci-Dusseau AC, Arpaci-Dusseau RH, Sen K, Borthakur D. FATE and DESTINI:A framework for cloud recovery testing. In:Proc. of the NSDI. 2011. 1-18.
[283] Alagappan R, Ganesan A, Patel Y, Pillai TS, Arpaci-Dusseau AC, Arpaci-Dusseau RH. Correlated crash vulnerabilities. In:Proc. of the OSDI. 2016. 151-167.
[284] Ganesan A, Alagappan R, Arpaci-Dusseau AC, Arpaci-Dusseau RH. Redundancy does not imply fault tolerance:Analysis of distributed storage reactions to file-system faults. In:Proc. of the FAST. 2017. 149-166.
[285] Alvaro P, Rosen J, Hellerstein JM. Lineage-Driven fault injection. In:Proc. of the SIGMOD. 2015. 331-346.
[286] Thompson K. Reflections on trusting trust. Communications of the ACM, 1984,27(8):761-763.
[287] Xiao C. Novel malware xcodeghost modifies xcode, infects apple iOS apps and hits app store. Technical Report, 2018.https://researchcenter.paloaltonetworks.com/2015/09/novel-malware-xcodeghost-modifies-xcode-infects-apple-ios-apps-and-hits-ap p-store/
[288] De Sutter B, de Bus B, de Bosschere K, Keyngnaert P, Demoen B. On the static analysis of indirect control transfers in binaries. In:Proc. of the PDPTA. 2000.
[289] Kinder J. Static analysis of x86 executables(statische analyse von programmen in x86-Maschinensprache)[Ph.D. Thesis].Fachbereich Informatik, Technische Universitat Darmstadt, 2010.
[290] Cifuentes C, van Emmerik M. Recovery of jump table case statements from binary code. Science of Computer Programming, 2001,40(2-3):171-188.
[291] Kinder J, Veith H. Jakstab:A static analysis platform for binaries. In:Proc. of the CAV. 2008. 423-427.
[292] Xu L, Sun F, Su Z. Constructing precise control flow graphs from binaries. Technical Report, 2009.
[293] Shin ECR, Song D, Moazzezi R. Recognizing functions in binaries with neural networks. In:Proc. of the USENIX Security. 2015.611-626.
[294] Andriesse D, Chen X, Van der Veen V, Slowinska A, Bos H. An in-depth analysis of disassembly on full-scale x86/x64 binaries. In:Proc. of the USENIX Security. 2016. 583-600.
[295] Chua ZL, Shen S, Saxena P, Liang Z. Neural nets can learn function type signatures from binaries. In:Proc. of the USENIX Security. 2017. 99-116.
[296] Tr(o|¨)ger J, Cifuentes C. Analysis of virtual method invocation for binary translation. In:Proc. of the WCRE. 2002. 65-74.
[297] Balakrishnan G, Reps T. Analyzing memory accesses in x86 executables. In:Proc. of the CC. 2004. 5-23.
[298] Jin W, Cohen C, Gennari J, Hines C, Chaki S, Gurfinkel A, Havrilla J, Narasimhan P. Recovering C++objects from binaries using inter-procedural data-flow analysis. In:Proc. of the POPL. 2014. 1-11.
[299] Lin Z, Zhang X, Xu D. Automatic reverse engineering of data structures from binary execution. In:Proc. of the NDSS. 2010.
[300] Zeng J, Lin Z. Towards automatic inference of kernel object semantics from binary code. In:Proc. of the RAID. 2015. 538-561.
[301] Smithson M, El Wazeer K, Anand K, Kotha A, Barua R. Static binary rewriting without supplemental information:Overcoming the tradeoff between coverage and correctness. In:Proc. of the WCRE. 2013. 52-61.
[302] Wang S, Wang P, Wu D. UROBOROS:Instrumenting stripped binaries with static reassembling. In:Proc. of the SANER. 2016.236-247.
[303] Wang S, Wang P, Wu D. Reassembleable disassembling. In:Proc. of the USENIX Security. 2015. 627-642.
[304] Wang R, Shoshitaishvili Y, Bianchi A, Machiry A, Grosen J, Grosen P, Kruegel C, Vigna G. RAMBLR:Making reassembly great again. In:Proc. of the NDSS. 2017.
[305] Song D, Brumley D, Yin H, Caballero J, Jager I, Kang MG, Liang Z, Newsome J, Poosankam P, Saxena P. BitBlaze:A new approach to computer security via binary analysis. In:Proc. of the ICISS. 2008. 1-25.
[306] Brumley D, Jager I, Avgerinos T, Schwartz EJ. BAP:A binary analysis platform. In:Proc. of the CAV. 2011. 463-469.
[307] Bruening D. Efficient, transparent, and comprehensive runtime code manipulation[Ph.D. Thesis]. Massachusetts Institute of Technology, 2004.
[308] Bernat AR, Miller BP. Anywhere, any-time binary instrumentation. In:Proc. of the PASTE. 2011. 9-16.
[309] Nethercote N, Seward J. Valgrind:A framework for heavyweight dynamic binary instrumentation. In:Proc. of the PLDI. 2007.89-100.
[310] Luk CK, Cohn R, Muth R, Patil H, Klauser A, Lowney G, Wallace S, Reddi VJ, Hazelwood K. Pin:Building customized program analysis tools with dynamic instrumentation. In:Proc. of the PLDI. 2005. 190-200.
[311] Machiry A, Spensky C, Corina J, Stephens N, Kruegel C, Vigna G, Barbara S. DR.CHECKER:A soundy analysis for Linux kernel drivers. In:Proc. of the USENIX Security. 2017. 1007-1024.
[312] Wang P, Krinke J, Lu K, Li G, Dodier-Lazaro S. How double-fetch situations turn into double-fetch vulnerabilities:A study of double fetches in the Linux kernel. In:Proc. of the USENIX Security. 2017. 1-16.
[313] Dewey D, Giffin J. Static detection of C++vtable escape vulnerabilities in binary code. In:Proc. of the NDSS. 2012.
[314] Kruegel C, Robertson W, Vigna G. Detecting kernel-level rootkits through binary analysis. In:Proc. of the ACSAC. 2004. 91-100.
[315] Bergeron J, Debbabi M, Erhioui MM, Ktari B. Static analysis of binary code to isolate malicious behaviors. In:Proc. of the WETICE. 1999. 184-189.
[316] Bergeron J, Debbabi M, Desharnais J, M.Erhioui M, Lavoie Y, Tawbi N. Static detection of malicious code in executable programs.In:Proc. of the Symp. on Requirements Engineering for Information Security. 2001.
[317] O'Sullivan P, Anand K, Kotha A, Smithson M, Barua R, Keromytis AD. Retrofitting security in COTS software with binary rewriting. In:Proc. of the SEC. 2011. 154-172.
[318] Wartell R, Mohan V, Hamlen KW, Lin Z. Binary stirring:Self-Randomizing instruction addresses of legacy x86 binary code. In:Proc. of the Computer and Communications Security. New York:ACM Press, 2012. 157-168.
[319] Wartell R, Mohan V, Hamlen KW, Lin Z. Securing untrusted code via compiler-agnostic binary rewriting. In:Proc. of the ACSAC.ACM Press, 2012. 299-308.
[320] Zhang M, Sekar R. Contol flow integrity for COTS binaries. In:Proc. of the USENIX Security. 2013. 337-352.
[321] Batyuk L, Herpich M, Camtepe SA, Raddatz K, Schmidt AD, Albayrak S. Using static analysis for automatic assessment and mitigation of unwanted and malicious activities within Android applications. In:Proc. of the MALWARE. 2011. 66-72.
[322] Zhang C, Song C, Chen KZ, Chen Z, Song D. VTint:Protecting virtual function tables’ integrity. In:Proc. of the NDSS. 2015.
[323] Xu Z, Zhang J. A test data generation tool for unit testing of C programs. In:Proc. of the QSIC. 2006. 107-116.
[324] Wu R, Wen M, Cheung SC, Zhang H. ChangeLocator:Locate crash-inducing changes based on crash reports. Empirical Software Engineering, 2017,23(5):2866-2900.
[325] Gao Q, Xiong Y, Mi Y, Zhang L, Yang W, Zhou Z, Xie B, Mei H. Safe memory-leak fixing for C programs. In:Proc. of the ICSE.2015. 459-470.
[326] Xuan J, Martinez M, De Marco F, Clement M, Marcote SL, Durieux T, Le Berre D, Monperrus M. NOPOL:Automatic repair of conditional statement bugs in Java programs. IEEE Trans. on Software Engineering, 2017,43(1):34-55.
[327] Briand LC, Daly JW, Wust J. A unified framework for cohesion measurement in object-oriented systems. Empirical Software Engineering, 1998,3(1):65-117.
[328] Briand LC, Daly JW, Wust JK. A unified framework for coupling measurement in object-oriented systems. IEEE Trans. on Software Engineering, 1999,25(1):91-121.
[329] Ethereum. 2018. https://www.ethereum.org/
[330] The DAO attacked:Code issue leads to 60 million ether theft. 2018. https://www.coindesk.com/dao-attacked-code-issue-leads-60-million-ether-theft/
[331] Accidental bug may have frozen$280 million worth of digital coinether in a cryptocurrency wallet. 2018. https://www.cnbc.com/2017/11/08/accidental-bug-may-have-frozen-280-worth-of-ether-on-parity-w allet.html
[332] Luu L, Chu DH, Olickel H, Saxena P, Hobor A. Making smart contracts smarter. In:Proc. of the CCS. 2016. 254-269.
[333] Nikolic I, Kolluri A, Sergey I, Saxena P, Hobor A. Finding the greedy, prodigal, and suicidal contracts at scale. In:Proc. of the CoRR. 2018. https://arxiv.org/pdf/1802.06038.pdf
[334] Hirai Y. Formal verification of deed contract in ethereum name service. Technical Report, 2016. 1-81.
[335] Bhargavan K, Delignat-Lavaud A, Fournet C, Gollamudi A, Gonthier G, Kobeissi N, Kulatova N, Rastogi A, Sibut-Pinote T,Swamy N, Zanella-Béguelin S. Formal verification of smart contracts. In:Proc. of the PLAS. 2016. 91-96.
[336] Bigi G, Bracciali A, Meacci G, Tuosto E. Validation of decentralised smart contracts through game theory and formal methods. In:Proc. of the Programming Languages with Applications to Biology and Security. 2015. 142-161.
[337] Kalra S, Goel S, Dhawan M, Sharma S. ZEUS:Analyzing safety of smart contracts. In:Proc. of the NDSS. 2018.
[338] Tsankov P, Dan A, Drachsler-Cohen D, Gervais A, Bunzli F, Vechev M. Securify:Practical security analysis of smart contracts. In:Proc. of the CoRR. 2018. https://arxiv.org/pdf/1806.01143.pdf
[339] Gurfinkel A, Kahsai T, Komuravelli A, Navas JA. The SeaHorn verification framework. In:Proc. of the CAV. 2004. 343-361.
[340] Masuda S, Ono K, Yasue T, Hosokawa N. A survey of software quality for machine learning applications. In:Proc. of the ICSTW.2018. 279-284.
[341] Qin Y, Wang H, Xu C, Ma X, Lu J. SynEva:Evaluating ML programs by mirror program synthesis. In:Proc. of the QRS. 2018.171-182.
[342] Sun Y, Wu M, Ruan W, Huang X, Kwiatkowska M, Kroening D. Concolic testing for deep neural networks. In:Proc. of the ASE.2018. 109-119.
[343] Ruan W, Huang X, Kwiatkowska M. Reachability analysis of deep neural networks with provable guarantees. In:Proc. of the IJCAI. 2018. 2651-2659.
[344] Huang X, Kwiatkowska M, Wang S, Wu M. Safety verification of deep neural networks. In:Proc. of the CAV. 2017. 3-29.
[345] Ma S, Aafer Y, Xu Z, Lee WC, Zhai J, Liu Y, Zhang X. LAMP:Data provenance for graph based machine learning algorithms through derivative computation. In:Proc. of the FSE. 2017. 786-797.
[346] Gulzar MA, Interlandi M, Yoo S, Tetali SD, Condie T, Millstein T, Kim M. BigDebug:Debugging primitives for interactive big data processing in spark. In:Proc. of the ICSE. 2016. 784-795.
[1]梅宏,王千祥,张路,王戟.软件分析技术进展.计算机学报,2009,32(9):1697-1710.
[97]张健.精确的程序静态分析.计算机学报,2008,31(9):1549-1553.
[2] Nielson F, Nielson HR, Hankin C. Principles of Program Analysis. Springer-Verlag, 1999.
[3] Rice HG. Classes of recursively enumerable sets and their decision problems. Trans. of the American Mathematical Society, 1952,74(2):358-366.
[4] Zhang J, Wang X. A constraint solver and its application to path feasibility analysis. Int'l Journal of Software Engineering and Knowledge Engineering, 2001,11(2):139-156.
[5] Cousot P, Giacobazzi R, Ranzato F. Program analysis is harder than verification:A computability perspective. In:Proc. of the CAV.2018. 75-95.
[6] Li Z, Lu S, Myagmar S, Zhou Y. CP-Miner:Finding copy-paste and related bugs in large-scale software code. IEEE Trans. on Software Engineering, 2006,32(3):176-192.
[7] Cousot P, Cousot R. Abstract interpretation:A unified lattice mode for static analysis of programs by construction or approximation of fixpoints. In:Proc. of the POPL. 1977. 238-252.
[8] Cousot P, Cousot R. Systematic design of program analysis frameworks. In:Proc. of the POPL. 1979. 269-282.
[9] Jeannet B, Min A. Apron:A library of numerical abstract domains for static analysis. In:Proc. of the CAV. 2009. 661-667.
[10] Singh G, Schel MP, Vechev MT. A practical construction for decomposing numerical abstract domains. In:Proc. of the POPL.2018. 1-28.
[11] Bagnara R, Hill PM, Zaffanella E. The parma polyhedra library:Toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems. Science of Computer Programming, 2008,72:3-21.
[12] Polyspace code prover. 2018. https://www.mathworks.com/products/polyspace-code-prover.html
[13] Astree runtime error analyzer. 2018. https://www.absint.com/astree/index.htm
[14] Kirchner F, Kosmatov N, Prevosto V, Signoles J, Yakobowski B. Frama-C:A software analysis perspective. Formal Aspects of Computing, 2015,27(3):573-609.
[15] Logozzo F. Practical verification for the working programmer with code contracts and abstract interpretation. In:Proc. of the VMCAI. 2011. 19-22.
[16] Interproc. 2018. http://pop-art.inrialpes.fr/people/bjeannet/bjeannet-forge/interproc/
[17] Blanchet B, Cousot P, Cousot R, Feret J, Mauborgne L, Mine A, Monniaux D, Rival X. A static analyzer for large safety-critical software. In:Proc. of the PLDI. 2003. 196-207.
[18] Mine A, Delmas D. Towards an industrial use of sound static analysis for the verification of concurrent embedded avionics software. In:Proc. of the EMSOFT. 2015. 65-74.
[19] Roux P, Garoche PL. Practical policy iterations-a practical use of policy iterations for static analysis:The quadratic case. Formal Methods in System Design, 2015,46(2):163-196.
[20] Jeannet B, Schrammel P, Sankaranarayanan S. Abstract acceleration of general linear loops. In:Proc. of the POPL. 2013. 529-540.
[21] Amato G, Scozzari F, Seidl H, Apinis K, Vojdani V. Efficiently intertwining widening and narrowing. Science of Computer Programming, 2016,120:1-24.
[22] Li Y, Albarghouthi A, Kincaid Z, Gurfinkel A, Chechik M. Symbolic optimization with SMT solvers. In:Proc. of the POPL. 2014.607-618.
[23] Jiang J, Chen L, Wu X, Wang J. Block-Wise abstract interpretation by combining abstract domains with SMT. In:Proc. of the VMCAI. 2017. 310-329.
[24] Cousot P. Abstracting induction by extrapolation and interpolation. In:Proc. of the VMCAI. 2015. 19-42.
[25] Chen L, Liu J, Mine A, Kapur D, Wang J. An abstract domain to infer octagonal constraints with absolute value. In:Proc. of the SAS. 2014. 101-117.
[26] Chen J, Cousot P. A binary decision tree abstract domain functor. In:Proc. of the SAS. 2015. 36-53.
[27] Kincaid Z, Breck J, Reps T. Compositional recurrence analysis revisited. In:Proc. of the PLDI. 2017. 248-262.
[28] Kincaid Z, Cyphert J, Breck J, Reps T. Non-Linear reasoning for invariant synthesis. In:Proc. of the POPL. 2017. 1-33.
[29] Allamigeon X, Gaubert S, Goubault E, Putot S, Stott N. A fast method to compute disjunctive quadratic invariants of numerical programs. Trans. on Embedded Computing Systems, 2017,16(5):1-19.
[30] Oh H, Heo K, Lee W, Lee W, Park D, Kang J, Yi K. Global sparse analysis framework. Trans. on Programming Languages and Systems, 2014,36(3):1-44.
[31] Oh H, Lee W, Heo K, Yang H, Yi K. Selective x-sensitive analysis guided by impact pre-analysis. Trans. on Programming Languages and Systems, 2015,38(2):1-45.
[32] Singh G, Püschel M, Vechev M. Making numerical program analysis fast. In:Proc. of the PLDI. 2015. 303-313.
[33] Singh G, Püschel M, Vechev M. Fast polyhedra abstract domain. In:Proc. of the POPL. 2017. 46-59.
[34] Singh G, Püschel M, Vechev M. A practical construction for decomposing numerical abstract domains. In:Proc. of the POPL. 2018.46-59.
[35] Singh G, Püschel M, Vechev M. Fast numerical program analysis with reinforcement learning. In:Proc. of the CAV. 2018.211-229.
[36] Becchi A, Zaffanella E. A direct encoding for NNC polyhedra. In:Proc. of the CAV. 2018. 230-248.
[37] Liu J, Rival X. Abstraction of arrays based on non contiguous partitions. In:Proc. of the VMCAI. 2015. 282-299.
[38] Liu J, Rival X, Chen L. Automatic verification of embedded manipulating dynamic structures stored in system code contiguous regions. In:Proc. of the EMSOFT. 2018.
[39] Chen L, Mine A, Wang J, Cousot P. An abstract domain to discover interval linear equalities. In:Proc. of the VMCAI. 2010.112-128.
[40] Fu Z. Modularly combining numeric abstract domains with points-to analysis, and a scalable static numeric analyzer for Java. In:Proc. of the VMCAI. 2014. 282-301.
[41] Illous H, Lemerre M, Rival X. A relational shape abstract domain. In:Proc. of the NFM. 2013. 212-229.
[42] Wu X, Chen L, Mine A, Dong W, Wang J. Static analysis of runtime errors in interrupt-driven programs via sequentialization.ACM Trans. on Embedded Computing Systems, 2016,15(4):1-26.
[43] Sung C, Kusano M, Wang C. Modular verification of interrupt-driven software. In:Proc. of the ASE. 2017. 206-216.
[44] Chakarov A, Sankaranarayanan S. Expectation invariants for probabilistic program loops as fixed points. In:Proc. of the SAS. 2014.85-100.
[45] Wang D, Hoffmann J, Reps T. PMAF:An algebraic framework for static analysis of probabilistic programs. In:Proc. of the PLDI.2018. 513-528.
[46] Ouadjaout A, Mine A, Lasla N, Badache N. Static analysis by abstract interpretation of functional properties of device drivers in TinyOS. Journal of Systems and Software, 2016,120:114-132.
[47] Cox A, Chang BE, Rival X. Desynchronized multi-state abstractions for open programs in dynamic languages. In:Proc. of the ESOP. 2015. 483-509.
[48] Lim J, Reps T. TSL:A system for generating abstract interpreters and its application to machine-code analysis. Trans. on Programming Languages and Systems, 2013,35(1):1-59.
[49] Tripp O, Pistoia M, Cousot P, Cousot R, Guarnieri S. Andromeda:Accurate and scalable security analysis of Web applications. In:Proc. of the FASE. 2013. 210-225.
[50] Urban C, Mine A. Proving guarantee and recurrence temporal properties by abstract interpretation. In:Proc. of the VMCAI. 2015.190-208.
[51] Urban C. FuncTion:An abstract domain functor for termination. In:Proc. of the TACAS. 2015. 464-466.
[52] Gonnord L, Monniaux D, Radanne G. Synthesis of ranking functions using extremal counterexamples. In:Proc. of the PLDI. 2015.608-618.
[53] Dan A, Meshman Y, Vechev M, Yahav E. Effective abstractions for verification under relaxed memory models. In:Proc. of the VMCAI. 2017. 62-76.
[54] Alglave J, Cousot P. Ogre and Pythia:An invariance proof method for weak consistency models. In:Proc. of the PLDI. 2017. 3-18.
[55] Gehr T, Mirman M, Drachsler-Cohen D, Tsankov P, Chaudhuri S, Vechev M. AI2:Safety and robustness certification of neural networks with abstract interpretation. In:Proc. of the IEEE S&P. 2018. 3-18.
[56] Wang S, Pei K, Whitehouse J, Yang J, Jana S. Formal security analysis of neural networks using symbolic intervals. Technical Report, 1804.10829, 2018.
[57] Urban C, Muller P. An abstract interpretation framework for input data usage. In:Proc. of the ESOP. 2018. 683-710.
[58] Fromherz A, Ouadjaout A, Mine A. Static value analysis of python programs by abstract interpretation. In:Proc. of the NFM. 2018.185-202.
[59] Chae K, Oh H, Heo K, Yang H. Automatically generating features for learning program analysis heuristics for C-like languages. In:Proc. of the OOPSLA. 2017. 1-25.
[60] Seladji Y. Finding relevant templates via the principal component analysis. In:Proc. of the VMCAI. 2017. 483-499.
[61] Cousot P, Cousot R. Abstract interpretation:Past, present and future. In:Proc. of the CSL-LICS. 2014. 1-10.
[62] Aho AV, Sethi R, Ullman JD, et al. Compilers:Principles, Techniques, and Tools. Pearson Education Singapore, 1986.
[63] Reps T, Horwitz S, Sagiv M. Precise interprocedural dataflow analysis via graph reachability. In:Proc. of the POPL. 1995. 49-61.
[64] Bodden E. Inter-Procedural data-flow analysis with IFDS/IDE and Soot. In:Proc. of the SOAP. 2012. 3-8.
[65] Dolby J. Watson libraries for analysis(WALA). 2018. https://github.com/wala/WALA
[66] Arzt S, Rasthofer S, Fritz C, Bodden E, Bartel A, Klein J, Traon YL, Octeau D, McDaniel P. FlowDroid:Precise context, flow,field, object-sensitive and lifecycle-aware taint analysis for Android apps. In:Proc. of the PLDI. 2014. 259-269.
[67] Reps T. Program analysis via graph reachability. Information and Software Technology, 1998,40(11-12):701-726.
[68] Sridharan M, Bodik R. Refinement-Based context-sensitive points-to analysis for Java. In:Proc. of the PLDI. 2006. 387-400.
[69] Sui Y, Li Y, Xue J. Query-Directed adaptive heap cloning for optimizing compilers. In:Proc. of the CGO. 2013. 1-11.
[70] Pratikakis P, Foster JS, Hicks M. LOCKSMITH:Context-Sensitive correlation analysis for race detection. In:Proc. of the PLDI.2006. 320-331.
[71] Zhou Q, Li L, Wang L, Xue J, Feng X. May-Happen-in-Parallel analysis with static vector clocks. In:Proc. of the CGO. 2018.228-240.
[72] Li L, Cifuentes C, Keynes N. Boosting the performance of flow-sensitive points-to analysis using value flow. In:Proc. of the FSE.2011. 343-353.
[73] Sui Y, Xue J. On-Demand strong update analysis via value-flow refinement. In:Proc. of the FSE. 2016. 460-473.
[74] Yu H, Xue J, Huo W, Feng X, Zhang Z. Level by level:Making flow-and context-sensitive pointer analysis scalable for millions of lines of code. In:Proc. of the CGO. 2010. 218-229.
[75] Hardekopf B, Lin C. Flow-Sensitive pointer analysis for millions of lines of code. In:Proc. of the CGO. 2011. 289-298.
[76] Li L, Cifuentes C, Keynes N. Precise and scalable context-sensitive pointer analysis via value flow graph. In:Proc. of the ISMM.2013. 85-96.
[77] Ali K, Lhotak O. Application-Only call graph construction. In:Proc. of the ECOOP. 2012. 688-712.
[78] Ali K, Lhotak O. Averroes:Whole-Program analysis without the whole program. In:Proc. of the ECOOP. 2013. 378-400.
[79] Dillig I, Dillig T, Aiken A. Reasoning about the unknown in static analysis. Communications of the ACM, 2010,53(8):115-123.
[80] Cousot P, Cousot R. Modular static program analysis. In:Proc. of the CC. 2002. 159-179.
[81] Smaragdakis Y, Balatsouras G, Kastrinis G. Set-Based pre-processing for points-to analysis. In:Proc. of the OOPSLA. 2013.253-270.
[82] Rountev A, Ryder BG. Points-To and side-effect analyses for programs built with precompiled libraries. In:Proc. of the CC. 2001.20-36.
[83] Rountev A, Kagan S, Marlowe T. Interprocedural dataflow analysis in the presence of large libraries. In:Proc. of the CC. 2006.2-16.
[84] Rountev A, Sharp M, Xu G. IDE dataflow analysis in the presence of large object-oriented libraries. In:Proc. of the CC. 2008.53-68.
[85] Sharir M, Pnueli A. Two approaches to interprocedural data flow analysis. Computer Science Department, Courant Institute of Mathematical Sciences, New York University, 1978. http://www.rw.cdl.uni-saarland.de/teaching/spa10/slides/kboesche.pdf
[86] Arzt S, Bodden E. StubDroid:Automatic inference of precise data-flow summaries for the Android framework. In:Proc. of the ICSE. 2016. 725-735.
[87] Tang H, Wang X, Zhang L, Xie B, Zhang L, Mei H. Summary-Based context-sensitive data-dependence analysis in presence of callbacks. In:Proc. of the POPL. 2015. 83-95.
[88] Tang H, Wang D, Xiong Y, Zhang L, Wang X, Zhang L. Conditional DYCK-CFL reachability analysis for complete and efficient library summarization. In:Proc. of the ESOP. 2017. 880-908.
[89] Palepu VK, Xu G, Jones JA. Improving efficiency of dynamic analysis with dynamic dependence summaries. In:Proc. of the ASE.2013. 59-69.
[90] Kulkarni S, Mangal R, Zhang X, Naik M. Accelerating program analyses by cross-program training. In:Proc. of the OOPSLA.2016. 359-377.
[91] Yorsh G, Yahav E, Chandra S. Generating precise and concise procedure summaries. In:Proc. of the POPL. 2008. 221-234.
[92] Strom RE, Yemini S. Typestate:A programming language concept for enchancing software reliability. IEEE Trans. on Software Engineering, 1986,12(1):157-171.
[93] Dillig I, Dillig T, Aiken A, Sagiv M. Precise and compact modular procedure summaries for heap manipulating programs. In:Proc.of the PLDI. 2011. 567-577.
[94] Boyer RS, Elspas B, Levitt KN. SELECT—A formal system for testing and debugging programs by symbolic execution. ACM SIGPLAN Notices, 1975,10(6):234-245.
[95] Clarke LA. A program testing system. In:Proc. of the Annual Conf. 1976. 488-491.
[96] King JC. Symbolic execution and program testing. Communications of the ACM, 1976,19(7):385-394.
[97] Zhang J. Sharp static analysis of programs. Chinese Journal of Computers, 2008,31(9):1549-1553(in Chinese with English abstract).
[98] Zhang J. Constraint solving and symbolic execution. In:Proc. of the VSTTE. 2008. 539-544.
[99] De Moura L, Bjφrner N. Z3:An efficient SMT solver. In:Proc. of the TACAS. 2008. 337-340.
[100] Ganesh V, Dill DL. A decision procedure for bit-vectors and arrays. In:Proc. of the CAV. 2007. 519-531.
[101] Dutertre B, de Moura L. A fast linear-arithmetic solver for DPLL(T). In:Proc. of the CAV. 2016. 81-94.
[102] Godefroid P, Klarlund N, Sen K. DART:Directed automated random testing. In:Proc. of the PLDI. 2005. 213-223.
[103] Sen K, Marinov D, Agha G. CUTE:A concolic unit testing engine for C. In:Proc. of the FSE. 2005. 263-272.
[104] Godefroid P, Levin MY, Molnar D. Automated whitebox fuzz testing. In:Proc. of the NDSS. 2008. 151-166.
[105] Cadar C, Dunbar D, Engler D. KLEE:Unassisted and automatic generation of high-coverage tests for complex systems programs.In:Proc. of the OSDI. 2008. 209-224.
[106] Pǎsǎreanu CS, Mehlitz PC, Bushnell DH, Gundy-Burlet K, Lowry M, Person S, Pape M. Combining unit-level symbolic execution and system-level concrete execution for testing NASA software. In:Proc. of the ISSTA. 2008. 15-26.
[107] Tillmann N, de Halleux J. Pex-White box test generation for.NET. In:Proc. of the TAP. 2008. 134-153.
[108] Chipounov V, Kuznetsov V, Candea G. S2E:A platform for in-vivo multi-path analysis of software systems. In:Proc. of the ASPLOS. 2011. 265-278.
[109] Xie T, Tillmann N, de Halleux J, Schulte W. Fitness-Guided path exploration in dynamic symbolic execution. In:Proc. of the DSN.2009. 359-368.
[110] Li Y, Su Z, Wang L, Li X. Steering symbolic execution to less traveled paths. In:Proc. of the OOPSLA. 2013. 19-32.
[111] Seo H, Kim S. How we get there:A context-guided search strategy in concolic testing. In:Proc. of the FSE. 2014. 413-424.
[112] Ma KK, Khoo YP, Foster JS, Hicks M. Directed symbolic execution. In:Proc. of the SAS. 2011. 95-111.
[113] Zhang Y, Chen Z, Wang J, Dong W, Liu Z. Regular property guided dynamic symbolic execution. In:Proc. of the ICSE. 2015.643-653.
[114] Person S, Yang G, Rungta N, Khurshid S. Directed incremental symbolic execution. In:Proc. of the PLDI. 2011. 504-515.
[115] Dan Marinescu P, Cadar C. Make test-zesti:A symbolic execution solution for improving regression testing. In:Proc. of the ICSE.2012. 716-726.
[116] Godefroid P, Kiezun A, Levin MY. Grammar-Based whitebox fuzzing. In:Proc. of the PLDI. 2008. 206-215.
[117] Siddiqui JH, Khurshid S. Scaling symbolic execution using ranged analysis. In:Proc. of the OOPSLA. 2012. 523-536.
[118] Slaby J, Strejcek J, Trtik M. Checking properties described by state machines:On synergy of instrumentation, slicing, and symbolic execution. In:Proc. of the FMICS. 2012. 207-221.
[119] Cui H, Hu G, Wu J, Yang J. Verifying systems rules using rule-directed symbolic execution. In:Proc. of the ASPLOS. 2013.329-342.
[120] Trabish D, Mattavelli A, Rinetzky N, Cadar C. Chopped symbolic execution. In:Proc. of the ICSE. 2018. 350-360.
[121] Yu H, Chen Z, Wang J, Su Z, Dong W. Symbolic verification of regular properties. In:Proc. of the ICSE. 2018. 871-881.
[122] Boonstoppel P, Cadar C, Engler D. RWset:Attacking path explosion in constraint-based test generation. In:Proc. of the TACAS.2008. 351-366.
[123] Jaffar J, Murali V, Navas JA. Boosting concolic testing via interpolation. In:Proc. of the FSE. 2013. 48-58.
[124] Godefroid P. Compositional dynamic test generation. In:Proc. of the POPL. 2007. 47-54.
[125] Saxena P, Poosankam P, McCamant S, Song D. Loop-Extended symbolic execution on binary programs. In:Proc. of the ISSTA.2009. 225-236.
[126] Godefroid P, Luchaup D. Automatic partial loop summarization in dynamic test generation. In:Proc. of the ISSTA. 2011. 23-33.
[127] Strejcek J, Trtik M. Abstracting path conditions. In:Proc. of the ISSTA. 2012. 155-165.
[128] Qiu R, Yang G, Pasareanu CS, Khurshid S. Compositional symbolic execution with memoized replay. In:Proc. of the ICSE. 2015.632-642.
[129] Yi Q, Yang Z, Guo S, Wang C, Liu J, Zhao C. Eliminating path redundancy via postconditioned symbolic execution. IEEE Trans.on Software Engineering, 2018,44(1):25-43.
[130] Sen K. Scalable automated methods for dynamic program analysis[Ph.D. Thesis]. University of Illinois at Urbana-Champaign,2006.
[131] Wang C, Yang Z, Kahlon V, Gupta A. Peephole partial order reduction. In:Proc. of the TACAS. 2008. 382-396.
[132] Kuznetsov V, Kinder J, Bucur S, Candea G. Efficient state merging in symbolic execution. ACM SIGPLAN Notices, 2012,47(6):193-204.
[133] Avgerinos T, Rebert A, Sang KC, Brumley D. Enhancing symbolic execution with veritesting. In:Proc. of the ICSE. 2014.1083-1094.
[134] Qi D, Nguyen HDT, Roychoudhury A. Path exploration based on symbolic output. ACM Trans. on Software Engineering and Methodology, 2013,22(4):32.
[135] Guo S, Kusano M, Wang C, Yang Z, Gupta A. Assertion guided symbolic execution of multithreaded programs. In:Proc. of the FSE. 2015. 854-865.
[136] Wang H, Liu T, Guan X, Shen C, Zheng Q, Yang Z. Dependence guided symbolic execution. IEEE Trans. on Software Engineering,2017,43(3):252-271.
[137] Visser W, Geldenhuys J, Dwyer MB. Green:Reducing, reusing and recycling constraints in program analysis. In:Proc. of the FSE.2012. 58.
[138] Aquino A, Bianchi FA, Chen M, Denaro G, Pezze M. Reusing constraint proofs in program analysis. In:Proc. of the ISSTA. 2015.305-315.
[139] Jia X, Ghezzi C, Ying S. Enhancing reuse of constraint solutions to improve symbolic execution. In:Proc. of the ISSTA. 2015.177-187.
[140] Zhang Y, Chen Z, Wang J. Speculative symbolic execution. In:Proc. of the ISSRE. 2012. 101-110.
[141] Barr ET, Vo T, Le V, Su Z. Automatic detection of floating-point exceptions. In:Proc. of the POPL. 2013. 549-560.
[142] Lakhotia K, Tillmann N, Harman M, de Halleux J. FloPSy-Search-Based floating point constraint solving for symbolic execution.In:Proc. of the ICTSS. 2010. 142-157.
[143] Romano A. Practical floating-point tests with integer code. In:Proc. of the VMCAI. 2014. 337-356.
[144] Li X, Liang Y, Qian H, Hu YQ, Bu L, Yu Y, Chen X, Li X. Symbolic execution of complex program driven by machine learning based constraint solving. In:Proc. of the ASE. 2016. 554-559.
[145] Fu Z, Su Z. XSat:A fast floating-point satisfiability solver. In:Proc. of the CAV. 2016. 187-209.
[146] Bjorner N, Tillmann N, Voronkov A. Path feasibility analysis for string-manipulating programs. In:Proc. of the TACAS. 2009.307-321.
[147] Khurshid S, Pasareanu CS, Visser W. Generalized symbolic execution for model checking and testing. In:Proc. of the TACAS.2003. 553-568.
[148] Ramos DA, Engler D. Under-Constrained symbolic execution:Correctness checking for real code. In:Proc. of the USENIX Security. 2015. 49-64.
[149] Rosner N, Geldenhuys J, Aguirre NM, Visser W, Frias MF. BLISS:Improved symbolic execution by bounded lazy initialization with SAT support. IEEE Trans. on Software Engineering, 2015,41(7):639-660.
[150] Jeon J, Qiu X, Fetter-Degges J, Foster JS, Solar-Lezama A. Synthesizing framework models for symbolic execution. In:Proc. of the ICSE. 2016. 156-167.
[151] Cha SK, Avgerinos T, Rebert A, Brumley D. Unleashing mayhem on binary code. In:Proc. of the IEEE S&P. 2012. 380-394.
[152] Shoshitaishvili Y, Wang R, Salls C, Stephens N, Polino M, Dutcher A, Grosen J, Feng S, Hauser C, Kruegel C, Vigna G. SOK:(state of)the art of war:Offensive techniques in binary analysis. In:Proc. of the IEEE S&P. 2016. 138-157.
[153] Banabic R, Candea G, Guerraoui R. Finding trojan message vulnerabilities in distributed systems. In:Proc. of the ASPLOS. 2014.113-126.
[154] Bucur S, Kinder J, Candea G. Prototyping symbolic execution engines for interpreted languages. In:Proc. of the ASPLOS. 2014.239-253.
[155] Emmi M, Majumdar R, Sen K. Dynamic test input generation for database applications. In:Proc. of the ISSTA. 2007. 151-162.
[156] Sasnauskas R, Landsiedel O, Alizai MH, Weise C, Kowalewski S, Wehrle K. KleeNet:Discovering insidious interaction bugs in wireless sensor networks before deployment. In:Proc. of the IPSN. 2010. 186-196.
[157] Fu X, Chen Z, Yu H, Huang C, Dong W, Wang J. Poster:Symbolic execution of MPI programs. In:Proc. of the ICSE. 2015.809-810.
[158] Yu H. Combining symbolic execution and model checking to verify MPI programs. In:Proc. of the ICSE. 2018. 527-529.
[159] Davidson D, Moench B, Jha S, Ristenpart T. FIE on firmware:Finding vulnerabilities in embedded systems using symbolic execution. In:Proc. of the USENIX Security. 2013. 463-478.
[160] Guo S, Wu M, Wang C. Symbolic execution of programmable logic controller code. In:Proc. of the FSE. 2017. 326-336.
[161] Liu S, Zhang J. Program analysis:From qualitative analysis to quantitative analysis. In:Proc. of the ICSE. 2011. 956-959.
[162] Geldenhuys J, Dwyer MB, Visser W. Probabilistic symbolic execution. In:Proc. of the ISSTA. 2012. 166-176.
[163] Filieri A, Pasareanu CS, Visser W. Reliability analysis in symbolic pathFinder. In:Proc. of the ICSE. 2013. 622-631.
[164] Chen B, Liu Y, Le W. Generating performance distributions via probabilistic symbolic execution. In:Proc. of the ICSE. 2016.49-60.
[165] Filieri A, Pasareanu CS, Yang G. Quantification of software changes through probabilistic symbolic execution. In:Proc. of the ASE. 2015. 703-708.
[166] Godefroid P, Levin MY, Molnar D. SAGE:Whitebox fuzzing for security testing. Communications of the ACM, 2012,10(3):40-44.
[167] Miscrosfot. Visual studio 2015 RTM. 2018. https://www.visualstudio.com/news/vs2015-vs#Testing
[168] Xu Z, Zhang J, Wang J. Canalyze:A static bug-finding tool for C programs. In:Proc. of the ISSTA. 2014. 425-428.
[169] Cha S, Hong S, Lee J, Oh H. Automatically generating search heuristics for concolic testing. In:Proc. of the ICSE. 2018.1244-1254.
[170] Su T, Fu Z, Pu G, He J, Su Z. Combining symbolic execution and model checking for data flow testing. In:Proc. of the ICSE. 2015.654-665.
[171] Christakis M, Müller P, Wüstholz V. Guiding dynamic symbolic execution toward unverified program executions. In:Proc. of the ICSE. 2016. 144-155.
[172] Wang X, Sun J, Chen Z, Zhang P, Wang J, Lin Y. Towards optimal concolic testing. In:Proc. of the ICSE. 2018. 291-302.
[173] Stephens N, Grosen J, Salls C, Dutcher A, Wang R, Corbetta J, Shoshitaishvili Y, Kruegel C, Vigna G. Driller:Augmenting fuzzing through selective symbolic execution. In:Proc. of the NDSS. 2016. 21-24.
[174] Gosain A, Sharma G. A survey of dynamic program analysis techniques and tools. In:Proc. of the FICTA. 2014. 113-122.
[175] Kong P, Li Y, Chen X, Sun J, Sun M, Wang J. Towards concolic testing for hybrid systems. In:Proc. of the FM. 2016. 460-478.
[176] Chen Y, Poskitt CM, Sun J. Learning from mutants:Using code mutation to learn and monitor invariants of a cyber-physical system. In:Proc. of the SP. 2018. 648-660.
[177] Xiong Y, Wang B, Fu G, Zang L. Learning to synthesize. In:Proc. of the GI. 2018. 37-44.
[178] Heo K, Oh H, Yi K. Machine-Learning-Guided selectively unsound static analysis. In:Proc. of the ICSE. 2017. 519-529.
[179] Oh H, Yang H, Yi K. Learning a strategy for adapting a program analysis via Bayesian optimisation. In:Proc. of the OOPSLA.2015. 572-588.
[180] Heo K, Oh H, Yang H, Yi K. Adapting static analysis via learning with bayesian optimization. ACM Trans. on Programming Languages and Systems, 2018.
[181] Jeong S, Jeon M, Cha S, Oh H. Data-Driven context-sensitivity for points-to analysis. In:Proc. of the OOPSLA. 2017. 1-28.
[182] Enck W, Gilbert P, Chun BG, Cox LP, Jung J, McDaniel P, Sheth AN. TaintDroid:An information-flow tracking system for realtime privacy monitoring on smartphones. In:Proc. of the USENIX Security. 2014. 393-407.
[183] Hornyack P, Han S, Jung J, Schechter S, Wetherall D. These aren't the Droids you're looking for:Retrofitting Android to protect data from imperious applications. In:Proc. of the CCS. 2011. 639-652.
[184] DroidBox:Android application sandbox. 2018. http://code.google.com/p/droidbox/
[185] Yan LK, Yin H. DroidScope:Seamlessly reconstructing the OS and Dalvik semantic views for dynamic Android malware analysis.In:Proc. of the USENIX Security. 2014. 569-584.
[186] Bellard F. QEMU, a fast and portable dynamic translator. In:Proc. of the ATEC. 2005. 41-46.
[187] TEMU:The BitBlaze dynamic analysis component. 2018. http://bitblaze.cs.berkeley.edu/temu.html
[188] Gibler C, Crussell J, Erickson J, Chen H. AndroidLeaks:Automatically detecting potential privacy leaks in Android applications on a large scale. In:Proc. of the TRUST. 2012. 291-307.
[189] Feng Y, Anand S, Dillig I, Aiken A. Apposcopy:Semantics-Based detection of Android malware through static analysis. In:Proc.of the FSE. 2014. 576-587.
[190] Gordon MI, Kim D, Perkins J, Gilham L, Nguyen N, Rinard M. Information-Flow analysis of Android applications in DroidSafe. In:Proc. of the NDSS. 2015. 8-11.
[191] Jin X, Hu X, Ying K, Du W, Yin H, Peri GN. Code injection attacks on HTML5-based mobile apps:Characterization, detection and mitigation. In:Proc. of the CCS. 2014. 66-77.
[192] Egele M, Kruegel C, Kirda E, Vigna G. PiOS:Detecting privacy leaks in iOS applications. In:Proc. of the NDSS. 2011. 11.
[193] Octeau D, McDaniel P, Jha S, Bartel A, Bodden E, Klein J, Traon YL. Effective inter-component communication mapping in Android with Epicc:An essential step towards holistic security analysis. In:Proc. of the USENIX Security. 2013. 543-558.
[194] Wu T, Liu J, Xu Z, Guo C, Zhang Y, Yan J, Zhang J. Light-Weight, inter-procedural and callback-aware resource leak detection for Android apps. IEEE Trans. on Software Engineering, 2016,42(11):1054-1076.
[195] Chan PPF, Hui LCK, Yiu SM. DroidChecker:Analyzing Android applications for capability leak categories. In:Proc. of the WISEC. 2012. 125-136.
[196] Felt AP, Wang HJ, Moshchuk A, Hanna S, Chin E. Permission re-delegation:Attacks and defenses. In:Proc. of the USENIX Security. 2011. 22-22.
[197] Amalfitano D, Fasolino AR, Tramontana P, De Carmine S, Memon AM. Using GUI ripping for automated testing of Android applications. In:Proc. of the ASE. 2012. 258-261.
[198] Machiry A, Tahiliani R, Naik M. Dynodroid:An input generation system for Android apps. In:Proc. of the FSE. 2013. 224-234.
[199] Hu G, Yuan X, Tang Y, Yang J. Efficiently, effectively detecting mobile app bugs with AppDoctor. In:Proc. of the EuroSys. 2014.1-15.
[200] Mahmood R, Mirzaei N, Malek S. EvoDroid:Segmented evolutionary testing of Android apps. In:Proc. of the FSE. 2014.599-609.
[201] Mirzaei N, Garcia J, Bagheri H, Sadeghi A, Malek S. Reducing combinatorics in GUI testing of Android applications. In:Proc. of the ICSE. 2016. 559-570.
[202] You W, Liang B, Shi W, Zhu S, Wang P, Xie S, Zhang X. Reference hijacking:Patching, protecting and analyzing on unmodified and non-rooted Android devices. In:Proc. of the ICSE. 2016. 959-970.
[203] Au KWY, Zhou YF, Huang Z, Lie D. PScout:Analyzing the Android permission specification. In:Proc. of the CCS. 2012.217-228.
[204] Cao Y, Fratantonio Y, Bianchi A, Egele M, Kruegel C, Vigna G, Chen Y. EdgeMiner:Automatically detecting implicit control flow transitions through the Android framework. In:Proc. of the NDSS. 2015. 8-11.
[205] Rasthofer S, Arzt S, Bodden E. A machine-learning approach for classifying and categorizing Android sources and sinks. In:Proc.of the NDSS. 2014. 23-26.
[206] Zhang Y, Luo X, Yin H. DexHunter:Toward extracting hidden code from packed Android applications. In:Proc. of the ESORICS.2015. 293-311.
[207] Xue L, Luo X, Yu L, Wang S, Wu D. Adaptive unpacking of Android apps. In:Proc. of the ICSE. 2017. 358-369.
[208] Clarke EM, Emerson EA, Sistla AP. Automatic verification of finite-state concurrent systems using temporal logic specifications.Trans. on Programming Languages and Systems, 1986,8(2):244-263.
[209] Bron A, Farchi E, Magid Y, Nir Y, Ur S. Applications of synchronization coverage. In:Proc. of the PPoPP. 2005. 206-212.
[210] Krena B, Letko Z, Vojnar T. Coverage metrics for saturation-based and search-based testing of concurrent software. In:Proc. of the RV. 2011. 177-192.
[211] Sorrentino F, Farzan A, Madhusudan P. PENELOPE:Weaving threads to expose atomicity violations. In:Proc. of the FSE. 2010.37-46.
[212] Wang C, Said M, Gupta A. Coverage guided systematic concurrency testing. In:Proc. of the ICSE. 2011. 221-230.
[213] Musuvathi M, Qadeer S, Ball T, Basler G, Nainar PA, Neamtiu I. Finding and reproducing heisenbugs in concurrent programs. In:Proc. of the OSDI. 2008. 267-280.
[214] Kahlon V, Sinha N, Kruus E, Zhang Y. Static data race detection for concurrent programs with asynchronous calls. In:Proc. of the FSE. 2009. 13-22.
[215] Naik M, Aiken A, Whaley J. Effective static race detection for Java. In:Proc. of the PLDI. 2006. 308-319.
[216] Voung JW, Ranjit J, Lerner S. RELAY:Static race detection on millions of lines of code. In:Proc. of the FSE. 2007. 205-214.
[217] Cai Y, Wu S, Chan WK. ConLock:A constraint-based approach to dynamic checking on deadlocks in multithreaded programs. In:Proc. of the ICSE. 2014. 491-502.
[218] Pozniansky E, Schuster A. Efficient on-the-fly data race detection in multihreaded C++programs. In:Proc. of the PPoPP. 2003.179-190.
[219] Savage S, Burrows M, Nelson G, Sobalvarro P, Anderson T. Eraser:A dynamic data race detector for multithreaded programs.ACM Trans. on Computer Systems, 1997,15(4):391-411.
[220] Yu Y, Rodeheffer T, Chen W. RaceTrack:Efficient detection of data race conditions via adaptive tracking. In:Proc. of the SOSP.2005. 221-234.
[221] Xie X, Xue J. Acculock:Accurate and efficient detection of data races. In:Proc. of the CGO. 2011. 201-212.
[222] Kasikci B, Zamfir C, Candea G. RaceMob:Crowdsourced data race detection. In:Proc. of the SOSP. 2013. 406-422.
[223] Williams A, Thies W, Ernst M. Static deadlock detection for Java libraries. In:Proc. of the ECOOP. 2005. 602-629.
[224] Clarke EM, Emerson EA. Design and synthesis of synchronization skeletons using branching time temporal logic. In:Proc. of the Logic of Programs. 1981. 52-71.
[225] Bach M, Charney M, Cohn R, Demikhovsky E, Devor T, Hazelwood K, Jaleel A, Luk C, Lyons G, Patil H, Tal A. Analyzing parallel programs with pin. IEEE Computer, 2010,43(3):34-41.
[226] Eslamimehr M, Palsberg J. Race directed scheduling of concurrent programs. In:Proc. of the PPoPP. 2014. 301-314.
[227] Edelstein O, Farchi E, Nir Y, Ratsaby G, Ur S. Multithreaded Java program test generation. IBM Systems Journal, 2002,41(1):111-125.
[228] Burckhardt S, Kothari P, Musuvathi M, Nagarakatte S. A randomized scheduler with probabilistic guarantees of finding bugs. In:Proc. of the ASPLOS. 2010. 167-178.
[229] Cai Y, Yang Z. Radius aware probabilistic testing of deadlocks with guarantees. In:Proc. of the ASE. 2016. 356-367.
[230] Fonseca P, Rodrigues R, B.Brandenburg B. SKI:Exposing kernel concurrency bugs through systematic schedule exploration. In:Proc. of the OSDI. 2014. 415-431.
[231] Yu J, Narayanasamy S, Pereira C, Pokam G. Maple:A coverage-driven testing tool for multithreaded programs. In:Proc. of the OOPSLA. 2012.
[232] Abdelrasoul M. Promoting secondary orders of event pairs in randomized scheduling using a randomized stride. In:Proc. of the ASE. 2017. 741-752.
[233] Lu S, Park S, Seo E, Zhou Y. Learning from mistakes—A comprehensive study on real world concurrency bug characteristics. In:Proc. of the ASPLOS. 2008. 329-339.
[234] Flanagan C, Freund SN. FastTrack:Efficient and precise dynamic race detection. Communications of the ACM, 2010,53(11):93-101.
[235] Cai Y, Cao L. Effective and precise dynamic detection of hidden races for Java programs. In:Proc. of the FSE. 2015. 450-461.
[236] Smaragdakis Y, Evans JM, Sadowski C, Yi J, Flanagan C. Sound predictive race detection in polynomial time. In:Proc. of the POPL. 2012. 387-400.
[237] Marino D, Musuvathi M, Narayanasamy S. LiteRace:Effective sampling for lightweight data-race detection. In:Proc. of the PLDI.2009. 134-143.
[238] Bond MD, Coons KE, Mckinley KS. PACER:Proportional detection of data races. In:Proc. of the PLDI. 2010. 255-268.
[239] Zhai K, Xu B, Chan WK, Tse TH. CARISMA:A context-sensitive approach to race-condition sample-instance selection for multithreaded applications. In:Proc. of the ISSTA. 2012. 221-231.
[240] Erickson J, Musuvathi M, Burckhardt S, Olynyk K. Effective data-race detection for the kernel. In:Proc. of the OSDI. 2010. 1-16.
[241] Sen K. Race directed random testing of concurrent programs. In:Proc. of the PLDI. 2008. 11-21.
[242] Joshi P, Park CS, Sen K, Naik M. A randomized dynamic program analysis technique for detecting real deadlocks. In:Proc. of the PLDI. 2009. 110-120.
[243] Huang J, Meredith PO, Rosu G. Maximal sound predictive race detection with control flow abstraction. In:Proc. of the PLDI. 2013.337-348.
[244] Cai Y, Zhang J, Cao L, Liu J. A deployable sampling strategy for data race detection. In:Proc. of the PLDI. 2016. 810-821.
[245] Guo Y, Cai Y, Yang Z. AtexRace:Across thread and execution sampling for in-house race detection. In:Proc. of the FSE. 2017.315-325.
[246] Lu S, Tucek J, Qin F, Zhou Y. AVIO:Detecting atomicity violations via access-interleaving invariants. In:Proc. of the ASPLOS.2006. 37-48.
[247] Lu S, Park S, Hu C, Ma X, Jiang W, Li Z, Popa RA, Zhou Y. MUVI:Automatically inferring multi-variable access correlations and detecting related semantic and concurrency bugs. In:Proc. of the SOSP. 2007. 103-116.
[248] Park CS, Sen K. Randomized active atomicity violation detection in concurrent programs. In:Proc. of the FSE. 2008. 135-145.
[249] Muzahid A, Otsuki N, Torrellas J. AtomTracker:A comprehensive approach to atomic region inference and violation detection. In:Proc. of the MICRO. 2010. 287-297.
[250] Cai Y, Chan WK. MagicFuzzer:Scalable deadlock detection for large-scale applications. In:Proc. of the ICSE. 2012. 606-616.
[251] Cai Y, Chan WK. Magiclock:Scalable detection of potential deadlocks in large-scale multithreaded programs. IEEE Trans, on Software Engineering, 2014,40(3):266-281.
[252] Cai Y, Lu Q. Dynamic testing for deadlocks via constraints. IEEE Trans, on Software Engineering, 2016,42(9):825-842.
[253] Cai Y, Jia C, Wu S, Zhai K, Chan WK. ASN:A dynamic barrier-based approach to confirmation of deadlocks from warnings for large-scale multithreaded programs. IEEE Trans. on Parallel and Distributed Systems, 2015,26(1):13-23.
[254] Pradel M, Gross TR. Fully automatic and precise detection of thread safety violations. In:Proc. of the PLDI. 2012. 521-530.
[255] Choudhary A, Lu S, Pradel M. Efficient detection of thread safety violations via coverage-guided generation of concurrent tests. In:Proc. of the ICSE. 2017. 266-277.
[256] The 10 biggest cloud outages of 2014. 2018. http://www.crn.com/slide-shows/cloud/300075204/the-10-biggest-cloud-outages-of-2014.html
[257] Gunawi HS, Hao M, Leesatapornwongsa T, Patana-anake T, Do T, Adityatama J, Eliazar KJ, Laksono A, Lukman JF, Martin V,Satria AD. What bugs live in the cloud? A study of 3000+issues in cloud systems. In:Proc. of the SOCC. 2014. 1-14.
[258] Leesatapornwongsa T, Lukman JF, Lu S, Gunawi HS. TaxDC:A taxonomy of non-deterministic concurrency bugs in datacenter distributed systems. In:Proc. of the ASPLOS. 2016. 517-530.
[259] Dai T, He J, Gu X, Lu S. Understanding real-world timeout problems in cloud server systems. In:Proc. of the IC2E. 2018. 1-11.
[260] Gao Y, Dou W, Qin F, Gao C, Wang D, Wei J, Huang R, Zhou L, Wu Y. An empirical study on crash recovery bugs in large-scale distributed systems. In:Proc. of the FSE. 2018. 539-550.
[261] Guo Z, McDirmid S, Yang M, Zhuang L, Zhang P, Luo Y, Bergan T, Bodik P, Musuvathi M, Zhang Z, Zhou L. Failure recovery:When the cure is worse than the disease. In:Proc. of the HotOS. 2013. 1-6.
[262] Yuan D, Luo Y, Zhuang X, Rodrigues GR, Zhao X, Zhang Y, Jain PU, Stumm M. Simple testing can prevent most critical failures:An analysis of production failures in distributed data-intensive systems. In:Proc. of the OSDI. 2014. 249-265.
[263] Wang G, Zhang L, Xu W. What can we learn from four years of data center hardware failures? In:Proc. of the DSN. 2017. 25-36.
[264] Liu H, Li G, Lukman JF, Li J, Lu S, Gunawi HS, Tian C. DCatch:Automatically detecting distributed concurrency bugs in cloud systems cloud systems. In:Proc. of the ASPLOS. 2017. 677-691.
[265] Liu H, Wang X, Li G, Lu S, Ye F, Tian C. FCatch:Automatically detecting time-of-fault bugs in cloud systems. In:Proc. of the ASPLOS. 2018. 1-11.
[266] Liu X, Guo Z, Wang X, Chen F, Lian X, Tang J, Wu M, Kaashoek MF, Zhang Z. D3S:Debugging deployed distributed systems. In:Proc. of the NSDI. 2008. 423-437.
[267] Xu W, Huang L, Fox A, Patterson D, Jordan MI. Detecting large-scale system problems by mining console logs. In:Proc. of the SOSP. 2009. 117-132.
[268] Grant S, Cech H, Beschastnikh I. Inferring and asserting distributed system invariants. In:Proc. of the ICSE. 2018. 1149-1159.
[269] Scott C, Panda A, Brajkovic V, Necula G, Krishnamurthy A, Shenker S. Minimizing faulty executions of distributed systems. In:Proc. of the NSDI. 2016. 291-309.
[270] Flanagan C, Godefroid P. Dynamic partial-order reduction for model checking software. In:Proc. of the POPL. 2005. 110-121.
[271] Zeller A, Hildebrandt R. Simplifying and isolating failure-inducing input. IEEE Trans. on Software Engineering, 2002,28(2):183-200.
[272] Wilcox JR, Woos D, Panchekha P, Tatlock Z, Wang X, Ernst MD, Anderson T. Verdi:A framework for implementing and formally verifying distributed systems. In:Proc. of the PLDI. 2015. 357-368.
[273] 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 SOSP. 2015. 1-17.
[274] Lesani M, Bell CJ, Chlipala A. Chapar:Certified causally consistent distributed key-value stores. In:Proc. of the POPL. 2016.357-370.
[275] Fonseca P, Zhang K, Wang X, Krishnamurthy A. An empirical study on the correctness of formally verified distributed systems. In:Proc. of the EuroSys. 2017. 328-343.
[276] Yang J, Chen T, Wu M, Xu Z, Liu X, Lin H, Yang M, Long F, Zhang L, Zhou L. MODIST:Transparent model checking of unmodified distributed systems. In:Proc. of the NSDI. 2009. 213-228.
[277] Guo H, Wu M, Zhou L, Hu G, Yang J, Zhang L. Practical software model checking via dynamic interface reduction. In:Proc. of the SOSP. 2011. 265-278.
[278] Leesatapornwongsa T, Hao M, Joshi P, Lukman JF, Gunawi HS. SAMC:Semantic-Aware model checking for fast discovery of deep bugs in cloud systems. In:Proc. of the OSDI. 2014. 399-414.
[279] Sasnauskas R, Dustmann OS, Kaminski BL, Wehrle K, Weise C, Kowalewski S. Scalable symbolic execution of distributed systems. In:Proc. of the ICDCS. 2011. 333-342.
[280] Joahi P, Ganai M, Balakrishnan G, Gupta A, Papakonstantinou N. SETSUDO:Perturbation-Based testing framework for scalable distributed systems pallavi. In:Proc. of the TRIOS. 2013. 1-14.
[281] Joshi P, Gunawi HS, Sen K. PREFAIL:A programmable tool for multiple-failure injection. In:Proc. of the OOPSLA. 2011.171-188.
[282] Gunawi HS, Do T, Joshi P, Alvaro P, Hellerstein JM, Arpaci-Dusseau AC, Arpaci-Dusseau RH, Sen K, Borthakur D. FATE and DESTINI:A framework for cloud recovery testing. In:Proc. of the NSDI. 2011. 1-18.
[283] Alagappan R, Ganesan A, Patel Y, Pillai TS, Arpaci-Dusseau AC, Arpaci-Dusseau RH. Correlated crash vulnerabilities. In:Proc. of the OSDI. 2016. 151-167.
[284] Ganesan A, Alagappan R, Arpaci-Dusseau AC, Arpaci-Dusseau RH. Redundancy does not imply fault tolerance:Analysis of distributed storage reactions to file-system faults. In:Proc. of the FAST. 2017. 149-166.
[285] Alvaro P, Rosen J, Hellerstein JM. Lineage-Driven fault injection. In:Proc. of the SIGMOD. 2015. 331-346.
[286] Thompson K. Reflections on trusting trust. Communications of the ACM, 1984,27(8):761-763.
[287] Xiao C. Novel malware xcodeghost modifies xcode, infects apple iOS apps and hits app store. Technical Report, 2018.https://researchcenter.paloaltonetworks.com/2015/09/novel-malware-xcodeghost-modifies-xcode-infects-apple-ios-apps-and-hits-ap p-store/
[288] De Sutter B, de Bus B, de Bosschere K, Keyngnaert P, Demoen B. On the static analysis of indirect control transfers in binaries. In:Proc. of the PDPTA. 2000.
[289] Kinder J. Static analysis of x86 executables(statische analyse von programmen in x86-Maschinensprache)[Ph.D. Thesis].Fachbereich Informatik, Technische Universitat Darmstadt, 2010.
[290] Cifuentes C, van Emmerik M. Recovery of jump table case statements from binary code. Science of Computer Programming, 2001,40(2-3):171-188.
[291] Kinder J, Veith H. Jakstab:A static analysis platform for binaries. In:Proc. of the CAV. 2008. 423-427.
[292] Xu L, Sun F, Su Z. Constructing precise control flow graphs from binaries. Technical Report, 2009.
[293] Shin ECR, Song D, Moazzezi R. Recognizing functions in binaries with neural networks. In:Proc. of the USENIX Security. 2015.611-626.
[294] Andriesse D, Chen X, Van der Veen V, Slowinska A, Bos H. An in-depth analysis of disassembly on full-scale x86/x64 binaries. In:Proc. of the USENIX Security. 2016. 583-600.
[295] Chua ZL, Shen S, Saxena P, Liang Z. Neural nets can learn function type signatures from binaries. In:Proc. of the USENIX Security. 2017. 99-116.
[296] Tr(o|¨)ger J, Cifuentes C. Analysis of virtual method invocation for binary translation. In:Proc. of the WCRE. 2002. 65-74.
[297] Balakrishnan G, Reps T. Analyzing memory accesses in x86 executables. In:Proc. of the CC. 2004. 5-23.
[298] Jin W, Cohen C, Gennari J, Hines C, Chaki S, Gurfinkel A, Havrilla J, Narasimhan P. Recovering C++objects from binaries using inter-procedural data-flow analysis. In:Proc. of the POPL. 2014. 1-11.
[299] Lin Z, Zhang X, Xu D. Automatic reverse engineering of data structures from binary execution. In:Proc. of the NDSS. 2010.
[300] Zeng J, Lin Z. Towards automatic inference of kernel object semantics from binary code. In:Proc. of the RAID. 2015. 538-561.
[301] Smithson M, El Wazeer K, Anand K, Kotha A, Barua R. Static binary rewriting without supplemental information:Overcoming the tradeoff between coverage and correctness. In:Proc. of the WCRE. 2013. 52-61.
[302] Wang S, Wang P, Wu D. UROBOROS:Instrumenting stripped binaries with static reassembling. In:Proc. of the SANER. 2016.236-247.
[303] Wang S, Wang P, Wu D. Reassembleable disassembling. In:Proc. of the USENIX Security. 2015. 627-642.
[304] Wang R, Shoshitaishvili Y, Bianchi A, Machiry A, Grosen J, Grosen P, Kruegel C, Vigna G. RAMBLR:Making reassembly great again. In:Proc. of the NDSS. 2017.
[305] Song D, Brumley D, Yin H, Caballero J, Jager I, Kang MG, Liang Z, Newsome J, Poosankam P, Saxena P. BitBlaze:A new approach to computer security via binary analysis. In:Proc. of the ICISS. 2008. 1-25.
[306] Brumley D, Jager I, Avgerinos T, Schwartz EJ. BAP:A binary analysis platform. In:Proc. of the CAV. 2011. 463-469.
[307] Bruening D. Efficient, transparent, and comprehensive runtime code manipulation[Ph.D. Thesis]. Massachusetts Institute of Technology, 2004.
[308] Bernat AR, Miller BP. Anywhere, any-time binary instrumentation. In:Proc. of the PASTE. 2011. 9-16.
[309] Nethercote N, Seward J. Valgrind:A framework for heavyweight dynamic binary instrumentation. In:Proc. of the PLDI. 2007.89-100.
[310] Luk CK, Cohn R, Muth R, Patil H, Klauser A, Lowney G, Wallace S, Reddi VJ, Hazelwood K. Pin:Building customized program analysis tools with dynamic instrumentation. In:Proc. of the PLDI. 2005. 190-200.
[311] Machiry A, Spensky C, Corina J, Stephens N, Kruegel C, Vigna G, Barbara S. DR.CHECKER:A soundy analysis for Linux kernel drivers. In:Proc. of the USENIX Security. 2017. 1007-1024.
[312] Wang P, Krinke J, Lu K, Li G, Dodier-Lazaro S. How double-fetch situations turn into double-fetch vulnerabilities:A study of double fetches in the Linux kernel. In:Proc. of the USENIX Security. 2017. 1-16.
[313] Dewey D, Giffin J. Static detection of C++vtable escape vulnerabilities in binary code. In:Proc. of the NDSS. 2012.
[314] Kruegel C, Robertson W, Vigna G. Detecting kernel-level rootkits through binary analysis. In:Proc. of the ACSAC. 2004. 91-100.
[315] Bergeron J, Debbabi M, Erhioui MM, Ktari B. Static analysis of binary code to isolate malicious behaviors. In:Proc. of the WETICE. 1999. 184-189.
[316] Bergeron J, Debbabi M, Desharnais J, M.Erhioui M, Lavoie Y, Tawbi N. Static detection of malicious code in executable programs.In:Proc. of the Symp. on Requirements Engineering for Information Security. 2001.
[317] O'Sullivan P, Anand K, Kotha A, Smithson M, Barua R, Keromytis AD. Retrofitting security in COTS software with binary rewriting. In:Proc. of the SEC. 2011. 154-172.
[318] Wartell R, Mohan V, Hamlen KW, Lin Z. Binary stirring:Self-Randomizing instruction addresses of legacy x86 binary code. In:Proc. of the Computer and Communications Security. New York:ACM Press, 2012. 157-168.
[319] Wartell R, Mohan V, Hamlen KW, Lin Z. Securing untrusted code via compiler-agnostic binary rewriting. In:Proc. of the ACSAC.ACM Press, 2012. 299-308.
[320] Zhang M, Sekar R. Contol flow integrity for COTS binaries. In:Proc. of the USENIX Security. 2013. 337-352.
[321] Batyuk L, Herpich M, Camtepe SA, Raddatz K, Schmidt AD, Albayrak S. Using static analysis for automatic assessment and mitigation of unwanted and malicious activities within Android applications. In:Proc. of the MALWARE. 2011. 66-72.
[322] Zhang C, Song C, Chen KZ, Chen Z, Song D. VTint:Protecting virtual function tables’ integrity. In:Proc. of the NDSS. 2015.
[323] Xu Z, Zhang J. A test data generation tool for unit testing of C programs. In:Proc. of the QSIC. 2006. 107-116.
[324] Wu R, Wen M, Cheung SC, Zhang H. ChangeLocator:Locate crash-inducing changes based on crash reports. Empirical Software Engineering, 2017,23(5):2866-2900.
[325] Gao Q, Xiong Y, Mi Y, Zhang L, Yang W, Zhou Z, Xie B, Mei H. Safe memory-leak fixing for C programs. In:Proc. of the ICSE.2015. 459-470.
[326] Xuan J, Martinez M, De Marco F, Clement M, Marcote SL, Durieux T, Le Berre D, Monperrus M. NOPOL:Automatic repair of conditional statement bugs in Java programs. IEEE Trans. on Software Engineering, 2017,43(1):34-55.
[327] Briand LC, Daly JW, Wust J. A unified framework for cohesion measurement in object-oriented systems. Empirical Software Engineering, 1998,3(1):65-117.
[328] Briand LC, Daly JW, Wust JK. A unified framework for coupling measurement in object-oriented systems. IEEE Trans. on Software Engineering, 1999,25(1):91-121.
[329] Ethereum. 2018. https://www.ethereum.org/
[330] The DAO attacked:Code issue leads to 60 million ether theft. 2018. https://www.coindesk.com/dao-attacked-code-issue-leads-60-million-ether-theft/
[331] Accidental bug may have frozen$280 million worth of digital coinether in a cryptocurrency wallet. 2018. https://www.cnbc.com/2017/11/08/accidental-bug-may-have-frozen-280-worth-of-ether-on-parity-w allet.html
[332] Luu L, Chu DH, Olickel H, Saxena P, Hobor A. Making smart contracts smarter. In:Proc. of the CCS. 2016. 254-269.
[333] Nikolic I, Kolluri A, Sergey I, Saxena P, Hobor A. Finding the greedy, prodigal, and suicidal contracts at scale. In:Proc. of the CoRR. 2018. https://arxiv.org/pdf/1802.06038.pdf
[334] Hirai Y. Formal verification of deed contract in ethereum name service. Technical Report, 2016. 1-81.
[335] Bhargavan K, Delignat-Lavaud A, Fournet C, Gollamudi A, Gonthier G, Kobeissi N, Kulatova N, Rastogi A, Sibut-Pinote T,Swamy N, Zanella-Béguelin S. Formal verification of smart contracts. In:Proc. of the PLAS. 2016. 91-96.
[336] Bigi G, Bracciali A, Meacci G, Tuosto E. Validation of decentralised smart contracts through game theory and formal methods. In:Proc. of the Programming Languages with Applications to Biology and Security. 2015. 142-161.
[337] Kalra S, Goel S, Dhawan M, Sharma S. ZEUS:Analyzing safety of smart contracts. In:Proc. of the NDSS. 2018.
[338] Tsankov P, Dan A, Drachsler-Cohen D, Gervais A, Bunzli F, Vechev M. Securify:Practical security analysis of smart contracts. In:Proc. of the CoRR. 2018. https://arxiv.org/pdf/1806.01143.pdf
[339] Gurfinkel A, Kahsai T, Komuravelli A, Navas JA. The SeaHorn verification framework. In:Proc. of the CAV. 2004. 343-361.
[340] Masuda S, Ono K, Yasue T, Hosokawa N. A survey of software quality for machine learning applications. In:Proc. of the ICSTW.2018. 279-284.
[341] Qin Y, Wang H, Xu C, Ma X, Lu J. SynEva:Evaluating ML programs by mirror program synthesis. In:Proc. of the QRS. 2018.171-182.
[342] Sun Y, Wu M, Ruan W, Huang X, Kwiatkowska M, Kroening D. Concolic testing for deep neural networks. In:Proc. of the ASE.2018. 109-119.
[343] Ruan W, Huang X, Kwiatkowska M. Reachability analysis of deep neural networks with provable guarantees. In:Proc. of the IJCAI. 2018. 2651-2659.
[344] Huang X, Kwiatkowska M, Wang S, Wu M. Safety verification of deep neural networks. In:Proc. of the CAV. 2017. 3-29.
[345] Ma S, Aafer Y, Xu Z, Lee WC, Zhai J, Liu Y, Zhang X. LAMP:Data provenance for graph based machine learning algorithms through derivative computation. In:Proc. of the FSE. 2017. 786-797.
[346] Gulzar MA, Interlandi M, Yoo S, Tetali SD, Condie T, Millstein T, Kim M. BigDebug:Debugging primitives for interactive big data processing in spark. In:Proc. of the ICSE. 2016. 784-795.
[1]梅宏,王千祥,张路,王戟.软件分析技术进展.计算机学报,2009,32(9):1697-1710.
[97]张健.精确的程序静态分析.计算机学报,2008,31(9):1549-1553.