CoSMed: A Confidentiality-Verified Social Media Platform

DOI10.1007/978-3-319-43144-4_6zbMATH Open1451.68167OpenAlexW3016501173MaRDI QIDQ2829248FDOQ2829248

Armando Pesenti Gritti, Andrei Popescu, Author name not available (Why is that?), Thomas Bauereiß

Publication date: 27 October 2016

Published in: Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL: https://eprints.mdx.ac.uk/22094/1/CoSMedITP2016.pdf

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites Work

• Ur/Web
• Isabelle/HOL. A proof assistant for higher-order logic
• Concrete Semantics
• CakeML
• Code Generation via Higher-Order Rewrite Systems
• A verified information-flow architecture
• Java and the Java Memory Model — A Unified, Machine-Checked Formalisation
• A note on spark varieties

Cited In (1)

• CoSMed: a confidentiality-verified social media platform

Uses Software

• Isabelle/HOL
• CakeML
• seL4
• Jif
• CoSMed
• Ur/Web
• CAVA LTL Modelchecker
• FlowFox

This page was built for publication: CoSMed: A Confidentiality-Verified Social Media Platform

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