Symbolic execution calls for specialized address translation. Unlike a pointer on a traditional machine model, which corresponds to a single address, a symbolic pointer may represent multiple feasible addresses. A symbolic pointer dereference manipulates symbolic state, potentially submitting many theorem prover requests in the process. Hence, design and management of symbolic accesses critically affects symbolic executor performance, complexity, and completeness.

Pintos is an instructional operating system, complete with documentation and ready-made, modular projects that introduce students to the principles of multi-programming, scheduling, virtual memory, and filesystems. By allowing students to run their work product on actual hardware, while simultaneously benefiting from debugging and dynamic analysis tools provided in simulated and emulated environments, Pintos increases student engagement. Unlike tailored versions of commercial or open source OS such as Linux, Pintos is designed from the ground up from an educational perspective. It has been used by multiple institutions for a number of years and is available for wider use.