Interactive verification of concurrent systems using symbolic execution
Simon Bäumler, Michael Balser, Florian Nafz, Wolfgang Reif, Gerhard Schellhorn · AI Communications · 2010
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.