{"entities":{"Q2845512":{"pageid":2856232,"ns":120,"title":"Item:Q2845512","lastrevid":83855417,"modified":"2026-05-07T13:00:54Z","type":"item","id":"Q2845512","labels":{"en":{"language":"en","value":"A satisfiability-based approach to abstraction refinement in model checking"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6203491"}},"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":"Q2845512$DF2D15B0-BFB9-4512-BBB0-6E348AD32C8C","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"b6de6d8ba23a4b3a0df8b4cd4ae43a40aeb7dc14","datavalue":{"value":"1271.68143","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2845512$4BA50615-2B0C-40A2-B6CA-329F47D94F8C","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"3d1bd835aad3f28b70e4d220903c239104ceef70","datavalue":{"value":{"entity-type":"item","numeric-id":432141,"id":"Q432141"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2845512$5BBB78BD-9EAC-4BCE-BB8A-9581AB29E780","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"58f58cd250110bf59c28a29d5e30b88533180a96","datavalue":{"value":{"entity-type":"item","numeric-id":832299,"id":"Q832299"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2845512$43F2FF1B-C419-4D64-A37D-79B1CBEBCB01","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"349454d3a8c56c84dd359b5751b956560f489b3d","datavalue":{"value":{"entity-type":"item","numeric-id":6285498,"id":"Q6285498"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2845512$E3E79211-8F08-4D3D-ABFE-EEAF8BAD40EE","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"dbe91a82e9327cf79ad7ddd82bc8f3cac46bf53c","datavalue":{"value":{"time":"+2013-08-30T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2845512$B4FFE7DB-8A3C-4474-A03F-9A0A9FF5F8B4","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"f3ed8a7c54dd5234e0f23f6dcd6b76a62fe2bfca","datavalue":{"value":"http://www.sciencedirect.com/science/article/pii/S1571066105825460","type":"string"},"datatype":"url"},"type":"statement","id":"Q2845512$AADC349E-6486-4A79-8A7C-258688463536","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2845512$EBBF21DB-593B-4893-B9E6-F6BABE1A570F","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"78bf0c704a6cdbcd83d0158e19e3b2ef34ff8683","datavalue":{"value":"6203491","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2845512$C40ADF7F-E2D6-4DB7-9368-1937350EFDC4","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":"Q2845512$70A27FA1-F6F6-46BB-8CED-6AE582425DC2","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"cf1cd4393cebc142398a488ae2d836a5e3694d92","datavalue":{"value":{"text":"A satisfiability-based approach to abstraction refinement in model checking","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2845512$4CC04A1A-DC7D-4AF8-B35E-72A04EA14540","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"aaa75d14f411a29ded225a875d13f512a1857ea9","datavalue":{"value":{"entity-type":"item","numeric-id":4427894,"id":"Q4427894"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"06c01fe7685066d647ac2c6bd03fe5275f9d9d23","datavalue":{"value":{"amount":"+0.8649091124534607","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":"Q2845512$5B24383C-4584-4C2B-B3BA-E932D18BD8B1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"edc30b245ec6b807d4e24f0d259d8f49ecc3c7a9","datavalue":{"value":{"entity-type":"item","numeric-id":5758121,"id":"Q5758121"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b0f84994188691588a218510f9da2385ff355b5b","datavalue":{"value":{"amount":"+0.8515638113021851","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":"Q2845512$5CD9CD4D-09E3-4AD6-A335-6967A82E1DB8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9d3eab57d91a654c4eadcc66da4fb3257585003c","datavalue":{"value":{"entity-type":"item","numeric-id":4738460,"id":"Q4738460"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3942d01884bfd8f480872dbe7af66ff6af634b45","datavalue":{"value":{"amount":"+0.8431967496871948","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":"Q2845512$E7F6E169-7592-4036-AC80-40296A838631","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bd40460bef7592e9f11c579ff25795b0835cbe7c","datavalue":{"value":{"entity-type":"item","numeric-id":4417909,"id":"Q4417909"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d0a88b9f1242c2c33e93be2a04d314970770758f","datavalue":{"value":{"amount":"+0.8426084518432617","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":"Q2845512$5B220B81-DCDE-4970-A174-FC7A983D16BC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f3e4418b90254da47f1e3ab57975e595d219a0be","datavalue":{"value":{"entity-type":"item","numeric-id":5899061,"id":"Q5899061"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"210bcfbbc964116a943f168befccb682c235468e","datavalue":{"value":{"amount":"+0.8415626883506775","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":"Q2845512$92DF8123-94C0-4FD7-A0A8-9637F522A558","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A satisfiability-based approach to abstraction refinement in model checking","badges":[]}}}}}