LEAP

LEAP receives as input an annotated program and a temporal specification. As output, it states whether the temporal specification holds under the assumption of an unbounded number of threads executing the input program. To accomplish this, in its core LEAP implements: - A collection of specialized deductive proof rules which reduce the verification problem to a finite collection of verification conditions, whose validity entails the satisfaction of the temporal specification by the parametrized system. - A set of decision procedures, which can automatically verify the validity of the previously generated verification conditions.