Proof Tactics for Theorem Proving Graph Grammars through Rodin

Authors

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

DOI:

https://doi.org/10.22456/2175-2745.50383

Abstract

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.

Downloads

Download data is not yet available.

Downloads

Published

2015-05-18

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. https://doi.org/10.22456/2175-2745.50383

Issue

Section

Melhores Artigos WEIT-2013

Most read articles by the same author(s)