Building correct-by-construction systems with formal patterns
From MaRDI portal
Publication:6562511
DOI10.1007/978-3-031-43345-0_1MaRDI QIDQ6562511
Publication date: 26 June 2024
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Formalization and correctness of the PALS architectural pattern for distributed real-time systems
- Algebraic simulations
- Reflection in membership equational logic, many-sorted equational logic, Horn logic with equality, and rewriting logic
- Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols
- Maude's module algebra
- Equational abstractions
- All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
- Conditional rewriting logic as a unified model of concurrency
- Equational rules for rewriting logic
- ISSAC '88, Proceedings of the International Symposium on Symbolic and Algebraic Computation. Rome, Italy, July 4--8, 1988.
- Induction = I-axiomatization + first-order consistency.
- CASL reference manual. The complete documentation of the common algebraic specification language.
- Twenty years of rewriting logic
- On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories
- Folding variant narrowing and optimal variant termination
- Equational unification and matching, and symbolic reachability analysis in Maude 3.2 (system description)
- Generalized rewrite theories, coherence completion, and symbolic methods
- Programming and symbolic computation in Maude
- A partial evaluation framework for order-sorted equational programs modulo axioms
- Read atomic transactions with prevention of lost updates: ROLA and its formal analysis
- Semantic foundations for generalized rewrite theories
- Abstract Logical Model Checking of Infinite-State Systems Using Narrowing
- Proving Safety Properties of Rewrite Theories
- Termination Modulo Combinations of Equational Theories
- A Formal Pattern Architecture for Safe Medical Systems
- A Constructor-Based Reachability Logic for Rewrite Theories
- Mechanical Analysis of Reliable Communication in the Alternating Bit Protocol Using the Maude Invariant Analyzer Tool
- Automatic analysis of consistency properties of distributed transaction systems in Maude
- Inductive Reasoning with Equality Predicates, Contextual Rewriting and Variant-Based Simplification
- Verification of the IBOS Browser Security Properties in Reachability Logic
- Checking Sufficient Completeness by Inductive Theorem Proving
- A survey of statistical model checking
This page was built for publication: Building correct-by-construction systems with formal patterns
