formal methods


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.