Each .sbl file demonstrates a different verification scenario — from classic concurrency (dining philosophers, MESI cache coherence, PoS consensus) to vulnerability classes in packet parsers, smart contracts, and protocol stacks.
Network packet parser that computes an allocation size, copies data, and frees on error. Integer overflow → undersized buffer → out-of-bounds write → use-after-free in the error path.
saple analyze examples/vulnerable_server.sbl \
--verbosex86-64 instruction chain where a loop copies user input into a stack frame without bounds checking. SAPLE finds the overflow and the return-address overwrite.
saple analyze examples/stack_buffer_overflow.sbl \
--verboseMulti-layer TCP/IP stack (Ethernet → IP → TCP → Application) with six classes of vulnerability: header underflow, fragment-reassembly overflow, SYN flood, heap overflow, malformed-frame acceptance, incorrect length.
saple analyze examples/network_protocol_stack.sbl \
--verboseThe classic concurrency benchmark: 5 philosophers, 5 forks. Verifies noDeadlock, mutualExclusion, and progress.
saple analyze examples/dining_philosophers.sbl --verboseSimplified ERC-20 token. Detects external-call reentrancy, unchecked mint overflow, unauthorized mint, and the approval double-spend race.
saple analyze examples/token_contract.sbl --verboseFour-core MESI cache protocol. Detects concurrent writes without invalidation and stale reads of remotely-modified lines. Properties: coherence, exclusiveIsolation, liveness.
saple analyze examples/cache_coherence.sbl --verboseMulti-node proof-of-stake consensus protocol with validator selection and block creation. Checks safety and liveness across configurations.
saple analyze examples/consensus.sbl --verboseAdd --extract-rules to any of the above. SAPLE turns each finding into a reusable .sbl pattern, cross-validates it through the SMT solver, and stores it under patterns/generated/. On subsequent runs, those rules auto-load and apply to new files.
saple analyze examples/vulnerable_server.sbl \
--extract-rules --export rules.json \
--verbose