TOPICS is a tool dedicated to the verification of Clike programs. The particularity of this tool lies in the fact that it can deal with programs manipulating dynamic data structures. In this first version, TOPICS can treat programs working over singly linked lists, but this feature will be extended to more complex data structures. The main feature of TOPICS is the translation of Clike programs into a bisimilar counter system, where counter systems correspond to finite automata extended with (unbounded) integer variables. This translation allows to use tools which verifies counter systems in order to check that the given program do not realize errors as memory violation, memory leakage or out of bound error.
The translation implemented in TOPICS corresponds to the one presented in the article From Pointer Systems to Counter Systems Using Shape Analysis. The programs given in input of TOPICS are written in a syntaxic fragment of the C programming language. These programs can manipulate integer variables, singly linked lists and arrays of integers and of lists. Whereas there is no restriction on the size of the manipulating lists, the arrays have to be of finite size. The user has also the possibility to give an initial configuration to TOPICS, in which he will characterize the initial state of the memory he wants the programs to begin with.
The following table gives some files produced by TOPICS for different programs.
In the first two colums, there are the program given in input and the description of the initial configuration. The third column contains a representation of the control flow graph produced by TOPICS. The fourth column contains a description of the counter system produced by TOPICS. The two last columns contain the files produced for the tools FAST and ASPIC.
Program  Initial configuration  Control Flow Graph  Counter automaton  FAST file  ASPIC files 

create.c  create_automaton.pdf  createCA.pdf  create.fst  create_MemL_aspic.fst  
insert.c  conf.init  insert_automaton.pdf  insertCA.pdf  insert.fst  insert_MemL_aspic.fst 
reverse.c  conf.init  reverse_automaton.pdf  reverseCA.pdf  reverse.fst  reverse_MemL_aspic.fst 
deleteAll.c  conf.init  deleteAll_automaton.pdf  deleteAllCA.pdf  deleteAll.fst  deleteAll_MemL_aspic.fst 
merge.c  conf.init  merge_automaton.pdf  The counter automaton is too big  merge.fst 
merge_MemL_aspic.fst merge_SegF_aspic.fst 
mainReverse.c  main_automaton.pdf  mainCA.pdf  main.fst 
main_MemL_aspic.fst main_Undef_aspic.fst 

doubleFree.c  conf.init  doubleFree_automaton.pdf  doubleFreeCA.pdf  doubleFree.fst 
doubleFree_SegF_aspic.fst doubleFree_MemL_aspic.fst 
doubleFree.c 
conf.init with list of even length 
doubleFree_automaton.pdf  doubleFreeCA.pdf  doubleFree.fst 
doubleFree_SegF_aspic.fst doubleFree_MemL_aspic.fst 