Static Analysis of Pasta

This paper was my 4th year undergraduate project, again written in Haskell, for which I implemented a proof generator for Pasta (a pointer programming language)

Most errors in computer programs are only found once they are run, which results in critical errors being missed due to inadequate testing. If additional static analysis is performed, then the possibility exists for detecting such errors, and correcting them. This helps to improve the quality of the resulting code, increasing reliability.

In this project the existing static analysis research is reviewed, along with implementations used both by normal programmers, and used in safety critical applications. A static analysis program is then designed and implemented for the experimental pointer based language Pasta.

The resulting program checks for totality, proving that a particular procedure cannot crash and will terminate. Where a procedure does not satisfy this, the preconditions for the procedure are generated.


Tags: haskell program