File
Open .ivy spec...
Open Event Trace...
Save as...
Download current model
Save Analysis State...
Load Analysis State...
Save Invariant...
New Model
CTI
reachability
Mode
Induction
PDR
Concrete
Abstract
Bounded
Abstractor
top/bottom
concrete
propagate
propagate & conjectures
concept space
BMC
1
3
5
10
15
Check
Show Reachable
Reset Domain
Diagram Domain
isolate
Hide Tutorial
Sheet 1
Reachability Graph
Reachability Graph
Invariant
Check induction
Bounded check
Diagram
Weaken
Save Invariant...
Action
Recalculate all
Show reachable states
Details
Select a node or edge to see details
Concept graph
Concept graph
background grayscale slider
Conjecture
Undo
Redo
Gather
Bounded check
Minimize
Check sufficient
Check relative induction
Strengthen
Export
Action
Undo
Redo
PDR step
Concrete
Gather
Reverse
Path reach
Reach
Conjecture
Backtrack
Recalculate
Diagram
Remember
Export
View
Add relation
Relayout (dot)
State/relations
State/relations
State: 0
Relations to minimize
+
?
-
T
Relation
Editor
Editing:
(unsaved file)
x
Re-open last file
Sublime
Emacs-ish
Vim
keymap docs
◀
▶
↻
×
Job Control
x
danger: clear saved session data
Log
browser
remote
run in browser
No running jobs
The browser security model requires re-confirmation of the save path on disk when IvyWeb cannot locate an IndexedDB cached file handle.
Loading...
Cancel
Ready