Automatic fully semantic slicing procedure for LLVM programs

Developed and maintained at the Institute of Theoretical Informatics at KIT.

or enter a program:

Click for an explanation of the methods.
Click for an explanation of the options.
Activate heap
Replace undefined values by zero
Syntactic post processing

Your program has been sent to the server.
Please be a little patient for the answer …

SemSlice automatically slices C functions with taking program semantics into account. For details take a look at the Usage page.

SemSlice has been written and is maintained by Stephan Gocht, Daniel Lentzsch, Thorsten Bormer, Mihai Hera and Mattias Ulbrich. The tool is based on our regression verification engine llreve.