FLOPS 2022
Tue 10 - Thu 12 May 2022 Online
Tue 10 May 2022 14:00 - 14:45 at 大講演室 - Day 1

In this talk, we present our recent and ongoing work on constraint-based approach to relational and temporal verification of infinite-state programs. We advocate a class of predicate Constraint Satisfaction Problems called pfwCSP that extends the well-studied class of Constrained Horn Clauses (CHCs) with non-Horn clauses, functionality, and well-foundedness constraints on predicate variables. We then present reductions from relational verification problems to pfwCSP that can handle hyperproperties beyond k-safety such as generalized non-interference and co-termination. Furthermore, we introduce a new class $\mu$CLP of constraint logic programs with arbitrarily nested inductive and co-inductive predicates that is capable of modularly encoding temporal verification problems such as termination/non-termination, LTL, CTL, and even the full modal $\mu$-calculus model checking. For automated verification, we present a reduction from $\mu$CLP to pfwCSP and a CEGIS-based constraint solver for pfwCSP.

#### Tue 10 MayDisplayed time zone: Osaka, Sapporo, Tokyo change

 14:00 - 17:00 Day 1AiDL 2022 at 大講演室 14:0045mTalk Constraint-based Relational and Temporal VerificationAiDL 2022Hiroshi Unno University of Tsukuba; RIKEN AIP 14:4545mTalk Validating OCaml soundness by translation into CoqAiDL 2022Jacques Garrigue Nagoya University 15:3090mMeeting Discussion (1)AiDL 2022