Application of modal logics to the specification and verification of programs

MaRDI QIDQ2759366zbMATH OpenFDO

Authors V. B. Popov, A. S. Anafiev

Publication date 12 December 2001

Published in Dinamicheskie Sistemy (Simferopol') (Search for Journal in Brave)

zbMATH Keywords

algorithmsmodal logicsprogramsemantic tablestemporal logics

Mathematics Subject Classification ID

Logic programming (68N17) Semantics in the theory of computing (68Q55)

Review text

Results of using the methods and algorithms of temporal logics for program verification are presented. The method of temporal semantic tables for investigation of the properties of dynamic processes is presented. The aim of investigations is to transfer the sequential calculation strategies to the regions of the output strategies in the modal logics, particularly, in the temporal logics.

Recommendations

• scientific article; zbMATH DE number 3982508
• scientific article; zbMATH DE number 4055577
• Application of temporal logic to program specification
• scientific article; zbMATH DE number 47403
• scientific article; zbMATH DE number 3924132

Cited in

(16)

• On pushout consistency, modularity and interpolation for logical specifications
• Operational semantics and program verification using many-sorted hybrid modal logic
• Modal Kleene algebra applied to program correctness
• Specifying program properties using modal fixpoint logics: a survey of results
• Specification and Development of Interactive Systems
• Logics of Modal Terms for Systems Specification
• Verification of temporal properties of nondeterministic algorithms
• scientific article; zbMATH DE number 3924132 (Why is no real title available?)
• scientific article; zbMATH DE number 3926220 (Why is no real title available?)
• scientific article; zbMATH DE number 3982508 (Why is no real title available?)
• scientific article; zbMATH DE number 4055577 (Why is no real title available?)
• scientific article; zbMATH DE number 4085007 (Why is no real title available?)
• scientific article; zbMATH DE number 1215473 (Why is no real title available?)
• scientific article; zbMATH DE number 2144768 (Why is no real title available?)
• scientific article; zbMATH DE number 4118343 (Why is no real title available?)
• Application of temporal logic to program specification

This page was built for publication: Application of modal logics to the specification and verification of programs

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