Interactive verification of concurrent systems using symbolic execution

Issue title: Practical Aspects of Automated Reasoning

Article type: Research Article

Authors: Bäumler, Simon | Balser, Michael | Nafz, Florian | Reif, Wolfgang | Schellhorn, Gerhard

Affiliations: Lehrstuhl für Softwaretechnik und Programmiersprachen, Universität Augsburg, D-86135 Augsburg, Germany. E-mails: {baeumler, balser, nafz, reif, schellhorn}@informatik.uni-augsburg.de

Note: [] Coresponding author. E-mail: [email protected].

Abstract: This paper presents an interactive proof method for the verification of temporal properties of concurrent systems based on symbolic execution. Symbolic execution is a well known and very intuitive strategy for the verification of sequential programs. We have carried over this approach to the interactive verification of arbitrary linear temporal logic properties of (infinite state) parallel programs. The resulting proof method is very intuitive to apply and can be automated to a large extent. It smoothly combines first-order reasoning with reasoning in temporal logic. The proof method has been implemented in the interactive verification environment KIV and has been used in several case studies.

Keywords: Temporal logic, interactive verification, compositional reasoning, theorem prover

DOI: 10.3233/AIC-2010-0458

Journal: AI Communications, vol. 23, no. 2-3, pp. 285-307, 2010