About: Program Verification in the Presence of I/O

Not logged in : Login

(Sponging disallowed)

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

About: Program Verification in the Presence of I/O Goto Sponge NotDistinct Permalink

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

Attributes	Values
type	http://eprints.org/ontology/BookSectionEPrint http://eprints.org/ontology/EPrint Article Book Section
seeAlso	HTML Summary of #71298 Program Verification in the Presence of I/O
sameAs	Program Verification in the Presence of I/O
http://eprints.org/ontology/hasAccepted	Program Verification in the Presence of I/O (PDF)
http://eprints.org/ontology/hasDocument	Program Verification in the Presence of I/O (PDF) Program Verification in the Presence of I/O (Other) Program Verification in the Presence of I/O (Other) Program Verification in the Presence of I/O (Other) Program Verification in the Presence of I/O (Other) Program Verification in the Presence of I/O (Other)
dc:hasVersion	Program Verification in the Presence of I/O (PDF)
Title	Program Verification in the Presence of I/O
described by	https://demo.openlinksw.com/about/id/entity/https/www.cs.kent.ac.uk/people/staff/akj22/materials/CO644/export_kar_RDFN3.n3
Date	2018-08-15
Creator	Magnus O. Myreen Ramana Kumar Johannes Aman Pohjola Son Ho Hugo Férée Scott Owens
status	peer reviewed published
Publisher	Springer
abstract	Software veri?cation tools that build machine-checked proofs of functional correctness usually focus on the algorithmic content of the code. Their proofs are not grounded in a formal semantic model of the environment that the program runs in, or the program’s interaction with that environment. As a result, several layers of translation and wrapper code must be trusted. In contrast, the CakeML project focuses on endto-end veri?cation to replace this trusted code with veri?ed code in a cost-e?ective manner. In this paper, we present infrastructure for developing and verifying impure functional programs with I/O and imperative ?le handling. Specifically, we extend CakeML with a low-level model of ?le I/O, and verify a high-level ?le I/O library in terms of the model. We use this library to develop and verify several Unix-style command-line utilities: cat, sort, grep, di? and patch. The work?ow we present is built around the HOL4 theorem prover, and therefore all our results have machine-checked proofs.
Is Part Of	https://kar.kent.ac.uk/id/repository
Subject	QA 76 Software, computer programming,
list of authors	https://kar.kent.ac.uk/id/eprint/71298#authors
presented at	10th International Conference on Verified Software: Theories, Tools, and Experiments
is topic of	https://www.cs.kent.ac.uk/people/staff/akj22/materials/CO644/export_kar_RDFN3.n3
is primary topic of	HTML Summary of #71298 Program Verification in the Presence of I/O

Faceted Search & Find service v1.17_git149 as of Dec 03 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, 44 GB memory in use)
Data on this page belongs to its respective rights holders.
Virtuoso Faceted Browser Copyright © 2009-2024 OpenLink Software