Home > Research > Publications & Outputs > The Faultless Way of Programming

Research

Electronic data

  • EuroPLoP 2024 Faultless Preprint

    Accepted author manuscript, 879 KB, PDF document

    Available under license: CC BY: Creative Commons Attribution 4.0 International License

Keywords

View graph of relations

The Faultless Way of Programming: Principles, Patterns, Practices, and Peculiarities for Verification in Dafny

Research output: Contribution in Book/Report/Proceedings - With ISBN/ISSN › Conference contribution/Paper › peer-review

E-pub ahead of print

Standard

The Faultless Way of Programming: Principles, Patterns, Practices, and Peculiarities for Verification in Dafny. / Noble, James; Weir, Charles.
EuroPLoP 2024 Proceedings. New York: ACM, 2024.

Research output: Contribution in Book/Report/Proceedings - With ISBN/ISSN › Conference contribution/Paper › peer-review

Harvard

Noble, J & Weir, C 2024, The Faultless Way of Programming: Principles, Patterns, Practices, and Peculiarities for Verification in Dafny. in EuroPLoP 2024 Proceedings. ACM, New York.

APA

Noble, J., & Weir, C. (2024). The Faultless Way of Programming: Principles, Patterns, Practices, and Peculiarities for Verification in Dafny. In EuroPLoP 2024 Proceedings ACM. Advance online publication.

Vancouver

Noble J, Weir C. The Faultless Way of Programming: Principles, Patterns, Practices, and Peculiarities for Verification in Dafny. In EuroPLoP 2024 Proceedings. New York: ACM. 2024 Epub 2024 Nov 15.

Author

Noble, James ; Weir, Charles. / The Faultless Way of Programming : Principles, Patterns, Practices, and Peculiarities for Verification in Dafny. EuroPLoP 2024 Proceedings. New York : ACM, 2024.

Bibtex

@inproceedings{d7c334fb2ab544e7854e4c4d26ca5665,
title = "The Faultless Way of Programming: Principles, Patterns, Practices, and Peculiarities for Verification in Dafny",
abstract = "There is one faultless way of programming. It uses computer intelligence to validate computer code: formal verification. Yet for developers this faultless approach has remained alien, incomprehensible, and many miss out on its proven benefits. This set of patterns introduces Dafny to developers. Dafny provides a powerful way to incorporate formal verification into software that is integrated with languages like Java and C#, generating code that is provably free from defects and problems.The patterns range from the Dafny design philosophy to concepts like ghost variables and implementation details such as the use of generative artificial intelligence. By offering an accessible approach to a difficult subject, they support developers in producing faultless code.",
keywords = "Patterns, Dafny, Correctness, Verification",
author = "James Noble and Charles Weir",
year = "2024",
month = nov,
day = "15",
language = "English",
booktitle = "EuroPLoP 2024 Proceedings",
publisher = "ACM",

}

RIS

TY - GEN

T1 - The Faultless Way of Programming

T2 - Principles, Patterns, Practices, and Peculiarities for Verification in Dafny

AU - Noble, James

AU - Weir, Charles

PY - 2024/11/15

Y1 - 2024/11/15

N2 - There is one faultless way of programming. It uses computer intelligence to validate computer code: formal verification. Yet for developers this faultless approach has remained alien, incomprehensible, and many miss out on its proven benefits. This set of patterns introduces Dafny to developers. Dafny provides a powerful way to incorporate formal verification into software that is integrated with languages like Java and C#, generating code that is provably free from defects and problems.The patterns range from the Dafny design philosophy to concepts like ghost variables and implementation details such as the use of generative artificial intelligence. By offering an accessible approach to a difficult subject, they support developers in producing faultless code.

AB - There is one faultless way of programming. It uses computer intelligence to validate computer code: formal verification. Yet for developers this faultless approach has remained alien, incomprehensible, and many miss out on its proven benefits. This set of patterns introduces Dafny to developers. Dafny provides a powerful way to incorporate formal verification into software that is integrated with languages like Java and C#, generating code that is provably free from defects and problems.The patterns range from the Dafny design philosophy to concepts like ghost variables and implementation details such as the use of generative artificial intelligence. By offering an accessible approach to a difficult subject, they support developers in producing faultless code.

KW - Patterns

KW - Dafny

KW - Correctness

KW - Verification

M3 - Conference contribution/Paper

BT - EuroPLoP 2024 Proceedings

PB - ACM

CY - New York

ER -