From 8917147eeeaeaa0b75426f1c850a93d52e38718d Mon Sep 17 00:00:00 2001 From: Akos Hajdu Date: Tue, 11 Aug 2020 21:37:32 +0200 Subject: [PATCH] Add some details on frontends in readme --- README.md | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) 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