A formal definition of JML in Coq and its application to runtime assertion checking

Metadata Label Value
Author(s): Lehner, Hermann
Publisher: ETH
Citation:

Lehner, Hermann. A formal definition of JML in Coq and its application to runtime assertion checking. ETH (2011). http://dx.doi.org/10.3929/ethz-a-006680049

Document Type: Doctoral and Habilitation Theses  
Documents: Abstract (156.56KB), Fulltext (1.61MB)

Detailed Information

Metadata Description
Title A formal definition of JML in Coq and its application to runtime assertion checking
Author(s) Lehner, Hermann
Publication Place Zürich
Publisher ETH
Publication Date 2011
Notes Diss., Eidgenössische Technische Hochschule ETH Zürich, Nr. 19971, 2011
Language English
DOI http://dx.doi.org/10.3929/ethz-a-006680049
Subject(s) Software
Keyword(s) SPECIFICATION LANGUAGES
PROGRAMMING LANGUAGES
VERIFICATION
COMPUTING TIME
RUNNING TIME
COMPUTER SYSTEMS
Description File Name MIME Type Size
Abstract   eth-4555-01.pdf application/pdf 156.56KB
Fulltext   eth-4555-02.pdf application/pdf 1.61MB
Abstract Views and Downloads
Views 38  abstracts
Downloads 76  downloads

Abstract Views and Downloads by Country
Views abstracts
Downloads 24  downloads
Switzerland Views abstracts
Downloads 13  downloads
China Views 12  abstracts
Downloads downloads
Germany Views abstracts
Downloads downloads
Japan Views abstracts
Downloads downloads
United States Views abstracts
Downloads downloads
Italy Views abstracts
Downloads downloads
United Kingdom Views abstracts
Downloads downloads
Brazil Views abstracts
Downloads downloads
Bulgaria Views abstracts
Downloads downloads
Denmark Views abstracts
Downloads downloads
Hungary Views abstracts
Downloads downloads
Malaysia Views abstracts
Downloads downloads
Peru Views abstracts
Downloads downloads
South Africa Views abstracts
Downloads downloads
France Views abstracts
Downloads downloads
Netherlands Views abstracts
Downloads downloads


E-Collection record created: Thu, 03 Nov 2011, 22:48:35 CET