This HTML5 document contains 29 embedded RDF statements represented using HTML+Microdata notation.

The embedded RDF content will be recognized by any processor of HTML5 Microdata.

Namespace Prefixes

PrefixIRI
dctermshttp://purl.org/dc/terms/
n12https://kar.kent.ac.uk/67658/
n2https://kar.kent.ac.uk/id/eprint/
wdrshttp://www.w3.org/2007/05/powder-s#
dchttp://purl.org/dc/elements/1.1/
n16http://purl.org/ontology/bibo/status/
rdfshttp://www.w3.org/2000/01/rdf-schema#
n9https://kar.kent.ac.uk/id/subject/
n6https://demo.openlinksw.com/about/id/entity/https/raw.githubusercontent.com/annajordanous/CO644Files/main/
n3http://eprints.org/ontology/
n14https://kar.kent.ac.uk/id/eprint/67658#
bibohttp://purl.org/ontology/bibo/
n15https://kar.kent.ac.uk/id/publication/
n13https://kar.kent.ac.uk/id/org/
rdfhttp://www.w3.org/1999/02/22-rdf-syntax-ns#
n20doi:10.1016/
owlhttp://www.w3.org/2002/07/owl#
n4https://kar.kent.ac.uk/id/document/
n17https://kar.kent.ac.uk/id/
xsdhhttp://www.w3.org/2001/XMLSchema#
n21https://demo.openlinksw.com/about/id/entity/https/www.cs.kent.ac.uk/people/staff/akj22/materials/CO644/
n8https://kar.kent.ac.uk/id/person/

Statements

Subject Item
n2:67658
rdf:type
bibo:Article n3:EPrint n3:ArticleEPrint bibo:AcademicArticle
rdfs:seeAlso
n12:
owl:sameAs
n20:j.jlamp.2017.09.004
n3:hasAccepted
n4:2227455
n3:hasDocument
n4:2228739 n4:2227455 n4:2658552 n4:2658549 n4:2658550 n4:2658551
dc:hasVersion
n4:2227455
dcterms:title
Formally verifying Exceptions for Low-level code with Separation Logic
wdrs:describedby
n6:export_kar_RDFN3.n3 n21:export_kar_RDFN3.n3
dcterms:date
2018-01
dcterms:creator
n8:ext-3218418859fa420516900947fe2c4db3 n8:ext-m.paviotti@kent.ac.uk
bibo:status
n16:peerReviewed n16:published
dcterms:publisher
n13:ext-f308aad1ef8f70546c3a197f104f2ad5
bibo:abstract
Exceptions in low-level architectures are implemented as synchronous interrupts: upon the execution of a faulty instruction the processor jumps to a piece of code that handles the error. Previous work has shown that assembly programs can be written, verified and run using higher-order separation logic. However, execution of faulty instructions is then specified as either being undefined or terminating with an error. In this paper, we study synchronous interrupts and show their usefulness by implementing a memory allocator. This shows that it is indeed possible to write positive specifications of programs that fault. All of our results are mechanised in the interactive proof assistant Coq.
dcterms:isPartOf
n15:ext-23522208 n17:repository
dcterms:subject
n9:QA76
bibo:authorList
n14:authors
bibo:volume
94