Program

Sunday, 28 March, 2021 (All times are in CEST).


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).