Listar AD - CTG – Informática por autor "649eba80a4c919beefa7d19955bc2950"

Mostrando ítems 1-12 de 12

    • Automatic proof-search heuristics in the Maude invariant analyzer tool 

      Rocha, Camilo (Switzerland, 2013)
      The Invariant Analyzer Tool is an interactive tool that mechanizes an inference system for proving safety properties of concurrent systems, which may be infinite-state or whose set of initial states may be infinite. This ...

    • Axiomatic Set Theory à la Dijkstra and Scholten 

      Acosta, Ernesto; Aldana, Bernarda; Bohórquez, Jaime; Rocha, Camilo (Springer NatureSuiza, 2017)
      The algebraic approach by E.W. Dijkstra and C.S. Scholten to formal logic is a proof calculus, where the notion of proof is a sequence of equivalences proved – mainly – by using substitution of ‘equals for equals’. This ...

    • Axiomatic Set Theory à la Dijkstra and Scholten 

      Acosta, Ernesto; Aldana, Bernarda; Bohórquez, Jaime; Rocha, Camilo (Springer NatureUSA., 2017)
      The algebraic approach by E.W. Dijkstra and C.S. Scholten to formal logic is a proof calculus, where the notion of proof is a sequence of equivalences proved – mainly – by using substitution of ‘equals for equals’. This ...

    • A Formal Interactive Verification Environment for the Plan Execution Interchange Language 

      Rocha, Camilo; Cadavid, Héctor; Siminiceanu, Radu (© 2020 Springer Nature Switzerland AG.Springer, Berlin, Heidelberg., 2012)
      The Plan Execution Interchange Language (PLEXIL) is an open source synchronous language developed by NASA for commanding and monitoring autonomous systems. This paper reports the development of the PLEXIL’s Formal Interactive ...

    • 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 ...

    • Order-Sorted Equality Enrichments Modulo Axioms 

      Gutiérrez, Raúl; Meseguer, José; Rocha, Camilo (SpringerBerlin., 2012)
      Built-in equality and inequality predicates based on comparison of canonical forms in algebraic specifications are frequently used because they are handy and efficient. However, their use places algebraic specifications ...

    • 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 ...

    • Reliable Control Architecture with PLEXIL and ROS for Autonomous Wheeled Robots 

      Cadavid, Héctor; Pérez, Alexander; Rocha, Camilo (Springer NatureSuiza, 2017)
      Today’s autonomous robots are being used for complex tasks, including space exploration, military applications, and precision agriculture. As the complexity of control architectures increases, reliability of autonomous ...

    • Rewriting modulo SMT and open system analysis 

      Rocha, Camilo; Meseguer, José; Muñoz, César (Elsevier, 2016)
      This paper proposes rewriting modulo SMT, a new technique that combines the power of SMT solving, rewriting modulo theories, and model checking. Rewriting modulo SMT is ideally suited to model and analyze reachability ...

    • Theorem Proving Modulo Based on Boolean Equational Procedures 

      Rocha, Camilo; Meseguer, José (Springer, 2008)
      Deduction with inference rules modulo computation rules plays an important role in automated deduction as an effective method for scaling up. We present four equational theories that are isomorphic to the traditional Boolean ...

    • Towards a Maude Formal Environment 

      Durán, Francisco; Rocha, Camilo; Álvarez, José María (SpringerBerlín, 2011)
      Maude is a declarative and reflective language based on rewriting logic in which computation corresponds to efficient deduction by rewriting. Because of its reflective capabilities, Maude has been useful as a metatool in ...