SemSlice

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

Checking
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 (anonymized for blind review). The tool is based on our regression verification engine llreve.