[FPBench] Soonho Kong on Thursday

[Pavel Panchekha]

Hi all! This Thursday is our monthly Community Meeting, featuring Soonho Kong, a Senior Applied Scientist at Amazon Web Services who develops and utilizes automated reasoning tools for real-world applications. He’ll be talking about Automated Reasoning over the Reals.

In cyber-physical systems such as autonomous driving systems and robotics components, ordinary differential equations and nonlinear functions such as the exponential function and the trigonometric functions appear almost universally. To adopt automated reasoning techniques in these domains, it is necessary to develop a tool that can handle logical encodings with those functions. 

 

In this talk, I will present the design and implementation of a delta-decision procedure, dReal. First, we will discuss the theory of delta-decidability briefly. Then I will explain 1) how the tool handles nonlinear functions and ordinary differential equations, 2) how it can solve optimization and synthesis problems (∃∀-formulas), and 3) how the tool utilizes multiple cores to speed up the solving process in parallel. I will show that the tool helps tackle instances from real-world applications including bounded model-checking for cyber-physical systems, nonlinear global optimization, and Lyapunov-stability analysis in robotics.

Looking forward to seeing you all at the talk! As always, the meetings are 9am Pacific on Zoom at https://washington.zoom.us/j/92831331326.

—Pavel Panchekha