-
Notifications
You must be signed in to change notification settings - Fork 79
Program Analysis
Julian Cohen edited this page Dec 3, 2013
·
25 revisions
Program analysis is the process of automatically analyzing the behavior of computer programs.
- Introduction to Abstract Interpretation
- All You Ever Wanted to Know About Dynamic Taint Analysis and Forward Symbolic Execution (but might have been afraid to ask)
- Security Applications of Dynamic Binary Translation
- Symbolic Execution
- Symbolic Execution
- Program Analysis, Understanding, and Synthesis with Symbolic Execution
- Symbolic Execution and Program Testing
- Using LLVM For Program Transformation
- Static Program Analysis from RWTH Aachen University
- MIT SAT/SMT Summer School 2011
- University of Maryland CMSC 838G
- BAP: A Binary Analysis Platform
- KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs
- Automated Whitebox Fuzz Testing
- SAGE: Whitebox Fuzzing for Security Testing
- EXE: A System for Automatically Generating Inputs of Death Using Symbolic Execution
- Practical Automated Bug Finding
- Augmenting Vulnerability Analysis of Binary Code
- Symbolic Execution Algorithms for Test Generation
- A survey of new trends in symbolic execution for software testing and analysis
- Automatic Generation of Control Flow Hijacking Exploits for Software Vulnerabilities
- AEG: Automatic Exploit Generation
- Q: Exploit Hardening Made Easy
- Symbolic Execution for Software Testing in Practice – Preliminary Assessment
- Automated Synthesis of Symbolic Instruction Encodings from I/O Samples
- Unleashing Mayhem on Binary Code (video)
- The Astrée Static Analyzer
- BAP: The Next-Generation Binary Analysis Platform
- BitBlaze: Binary Analysis for Computer Security
- The KLEE Symbolic Virtual Machine
- The Insight Project
- Jakstab
- Cloud9 - Automated Software Testing at Scale (Includes KLEE Improvements)
- FindBugs - Find Bugs in Java Programs
- PMD
- Polyglot: A compiler front end framework for building Java language extensions
- ANTLR (ANother Tool for Language Recognition)
- libdft
- BLAST (Berkeley Lazy Abstraction Software verification Tool)
- libemu – x86 Shellcode Emulation
- ForAllSecure (Uses Mayhem)
- BUG CHECKER .NET (Uses klee-mc)
- BugsDuJour.com (Uses klee-mc)
- FuzzBALL: Vine-based Binary Symbolic Execution
- tree-cbass: Taint-enabled Reverse Engineering Environment on top of a Cross-platform Binary Symbolic execution System
- VCC: A Verifier for Concurrent C
- Frama-C
- Coq Proof Assistant
- Quark: A Web Browser with a Formally Verified Kernel
- http://moflow.org/#%5B%5BReference%20Library%5D%5D
- http://en.wikipedia.org/wiki/Abstract_interpretation
- http://en.wikipedia.org/wiki/Interpreter_(computing)
- http://en.wikipedia.org/wiki/Symbolic_execution
- http://en.wikipedia.org/wiki/Model_checking
- http://en.wikipedia.org/wiki/Compiler
- http://www.amazon.com/dp/0321486811/
- http://en.wikipedia.org/wiki/Source-to-source_compiler
- http://en.wikipedia.org/wiki/Intermediate_language
- https://gist.github.com/HockeyInJune/be41442c75b31f2315d2