Verifying a signature architecture: a comparative case study

DOI10.1007/s00165-006-0012-5zbMath1111.68075OpenAlexW1989012792MaRDI QIDQ877156

Kazuo Takaragi, Burkhart Wolff, Hironobu Kuruma, Kunihiko Miyazaki, David A. Basin

Publication date: 19 April 2007

Published in: Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL: http://doc.rero.ch/record/316084/files/165_2006_Article_12.pdf

zbMATH Keywords

Theorem provingModel checkingSecurityFormal methodsComparisonCase study

Mathematics Subject Classification ID

Related Items (4)

Proving fairness and implementation correctness of a microkernel scheduler ⋮ HOL-Boogie -- an interactive prover-backend for the verifying C compiler ⋮ Mechanizing the Powerset Construction for Restricted Classes of ω-Automata ⋮ HOL-Boogie — An Interactive Prover for the Boogie Program-Verifier

Uses Software

• HOL-Z
• SPIN
• PVS
• Nuprl
• NQTHM
• OFMC
• Z
• LTL2BA
• ICS

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Combining partial-order reductions with on-the-fly model-checking.
• Automata-theoretic techniques for modal logics of programs
• Completing the temporal picture
• Isabelle/HOL. A proof assistant for higher-order logic
• Experimental evaluation of verification and validation tools on Martian Rover software
• Complete Integer Decision Procedures as Derived Rules in HOL
• The B-Book
• A really temporal logic
• Automated Deduction – CADE-20
• FM 2005: Formal Methods

This page was built for publication: Verifying a signature architecture: a comparative case study