Extending the Dafny IDE with tactics and dead annotation analysis (tool demo)

Gudmund Grov, Yuhui Lin, Léon McGregor, Vytautas Tumas, Duncan Cameron

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

This tool demonstration shows two extensions to the Dafny Visual Studio IDE. Both of the extensions have the ability to improve the program text and to support users when developing Dafny programs: re-usable tactics can replace proofs by high-level proof patterns, while proof elements that are not required can be removed in a semi-automatic manner.

Original languageEnglish
Title of host publicationProceedings of the Third Workshop on Formal Integrated Development Environment
EditorsCatherine Dubois, Paolo Masci, Dominique Méry
Number of pages5
Volume240
Publication statusPublished - 27 Jan 2017
EventThird Workshop on Formal Integrated Development Environment - Limassol, Cyprus
Duration: 8 Nov 20168 Nov 2016

Workshop

WorkshopThird Workshop on Formal Integrated Development Environment
CountryCyprus
CityLimassol
Period8/11/168/11/16

ASJC Scopus subject areas

  • Software

Fingerprint Dive into the research topics of 'Extending the Dafny IDE with tactics and dead annotation analysis (tool demo)'. Together they form a unique fingerprint.

Cite this