diff --git a/README.md b/README.md
index 57bfa99a5..582405982 100644
--- a/README.md
+++ b/README.md
@@ -36,294 +36,8 @@ with a wide variety of benchmarked tools and hundreds of thousands benchmark run
 
 BenchExec is developed at the [Software Systems Lab](http://www.sosy-lab.org) at the [University of Passau](http://www.uni-passau.de).
 
-
 ### Links
+- [Documentation](https://github.com/dbeyer/benchexec/tree/master/doc/INDEX.md)
 - [BenchExec GitHub Repository](https://github.com/dbeyer/benchexec),
   use this for reporting [issues](https://github.com/dbeyer/benchexec/issues)
 - [BenchExec at PyPI](https://pypi.python.org/pypi/BenchExec)
-
-
-## Documentation
-
-### Download and Installation
-BenchExec requires at least Python 3.2.
-
-To install BenchExec we recommend to use the Python package installer pip
-(installable for example with `sudo apt-get install pip3` on Debian/Ubuntu).
-
-To automatically download and install the latest stable version and its dependencies
-from the [Python Packaging Index](https://pypi.python.org/pypi/BenchExec),
-run this command:
-
-    sudo pip3 install benchexec
-
-You can also install BenchExec only for your user with
-
-    pip3 install --user benchexec
-
-In this case you probably need to add the directory where pip installs the commands
-to the PATH environment by adding the following line to your `~/.profile` file:
-
-    export PATH=~/.local/bin:$PATH
-
-Of course you can also install BenchExec in a virtualenv if you are familiar with Python tools.
-
-To install the latest development version from the
-[GitHub repository](https://github.com/dbeyer/benchexec), run this command:
-
-    pip3 install --user git+https://github.com/dbeyer/benchexec.git
-
-
-### Setting up Cgroups
-To execute benchmarks and reliably measure and limit their resource consumption,
-BenchExec requires that the user which executes the benchmarks
-can create and modify cgroups.
-
-Any Linux kernel version of the last years is
-acceptable, though there have been performance improvements for the memory
-controller in version 3.3, and cgroups in general are still getting improved, thus,
-using a recent kernel is a good idea.
-
-The cgroup virtual file system is typically mounted at `/sys/fs/cgroup`.
-If it is not, you can mount it with
-
-    sudo mount -t cgroup cgroup /sys/fs/cgroup
-
-To give all users on the system the ability to create their own cgroups,
-you can use
-
-    sudo chmod o+wt,g+w /sys/fs/cgroup/
-
-Of course permissions can also be assigned in a more fine-grained way if necessary.
-
-Alternatively, software such as `cgrulesengd` from
-the [cgroup-bin](http://libcg.sourceforge.net/) package
-can be used to setup the cgroups hierarchy.
-
-If your machine has swap, cgroups should be configured to also track swap memory.
-If the file `memory.memsw.usage_in_bytes` does not exist in the directory
-where the cgroup file system is mounted, this needs to be enabled by setting
-`swapaccount=1` on the command line of the kernel.
-To do so, you typically need to edit your bootloader configuration
-(under Ubuntu for example in `/etc/default/grub`, line `GRUB_CMDLINE_LINUX`),
-update the bootloader (`sudo update-grub`), and reboot.
-
-It may be that your Linux distribution already mounts the cgroup file system
-and creates a cgroup hierarchy for you.
-In this case you need to adjust the above commands appropriately.
-To optimally use BenchExec,
-the cgroup controllers `cpuacct`, `cpuset`, `freezer`, and `memory`
-should be mounted and usable,
-i.e., they should be listed in `/proc/self/cgroups` and the current user
-should have at least the permission to create sub-cgroups of the current cgroup(s)
-listed in this file for these controllers.
-
-
-### Using runexec to Benchmark a Single Run
-
-BenchExec provides a program called `runexec` that can be used to
-easily execute a single command while measuring its resource consumption,
-similarly to the tool `time` but with more reliable time measurements
-and with measurement of memory usage.
-To use it, simply pass as parameters the command that should be executed
-(adding `--` before the command will ensure that the arguments to the command
-will not be misinterpreted as arguments to `runexec`):
-
-    runexec -- <cmd> <arg> ...
-
-This will start the command, write its output to the file `output.log`,
-and print resource measurements to stdout. Example:
-
-    $ runexec echo Test
-    2015-03-06 12:54:01,707 - INFO - Starting command echo Test
-    2015-03-06 12:54:01,708 - INFO - Writing output to output.log
-    exitcode=0
-    returnvalue=0
-    walltime=0.0024175643920898438s
-    cputime=0.001671s
-    memory=131072
-
-Resource limits can be enabled with additional arguments to `runexec`,
-e.g. for CPU time (`--timelimit`), wall time (`--walltimelimit`),
-or memory consumption (`--memlimit`). If any of the limits is exceeded,
-the started command is killed forcefully (including any child processes it started).
-
-`runexec` can also restrict the executed command to a set of specific CPU cores
-with the parameters `--cores`,
-and (on NUMA systems) to specific memory regions with `--memoryNodes`.
-The IDs used for CPU cores and memory regions are the same as used by the kernel
-and can be seen in the directories `/sys/devices/system/cpu` and `/sys/devices/system/node`.
-
-Additional parameters allow to change the name of the output file and the working directory.
-The full set of available parameters can be seen with `runexec -h`.
-
-
-### Using benchexec to Benchmark a Collection of Runs
-
-The program `benchexec` provides the possibility to easily benchmark
-multiple executions of a tool in one go.
-
-#### Input for benchexec
-`benchexec` uses as input an XML file that defines the command(s) to execute,
-the resource limits, and the input files for which the command should be run.
-A complete definition of the input format can be found in the file
-[doc/benchmark.xml](doc/benchmark.xml),
-and examples in [doc/benchmark-example-rand.xml](doc/benchmark-example-rand.xml)
-and [doc/benchmark-example-cbmc.xml](doc/benchmark-example-cbmc.xml).
-A document-type definition with a formal specification of such files can be found in
-[doc/benchmark.dtd](doc/benchmark.dtd).
-Such benchmark-definition files consist of a root tag `<benchmark>`
-that has attributes for the tool to use and the resource limits.
-Nested `<rundefinition>` tags allow to specify multiple different configurations of the tool,
-each of which is executed with the input files.
-The input files are defined in nested `<inputfiles>` tags,
-either with `<include>` tags (which directly specify patterns of input files)
-or with `<includesfile>` tags (which specify text files with file-name patterns on each line).
-Relative file names in these tags are interpreted as relative to the directory of the XML file. 
-Command-line arguments for the tool are given with `<option>` tags,
-which can appear directly inside the root tag (always effective),
-inside a `<rundefinition>` tag (affective for this configuration),
-or inside a `<inputfiles>` tag (affective only for this subset of files for all configurations).
-Note that you need to use a separate `<option>` tag for each argument,
-putting multiple arguments separated by spaces into a single tag will not have the desired effect.
-
-BenchExec allows to check whether the output of the tool matches the expected result
-for a given input file, and to categorize the results accordingly.
-This is currently only available for the domain of software verification,
-where `benchexec` uses a
-[property file as defined by the International Competition on Software Verification](http://sv-comp.sosy-lab.org/2015/rules.php).
-Such files can be specified with the tag `<propertyfile>`.
-
-Inside the `<option>` tag and other tags some variables can be used
-that will be expanded by BenchExec. The following variables are supported:
-
-    ${benchmark_name}       Name of benchmark execution
-    ${benchmark_date}       Timestamp of benchmark execution
-    ${benchmark_path}       Directory of benchmark XML file
-    ${benchmark_path_abs}   Directory of benchmark XML file (absolute path)
-    ${benchmark_file}       Name of benchmark XML file (without path)
-    ${logfile_path}         Directory where tool-output files will be stored
-    ${logfile_path_abs}     Directory where tool-output files will be stored (absolute path)
-    ${rundefinition_name}   Name of current run definition
-    ${inputfile_name}       Name of current input file (without path)
-    ${inputfile_path}       Directory of current input file
-    ${inputfile_path_abs}   Directory of current input file (absolute path)
-
-For example, to pass as additional tool parameter the name of a file
-that is in the same directory as each input files, use
-
-    <option name="-f">${inputfile_path}/additional-file.txt</option>
-
-#### Adopting benchexec for a specific tool
-In order to know how to execute a tool and how to interpret its output,
-`benchexec` needs a tool-specific Python module
-with functions for creating the appropriate command-line arguments for a run etc.
-Such modules need to define a class `Tool` that inherits from `benchexec.tools.template.BaseTool`.
-This class also defines the [documentation](benchexec/tools/template.py)
-on how to write such a module.
-BenchExec already provides such [ready-to-use modules for some common tools](benchexec/tools/).
-
-#### Starting benchexec
-To use `benchexec`, simply call it with an XML file with a benchmark definition:
-
-    benchexec doc/benchmark-example-rand.xml
-
-Command-line arguments to `benchexec` allow to override the defined resource limits.
-If one wants to execute only a subset of the defined benchmark runs,
-the name of the `<rundefinition>` and/or `<inputfiles>` tags
-that should be executed can also be given on the command line.
-To start multiple executions of the benchmarked tool in parallel
-(if the local machine has enough resources),
-use the parameter `--numOfThreads`.
-Example:
-
-    benchexec doc/benchmark-example-rand.xml --inputfiles "XML files" --limitCores 1 --timelimit 10 --numOfThreads 4
-
-The full set of available parameters can be seen with `benchexec -h`.
-
-`benchexec` produces as output the results and resource measurements
-of all the individual tool executions in XML files
-from which tables can be created using `table-generator`.
-There is one file per run definition/tool configuration,
-and additional files for each subset of input files
-(all by default in directory `./result/`).
-A document-type definition with a formal specification of such result files can be found in
-[doc/benchmark-result.dtd](doc/benchmark-result.dtd).
-The output of the tool executions is stored in additional files in a sub-directory.
-If the target directory for the output files (specified with `--outputpath`)
-is a git repository without uncommitted changes and the option `--commit`
-is specified, `benchexec` will add and commit all created files to the git repository.
-One can use this to create a reliable archive of experimental results.
-
-
-### Using table-generator to Generate Tables of Results
-
-The program `table-generator` allows to generate HTML and CSV tables.
-It takes one or more XML files with results from `benchexec`
-and produces tables with columns for each of the files,
-such that all results for a given input file appear on the same line.
-To start it, simply pass all result files on the command line, e.g.
-
-    table-generator results/benchmark-example-rand.*.results.xml
-
-Further command-line arguments can be used to customized the table,
-e.g. for ignoring all incorrect results (`--correct-only`),
-or for specifying name and location of the table files (`--name`, `--outputpath`).
-The full set of available parameters can be seen with `table-generator -h`.
-
-`table-generator` also supports using a special file as input
-that defines the layout of the generated tables
-and allows even more customizations,
-including the ability to extract arbitrary values
-from the output of the tool of each run
-and inserting them into the table.
-Such table-definitition files are also in XML format
-and a complete definition can be found in the file
-[doc/table-generator.xml](doc/table-generator.xml),
-and an example in [doc/table-generator-example.xml](doc/table-generator-example.xml).
-A document-type definition with a formal specification of such files can be found in
-[doc/table-generator.dtd](doc/table-generator.dtd).
-To use such files pass them with the parameter `-x` to `table-generator`:
-
-    table-generator -x doc/table-generator-example.xml
-
-
-### Integration into other Benchmarking Frameworks
-
-BenchExec can be used inside other benchmarking frameworks
-for the actual command execution and handling of the resource limits and measurements.
-To do so, simply use the `runexec` command in your benchmarking framework
-as a wrapper around the actual command, and pass the appropriate command-line flags
-for resource limits and read the resource measurements from the output.
-If you want to bundle BenchExec with your framework,
-you only need to use the `.egg` file for BenchExec,
-no external dependencies are required.
-You can also execute `runexec` directly from the `.egg` file with the following command
-(no separate start script or installation is necessary):
-
-    PYTHONPATH=path/to/BenchExec.egg python3 -m benchexec.runexecutor ...
-
-From within Python, BenchExec can be used to execute a command as in the following example:
-
-    from benchexec.runexecutor import RunExecutor
-    executor = RunExecutor()
-    result = executor.execute_run(args=[<TOOL_CMD>], ...)
-
-Further parameters for `execute_run` can be used to specify resource limits
-(c.f. [runexecutor.py](benchexec/runexecutor.py)).
-The result is a dictionary with the same information about the run
-that is printed to stdout by the `runexec` command-line tool.
-
-
-### Extending BenchExec
-
-BenchExec executes all runs on the local machine.
-In some cases, it might be desired to use for example some cloud service
-to execute the commands, and BenchExec should only handle the benchmark definition
-and aggregate the results.
-This can be done by replacing the module `benchexec.localexecution`,
-which is responsible for executing a collection of runs, by something else.
-To do so, inherit from the BenchExec main class `benchexec.BenchExec`
-and override the necessary methods such as `load_executor`
-(which by default returns the `benchexec.localexecution` module),
-`create_argument_parser` (to add your own command-line arguments) etc.
diff --git a/doc/INDEX.md b/doc/INDEX.md
new file mode 100644
index 000000000..7f6986729
--- /dev/null
+++ b/doc/INDEX.md
@@ -0,0 +1,14 @@
+# BenchExec: Documentation
+
+BenchExec consists of three programs:
+
+- `benchexec`: main benchmarking utility
+- `table-generator`: for generating result tables
+- `runexec`: for benchmarking a single tool execution (can also be integrated into other benchmarking frameworks)
+
+The documentation for BenchExec is available in the following files:
+
+- [General installation instructions](INSTALL.md)
+- [benchexec](benchexec.md)
+- [table-generator](table-generator.md)
+- [runexec](runexec.md)
diff --git a/doc/INSTALL.md b/doc/INSTALL.md
new file mode 100644
index 000000000..0c4648ed9
--- /dev/null
+++ b/doc/INSTALL.md
@@ -0,0 +1,76 @@
+# BenchExec: Setup
+
+## Download and Installation
+
+BenchExec requires at least Python 3.2.
+
+To install BenchExec we recommend to use the Python package installer pip
+(installable for example with `sudo apt-get install pip3` on Debian/Ubuntu).
+
+To automatically download and install the latest stable version and its dependencies
+from the [Python Packaging Index](https://pypi.python.org/pypi/BenchExec),
+run this command:
+
+    sudo pip3 install benchexec
+
+You can also install BenchExec only for your user with
+
+    pip3 install --user benchexec
+
+In this case you probably need to add the directory where pip installs the commands
+to the PATH environment by adding the following line to your `~/.profile` file:
+
+    export PATH=~/.local/bin:$PATH
+
+Of course you can also install BenchExec in a virtualenv if you are familiar with Python tools.
+
+To install the latest development version from the
+[GitHub repository](https://github.com/dbeyer/benchexec), run this command:
+
+    pip3 install --user git+https://github.com/dbeyer/benchexec.git
+
+
+## Setting up Cgroups
+
+To execute benchmarks and reliably measure and limit their resource consumption,
+BenchExec requires that the user which executes the benchmarks
+can create and modify cgroups.
+
+Any Linux kernel version of the last years is
+acceptable, though there have been performance improvements for the memory
+controller in version 3.3, and cgroups in general are still getting improved, thus,
+using a recent kernel is a good idea.
+
+The cgroup virtual file system is typically mounted at `/sys/fs/cgroup`.
+If it is not, you can mount it with
+
+    sudo mount -t cgroup cgroup /sys/fs/cgroup
+
+To give all users on the system the ability to create their own cgroups,
+you can use
+
+    sudo chmod o+wt,g+w /sys/fs/cgroup/
+
+Of course permissions can also be assigned in a more fine-grained way if necessary.
+
+Alternatively, software such as `cgrulesengd` from
+the [cgroup-bin](http://libcg.sourceforge.net/) package
+can be used to setup the cgroups hierarchy.
+
+If your machine has swap, cgroups should be configured to also track swap memory.
+If the file `memory.memsw.usage_in_bytes` does not exist in the directory
+where the cgroup file system is mounted, this needs to be enabled by setting
+`swapaccount=1` on the command line of the kernel.
+To do so, you typically need to edit your bootloader configuration
+(under Ubuntu for example in `/etc/default/grub`, line `GRUB_CMDLINE_LINUX`),
+update the bootloader (`sudo update-grub`), and reboot.
+
+It may be that your Linux distribution already mounts the cgroup file system
+and creates a cgroup hierarchy for you.
+In this case you need to adjust the above commands appropriately.
+To optimally use BenchExec,
+the cgroup controllers `cpuacct`, `cpuset`, `freezer`, and `memory`
+should be mounted and usable,
+i.e., they should be listed in `/proc/self/cgroups` and the current user
+should have at least the permission to create sub-cgroups of the current cgroup(s)
+listed in this file for these controllers.
diff --git a/doc/benchexec.md b/doc/benchexec.md
new file mode 100644
index 000000000..b45e5c1ee
--- /dev/null
+++ b/doc/benchexec.md
@@ -0,0 +1,110 @@
+# BenchExec: benchexec
+## Benchmarking a Collection of Runs
+
+The program `benchexec` provides the possibility to easily benchmark
+multiple executions of a tool in one go.
+
+### Input for benchexec
+`benchexec` uses as input an XML file that defines the command(s) to execute,
+the resource limits, and the input files for which the command should be run.
+A complete definition of the input format can be found in the file
+[doc/benchmark.xml](benchmark.xml),
+and examples in [doc/benchmark-example-rand.xml](benchmark-example-rand.xml)
+and [doc/benchmark-example-cbmc.xml](benchmark-example-cbmc.xml).
+A document-type definition with a formal specification of such files can be found in
+[doc/benchmark.dtd](benchmark.dtd).
+Such benchmark-definition files consist of a root tag `<benchmark>`
+that has attributes for the tool to use and the resource limits.
+Nested `<rundefinition>` tags allow to specify multiple different configurations of the tool,
+each of which is executed with the input files.
+The input files are defined in nested `<inputfiles>` tags,
+either with `<include>` tags (which directly specify patterns of input files)
+or with `<includesfile>` tags (which specify text files with file-name patterns on each line).
+Relative file names in these tags are interpreted as relative to the directory of the XML file. 
+Command-line arguments for the tool are given with `<option>` tags,
+which can appear directly inside the root tag (always effective),
+inside a `<rundefinition>` tag (affective for this configuration),
+or inside a `<inputfiles>` tag (affective only for this subset of files for all configurations).
+Note that you need to use a separate `<option>` tag for each argument,
+putting multiple arguments separated by spaces into a single tag will not have the desired effect.
+
+BenchExec allows to check whether the output of the tool matches the expected result
+for a given input file, and to categorize the results accordingly.
+This is currently only available for the domain of software verification,
+where `benchexec` uses a
+[property file as defined by the International Competition on Software Verification](http://sv-comp.sosy-lab.org/2015/rules.php).
+Such files can be specified with the tag `<propertyfile>`.
+
+Inside the `<option>` tag and other tags some variables can be used
+that will be expanded by BenchExec. The following variables are supported:
+
+    ${benchmark_name}       Name of benchmark execution
+    ${benchmark_date}       Timestamp of benchmark execution
+    ${benchmark_path}       Directory of benchmark XML file
+    ${benchmark_path_abs}   Directory of benchmark XML file (absolute path)
+    ${benchmark_file}       Name of benchmark XML file (without path)
+    ${logfile_path}         Directory where tool-output files will be stored
+    ${logfile_path_abs}     Directory where tool-output files will be stored (absolute path)
+    ${rundefinition_name}   Name of current run definition
+    ${inputfile_name}       Name of current input file (without path)
+    ${inputfile_path}       Directory of current input file
+    ${inputfile_path_abs}   Directory of current input file (absolute path)
+
+For example, to pass as additional tool parameter the name of a file
+that is in the same directory as each input files, use
+
+    <option name="-f">${inputfile_path}/additional-file.txt</option>
+
+### Adopting benchexec for a specific tool
+In order to know how to execute a tool and how to interpret its output,
+`benchexec` needs a tool-specific Python module
+with functions for creating the appropriate command-line arguments for a run etc.
+Such modules need to define a class `Tool` that inherits from `benchexec.tools.template.BaseTool`.
+This class also defines the [documentation](../benchexec/tools/template.py)
+on how to write such a module.
+BenchExec already provides such [ready-to-use modules for some common tools](../benchexec/tools/).
+
+### Starting benchexec
+To use `benchexec`, simply call it with an XML file with a benchmark definition:
+
+    benchexec doc/benchmark-example-rand.xml
+
+Command-line arguments to `benchexec` allow to override the defined resource limits.
+If one wants to execute only a subset of the defined benchmark runs,
+the name of the `<rundefinition>` and/or `<inputfiles>` tags
+that should be executed can also be given on the command line.
+To start multiple executions of the benchmarked tool in parallel
+(if the local machine has enough resources),
+use the parameter `--numOfThreads`.
+Example:
+
+    benchexec doc/benchmark-example-rand.xml --inputfiles "XML files" --limitCores 1 --timelimit 10 --numOfThreads 4
+
+The full set of available parameters can be seen with `benchexec -h`.
+
+`benchexec` produces as output the results and resource measurements
+of all the individual tool executions in XML files
+from which tables can be created using `table-generator`.
+There is one file per run definition/tool configuration,
+and additional files for each subset of input files
+(all by default in directory `./result/`).
+A document-type definition with a formal specification of such result files can be found in
+[doc/benchmark-result.dtd](benchmark-result.dtd).
+The output of the tool executions is stored in additional files in a sub-directory.
+If the target directory for the output files (specified with `--outputpath`)
+is a git repository without uncommitted changes and the option `--commit`
+is specified, `benchexec` will add and commit all created files to the git repository.
+One can use this to create a reliable archive of experimental results.
+
+
+### Extending BenchExec
+BenchExec executes all runs on the local machine.
+In some cases, it might be desired to use for example some cloud service
+to execute the commands, and BenchExec should only handle the benchmark definition
+and aggregate the results.
+This can be done by replacing the module `benchexec.localexecution`,
+which is responsible for executing a collection of runs, by something else.
+To do so, inherit from the BenchExec main class `benchexec.BenchExec`
+and override the necessary methods such as `load_executor`
+(which by default returns the `benchexec.localexecution` module),
+`create_argument_parser` (to add your own command-line arguments) etc.
diff --git a/doc/runexec.md b/doc/runexec.md
new file mode 100644
index 000000000..3e857546f
--- /dev/null
+++ b/doc/runexec.md
@@ -0,0 +1,64 @@
+# BenchExec: runexec
+## Benchmarking a Single Run
+
+BenchExec provides a program called `runexec` that can be used to
+easily execute a single command while measuring its resource consumption,
+similarly to the tool `time` but with more reliable time measurements
+and with measurement of memory usage.
+To use it, simply pass as parameters the command that should be executed
+(adding `--` before the command will ensure that the arguments to the command
+will not be misinterpreted as arguments to `runexec`):
+
+    runexec -- <cmd> <arg> ...
+
+This will start the command, write its output to the file `output.log`,
+and print resource measurements to stdout. Example:
+
+    $ runexec echo Test
+    2015-03-06 12:54:01,707 - INFO - Starting command echo Test
+    2015-03-06 12:54:01,708 - INFO - Writing output to output.log
+    exitcode=0
+    returnvalue=0
+    walltime=0.0024175643920898438s
+    cputime=0.001671s
+    memory=131072
+
+Resource limits can be enabled with additional arguments to `runexec`,
+e.g. for CPU time (`--timelimit`), wall time (`--walltimelimit`),
+or memory consumption (`--memlimit`). If any of the limits is exceeded,
+the started command is killed forcefully (including any child processes it started).
+
+`runexec` can also restrict the executed command to a set of specific CPU cores
+with the parameters `--cores`,
+and (on NUMA systems) to specific memory regions with `--memoryNodes`.
+The IDs used for CPU cores and memory regions are the same as used by the kernel
+and can be seen in the directories `/sys/devices/system/cpu` and `/sys/devices/system/node`.
+
+Additional parameters allow to change the name of the output file and the working directory.
+The full set of available parameters can be seen with `runexec -h`.
+
+## Integration into other Benchmarking Frameworks
+
+BenchExec can be used inside other benchmarking frameworks
+for the actual command execution and handling of the resource limits and measurements.
+To do so, simply use the `runexec` command in your benchmarking framework
+as a wrapper around the actual command, and pass the appropriate command-line flags
+for resource limits and read the resource measurements from the output.
+If you want to bundle BenchExec with your framework,
+you only need to use the `.egg` file for BenchExec,
+no external dependencies are required.
+You can also execute `runexec` directly from the `.egg` file with the following command
+(no separate start script or installation is necessary):
+
+    PYTHONPATH=path/to/BenchExec.egg python3 -m benchexec.runexecutor ...
+
+From within Python, BenchExec can be used to execute a command as in the following example:
+
+    from benchexec.runexecutor import RunExecutor
+    executor = RunExecutor()
+    result = executor.execute_run(args=[<TOOL_CMD>], ...)
+
+Further parameters for `execute_run` can be used to specify resource limits
+(c.f. [runexecutor.py](../benchexec/runexecutor.py)).
+The result is a dictionary with the same information about the run
+that is printed to stdout by the `runexec` command-line tool.
diff --git a/doc/table-generator.md b/doc/table-generator.md
new file mode 100644
index 000000000..f17b497cf
--- /dev/null
+++ b/doc/table-generator.md
@@ -0,0 +1,31 @@
+# BenchExec: table-generator
+## Generating Tables of Results
+
+The program `table-generator` allows to generate HTML and CSV tables.
+It takes one or more XML files with results from `benchexec`
+and produces tables with columns for each of the files,
+such that all results for a given input file appear on the same line.
+To start it, simply pass all result files on the command line, e.g.
+
+    table-generator results/benchmark-example-rand.*.results.xml
+
+Further command-line arguments can be used to customized the table,
+e.g. for ignoring all incorrect results (`--correct-only`),
+or for specifying name and location of the table files (`--name`, `--outputpath`).
+The full set of available parameters can be seen with `table-generator -h`.
+
+`table-generator` also supports using a special file as input
+that defines the layout of the generated tables
+and allows even more customizations,
+including the ability to extract arbitrary values
+from the output of the tool of each run
+and inserting them into the table.
+Such table-definitition files are also in XML format
+and a complete definition can be found in the file
+[doc/table-generator.xml](table-generator.xml),
+and an example in [doc/table-generator-example.xml](table-generator-example.xml).
+A document-type definition with a formal specification of such files can be found in
+[doc/table-generator.dtd](table-generator.dtd).
+To use such files pass them with the parameter `-x` to `table-generator`:
+
+    table-generator -x doc/table-generator-example.xml