diff --git a/diagram/symbolic-execution.svg b/diagram/symbolic-execution.svg index d77092d..28271bf 100644 --- a/diagram/symbolic-execution.svg +++ b/diagram/symbolic-execution.svg @@ -1,5 +1,5 @@ - - + + @@ -49,8 +49,9 @@ - + + @@ -70,12 +71,12 @@ - - - + + + - + @@ -83,7 +84,7 @@ - + @@ -120,7 +121,7 @@ - + @@ -140,13 +141,13 @@ - + - - + + @@ -165,19 +166,18 @@ - - - - - - - - + + + + + + + - + @@ -190,12 +190,12 @@ - + - - + + - + @@ -264,7 +264,7 @@ - + @@ -276,9 +276,14 @@ - - - + + + + + + + + @@ -289,8 +294,8 @@ - - + + @@ -298,14 +303,14 @@ - + - + @@ -345,7 +350,7 @@ - + @@ -435,14 +440,14 @@ Ghent - - Duke + + Duke Syracuse, USA - - Hong Kong + + Hong Kong Nantes @@ -495,8 +500,8 @@ Maryland - - Pennsylvania + + Pennsylvania New York @@ -513,14 +518,14 @@ ETH Zürich - - Texas + + Texas - - IBM + + IBM - - New York + + New York Stellenbosch @@ -546,8 +551,8 @@ Virginia - - EPFL + + EPFL California, Los Angeles @@ -570,8 +575,8 @@ Nancy - - Intel + + Intel SRI @@ -597,25 +602,28 @@ SRI - - Oxford + + Oxford + + + Immunity JNuke 2004 Java instrumentation, virtual machine, data races, - - NDroid 2014 for Android: Java and JNI, tracks data flow random input data + + NDroid 2014 for Android: Java and JNI, tracks data flow random input data - - TaintDroid 2010 for Android, no JNI, only tracks data flow, use taint tags between real variables + + TaintDroid 2010 for Android, no JNI, only tracks data flow, use taint tags between real variables DroidScope 2012 for Android, Dalvik, Java and JNI, taint tracker for leaks - - Jinn 2010 for Java, JNI, dynamic analysis + + Jinn 2010 for Java, JNI, dynamic analysis Java PathFinder 2005 model checking, their own JVM @@ -659,8 +667,8 @@ HotSpot 1999 - - S2 E 2011 selsctive symbolic, concrete execution framework + + S2 E 2011 selsctive symbolic, concrete execution framework Sherlock 2014 static analysis and concolic for deadlocks scheduler control @@ -795,7 +803,7 @@ Pin - SANTE 2012 combination of dynamic + SANTE 2012 combination of dynamic Dowser 2013 guided fuzzer @@ -862,11 +870,11 @@ MemorySanitizer 2015 - - KLEE + + KLEE - - QEMU + + QEMU BLT bounded integer linear constraints @@ -938,7 +946,7 @@ SMART 2007 - Java PathFinder 1998 Java → Promela + Java PathFinder 1998 Java → Promela Spin @@ -967,8 +975,8 @@ Jikes RVM 1997 Research Virtual Machine, for PowerPC and IA-32 - - LLVM + + LLVM Omega @@ -1198,8 +1206,8 @@ MiniSAT - - Cloud9 2011 + + Cloud9 2011 SymDroid 2012 for Dalvik @@ -1234,14 +1242,23 @@ SELECT 1976 path constraints, test generation, assertions check - - AXGEN 2009 exploit generation + + AXGEN 2009 exploit generation + + + Yices + + + Pin - - Yices + + Debugger static symbolic execution, reverse engeneering - - Pin + + ILLITHID static symbolic execution, finding vulnerabilities + + + CVC3 @@ -1266,14 +1283,14 @@ Java - - Java + + Java Java - - Java + + Java Java @@ -1296,8 +1313,8 @@ Java bytecode - - Java + + Java C @@ -1317,8 +1334,8 @@ binary - - binary + + binary binary @@ -1437,8 +1454,8 @@ binary - - binary + + binary @@ -1534,10 +1551,12 @@ + + - - G. Candea V. Kuznetsov V. Chipounov + + G. Candea V. Kuznetsov V. Chipounov D. Brumley J. Newsome J. Franklin @@ -1638,32 +1657,29 @@ D. Brumley J. Caballero Z. Liang J. Newsome D. Song - - concoli c/DSE path exploration - - - black-box fuzzing path exploration + + concoli c/DSE path exploration - - static + + black-box fuzzing path exploration - - dynamic + + static - - SAT + + dynamic - - model checking + + SAT - - static analysis + + model checking - - Java virtual machine + + Java virtual machine - - other + + other P. Godefroid @@ -1677,8 +1693,8 @@ M. Zalewski - - Dynamic analysis + + Dynamic analysis D. Brumley, ... @@ -1695,20 +1711,20 @@ C. Cadar D. Engler - - dynamic analysis within one path + + dynamic analysis within one path - - Instrumentation + + Instrumentation - - Solving + + Solving - - SMT + + SMT - - concolic/DSE within one path + + concolic/DSE within one path P. Godefroid @@ -1746,8 +1762,8 @@ C. Barrett (N) ... - - B. Lee (T) B. Wiedermann (T), ... + + B. Lee (T) B. Wiedermann (T), ... M. Vuagnoux @@ -1833,11 +1849,11 @@ A. D. Keromytis (C) S. J. Stolfo (C) Junfeng Yang (C), ... - - Sergey Varatnov and GitHub contributors, 2017 + + Sergey Varatnov and GitHub contributors, 2017 - - github.com/enzet/symbolic-execution + + github.com/enzet/symbolic-execution Y. G. Guéhéneuc R. Douence, ... @@ -1854,11 +1870,11 @@ L. de Moura - - W. Enck (P) P. Gilbert (D), ... + + W. Enck (P) P. Gilbert (D), ... - - S. Bucur V. Ureche, ... + + S. Bucur V. Ureche, ... J. Jeon K. K. Micinski J. S. Foster @@ -1887,11 +1903,26 @@ R. S. Boyer B. Elspas K. N. Levitt - - S. Heelan + + S. Heelan + + + Symbolic execution + + + static symbolic execution + + + P. Sole S. Heelan + + + S. Heelan P. Sole R. Huizer + + + static symbolic execution - - Symbolic execution + + S. Heelan