{"entities":{"Q7361062":{"pageid":31518725,"ns":120,"title":"Item:Q7361062","lastrevid":105362549,"modified":"2026-10-07T13:34:22Z","type":"item","id":"Q7361062","labels":{"en":{"language":"en","value":"Promela Formalization"}},"descriptions":{"en":{"language":"en","value":"AFP entry Promela"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"a3878a92a7dafff519370a2bd89fc15b0b351c88","datavalue":{"value":"https://isa-afp.org/entries/Promela.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361062$0E7CE295-0DE5-4A09-8B07-86DD0A4FC825","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":"Q7361062$580342F6-F50E-471E-88CC-2FCFF707510A","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"0ecc22d00a75bcea18b023112e4b2e17fe97020a","datavalue":{"value":"Ren\u00e9 Neumann","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361062$53731B54-31FE-427E-951B-0313D2806686","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"e9ef13ead642b08a0946fe137bcebc7d9397c064","datavalue":{"value":{"text":"Promela Formalization","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361062$F1F1E5A6-B098-4DE5-A749-DE98005D49FC","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"f3cd8b9c744774abb72b67ba4dba4647fd6f6039","datavalue":{"value":"We present an executable formalization of the language Promela, the description language for models of the model checker SPIN. This formalization is part of the work for a completely verified model checker (CAVA), but also serves as a useful (and executable!) description of the semantics of the language itself, something that is currently missing. The formalization uses three steps: It takes an abstract syntax tree generated from an SML parser, removes syntactic sugar and enriches it with type information. This further gets translated into a transition system, on which the semantic engine (read: successor function) operates.","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361062$16E6FF6A-68CF-473F-B086-88154C9DCDFD","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":"Q7361062$0C0E4A62-C9AC-40D5-85D1-D4FD44AEA8B3","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":"Q7361062$302319CB-EEE6-4A39-B94E-3B8CE1265BF6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"8ac34df43fbb99027916440c753dc68e36985fe2","datavalue":{"value":{"entity-type":"item","numeric-id":7361475,"id":"Q7361475"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361062$4068F852-81C0-4B3C-A5E9-AFDF46B5035A","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"f085ec8bce9c9a4092e513b2e77970e0472cd8eb","datavalue":{"value":{"entity-type":"item","numeric-id":7360804,"id":"Q7360804"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361062$92E05DBB-9BD3-452B-9846-62BE437C5371","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":"Q7361062$27997210-E52C-4DA3-AEC3-8F6BB2148112","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Promela Formalization","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Promela_Formalization"}}}}}