ATVA 2025
Mon 27 - Fri 31 October 2025 Bengaluru, India

This program is tentative and subject to change.

Tue 28 Oct 2025 09:30 - 10:30 at InvitedTalk room - Invited Talk 1 Chair(s): Alex Potanin

Viper is a verification infrastructure that facilitates the development of automated verifiers based on separation logic. Viper consists of the Viper intermediate language and two backend verifiers based on symbolic execution and verification condition generation, respectively. It has been used to build over a dozen program verifiers that translate verification problems in Go, Java, Python, Rust, and many others, into the Viper language and automate verification using the Viper backends. In this talk, we summarize the core ideas behind Viper, give an overview of its applications, and explain our principles for evolving the system.

This program is tentative and subject to change.

Tue 28 Oct

Displayed time zone: Chennai, Kolkata, Mumbai, New Delhi change

09:30 - 10:30
Invited Talk 1Invited Talks at InvitedTalk room
Chair(s): Alex Potanin Australian National University

(Joint APLAS-ATVA Invited Talk)

09:30
60m
Talk
15 Years of Viper: Building and Evolving a Verification Infrastructure (Joint APLAS-ATVA Invited Talk)
Invited Talks
Peter Müller ETH Zurich