Viper verification stage

• (With Prusti server only) Send VIR to the server.
• VIR is encoded into Viper.
• The Viper verifier is called and the results are obtained.
• (With Prusti server only) Send verification results back to the client.

Prusti server

Prusti server is an optional component of Prusti that can significantly reduce verification times by running a background process. The background process keeps an instance of JVM open, which is what Viper backends use to perform verification of Viper code. With the server enabled, a client only needs to send VIR to the server and receive the results once they are ready.

• prusti-viper/src/verifier.rs - Verifier::verify - verification with the server.
• prusti-viper/src/verifier.rs - Verifier::verify - verification without the server.

Encoding VIR to Viper

As noted in the previous section, VIR is an intermediate representation separate from Viper AST. In this step the encoding from one to the other is performed.

• prusti-server/src/verifier_runner.rs - VerifierRunner::verify - call to to_viper.
• prusti-common/src/vir/to_viper.rs - implementation of ToViper trait.