Lehrstuhl für Softwaretechnik (Prof. Zeller)
Universität des Saarlandes – Informatik
Informatik Campus des Saarlandes
Campus E9 1 (CISPA)
E-mail: zeller @ cs.uni-saarland.de
Telefon: +49 681 302-70970
Cebit 2010We have released a web service that allows anyone to check his/her own code against the wisdom of 200 million lines of linux code. Check your code at checkmycode.org.
A caller must satisfy the callee's precondition—that is, reach a state in which the callee may be called. Preconditions describe the state that needs to be reached, but not how to reach it.
Our tool, Tikanga (meaning "correct procedure" in Mãori), combines static analysis with model checking to mine Computation Tree Logic (CTL) formulas that describe the operations a parameter goes through. We call these temporal specifications operational preconditions, and Tikanga can both mine them as well as check the program for their violations.
How Tikanga works
The process, by which Tikanga mines operational preconditions and finds their violations consists of four steps:
For more details on the whole process, consult our publication.
We have applied Tikanga to six open-source projects and found that it was able to find problems with all of them. Its effectiveness varied from 16% to 80%, depending on the project. In particular, Tikanga managed to find in total 14 defects in the projects we have analyzed. For more details on the results, consult our publication.
Below you can find links to people working on mining temporal specifications. Please contact us for questions, rants, and raves.<email@example.com> · http://www.st.cs.uni-saarland.de/models/tikanga/?lang=en · Stand: 2018-04-05 13:41