Write a Blog >>
ASE 2020
Mon 21 - Fri 25 September 2020 Melbourne, Australia
Tue 22 Sep 2020 03:00 - 03:10 at Koala - Formal Methods (1) Chair(s): Nazareno Aguirre

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 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
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
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
Proving Termination by k-Induction
NIER track
Jianhui Chen Tsinghua University, Fei He Tsinghua University, China