Proving Non-Termination by Acceleration Driven Clause Learning

Title:Proving Non-Termination by Acceleration Driven Clause Learning

Authors:Florian Frohn and Jürgen Giesl

Conference:CADE-29

Tags:Loop Acceleration, Non-Termination and Transition Systems

Abstract:

We recently proposed Acceleration Driven Clause Learning (ADCL), a novel calculus to analyze satisfiability of Constrained Horn Clauses (CHCs). Here, we adapt ADCL to transition systems and introduce ADCL-NT, a variant for disproving termination. We implemented ADCL-NT in our tool LoAT and evaluate it against the state of the art.

Proving Non-Termination by Acceleration Driven Clause Learning

1

2

3

4

5

6

7

8

9

10

11

12

13

14

15

16

17

18

19

20

21

22

23

24

25

26

27

28

29

30

31

32

33

34

35

36

37

38

39

40

41

42

43

44

45

46

47

48

1of48

1

2

3

4