1. An apparatus comprising processing circuitry configured to execute instructions for: receiving a program and employing a disassembler to disassemble the program; generating a function call tree for the program based on disassembly of the program; receiving an indication of a post condition for which analysis of the program is desired; transforming program statements into logical equations; simplifying the logical equations; propagating post conditions backwards via Dijkstra's weakest preconditions variant; analyzing aliases and processing loops to generate a precondition; and using an automated solver to determine whether the precondition is realizable and, if so, providing program inputs required to realize the precondition.