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:27] vaibhav.rajan |
constraint_based_analysis_of_java_using_jahob_and_amrc [2007/06/21 15:33] vaibhav.rajan |
||
---|---|---|---|
Line 22: | Line 22: | ||
- ''Abstract Fixed Point'' finds a fixed point which does not contain error state. | - ''Abstract Fixed Point'' finds a fixed point which does not contain error state. | ||
- ''Feasible Counter Example'' finds a concrete counter example. | - ''Feasible Counter Example'' finds a concrete counter example. | ||
- | | ||
- | === Abstract Fixed Point === | ||
+ | ===== 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. | ||