This work presents a sound backward analysis for sufficient pre-conditions inference in C programs, by abstract interpretation. It builds upon previous works done for a purely numeric subset of C, and extends them to support the C memory model. Pointer dereferences are handled with the cell abstraction and dynamic memory…
In Fortran/Algol tradition, a mutable variable is a variable that can be directly mutated as such by assignment, increment, etc. In contrast, ML tradition uses variables of reference types, bound to ‘boxed values’, or reference cells. These are ordinary, lambda-calculus variables that can be substituted for but not mutated…
Biological system modeling is an iterative process where uncertainties may arise, especially in the early stages of the modeling. Static analysis tools are needed during each stage of the modeling to help modelers detect unexpected behaviors early by automatically inferring properties about the model. However, the rule-based modeling language Kappa…
