Proving Reachability-Logic Formulas Incrementally

Vlad Rusu 1 Andrei Arusoaie 1, 2
1 DREAMPAL - Dynamic Reconfigurable Massively Parallel Architectures and Languages
Inria Lille - Nord Europe, CRIStAL - Centre de Recherche en Informatique, Signal et Automatique de Lille (CRIStAL) - UMR 9189
Abstract : Reachability Logic (RL) is a formalism for defining the operational semantics of programming languages and for specifying program properties. As a program logic it can be seen as a language-independent alternative to Hoare Logics. Several verification techniques have been proposed for RL, all of which have a circular nature: the RL formula under proof can circularly be used as a hypothesis in the proof of another RL formula, or even in its own proof. This feature is essential for dealing with possibly unbounded repetitive behaviour (e.g., program loops). The downside of such approaches is that the verification of a set of RL formulas is monolithic, i.e., either all formulas in the set are proved valid, or nothing can be inferred about any of the formula's validity or invalidity. In this paper we propose a new, incremental method for proving a large class of RL formulas. The proposed method takes as input a given RL formula under proof (corresponding to a given program fragment), together with a (possibly empty) set of other valid RL formulas (e.g., already proved using our method), which specify sub-programs of the program fragment under verification. It then checks certain conditions are shown to be equivalent to the validity of the RL formula under proof. A newly proved formula can then be incrementally used in the proof of other RL formulas, corresponding to larger program fragments. The process is repeated until the whole program is proved. We illustrate our approach by verifying the nontrivial Knuth-Morris-Pratt string-matching program.
Type de document :
Communication dans un congrès
11th International Workshop on Rewriting Logic and its Applications, Apr 2016, Eindhoven, Netherlands. LNCS (to appear)
Liste complète des métadonnées

Littérature citée [25 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01282379
Contributeur : Pal Dream <>
Soumis le : jeudi 3 mars 2016 - 16:00:52
Dernière modification le : mercredi 25 avril 2018 - 15:43:24
Document(s) archivé(s) le : samedi 4 juin 2016 - 11:11:27

Fichier

paper.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01282379, version 1

Collections

Citation

Vlad Rusu, Andrei Arusoaie. Proving Reachability-Logic Formulas Incrementally. 11th International Workshop on Rewriting Logic and its Applications, Apr 2016, Eindhoven, Netherlands. LNCS (to appear). 〈hal-01282379〉

Partager

Métriques

Consultations de la notice

215

Téléchargements de fichiers

66