Two-stage agent program verification
Louise A. Dennis, Michael Fisher, Matt Webster · Journal of Logic and Computation · 2015
We describe an extension to the AJPF agent program model-checker so that it may be used to generate models for input into other, non-agent, model-checkers. We motivate this adaptation, arguing that it potentially improves the efficiency of the model-checking process and provides access to richer property specification languages. We illustrate the approach by describing the export of AJPF program models to both the SPIN and P rism model-checkers. We also investigate, experimentally, the effect the process has on the overall efficiency of model-checking.