• Όλες οι κατηγορίες
• Δημόσιες Ανακοινώσεις
• Διαλέξεις / Ημερίδες / Εκδηλώσεις
• Ομιλία Dr Νίκη Βάζου "Practical Program Verification with Refinement Types "

Ομιλία Dr Νίκη Βάζου "Practical Program Verification with Refinement Types "

• 1

• Συντάχθηκε 12-07-2024 08:47

  Ενημερώθηκε: -

  Τόπος: Λ - Κτίριο Επιστημών/ΗΜΜΥ, 145Π-42
  Έναρξη: 18/07/2024 17:00
  Λήξη: 18/07/2024 18:00

  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. 

  
  

  Σύνδεσμος εκδήλωσης

  ---

• 1