Formal Verification through Python – Why and How?
summary
Shows how to integrate the NuSMV model checker with Python to make formal verification workflows more user-friendly and modular: Python generates NuSMV input files, runs NuSMV as a subprocess, parses its results, and adapts runs when problem parameters change. Demonstrates this approach in reinforcement learning (Q-learning on OpenAI-style Frozen Lake): using NuSMV to check solvability before training, to evaluate epsilon-to-convergence choices, and to act as an expert during training to determine if the agent has enough information to find an optimal route.
AI-written summary · about
related talks
28mDerivations, Not Just Simulations: Teaching Applied Mathematics with Scientific Python
19mPython as a language for testing and code generation
23mHow cocotb made Python-powered verification mainstream -- and what comes next
15mModeling Hardware in Python with Zuspec
30mMultibody Simulation Using sympy, scipy and vpython
32mProcess Mining in Python
24mTesting Your Python Code
14mSynthesizing Vectorized Code via Verified Lifting