Zobrazeno 1 - 9
of 9
pro vyhledávání: '"Hannes Mehnert"'
Autor:
Matthew Fairbairn, Hannes Mehnert, Tom Ridge, Michael J. A. Smith, Peter Sewell, Michael Norrish, Steve Bishop, Keith Wansbrough
Conventional computer engineering relies on test-and-debug development processes, with the behavior of common interfaces described (at best) with prose specification documents. But prose specifications cannot be used in test-and-debug development in
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::e46bdb0f32d4e913906cbc78c2fd2b71
Im Alltag der imperativen Programmierung mit JavaScript bringen ungeplante Programmänderungen die gewohnten Abstraktionsmechanismen mitunter an ihre Grenzen. In diesem Buch wird ein Einstieg in die funktionale Programmierung dargeboten, deren Ansatz
Publikováno v:
Lecture Notes in Computer Science ISBN: 9783319064093
The presence of aliasing makes modular verification of object-oriented code difficult. If multiple clients depend on the properties of an object, one client may break a property that others depend on. We have developed a modular verification approach
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::9e3487f4be8e151721afbcd913927c19
https://doi.org/10.1007/978-3-319-06410-9_34
https://doi.org/10.1007/978-3-319-06410-9_34
Publikováno v:
FTfJP@ECOOP
Mackay, J, Mehnert, H, Potanin, A, Groves, L & Cameron, N 2012, Encoding Featherweight Java with Assignment and Immutability using The Coq Proof Assistant . in FTfJP 12.Proceedings of the 14th Workshop on Formal Techniques for Java-like Programs . Association for Computing Machinery, pp. 11-19 . https://doi.org/10.1145/2318202.2318206
Mackay, J, Mehnert, H, Potanin, A, Groves, L & Cameron, N 2012, Encoding Featherweight Java with Assignment and Immutability using The Coq Proof Assistant . in FTfJP 12.Proceedings of the 14th Workshop on Formal Techniques for Java-like Programs . Association for Computing Machinery, pp. 11-19 . https://doi.org/10.1145/2318202.2318206
We develop a mechanized proof of Featherweight Java with Assignment and Immutability in the Coq proof assistant. This is a step towards more machine-checked proofs of a non-trivial type system. We used object immutability close to that of IGJ [9] . W
Autor:
Hannes Mehnert, Jonathan Aldrich
Publikováno v:
Mehnert, H & Aldrich, J 2012, ' Verification of Snapshotable Trees using Access Permissions and Typestate ', Lecture Notes in Computer Science, vol. 7304, pp. 187-201 . https://doi.org/10.1007/978-3-642-30561-0_14
Objects, Models, Components, Patterns ISBN: 9783642305603
TOOLS (50)
Objects, Models, Components, Patterns ISBN: 9783642305603
TOOLS (50)
We use access permissions and typestate to specify and ver- ify a Java library that implements snapshotable search trees, as well as some client code. We formalize our approach in the Plural tool, a sound modular typestate checking tool. We describe
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::f01365370699f512902fbb4f02470bbb
Publikováno v:
Verified Software: Theories, Tools, Experiments ISBN: 9783642277047
VSTTE
VSTTE
We use separation logic to specify and verify a Java program that implements snapshotable search trees, fully formalizing the specification and verification in the Coq proof assistant. We achieve local and modular reasoning about a tree and its snaps
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::a822637973d0fc4b7473dff3e85a75ed
https://doi.org/10.1007/978-3-642-27705-4_15
https://doi.org/10.1007/978-3-642-27705-4_15
Autor:
Hannes Mehnert
Publikováno v:
Lecture Notes in Computer Science ISBN: 9783642203978
NASA Formal Methods
NASA Formal Methods
We are developing Kopitiam, a tool to interactively prove full functional correctness of Java programs using separation logic by interacting with the interactive theorem prover Coq. Kopitiam is an Eclipse plugin, enabling seamless integration into th
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::1edcbb2812b08dbf056f62b2bcca296b
https://doi.org/10.1007/978-3-642-20398-5_42
https://doi.org/10.1007/978-3-642-20398-5_42
Autor:
Hannes Mehnert
Publikováno v:
Mehnert, H 2010, Extending Dylan's type system for better type inference and error detection . in ILC '10 Proceedings of the 2010 international conference on Lisp . Association for Computing Machinery, Reno/Tahoe, Nevada, USA, pp. 1-10 . https://doi.org/10.1145/1869643.1869645
ILC
ILC
Whereas dynamic typing enables rapid prototyping and easy experimentation, static typing provides early error detection and better compile time optimization. Gradual typing [26] provides the best of both worlds. This paper shows how to define and imp
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::74394d123dd1635993e47e79a15d8ac0
https://pure.itu.dk/ws/files/31634506/p1_mehnert.pdf
https://pure.itu.dk/ws/files/31634506/p1_mehnert.pdf
Autor:
Andreas Bogk, Hannes Mehnert
Publikováno v:
ILC
We present a domain specific language for manipulation of binary data, or structured byte sequences, as they appear in everyday applications such as networking or graphics file manipulation. Our DSL is implemented as an extension of the Dylan languag