Proving Partial Correctness Beyond Programs

International audiencePartial 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