Accessible Software Verification with Dafny

被引：2
|
作者：
Leino, K. Rustan M. [1 ,2 ]
机构：
[1] Microsoft Res, Software Engn Grp, Washington, DC 98052 USA
[2] Imperial Coll Londons, Dept Comp, London, England
来源：
IEEE SOFTWARE | 2017年 / 34卷 / 06期
关键词：
D O I：
暂无
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
引用
收藏
页码：94 / 97
页数：4
相关论文
共 50 条
  • [1] Mechanised Verification Patterns for Dafny
    Grov, Gudmund
    Lin, Yuhui
    Tumas, Vytautas
    FM 2016: FORMAL METHODS, 2016, 9995 : 326 - 343
  • [2] Deductive Verification of Smart Contracts with Dafny
    Cassez, Franck
    Fuller, Joanne
    Quiles, Horacio Mijail Anton
    FORMAL METHODS FOR INDUSTRIAL CRITICAL SYSTEMS (FMICS 2022), 2022, 13487 : 50 - 66
  • [3] Automatic Verification of Dafny Programs with Traits
    Ahmadi, Reza
    Leino, K. Rustan M.
    Nummenmaa, Jyrki
    17TH WORKSHOP ON FORMAL TECHNIQUES FOR JAVA-LIKE PROGRAMS (FTFJP 2015), 2015,
  • [4] Verification of Scapegoat Trees Using Dafny
    Wang, Jiapeng
    Chen, Sini
    Zhu, Huibiao
    NASA FORMAL METHODS, NFM 2024, 2024, 14627 : 118 - 135
  • [5] Deductive verification of smart contracts with Dafny
    Franck Cassez
    Joanne Fuller
    Horacio Mijail Antón Quiles
    International Journal on Software Tools for Technology Transfer, 2024, 26 : 131 - 145
  • [6] Deductive verification of smart contracts with Dafny
    Cassez, Franck
    Fuller, Joanne
    Quiles, Horacio Mijail Anton
    INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER, 2024, 26 (02) : 131 - 145
  • [7] Dafny Meets the Verification Benchmarks Challenge
    Leino, K. Rustan M.
    Monahan, Rosemary
    VERIFIED SOFTWARE: THEORIES, TOOLS, EXPERIMENTS, 2010, 6217 : 112 - +
  • [8] Verification of the Incremental Merkle Tree Algorithm with Dafny
    Cassez, Franck
    FORMAL METHODS, FM 2021, 2021, 13047 : 445 - 462
  • [9] A Tutorial on Using Dafny to Construct Verified Software
    Lucio, Paqui
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2017, (237): : 1 - 19
  • [10] DIONE: A Protocol Verification System Built with DAFNY for I/O Automata
    Hsieh, Chiao
    Mitra, Sayan
    INTEGRATED FORMAL METHODS, IFM 2019, 2019, 11918 : 227 - 245
12345