Έμβλημα Πολυτεχνείου Κρήτης με τίτλο Σχολή Ηλεκτρολόγων Μηχανικών & Μηχανικών Υπολογιστών
Η Σχολή ΗΜΜΥ στο Facebook  Η Σχολή ΗΜΜΥ στο Youtube

SIGLE NEWS - DO NOT DELETE

18 July 2024 - "Practical Program Verification with Refinement Types " by Dr. Niki Vazou

18 July 2024, 17:00 Athens time, 145Π42

 

Who

Dr. Niki Vazou
Associate Research Professor at IMDEA Software Institute

 

When

18 July 2024, 17:00 Athens time, Science Building 145Π42

 

Title

 

Practical Program Verification with Refinement Types

 

Abstract

 

Refinement types decorate the types of a programming language with logical predicates to allow more expressive type specifications. Originally, refinement type based specifications were restricted to SMT decidable theories and allowed automatic “light” verification, for example properties like non-division by zero or in-bound indexing. In this talk, I will present an overview of refinement types and using Liquid Haskell as the prototype refinement type implementation, will discuss the features that make refinement types a practical verification technology. 


About the Speaker

Niki is an Associate Research Professor at IMDEA Software Institute. She received her Ph.D. at UC San Diego, where she co develop Liquid Haskell, a refinement type checker for Haskell programs. Since then, she works on both the theory of refinement typing and their applications to verify real world properties. For this research purpose, in 2022 she received the ERC Starting Grant CRETE. 

© Σχολή Ηλεκτρολόγων Μηχανικών & Μηχανικών Υπολογιστών 2014
Πολυτεχνείο Κρήτης