Author of the publication

Mondex , an electronic purse: specification and refinement checks with the Alloy model-finding method

. Formal Aspects of Computing, 20 (1): 21--39 (January 2008)
DOI: http://dx.doi.org/10.1007/s00165-007-0058-z

Please choose a person to relate this publication to

To differ between persons with the same name, the academic degree and the title of an important publication will be displayed. You can also use the button next to the name to display some publications already assigned to the person.

 

Other publications of authors with the same name

EverCrypt: A Fast, Verified, Cross-Platform Cryptographic Provider., , , , , , , , , and 5 other author(s). IACR Cryptol. ePrint Arch., (2019)EverCrypt: A Fast, Verified, Cross-Platform Cryptographic Provider., , , , , , , , , and 6 other author(s). SP, page 983-1002. IEEE, (2020)Mondex , an electronic purse: specification and refinement checks with the Alloy model-finding method. Formal Aspects of Computing, 20 (1): 21--39 (January 2008)Hardening attack surfaces with formally proven binary format parsers., , , , , , , , , and . PLDI, page 31-45. ACM, (2022)Meta-F ^: Proof Automation with SMT, Tactics, and Metaprograms., , , , , , , , , and 3 other author(s). ESOP, volume 11423 of Lecture Notes in Computer Science, page 30-59. Springer, (2019)Meta-F*: Metaprogramming and Tactics in an Effectful Program Verifier., , , , , , , , , and 3 other author(s). CoRR, (2018)EverParse: Verified Secure Zero-Copy Parsers for Authenticated Message Formats., , , , , , and . USENIX Security Symposium, page 1465-1482. USENIX Association, (2019)FastVer2: A Provably Correct Monitor for Concurrent, Key-Value Stores., , , , , , , and . CPP, page 30-46. ACM, (2023)A Security Model and Fully Verified Implementation for the IETF QUIC Record Layer., , , , , , , , and . SP, page 1162-1178. IEEE, (2021)Steel: proof-oriented programming in a dependently typed concurrent separation logic., , , , , , and . Proc. ACM Program. Lang., 5 (ICFP): 1-30 (2021)