Ensuring correctness of model transformations while remaining decidable

DOI10.1007/978-3-319-46750-4_18MaRDI QIDQ3179408zbMATH OpenOpenAlexFDO

Authors Jon Haël Brenas, Rachid Echahed, Martin Strecker

Publication date 21 December 2016

Published in Theoretical Aspects of Computing – ICTAC 2016 (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-46750-4_18

zbMATH Keywords

modal logicprogram verificationclassical logicgraph transformationmodel transformation

Mathematics Subject Classification ID

Knowledge representation (68T30) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Grammars and rewriting systems (68Q42) Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70)

Recommendations

• On the Specification and Verification of Model Transformations
• Modeling and verifying graph transformations in proof assistants
• Towards verifying model transformations
• Towards automatic verification of behavior preservation for model transformation via invariant checking
• Semantical Correctness and Completeness of Model Transformations Using Graph and Rule Transformation

Cites work

• scientific article; zbMATH DE number 1936671 (Why is no real title available?)
• A Hoare calculus for graph programs
• A dynamic logic for termgraph rewriting
• Correctness of high-level transformation systems relative to nested conditions
• Dafny: an automatic program verifier for functional correctness
• Deciding effectively propositional logic using DPLL and substitution sets
• Hybrid logics: Characterization, interpolation and complexity
• Inductively Sequential Term-Graph Rewrite Systems
• Managing Change in Graph-Structured Data Using Description Logics
• On the Use of Alloy to Analyze Graph Transformation Systems
• Proving correctness of logically decorated graph rewriting systems
• Sesqui-Pushout Rewriting
• The classical decision problem.
• The monadic second-order logic of graphs. I: Recognizable sets of finite graphs
• Verifying monadic second-order properties of graph programs

Cited in

(3)

• scientific article; zbMATH DE number 1693441 (Why is no real title available?)
• Modeling and verifying graph transformations in proof assistants
• Reasoning formally about database queries and updates

Describes a project that uses

Uses Software

• AutoProof
• z3
• Dafny

This page was built for publication: Ensuring correctness of model transformations while remaining decidable

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3179408)