For the most recent entries see the Petri Nets Newsletter.

Verifying Intuition - ILF Checks DAWN Proofs.

Baar, Thomas; Kindler, Ekkart; Völzer, Hagen

In: Donatelli, Susanna; Kleijn, Jetty: Lecture Notes in Computer Science, Vol. 1630: Application and Theory of Petri Nets 1999, 20th International Conference, ICATPN'99, Williamsburg, Virginia, USA, pages 404-423. Springer-Verlag, June 1999.

Abstract: The DAWN approach allows to model and verify distributed algorithms in an intuitive way. At a first glance, a DAWN proof may appear to be informal. In this paper, we argue that DAWN proofs are formal and can be checked for correctness fully automatically by automated theorem provers. The basic technique are proof rules which generate proof obligations. For the definition of the proof rules we adopt assertions and we introduce conflict formulas for algebraic Petri nets. Experiments show that the generated proof obligations can be automatically checked by theorem provers.


Do you need a refined search? Try our search engine which allows complex field-based queries.

Back to the Petri Nets Bibliography