Skip to Main content Skip to Navigation
Preprints, Working Papers, ...

A Pragmatic Type System for Deductive Verification

Abstract : In the context of deductive verication, it is customary today to handle programs with pointers using either separation logic, dynamic frames, or explicit memory models. Yet we can observe that in numerous programs, a large amount of code ts within the scope of Hoare logic, provided we can statically control aliasing. When this is the case, the code correctness can be reduced to simpler verication conditions which do not require any explicit memory model. This makes verication conditions more amenable both to automated theorem proving and to manual inspection and debugging. In this paper, we devise a method of such static aliasing control for a programming language featuring nested data structures with mutable components. Our solution is based on a type system with singleton regions and eects, which we prove to be sound.
Document type :
Preprints, Working Papers, ...
Complete list of metadata

Cited literature [31 references]  Display  Hide  Download

https://hal.inria.fr/hal-01256434
Contributor : Jean-Christophe Filliâtre <>
Submitted on : Monday, February 1, 2016 - 10:24:14 AM
Last modification on : Friday, April 30, 2021 - 9:58:01 AM
Long-term archiving on: : Friday, November 11, 2016 - 9:08:23 PM

File

main (1).pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01256434, version 3

Citation

Jean-Christophe Filliâtre, Léon Gondelman, Andrei Paskevich. A Pragmatic Type System for Deductive Verification. 2016. ⟨hal-01256434v3⟩

Share

Metrics

Record views

678

Files downloads

510