Proving Non-Termination via Loop Acceleration
| Autor: | Florian Frohn, Jürgen Giesl |
|---|---|
| Rok vydání: | 2019 |
| Předmět: |
FOS: Computer and information sciences
Computer Science - Logic in Computer Science Logic in computer science Fully automated Control theory Computer science 0202 electrical engineering electronic engineering information engineering Inference 020201 artificial intelligence & image processing 02 engineering and technology Invariant (computer science) 020202 computer hardware & architecture Logic in Computer Science (cs.LO) |
| Zdroj: | FMCAD |
| DOI: | 10.48550/arxiv.1905.11187 |
| Popis: | We present the first approach to prove non-termination of integer programs that is based on loop acceleration. If our technique cannot show non-termination of a loop, it tries to accelerate it instead in order to find paths to other non-terminating loops automatically. The prerequisites for our novel loop acceleration technique generalize a simple yet effective non-termination criterion. Thus, we can use the same program transformations to facilitate both non-termination proving and loop acceleration. In particular, we present a novel invariant inference technique that is tailored to our approach. An extensive evaluation of our fully automated tool LoAT shows that it is competitive with the state of the art. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|