HCSS Conference 2020


Visible to the public Jones_Mark_hcss2020-mpj.pdf


Visible to the public Affix: Micro-executing Binaries to Produce Static Analysis Models

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).


Visible to the public A New Kind of Program Logic

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.


Visible to the public HCSS 2020 Program Agenda


Visible to the public Distributed and Trustworthy Automated Reasoning

Distributed automated reasoning has become increasingly powerful and popular. This enabled solving very hard problems ranging from determining the correctness of complex systems to answering long-standing open questions in mathematics. The tools are based on a portfolio of solvers that share information or divide-and-conquer. The portfolio approach is effective on large formulas from industry, while divide-and-conquer shines on hard-combinatorial problems. Recently distributed solvers competed for the first time, with each tool running on 1600 cores in the Amazon cloud.