---
id: 3777
title: "Close Encounters with Symbolic Execution (Part 2)"
source_domain: blog.trailofbits.com
source_url: "https://blog.trailofbits.com/2014/12/04/close-encounters-with-symbolic-execution-part-2/"
published_at: "2014-12-04T13:50:36Z"
tags: ["reverse-engineering", "llvm", "darpa", "symbolic-execution", "mcsema", "klee"]
phying_url: "https://phying.com/item/3777"
lang: en
---

# Close Encounters with Symbolic Execution (Part 2)

## Summary

Part 2: how to build KLEE with LLVM 3.2 on Ubuntu 14.04 and use mcsema to symbolically execute a maze-oracle binary — translating it to bitcode and solving all paths with a symbolic-input driver.

## Intelligence Metadata

- **Sources:** blog.trailofbits.com
- **Published:** 2014-12-04T13:50:36Z
- **Original:** https://blog.trailofbits.com/2014/12/04/close-encounters-with-symbolic-execution-part-2/
- **Phying News:** https://phying.com/item/3777