As a formal method, static program analysis is highly appealing: today's tools can reason about useful properties (e.g., freedom from memory safety violations) at a modest of precision even for large programs. However, this statement is true only for source programs; (arbitrary) machine code is much harder to analyze precisely. To deal with machine (aka binary) code, we have been developing a tool called Affix (Figure 1).
Noddle is building a code synthesis technology called ``pyx''. Pyx is a generic tool that can be specialized to different domains. For a given domain, pyx enables developers to write high-level applications in Python and generate specialized code to run on a range of platforms. Code is generated using an using an infrastructure that combines source-to-source program transformation, inference and automated search to explore the design space of algorithms and representations.
