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

[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