Abstract
We present an advanced modeling and verification toolbox for functional programs with state and exceptions. The toolbox integrates an extensible, monad-based, component model, a monad-based Hoare logic and weakest precondition calculus, and proof systems for temporal logic and bisimilarity. It is implemented in Isabelle/HOL using shallow embeddings and incorporates as much modeling and reasoning power as possible from Isabelle/HOL. We have validated the toolbox's usefulness in a substantial security protocol verification project. © Springer-Verlag Berlin Heidelberg 2007.
Cite
CITATION STYLE
Sprenger, C., & Basin, D. (2007). A monad-based modeling and verification toolbox with application to security protocols. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4732 LNCS, pp. 302–318). Springer Verlag. https://doi.org/10.1007/978-3-540-74591-4_23
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
