The *(term) for a type of program or module that carries a verifiable specification of its behavior as it is _(migrated| migration) between contexts.

<ul class="links">
<li>_(Research in the area| http://www.cs.princeton.edu/sip/projects/pcc/).
<li>_(An overview| http://www-2.cs.cmu.edu/~petel/papers/pcc/pcc.html).
</ul>
