About: Formally verifying Exceptions for Low-level code with Separation Logic

Not logged in : Login

(Sponging disallowed)

Facets (new session)
Description
Metadata
Settings
- Rule:
- Inverse Functional Properties:
- "Same As":

About: Formally verifying Exceptions for Low-level code with Separation Logic Goto Sponge Distinct Permalink

An Entity of Type : bibo:AcademicArticle, within Data Space : linkeddata.uriburner.com:28898 associated with source document(s)

Attributes	Values
type	http://eprints.org/ontology/ArticleEPrint http://eprints.org/ontology/EPrint Article Academic Article
seeAlso	HTML Summary of #67658 Formally verifying Exceptions for Low-level code with Separation Logic
sameAs	Formally verifying Exceptions for Low-level code with Separation Logic
http://eprints.org/ontology/hasAccepted	Formally verifying Exceptions for Low-level code with Separation Logic (PDF)
http://eprints.org/ontology/hasDocument	Formally verifying Exceptions for Low-level code with Separation Logic (PDF) Formally verifying Exceptions for Low-level code with Separation Logic (Other) Formally verifying Exceptions for Low-level code with Separation Logic (Other) Formally verifying Exceptions for Low-level code with Separation Logic (Other) Formally verifying Exceptions for Low-level code with Separation Logic (Other) Formally verifying Exceptions for Low-level code with Separation Logic (Other)
dc:hasVersion	Formally verifying Exceptions for Low-level code with Separation Logic (PDF)
Title	Formally verifying Exceptions for Low-level code with Separation Logic
described by	https://demo.openlinksw.com/about/id/entity/https/raw.githubusercontent.com/annajordanous/CO644Files/main/export_kar_RDFN3.n3
Date	2018-01
Creator	Bengtson Jesper Marco Paviotti
status	peer reviewed published
Publisher	Elsevier
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.
Is Part Of	Journal of Logical and Algebraic Methods in Programming https://kar.kent.ac.uk/id/repository
Subject	QA 76 Software, computer programming,
list of authors	https://kar.kent.ac.uk/id/eprint/67658#authors
volume	94
is topic of	https://raw.githubusercontent.com/annajordanous/CO644Files/main/export_kar_RDFN3.n3
is primary topic of	HTML Summary of #67658 Formally verifying Exceptions for Low-level code with Separation Logic

Faceted Search & Find service v1.17_git144 as of Jul 26 2024

Alternative Linked Data Documents: iSPARQL | ODE Content Formats:

RDF

ODATA

Microdata

About

OpenLink Virtuoso version 08.03.3331 as of Aug 25 2024, on Linux (x86_64-ubuntu_noble-linux-glibc2.38-64), Single-Server Edition (378 GB total memory, 37 GB memory in use)
Data on this page belongs to its respective rights holders.
Virtuoso Faceted Browser Copyright © 2009-2024 OpenLink Software