PV1 ⊧ MuValchecks whether a C program will (non-)terminate

Termination analyzer?

Application domain/field

• Program termination
• Counterexample guided inductive synthesis (CEGIS)
• Ranking functions

Type of tool

(Non-)termination analyzer

Expected input

C program

Format:

.t2 file They provide a command that can be used to convert a .c file into a z.t2 file using llvm2kittel.

Expected output

Indicates whether the tool can prove that the program terminates (YES), the tool verifies non-termination(NO), timed out (TO), or could not find an answer (U).

Internals

They focus on synthesizing ranking functions. Ranking functions assign a natural number to each program state, in such a way that the values strictly decrease along transitions. If there is such a ranking function, it can be used to prove the termination of a program. Uses Z3

Comments

License: Apache-2.0