15 Years of Viper: Building and Evolving a Verification Infrastructure (Joint APLAS-ATVA Invited Talk) (APLAS 2025 - Keynotes)

Mon 27 - Thu 30 October 2025 Bengaluru, India

Track

APLAS 2025 Keynotes

This program is tentative and subject to change.

Time Zone

The program is currently displayed in (GMT+05:30) Chennai, Kolkata, Mumbai, New Delhi.

Use conference time zone: (GMT+05:30) Chennai, Kolkata, Mumbai, New DelhiSelect other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.

Display full programSpecify a time band

Save

When

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

Abstract

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.