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

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

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 proceeding › Conference 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 language	English
Title of host publication	Proceedings of the Third Workshop on Formal Integrated Development Environment
Editors	Catherine Dubois, Paolo Masci, Dominique Méry
Number of pages	5
Volume	240
Publication status	Published - 27 Jan 2017
Event	Third Workshop on Formal Integrated Development Environment - Limassol, Cyprus Duration: 8 Nov 2016 → 8 Nov 2016

Workshop

Workshop	Third Workshop on Formal Integrated Development Environment
Country/Territory	Cyprus
City	Limassol
Period	8/11/16 → 8/11/16

ASJC Scopus subject areas

Software

Cite this

@inproceedings{86393aefeff54641ba52c36d240c2bf2,

title = "Extending the Dafny IDE with tactics and dead annotation analysis (tool demo)",

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.",

author = "Gudmund Grov and Yuhui Lin and L{\'e}on McGregor and Vytautas Tumas and Duncan Cameron",

year = "2017",

month = jan,

day = "27",

language = "English",

volume = "240",

editor = "Dubois, {Catherine } and Masci, {Paolo } and M{\'e}ry, {Dominique }",

booktitle = "Proceedings of the Third Workshop on Formal Integrated Development Environment",

note = "Third Workshop on Formal Integrated Development Environment ; Conference date: 08-11-2016 Through 08-11-2016",

}

TY - GEN

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

AU - Grov, Gudmund

AU - Lin, Yuhui

AU - McGregor, Léon

AU - Tumas, Vytautas

AU - Cameron, Duncan

PY - 2017/1/27

Y1 - 2017/1/27

N2 - 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.

AB - 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.

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

M3 - Conference contribution

AN - SCOPUS:85018921723

VL - 240

BT - Proceedings of the Third Workshop on Formal Integrated Development Environment

A2 - Dubois, Catherine

A2 - Masci, Paolo

A2 - Méry, Dominique

T2 - Third Workshop on Formal Integrated Development Environment

Y2 - 8 November 2016 through 8 November 2016

ER -

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

Abstract

Workshop

ASJC Scopus subject areas

Other files and links

Fingerprint

Cite this