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 May

Displayed time zone: Osaka, Sapporo, Tokyo change

14:00 - 17:00
Constraint-based Relational and Temporal Verification
AiDL 2022
Hiroshi Unno University of Tsukuba; RIKEN AIP
Validating OCaml soundness by translation into Coq
AiDL 2022
Jacques Garrigue Nagoya University
Discussion (1)
AiDL 2022