About Verification / Validation Work
1. Plan of Action:
a.) Figure out different techniques available for reduction in state space and List them here
b.) Make a list of papers which need to be read and discussed
c.) Make a list of tools which need to be tried
d.) Make a list of Models which need to be tried on the tools
e.) Set Milestones, Deadlines for papers, atleast one a week, from both of us
f.) Keep a log of issues discussed
g.) Why not we write a survey paper first (On verification of Hardware C/C++ Models and include our study on what kind of programs / models worked on what kind of tool and what did not, and why they did not work? What do you say ?
h.) Talk to Jyotirmaya / Roopsha
2. Four week schedule:
a.) We should have done 4 papers each, discussed it, analysed it, understood it completely
b.) We should have done inspection of atleast 4 potential tools, excluding CBMC and Cute, along with the technique they use and the potential issues
c.) Tools should be for C and C++
d.) All the small models including both C and C++ should have been tried on them and if possible LC3B model too
Useful Links
Jacob's Page regarding Testing
Testing class at Univ of Cincinnati
Basic Model Checking Useful Lecture (Extracted from Huth and Ryan)
Basic Model Checking Useful Tutorial
Model Checking Useful Tutorial
Some papers which we are referring can be found here