An SMT-based approach to the verification of knowledge-based programs

DOI10.1145/3700150MaRDI QIDQ7027872zbMATH OpenFDO

Authors Francesco Belardinelli, Ioana Boureanu, Vadim Malvone, Fortunat Rajaona

Publication date 14 February 2025

Published in Formal Aspects of Computing (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1145/3700150

zbMATH Keywords

epistemic logicepistemic predicate transformersmodel checkingprogram semantics

Mathematics Subject Classification ID

Logics of knowledge and belief (including belief change) (03B42) Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Cites work

• A computationally grounded logic of visibility, perception, and knowledge
• An axiomatic basis for computer programming
• Computer Aided Verification
• scientific article; zbMATH DE number 3902018 (Why is no real title available?)
• scientific article; zbMATH DE number 3574936 (Why is no real title available?)
• scientific article; zbMATH DE number 605806 (Why is no real title available?)
• scientific article; zbMATH DE number 1032009 (Why is no real title available?)
• scientific article; zbMATH DE number 5585443 (Why is no real title available?)
• scientific article; zbMATH DE number 5051652 (Why is no real title available?)
• Knowledge-based programs
• Modal logic
• Program models and semi-public environments
• Program semantics and verification technique for AI-centred programs
• Semantic results for ontic and epistemic change
• Symbolic Model Checking for Dynamic Epistemic Logic
• The dining cryptographers problem: Unconditional sender and recipient untraceability
• The Secret Art of Computer Programming
• The Shadow Knows: Refinement of Ignorance in Sequential Programs
• VERICS 2007 -- a model checker for knowledgee and real-time

This page was built for publication: An SMT-based approach to the verification of knowledge-based programs

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