Titlebook: Rewriting Logic and Its Applications; 8th International Wo Peter Csaba Ölveczky Conference proceedings 2010 Springer Berlin Heidelberg 2010

hereditary

A Church-Rosser Checker Tool for Conditional Order-Sorted Equational Maude Specificationsr having a complete agreement between the specification’s initial algebra, mathematical semantics, and its operational semantics by rewriting. Checking this property for expressive specifications that are order-sorted, conditional with possibly extra variables in their condition, and whose equations

Antarctic

A Maude Coherence Checker Tool for Conditional Order-Sorted Rewrite Theoriesbe (ground) coherent with . modulo .. The correctness of many important formal verification tasks, including search, LTL model checking, and the development of abstractions, crucially depends on the theory being ground coherent. Furthermore, many specifications of interest are typed, have equations

notice

K-Maude: A Rewriting Based Tool for Semantics of Programming Languagesccepting K modules along with regular Maude modules and a collection of tools for transforming K language definitions into Maude rewrite theories for execution or analysis, or into . for documentation purposes. The current K-Maude prototype was successfully used in defining several languages and lan

Infusion

Collecting Semantics under Predicate Abstraction in the K Frameworkicate abstraction technique into the K framework. To express this technique in K, we go to the foundations of predicate abstraction, that is abstract interpretation, and use its collecting semantics. As such, we propose a suitable description in K for collecting semantics under predicate abstraction

avulsion

Concurrent Rewriting Semantics and Analysis of Asynchronous Digital Circuitsge of . (PRs). One of the present limitations of the state of the art in asynchronous circuit design is that no formal executable semantics of asynchronous circuits has yet been given at the PR level. The primary contribution of this paper is to define, using rewriting logic and Maude, an executable

注视

A Formal Pattern Architecture for Safe Medical Systemser, such patterns should also provide formal guarantees that critical safety properties are met. We leverage the power of rewriting logic and parameterization available in Real-Time Maude to add a formal basis for analysis of a novel safety pattern for medical devices. We demonstrate practicality an

badinage

BILIO

confide

The Linear Temporal Logic of Rewriting Maude Model Checkerstem. The Linear Temporal Logic of Rewriting (LTLR) extends linear temporal logic with spatial action patterns which represent rewriting events. LTLR generalizes and extends various state-based and event-based logics and aims to avoid certain types of mismatches between a system and its temporal log

甜食

Enhancing the Debugging of Maude Specificationsutation and guiding the user through it to find the error. Two different kinds of errors are considered for debugging: .—a wrong result obtained from an initial value—and .—a term that should be reachable but cannot be obtained from an initial value—, where the latter has only been considered in non