KPHP: An Executable Formal Semantics for PHP

About Overview Download Online interface


KPHP is an executable formal semantics for PHP written in K, a language definitional framework based on Rewriting Logic and implemented on top of the Maude system.

KPHP is described in the paper An Executable Formal Semantics of PHP by D. Filaretti and S. Maffeis, to appear at ECOOP 2014. An up-to-date, extended version of the paper is available here.

If you just want to try out KPHP, you can use the Online interface. All the source files are available in the Download section, together with a Linux-based virtual machine with a fresh working copy of the KPHP distribution and dependencies.

All files are copyright of the authors.

Work funded by EPSRC grant EP1004246/1.

An overview of the KPHP Project

Downloads and Documentation

All KPHP source files are human readable and executable via the K tools (see the instructions provided in the Documentation section).


We provide an informal documentation based on examples. We plan to expand and revise this documentation in the future.


You can download all the sources as a single zip file here. See the Documentation section and the README file included in the archive for usage information.

Note that it is necessary to obtain a binary distribution of the K Framework in order to compile and execute our semantics. Please get the latest build .

Using the KPHP virtual machine

Alternatively, in case you experience issues installing the K tools (which is unlikely), you can use our self-contained Linux-based virtual machine .

The archive contains the following files:

For detailed set-up and usage information, please refer to the KVM documentation . Note that the procedure is the same but there is no need to download the KVM or the K tools, as are already provided by us in this package.

When setting up the shared folders in VMWare (5th bulletpoint in the "Setting up the KVM" section) you should add the k folder as well as the folder containing the KPHP sources.