Skip to content (access key 's')
Logo of Technion
Logo of CS Department
Logo of CS4People
Events

The Taub Faculty of Computer Science Events and Talks

Automata over Infinite Data Domains: Learnability and Applications in Program Verification and Repair
event speaker icon
Hadar Frenkel (Ph.D. Thesis Seminar)
event date icon
Tuesday, 02.03.2021, 17:00
event location icon
Zoom Lecture: 97090529670
For password to lecture, please contact: hfrenkel@cs.technion.ac.il
event speaker icon
Advisor: 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.