Differences

This shows you the differences between two versions of the page.

--- 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:53]
vaibhav.rajan
@@ Line 9: / Line 9: @@
 {{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 ===