Browsing by Subject "Regla de inferencia"

Now showing items 1-3 of 3

    • The Formal System of Dijkstra and Scholten 

      Rocha, Camilo (Springer.Springer, Cham., 2015)
      The logic of E.W. Dijkstra and C.S. Scholten has been shown to be useful in program correctness proofs and has attracted a substantial following in research, teaching, and programming. However, there is confusion regarding ...

    • Mechanical Analysis of Reliable Communication in the Alternating Bit Protocol Using the Maude Invariant Analyzer Tool 

      Rocha, Camilo; Meseguer, José (Springer., 2014)
      The InvA tool supports the deductive verification of safety properties of infinite-state concurrent systems. Given a concurrent system specified as a rewrite theory and a safety formula to be verified, InvA reduces such a ...

    • Proving Safety Properties of Rewrite Theories 

      Rocha, Camilo; Meseguer, José (SpringerBerlín, 2011)
      Rewrite theories are a general and expressive formalism for specifying concurrent systems in which states are axiomatized by equations and transitions among states are axiomatized by rewrite rules. We present a deductive ...