diff --git a/README.md b/README.md
index 4b8c0b2491..74bf6f0982 100644
--- a/README.md
+++ b/README.md
@@ -21,9 +21,11 @@ Currently, the following 3 tools are available.
 Follow the links for more information about each tool.
 
 * [`theta-cfa-cli`](subprojects/cfa-cli): Reachability checking of error locations in Control Flow Automata (CFA) using CEGAR-based algorithms.
-  * [Gazer](https://github.com/FTSRG/gazer) is an LLVM-based frontend to verify C programs using theta-cfa.
+  * [Gazer](https://github.com/FTSRG/gazer) is an [LLVM](https://llvm.org/)-based frontend to verify C programs using theta-cfa-cli.
+  * [PLCverif](https://cern.ch/plcverif) is a tool developed at CERN for the formal specification and verification of PLC (Programmable Logic Controller) programs, supporting theta-cfa-cli as one of its verification backends.
 * [`theta-sts-cli`](subprojects/sts-cli): Verification of safety properties in Symbolic Transition Systems (STS) using CEGAR-based algorithms.
-* [`theta-xta-cli`](subprojects/xta-cli): Verification of Uppaal timed automata (XTA).
+  * theta-sts-cli natively supports the [AIGER format](http://fmv.jku.at/aiger/) of the [Hardware Model Checking Competition (HWMCC)](http://fmv.jku.at/hwmcc/).
+* [`theta-xta-cli`](subprojects/xta-cli): Verification of [Uppaal](http://www.uppaal.org/) timed automata (XTA).
 
 ## Extend Theta