Talk:List of model checking tools

Hi to all!

My idea is to create a wiki page in which Model Checking Tools can be listed; I would write something like this Comparison_of_wiki_software.

Here the only MC tools list that I've found in wiki, but there is [this] database where a lot of tools are listed.

I cannot index all the tools, help me to expand the table.

PoorUser (talk) 13:39, 6 October 2009 (UTC)

Alloy

Someone please add Alloy (http://alloytools.org/), I'm not too sure of what to put in some columns so can't do it myself. JidGom (talk) 21:58, 19 September 2019 (UTC)

"FUSC" license?

I see here a lot of tools with "FUSC" license... googling for "fusc license" redirects me to this very page on wikipedia... — Preceding unsigned comment added by 157.193.9.165 (talk) 16:01, 7 September 2011 (UTC)

I'm just guessing here, but I think "FUSC" stands for "Free Under Special (or Specified) Conditions" (actually, I've just realised it says so [with "Specific" for S] in the key at the bottom of the page). In most cases, this seems to amount to "free for academic use only". In one or two cases, the project is actually under a Free (as in freedom - i.e. open-source) licence, but is mislabelled as "FUSC". -Spacemartin (talk) 18:02, 6 January 2015 (UTC)

Graphical specification?

I wonder what graphical specification means?

Vandalism? (2018)

We have been informed by our computer science students at Univ. Grenoble Alpes that most entries of this page had been deleted by user Chrissymad in March 2018.

The reason for such deletions is unclear ("not linkfarm") and the deletion seems to have been made on a random basis, as most deleted entries correspond to actual model checkers well known from the scientific community, for which published articles or even books exist. The result is a blatantly incomplete list of model checking tools.

The deletion was undone, but user Chrissymad did it again, still without explanation, removing later additions as well. So, we had no other choice than restoring again and complain about this situation.

It is a fact of life that the formal verification community is active and that universities of many countries compete and co-operate to develop many model checkers. This should be accepted as is, rather than making a random selection of a handful tools.

Vasywriter (talk) April 26 2018 (UTC)

Vasywriter I explained in both my edit summaries why it was removed. The onus is on you to provide reliable sources which support their inclusion and you've not done so. Wikipedia isn't for listing everything that exists. Please also note that the English Wikipedia does not allow shared accounts. CHRISSYMAD ❯❯❯¯\_(ツ)_/¯ 17:27, 26 April 2018 (UTC)

Wikipedia is not a link farm. Please stop re-adding external links to those webpages. SQL^{Query me!} 17:32, 26 April 2018 (UTC)

1. Sorry but, besides a very general statement about what Wikipedia should be or not, you did not mention any objective criterion why certain tools have been dropped and others kept. It is your responsibility to justify why you suddenly and selectively delete scientific information written by many different users.

2. Specifically, consider the following scientific paper from ISTI-CNR, Pisa, Italy ("Ten Diverse Formal Models for a CBTC Automatic Train Supervision System"). This is a 3rd-party paper from a serious academic institution, and it is recent too. The authors evaluate 10 model checkers on a common case study of the railway industry. You removed 4 of these model checkers from Wikipedia. Why? -Vasywriter (talk) 20:30, 26 April 2018.

Chrissymad, please explain the criteria you used to alter the list of model checkers. For instance, why did you decide to remove the TLA+ tool, written by a Turing award winner, while keeping the DREAM tool, a prototype tool (still in version beta 0.7 on Sourceforge) developed by a PhD student between 2005 and 2009?

Vasywriter (talk) April 28 2018 (UTC)

I have already explained it, as did SQL. CHRISSYMAD ❯❯❯¯\_(ツ)_/¯ 18:37, 2 May 2018 (UTC)

Sorry, the question does not concern your (or someone else's) opinion on this page, but your own actions. So far, you failed to provide any justification for the selective deletions you brought. Please contribute to the discussion. Any proposal for consensus? --Vasywriter (talk) 09:31, 5 May 2018 (UTC)

I agree that there should be a list of criteria for deciding whether a model checker should be listed or not. How about the following to start with:

1. Availability: The model checker is available for download, either from a commercial shop or from a project web site.
2. License: The model checker has a declared license, such that a user can find out what one is allowed to do with it.
3. Visibility: The model checker (a description of it) was published in archived literature.

@ Vasywriter, Chrissymad, SQL: Do you agree with the above list?

I recommend to add one more column: Participation in comparative evaluations or competitions.

-- Dirk Beyer (not an active Wikipedia user) — Preceding unsigned comment added by 88.133.199.106 (talk) 19:45, 8 May 2018 (UTC)

Detailed analysis of the deletions performed by Chrissymad

On March 10, between 19:14 and 19:34, Chrissymad deleted contents in 10 different Wikipedia articles, many of which dealing with software (neuroimaging, spectrometry, interactive geometry, etc.) but also with startups in Pakistan or Armenian and Indian journalists.

In the present article, 36 entries were deleted in one single minute (between 19:32 and 19:33).

For these deletions, Chrissymad left the following edit summary: "rmv linkfarm, unsourced, nn".

This is blatantly false:

• The three internal links that have been removed (BLAST, CADP, and TLA+) were properly sourced with 4, 10, and 25 references, respectively.

• The "nn" claim is also wrong, as most of these tools are perfectly notable. For instance, the TLA+ model checker has been developed by Turing award winner Leslie Lamport. Also, ESBMC tool has won too medals at the 6th International Competition on Software Verification (2017).

• The three criteria proposed by Prof. Dirk Beyer are quite reasonable. Investigation shows that 26 out of the 36 tools deleted by Chrissymad satisfy all these three criteria.

Chrissymad, in light of these remarks, would you agree to revert your changes? --Vasywriter (talk) 17:27, 15 May 2018 (UTC)

Vasywriter Then you should have no problem writing an article for each of them and then adding them to the list so that they meet inclusion criteria. CHRISSYMAD ❯❯❯¯\_(ツ)_/¯ 17:41, 15 May 2018 (UTC)

Is the following list of criteria complete then?

1. Availability: The model checker is available for download, either from a commercial shop or from a project web site.
2. License: The model checker has a declared license, such that a user can find out what one is allowed to do with it.
3. Visibility: The model checker (a description of it) was published in archived literature.
4. Wikipedia Presence: The model checker needs to have a Wikipedia page describing it.

If yes, could you please re-add all model checkers that satisfy the four criteria, Vasywriter or Chrissymad? That would be great! (And I would prefer to mention these criteria in the article, not only here on the talk page, such that readers can understand why one is included and another not.) Dirkbeyer (talk) 05:51, 16 May 2018 (UTC)

Is availability enough? How about maintenance? I infer from its buglist that BLAST, for example, has been dormant for over a decade. Another model checker whose website is similarly comatose is SLAM, which is not on the list although it appears to meet the listing criteria.

As Wikipedia carries articles about long-dead software, it may be appropriate to include obsolete checkers and record availability and vitality in a "status" column. There is often more interest in pioneering systems than in their surviving descendents. Mdmi (talk) 02:24, 31 March 2024 (UTC)

Done. Can you proceed by inserting in the page the criteria you proposed, so that cleaning can be done next on the basis of these criteria? Thanks --Vasywriter (talk) 11:03, 18 May 2018 (UTC)

Done with including the criteria on the Article page and hope this is helpful for similar situations in the future. Dirkbeyer (talk) 22:48, 22 May 2018 (UTC)

TCTL now forwards to TTL

Presumably TCTL is a variant of CTL, but the TCTL page now redirects to Two-transistor logic. Would it be reasonable to change the TCTL links to CTL, or should TCTL be made into a disambiguation page? — Preceding unsigned comment added by 166.70.31.28 (talk) 18:38, 19 August 2019 (UTC)