Tampere University of Technology

TUTCRIS Research Portal

Automatic verification of Dafny programs with traits

Research output: Chapter in Book/Report/Conference proceedingConference contributionScientificpeer-review

Standard

Automatic verification of Dafny programs with traits. / Ahmadi, Reza; Leino, K. Rustan M; Nummenmaa, Jyrki.

Proceedings for the 17th Workshop on Formal Techniques for Java-like Programs, FTfJP 2015: co-located with ECOOP 2015. Association for Computing Machinery, Inc, 2015. a4.

Research output: Chapter in Book/Report/Conference proceedingConference contributionScientificpeer-review

Harvard

Ahmadi, R, Leino, KRM & Nummenmaa, J 2015, Automatic verification of Dafny programs with traits. in Proceedings for the 17th Workshop on Formal Techniques for Java-like Programs, FTfJP 2015: co-located with ECOOP 2015., a4, Association for Computing Machinery, Inc, 17th Workshop on Formal Techniques for Java-like Programs, FTfJP 2015, Prague, Czech Republic, 7/07/15. https://doi.org/10.1145/2786536.2786542

APA

Ahmadi, R., Leino, K. R. M., & Nummenmaa, J. (2015). Automatic verification of Dafny programs with traits. In Proceedings for the 17th Workshop on Formal Techniques for Java-like Programs, FTfJP 2015: co-located with ECOOP 2015 [a4] Association for Computing Machinery, Inc. https://doi.org/10.1145/2786536.2786542

Vancouver

Ahmadi R, Leino KRM, Nummenmaa J. Automatic verification of Dafny programs with traits. In Proceedings for the 17th Workshop on Formal Techniques for Java-like Programs, FTfJP 2015: co-located with ECOOP 2015. Association for Computing Machinery, Inc. 2015. a4 https://doi.org/10.1145/2786536.2786542

Author

Ahmadi, Reza ; Leino, K. Rustan M ; Nummenmaa, Jyrki. / Automatic verification of Dafny programs with traits. Proceedings for the 17th Workshop on Formal Techniques for Java-like Programs, FTfJP 2015: co-located with ECOOP 2015. Association for Computing Machinery, Inc, 2015.

Bibtex - Download

@inproceedings{3e748b744bc54e4e95ec9bd99364d5a6,
title = "Automatic verification of Dafny programs with traits",
abstract = "This paper describes the design of traits, abstract superclasses, in the verification-aware programming language Dafny. Although there is no inheritance among classes in Dafny, the traits make it possible to describe behavior common to several classes and to write code that abstracts over the particular classes involved. The design incorporates behavioral specifications for a trait's methods and functions, just like for classes in Dafny. The design has been implemented in the Dafny tool.",
keywords = "Boogie, Dafny, Program verification, Traits",
author = "Reza Ahmadi and Leino, {K. Rustan M} and Jyrki Nummenmaa",
year = "2015",
month = "7",
day = "7",
doi = "10.1145/2786536.2786542",
language = "English",
booktitle = "Proceedings for the 17th Workshop on Formal Techniques for Java-like Programs, FTfJP 2015: co-located with ECOOP 2015",
publisher = "Association for Computing Machinery, Inc",

}

RIS (suitable for import to EndNote) - Download

TY - GEN

T1 - Automatic verification of Dafny programs with traits

AU - Ahmadi, Reza

AU - Leino, K. Rustan M

AU - Nummenmaa, Jyrki

PY - 2015/7/7

Y1 - 2015/7/7

N2 - This paper describes the design of traits, abstract superclasses, in the verification-aware programming language Dafny. Although there is no inheritance among classes in Dafny, the traits make it possible to describe behavior common to several classes and to write code that abstracts over the particular classes involved. The design incorporates behavioral specifications for a trait's methods and functions, just like for classes in Dafny. The design has been implemented in the Dafny tool.

AB - This paper describes the design of traits, abstract superclasses, in the verification-aware programming language Dafny. Although there is no inheritance among classes in Dafny, the traits make it possible to describe behavior common to several classes and to write code that abstracts over the particular classes involved. The design incorporates behavioral specifications for a trait's methods and functions, just like for classes in Dafny. The design has been implemented in the Dafny tool.

KW - Boogie

KW - Dafny

KW - Program verification

KW - Traits

UR - http://www.scopus.com/inward/record.url?scp=84958750086&partnerID=8YFLogxK

U2 - 10.1145/2786536.2786542

DO - 10.1145/2786536.2786542

M3 - Conference contribution

BT - Proceedings for the 17th Workshop on Formal Techniques for Java-like Programs, FTfJP 2015: co-located with ECOOP 2015

PB - Association for Computing Machinery, Inc

ER -