Skip to Main content Skip to Navigation
Conference papers

Proving Partial Correctness Beyond Programs

Vlad Rusu 1
1 DREAMPAL - Dynamic Reconfigurable Massively Parallel Architectures and Languages
CRIStAL - Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189, Inria Lille - Nord Europe
Abstract : Partial correctness is perhaps the most important functional property of algo-rithmic programs. It can be broadly stated as: on all terminating executions, a given relation holds between a program's inputs and outputs. It has been formalised in several logics, from, e.g, Hoare logics [1] to temporal logics [2]. Partial correctness is also a relevant property for any class of specification that has a notion of terminating execution. For example, communication protocols have both nonterminating executions (all messages are forever lost and resent) and terminating executions (all messages sent are properly received). Here, partial correctness may, for instance, require that on all terminating executions , the set of messages corresponding to the transmission of a given file are received and the reception of every message is acknowledged. How can one naturally specify such generic partial-correctness properties, and how can one verify them in a maximally trustworthy manner? One possibility would be to use Hoare logics, but that solution is not optimal because Hoare logics intrinsically require programs (as their deduction rules focus on how program-instructions modify logical predicates), and we are targeting systems specified in formalisms that are not programs but more abstract models, e.g., one more naturally specifies communication protocols in some version of state-transition systems. Another possibility is to state partial-correctness properties in temporal logic and to use a model checker to prove the temporal formula on a state-transition system specification. This is a better solution, since it stays at a model-abstraction level; however, as we are aiming at trustworthy verification, this is not satisfactory as even in case of a successful verification, one's trust in the result is limited as one does not get independently-checkable verification certificates. Moreover, model checkers are limited to essentially finite-state systems (perhaps up to some data abstraction), a limitation we want to avoid.
Complete list of metadata

Cited literature [21 references]  Display  Hide  Download

https://hal.inria.fr/hal-01627555
Contributor : Pal Dream <>
Submitted on : Thursday, November 2, 2017 - 12:21:46 AM
Last modification on : Friday, December 11, 2020 - 6:44:06 PM
Long-term archiving on: : Saturday, February 3, 2018 - 12:11:31 PM

File

from2017.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01627555, version 1

Citation

Vlad Rusu. Proving Partial Correctness Beyond Programs. FROM 2017 - Working Formal Methods Symposium, Jul 2017, Bucharest, Romania. pp.1-3. ⟨hal-01627555⟩

Share

Metrics

Record views

161

Files downloads

67