FPBench Community Meeting 2021-12-02

[Bill Zorn]

Hi all!

This Thursday (December 2nd) at 9am Pacific time we will have our next FPBench Community Meeting. The meeting is a chance to talk about numerics research, share early demos, brainstorm new ideas, and stay in touch. We'll keep tweaking the format as we learn more about what works for the community.

We have a special presentation this week from Andrew Reynolds, a research scientist at the University of Iowa and one of the lead developers of cvc5. I’ll provide his title and abstract below:

Automated Discovery of Invertibility Conditions via Syntax-Guided Synthesis

Satisfiability Modulo Theories (SMT) solvers have gained widespread popularity as reasoning engines in numerous formal methods applications, including in syntax-guided synthesis (SyGuS) applications. In this talk, we focus on an emerging class of applications for syntax-guided synthesis, namely, the use of a SyGuS solver to (partially) automate further development and improvements to the SMT solver itself. We describe several recent features in the SMT solver cvc5 that follow this paradigm. These include syntax-guided enumeration of rewrite rules, selection of test inputs, and discovery of solved forms for quantified constraints. For the latter, we describe how syntax-guided synthesis recently played a pivotal role in the development of a new algorithm for quantified bit-vector constraints based on invertibility conditions, and how this technique can be extended for similar algorithms that target quantified constraints in other theories, including the theory of floating points.

Zoom: https://washington.zoom.us/j/92831331326

Notes: FPBench Community Minutes

Slack: Invite link

Hope to see y'all there :)