דלג לתוכן (מקש קיצור 's')
Logo of Technion
Logo of CS Department
אירועים

אירועים

Automata over Infinite Data Domains: Learnability and Applications in Program Verification and Repair
event speaker icon
הדר פרנקל, הרצאה סמינריונית לדוקטורט
event date icon
יום שלישי, 2.3.2021, 17:00
event location icon
Zoom Lecture: 97090529670
For password to lecture, please contact: hfrenkel@cs.technion.ac.il
event speaker icon
מנחה:  Prof. Orna Grumberg and Dr. Sarai Sheinvald
We present automata over infinite data domains and their use in program verification and repair. In particular, we discuss assume-guarantee based verification, a compositional verification method that uses automata learning in order to modularly verify the correctness of a system. Then we present Assume-Guarantee-Repair (AGR) – a framework that verifies that a program satisfies a set of properties, and repairs the program in case the verification fails. We consider communicating programs – these are simple C-like programs, extended with synchronous communication actions over communication channels. We model these infinite-state systems using finite automata, and reduce the semantic problems in hand – satisfying complex specifications that also contain first-order constraints – to syntactic ones, namely membership and equivalence queries for regular languages.  
[בחזרה לאינדקס האירועים]