mlsanityData to 7 Oct 2026

Neural Termination Analysis

arXiv 2102.03824 ↗First posted 7 Feb 2021cs.LG cs.LO cs.PLcited by 16

Not on the map. Why?

Abstract (arXiv)

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.

Key facts. Cited by 16 papers in the map (data through 7 Oct 2026). Builds on 32 of its 123 references that are in the map. First posted on arXiv 7 Feb 2021.

Builds on

32 of 123 references.

References · 32

  1. 2019PyTorch: An Imperative Style, High-Performance Deep Learning Librarycited by 20,160
  2. 2013Intriguing properties of neural networkscited by 5,114
  3. 2017Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networkscited by 739
  4. 2018Efficient Neural Network Robustness Certification with General Activation Functionscited by 439
  5. 2016Safety Verification of Deep Neural Networkscited by 262
  6. 2017Formal Verification of Piece-Wise Linear Feed-Forward Neural Networkscited by 241
  7. 2019Algorithms for Verifying Deep Neural Networkscited by 221
  8. 2020Neural Lyapunov Controlcited by 142
  9. 2020NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systemscited by 128
  10. 2016Neuro-Symbolic Program Synthesiscited by 84
  11. 2018Verisig: verifying safety properties of hybrid systems with neural network controllerscited by 83
  12. 2016DeepMath - Deep Sequence Models for Premise Selectioncited by 80
20 more
  1. 2017Verifying Properties of Binarized Deep Neural Networkscited by 77
  2. 2020Verification of Deep Convolutional Neural Networks Using ImageStarscited by 75
  3. 2021Learning Safe Multi-Agent Control with Decentralized Neural Barrier Certificatescited by 71
  4. 2019Quantitative Verification of Neural Networks And its Security Applicationscited by 56
  5. 2019Graph Representations for Higher-Order Logic and Theorem Provingcited by 55
  6. 2020Learning Certified Control using Contraction Metriccited by 48
  7. 2020An SMT-Based Approach for Verifying Binarized Neural Networkscited by 47
  8. 2020Reachable Polyhedral Marching (RPM): A Safety Verification Algorithm for Robotic Systems with Deep Neural Network Componentscited by 36
  9. 2020Scalable Verification of Quantized Neural Networks (Technical Report)cited by 28
  10. 2020Learning Lyapunov Functions for Hybrid Systemscited by 24
  11. 2019Property Invariant Embedding for Automated Reasoningcited by 22
  12. 2019CLN2INV: Learning Loop Invariants with Continuous Logic Networkscited by 20
  13. 2014Termination Analysis by Learning Terminating Programscited by 9
  14. 2021Termination Analysis Without the Tearscited by 9
  15. 2018Automated Verification of Neural Networks: Advances, Challenges and Perspectivescited by 7
  16. 2020Automated and Formal Synthesis of Neural Barrier Certificates for Dynamical Modelscited by 3
  17. 2020DynamiTe: Dynamic Termination and Non-termination Proofscited by 3
  18. 2014Ranking Templates for Linear Loopscited by 2
  19. 2019SymInfer: Inferring Program Invariants using Symbolic Statescited by 2
  20. 2015T2: Temporal Property Verificationcited by 1

Built on by

Cited by year

Citing papers per year: 2021: 3; 2022: 4; 2023: 3; 2024: 5; 2025: 1.

16 papers.

Sort:

  1. 2023Can ChatGPT support software verification?cited by 14
  2. 2023Neural Abstractionscited by 11
  3. 2024Neural Model Checkingcited by 6
  4. 2024Bisimulation Learningcited by 5
  5. 2024NeuroSynt: A Neuro-symbolic Portfolio Solver for Reactive Synthesiscited by 3
  6. 2024Application of AI to formal methods - an analysis of current trendscited by 2
  7. 2021SINGA-Easy: An Easy-to-Use Framework for MultiModal Analysiscited by 0
  8. 2021VisualTextRank: Unsupervised Graph-based Content Extraction for Automating Ad Text to Image Searchcited by 0
  9. 2021Text is NOT Enough: Integrating Visual Impressions into Open-domain Dialogue Generationcited by 0
  10. 2022Discovering Personalized Semantics for Soft Attributes in Recommender Systems using Concept Activation Vectorscited by 0
  11. 2022Reinforced MOOCs Concept Recommendation in Heterogeneous Information Networkscited by 0
  12. 2022Explanation-Guided Fairness Testing through Genetic Algorithmcited by 0
4 more
  1. 2022Using Graph Neural Networks for Program Terminationcited by 0
  2. 2023Tribe or Not? Critical Inspection of Group Differences Using TribalGramcited by 0
  3. 2024Automated Strategy Invention for Confluence of Term Rewrite Systemscited by 0
  4. 2025VeRecycle: Reclaiming Guarantees from Probabilistic Certificates for Stochastic Dynamical Systems after Changecited by 0