{"entities":{"Q2979849":{"pageid":2990574,"ns":120,"title":"Item:Q2979849","lastrevid":52791956,"modified":"2026-01-23T12:39:16Z","type":"item","id":"Q2979849","labels":{"en":{"language":"en","value":"Formal verification of programs for abstract register machines"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6708328"}},"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":"Q2979849$1992FEBB-2BD7-43AE-9DC7-8C2D3460327E","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"b56a6011068237cffe9e66a8317c03d2f145ffa9","datavalue":{"value":"1374.68275","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2979849$400A2862-6B3D-439F-B9AD-0AFF68EB4EB0","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"780337e612606e6b0cfc1a9e4d31030a02569608","datavalue":{"value":{"entity-type":"item","numeric-id":2729919,"id":"Q2729919"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2979849$7725ACCA-2222-4346-A2A2-4450C38D6731","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"f12ab6a50dca285e32f059f3cef41583e61bc6ed","datavalue":{"value":{"entity-type":"item","numeric-id":174086,"id":"Q174086"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2979849$B1666803-2BB1-430E-BC7C-122773EC7848","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"5136aa5d1d5384ee622607c2cb579d682b7a682f","datavalue":{"value":{"time":"+2017-04-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":"Q2979849$7F24A7EF-5AF8-4CF5-9EB7-59EE30FC7072","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"676b138861cd176e42e4b38c451328820d2be470","datavalue":{"value":"http://bulletin.iis.nsk.su/files/article/chkliaev.pdf","type":"string"},"datatype":"url"},"type":"statement","id":"Q2979849$B1EE1B45-42DF-4D11-87D4-6CB6CEDD632A","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2979849$724C7B4E-58BD-4B01-9DB9-D6D2E4A338C5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a7dde57cbaf704d564d8f981ca98d6340e3d4aaf","datavalue":{"value":"68Q05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2979849$44CB985A-9B5D-4F36-8A17-348AA9C2DA74","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2979849$309E28DC-28CE-4BBD-BABC-35932248AC0F","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"fb46635510d4378a23b6be1ab5320844374a1f08","datavalue":{"value":"6708328","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2979849$704263BE-9634-4455-B099-808ABBD6BFD5","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5072102dc4d0eddabb24928f1a99263ee32cc5d1","datavalue":{"value":"abstract register machines","type":"string"},"datatype":"string"},"type":"statement","id":"Q2979849$D55CD207-AB13-406E-B726-479004C9A2D6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5f9db6f5f97e6e3ddf1d32daa1cd8a15b07ef492","datavalue":{"value":"random-access machines","type":"string"},"datatype":"string"},"type":"statement","id":"Q2979849$75F2F665-23EA-42A5-AE77-44F893288E2B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"87994eb840961e5165378eb7f918102952689b42","datavalue":{"value":"formal specification","type":"string"},"datatype":"string"},"type":"statement","id":"Q2979849$856EFF2E-1B7A-477D-A7B9-2EDCC7087163","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a5c8ba46ca3cfc960c989c4fc1677ad7c552dab4","datavalue":{"value":"automated verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q2979849$FE0B9EA0-F580-4A80-8B59-01571AE7C301","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"21cf102e52d55bb9e3ba4ca1c32b8839281988dc","datavalue":{"value":"interactive theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q2979849$E533215A-A485-40A0-BB35-782C3DE616EB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"14b5e090dbc9bcb80548540aca8b83d5cf21b1b3","datavalue":{"value":"verification system PVS","type":"string"},"datatype":"string"},"type":"statement","id":"Q2979849$47C1181E-5441-46EF-82CD-ED0BF9C47B17","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c46d84e301480ba8a5854ea89c3d27b865a03eb9","datavalue":{"value":{"entity-type":"item","numeric-id":16016,"id":"Q16016"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2979849$0510098A-1861-453E-8C97-1E7AC5C4315C","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":"Q2979849$1C4D38DA-4316-4C1E-9A4C-196C4BB27B2E","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"31b4875c72be6699ef595f44c08d6b0619d8b03c","datavalue":{"value":{"entity-type":"item","numeric-id":2979871,"id":"Q2979871"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8af3307b657613ae23559c10ec9042447cee8070","datavalue":{"value":{"amount":"+0.8636382818222046","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":"Q2979849$F4CA4307-6B59-4584-8516-D2290682E56D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"747262510cb6b2d1e886a4e3f4a91d7ce069382a","datavalue":{"value":{"entity-type":"item","numeric-id":4818811,"id":"Q4818811"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b49b4741327fbf4007d0f3bebf411f8b92bfc645","datavalue":{"value":{"amount":"+0.7619984149932861","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":"Q2979849$42BC39F1-292E-41D1-8977-D39CB3E60BC5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2a76b3577a7618bb02f9806580f51d2b7da93b94","datavalue":{"value":{"entity-type":"item","numeric-id":5900551,"id":"Q5900551"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"40abbc1d8bb0a54df5e538400b8a8c6b46f670b3","datavalue":{"value":{"amount":"+0.728577733039856","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":"Q2979849$074EF1E5-1519-44CC-AF56-D27DC1F36AEF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3a6f50e448f9d59543880222f04826077ababfca","datavalue":{"value":{"entity-type":"item","numeric-id":3806803,"id":"Q3806803"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"550b34d8dcebc1ebedd704593818342e492dcda8","datavalue":{"value":{"amount":"+0.7224977612495422","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":"Q2979849$21F54486-E072-4EC2-BCA3-4A39AB224EF5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4272bd6738545a81c2018c26962d92a456a460e5","datavalue":{"value":{"entity-type":"item","numeric-id":3132070,"id":"Q3132070"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"dc646a6bcb9948a152c66c38eaa77271a72b7ffd","datavalue":{"value":{"amount":"+0.7163974046707153","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":"Q2979849$1B46A3C8-6813-401E-BEA2-E9F15B9B7B51","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2979849","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2979849"}}}}}