Model checking: Neural Termination Analysis

Add to your list(s) Download to your calendar using vCal

• Daniel Kroening (Amazon Web Services)
• Friday 22 July 2022, 14:15-15:00
• Seminar Room 2, Newton Institute.

If you have a question about this talk, please contact nobody.

VSO2 - Verified software

We introduce a novel approach to the automated termination analysis of computer programs: we train neural networks to behave as ranking functions. Ranking functions map program states to values that are bounded from below and decrease as the program runs.  The existence of a ranking function proves that the program terminates.  We learn ranking functions from execution traces by training a neural network so that its output decreases along the sampled executions; then, we use symbolic reasoning to formally verify that it generalises to all possible executions.  We demonstrate that, thanks to the ability of neural networks to represent highly complex functions, our method succeeds over programs that are beyond the reach of state-of-the-art tools.  This includes programs that use loop guards with disjunctions and programs that exhibit nonlinear behaviour. 

This talk is part of the Isaac Newton Institute Seminar Series series.

This talk is included in these lists:

• All CMS events
• Featured lists
• INI info aggregator
• Isaac Newton Institute Seminar Series
• School of Physical Sciences
• Seminar Room 2, Newton Institute
• bld31

Note that ex-directory lists are not shown.