ASE 2020 (series) / New Ideas and Emerging Results (NIER) track /
Proving Termination by k-Induction
We propose a novel approach to proving the termination of imperative programs by k-induction. By our approach, the termination proving problem can be formalized as a k-inductive invariant synthesis task. On the one hand, k-induction uses weaker invariants than that required by the standard inductive approach. On the other hand, the base case of k-induction, which unrolls the program, can provide stronger pre-condition for invariant synthesis. As a result, the termination arguments of our approach can be synthesized more efficiently than the standard method. We implement a prototype of our k-inductive approach. The experimental results show the significant effectiveness and efficiency of our approach.
Tue 22 SepDisplayed time zone: (UTC) Coordinated Universal Time change
Tue 22 Sep
Displayed time zone: (UTC) Coordinated Universal Time change
02:20 - 03:20 | Formal Methods (1)NIER track / Research Papers at Koala Chair(s): Nazareno Aguirre Dept. of Computer Science FCEFQyN, University of Rio Cuarto | ||
02:20 20mTalk | Accelerating All-SAT Computation with Short Blocking Clauses Research Papers Yueling Zhang Singapore Management University, Geguang Pu East China Normal University, Jun Sun Singapore Management University | ||
02:40 20mTalk | A Predictive Analysis for Detecting Deadlock in MPI Programs Research Papers Yu Huang Southwestern University of Finance and Economics, Benjamin Ogles Brigham Young University, Eric Mercer Brigham Young University Pre-print | ||
03:00 10mTalk | Proving Termination by k-Induction NIER track |