Tutorial or any guide on how to use IC3 and its working

[fahad-ibrar]

Hi,
I want to use IC3 for ICC in Android. I have gone through the Epicc research paper and successfully setup IC3 on my machine. After running IC3 on an app I looked at the results and data stored in the database but I was not able to figure out that how to interpret these results. Can you please tell me if there is available any tutorial or guide on how to use IC3 and interpret its result? It would be very helpful for me to understand IC3 more efficiently

Regards,
Fahad Ibrar

[docteau]

The site hosting the IC3 documentation is temporarily down. I'll look into putting some of the relevant content here. In the meantime for your question about interpreting the results, in order to make it easier I would advise you to first output to a protocol buffer, which would give you a more easily understandable view of the app as you experiment.

The relevant part of the site that tells you how to use protocol buffers is given below:

It is also possible to have IC3 output the results of its analysis to protocol buffers. This allows you to examine results in an easier way than through the database. More importantly, you can easily load IC3 results using code written in Java, Python or C++. In order to output to a protocol buffer, the -protobuf option followed by the path to an output directory can be used. In order to output to a binary protocol buffer (which is slightly faster and takes less space), use the -binary option. The -protobuf option is not compatible with the -db option.

Finally, it is possible to have IC3 compute which components a message-sending program location belongs. This is done by specifying the -computecomponents flag on the command line.

Please let me know if you have questions about this output. The database output is similar in its content (but harder to interpret for a given application).

Regards,
Damien