Twenty years of rewriting logic
From MaRDI portal
Publication:1931904
DOI10.1016/j.jlap.2012.06.003zbMath1267.03043OpenAlexW2006766139MaRDI QIDQ1931904
Publication date: 16 January 2013
Published in: The Journal of Logic and Algebraic Programming (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.jlap.2012.06.003
securityreal-time systemssurvey paperbioinformaticsconcurrencylogical frameworksprogramming language semanticstemporal logicsrewriting logicprobabilistic systemsformal specification and verificationnetworks and distributed systems
Related Items
Detection and diagnosis of deviations in distributed systems of autonomous agents ⋮ From Outermost Reduction Semantics to Abstract Machine ⋮ Sentence-normalized conditional narrowing modulo in rewriting logic and Maude ⋮ Verifiable abstractions for contract-oriented systems ⋮ José Meseguer: Scientist and Friend Extraordinaire ⋮ Sentence-Normalized Conditional Narrowing Modulo in Rewriting Logic and Maude ⋮ Two Decades of Maude ⋮ Formal Universes ⋮ Generic Proof Scores for Generate & Check Method in CafeOBJ ⋮ Verifying Reachability-Logic Properties on Rewriting-Logic Specifications ⋮ Weak Bisimulation as a Congruence in MSOS ⋮ Algebraic Reinforcement Learning ⋮ On the accuracy of formal verification of selective defenses for TDoS attacks ⋮ Liveness Properties in CafeOBJ – A Case Study for Meta-Level Specifications ⋮ The Maude strategy language ⋮ Symbolic Analysis of Maude Theories with Narval ⋮ QMaude: quantitative specification and verification in rewriting logic ⋮ From hidden to visible: a unified framework for transforming behavioral theories into rewrite theories ⋮ Rewriting-based repairing strategies for XML repositories ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ A constraint-based language for multiparty interactions ⋮ Mechanical Analysis of Reliable Communication in the Alternating Bit Protocol Using the Maude Invariant Analyzer Tool ⋮ Strategies, model checking and branching-time properties in Maude ⋮ Strict coherence of conditional rewriting modulo axioms ⋮ Programming and symbolic computation in Maude ⋮ Applications and extensions of context-sensitive rewriting ⋮ Limited second-order functionality in a first-order setting ⋮ A Formal, Resource Consumption-Preserving Translation from Actors with Cooperative Scheduling to Haskell* ⋮ Labelled port graph -- a formal structure for models and computations ⋮ A rewriting logic approach to specification, proof-search, and meta-proofs in sequent systems ⋮ Capturing constrained constructor patterns in matching logic ⋮ Generate & Check Method for Verifying Transition Systems in CafeOBJ ⋮ Executable rewriting logic semantics of Orc and formal analysis of Orc programs ⋮ Symbolic computation in Maude: some tapas
Uses Software
Cites Work
- State space reduction in the Maude-NRL protocol analyzer
- Formal modeling: actors, open systems, biological systems. Essays dedicated to Carolyn Talcott on the occasion of her 70th birthday
- Using typed lambda calculus to implement formal systems on a machine
- Characterizing and proving operational termination of deterministic conditional term rewriting systems
- Computer security -- ESORICS 2009. 14th European symposium on research in computer security, Saint-Malo, France, September 21--23, 2009. Proceedings
- The gamma model and its discipline of programming
- Two case studies of semantics execution in Maude: CCS and LOTOS
- Algebraic simulations
- Complete symbolic reachability analysis using back-and-forth narrowing
- A rewriting-based inference system for the NRL protocol analyzer and its meta-logical properties
- Specification and analysis of the AER/NCA active network protocol suite in real-time Maude
- Algebraic methodology and software technology. 11th international conference, AMAST 2006, Kuressaare, Estonia, July 5--8, 2006. Proceedings.
- Reflection in membership equational logic, many-sorted equational logic, Horn logic with equality, and rewriting logic
- A rewriting logic framework for operational semantics of membrane systems
- The rewriting logic semantics project
- Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols
- Semantics and pragmatics of real-time maude
- Representing the MSR cryptoprotocol specification language in an extension of rewriting logic with dependent types
- Maude's module algebra
- Termination of just/fair computations in term rewriting
- Transactions on Computational Systems Biology VI
- Formal methods for computational systems biology. 8th international school on formal methods for the design of computer, communication, and software systems, SFM 2008 Bertinoro, Italy, June 2--7, 2008. Advanced lectures
- Formal methods for open object-based distributed systems. 10th IFIP WG 6.1 international conference, FMOODS 2008, Oslo, Norway, June 4--6, 2008. Proceedings
- Formal modeling and analysis of timed systems. 5th international conference, FORMATS 2007, Salzburg, Austria, October 3--5, 2007. Proceedings
- A timed semantics of Orc
- Equational abstractions
- An algebraic semantics for MOF
- Tests and proofs. 4th international conference, TAP 2010, Málaga, Spain, July 1--2, 2010. Proceedings
- An overview of the K semantic framework
- Context-sensitive dependency pairs
- All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
- Formal modeling, performance estimation, and model checking of wireless sensor network algorithms in Real-Time Maude
- Fundamental approaches to software engineering. 12th international conference, FASE 2009, held as part of the joint European conferences on theory and practice of software, ETAPS 2009, York, UK, March 22--29, 2009. Proceedings
- A rewriting logic approach to operational semantics
- FM 2009: Formal methods. Second world congress, Eindhoven, The Netherlands, November 2--6, 2009. Proceedings
- Operational termination of conditional term rewriting systems
- The calculus of constructions
- Sequential and concurrent behaviour in Petri net theory
- Formal methods for industrial applications. Specification and programming the Steam Boiler Control
- Conditional rewriting logic as a unified model of concurrency
- The chemical abstract machine
- A theory of timed automata
- Isabelle. A generic theorem prover
- Combining symbolic constraint solvers on algebraic domains
- A logic for reasoning about time and reliability
- Timed rewriting logic with an application to object-based specification
- Recent trends in algebraic development techniques. 12th international workshop, WADT '97, Tarquinia, Italy, June 3--7, 1997. Selected papers
- Specification and verification of the tree identify protocol of IEEE 1394 in rewriting logic
- Rewriting techniques and applications. 14th international conference, RTA 2003, Valencia, Spain, June 9--11, 2003. Proceedings
- Theorem proving modulo
- A causal semantics for CCS via rewriting logic
- ELAN from a rewriting logic point of view
- Maude: specification and programming in rewriting logic
- Reflection in conditional rewriting logic
- Specification of real-time and hybrid systems in rewriting logic
- Actor theories in rewriting logic
- Equational rules for rewriting logic
- A formal approach to object-oriented software engineering
- Rewriting logic: Roadmap and bibliography
- Data-driven modeling of Alzheimer disease pathogenesis
- Rewriting techniques and applications. 6th international conference, RTA-95, Kaiserslautern, Germany, April 5--7, 1995. Proceedings
- FM '99. Formal methods. World congress on Formal methods in the development of computing systems. Toulouse, France, September 20--24, 1999. Proceedings. In 2 vols
- Higher order unification via explicit substitutions
- Context-sensitive rewriting strategies
- External rewriting for skeptical proof assistants
- Membrane computing. An introduction.
- Handbook of philosophical logic. Vol. 9
- Axiomatizing the algebra of net computations and processes
- On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories
- Rewriting semantics of production rule sets
- Verifying hierarchical Ptolemy II discrete-event models using real-time maude
- Rewriting logic and its applications. 8th international workshop, WRLA 2010, held as a satellite event of ETAPS 2010, Paphos, Cyprus, March 20--21, 2010. Revised selected papers
- Specification and proof in membership equational logic
- Proving operational termination of membership equational programs
- Executable rewriting logic semantics of Orc and formal analysis of Orc programs
- Executable structural operational semantics in Maude
- Formal methods for open object-based distributed systems. 9th IFIP WG 6.1 international conference FMOODS 2007, Paphos, Cyprus, June 6--8, 2007. Proceedings.
- Formal methods in software and systems modeling. Essays dedicated to Hartmut Ehrig on the occasion of his 60th birthday
- Term rewriting and applications. 18th international conference, RTA 2007, Paris, France, June 26--28, 2007. Proceedings
- Semantic foundations for generalized rewrite theories
- Statistical probabilistic model checking with a focus on time-bounded properties
- Modular and incremental automated termination proofs
- Modular and incremental proofs of AC-termination
- HOL-λσ: an intentional first-order expression of higher-order logic
- Language Prototyping: An Algebraic Specification Approach
- Methods for Proving Termination of Rewriting-based Programming Languages by Transformation
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Rewriting Logic Specification of Membrane Systems with Promoters and Inhibitors
- Strategy-Based Proof Calculus for Membrane Systems
- Which Soft Constraints do you Prefer?
- Operational Termination of Membership Equational Programs: the Order-Sorted Way
- A Rewriting Semantics for Maude Strategies
- Proved trees
- REWRITING WITH STRATEGIES IN $\mathsf{ELAN}$: A FUNCTIONAL SEMANTICS
- SymPLFIED: Symbolic Program-Level Fault Injection and Error Detection Framework
- Reflective metalogical frameworks
- Automated Reasoning
- A rewriting calculus for cyclic higher-order term graphs
- Computer Aided Verification
- Algebraic Methodology and Software Technology
- Algebraic Methodology and Software Technology
- Algebraic Methodology and Software Technology
- Automatic Validation of Transformation Rules for Java Verification Against a Rewriting Semantics
- An Executable Formalization of the HOL/Nuprl Connection in the Metalogical Framework Twelf
- Variants, Unification, Narrowing, and Symbolic Reachability in Maude 2.6
- Pure Type Systems in Rewriting Logic: Specifying Typed Higher-Order Languages in a First-Order Logical Framework
- vlogsl: A Strategy Language for Simulation-Based Verification of Hardware
- Theoretical Aspects of Computing – ICTAC 2005
- Analyzing Pathways Using SAT-Based Approaches
- Symbolic Model Checking of Infinite-State Systems Using Narrowing
- On the Completeness of Context-Sensitive Order-Sorted Specifications
- Algebra and Coalgebra in Computer Science
- A Sound and Complete Deductive System for CTL* Verification
- Monadic Elementary Formal Systems
- Term Rewriting and Applications
- Term Rewriting and Applications
- Term Rewriting and Applications
- Recent Trends in Algebraic Development Techniques
- Computer Aided Verification
- FUNCTORIAL SEMANTICS OF ALGEBRAIC THEORIES
- Coverset Induction with Partiality and Subsorts: A Powerlist Case Study
- Non-intrusive Formal Methods and Strategic Rewriting for a Chemical Application
- Conditional rewriting logic: Deduction, models and concurrency
- Correct Hardware Design and Verification Methods
- Hybrid Systems: Computation and Control
- Automated Deduction – CADE-19
- Formal Methods for Open Object-Based Distributed Systems
- Formal Methods for Open Object-Based Distributed Systems
- Formal Methods for Open Object-Based Distributed Systems
- Rewriting logic as a semantic framework for concurrency: a progress report
- Deduction, Strategies, and Rewriting
- Abstraction and Completeness for Real-Time Maude
- A Rewriting Semantics for ABEL with Applications to Hardware/Software Co-Design and Analysis
- Partial Order Reduction for Rewriting Semantics of Programming Languages
- A Rewriting Logic Framework for Soft Constraints
- Narrowing and Rewriting Logic: from Foundations to Applications
- Termination of rewriting under strategies
- Abstract Certification of Global Non-interference in Rewriting Logic
- Type Fusion
- Matching Logic: An Alternative to Hoare/Floyd Logic
- The Rewriting Logic Semantics Project: A Progress Report
- Proving Safety Properties of Rewrite Theories
- The NRL Protocol Analyzer: An Overview
- Timed CTL Model Checking in Real-Time Maude
- What Is a Multi-modeling Language?
- Generalized Theoroidal Institution Comorphisms
- A Rewriting Logic Approach to Type Inference
- Declarative Debugging of Rewriting Logic Specifications
- Maude-NPA: Cryptographic Protocol Analysis Modulo Equational Properties
- Solving SAT and SAT Modulo Theories
- Theorem Proving Modulo Based on Boolean Equational Procedures
- The Temporal Logic of Rewriting: A Gentle Introduction
- Effectively Checking the Finite Variant Property
- Propositional Tree Automata
- MTT: The Maude Termination Tool (System Description)
- A Modular Equational Generalization Algorithm
- State Space Reduction of Rewrite Theories Using Invisible Transitions
- Termination Modulo Combinations of Equational Theories
- Completion of a Set of Rules Modulo a Set of Equations
- Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
- Complete Sets of Reductions for Some Equational Theories
- A framework for defining logics
- Institutions: abstract model theory for specification and programming
- Symmetric monoidal and cartesian double categories as a semantic framework for tile logic
- Axiomatizing permutation equivalence
- Proving Termination in the Context-Sensitive Dependency Pair Framework
- Folding Variant Narrowing and Optimal Variant Termination
- Concurrent Rewriting Semantics and Analysis of Asynchronous Digital Circuits
- A Formal Pattern Architecture for Safe Medical Systems
- On the Behavioral Semantics of Real-Time Domain Specific Visual Languages
- The Linear Temporal Logic of Rewriting Maude Model Checker
- Constructors, Sufficient Completeness, and Deadlock Freedom of Rewrite Theories
- Order-Sorted Generalization
- A Rewriting-Based Model Checker for the Linear Temporal Logic of Rewriting
- Order-sorted Equational Unification Revisited
- Strategy-Based Rewrite Semantics for Membrane Systems Preserves Maximal Concurrency of Evolution Rule Actions
- A Port Graph Calculus for Autonomic Computing and Invariant Verification
