Reseña: Isabelle and security
Se ha publicado un artículo sobre verifiación formal con Isabelle/HOL titulado Isabelle and security
Sus autores son
- Jasmin Christian Blanchette (del grupo VeriDis (Verification of Distributed Systems) en el Inria Nancy & LORIA y del grupo Automation of Logic en el Max Planck Institute for Informatics de Saarbrücken) y
- Andrei Popescu (del grupo Foundations of Computing en la Middlesex University London).
Su resumen es
Isabelle/HOL is a general-purpose proof assistant based on higher-order logic. Its main strengths are its simple-yet-expressive logic and its proof automation. Security researchers make up a significant fraction of Isabelle’s users. In the past few years, many exciting developments have taken place, connecting programming languages, operating system kernels, and security.