Loading...

Tutorial: Find Counterexample

474 views

Loading...

Loading...

Transcript

The interactive transcript could not be loaded.

Loading...

Rating is available when the video has been rented.
This feature is not available right now. Please try again later.
Published on Sep 18, 2013

This video is part of a tutorial series for the Theorem Prover KeYmaera.
http://symbolaris.com/info/KeYmaera.html
____________________________________________________

In this video, we show you how to use KeYmaera to find a counter example if the property you are trying to prove is not actually true.

When KeYmaera no longer thinks your property is true, it will stop applying rules automatically. In this case, you can click on the implication arrow to bring up the menu, then select Find Counterexample.

If KeYmaera is able to find a specific counter example, a pop-up window will display a set of variable values that cause your system to violate the property you're trying to prove.

Loading...

When autoplay is enabled, a suggested video will automatically play next.

Up next


to add this to Watch Later

Add to

Loading playlists...