Links for the talk at NVidia FM Week 2025
This is the material accompanying the talk given by Igor Konnov at NVidia FM Week 2025: Hands-on symbolic search & test generation with Apalache.
- To follow the talk, visit the slides.
- The model checker Apalache.
- The cyclic buffer example.
- [Blogpost][] that compares bounded model checking, randomized symbolic execution, and inductive invariants.
- The new JSON RPC API in Apalache and a Python library apalache-rpc-client.
- The TFTP protocol specification in TLA+ used in the talk.
- The project on testing TFTP with symbolic model checking: tftp-symbolic-testing.
- ITF JSON trace format and a Python library itf-py.