Bennet: Randomized Specification Testing for Heap-Manipulating Programs

on YouTube ↗15m

" summary

Bennet synthesizes C test generators from CN specifications by compiling preconditions into a DSL and running randomized backtracking search to place heap objects, enforce exclusive ownership, and carry size constraints on failure. It emits standalone C harnesses, generates 100 passing cases for nearly all non-buggy CN tutorial examples, finds two real bugs in existing code, and consistently rediscovers injected bugs (20/20 trials); some hard exact-list targets remain unsynthesized.

AI-written summary · about

" chapters (13)

1. 0:00Randomized specification testing
2. 1:02Separation logic in C
3. 2:25CN specs and predicates
4. 3:31Generator DSL for C
5. 4:54Backtracking and ownership
6. 6:21Consistent input distribution
7. 7:23Generator optimizations
8. 8:47Efficient constraint reordering
9. 9:28Bennett evaluation on CN code
10. 10:34Bugs found with Bennett
11. 11:17Optimization passes impact
12. 11:59Summary of CN generators
13. 12:25Q&A

" related talks

• 47mTesting the Hard Stuff and Staying SaneJohn Hughes · Clojure/West 2014
• 45mProperty based tests for the massesRomeu Moura · Code Mesh LDN 2018
• 32mGenerative Testing: Properties, State and BeyondJan Stępień · EuroClojure 2015
• 26mThe missing piece of testingMaciej Myśliński · FrontEnd Con 2018
• 01h 07mProgramming with GUTsKevlin Henney · Meeting C++ 2021
• 15mGrammar-Based Testing for Little Languages: An Experience Report with Student CompilersKonstantinos Sagonas, Phillip van Heerden, Moeketsi Raselimo, Bernd Fischer · SLE 2020
• 15mGradual Verification of Recursive Heap Data StructuresJonathan Aldrich, Éric Tanter, Johannes Bader, Jenna Wise, Cameron Wong, Joshua Sunshine, Jenna DiVincenzo · OOPSLA 2020
• 42mSurprise yourself with Property Based TestingMartin Hellspong · Øredev 2023