{"entities":{"Q40544":{"pageid":40600,"ns":120,"title":"Item:Q40544","lastrevid":105429380,"modified":"2026-10-09T10:11:53Z","type":"item","id":"Q40544","labels":{"en":{"language":"en","value":"CAVA LTL Modelchecker"}},"descriptions":{"en":{"language":"en","value":"AFP entry CAVA_LTL_Modelchecker"}},"aliases":{},"claims":{"P13":[{"mainsnak":{"snaktype":"value","property":"P13","hash":"d247ccec9396741686a7a4fe4e4e18aa915e92b5","datavalue":{"value":"28830","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40544$B5211423-E350-4FC5-BDF7-3916E5A38822","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"908c3454b3659c4b140ccce33c5aee31081edc8d","datavalue":{"value":{"entity-type":"item","numeric-id":5976450,"id":"Q5976450"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40544$3B4B3323-E29E-485F-84EE-87D89E978865","rank":"normal"}],"P29":[{"mainsnak":{"snaktype":"value","property":"P29","hash":"a5454d626e514b35e9a3ff6fa1961c95b8a571f1","datavalue":{"value":"https://www.isa-afp.org/entries/CAVA_LTL_Modelchecker.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q40544$0FCE9359-9DE6-4F42-A35D-A76664B2DBB7","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"0db99c3b17fc587dc6d0b047e5ff5ce0de1786ab","datavalue":{"value":"03","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40544$0CC50A76-EBBD-43D1-BE13-C161541F5805","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"95bde9084e6ca63a8492631a417b047b22c72453","datavalue":{"value":"05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40544$9585221C-C4F7-4894-A189-34A3149A1094","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"1a467a32e3049b1299c9c2b688461b7f273ec943","datavalue":{"value":"60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40544$C47BC0F6-8DC3-4F81-87D2-A59FE68FDA72","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"acf10290b955a69659a681d98822944f91bbad9e","datavalue":{"value":"68","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40544$FDA4B24B-3205-413C-9E6C-4583DDD9B89E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"541da1e359051dfcf3c498b9f1f1f8f905fbafe3","datavalue":{"value":"90","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40544$2769893A-795E-4211-AE49-7B8AE4B66F7C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a104733b1e30d91f56342777dc887a3edbb9e05f","datavalue":{"value":"65","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40544$780A91B4-A8E6-4D6E-8DC7-C62C90105E96","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"bebb7aa66b6973aa3a0c9749da8f6cd6626bb594","datavalue":{"value":"94","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40544$65FBFDE5-F6FB-4EFA-B347-13954C4FAE38","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"9ccfc2ffdb7a60cd36d8dca0a4e6d9d45f5228f3","datavalue":{"value":"3","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40544$50049A30-5538-480B-AA71-9E49A47A1D07","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"24f8ba20e8ffa07910d0666302c1f09a25449c97","datavalue":{"value":"5.0","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40544$050EBC6B-D63F-477B-9A2E-1141B4DF9FC9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"cb68336c6ece13b86917b0c80051f1685885b843","datavalue":{"value":"60.0","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40544$CDED108B-2B87-4CAF-9148-C6C58AA01BAD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"09f5e0c6033338f59ef27e37d6877da0f26d9646","datavalue":{"value":"68.0","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40544$FE44D2C7-9A61-4DE4-9FCF-066C27DBA10A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"1a8aa801742e290b2e6820d89349e86d8f23555f","datavalue":{"value":"90.0","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40544$D894EBB9-EBE4-4F1C-9479-84CF11D26B91","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"467910eb92f3fefb5ab991704afbc9c141aad063","datavalue":{"value":"65.0","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40544$38119A3B-86E5-41F8-8462-C6867C1E6F63","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"fb7b2d196cb181e838b342f41804d522dff44830","datavalue":{"value":"94.0","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40544$18450C29-1360-4278-8679-6E3F95E56FDD","rank":"normal"}],"P1458":[{"mainsnak":{"snaktype":"value","property":"P1458","hash":"a2a767ccd0e9bdc5b1b4a2069a6679f9340a857a","datavalue":{"value":{"entity-type":"item","numeric-id":14275,"id":"Q14275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40544$529A0508-0835-4531-ADA0-246FACB6A7A5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"03281999c3208b8f3a62eaceadadf1ce834fe219","datavalue":{"value":{"entity-type":"item","numeric-id":12929,"id":"Q12929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40544$40B8EE5F-51B3-4203-9FFB-9D517AD27FB1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"bb05cb23794774f62a8e4aa4de610af231973a1d","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40544$8661C742-A89D-4515-A2E1-A7DC99573657","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"ac6e4b2309e3317f96b1f72a4f626411283f5bc5","datavalue":{"value":{"entity-type":"item","numeric-id":40629,"id":"Q40629"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40544$10C39EA5-6950-4DB5-B1C2-52D06601062E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"ecda3e6d8e971c0b93d4cf3afb41990e853f830f","datavalue":{"value":{"entity-type":"item","numeric-id":13212,"id":"Q13212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40544$F82B7E32-6EA9-48FE-846A-D467E1E27E50","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"4eea1e5549472c93f3282a38917960fdec6b61a1","datavalue":{"value":{"entity-type":"item","numeric-id":24733,"id":"Q24733"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40544$2EC2FE5D-C82D-4A35-88A9-A05B99B857C4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"cc41d9364226bfa8139f8dbc43b1b77967245f13","datavalue":{"value":{"entity-type":"item","numeric-id":17631,"id":"Q17631"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40544$04E7478F-126F-4595-B319-09B23E4765B3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"7343f563fd02ee3f7d39ccb038f5c1c6c726769a","datavalue":{"value":{"entity-type":"item","numeric-id":20799,"id":"Q20799"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40544$29419143-7E0D-402E-9345-A33770B74D0A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"ed15eb8701a335444fde1bcc3327d1067ce64751","datavalue":{"value":{"entity-type":"item","numeric-id":24376,"id":"Q24376"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40544$7BFA8686-5B45-46FE-A557-020CDD50EE1E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"0566ad334499237f2689386a24c3ff4452487d83","datavalue":{"value":{"entity-type":"item","numeric-id":15987,"id":"Q15987"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40544$79699292-7FA7-496D-9A60-F984BF2B9120","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"8533330b9fa0c1f7979d4af1d0e8bdba3ffc811c","datavalue":{"value":{"entity-type":"item","numeric-id":56651,"id":"Q56651"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40544$DD702612-61B2-46DD-AF95-FD66221ADC26","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"ccca80b6de24b80a4ce2a4ab4e48d31e9686f36a","datavalue":{"value":{"entity-type":"item","numeric-id":40262,"id":"Q40262"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40544$8E0FC84A-F60C-4D30-BF67-6F92D968F343","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"144f0221487b5ba035abaca0f440960a9e47efeb","datavalue":{"value":{"entity-type":"item","numeric-id":27113,"id":"Q27113"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40544$F97E8C24-9485-4AD7-BB15-8FF8D18750FE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"7434bcf5c727d2c07e931aea1694436d0b39cd53","datavalue":{"value":{"entity-type":"item","numeric-id":27041,"id":"Q27041"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40544$017D8BE5-461E-47B7-BE57-875AF0B3B53E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"f70e8f897325b539c702d8d7cb97dfafe554224c","datavalue":{"value":{"entity-type":"item","numeric-id":32823,"id":"Q32823"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40544$120FA37B-970D-479A-A985-5E8F57D60AF6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"9ad8338290e864661fc95f2a66261cf7e07a407c","datavalue":{"value":{"entity-type":"item","numeric-id":32822,"id":"Q32822"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40544$E314DB63-3FF7-4186-9815-5BE4B5DCB88C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"8dde418bf28e22fefe1976bd953eb7c8ec5b548d","datavalue":{"value":{"entity-type":"item","numeric-id":16770,"id":"Q16770"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40544$8DCE6400-C9A9-43F6-AE39-94475F83CD4F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"ab75a27745b95bbc51eed60e2ef7157b7c449125","datavalue":{"value":{"entity-type":"item","numeric-id":33768,"id":"Q33768"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40544$99A7D74F-A5CE-427C-BB31-BD56ED39938B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"07eb0f28b45c8f9b5cf112bbf02e95717fb938ca","datavalue":{"value":{"entity-type":"item","numeric-id":25202,"id":"Q25202"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40544$874C17B3-0194-4701-81A6-F26A28598E65","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"587eb1ff352d74d75ec39594cac10abdfc1440c2","datavalue":{"value":{"entity-type":"item","numeric-id":40265,"id":"Q40265"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40544$2A5DD55C-BBCF-4E3A-9DD1-57B684F0C77D","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"3140845d40a69cd5a5d66cbaec3315ca4fca43f1","datavalue":{"value":"https://isa-afp.org/entries/CAVA_LTL_Modelchecker.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q40544$96172564-28BF-450F-BE09-6CE0C22EC2E2","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"3629029537b4815531613478c102e8346a275f5b","datavalue":{"value":"Javier Esparza","type":"string"},"datatype":"string"},"type":"statement","id":"Q40544$FD1029C9-AD34-418D-9A5E-1A667BF42340","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"7545c5768cca6bd4b47e52bfec18c22cb81849df","datavalue":{"value":"Peter Lammich","type":"string"},"datatype":"string"},"type":"statement","id":"Q40544$0679FB14-3A85-4B3E-8462-88EF8CA083C9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"0ecc22d00a75bcea18b023112e4b2e17fe97020a","datavalue":{"value":"Ren\u00e9 Neumann","type":"string"},"datatype":"string"},"type":"statement","id":"Q40544$2812ABE8-508A-4CAD-A292-B2E698D9A7A7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"78083bbf5b06a4f292e9e00ee445948e4fa51db5","datavalue":{"value":"Tobias Nipkow","type":"string"},"datatype":"string"},"type":"statement","id":"Q40544$BE400749-4E28-4D1B-9FEA-DDE352032A1A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"493dbd4a2996bd8d532db178e854c885e9335058","datavalue":{"value":"Alexander Schimpf","type":"string"},"datatype":"string"},"type":"statement","id":"Q40544$71A5B8E8-87A7-40DE-89F5-0A15C9855349","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"eb47f8ac38607e782d3ab308bb9dc9c3bd87e37f","datavalue":{"value":"Jan-Georg Smaus","type":"string"},"datatype":"string"},"type":"statement","id":"Q40544$10F28B57-69EE-4F0E-8CE2-D885E16B9EB9","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"cf6d73504760825d415607e0aa38dd950421ee53","datavalue":{"value":"We present an LTL model checker whose code has been completely verified using the Isabelle theorem prover. The checker consists of over 4000 lines of ML code. The code is produced using the Isabelle Refinement Framework, which allows us to split its correctness proof into (1) the proof of an abstract version of the checker, consisting of a few hundred lines of \u201cformalized pseudocode\u201d, and (2) a verified refinement step in which mathematical sets and other abstract structures are replaced by implementations of efficient structures like red-black trees and functional arrays. This leads to a checker that, while still slower than unverified checkers, can already be used as a trusted reference implementation against which advanced implementations can be tested.","type":"string"},"datatype":"string"},"type":"statement","id":"Q40544$2DE71700-B8DF-4425-92F1-1EDCFED971A3","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"31067e58485990e94b288d36b9237062670ad8fb","datavalue":{"value":{"entity-type":"item","numeric-id":4356435,"id":"Q4356435"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40544$B760BE17-9D30-4047-B197-4BF7364A30B3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2235cb100f2692698d1e78c89e440355cd4f7add","datavalue":{"value":{"entity-type":"item","numeric-id":2879261,"id":"Q2879261"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40544$887371D6-FEDF-4B11-A591-1CCCDAE35C4D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"829c2fc52e5b12c8e00ff0f0fcc73378436c283b","datavalue":{"value":{"entity-type":"item","numeric-id":5703757,"id":"Q5703757"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40544$3218E29C-84DC-4F3A-93CA-F4AB2777CA1F","rank":"normal"}],"P585":[{"mainsnak":{"snaktype":"value","property":"P585","hash":"57153f9096aa0dddca483f863db49f1a20c72ecc","datavalue":{"value":{"entity-type":"item","numeric-id":7361530,"id":"Q7361530"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40544$91ED5CFD-53BF-419F-860E-7C5228984358","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"c0e4b154d3cbaa6adcd084b741855073f781fcfd","datavalue":{"value":{"entity-type":"item","numeric-id":7361011,"id":"Q7361011"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40544$7ABDFC4B-B8AB-4A1A-8493-166DE407C92E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"fd79867ce10ec25799473c4691ec619caa547136","datavalue":{"value":{"entity-type":"item","numeric-id":7361723,"id":"Q7361723"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40544$427C3A0F-143A-4551-A5A8-F38130BCD67C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"b624f9adb4e4340b0d07df82b6bfbae1c5626990","datavalue":{"value":{"entity-type":"item","numeric-id":7361954,"id":"Q7361954"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40544$EBD943CE-4B9F-48F0-BEB0-3406B4710C24","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"cabe8e3c8776c0f4fa7d4470a5e10fb258975536","datavalue":{"value":{"entity-type":"item","numeric-id":7361937,"id":"Q7361937"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40544$23D0F54E-0DE2-4FEB-A2CD-B3DB8616A7C8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"734e2b7032c0842d1b31ef498b1859b885488686","datavalue":{"value":{"entity-type":"item","numeric-id":7361062,"id":"Q7361062"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40544$9FB72E71-2E5B-4737-8842-83E28373023D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"e311985e283a0fa73130406ac266a6c4f80c0424","datavalue":{"value":{"entity-type":"item","numeric-id":7361873,"id":"Q7361873"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40544$0B581641-7D94-47A1-B3DB-0F918CF5B8F9","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"a696f05378d1338ede6149124bc9da54876abcc7","datavalue":{"value":{"time":"+2014-05-28T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q40544$A01F2D4B-D213-4BF0-92BB-D07580C22883","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"6d853b2cf6d3d24be7c916e313d33bcf9ab312cb","datavalue":{"value":{"text":"A Fully Verified Executable LTL Model Checker","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q40544$49E784BE-B365-4D58-B853-19E64686AC77","rank":"normal"}],"P37":[{"mainsnak":{"snaktype":"value","property":"P37","hash":"9a21a8eebe97539644aa32b24dda137c12e751dc","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40544$E311E798-3632-4D9C-9AE5-6EFF16AFFDE7","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"73d93a21b0749f7f2c51d7daeb11b162660cd756","datavalue":{"value":{"entity-type":"item","numeric-id":7360784,"id":"Q7360784"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40544$6CFD523E-37FB-4239-B3E8-31AD8A650504","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"CAVA LTL Modelchecker","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/CAVA_LTL_Modelchecker"}}}}}