Kopitiam: Modular Incremental Interactive Full Functional Static Verification of Java Code

Hannes Mehnert

doi:10.1007/978-3-642-20398-5_42

Kopitiam: Modular Incremental Interactive Full Functional Static Verification of Java Code

Hannes Mehnert

Research output: Conference Article in Proceeding or Book/Report chapter › Article in proceedings › Research › peer-review

Abstract

WearedevelopingKopitiam,atooltointeractivelyprovefull functional correctness of Java programs using separation logic by inter- acting with the interactive theorem prover Coq. Kopitiam is an Eclipse plugin, enabling seamless integration into the workflow of a developer. Kopitiam enables a user to develop proofs side-by-side with Java pro- grams in Eclipse.

Original language	English
Title of host publication	NASA Formal Methods Third International Symposium, NFM 2011, Pasadena, CA, USA, April 18-20, 2011. Proceedings
Editors	Mihaela Bobaru, Klaus Havelund, Gerard J. Holzmann, Rajeev Joshi
Number of pages	7
Volume	6617
Publisher	Association for Computing Machinery
Publication date	6 Apr 2011
Pages	518-524
ISBN (Print)	978-3-642-20397-8
ISBN (Electronic)	978-3-642-20397-8
DOIs	https://doi.org/10.1007/978-3-642-20398-5_42
Publication status	Published - 6 Apr 2011

Keywords

Separation Logic
Interactive Theorem Prover
Functional Correctness
Eclipse Plugin
Java Program Verification

Access to Document

10.1007/978-3-642-20398-5_42

StoryAccepted author manuscript, 186 KB

http://www.springerlink.com/content/y548128404v64584/

ToMeSo: Tools and Methods for Scalable Software Verifications
Sestoft, P. (CoI), Birkedal, L. (PI), Mehnert, H. (CoI), Jensen, J. B. (CoI), Bengtson, J. (CoI), Thamsborg, J. J. (CoI), Hartmann Jensen, M. (CoI), Sieczkowski, F. (CoI), Mehnert, H. (CoI) & Svendsen, K. (CoI)
Independent Research Fund Denmark
01/03/2009 → 30/06/2013
Project: Research

Cite this

Mehnert, H. (2011). Kopitiam: Modular Incremental Interactive Full Functional Static Verification of Java Code. In M. Bobaru, K. Havelund, G. J. Holzmann, & R. Joshi (Eds.), NASA Formal Methods Third International Symposium, NFM 2011, Pasadena, CA, USA, April 18-20, 2011. Proceedings (Vol. 6617, pp. 518-524). Association for Computing Machinery. https://doi.org/10.1007/978-3-642-20398-5_42

@inproceedings{9c1fa04271db4399a09b3867987104a3,

title = "Kopitiam: Modular Incremental Interactive Full Functional Static Verification of Java Code",

abstract = "WearedevelopingKopitiam,atooltointeractivelyprovefull functional correctness of Java programs using separation logic by inter- acting with the interactive theorem prover Coq. Kopitiam is an Eclipse plugin, enabling seamless integration into the workflow of a developer. Kopitiam enables a user to develop proofs side-by-side with Java pro- grams in Eclipse.",

keywords = "Separation Logic, , Interactive Theorem Prover, , Functional Correctness, , Eclipse Plugin, , Java Program Verification, Separation Logic, , Interactive Theorem Prover, , Functional Correctness, , Eclipse Plugin, , Java Program Verification",

author = "Hannes Mehnert",

note = "@incollection {springerlink:10.1007/978-3-642-20398-5_42, author = {Mehnert, Hannes}, affiliation = {IT University of Copenhagen, 2300 K{\o}benhavn S, Denmark}, title = {Kopitiam: Modular Incremental Interactive Full Functional Static Verification of Java Code}, booktitle = {NASA Formal Methods}, series = {Lecture Notes in Computer Science}, editor = {Bobaru, Mihaela and Havelund, Klaus and Holzmann, Gerard and Joshi, Rajeev}, publisher = {Springer Berlin / Heidelberg}, isbn = {978-3-642-20397-8}, keyword = {Computer Science}, pages = {518-524}, volume = {6617}, url = {http://dx.doi.org/10.1007/978-3-642-20398-5_42}, note = {10.1007/978-3-642-20398-5_42}, year = {2011} ",

year = "2011",

month = apr,

day = "6",

doi = "10.1007/978-3-642-20398-5_42",

language = "English",

isbn = "978-3-642-20397-8",

volume = "6617",

pages = "518--524",

editor = "Mihaela Bobaru and Klaus Havelund and Holzmann, {Gerard J.} and Rajeev Joshi",

booktitle = "NASA Formal Methods Third International Symposium, NFM 2011, Pasadena, CA, USA, April 18-20, 2011. Proceedings",

publisher = "Association for Computing Machinery",

address = "United States",

}

Mehnert, H 2011, Kopitiam: Modular Incremental Interactive Full Functional Static Verification of Java Code. in M Bobaru, K Havelund, GJ Holzmann & R Joshi (eds), NASA Formal Methods Third International Symposium, NFM 2011, Pasadena, CA, USA, April 18-20, 2011. Proceedings. vol. 6617, Association for Computing Machinery, pp. 518-524. https://doi.org/10.1007/978-3-642-20398-5_42

Kopitiam: Modular Incremental Interactive Full Functional Static Verification of Java Code. / Mehnert, Hannes.
NASA Formal Methods Third International Symposium, NFM 2011, Pasadena, CA, USA, April 18-20, 2011. Proceedings. ed. / Mihaela Bobaru; Klaus Havelund; Gerard J. Holzmann; Rajeev Joshi. Vol. 6617 Association for Computing Machinery, 2011. p. 518-524.

Research output: Conference Article in Proceeding or Book/Report chapter › Article in proceedings › Research › peer-review

TY - GEN

T1 - Kopitiam: Modular Incremental Interactive Full Functional Static Verification of Java Code

AU - Mehnert, Hannes

N1 - @incollection {springerlink:10.1007/978-3-642-20398-5_42, author = {Mehnert, Hannes}, affiliation = {IT University of Copenhagen, 2300 København S, Denmark}, title = {Kopitiam: Modular Incremental Interactive Full Functional Static Verification of Java Code}, booktitle = {NASA Formal Methods}, series = {Lecture Notes in Computer Science}, editor = {Bobaru, Mihaela and Havelund, Klaus and Holzmann, Gerard and Joshi, Rajeev}, publisher = {Springer Berlin / Heidelberg}, isbn = {978-3-642-20397-8}, keyword = {Computer Science}, pages = {518-524}, volume = {6617}, url = {http://dx.doi.org/10.1007/978-3-642-20398-5_42}, note = {10.1007/978-3-642-20398-5_42}, year = {2011}

PY - 2011/4/6

Y1 - 2011/4/6

N2 - WearedevelopingKopitiam,atooltointeractivelyprovefull functional correctness of Java programs using separation logic by inter- acting with the interactive theorem prover Coq. Kopitiam is an Eclipse plugin, enabling seamless integration into the workflow of a developer. Kopitiam enables a user to develop proofs side-by-side with Java pro- grams in Eclipse.

AB - WearedevelopingKopitiam,atooltointeractivelyprovefull functional correctness of Java programs using separation logic by inter- acting with the interactive theorem prover Coq. Kopitiam is an Eclipse plugin, enabling seamless integration into the workflow of a developer. Kopitiam enables a user to develop proofs side-by-side with Java pro- grams in Eclipse.

KW - Separation Logic

KW - Interactive Theorem Prover

KW - Functional Correctness

KW - Eclipse Plugin

KW - Java Program Verification

KW - Separation Logic

KW - Interactive Theorem Prover

KW - Functional Correctness

KW - Eclipse Plugin

KW - Java Program Verification

U2 - 10.1007/978-3-642-20398-5_42

DO - 10.1007/978-3-642-20398-5_42

M3 - Article in proceedings

SN - 978-3-642-20397-8

VL - 6617

SP - 518

EP - 524

BT - NASA Formal Methods Third International Symposium, NFM 2011, Pasadena, CA, USA, April 18-20, 2011. Proceedings

A2 - Bobaru, Mihaela

A2 - Havelund, Klaus

A2 - Holzmann, Gerard J.

A2 - Joshi, Rajeev

PB - Association for Computing Machinery

ER -

Kopitiam: Modular Incremental Interactive Full Functional Static Verification of Java Code

Abstract

Keywords

Access to Document

Fingerprint

Projects

ToMeSo: Tools and Methods for Scalable Software Verifications

Cite this