Tony's Wiki

Software Verification in muCLP

5 min read

The logic

Formulas

  • support any background theory
  • mu to the limit --- Bot
  • nu to the limit --- Top
  • Orders of nested recursion (in equational form) matters

Partial Correctness

{P} c {Q} encoded as forall i o x, R(x,i,o) /\ terminal_state(...) --> Q(y) where R is describing the set of reachable states (inductively), and will include the pre-condition description

Other VC: based on the weakest precondition (coinductively), and show P(...) ==> WP⇐- WP is the safe states enough to reach the final state

Total Correctness

[P] c [Q]: always terminates and satisfied the resulting state

  • WP-style: we use the inductive operator

Partial Correctness + Finitely branching angelic non-determinism

  • read_bool()
  • there exists an execution of the program such that post condition is satisfied

Non-termination can be encoded as : {P} c {False}

Partial Correctness + Infinitely branching angelic non-determinism

  • read_int()
  • can be just encoded as exists (x:int) . .....

Benefits

  • modular spec ←> program
  • closed under complement neg mu ... = nu. neg ...
    • termination ←> non-termination problem for free

Example: modal mu-calculus model checking

from SAS2019

  • modal mu-calculus model checking

Example: Cost analysis

ICFP21 work:

use CPS transformation to perform expected cost analyis

  • expected cost of f = results of f' (...) (\x. 0) HFL = (generlized) higher-order (in the sense that continuation introduces higher order function) fixed point logic

POPL23 work:

generalizes:

  • CPS eqv WP holds for various kinds of effectful programs

Reduce to a constraint-solving problem

  • Limitations of CHC

    • limit to linear-time safety properties
      • non liveness
      • non branching (angelic non-det)

  • extend to pCSP: predicate constraint solving problem

    • read_bool()
    • allow disjunction on left position (representing angelic non-det)

  • pfwCSP: with Functional and Well-founded predicates

    • to handle infinitary branching
      • read_int()
    • allow total + well-foundedness / functionals in the clauses
      • use functional predicate to encode existentials
      • well-founded relation for termination of the loop
    • applicable to (infinite) branching + liveness / safety

  • to support HFL:

    • extend CHC with
      • fixed point fix
      • integration

The reduction: muCLP to pfwCSP

For greatest fixed-point

  • idea: use Knaster-tarski theorem
    • an under approximation of the greatest fixed point

For Least fixed-point:

|= F(S) => S
-------------
|= mu. F => S

No longer an underapproximation, idea, find G. s.t. nu. G <=> mu . G => mu F.

The need for well-founded predicates (inserting guards)

|= S => G(S)
------------
|= S => nu. G

question sound and complete?

Reduction from HFL to CHC[adm, ∫]

  • refinement type (for higher order arguments) + HFL formula

    • infer simple types
    • generate template for refinement types
    • generate CHC constraints for refinement type system

  • key typing rule for fixed points (à la type system)

    • By scott induction
      • required admissibility - to ensure soundness

Counterexample guided synthesis

expectation: general solution form can be inductively learned + deductive verified

~ online supervised learning

  • Adapt ML models to improve learner heuristics

Cyclic-proof search for validity checking

Software model-checking ←> CLP validity / CHC SAT problem software model-checking algorithms = proof search heuristics ~ partially constructed proofs

  • finding appropriate cut formula ~~~~ cyclic proof search

Software model-checking

Algorithmic analysis of execution of a program

e.g. safety verification of a while program with possibly infinite set of states + inital + bad +transition relation

witness of safety given by an inductive invariant

  • P closed under transition
  • no bad states
  • all initial states

⇒ system never reaches a bad state

  • easy to check, need clever ways to find

Logic formalization

find least solution mu. R for P and show mu . R ==> neg BadState Due to martin Lof, we can verify the above safety proposition but only applicable when mu .R is found

so, we use a cyclic proof system:

  • Cycle ~~ use of induction hypothesis

Key observations

Techniques used in software model checking can be backed up by cyclic proof search strategies (e.g. derived rules …)

Heruristic 1

  • Symbolic execution can be interpreted as nu . R proof serch
  • ⇒ Bounded model checking
    • trying to fit the shape of unproved sequents into the form \Phi(x) |- \nu. S(x) is just trying to find cyclic proofs after k-th iteration of symbolic execution (we have k induction hypothesis available compared to plain ones)

Heruristic 2: More aggressive use of (Cut)

Let the cut formula be the strongest such that

  • predicate abstraction

Heruristic 3/4: Tentatively choose T as the cut formula, and when the proof attempt fails, strengthen the cut formulas

  • Replace the cut formula phi_i with fresh constraints Qi (to be solved) and
  • interpolation

Heuristic 5: strengthening, keep as many cut formulas unchanged as possible

maximally conservative

PLDI 2024, MuCyc

Benchmark: https://chc-comp.github.io/2025/CHC-COMP%202025%20Report%20-%20SPIN.pdf

Relational Program Verification

verify ADT with algebraic specs http://lfp.dip.jp/rcaml/

relational:

  • proving program equivalence
  • functional (input/output) refinement relation
    • useful for transferring properties and proofs

needs integration of SMT + CHC solvers

  • limited ability to discover lemmas

Game solving for validity checking

A Primal-Dual Perspective on Program Verification Algorithms

  • based on the idea of lagrangian duality (as seen in optimization)
  • for program verification
L : X \times Y -> Z

sup_y inf_x L(x, y) <= inf_x sup_y L(x, y)

X - space of possible (partial, abstract) counterexamples

Y - space of possible (partial, abstract) proofs

“

Graph View