Analysis of Agent-Based Systems Using Decision Procedures
NAVAL RESEARCH LAB WASHINGTON DC CENTER FOR HIGH ASSURANCE COMPUTING SYSTEMS (CHACS)
Pagination or Media Count:
In recent years, model checking has emerged as a remarkably effective technique for the automated analysis of descriptions of hardware systems and communication protocols. To analyze software system descriptions, however, a direct application of model checking rarely succeeds, since these descriptions often have huge often infinite state spaces that are not amenable to the finite-state methods of model checking. More important, the computation of a fixpoint the hallmark of the model-checking approach is not always needed in practice for the verification of an interesting class of properties, viz, properties that are invariantly true in all reachable states or transitions of the system. To establish a property as an invariant, an induction proof, suitably augmented with automatically generated lemmas, often suffices.
- Computer Programming and Software