Software Research Seminar

  • Gates Hillman 4215 and Panopto
  • In Person and LiveStream ET
  • Ph.D. Students
  • Ph.D. Program in Software Engineering
  • Institute for Sofware Research, Carnegie Mellon University

►  Jenna Wise , Ph.D. Student in Software Engineering
      Gradual Viper: Symbolic Execution for Efficient Gradual Verification

— Current static verification techniques do not provide good support for incrementality, making it difficult for developers to focus on specifying and verifying the properties and components that are most important. Dynamic verification approaches support incrementality, but cannot provide static guarantees. To bridge this gap, prior work proposed gradual verification, which supports incrementality by allowing every assertion to be complete, partial, or omitted, and provides sound verification that smoothly scales from dynamic to static checking. Our OOPSLA’20 paper extended gradual verification to programs that manipulate recursive, mutable data structures on the heap. As follow-up, we built a working gradual verifier based on this work, and I present the verifier’s design in this talk. The verifier is implemented on top of the Viper static verifier and supports the C0 programming language. The C0 language is a safer, smaller subset of C taught in introductory CS courses at CMU. Finally, I conclude the talk with my short-term plans to evaluate our tool, which includes a case study on web browser JIT code.

►  Ryan Wagner, Ph.D. Student in Software Engineering

For More Information, Please Contact: