Welcome to FuncTion’s web interface!

FuncTion is a research prototype static analyzer, which is able to infer piecewise-defined ranking functions for programs written in a C-like language. To avoid flooding the servers, the analyzer rejects programs that are too large or feature too many variables, and timeouts after a few seconds.

The analyzer is written in OCaml and is implemented on top of the APRON library.

Grateful acknowledgements go to Antoine Miné for making the source code of his prototype available for download, and for allowing me to reuse many parts of it.

Type your program:

or choose a predefined example: Choose File     ---- conflict-driven conditional termination ----     example1a.c example1b.c example1c.c example1d.c example1e.c example2.c example2a.c example2b.c example2c.c example2d.c example2e.c     ---- terminating programs ----     vmcai2004a.c example1.c tacas2013a.c tacas2013b.c tacas2013c.c tacas2013d.c example8.c cacm2009a.c cav2006.c bubblesort.c sas2010.c sorting4.c     ---- ordinal-valued ranking functions ----     cacm2009b.c example10.c     ---- conditional termination ----     vmcai2004b.c example5.c example7.c tap2008a.c tap2008b.c tap2008d.c zune.c     ---- guarantee properties ----     simple.c countdown.c sink.c pingpong.c     ---- recurrence properties ----     simple.c countdown.c sink.c peterson.c

and choose an entry point:

Termination Guarantee Recurrence

Type your property:

Conflict-Driven Conditional Termination:

1. •Number of Decisions:
   

Forward options:

1. •Widening delay:
   

Backward options:

1. •Partition Abstract Domain: Intervals Octagons Polyhedra Intervals
   

2. •Function Abstract Domain: Affine Functions
   Ordinal-Valued Functions
   

3. •Maximum Degree:
   

4. •Widening delay:
   

Last updated on 9th February 2015