top-down analysis of each node

[hbourbouh]

Hi Daniel,

I know there is a possibility to do a Bottom-up analysis of each node (using --modular true).
What about a top-down analysis in a compositional setting. I believe it may produce results for top contracts in the limited timeout given by the user for large complex models. While most of the time in bottom-up analysis, I noticed kind2 gives up quickly on the bottom contracts as they are hard to prove and it stops the analysis.

top-down analysis may require computing the dependency graph of nodes and do a BFS of contracts.

--timeout_analysis is useful to limit the timeout per analysis, but I would like to experiment kind2 in a top-down analysis.

In the mean time, what about an option to give a list of nodes to analyze by order in the same execution? Currently I use --lus_main for each node on several executions of kind2.

Thanks

[daniel-larraz]

Hi Hamza,

The choice of a bottom-up approach in modular analysis was not an arbitrary one. A bottom-up analysis has several advantages over a top-down analysis or other analyses that use an arbitrary order. For instance, it allows Kind 2 to easily reuse in parent nodes previously discovered invariants in subnodes, or avoid re-checking proved properties after the refinement of a subnode whose contract was proved valid.

If your main concern is that Kind 2 doesn't start the analysis of top-level nodes given some global timeout because it spends a lot of time in hard-to-verify leave nodes, and you don't want to use a timeout per analysis, then I recommend you to create a version of the model with an abstraction of the hard-to-verify nodes by removing their body, keeping only their contract, and marking them as imported. In this way, Kind 2 will not spend time analyzing these nodes, but it will use their contracts in the analysis of the top-level nodes, and you will enjoy the rest of the advantages of a bottom-up approach.

Daniel