Email Gateway (Aug 18 2022 at 13:00): Email Gateway (Aug 18 2022 at 13:00):From: Burkhart Wolff <Burkhart.Wolff@lri.fr>
Dear all,
we are happy to announce the following paper:
Authors: Achim D. Brucker and Burkhart Wolff
Title: An Extensible Encoding of Object-oriented Data Models in
HOL with an Application to IMP++
Abstract:
We present an extensible encoding of object-oriented data
models into higher-order logic (HOL). Our encoding is
supported by a datatype package that leverages the use of
the shallow embedding technique to object-oriented
specification and programming languages. The package
incrementally compiles an object-oriented data model, i.e.,
a class model, to a theory containing object-universes,
constructors, accessor functions, coercions (casts) between
dynamic and static types, characteristic sets, and
co-inductive class invariants. The package is conservative,
i. e., all properties are derived entirely from constant
definitions, including the constraints over object
structures. As an application, we use the package for an
object-oriented core-language called IMP++, for which we
formally prove the correctness of a Hoare logic with
respect to a denotational semantics.
Comments and discussions are welcome!
Best regards,
Achim & bu
Bibtex-Entry:
@ARTICLE{brucker.ea:extensible:2008,
author = {Achim D. Brucker and Burkhart Wolff},
journal = {Journal of Automated Reasoning (JAR)},
language = {USenglish},
note = {Serge Autexier, Heiko Mantel, Stephan Merz, and Tobias
Nipkow (eds)},
pdf = {http://kisogawa.inf.ethz.ch/WebBIB/publications/papers/2008/0_brucker.ea-datatype-2007.pdf
},
title = {An Extensible Encoding of Object-oriented Data Models in
HOL with an Application to IMP++},
volume = {Selected Papers of the AVOCS-VERIFY Workshop 2006},
doi = {10.1007/s10817-008-9108-3},
pages = {219-249},
volume = 41,
number = {3--4},
year = 2008
}
Email Gateway (Aug 18 2022 at 13:36):From: Matthias Daum <md11@wjpserver.cs.uni-sb.de>
Dear all,
we are happy to announce the following paper:
Authors: Matthias Daum, Jan Dörrenbächer, and Burkhart Wolff
Title: Proving Fairness and Implementation Correctness
of a Microkernel Scheduler
In: Journal of Automated Reasoning, Springer
EE: <http://www.springerlink.com/content/m4142567605g74p5/>
Comments and discussions are welcome!
Best regards,
Matthias, Jan, and Burkhart.
Last updated: May 03 2024 at 12:27 UTC