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

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

Namespace Prefixes

PrefixIRI
n6https://kar.kent.ac.uk/id/eprint/71298#
n17doi:10.1007/
dctermshttp://purl.org/dc/terms/
n2https://kar.kent.ac.uk/id/eprint/
n15https://kar.kent.ac.uk/71298/
wdrshttp://www.w3.org/2007/05/powder-s#
dchttp://purl.org/dc/elements/1.1/
n20http://purl.org/ontology/bibo/status/
n19https://kar.kent.ac.uk/id/subject/
rdfshttp://www.w3.org/2000/01/rdf-schema#
n18https://demo.openlinksw.com/about/id/entity/https/raw.githubusercontent.com/annajordanous/CO644Files/main/
n11http://eprints.org/ontology/
n10https://kar.kent.ac.uk/id/event/
bibohttp://purl.org/ontology/bibo/
n7https://kar.kent.ac.uk/id/org/
rdfhttp://www.w3.org/1999/02/22-rdf-syntax-ns#
owlhttp://www.w3.org/2002/07/owl#
n12https://kar.kent.ac.uk/id/document/
n13https://kar.kent.ac.uk/id/
xsdhhttp://www.w3.org/2001/XMLSchema#
n9https://demo.openlinksw.com/about/id/entity/https/www.cs.kent.ac.uk/people/staff/akj22/materials/CO644/
n4https://kar.kent.ac.uk/id/person/

Statements

Subject Item
n2:71298
rdf:type
n11:EPrint bibo:BookSection n11:BookSectionEPrint bibo:Article
rdfs:seeAlso
n15:
owl:sameAs
n17:978-3-030-03592-1_6
n11:hasAccepted
n12:3144757
n11:hasDocument
n12:3147868 n12:3147865 n12:3147866 n12:3147867 n12:3144788 n12:3144757
dc:hasVersion
n12:3144757
dcterms:title
Program Verification in the Presence of I/O
wdrs:describedby
n9:export_kar_RDFN3.n3 n18:export_kar_RDFN3.n3
dcterms:date
2018-08-15
dcterms:creator
n4:ext-s.a.owens@kent.ac.uk n4:ext-h.feree@kent.ac.uk n4:ext-12296c9a30183cb4cc601571a51da980 n4:ext-06533d5330887204a90aba4b527050a7 n4:ext-6bb34d61c501e2fd98104177a62113b0 n4:ext-3c571964eaafc3e0ec0d1dd0209239eb
bibo:status
n20:peerReviewed n20:published
dcterms:publisher
n7:ext-1c5ddec173ca8cdfba8b274309638579
bibo: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.
dcterms:isPartOf
n13:repository
dcterms:subject
n19:QA76
bibo:authorList
n6:authors
bibo:presentedAt
n10:ext-5bcd65e37a317e03300b699dda45d8da