PropertyValue
?:abstract
  • Reduction to the satisfiablility problem for constrained Horn clauses (CHCs) is a widely studied approach to automated program verification. The current CHC-based methods for pointer-manipulating programs, however, are not very scalable. This paper proposes a novel translation of pointer-manipulating Rust programs into CHCs, which clears away pointers and heaps by leveraging ownership. We formalize the translation for a simplified core of Rust and prove its correctness. We have implemented a prototype verifier for a subset of Rust and confirmed the effectiveness of our method.
is ?:annotates of
?:creator
?:doi
  • 10.1007/978-3-030-44914-8_18
?:doi
?:externalLink
?:journal
  • Programming_Languages_and_Systems
?:license
  • cc-by
?:pdf_json_files
  • document_parses/pdf_json/ddf6349b0cf4e9ff2cb1d4b838b960f53b5cd529.json
?:pmcid
?:publication_isRelatedTo_Disease
?:sha_id
?:source
  • PMC
?:title
  • RustHorn: CHC-Based Verification for Rust Programs
?:type
?:year
  • 2020-04-18

Metadata

Anon_0  
<http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <http://purl.org/net/provenance/ns#DataItem>
<http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <http://www.w3.org/2004/03/trix/rdfg-1/Graph>
<http://xmlns.com/foaf/0.1/primaryTopic> <https://research.tib.eu/covid-19/entity/rft1vbkm>
<http://xmlns.com/foaf/0.1/topic> Anon_0
<http://www.ontologydesignpatterns.org/cp/owl/informationrealization.owl#realizes> <https://research.tib.eu/covid-19/data/entity/rft1vbkm>
<http://purl.org/net/provenance/ns#createdBy>
Anon_1   (more)
expand all