Proving non-termination

DOI10.1145/1328438.1328459zbMath1295.68158OpenAlexW1989813138MaRDI QIDQ3189834

Andrey Rybalchenko, Ru-Gang Xu, Ashutosh Gupta, Rupak Majumdar, Thomas A. Henzinger

Publication date: 12 September 2014

Published in: Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/1328438.1328459

zbMATH Keywords

testingmodel checkingprogram verificationnon-terminationrecurrent sets

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (19)

A Calculus for Modular Loop Acceleration ⋮ Decision tree learning in CEGIS-based termination analysis ⋮ Loop detection by logically constrained term rewriting ⋮ Summarization for termination: No return! ⋮ Automatic discovery of fair paths in infinite-state transition systems ⋮ Convergence: integrating termination and abort-freedom ⋮ Synthesising programs with non-trivial constants ⋮ Unnamed Item ⋮ Proving the existence of fair paths in infinite-state systems ⋮ Proving Termination Through Conditional Termination ⋮ From invariant checking to invariant inference using randomized search ⋮ Extended Nested Dual System Groups, Revisited ⋮ All-Termination(T) ⋮ A non-termination criterion for binary constraint logic programs ⋮ Proving the Correctness of the Implementation of a Control-Command Algorithm ⋮ O-Minimal Invariants for Discrete-Time Dynamical Systems ⋮ Discovering non-terminating inputs for multi-path polynomial programs ⋮ \textsc{LTL} falsification in infinite-state systems ⋮ A second-order formulation of non-termination

This page was built for publication: Proving non-termination