diff --git a/README.md b/README.md
index 21f0fa5b731bc6c3dc3e0792e897cd4ad2dd728f..c6abd59858a99994d71ad3b6683d52476c3bba00 100644
--- a/README.md
+++ b/README.md
@@ -21,7 +21,7 @@ Please remove "nospam" from the email addresses.
 
 WSymb is a WCET analysis tool. Its main specificity is that, instead of
 a constant WCET, it computes a *WCET formula*, where symbols (or
-parameters) can correspond to various kind of values unnkown at analysis
+parameters) can correspond to various kinds of values unnkown at analysis
 time. The formula can later be *instanciated*, when parameter values are
 known. For more details on the underlying theory, check out the papers
 [1,2].
@@ -145,6 +145,20 @@ identifiers to their values. In this example, the WCET is successively
 instantiated with values ranges from 0 to 20 for parameter 1. Parameter
 identifiers are visible in the `.pwf` file.
 
+### Procedures with a parametric WCET
+
+You can specify a procedure for which the WCET is a parameter (i.e. the
+WCET of the procedure is considered to be unknown by `dumpcft`). To do
+so:
+1. Write a `.pfl` file, where each line consists of a procedure name and
+   a parameter identifier (an integer);
+2. Pass that file as an argument to `dumpcft`. This produces a `.pwf`
+   file, where the WCET of the procedure is replaced by the
+   corresponding parameter idenfitier;
+3. For parameter instanciation, see the example `pwcet_instantiator.c`,
+   where the procedure `param_valuation` relates parameter identifiers
+   to their values (same as for parametric loop bounds).
+
 ----
 ## References