{"entities":{"Q937300":{"pageid":939148,"ns":120,"title":"Item:Q937300","lastrevid":65482395,"modified":"2026-04-12T02:53:30Z","type":"item","id":"Q937300","labels":{"en":{"language":"en","value":"Compositional verification of sequential programs with procedures"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5312289"}},"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":"Q937300$F54FF933-1075-4898-A352-6EB4EE7AE9A0","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"e2e19ac05929b3e72e4a97e950ba7f771c54cbb8","datavalue":{"value":{"text":"Compositional verification of sequential programs with procedures","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q937300$E5C9CF69-1868-4CD6-9595-3025C0DAC4CD","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"cccca15214e4c8d1ac9e80abb4e64560093b8ec3","datavalue":{"value":"1153.68036","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q937300$3AE05B75-552F-42DB-990F-C1EFED1C9734","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"8de0358d5843909f727261d501d479a1091d2554","datavalue":{"value":{"entity-type":"item","numeric-id":385022,"id":"Q385022"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q937300$B6A91AEF-59A4-49A8-AA1D-C10B095F20E9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"3772d5f7c7aac4e0fdecccd336d0d84f954a370a","datavalue":{"value":{"entity-type":"item","numeric-id":225075,"id":"Q225075"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q937300$0DA6609C-0791-4FD5-90F8-8A410EEC1857","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"42fd711c82655f9391f9c9ac0883e7ae53c27ad3","datavalue":{"value":{"entity-type":"item","numeric-id":937299,"id":"Q937299"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q937300$9E2036A7-4EBE-4332-B981-A15B5730C860","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"fa2d1ad91af9619c8dd37ab889fe279a84c4057e","datavalue":{"value":{"entity-type":"item","numeric-id":259032,"id":"Q259032"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q937300$A5301675-20D7-4621-A7E0-8EBEAA774147","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"37dcd1680f174cc4709a12092d5efd1d01f69bf2","datavalue":{"value":{"time":"+2008-08-14T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q937300$4AEEC734-A527-43CA-85D6-C273D3430771","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q937300$274C8372-B625-4FBE-935B-047D2CAF7624","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q937300$F328C9E8-B92B-4A7B-96BF-A546B343B426","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"f37c9d67830fde98487e7e273354c17a91a1a626","datavalue":{"value":"5312289","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q937300$73E6D9A0-575F-4409-9D04-FDB40A26B16A","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c50d987ab7c3ea2a41cb6aca681d912964971ed8","datavalue":{"value":"program verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q937300$ECFAED3E-79D3-49BC-B176-3A57319B247E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7826a90d3092607baa9d65a6435192c15dce600c","datavalue":{"value":"control-flow behaviour","type":"string"},"datatype":"string"},"type":"statement","id":"Q937300$7C4D437C-21A4-4443-A207-9FC2208034CC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d8f9062a19f85971c14b4d71d981f064b7b13591","datavalue":{"value":"compositional reasoning","type":"string"},"datatype":"string"},"type":"statement","id":"Q937300$3539A2F3-16BD-4CC3-A822-28EE96FFB0D9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"70385047063e32e899a03bc21d34ece5ee0e5655","datavalue":{"value":"modal \\(\\mu \\)-calculus","type":"string"},"datatype":"string"},"type":"statement","id":"Q937300$4F6ECCBA-BB13-4EB3-B76E-249EED458F31","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"0e07787a1cd26c789140f5c3150ac09bb65f07f7","datavalue":{"value":"safety properties","type":"string"},"datatype":"string"},"type":"statement","id":"Q937300$C9ABBB9E-2172-407A-A851-9A6E04818FEE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"087e2bcc5afb7e5ed3a2f2e6c0eca58a80e1602b","datavalue":{"value":"maximal model","type":"string"},"datatype":"string"},"type":"statement","id":"Q937300$BD7F81DD-0911-4F81-8444-B7473A54C75C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"70dee8a3f09645e8fb3a5797785fcda4ea76ab43","datavalue":{"value":"private procedures","type":"string"},"datatype":"string"},"type":"statement","id":"Q937300$D1D5EA60-1772-42D7-A909-412B4AECD6DF","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"7f001eb735991a93b9abcf6784d2099d4ede049e","datavalue":{"value":{"entity-type":"item","numeric-id":19681,"id":"Q19681"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q937300$519DCE6E-B8DF-4369-9E54-A1D360BD08D5","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":"Q937300$7C79057D-6885-4131-AA9F-095619E600D0","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"a78c833f02ae8df9ee5f9262da1c14e65c523847","datavalue":{"value":"https://doi.org/10.1016/j.ic.2008.03.003","type":"string"},"datatype":"url"},"type":"statement","id":"Q937300$8B982D2F-E96C-4C2E-AA68-2AF60961B643","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"9adde7f21dcde8005f054f08ae0d3562910674a8","datavalue":{"value":"W2034063260","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q937300$94D7C226-DD17-471A-9967-1AB967B71F04","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"a133b2b9476ffc4401b56d83bdfd1f487592e7be","datavalue":{"value":{"entity-type":"item","numeric-id":2754086,"id":"Q2754086"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q937300$963251F9-F355-451F-8FA3-7B9CBADF2BE4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7f7d1afa57ee8c8dbc48f47ac1b2806dcd78e44d","datavalue":{"value":{"entity-type":"item","numeric-id":4738309,"id":"Q4738309"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q937300$C00AC507-A954-4443-B027-6FE41D134000","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1f5a45904f81b6a39ede475e2e86ab18eb54c04e","datavalue":{"value":{"entity-type":"item","numeric-id":801893,"id":"Q801893"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q937300$47695FA4-936C-4028-BBD9-F17B7F6349FD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"48ec8cdee5c993dff7cc7451da7a82da8eaf8ea9","datavalue":{"value":{"entity-type":"item","numeric-id":4036555,"id":"Q4036555"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q937300$A336400E-F65B-482C-BD23-DB28AAD11FD7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e78abf06cd43bc8b5469b6b54f3aaf21e033b53e","datavalue":{"value":{"entity-type":"item","numeric-id":2760246,"id":"Q2760246"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q937300$9D5F84E3-FD7B-4BD7-8389-42646196E8EB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"440830e13930465acffe0122175a4a04e8328aff","datavalue":{"value":{"entity-type":"item","numeric-id":5756743,"id":"Q5756743"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q937300$3EB3420A-39F0-43CF-A50D-5B9FB21AF880","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4b6196bb057adc2087bd5262ca2bda33f9a480e1","datavalue":{"value":{"entity-type":"item","numeric-id":5308427,"id":"Q5308427"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q937300$C6ED9AD7-E90D-4C41-AB2D-6D9AF2D572D8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"12e4059e3e3788a873388fc3b6237dcbc3b49d09","datavalue":{"value":{"entity-type":"item","numeric-id":2768503,"id":"Q2768503"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q937300$9C7E76BF-36CE-43B8-B127-7A4401603F2F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6bf041137b656f4944d9f4b0e4049736dafdf62d","datavalue":{"value":{"entity-type":"item","numeric-id":5311128,"id":"Q5311128"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q937300$CD257269-50BA-40C0-9FA0-03AD59272F6B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"875736f390fbee8f5115e55c84e89462043693ee","datavalue":{"value":{"entity-type":"item","numeric-id":685358,"id":"Q685358"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q937300$16FA85C9-B3D7-44CC-83F2-AF4BE9E808D0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3f1166c2c780e84fac7578b928060fa8bdd72e28","datavalue":{"value":{"entity-type":"item","numeric-id":1188590,"id":"Q1188590"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q937300$3D3652E3-30DE-4A58-B25D-3368C26862E1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cf8ebc11e5152a7aaca233f3b6037de5f36fc738","datavalue":{"value":{"entity-type":"item","numeric-id":3766826,"id":"Q3766826"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q937300$A8EC6DB7-6499-4D97-9A63-FCA9F9781D91","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"98f488ca0bee76ae556527d1ce554b7c31a7e653","datavalue":{"value":{"entity-type":"item","numeric-id":5711491,"id":"Q5711491"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q937300$014312AE-3EFD-43D3-A958-90A69FA28D5F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a39baa8ae7ba81a618958b1612caee5a01b3f45e","datavalue":{"value":{"entity-type":"item","numeric-id":5758114,"id":"Q5758114"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q937300$9D0C25D1-28CC-4113-8317-C720A19E41C3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8f12c54a1927788e5cc5895c0dd2a470de2b29e2","datavalue":{"value":{"entity-type":"item","numeric-id":5428881,"id":"Q5428881"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q937300$274AF5AE-E029-49C7-91DB-C6EFAFDF1712","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dcccba79861386df19c84997945862e47e9786d2","datavalue":{"value":{"entity-type":"item","numeric-id":5941060,"id":"Q5941060"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q937300$28079FB1-A487-4EB2-A95D-A652989703DD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e320d5ab20d9378e83c08a862b63bf2725892d4a","datavalue":{"value":{"entity-type":"item","numeric-id":2653567,"id":"Q2653567"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q937300$53948189-3F65-4980-A115-FDB8A3662EC0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"64094cc4201a6201db371ef94b6e6db97b1ecea8","datavalue":{"value":{"entity-type":"item","numeric-id":5926539,"id":"Q5926539"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q937300$5C254646-1281-42CC-A129-F668F90CCD71","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"54e7a108370169c16838733bc613c6abdf38f709","datavalue":{"value":{"entity-type":"item","numeric-id":6044114,"id":"Q6044114"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q937300$6CDAF49F-870C-4FD5-AB0F-57D314624098","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"450718654d1b493daa1574e3d42524d52ede3f50","datavalue":{"value":{"entity-type":"item","numeric-id":1776578,"id":"Q1776578"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q937300$BCDBC42D-A8CA-4B6F-AECA-26917A03CD3A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ed8509b217b4bb778d594e037855d6eca1d9aca1","datavalue":{"value":{"entity-type":"item","numeric-id":2753762,"id":"Q2753762"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q937300$2B8629FE-1705-4F19-AEE9-0DC1DC1EFE7C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"05714b3da002b8b1bc619de4e60891497dad85dd","datavalue":{"value":{"entity-type":"item","numeric-id":2942913,"id":"Q2942913"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q937300$09BA0C00-0260-4BCC-82BB-6C86725A81FF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f6d44e0d283ee4a6747f41419e53b399d833e2ad","datavalue":{"value":{"entity-type":"item","numeric-id":5897782,"id":"Q5897782"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q937300$5F403FD8-A183-4B1A-B3E1-BF6D1BEAD8B5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"06a1669ea55c70484627fcb886923a0a7a7abbca","datavalue":{"value":{"entity-type":"item","numeric-id":5703798,"id":"Q5703798"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q937300$CA08A451-2B8F-404A-8486-C21C55C971F0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1bb02b522788dcae4f7c70e998dfe4d8893f7b5d","datavalue":{"value":{"entity-type":"item","numeric-id":3623920,"id":"Q3623920"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q937300$2EA53D02-2232-465A-829A-34ABC9CC548D","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"df9f8a09bdfd05889aa2f4629cb6972309dd8b68","datavalue":{"value":"10.1016/J.IC.2008.03.003","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q937300$4D5D8C35-5EE5-406C-B879-903BDBE90F9D","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1c4a4c374be6241a25b606e6890de1070c2facd8","datavalue":{"value":{"entity-type":"item","numeric-id":3067539,"id":"Q3067539"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"327c79a538152a028971925416322c500bbf0cf0","datavalue":{"value":{"amount":"+0.8013464212417603","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":"Q937300$04B7EABC-B229-43B8-9B6B-B24506A54AA3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"48dccb07c209d1cd5df915ef66fa8d14a71436db","datavalue":{"value":{"entity-type":"item","numeric-id":5311128,"id":"Q5311128"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8d0fbab221d1f262a6d2387ffd1a10e441655a9b","datavalue":{"value":{"amount":"+0.7752298712730408","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":"Q937300$718537CB-72E6-4087-A052-329EAAAB9C7C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"562c92cb91f0b2ecd3f6b1b6b8e9d74cd40afb2a","datavalue":{"value":{"entity-type":"item","numeric-id":3012541,"id":"Q3012541"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fc0780c256cb48a4e857835977b3a1aff1af084e","datavalue":{"value":{"amount":"+0.7695274353027344","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":"Q937300$E1E87A1A-5846-4EB0-A9DA-A0B097B4E69E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5b6f1b6e5cd0336e7aa2e8607e5cba00c3b036e5","datavalue":{"value":{"entity-type":"item","numeric-id":3176375,"id":"Q3176375"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3410db85e2d741ffcba597f8cf164b720f708e5b","datavalue":{"value":{"amount":"+0.75848388671875","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":"Q937300$017B65C1-E461-438F-A8AB-6BB28709C8EF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"452e8f5f93193c768f7656d35b14dff3083ca69d","datavalue":{"value":{"entity-type":"item","numeric-id":3095249,"id":"Q3095249"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d21de29965884648bc56d45f3bd7150217d36d67","datavalue":{"value":{"amount":"+0.7495293617248535","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":"Q937300$4CD26D83-6CB0-4FB7-9E33-A7C50A14D773","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Compositional verification of sequential programs with procedures","badges":[]}}}}}