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/21 15:35]
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.
+===== Project Status =====
+  - Infrastructure for ARMC translation is done.
+  - Able to translate simple arithmetic programs.
+  - De-sugaring of program  calls yet to be done.
+  - Only very simple formula can be processed.( Need to convert Formula to DNF form)
+  - Sometimes generates buggy transition relation ( But few tests are working well. )
+  - Support for If and Loops is incomplete.
+===== Difficulties and issues =====
+  - It took some time to understand Jahob data-structures.
+  - Some places it was difficult to say what format of formula program will receive.
+  - Needs more experimentation and effort.