File(s) not publicly available
About Hoare logics for higher-order store
No description supplied
History
Publication status
- Published
ISSN
0302-9743Publisher
SpringerExternal DOI
Volume
3580Pages
12.0Presentation Type
- paper
Event name
32nd International Colloquium on Automata, Languages and Programming Languages (ICALP), LNCSEvent location
LisbonEvent type
conferenceISBN
3-540-27580-0Department affiliated with
- Informatics Publications
Notes
Originality: discusses a new program logic for a language with general updatable code pointers; can deal with recursion through the store. Rigour: denotational model and soundness proof using results about existence of recursive predicates, Significance/Impact: provides the first deduction rule for "recursion through the store". It allows one to do formal reasoning on languages that use code pointers. This is e.g. used in device drivers written in C. Hongseok Yang (EPSRC advanced research fellow) investigates this and a joint co-operation with him has been started. It has spawned further research on new logics for object-oriented languages that implicitly use code pointers (project proposal in preparation). Impact: it may lead to program logics for languages with code pointers like C or even languages with advanced features that can be modeled by code pointers (for example aspect-oriented languages or dynamic class loading). Birkedal (Copenhagen) and Yang (Queen Mary) have been interested and are now collaborating with us. Outlet/citations: ICALP is a top long running (over 32 years) international conference and Track B had < 32% acceptance rate that year.Full text available
- No
Peer reviewed?
- Yes
Editors
L Monteior, L Caires, C Palamidessi, GF Italiano, M YungLegacy Posted Date
2012-02-06Usage metrics
Categories
No categories selectedKeywords
Licence
Exports
RefWorks
BibTeX
Ref. manager
Endnote
DataCite
NLM
DC