Verifying a Verifier: On the Formal Correctness of an LTS Transformation Verification Technique

DOI10.1007/978-3-662-49665-7_23zbMATH Open1378.68114OpenAlexW2477444687MaRDI QIDQ2801764FDOQ2801764

Authors: Sander de Putter, Anton Wijs 

Publication date: 21 April 2016

Published in: Fundamental Approaches to Software Engineering (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-662-49665-7_23

Recommendations

• scientific article; zbMATH DE number 1538039
• Correct Hardware Design and Verification Methods
• An LTL proof system for runtime verification
• Model Checking Software
• Program derivation with verified transformations — a case study
• Verification of object-oriented programs: a transformational approach
• Formal verification of an executable LTL model checker with partial order reduction

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Cited In (3)

• LMS-Verify: abstraction without regret for verified systems programming
• A formal verification technique for behavioural model-to-model transformations
• Formal verification of translation validators

Uses Software

• Coq
• REFINER

This page was built for publication: Verifying a Verifier: On the Formal Correctness of an LTS Transformation Verification Technique

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