Buscar
Mostrando ítems 1-10 de 12
Towards a Maude Formal Environment
(Springer, 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 ...
Axiomatic Set Theory à la Dijkstra and Scholten
(Springer Nature, 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 ...
Mechanical Analysis of Reliable Communication in the Alternating Bit Protocol Using the Maude Invariant Analyzer Tool
(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 ...
Axiomatic Set Theory à la Dijkstra and Scholten
(Springer Nature, 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 ...
Rewriting modulo SMT and open system analysis
(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 ...
Reliable Control Architecture with PLEXIL and ROS for Autonomous Wheeled Robots
(Springer Nature, 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 ...
Theorem Proving Modulo Based on Boolean Equational Procedures
(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 ...
The Formal System of Dijkstra and Scholten
(Springer., 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 ...
Automatic proof-search heuristics in the Maude invariant analyzer tool
(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 ...
A Formal Interactive Verification Environment for the Plan Execution Interchange Language
(© 2020 Springer Nature Switzerland AG., 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 ...