Computer Science ›› 2018, Vol. 45 ›› Issue (6A): 28-35.
• Review • Previous Articles Next Articles
YE Zhi-bin,YAN Bo
CLC Number:
[1]BOYER R S,ELSPAS B,LEVITT K N.Select—a formal sys- tem for testing and debugging programs by symbolic execution[C]∥International Conference on Reliable Software.New York,USA,ACM,1975:234-245. [2]KING J C.Symbolic execution and program testing[J].Communications of the Acm,1976,19(7):385-394. [3]MYERS G J.Art of Software Testing.New York:John Wiley & Sons,Inc.,1979. [4]CADAR.Symbolic Execution for Software Testing in Practice-a Preliminary Assessment[C]∥International Conference on Software Engineering.IEEE,2011:1066-1071. [5]SEN K.Concolic testing[C]∥Ieee/acm International Conferen- ce on Automated Software Engineering.ACM,2007:571-572. [6]MESNARD F, TIENNE P,GERMN V.Concolic testing in logic programming[J].Theory & Practice of Logic Programming,2015,15(4/5):711-725. [7]PALACIOS A,VIDAL G.Concolic Execution in Functional Programming by Program Instrumentation[C]∥International Symposium on Logic-Based Program Synthesis and Transformation.Springer International Publishing,2015:277-292. [8]SEN K.Concolic testing:a decade later (keynote)[C]∥International Workshop on Dynamic Analysis.ACM,2015:1-1. [9]CADAR C,GANESH V,PAWLOWSKI P M,et al.EXE:automatically generating inputs of death[C]∥Proceedings of the 13th ACM Conference on Computer and Communications Security.ACM,2006:322-335. [10]CADAR C,ENGLER D.Execution Generated Test Cases:How to Make Systems Code Crash Itself[M]∥Model Checking Software.DBLP,2005:902-902. [11]CADAR C,SEN K.Symbolic execution for software testing: three decades later.http://www.cs.umd.edu/class/fall2017/cmsc818O/papers/symbolic-execution.pdf. [12] CHIPOUNOV V,GEORGESCU V,ZAMFIR C,et al.Selective Symbolic Execution[C]∥The Workshop on Hot Topics in System Dependability.2009:1286-1299. [13]MAJUMDAR R,SEN K.Hybrid Concolic Testing[C]∥International Conference on Software Engineering.IEEE,2007:416-426. [14]WEN S,FENG C,MENG Q,et al.Testing Network Protocol Binary Software with Selective Symbolic Execution[C]∥International Conference on Computational Intelligence and Security.IEEE,2017:318-322. [15]MORAN K,LINARES-VSQUEZ,BERNAL-CRDENAS, et al. Denys Poshyvanyk[C]∥2016 IEEE International Conference on Automatically Discovering Reporting and Reproducing Android Application Crashes,Software Testing Verification and Validation (ICST).2016:33-44. [16]STEPHENS N,GROSEN J,SALLS C,et al.Driller:Augmen- ting fuzzing through selective symbolic execution[C]∥23nd Annual Network and Distributed System Security Symposium(NDSS 2016).2016. [17]CADAR C,DUNBAR D,ENGLER D R.KLEE:Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs[C]∥Usenix Conference on Operating Systems Design and Implementation.USENIX Association,2008:209-224. [18]BURNIM J,SEN K.Heuristics for Scalable Dynamic Test Gene- ration[C]∥IEEE/ACM International Conference on Automated Software Engineering.2008:443-446. [19]SEN K,AGHA G.CUTE and jCUTE:Concolic Unit Testing and Explicit Path Model-Checking Tools∥International Conference on Computer Aided Verification.2006:419-423. [20]BOONSTOPPEL P,CADAR C,ENGLER D.RWset:Attacking Path Explosion in Constraint-Based Test Generation[C]∥Theory and Practice of Software,International Conference on TOOLS and Algorithms for the Construction and Analysis of Systems.Springer-Verlag,2008:351-366. [21]GODEFROID P.Compositional dynamic test generation[C]∥Proceedings of the 34th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages(POPL 2007).New York,USA,ACM,2007:47-54. [22]HANSEN T,SCHACHTE P,S NDERGAARD H.Runtime verification.chapter State Joining and Splitting for the Symbolic Execution of Binaries[M]∥Berlin:Springer-Verlag,2009:76-92. [23]KUZNETSOV V,KINDER J,BUCUR S,et al.Efficient state merging in symbolic execution.In Proceedings of the 33rd ACM SIGPLAN Conference on Programming Language Design and Implementation(PLDI 2012).New York,USA,ACM,2012:193-204. [24]AVGERINOS T,REBERT A,SANG K C,et al.Enhancing symbolic execution with veritesting∥International Conferen-ce on Software Engineering.ACM,2014:1083-1094. [25]MARINESCU P D,CADAR C.make test-zesti:a symbolic execution solution for improving regression testing[C]∥International Conference on Software Engineering.IEEE,2012:716-726. [26]ENGLER D,DUNBAR D.Under-constrained execution:making automatic code destruction easy and scalable[C]∥International Symposium of Software Testing and Analysis.ACM,2007:1-4. [27]RAMOS D A,ENGLER D.Under-constrained symbolic execution:correctness checking for real code[C]∥Usenix Conference on Security Symposium.USENIX Association,2015:49-64. [28]MOURA L D,BJ RNER N.Z3:An Efficient SMT Solver∥ Tools and Algorithms for the Construction and Analysis of Systems.Springer Berlin Heidelberg,2008:337-340. [29]SANG K C,AVGERINOS T,REBERT A,et al.Unleashing Mayhem on Binary Code[C]∥Security and Privacy.IEEE,2012:380-394. [30]BARRETT C,BEREZIN S.CVC Lite:A New Implementation of the Cooperating Validity Checker[C]∥Computer Aided Verification,International Conference(CAV 2004).Boston,MA,USA,DBLP,2004:515-518. [31]BARRETT C,TINELLI C.19th International Conference on Computer Aided Verification (CAV’07)[M]∥Damm W,Hermanns H,eds.Berlin:Springer,2007:298-302. [32]ENDERTON H B,COMPUTABILITY M D,UNSOLVABILITY.Hilbert’s Tenth Problem is Unsolvable∥American Mathematical Monthly.1973:233-269. [33]XIAO X,XIE T,TILLMANN N,et al.Precise identification of problems for structural test generation[C]∥ICSE 2011.ACM,2011:611-620. [34]RAMOS D A,ENGLER D.Under-constrained symbolic execution:correctness checking for real code[C]∥Usenix Conference on Security Symposium.USENIX Association,2015:49-64. [35]SEN K,AGHA G.CUTE and jCUTE:Concolic Unit Testing and Explicit Path Model-Checking Tools[C]∥International Conference on Computer Aided Verification.Springer-Verlag,2006:419-423. [36]CHAUDHURI A,FOSTER J S.Symbolic security analysis of ruby-on-rails web applications[C]∥ACM Conference on Computer and Communications Security.ACM,2010:585-594. [37]TILLMANN N,DE HALLEUX J.Pex:white box test generation for .NET∥Tests & Proofs,Second International Conference.Tap,Prato,Italy,2008:134-153. [38]P S REANU C S,RUNGTA N.Symbolic PathFinder:sym- bolic execution of Java bytecode[C]∥IEEE/ACM International Conference on Automated Software Engineering(ASE 2010).Antwerp,Belgium,DBLP,2010:179-180. [39]SHOSHITAISHVILI Y,WANG R,SALLS C,et al.SOK: (State of) The Art of War:Offensive Techniques in Binary Analysis[C]∥2016 IEEE Symposium on Security and Privacy (SP).IEEE,2016:138-157. [40]YAN S,WANG R,HAUSER C,et al.Firmalice-Automatic Detection of Authentication Bypass Vulnerabilities in Binary Firmware[C]∥Network and Distributed System Security Sympo-sium.2015. [41]STEPHENS N,GROSEN J,SALLS C,et al.Driller:Augmen- ting Fuzzing Through Selective Symbolic Execution[C]∥Network and Distributed System Security Symposium.2016. [42]LEVIN M Y,LEVIN M Y,MOLNAR D.SAGE:whitebox fuzzing for security testing.https://www.researchgate.net/publication/220309880_SAGE_Whitebox_Fuzzing_for_Security_Testing. [43]GODEFROID P,KLARLUND N,SEN K.DART:directed automated random testing[C]∥ACM Sigplan Conference on Programming Language Design and Implementation.ACM,2005:213-223. [44]SONG D,BRUMLEY D,YIN H,et al.BitBlaze:A New Approach to Computer Security via Binary Analysis[C]∥Information Systems Security,International Conference(ICISS 2008).Hyderabad,India,DBLP,2008:1-25. [45]BABIC′ D,MARTIGNONI L,MCCAMANT S,et al.Statically-directed dynamic automated test generation[C]∥Proceedings of the 2011 International Symposium on Software Testing and Analysis.ACM,2011:12-22. [46]MARTIGNONI L,MCCAMANT S,POOSANKAM P,et al. Path-exploration lifting:Hi-fi tests for lo-fi emulators[C]∥ACM SIGARCH Computer Architecture News.ACM,2012:337-348. |
[1] | ZHOU Sheng-yi, ZENG Hong-wei. Program Complexity Analysis Method Combining Evolutionary Algorithm with Symbolic Execution [J]. Computer Science, 2021, 48(12): 107-116. |
[2] | HUANG Zhao,HUANG Shu-guang,DENG Zhao-kun,HUANG Hui. Automatic Vulnerability Detection and Test Cases Generation Method for Vulnerabilities Caused by SEH [J]. Computer Science, 2019, 46(7): 133-138. |
[3] | FANG Hao, WU Li-fa, WU Zhi-yong. Automatic Return-to-dl-resolve Exploit Generation Method Based on Symbolic Execution [J]. Computer Science, 2019, 46(2): 127-132. |
[4] | CHEN Zheng-zhao, JIANG Ren-he, PAN Min-xue, ZHANG Tian, LI Xuan-dong. Empirical Study of Code Query Technique Based on Constraint Solving on StackOverflow [J]. Computer Science, 2019, 46(11): 137-144. |
[5] | ZHANG Yong-gang, CHENG Zhu-yuan. Research Progress on Max Restricted Path Consistency Constraint Propagation Algorithms [J]. Computer Science, 2018, 45(6A): 41-45. |
[6] | LI Hang, ZANG Lie, GAN Lu. Search of Speculative Symbolic Execution Path Based on Ant Colony Algorithm [J]. Computer Science, 2018, 45(6): 145-150. |
[7] | ZHANG Jing, ZHOU An-min, LIU Liang, JIA Peng and LIU Lu-ping. Review of Crash Exploitability Analysis Methods [J]. Computer Science, 2018, 45(5): 5-14. |
[8] | DENG Wei and LI Zhao-peng. State Merging for Symbolic Execution Engine with Shape Analysis [J]. Computer Science, 2017, 44(2): 209-215. |
[9] | CHEN Yong and XU Chao. Symbolic Execution and Human-Machine Interaction Based Auto Vectorization Method [J]. Computer Science, 2016, 43(Z6): 461-466. |
[10] | LIANG Jia-biao, LI Zhao-peng, ZHU Ling and SHEN Xian-fei. Symbolic Execution Engine with Shape Analysis [J]. Computer Science, 2016, 43(3): 193-198. |
[11] | LI Hua, XING Yi and ZHANG Yu-rong. Modeling OpenStack Single Plane Network Based on Token Selection [J]. Computer Science, 2016, 43(11): 66-70. |
[12] | WANG Zhi-wen,HUANG Xiao-long,WANG Hai-jun,LIU Ting and YU Le-chen. Program Slicing-guied Test Case Generation System [J]. Computer Science, 2014, 41(9): 71-74. |
[13] | ZHANG Ya-jun,LI Zhou-jun,LIAO Xiang-ke,JIANG Rui-cheng and LI Hai-feng. Survey of Automated Whitebox Fuzz Testing [J]. Computer Science, 2014, 41(2): 7-10. |
[14] | CHEN Shu,YE Jun-min and ZHANG Fan. Automatic Program Testing with Dynamic Symbolic Execution and Model Learning [J]. Computer Science, 2013, 40(8): 161-164. |
[15] | CHEN Xiang,GU Qing and CHEN Dao-xu. Research Advances in Test Suite Augmentation for Regression Testing [J]. Computer Science, 2013, 40(6): 8-15. |
|