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

DOI10.1007/978-3-662-49665-7_23MaRDI QIDQ2801764zbMATH OpenOpenAlexFDO

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

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)

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

Cited in

(3)

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

Describes a project that uses

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)