Verify safety of StrSearcher (Challenge 21) - #538

Open

jrey8343 wants to merge 11 commits into

model-checking:mainfrom

jrey8343:challenge-21-str-searcher

Commits on Feb 6, 2026

Verify safety of char-related Searcher methods (Challenge 20)
jrey8343
committed
bdb88ae
Fix CI: remove loop invariants that cause CBMC assigns check interference
jrey8343
committed
fd5215c

Commits on Feb 7, 2026

Commits on Feb 11, 2026

Abstract next_match/next_match_back with #[cfg(kani)] nondeterministic overapproximation
jrey8343
committed
b2ec02c

Commits on Feb 21, 2026

Fix arithmetic overflow in next_match/next_match_back Kani abstractions
jrey8343
committed
d50b119

Commits on Apr 2, 2026

Add UTF-8 char boundary constraints and fix overflow in Kani abstractions
jrey8343
committed
bdcbda1

Commits on Aug 6, 2026

Relax TwoWaySearcher::new Kani bounds and remove unsafe from abstractions

jrey8343
and
claude
committed
941021c
Strengthen Ch21 harnesses: inductive invariant proofs with symbolic inputs

jrey8343
and
claude
committed
c0258c9