{"entities":{"Q1888196":{"pageid":1898938,"ns":120,"title":"Item:Q1888196","lastrevid":71067519,"modified":"2026-04-13T19:16:11Z","type":"item","id":"Q1888196","labels":{"en":{"language":"en","value":"Predicate abstraction of ANSI-C programs using SAT"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 2117713"}},"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":"Q1888196$773F131A-43A5-40C3-BFD6-3C483FE68784","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"415fa131379140538818ccdccf6f13b4392dcc41","datavalue":{"value":{"text":"Predicate abstraction of ANSI-C programs using SAT","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1888196$F7A675A3-5DFF-4155-9F5B-7BB70A0471BB","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"484c768a59995bc4221984c919ed99e4a8f32399","datavalue":{"value":"1090.68022","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1888196$F4BF1B70-B877-4924-AEF0-292C3A4439AD","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"de4a775b741b129661b3807102896dab39bea660","datavalue":{"value":{"entity-type":"item","numeric-id":438554,"id":"Q438554"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1888196$A4CF3106-5226-42D7-B422-DC2C1CB2B078","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"66a480d2e9b29ea82a9b0fc72873fd6d8201d31c","datavalue":{"value":{"entity-type":"item","numeric-id":287271,"id":"Q287271"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1888196$DA05181A-5147-467D-AA1A-001F2BC0F05A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"b93a7ab83eb4b01c8fa415c14a8ae5c22018daae","datavalue":{"value":{"entity-type":"item","numeric-id":1039849,"id":"Q1039849"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1888196$A233271B-3728-40B7-8C4B-8E172D414690","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"4e4e5ed72bee66087d415d4f69d49eefd101a453","datavalue":{"value":{"entity-type":"item","numeric-id":526749,"id":"Q526749"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1888196$EE339A26-588E-4587-A938-4130614C87EA","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"70551fcc6e89042fc26ae9242a005533b44a2d7a","datavalue":{"value":{"entity-type":"item","numeric-id":169908,"id":"Q169908"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1888196$8B47A0FA-FFCB-46B0-8FEF-EE16261D87ED","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"df3f0f81c599b7f3be622e55e11802c61c03707a","datavalue":{"value":{"time":"+2004-11-22T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1888196$ACF9E5ED-DAE4-40A5-A577-FBF1E7F78187","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1888196$DA9291DC-D8CD-45F3-AE99-F61964787DBE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1888196$345368EA-1D15-4500-AF04-FB73E79A38A3","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"3c90b19f6407d8d56caa2a7ea2936792e9466845","datavalue":{"value":"2117713","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1888196$929EB54E-790C-4847-9638-C5F6131FBC81","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6377a628e12b96a6a919606a8ef231bc11537970","datavalue":{"value":"Predicate abstraction","type":"string"},"datatype":"string"},"type":"statement","id":"Q1888196$9E64FB10-43D7-4BF5-9A19-F4964CCD1675","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"0273d6e723577adcd03d9fc0abfab3e68962b14a","datavalue":{"value":"ANSI-C","type":"string"},"datatype":"string"},"type":"statement","id":"Q1888196$28D7A1F9-1831-4F44-A188-B90BE9EDD4CA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5867ec7b44aefc01672736513dfe6410a0300cd5","datavalue":{"value":"SAT","type":"string"},"datatype":"string"},"type":"statement","id":"Q1888196$2C1DC4E4-828A-44F1-A036-2696ECC05A79","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"478f9061f14e098e3fdf3fe3667d3a7084c42e61","datavalue":{"value":{"entity-type":"item","numeric-id":18982,"id":"Q18982"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1888196$DFF12DFB-57D5-4D11-8F2C-191AB13888FB","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":"Q1888196$CF32AC82-B756-4FEA-B619-9550B2ED4B2D","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":"Q1888196$1A07B21A-301A-4A78-A709-F98F47322D47","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"219822e000a5916505bf35a8cabe5db39887c84f","datavalue":{"value":"10.1023/B:FORM.0000040025.89719.F3","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1888196$2AFAA3DA-4832-4A05-AA50-0705E16F5AC2","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ca6fc1c7040746ccf23490e6a79939676fc43565","datavalue":{"value":{"entity-type":"item","numeric-id":5703792,"id":"Q5703792"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e19aa92e0c6eca9762805d91e4096620867531d9","datavalue":{"value":{"amount":"+0.8718177676200867","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":"Q1888196$6062BA80-9F86-4308-85C1-9EFA75F36556","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"79ffa5ff30461cd51e0211fecdb41174f0327193","datavalue":{"value":{"entity-type":"item","numeric-id":5897055,"id":"Q5897055"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"dd3794ca9c58e52faffbceba937a6e10301f1c3c","datavalue":{"value":{"amount":"+0.8456651568412781","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":"Q1888196$FF396A79-660A-4767-BD46-62DCA93FF152","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5bb0e9b3dbee4bdb0590f729f77b329e548a2945","datavalue":{"value":{"entity-type":"item","numeric-id":5703774,"id":"Q5703774"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ff47168b1df7fd5c3a312a876e887dafe926131c","datavalue":{"value":{"amount":"+0.833751380443573","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":"Q1888196$343C0191-BF41-4249-B8FA-A79785DEB1C7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6ba55ee38a99d46604b9b2feddb9efbde5b9b1bb","datavalue":{"value":{"entity-type":"item","numeric-id":5240105,"id":"Q5240105"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9eb8a9b345a2ae8251cb01e852fa65cdc71b6c0d","datavalue":{"value":{"amount":"+0.8228955268859863","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":"Q1888196$67F31CA7-C21C-4670-B2A5-845E1C9E18B1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"dfe92b7258e0af482e7fb1d334c65fe05402d844","datavalue":{"value":{"entity-type":"item","numeric-id":968302,"id":"Q968302"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a11ba433d76bca8bd2d4e2502ef5d6072e6af346","datavalue":{"value":{"amount":"+0.8114013075828552","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":"Q1888196$C0897658-9594-4746-98A2-A7706C976AF1","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Predicate abstraction of ANSI-C programs using SAT","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Predicate_abstraction_of_ANSI-C_programs_using_SAT"}}}}}