An automatically verified prototype of the Tokeneer ID station specification

DOI10.1007/s10817-021-09602-2OpenAlexW3196661045MaRDI QIDQ2069869

Gianfranco Rossi, Maximiliano Cristiá

Publication date: 21 January 2022

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/2009.00999

zbMATH Keywords

Z notationconstraint programmingautomated verificationprototypingautomated proof\(\{log\}\)Tokeneer ID station specification

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (3)

An automatically verified prototype of the Android permissions system ⋮ A Decision Procedure for a Theory of Finite Sets with Finite Integer Intervals ⋮ Unnamed Item

Uses Software

• Z
• seL4
• JSetL
• SETL

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• A set solver for finite set relation algebra
• Automated proof of Bell-LaPadula security properties
• Solving quantifier-free first-order constraints over finite sets and binary relations
• Integrated formal methods. 6th international conference, IFM 2007, Oxford, UK, July 2--5, 2007. Proceedings.
• A decision procedure for restricted intensional sets
• Automated reasoning with restricted intensional sets
• The Tokeneer Experiments
• Set unification
• Decision problems for equational theories of relation algebras
• Formal Analysis of Android's Permission-Based Security Model
• Using Answer Set Programming in the Development of Verified Software.

This page was built for publication: An automatically verified prototype of the Tokeneer ID station specification