{"entities":{"Q1077917":{"pageid":1088669,"ns":120,"title":"Item:Q1077917","lastrevid":69587439,"modified":"2026-04-13T08:01:36Z","type":"item","id":"Q1077917","labels":{"en":{"language":"en","value":"Redundant proofs of non-interference in Levin-Gries CSP program proofs"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 3958705"}},"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":"Q1077917$050857C1-3AFF-40D3-9B65-2E625A5658DB","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"6e37cff259ff51af7a2201e868927ef67dc2db7e","datavalue":{"value":{"text":"Redundant proofs of non-interference in Levin-Gries CSP program proofs","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1077917$F8B1EE48-16B5-4B19-AE3B-99B96D4F9EF7","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"17bdf6fbcf706fbf8f1dad973b8159a6a6ef01e2","datavalue":{"value":"0595.68017","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1077917$2B6D1864-45C5-4DCF-AD2D-4C0AF4D500A9","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"1c2d3fd31c3823c21d3a254523df5de25c7a482b","datavalue":{"value":"10.1007/BF00264361","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1077917$9C174363-A912-4D29-A403-D063FEA6CB99","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"ce4d2970c3170bf939b371f8a7365b388a8bd3ff","datavalue":{"value":{"entity-type":"item","numeric-id":1077916,"id":"Q1077916"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1077917$AB958D03-1740-4B7C-BA0E-9E0DA30CE913","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"7d0f02e85530cd06ceb2c58a40dc9c2e0258e194","datavalue":{"value":{"entity-type":"item","numeric-id":161641,"id":"Q161641"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1077917$09E03C69-A9EB-40DF-99BE-BB986E8FA55E","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"5ae48c61eed19d1e1e1f33f9255d5b329362d064","datavalue":{"value":{"time":"+1987-00-00T00:00:00Z","timezone":0,"before":0,"after":0,"precision":9,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1077917$8BB1B676-EC45-47FF-8A4D-30A336B126F9","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"450b3c609ab9c7254bb912adcc5e39a2345ed622","datavalue":{"value":"The proof system for Hoare's CSP language proposed by Levin and Gries requires that non-interference be proven for each assertion used in the proof of a process. In the worst case, the effort required to provide such proofs could be enormous. The need for these proofs has been identified as a significant weakness of the system. In this paper, we show that most of the proofs of non-interference required are unnecessary. In particular, we show that once proofs of non-interference have been found for those assertions that precede certain synchronization points in a program the remaining proofs of non-interference required in the Levin-Gries system can be constructed automatically. This suggests that proving non-interference in the Levin-Gries system may be far less burdensome than had previously been assumed.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1077917$3AC600B5-7A29-43CC-99B6-B9C89FB0F6B5","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1077917$0CAD8E5D-116E-40C7-8857-B586814F7E65","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"f8460f413c2e8104dd2e0e9d835690973b6a2e6f","datavalue":{"value":"3958705","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1077917$0E5AE9F8-7029-4E70-80BA-EDA0F155CEF3","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1f2806d881d60d09f86c4a9af61ec1df28165067","datavalue":{"value":"proof system for Hoare's CSP language","type":"string"},"datatype":"string"},"type":"statement","id":"Q1077917$B61E2422-3B99-4BF3-B768-C681F07CE21B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"047c6c37b1b59065ab8a30c63416b0516d5d913a","datavalue":{"value":"non-interference","type":"string"},"datatype":"string"},"type":"statement","id":"Q1077917$FC28FC44-2D23-4CA2-8863-2B14C13DC53B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d9cc79f4e2222aa09ced1c7c790ecbb376b1ab5b","datavalue":{"value":"synchronization points","type":"string"},"datatype":"string"},"type":"statement","id":"Q1077917$126E02BF-D6D8-434B-A26D-B436329828FE","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":"Q1077917$DA2C38B6-0BB1-4D83-8418-42D9E5596DC2","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"c68d25f18b69eecd7a17d6824820023e6fdc03d9","datavalue":{"value":"https://doi.org/10.1007/bf00264361","type":"string"},"datatype":"url"},"type":"statement","id":"Q1077917$CF0EB4BB-B07B-4A7F-88F9-6BADE7D6ECA4","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"9806883a0abcdf87cc30b757996bd728ce9eba2c","datavalue":{"value":"W2060914329","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1077917$5FB64F38-6956-45C2-A6A7-936BC1141310","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a49713591421d542ac856c60647732701ed74a86","datavalue":{"value":{"entity-type":"item","numeric-id":4916055,"id":"Q4916055"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"37b881dc9f8bceb18783fd53eaf3de951628a3e8","datavalue":{"value":{"amount":"+0.7518969178199768","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":"Q1077917$772DACFE-E806-48A5-B2A1-9E483316FF3A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6c627fee83162a10b7f15ae07d2cce803aaaeed7","datavalue":{"value":{"entity-type":"item","numeric-id":3553917,"id":"Q3553917"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"30aca8eed1a697249c0ae764e309f59d8b682ed2","datavalue":{"value":{"amount":"+0.7431042194366455","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":"Q1077917$D01A06ED-30E3-4AFE-9A6E-C743A20E533E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1ceef99efb4f24cb192d0ef779a1f04780babd41","datavalue":{"value":{"entity-type":"item","numeric-id":5311263,"id":"Q5311263"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ff87ac2b7f7084ec7b8bee74ab79fa29aee50688","datavalue":{"value":{"amount":"+0.7369254231452942","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":"Q1077917$718E2C2A-EAAE-460D-9B36-F0DB68CD6679","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5460c3c4115d038ac07973252e2a76e86093dad7","datavalue":{"value":{"entity-type":"item","numeric-id":3681909,"id":"Q3681909"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4541ffa641c7f61f438a0a27fdcda006162cfbcb","datavalue":{"value":{"amount":"+0.7345881462097168","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":"Q1077917$D270F4D3-1739-4746-85B9-07FC39967A6A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"508b3f50a1bc845a7286cb66a16d7d0f187e3555","datavalue":{"value":{"entity-type":"item","numeric-id":5348913,"id":"Q5348913"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7afe428cb928546f043b4f596d6a42b56689f248","datavalue":{"value":{"amount":"+0.7211519479751587","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":"Q1077917$CC1BFD55-785B-426B-A665-B98B23E1AB3C","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Redundant proofs of non-interference in Levin-Gries CSP program proofs","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Redundant_proofs_of_non-interference_in_Levin-Gries_CSP_program_proofs"}}}}}