Cocktail II

M.G.J. Franssen

Cocktail II

M.G.J. Franssen

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

Abstract

Cocktail II is an interactive tool for deriving programs from specifications. Instead of verifying a program after it was constructed, Cocktail II aids the goal oriented derivation of a program. First, the user provides a pre- and postcondition. Then, the program to fill the gap between these condition is constructed by manually inserting statements between them. The tool computes the sub specifications of the new gaps, which can then be manually refined further. Finally, when a precondition of a gap implies its postcondition, the gap can be closed. Cocktail II also provides support for constructing the required proof. The program is complete when all gaps are closed.

Original language	English
Title of host publication	Proceedings of the 3rd International Workshop on Invariant Generation (WING 2010), July 21, 2010, Edinburgh, UK
Editors	A. Voronkov, L. Kovacs, N. Bjorner
Place of Publication	S.l.
Publisher	EasyChair
Pages	92-93
Publication status	Published - 2012
Event	conference; WING 2010 - Duration: 1 Jan 2012 → …

Publication series

Name	EPiC Series
Volume	1
ISSN (Print)	2040-557X

Conference

Conference	conference; WING 2010
Period	1/01/12 → …
Other	WING 2010

UN SDGs

This output contributes to the following UN Sustainable Development Goals (SDGs)

Cite this

@inproceedings{f7140423d71542b49fd66c4486eef400,

title = "Cocktail II",

abstract = "Cocktail II is an interactive tool for deriving programs from specifications. Instead of verifying a program after it was constructed, Cocktail II aids the goal oriented derivation of a program. First, the user provides a pre- and postcondition. Then, the program to fill the gap between these condition is constructed by manually inserting statements between them. The tool computes the sub specifications of the new gaps, which can then be manually refined further. Finally, when a precondition of a gap implies its postcondition, the gap can be closed. Cocktail II also provides support for constructing the required proof. The program is complete when all gaps are closed.",

author = "M.G.J. Franssen",

year = "2012",

language = "English",

series = "EPiC Series",

publisher = "EasyChair",

pages = "92--93",

editor = "A. Voronkov and L. Kovacs and N. Bjorner",

booktitle = "Proceedings of the 3rd International Workshop on Invariant Generation (WING 2010), July 21, 2010, Edinburgh, UK",

note = "conference; WING 2010 ; Conference date: 01-01-2012",

}

TY - GEN

T1 - Cocktail II

AU - Franssen, M.G.J.

PY - 2012

Y1 - 2012

N2 - Cocktail II is an interactive tool for deriving programs from specifications. Instead of verifying a program after it was constructed, Cocktail II aids the goal oriented derivation of a program. First, the user provides a pre- and postcondition. Then, the program to fill the gap between these condition is constructed by manually inserting statements between them. The tool computes the sub specifications of the new gaps, which can then be manually refined further. Finally, when a precondition of a gap implies its postcondition, the gap can be closed. Cocktail II also provides support for constructing the required proof. The program is complete when all gaps are closed.

AB - Cocktail II is an interactive tool for deriving programs from specifications. Instead of verifying a program after it was constructed, Cocktail II aids the goal oriented derivation of a program. First, the user provides a pre- and postcondition. Then, the program to fill the gap between these condition is constructed by manually inserting statements between them. The tool computes the sub specifications of the new gaps, which can then be manually refined further. Finally, when a precondition of a gap implies its postcondition, the gap can be closed. Cocktail II also provides support for constructing the required proof. The program is complete when all gaps are closed.

M3 - Conference contribution

T3 - EPiC Series

SP - 92

EP - 93

BT - Proceedings of the 3rd International Workshop on Invariant Generation (WING 2010), July 21, 2010, Edinburgh, UK

A2 - Voronkov, A.

A2 - Kovacs, L.

A2 - Bjorner, N.

PB - EasyChair

CY - S.l.

T2 - conference; WING 2010

Y2 - 1 January 2012

ER -

Cocktail II

Abstract

Publication series

Conference

UN SDGs

Fingerprint

Cite this