Related Work

CFG Recovery by Abstract Interpretation

• Johannes Kinder and Dmitry Kravchenko. ​Alternating control flow reconstruction. In Proceeding of 13th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI’2012), volume 7148 of Lecture Notes in Computer Science, pages 267–282, Philadelphia, PA, 2012. Springer.
• Johannes Kinder and Helmut Veith. ​Jakstab : A static analysis platform for binaries. In Proceedings of 20th International Conference on Computer Aided Verification (CAV’2008), volume 5123 of Lecture Notes in Computer Science, pages 423–427, Princeton, NJ, USA, 2008. Springer.
• Johannes Kinder and Helmut Veith. ​Precise static-analysis of untrusted driver binaries. In Proceedings of 10th International Conference on Formal Methods in Computer Aided Design (FMCAD’2010), pages 43–50, Lugano, Switzerland, 2010. IEEE Computer Society.
• Johannes Kinder, Florian Zuleger, and Helmut Veith. ​An abstract interpretation-based framework for control flow reconstruction from binaries. In Proceedings of 10th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI’2009), volume 5403 of Lecture Notes in Computer Science, pages 214–228, Savannah, GA, USA, 2009. Springer.

CFG Recovery by Directed Automated Search

• Sébastien Bardin and Philippe Herrmann. ​OSMOSE : automatic structural testing of executables. Software Testing, Verification and Reliability, 21(1) :29–54, 2011.
• Sébastien Bardin and Philippe Herrmann. ​Structural testing of executables (​Slides). In Proceedings of First International Conference on Software Testing, Verification, and Validation (ICST’2008), pages 22–31, Lillehammer, Norway, 2008. IEEE Computer Society.
• Sébastien Bardin, Philippe Herrmann, and Florian Perroud. ​An alternative to SAT-based approaches for bit-vectors. In Proceedings of 16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’2010), volume 6015 of Lecture Notes in Computer Science, pages 84–98, Paphos, Cyprus, 2010. Springer.
• Sébastien Bardin, Philippe Herrmann, and Franck Védrine. ​Refinement-based CFG reconstruction from unstructured programs. In Proceedings of 12th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI’2011), volume 6538 of Lecture Notes in Computer Science, pages 54–69, Austin, TX, USA, 2011. Springer.
• Patrice Godefroid, Nils Klarlund, and Koushik Sen. ​DART : directed automated random testing. In Proceedings of the ACM SIGPLAN 2005 Conference on Programming Language Design and Implementation (PLDI’2005), pages 213–223, Chicago, IL, USA, 2005. ACM.
• Patrice Godefroid and Daniel Luchaup. ​Automatic partial loop summarization in dynamic test generation. In Proceedings of the 20th International Symposium on Software Testing and Analysis, (ISSTA’2011), pages 23–33, Toronto, ON, Canada, 2011. ACM.
• Patrice Godefroid, Michael Y. Levin, and David A. Molnar. ​Automated whitebox fuzz testing. In Proceedings of the 15th Network and Distributed System Security Symposium (NDSS’2008), San Diego, California, USA, 2008. The Internet Society.
• Patrice Godefroid, Shuvendu K. Lahiri, and Cindy Rubio-González. ​Statically validating must summaries for incremental compositional dynamic test generation. In Proceedings of the 18th International Static Analysis Symposium (SAS’2011), volume 6887 of Lecture Notes in Computer Science, pages 112–128, Venice, Italy, 2011. Springer.

Shape Analysis and TVLA

• Bertrand Jeannet, Alexey Loginov, Thomas W. Reps, and Mooly Sagiv. ​A relational approach to interprocedural shape analysis. Journal of ACM Transactions on Programming Languages and Systems (TOPLAS), 32(2), 2010.
• Shay Litvak, Nurit Dor, Ratislav Bodik, Noam Rinetzky, and Mooly Sagiv. ​Field-sensitive program dependence analysis. In Proceedings of ACM SIGSOFT 18th International Symposium on the Foundations of Software Engineering (FSE’2010), pages 287–296, Santa Fe, NM, USA, 2010. ACM.
• Noam Rinetzky, Mooly Sagiv, and Eran Yahav. ​Interprocedural shape analysis for cutpoint-free programs. In Proceedings of the 12th International Static Analysis Symposium (SAS’2005), volume 3672 of Lecture Notes in Computer Science, pages 284–302, London, UK, 2005. Springer.
• Mooly Sagiv, Thomas Reps, and Reinhard Wilhelm. ​Parametric shape analysis via 3-valued logic. Journal of ACM Transactions on Programming Languages and Systems (TOPLAS), 24(3) :217–298, 2002.
• Greta Yorsh, Alexander M. Rabinovich, Mooly Sagiv, Antoine Meyer, and Ahmed Bouajjani. ​A logic of reachable patterns in linked data-structures. Journal of Logic and Algebraic Programming, 73(1–2) :111–142, 2007.
• Greta Yorsh, Eran Yahav, and Satish Chandra. ​Generating precise and concise procedure summaries. In Proceedings of the 35th ACM Symposium on Principles of Programming Languages (POPL 2008), pages 221–234, San Francisco, CA, USA, 2008. ACM.

Other Related Papers (To be sorted)

• David Brumley, Ivan Jager, Thanassis Avgerinos, Edward J. Schwartz. ​BAP: A Binary Analysis Platform. In Proceedings of the 23rd International Conference on Computer Aided Verification (CAV'11), pages 463-469, Snowbird, UT, USA, 2011. Springer.
• Gogul Balakrishnan. ​WYSINWYX : What You See Is Not What You Execute. PhD thesis, University of Wisconsin-Madison, Madison, WI, USA, 2007.
• Gogul Balakrishnan and Thomas Reps. ​WYSINWYX : What You See Is Not What You eXecute. Journal of ACM Transactions on Programming Languages and Systems (TOPLAS), 32(6), 2010.
• Cristina Cifuentes and Antoine Fraboulet. ​Intraprocedural static slicing of binary executables. In Proceedings of the 5th IEEE International Conference on Software Maintenance (ICMS’1997), pages 188–197, Bari, Italy, 1997. IEEE Computer Society.
• Cristina Cifuentes and John K. Gough. ​Decompilation of binary programs. Journal of Software Practice and Experience, 25(7) :811–829, 1995.
• Cristian Cadar, Vijay Ganesh, Peter M. Pawlowski, David L. Dill, and Dawson R. Engler. ​Exe : automatically generating inputs of death. In Proceedings of the 13th ACM conference on Computer and Communications Security (CCS’2006, pages 322–335, Alexandria, VA, USA, 2006. ACM.
• Cristina Cifuentes. ​Reverse Compilation Techniques. PhD thesis, Queensland University of Technology, Department of Computer Science, Brisbane, Queensland, Australia, 1994.
• Cristina Cifuentes. ​Interprocedural data flow decompilation. Journal of Programming Languages, 4(2) :77–99, 1996.
• Cristina Cifuentes. ​Partial automation of an integrated reverse engineering environment of binary code. In Proceedings of the 3rd Working Conference on Reverse Engineering (WCRE’1996), pages 50–56, Monterey, CA, USA, 1996. IEEE Computer Society.
• Cristina Cifuentes. ​Structuring decompiled graphs. In Proceedings of the 6th International Conference on Compiler Construction (CC’1996), volume 1060 of Lecture Notes in Computer Science, pages 91–105, Linköping, Sweden, 1996. Springer.
• Cristina Cifuentes and Shane Sendall. ​Specifying the semantics of machine instructions. In Proceedings of the 6th International Workshop on Program Comprehension (IWPC ’98), pages 126–135, Ischia, Italy, 1998. IEEE Computer Society.
• Cristina Cifuentes and Doug Simon. ​Procedure abstraction recovery from binary code. In Proceedings of the Conference on Software Maintenance and Reengineering (CSMR’2000), pages 55–64, Zurich, Switzerland, 2000. IEEE Computer Society.
• Cristina Cifuentes, Doug Simon, and Antoine Fraboulet. ​Assembly to high-level language translation. In Proceedings of International Conference on Software Maintenance (ICSM’98), pages 228–237, Bethesda, Maryland, USA, 1998. IEEE Computer Society.
• Cristina Cifuentes and Mike Van Emmerik. ​Recovery of jump table case statements from binary code. Journal of Science of Computer Programming, 40(2–3) :171–188, 2001.
• Bhargav S. Gulavani, Thomas A. Henzinger, Yamini Kannan, Aditya V. Nori, and Sriram K. Rajamani. ​Synergy : a new algorithm for property checking. In Proceedings of the 14th ACM SIGSOFT International Symposium on Foundations of Software Engineering (FSE’2006), pages 117–127, Portland, Oregon, USA, 2006. ACM.
• Uday P. Khedker, Alan Mycroft, and Prashan Singh Rawat. ​Lazy pointer analysis. Computing Research Repository (CoRR), 2011.
• Lian Li, Cristina Cifuentes, and Nathan Keynes. ​Boosting the performance of flow-sensitive points-to analysis using value flow. In Proceedings of the 19th ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE”11) and the 13rd European Software Engineering Conference (ESEC’11), pages 343–353. ACM, 2011.
• Alan Mycroft. ​Type-based decompilation (or program reconstruction via type reconstruction). In Proceedings of the 8th European Symposium on Programming, ESOP’99, volume 1576 in Lecture Notes in Computer Science, pages 208–223, Amsterdam, Netherlands, 1999. Springer.