Write a Blog >>
ESEC/FSE 2022
Mon 14 - Fri 18 November 2022 Singapore
Tue 15 Nov 2022 15:00 - 15:15 at SRC LT 50 - Formal Methods Chair(s): Dirk Beyer

We introduce a novel approach to the automated termination analysis of
computer programs: we use neural networks to represent ranking functions.
Ranking functions map program states to values that are bounded from below
and decrease as a program runs; the existence of a ranking function proves
that the program terminates. We train a neural network from sampled
execution traces of a program so that the network's output decreases along
the traces; then, we use symbolic reasoning to formally verify that it
generalises to all possible executions. Upon the affirmative answer we obtain a
formal certificate of termination for the program, which we call a neural
ranking function. We demonstrate that, thanks to the ability of neural
networks to represent nonlinear functions, our method succeeds over programs
that are beyond the reach of state-of-the-art tools. This includes programs
that use disjunctions in their loop conditions and programs that include
nonlinear expressions.

Tue 15 Nov

Displayed time zone: Beijing, Chongqing, Hong Kong, Urumqi change

14:00 - 15:30
Formal MethodsResearch Papers / Demonstrations at SRC LT 50
Chair(s): Dirk Beyer LMU Munich
14:00
15m
Talk
Input Invariants
Research Papers
Dominic Steinhöfel CISPA Helmholtz Center for Information Security, Andreas Zeller CISPA Helmholtz Center for Information Security
DOI Pre-print
14:15
15m
Talk
Modus: A Datalog Dialect for Building Container Images
Research Papers
Chris Tomy University College London, Tingmao Wang University College London, Earl T. Barr University College London, Sergey Mechtaev University College London
DOI
14:30
15m
Talk
Multi-Phase Invariant Synthesis
Research Papers
Daniel Riley Florida State University, Grigory Fedyukovich Florida State University
DOI
14:45
15m
Talk
Parasol: Efficient Parallel Synthesis of Large Model Spaces
Research Papers
Clay Stevens University of Nebraska-Lincoln, Hamid Bagheri University of Nebraska-Lincoln
DOI
15:00
15m
Talk
Neural Termination Analysis
Research Papers
Mirco Giacobbe University of Birmingham, Daniel Kroening University of Oxford, Julian Parsert University of Oxford
DOI
15:15
7m
Talk
SolSEE: A Source-Level Symbolic Execution Engine for Solidity
Demonstrations
Shang-Wei Lin Nanyang Technological University, Palina Tolmach Nanyang Technological University, Singapore, Institute of High Performance Computing, Agency for Science, Technology and Research (A*STAR), Singapore, Ye Liu , Yi Li Nanyang Technological University
Pre-print
15:23
7m
Talk
MpBP: Verifying Robustness of Neural Networks with Multi-Path Bound Propagation
Demonstrations
Ye Zheng Shenzhen University, Shenzhen, China, Jiaxiang Liu Shenzhen University, Xiaomu Shi Shenzhen University