A structural embedding of Ocsid in PVS

DOI10.1007/3-540-44755-5_20MaRDI QIDQ4790666zbMATH OpenFDO

Authors P. Kellomäki

Publication date 4 February 2003

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2152/21520281

Mathematics Subject Classification ID

Recommendations

• PVS embedding of cCSP semantic models and their relationship
• A practical algorithm for structure embedding
• Embedding structures
• Embedded o-minimal structures
• Mechanization of an integrated approach: Shallow embedding into SAL/PVS
• Effective embeddings for pairs of structures
• A theory of PWD-structures
• Towards robustness analysis using PVS

Cited in

(6)

• Ocsid
• Mechanization of an integrated approach: Shallow embedding into SAL/PVS
• An embedding of Ruby in Isabelle
• Action systems in incremental and aspect-oriented modeling
• PVS embedding of cCSP semantic models and their relationship
• PVS as a proof obligation generator

Describes a project that uses

Uses Software

• HOL-UNITY
• PVS
• DisCo
• Coq
• HOL

This page was built for publication: A structural embedding of Ocsid in PVS

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