{"entities":{"Q6869964":{"pageid":20716375,"ns":120,"title":"Item:Q6869964","lastrevid":84234086,"modified":"2026-05-14T00:22:03Z","type":"item","id":"Q6869964","labels":{"en":{"language":"en","value":"Cazamariposas: automated instability debugging in SMT-based program verification"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 8149346"}},"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":"Q6869964$C0F2F140-D1B9-4BC4-A6B0-7F4DB7DB91DF","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"680dfa8457098eb472c703cbe4c4b8f30664d4fe","datavalue":{"value":{"text":"Cazamariposas: automated instability debugging in SMT-based program verification","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q6869964$74DC65BE-788E-4867-B82A-67DAB396F770","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"d180ae1399921cfde31f8ff448bda88c6d19bca7","datavalue":{"value":"10.1007/978-3-031-99984-0_5","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6869964$A6A102D8-4EF7-4237-B064-58F9E89B73AA","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"fca788e56cc52d98294eb71664c0dcd2e4dc9b51","datavalue":{"value":{"entity-type":"item","numeric-id":6189440,"id":"Q6189440"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6869964$C8B72478-76F3-4619-AD4B-5756FA982608","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"eb2cd30819e7c32710e315b231e696cb86b7fd0e","datavalue":{"value":{"entity-type":"item","numeric-id":6869962,"id":"Q6869962"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6869964$CE93829B-43A1-4270-BF55-E8C9322D19CC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"4545114e473836bad71ebea0181e527108d9e5ea","datavalue":{"value":{"entity-type":"item","numeric-id":352966,"id":"Q352966"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6869964$A88AA680-AA02-422E-9F04-4B7714DA374A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"08a4e440469bffc816f5d1639cdc7838dd8c9fbf","datavalue":{"value":{"entity-type":"item","numeric-id":6869963,"id":"Q6869963"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6869964$CC0AB478-C570-4790-BE7C-2C1DBADF19AC","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"056911bef05d64d4fd0798177ee591ee667e0cfb","datavalue":{"value":"Yi Zhou","type":"string"},"datatype":"string"},"type":"statement","id":"Q6869964$8B242387-0251-4DC4-974B-935242941AC0","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"bd0535754d1571e407a6ce2636467dab5aaebc85","datavalue":{"value":{"time":"+2026-01-21T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q6869964$E42BD512-5516-43A8-BFFB-257728920160","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6869964$0F4E7B7B-E71D-46C2-BBD2-9B609E63C301","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6869964$166D7594-847A-44BC-990D-0F5EE27968E3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"58b3a5d0bc4bfd215423308dfe52b6887acdeedd","datavalue":{"value":"68V20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6869964$B2603D10-2213-4A59-826C-A2CFCA0F2CC8","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"bfdfa0303ec7a046ad2953ca3a1cf88a85c557fc","datavalue":{"value":"8149346","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6869964$BC3FA8B7-385C-4A30-8A91-55C972137697","rank":"normal"}],"P163":[{"mainsnak":{"snaktype":"value","property":"P163","hash":"45fcd4163b5f33e6e8c784f5522d7246c0a1a61e","datavalue":{"value":{"entity-type":"item","numeric-id":57056,"id":"Q57056"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6869964$B57A9465-4E23-4C5F-9B92-25A5E12D309A","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"dc37cf6bf1a4fd159f089028e999146e64828fa8","datavalue":{"value":"SMT","type":"string"},"datatype":"string"},"type":"statement","id":"Q6869964$3ACD1D09-3499-4FF6-8F81-1979D8E351C1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c50d987ab7c3ea2a41cb6aca681d912964971ed8","datavalue":{"value":"program verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q6869964$54D6ECCD-8A4B-4B9F-82A3-971B88D2D92E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4327f30ebdd3403bc9fc916de70878a4d84945d9","datavalue":{"value":"proof instability","type":"string"},"datatype":"string"},"type":"statement","id":"Q6869964$FCA92573-4441-4698-8D9D-72E140A5D7B1","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":"Q6869964$0A59F9CB-4105-4CAF-B327-A162374600D9","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"b440b92b71497e1eb9d3de5c9138a6884c51ecf1","datavalue":{"value":{"entity-type":"item","numeric-id":4982446,"id":"Q4982446"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6869964$E363014A-1921-4BF7-9982-300052DB346B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6c50bf30b5dabdf4dda50dde9e43de872f1c8761","datavalue":{"value":{"entity-type":"item","numeric-id":5200032,"id":"Q5200032"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6869964$8F204610-5805-4C44-BAC5-AA3889A2115F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1b4f714dbb33bba32b50777c1d77c1cb7ff5fe56","datavalue":{"value":{"entity-type":"item","numeric-id":3608773,"id":"Q3608773"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6869964$01FF6A2C-F90B-4CA8-A8AE-A77BDAB7D000","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9297b6a91a7c29eb2b70ce4159ebd40915c17240","datavalue":{"value":{"entity-type":"item","numeric-id":2305435,"id":"Q2305435"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6869964$19C66E4E-925D-4885-A0F7-68FDECC3EA6E","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Cazamariposas: automated instability debugging in SMT-based program verification","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Cazamariposas:_automated_instability_debugging_in_SMT-based_program_verification"}}}}}