3.2 Verification & Logic Engine

[Mathnerd314]

Function: Integrates with the abstract interpreter for verification of safety and temporal properties over the IR; also provides invariant checking between components that ensures contracts are maintained and cleans up IR when needed. Configurable and modular checking of safety and temporal properties over IR, similar in spirit to CPAchecker but extended. arxiv

Inputs

• Verification-ready IR (post-normalization/partial evaluation).
• Properties: safety, temporal formulas (including μ-calculus-style), concurrency properties. di.ens- assertions, bounds, finalizers, reachability, termination, dead code, security/safety properties, deadlock/race conditions using memory model and concurrency model

Processing

• Integrate logic engine and term rewriting to drive choice and guard evaluation.
• Represent each abstract domain/analysis as a Configurable Program Analysis (CPA).
• Run configurable reachability over combinations of CPAs, maintaining an Abstract Reachability Graph (ARG). arxiv
• Extend to handle mu-modal temporal logic (e.g., via automata-based constructions or fixpoint computations). en.wikipedia
• Concurrent and incremental analysis

Outputs

• Verdict: safe/unsafe/unknown.
• Counterexamples or proofs.
• Result value or exception for (\mathrm{run}(p,d)).
• Profiling traces (if enabled).
• Residual programs (p_x) with static parts inlined and removed.
• Specialized hot-loop versions for JIT (via compiler).

Key references

• CPAchecker and CPA framework. github
• Abstract interpretation for verification. di.ens
• Partial evaluation and Futamura projections. gist.github