Aim - Modelling a dice game in NuSMV, testing using LTL & CTL, bounded software analysis using CIVL, static and run-time verification using Frama-C.
Implemented a simple dice game model in NuSMV
Tested the model using LTL & CTL constructs
Studied test cases for multiple winners in the game, state space exploration for increasing dice.
Proposed optimizations to the developed model.
Performed bounded software analysis using CIVL
Analyzed segments of code and functions to check for correct code behavior & boundability.
Performed static & run-time verification using Frama-C for different code segments and functions in code.
Comments