KPHP

Forming the central topic of my PhD thesis, KPHP is a formal (mathematical) specification for the PHP programming language developed using the K Framework.

Applications include the development of a prototype correct-by-construction bug-finding tool derived from the specification using the theory of abstract interpretation.

For more details please visit phpsemantics.org or the project’s GitHub repo, or see the following related publications:

An Executable Formal Semantics of PHP with Applications to Program Analysis. PhD Thesis, Imperial College London, 2016.

An Executable Formal Semantics for PHP - with S. Maffeis - ECOOP 2014.