Advanced Automata-based Algorithms for Program Termination Checking

Result code in IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F18%3APU130704" target="_blank" >RIV/00216305:26230/18:PU130704 - isvavai.cz</a>

Result on the web

<a href="http://www.fit.vutbr.cz/research/pubs/all.php?id=11668" target="_blank" >http://www.fit.vutbr.cz/research/pubs/all.php?id=11668</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1145/3192366.3192405" target="_blank" >10.1145/3192366.3192405</a>

Result language

angličtina

Original language name

Advanced Automata-based Algorithms for Program Termination Checking

Original language description

In 2014, Heizmann et al. proposed a novel framework for program termination analysis. The analysis starts with a termination proof of a sample path. The path is generalized to a Büchi automaton (BA) whose language (by construction) represents a set of terminating paths. All these paths can be safely removed from the program. The removal of paths is done using automata difference, implemented via BA complementation and intersection. The analysis constructs in this way a set of BAs that jointly "cover" the behavior of the program, thus proving its termination. An implementation of the approach in Ultimate Automizer won the 1st place in the Termination category of SV-Comp 2017. In this paper, we exploit advanced automata-based algorithms and propose several non-trivial improvements of the framework. To alleviate the complementation computation for BAs---one of the most expensive operations in the framework---, we propose a multi-stage generalization construction. We start with generalizations producing subclasses of BAs (such as deterministic BAs) for which efficient complementation algorithms are known, and proceed to more general classes only if necessary. Particularly, we focus on the quite expressive subclass of semideterministic BAs and provide an improved complementation algorithm for this class. Our experimental evaluation shows that the proposed approach significantly improves the power of termination checking within the Ultimate Automizer framework.

Czech name

—

Czech description

—

Type

D - Article in proceedings

CEP classification

—

OECD FORD branch

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Project

Result was created during the realization of more than one project. More information in the Projects tab.

Continuities

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Publication year

2018

Confidentiality

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Article name in the collection

Proceedings of PLDI'18

ISBN

978-1-4503-5698-5

ISSN

—

e-ISSN

—

Number of pages

16

Pages from-to

135-150

Publisher name

Association for Computing Machinery

Place of publication

Philadelphia

Event location

Philadelphia

Event date

Jun 18, 2018

Type of event by nationality

WRD - Celosvětová akce

UT code for WoS article

000452469600010