Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision | ||
|
constraint_based_analysis_of_java_using_jahob_and_amrc [2007/06/14 12:26] vaibhav.rajan |
constraint_based_analysis_of_java_using_jahob_and_amrc [2007/06/21 15:36] 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. | ||
| - | | + | |
| + | |||
| + | ===== 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 for making this plugin usable | ||