Immune System Inspired Approach for Program Verification

Program invariants encapsulate the computability and correctness of a particular program.

This work applies immune system inspired algorithms to find program invariants and prove correctness and termination.

A lot of work has been done on incomputability and undecidability in theoretical computer science.

The best characterization of this comes in the form of the Halting Problem and the Church-Turing thesis.

Biological systems also perform computation, e.g. the immune system computes the most efficient

way to eliminate pathogens in a timely manner without harming the host.

However it has been more difficult to define incomputability and undecidability for biological systems.

This work lays the foundation of applying the theoretical concepts of computability

and undecidability to the immune system and possibly biological computing in general.

This is the first application of undecidability to immuno-computing.

Read more about it here (pdf).

Fig. Mutations in the artificial immune system generate invariants for computer programs.