PV Studio

PV Studio untitled.pv

New model
Open project…Ctrl+O
Save projectCtrl+S
Export for ProVerif (.pv)Ctrl+E
Examples from ProVerif 2.05

UndoCtrl+Z
RedoCtrl+Shift+Z
Add role
Duplicate blockCtrl+D
Rename everywhereF2
Delete selectionDel
Pair messages automatically

Diagram
Diagram and code
Code
Zoom in
Zoom out
Fit diagram
Show messages
Light or dark theme
Engine settings…

Keyboard shortcuts
ProVerif manual
About PV Studio

VerifyF5
Stop verification
Engine settings…

Declarations 0

Diagram

Code untitled.pv Read only OK

Goal Click a step to show the block and the line that executed it.

No attack trace yet. Verify the model: when a goal is false, ProVerif's attack is drawn here.

Inspector

ProVerif engine

ProVerif 2.05 runs in your browser, compiled to JavaScript. Nothing is uploaded. It runs in a web worker.

Memory limit (MB)

The run stops when the clauses generated by ProVerif exceed this estimate. 0 means no limit.

Time limit (seconds)

0 means no limit. Runs in the page itself cannot be interrupted.

Extra ProVerif options

Keyboard shortcuts

`Ctrl` `Z`	Undo
`Ctrl` `Shift` `Z`	Redo
`Ctrl` `S`	Save the project
`Ctrl` `O`	Open a project
`Ctrl` `E`	Export for ProVerif (.pv)
`F5`	Verify
`F2`	Rename the selected declaration or role everywhere
`Ctrl` `D`	Duplicate the selected block
`Del`	Delete the selection
`Esc`	Clear the selection
`Ctrl` + wheel	Zoom the diagram

π PV Studio

A visual editor for ProVerif models. Each block is one construct of ProVerif's typed pi calculus; the diagram is exported as a .pv file and verified in your browser.

Demo version. Roberto Metere, University of York.

The verifier is ProVerif 2.05 by Bruno Blanchet, Vincent Cheval and Marc Sylvestre, © INRIA, CNRS, compiled to JavaScript with js_of_ocaml and distributed under the GNU GPL v2 or later (engine/LICENSE-ProVerif.txt). The examples come from the ProVerif distribution.