University of Cambridge > Talks.cam > Isaac Newton Institute Seminar Series > Model checking: Neural Termination Analysis

Model checking: Neural Termination Analysis

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

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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2022 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity