Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
constraint_based_analysis_of_java_using_jahob_and_amrc [2007/06/14 12:02] vaibhav.rajan |
constraint_based_analysis_of_java_using_jahob_and_amrc [2007/06/14 12:30] vaibhav.rajan |
||
---|---|---|---|
Line 9: | Line 9: | ||
{{padl07-armc.pdf|ARMC: The Logical Choice for Software Model Checking with Abstraction Refinement}} | {{padl07-armc.pdf|ARMC: The Logical Choice for Software Model Checking with Abstraction Refinement}} | ||
- | ==== Introduction ==== | + | ==== ARMC ==== |
+ | |||
+ | ARMC stands for Abstract Refinement Model Checker. We have already learned this methodlogy in the course. This model checker executes program using abstract set of states. Model checker divided its process in following three procedures: | ||
+ | |||
+ | - ''Abstract Fixed Point'' | ||
+ | - ''Feasible Counter Example'' | ||
+ | - ''Refine'' | ||
+ | |||
+ | ARMC calls them in a loop. Until any of the following two event happens: | ||
+ | |||
+ | |||
+ | - ''Abstract Fixed Point'' finds a fixed point which does not contain error state. | ||
+ | - ''Feasible Counter Example'' finds a concrete counter example. | ||
+ | |||
+ | |||
+ | === Abstract Fixed Point === | ||
+ | |||
+ | |||
+ | === Feasible Counter Example === | ||
+ | |||
+ | |||
+ | === Refine === | ||