Program
Sunday, 28 March, 2021 (All times are in CEST).
The videos of the talks are available here.
| 8:55 - 9:00 | Welcome (Hossein Hojjat and Bishoksan Kafle) | |
| 9:00 - 10:00 | Invited talk: Naoki Kobayashi | |
| An Overview of the HFL Model Checking Project. [ slides , video ] | ||
| Session chair: Hossein Hojjat | ||
| 10:00 - 10:15 | Coffee Break | |
| Session I - Session chair: Daniel Neider | ||
| 10:15 - 10:45 | Stefan Hetzl and Johannes Kloibhofer | |
| A fixed-point theorem for Horn formula equations. [ slides ] | ||
| 10:45 - 11:15 | Isabel Garcia-Contreras, Jose F. Morales and Manuel V. Hermenegildo | |
| Incremental and Modular Context-sensitive Analysis. [ slides ] | ||
| 11:15 - 11:45 | Jerome Jochems | |
| Reducing Higher-order Recursion Scheme Equivalence to Coinductive Higher-order Constrained Horn Clauses. [ slides ] | ||
| 11:45 - 12:45 | Lunch Break | |
| Session II - Session chair: Steven Ramsay | ||
| 12:45 - 13:45 | Invited talk: Samir Genaim | |
| Termination analysis of programs with multiphase control-flow. [ slides , video ] | ||
| 13:45 - 14:15 | Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi and Maurizio Proietti | |
| Removing Algebraic Data Types from Constrained Horn Clauses Using Difference Predicates. [ slides , video ] | ||
| 14:15 - 14:30 | Coffee Break | |
| Session III - Session chair: Emanuele De Angelis | ||
| 14:30 - 15:00 | Bishoksan Kafle, John P. Gallagher, Manuel V. Hermenegildo, Maximiliano Klemen, Pedro Lopez-Garcia and Jose F. Morales | |
| Regular path clauses and their application in solving loops. [ slides ] | ||
| 15:00 - 15:30 | Fabian Zaiser and C.-H. Luke Ong | |
| The Extended Theory of Trees and Algebraic (Co)datatypes. [ slides ] | ||
| 15:30 - 16:00 | Hari Govind Vediramana Krishnan, YuTing Chen, Sharon Shoham and Arie Gurfinkel | |
| Global Guidance for Local Generalization in Model Checking. [ slides ] | ||
| 16:00 - 16:15 | Coffee Break | |
| Session IV - Session chair: He Zhu | ||
| 16:15 - 16:45 | Yurii Kostyukov, Dmitry Mordvinov and Grigory Fedyukovich | |
| Solving Constrained Horn Clauses over ADTs by Finite Model Finding. [ slides ] | ||
| 16:45 - 17:15 | Brendan Hall, Sarat Chandra Varanasi and Gopal Gupta | |
| Knowledge-Assisted Reasoning of Formal Model-Based System Engineering with Event Calculus and Goal-Directed Answer Set Programming. [ slides ] | ||
| 17:15 - 17:45 | Philipp Rümmer and Grigory Fedyukovich | |
| CHC-COMP 2021 Report. [ slides ] | ||
| 17:45 - 18:00 | Closing (Hossein Hojjat and Bishoksan Kafle) | |
| 18:00 - 18:30 | The future of HCVS (PCs and steering committee members only). |