CoSMed: a confidentiality-verified social media platform
DOI10.1007/s10817-017-9443-3zbMath1451.68168OpenAlexW2775081510MaRDI QIDQ1663221
Franco Raimondi, Armando Pesenti Gritti, Andrei Popescu, Thomas Bauereiß
Publication date: 21 August 2018
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://eprints.mdx.ac.uk/23357/1/cosmed_extended.pdf
formal verificationIsabelle/HOLinteractive theorem provinginformation flow securitysecure social media platform
Specification and verification (program logics, model checking, etc.) (68Q60) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Related Items (1)
Uses Software
Cites Work
- Semi-intelligible Isar proofs from machine-generated proofs
- Automated reasoning with analytic tableaux and related methods. 24th international conference, TABLEAUX 2015, Wrocław, Poland, September 21--24, 2015. Proceedings
- Interactive theorem proving. 7th international conference, ITP 2016, Nancy, France, August 22--25, 2016. Proceedings
- Isabelle/HOL. A proof assistant for higher-order logic
- Algorithms for model checking HyperLTL and HyperCTL\(^*\)
- Automated verification of selected equivalences for security protocols
- CoSMed: A Confidentiality-Verified Social Media Platform
- Truly Modular (Co)datatypes for Isabelle/HOL
- Java and the Java Memory Model — A Unified, Machine-Checked Formalisation
- Concrete Semantics
- Encoding Monomorphic and Polymorphic Types
- A Brief Overview of Mizar
- Code Generation via Higher-Order Rewrite Systems
- Constructive Type Classes in Isabelle
- A mechanically checked proof of the AMD5/sub K/86/sup TM/ floating-point division program
- Formal certification of code-based cryptographic proofs
- A verified information-flow architecture
- CakeML
This page was built for publication: CoSMed: a confidentiality-verified social media platform
