Proving Non-termination Using Max-SMT
Abstract elided by the publisher.
Related papers
- Lower-Bound Synthesis Using Loop Specialization and Max-SMT CAV 2021
- Proving non-termination by program reversal PLDI 2021
- Synthesis of Super-Optimized Smart Contracts Using Max-SMT CAV 2020
- Recursive proofs for inductive tree data-structures POPL 2012
- Max-Policy Iteration, Revisited ESOP 2026
- A Max-SMT Superoptimizer for EVM handling Memory and Storage TACAS 2022
- Synthesis for Polynomial Lasso Programs VMCAI 2014
- TEA: Automatically Proving Termination of Programs in a Non-strict Higher-Order Functional Language SAS 1997