CoSMed: A Confidentiality-Verified Social Media Platform

DOI10.1007/978-3-319-43144-4_6zbMath1451.68167OpenAlexW3016501173MaRDI QIDQ2829248

Armando Pesenti Gritti, Franco Raimondi, Andrei Popescu, 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)

Related Items (1)

CoSMed: a confidentiality-verified social media platform

Uses Software

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

Cites Work

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

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