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.