Correctness of high-level transformation systems relative to nested conditions
From MaRDI portal
Publication:3625675
DOI10.1017/S0960129508007202zbMath1168.68022OpenAlexW2079370090MaRDI QIDQ3625675
Karl-Heinz Pennemann, Annegret Habel
Publication date: 6 May 2009
Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1017/s0960129508007202
verificationcorrectnesssatisfiabilitytransformation systemsnested constraintsnested graph conditions
Specification and verification (program logics, model checking, etc.) (68Q60) Grammars and rewriting systems (68Q42) Graphs, diagram schemes, precategories (18A10)
Related Items (62)
Theorem proving graph grammars with attributes and negative application conditions ⋮ Ensuring Correctness of Model Transformations While Remaining Decidable ⋮ Preserving consistency in geometric modeling with graph transformations ⋮ On the Specification and Verification of Model Transformations ⋮ On the Operationalization of Graph Queries with Generalized Discrimination Networks ⋮ Amalgamation of domain specific languages with behaviour ⋮ Satisfiability of Constraint Specifications on XML Documents ⋮ Presenting basic graph logic ⋮ Interactive and automated proofs for graph transformations ⋮ Translating Essential OCL Invariants to Nested Graph Constraints Focusing on Set Operations ⋮ Inductive Invariant Checking with Partial Negative Application Conditions ⋮ Constructing constraint-preserving interaction schemes in adhesive categories ⋮ Initial Conflicts for Transformation Rules with Nested Application Conditions ⋮ Rewriting Theory for the Life Sciences: A Unifying Theory of CTMC Semantics ⋮ Graph Parsing as Graph Transformation ⋮ Graph Consistency as a Graduated Property ⋮ Formal Verification of Invariants for Attributed Graph Transformation Systems Based on Nested Attributed Graph Conditions ⋮ Optimistic and Pessimistic On-the-fly Analysis for Metric Temporal Graph Logic ⋮ A Flexible and Easy-to-Use Library for the Rapid Development of Graph Tools in Java ⋮ A strict constrained superposition calculus for graphs ⋮ Double-pushout-rewriting in \(S\)-Cartesian functor categories: rewriting theory and application to partial triple graphs ⋮ Host-graph-sensitive RETE nets for incremental graph pattern matching with nested graph conditions ⋮ Bounded model checking for interval probabilistic timed graph transformation systems against properties of probabilistic metric temporal graph logic ⋮ Symbolic graphs for attributed graph constraints ⋮ A simple criterion for \(\mathcal{M}, \mathcal{N}\)-adhesivity ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ High-Level Programs and Program Conditions ⋮ Resolution-Like Theorem Proving for High-Level Conditions ⋮ Development of Correct Graph Transformation Systems ⋮ An Algorithm for Approximating the Satisfiability Problem of High-level Conditions ⋮ A navigational logic for reasoning about graph properties ⋮ Finitary -adhesive categories ⋮ Multi-amalgamation of rules with application conditions in -adhesive categories ⋮ -adhesive transformation systems with nested application conditions. Part 1: parallelism, concurrency and amalgamation ⋮ Formal analysis of model transformations based on triple graph grammars ⋮ Analysis of permutation equivalence in -adhesive transformation systems with negative application conditions ⋮ Reasoning with graph constraints ⋮ Evaluation diversity for graph conditions ⋮ Parallel Independence of Amalgamated Graph Transformations Applied to Model Transformation ⋮ Institutions for navigational logics for graphical structures ⋮ Single pushout rewriting in comprehensive systems of graph-like structures ⋮ Transformation rules with nested application conditions: critical pairs, initial conflicts \& minimality ⋮ Rewriting theory for the life sciences: a unifying theory of CTMC semantics ⋮ Comprehensive systems: a formal foundation for multi-model consistency management ⋮ Schema compliant consistency management via triple graph grammars and integer linear programming ⋮ Constructing optimized constraint-preserving application conditions for model transformation rules ⋮ A generalized concurrent rule construction for double-pushout rewriting: generalized concurrency theorem and language-preserving rule applications ⋮ Monadic second-order incorrectness logic for GP 2 ⋮ A generalized concurrent rule construction for double-pushout rewriting ⋮ Incorrectness logic for graph programs ⋮ Evaluation diversity for graph conditions ⋮ Rule-based top-down parsing for acyclic contextual hyperedge replacement grammars ⋮ Verifying graph programs with monadic second-order logic
Cites Work
- Unnamed Item
- Algebraic approach to single-pushout graph transformation
- Graph-based specification of access control policies
- Double-pushout graph transformation revisited
- Satisfiability of High-Level Conditions
- Weakest Preconditions for High-Level Programs
- Parallelism and concurrency in high-level replacement systems
- An Algorithm for Approximating the Satisfiability Problem of High-level Conditions
- A Logic of Graph Constraints
This page was built for publication: Correctness of high-level transformation systems relative to nested conditions