.jpg)
LEAP
LEAP is a prototype theorem prover which aims the formal verification of temporal properties, both safety and liveness, of parametrized programs. In particular, LEAP is designed for the analysis of programs that manipulate concurrent data types that store both finite and infinite data.
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.
Open source software registration at US Copyright Office