{"entities":{"Q2848674":{"pageid":2859394,"ns":120,"title":"Item:Q2848674","lastrevid":79757252,"modified":"2026-05-06T14:38:35Z","type":"item","id":"Q2848674","labels":{"en":{"language":"en","value":"Using satisfiability modulo theories for inductive verification of Lustre programs"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6212125"}},"aliases":{},"claims":{"P31":[{"mainsnak":{"snaktype":"value","property":"P31","hash":"fd5912e4dab4b881a8eb0eb27e7893fef55176ad","datavalue":{"value":{"entity-type":"item","numeric-id":56887,"id":"Q56887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2848674$FBC34D04-3996-4236-B135-D9A7BB117EEE","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"512808c6e106b4f6323d2e58f9d8fb16c9d8ba7c","datavalue":{"value":"1272.68103","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2848674$39A567E8-F372-46E3-98C2-2C64F69445ED","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"4cd48eb61e203d5044e95bf99a9a9627aeaf2505","datavalue":{"value":{"entity-type":"item","numeric-id":1037398,"id":"Q1037398"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2848674$A28EF698-088B-4509-A2AB-F1F9D4C38500","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"43e878d8f753446abefa1b1ceb0637b91afae47a","datavalue":{"value":{"time":"+2013-09-26T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2848674$7CDEE773-3881-4ACF-B687-99ED59ECFAAC","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"48eb4bca44add03eca9d0f2a712162588973fb48","datavalue":{"value":"http://www.sciencedirect.com/science/article/pii/S1571066105052412","type":"string"},"datatype":"url"},"type":"statement","id":"Q2848674$18FC1188-D8D9-4A95-9892-C22978D171D8","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2848674$2B99903F-6D6C-4C49-BFF4-6E2E8B1330D6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2848674$21DDC181-B176-432D-BBA7-A62643646A05","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"8ba8c177fe4dd33ea116b6c29b311342e00d39f8","datavalue":{"value":"6212125","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2848674$BF261C98-A36A-4A50-ADAB-C218D744916E","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"57f7fea50d2ce1b39b695c4a1313582eed405e38","datavalue":{"value":{"entity-type":"item","numeric-id":5976449,"id":"Q5976449"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2848674$F92B450C-66FC-4634-AEC0-B367A51FDD2C","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"f5c1b560eec929eb74d61fd0bf60d6972c552f2a","datavalue":{"value":{"text":"Using satisfiability modulo theories for inductive verification of Lustre programs","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2848674$5A4084F2-5352-4603-B6C8-EA06437FBC95","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"cf7c2dc62b8b21f444af3aa6abb5b63e601c5fb0","datavalue":{"value":{"entity-type":"item","numeric-id":2767016,"id":"Q2767016"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7b49c6bc2f92997599a02a5b1c7ef6752a26f021","datavalue":{"value":{"amount":"+0.7616645097732544","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2848674$FA477204-BE76-4882-AE12-7D88B7511B33","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"18ba98873d052f5816175646d512a17079b79c03","datavalue":{"value":{"entity-type":"item","numeric-id":3176369,"id":"Q3176369"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"94c6eca5483b931847148f4a617c39f75a9a0b94","datavalue":{"value":{"amount":"+0.7387425303459167","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2848674$33113896-ECEC-40D3-B1B9-BE2C64AC2538","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f1f943c54080b27de44312af7634875e7f707904","datavalue":{"value":{"entity-type":"item","numeric-id":5716582,"id":"Q5716582"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9cb703e2ee162bcb405efc1bb4aa8ec84e577e1f","datavalue":{"value":{"amount":"+0.7336203455924988","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2848674$E3202970-2353-4097-A02C-B379AB8AA154","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"193b6443352a3258f81fe7b2e5abf39f12aa60c8","datavalue":{"value":{"entity-type":"item","numeric-id":2845506,"id":"Q2845506"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"13c14e1529be02da318b4969bc917832b8b20d0e","datavalue":{"value":{"amount":"+0.7284640669822693","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2848674$3ECD9765-C401-439A-B71F-91B285F09594","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"392ac13dbf2c0c769ffa081dea87f7e451e65522","datavalue":{"value":{"entity-type":"item","numeric-id":1323369,"id":"Q1323369"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1c611c83a646501af24034b3fd7ae69cfa7572b4","datavalue":{"value":{"amount":"+0.7263173460960388","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2848674$F2F46FC3-586A-4EBF-AB19-9C446CCF412F","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Using satisfiability modulo theories for inductive verification of Lustre programs","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Using_satisfiability_modulo_theories_for_inductive_verification_of_Lustre_programs"}}}}}