tacasv2a: --slice that keeps the suite valid (reach + assert) - #68

Open

GuilhermeBn198 wants to merge 25 commits into

feat/tacas-slicing

Commits on Sep 26, 2026

docs(tacasv1): design spec — replace LibFuzzer with AFL++
GuilhermeBn198
committed
b72835b
docs(tacasv1): implementation plan — LibFuzzer to AFL++
GuilhermeBn198
committed
e98397d
feat(tacasv1): install AFL++ 4.40c (PCGUARD) in the dev image
GuilhermeBn198
committed
fdd1fb4
feat(tacasv1): resolve afl-clang-fast/afl-fuzz paths
GuilhermeBn198
committed
0031130
feat(tacasv1): replace FindLibFuzzer with FindAFLPlusPlus
GuilhermeBn198
committed
1455be8
feat(tacasv1): AFL++ persistent nondet generator
GuilhermeBn198
committed
208c6dc
feat(tacasv1): drive AFL++ from the Caller
GuilhermeBn198
committed
d9ab6d0
feat(tacasv1): --nondet-generator afl replaces fuzzer
GuilhermeBn198
committed
c18cd77
chore(tacasv1): rename SKIP_LIB_FUZZER→SKIP_AFL_PLUS_PLUS and update docs
GuilhermeBn198
committed
abae549
fix(tacasv1): make the AFL++ arm build and confirm violations

GuilhermeBn198
and
claude
committed
87f9aaa
fix(tacasv1): address the review of the AFL++ fix commit

GuilhermeBn198
and
claude
committed
d089c90
feat(tacasv1): CmpLog companion binary, and rewind the AFL++ read index

GuilhermeBn198
and
claude
committed
1a49aa5
fix(tacasv1): bound afl-fuzz by timeout alone, not also by -V

GuilhermeBn198
and
claude
committed
a6068c6
fix(verdict): an empty vector is a witness when the program reads no input

GuilhermeBn198
and
claude
committed
6c7b0f2

Commits on Sep 27, 2026

docs(tacasv2a): design spec — slicing for reach/assert that keeps the suite valid

GuilhermeBn198
and
claude
committed
a12ac9b
docs(tacasv2a): implementation plan

GuilhermeBn198
and
claude
committed
83ec67c
feat(tacasv2a): pure slicing helpers -- criteria, stub, statistics

GuilhermeBn198
and
claude
committed
74ecf4a
fix(tacasv2a): slice without cutoff and keep every nondet read

GuilhermeBn198
and
claude
committed
336a26d
feat(tacasv2a): --slice in assert mode

GuilhermeBn198
and
claude
committed
c36a532
docs(tacasv2a): diagnostic sample re-run on the implementation

GuilhermeBn198
and
claude
committed
75bdefd
fix(tacasv2a): take the nondet names from the program as well

GuilhermeBn198
and
claude
committed
ffad3e5
ci: run the PR gates on PRs stacked on tacas/** branches

GuilhermeBn198
and
claude
committed
0b0e855
Revert "ci: run the PR gates on PRs stacked on tacas/** branches"

GuilhermeBn198
and
claude
committed
8eb66b3
test(tacasv1): the evaluation runner's fuzzer arm is GENERATOR=afl

GuilhermeBn198
and
claude
committed
5a4e2fb
Merge branch 'feat/tacas-aflpp' into feat/tacas-slicing
GuilhermeBn198
committed
d182b20