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

Publikation: Konference artikel i Proceeding eller bog/rapport kapitel › Konferencebidrag i proceedings › Forskning › 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.

Originalsprog	Engelsk
Titel	NASA Formal Methods Third International Symposium, NFM 2011, Pasadena, CA, USA, April 18-20, 2011. Proceedings
Redaktører	Mihaela Bobaru, Klaus Havelund, Gerard J. Holzmann, Rajeev Joshi
Antal sider	7
Vol/bind	6617
Forlag	Association for Computing Machinery
Publikationsdato	6 apr. 2011
Sider	518-524
ISBN (Trykt)	978-3-642-20397-8
ISBN (Elektronisk)	978-3-642-20397-8
DOI	https://doi.org/10.1007/978-3-642-20398-5_42
Status	Udgivet - 6 apr. 2011

Emneord

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

Adgang til dokumentet

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

StoryAccepteret manuskript, 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)
Danmarks Frie Forskningsfond
01/03/2009 → 30/06/2013
Projekter: Projekt › Forskning

Citationsformater

Mehnert, H. (2011). Kopitiam: Modular Incremental Interactive Full Functional Static Verification of Java Code. I M. Bobaru, K. Havelund, G. J. Holzmann, & R. Joshi (red.), NASA Formal Methods Third International Symposium, NFM 2011, Pasadena, CA, USA, April 18-20, 2011. Proceedings (Bind 6617, s. 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. i M Bobaru, K Havelund, GJ Holzmann & R Joshi (red), NASA Formal Methods Third International Symposium, NFM 2011, Pasadena, CA, USA, April 18-20, 2011. Proceedings. bind 6617, Association for Computing Machinery, s. 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. red. / Mihaela Bobaru; Klaus Havelund; Gerard J. Holzmann; Rajeev Joshi. Bind 6617 Association for Computing Machinery, 2011. s. 518-524.

Publikation: Konference artikel i Proceeding eller bog/rapport kapitel › Konferencebidrag i proceedings › Forskning › 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

Emneord

Adgang til dokumentet

Fingeraftryk

Projekter

ToMeSo: Tools and Methods for Scalable Software Verifications

Citationsformater