Proof Tactics for Theorem Proving Graph Grammars through Rodin


  • Luiz Carlos Lemor Jr.
  • Simone André da Costa Cavalheiro
  • Luciana Foss



Graph grammar is a formal language suitable for the specification of distributed and concurrent systems. Theorem proving is a technique that allows the verification of systems with huge (and infinite) state space. One of the disadvantages of theorem proving graph grammars (and theorem proving in general) is the specific mathematical knowledge required from the user for concluding the proofs. Previous works have proposed proof strategies to help the developer in the verification process when adopting such approach, firstly establishing proof tactics for some properties and after proposing a visual representation for them. This paper extends the set of proposed tactics, with the aim of expanding the available strategies and encouraging the use of such a technique.


Download data is not yet available.




How to Cite

Lemor Jr., L. C., Cavalheiro, S. A. da C., & Foss, L. (2015). Proof Tactics for Theorem Proving Graph Grammars through Rodin. Revista De Informática Teórica E Aplicada, 22(1), 190–241.



Melhores Artigos WEIT-2013

Most read articles by the same author(s)