{"entities":{"Q5423869":{"pageid":7453443,"ns":120,"title":"Item:Q5423869","lastrevid":96261353,"modified":"2026-06-05T10:48:33Z","type":"item","id":"Q5423869","labels":{"en":{"language":"en","value":"Generating Unit Tests from Formal Proofs"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5207438"}},"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":"Q5423869$E4842501-93B1-4365-BFA5-F5383E5F7FC9","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"02e1f7d2156f2b4e07a2aad6c80edd503a38afa5","datavalue":{"value":{"text":"Generating Unit Tests from Formal Proofs","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5423869$E90CE0A5-4C81-444E-AEDA-26B565508404","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"4b76bc5f3586796f48bdcc121c238d157daa38a5","datavalue":{"value":"1196.68046","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5423869$9FE87C88-192F-49C5-9E02-295482D271DA","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"414d2b7cc98b5cceca799840c4ea2b0f33f1d254","datavalue":{"value":"10.1007/978-3-540-73770-4_10","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5423869$A878B3A1-D412-4675-BFB2-D63C78D9AAFA","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"9ba36ed7186931b4cc5b8bde1ac5f5f585332570","datavalue":{"value":{"entity-type":"item","numeric-id":5423868,"id":"Q5423868"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5423869$6B9598E5-4C95-444D-9E2C-EC3B67FC165D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"7743279316f8ce0cdbb2e6d0842ac12b618ecbfa","datavalue":{"value":{"entity-type":"item","numeric-id":679246,"id":"Q679246"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5423869$383A82EE-5DB3-4286-805A-7CBD6BA338BD","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"b59ea210f3608c8a62a77244182313fd466f62a3","datavalue":{"value":{"entity-type":"item","numeric-id":2827439,"id":"Q2827439"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5423869$105179AD-DCBE-4EB1-913F-FCD4F2D48EF0","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"27b591515f5fb68f7eef8b751b948f7aac1b317d","datavalue":{"value":{"time":"+2007-10-31T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5423869$F5905184-F0AB-48D8-87DD-3639C2DB39E5","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5423869$B990FCC4-99EC-432D-9049-4604688B7A92","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"35c3f01235ccba091e1644bb05c86f53d45fd7f7","datavalue":{"value":"68N19","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5423869$75D5E9C9-6746-4C25-AA8B-0F2A985995AC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5423869$D5FC8106-E920-4151-B65E-0634F4CB4DBD","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"f1aa505a635a40abe3272a528f2a2d7683acf2b7","datavalue":{"value":"5207438","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5423869$BDA5BE07-9B77-4202-A423-9F9C7CDC2958","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"78c970019c5d7186e4fa8736dbf7afee746108db","datavalue":{"value":"model-based testing","type":"string"},"datatype":"string"},"type":"statement","id":"Q5423869$90AD907C-EF11-4F27-A6EB-A4475261A11A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c50d987ab7c3ea2a41cb6aca681d912964971ed8","datavalue":{"value":"program verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q5423869$E39EE817-5E59-4D4B-A38D-8DC85927A1BD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"69dd490da9b67dc4fe4c624a05791d0c4fa27f2e","datavalue":{"value":"symbolic execution","type":"string"},"datatype":"string"},"type":"statement","id":"Q5423869$18433A18-B977-4D0E-851B-DE2DA5AD7531","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"0dbcaf7e90d7f94f5449e4510f7ce07f86055e21","datavalue":{"value":"test coverage","type":"string"},"datatype":"string"},"type":"statement","id":"Q5423869$FEEA2680-7444-4E40-9B27-30EBBA19C336","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"22498cf86e242a38d9fe355523225aa55193233b","datavalue":{"value":"theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q5423869$526F9480-9CF1-443F-8B05-9A8B8DF41AB9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7eacb6043920cdee645fa2efe526a8eb17cf25d1","datavalue":{"value":"unit testing","type":"string"},"datatype":"string"},"type":"statement","id":"Q5423869$D4F1DB0E-115F-4CEC-B5F3-624201FB7CBA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c1afc3f62018e7ff5b5398b18851ba2ccbd63506","datavalue":{"value":"white-box testing","type":"string"},"datatype":"string"},"type":"statement","id":"Q5423869$134AC822-D7AD-4C48-ACCF-D8D00E05D3E8","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"5f2fc6b1cac5942479e34eee08b7ed6cdecf60e4","datavalue":{"value":{"entity-type":"item","numeric-id":18658,"id":"Q18658"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5423869$83F87C20-6451-4A54-97C1-27BCE4BC1E4C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"332f296aaae9d4de9f8bb547239196c5fdde9be4","datavalue":{"value":{"entity-type":"item","numeric-id":19311,"id":"Q19311"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5423869$77CAADAE-0A7B-4599-91FD-022C539E8244","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2592836199d8c83558377103476ed4b6729ff0df","datavalue":{"value":{"entity-type":"item","numeric-id":14036,"id":"Q14036"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5423869$32F36761-BC0E-4A76-9852-303D1FE4B412","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"86b4d5730b37b9917aebaffbab7ba473acfa7fcf","datavalue":{"value":{"entity-type":"item","numeric-id":14040,"id":"Q14040"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5423869$2353C0CB-83D1-4A4D-B0CD-2B05C87DCD56","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"e735a85c793db0010dc65dd8f20a7b9930086dd3","datavalue":{"value":{"entity-type":"item","numeric-id":19307,"id":"Q19307"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5423869$270A401D-613B-4533-AD3A-D8A3A35CF0CF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"80eea1ed90a1a156489af434c921fb240a48ae8d","datavalue":{"value":{"entity-type":"item","numeric-id":19308,"id":"Q19308"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5423869$2328C14B-48B1-4864-84E6-8F327B7EEE9D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"cc47147a404ecf949cf86c4e92d2dcc5a8bfafcc","datavalue":{"value":{"entity-type":"item","numeric-id":19680,"id":"Q19680"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5423869$E90C8176-7557-45B9-9DEC-72F9D871FD01","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2822825cdea331aa7c0ec2c340c1eb36d62db00b","datavalue":{"value":{"entity-type":"item","numeric-id":17123,"id":"Q17123"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5423869$C6F94380-BF7B-494A-AC9D-FA24C9101CD8","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":"Q5423869$14F64161-3037-4616-B201-70D1590C379D","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"e1a53778741be9b7d35bdb513dda349fa3453994","datavalue":{"value":"https://doi.org/10.1007/978-3-540-73770-4_10","type":"string"},"datatype":"url"},"type":"statement","id":"Q5423869$95C59D13-991E-4919-B8B4-6CE775B7B108","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"b1ad38ef5e9781f6a8beb72a0e2ffcd551cdf45b","datavalue":{"value":"W1523035663","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5423869$71BAB0C9-D236-4850-A99B-2471CACD44D0","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6e3e8070704160d8960de969ecb012f5b6f69110","datavalue":{"value":{"entity-type":"item","numeric-id":2771756,"id":"Q2771756"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"53243a35fb14e8b12cdf2fbd7aef5bd880fd4e9d","datavalue":{"value":{"amount":"+0.7755436301231384","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":"Q5423869$341D12F4-1B48-4C01-8385-29B7217DD66C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d67e52f7de94239449be0d0611b33f6eb0264b7c","datavalue":{"value":{"entity-type":"item","numeric-id":4472265,"id":"Q4472265"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"354e30144b5d2b8e5467be98ea2e748b02d24ac5","datavalue":{"value":{"amount":"+0.7723371982574463","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":"Q5423869$941E3B09-DE03-4DE5-9BC8-5B595F7C62DE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6fd1edb70603b56470b91d59de6627ac629b1056","datavalue":{"value":{"entity-type":"item","numeric-id":4708482,"id":"Q4708482"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5fcd74c5ced0098cd59a2005854fa6e1435f4aaa","datavalue":{"value":{"amount":"+0.7652485966682434","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":"Q5423869$5445B136-6879-4886-87A4-25E8C9BF57DA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"dc2226623e729e3369244c5351070d6bd8a8d201","datavalue":{"value":{"entity-type":"item","numeric-id":4471927,"id":"Q4471927"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ac3020a073ed5d03d7f361ca1d62987985c92ed0","datavalue":{"value":{"amount":"+0.7643960118293762","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":"Q5423869$DD9D2A1C-5C39-4E54-A0C7-367D7D7EC0CC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"66808192518b3437f79acb74f6089f3faa3c8a78","datavalue":{"value":{"entity-type":"item","numeric-id":3067548,"id":"Q3067548"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f680c3844e1a2b724090f94ff2eedf57492efa28","datavalue":{"value":{"amount":"+0.7600964307785034","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":"Q5423869$B94E3017-EF5E-4056-AFA6-F806B3B1CAF0","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Generating Unit Tests from Formal Proofs","badges":[]}}}}}