{"entities":{"Q883144":{"pageid":884992,"ns":120,"title":"Item:Q883144","lastrevid":50109239,"modified":"2026-01-13T04:04:03Z","type":"item","id":"Q883144","labels":{"en":{"language":"en","value":"HySAT: An efficient proof engine for bounded model checking of hybrid systems"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5159783"}},"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":"Q883144$71EB21F8-3DED-4F66-8D7C-7F0891FC27B0","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"f45fc8fe1b0be04655ed4b1b5b9bfb61add345ff","datavalue":{"value":{"text":"HySAT: An efficient proof engine for bounded model checking of hybrid systems","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q883144$1DC9FF0B-51A5-43EF-9F5E-BA190E43E371","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"b09e2df98d795bec57b1daa3ad070c31b2a7b193","datavalue":{"value":"1116.68048","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q883144$FE31465C-68BA-4F8E-8DC4-E689C78C05B7","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"a014e6ba9fde789e090c1a340d6af73ab4b427b1","datavalue":{"value":{"entity-type":"item","numeric-id":394331,"id":"Q394331"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q883144$713085AA-7481-4320-A928-8330F7B9EB6F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"b966f75c8c0aa46508c2e1a843d2d063ac4942b9","datavalue":{"value":{"entity-type":"item","numeric-id":883143,"id":"Q883143"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q883144$27236D0E-DD7B-4259-A987-2FE80F1CB1AC","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":"Q883144$555F4985-FBD7-42A5-A041-EEFAFF808BB6","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"e35f0982f488bc16c2f1473de732103f14c19500","datavalue":{"value":{"time":"+2007-05-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":"Q883144$0616C442-1AA3-4A28-8F7E-7C3D59B0F43B","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q883144$51109D7D-7A70-4617-B218-53587CF8356C","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"ec28af9750533991875b5633667ee85b22d93744","datavalue":{"value":"5159783","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q883144$8B4577E2-70B9-499C-81D0-D8D9B2E8E1C3","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"68be6715570c298de2f7dfb5b1baeb889a9c5942","datavalue":{"value":"Verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q883144$9C3FF2C4-CB6A-4EFB-AFEE-842D95082F53","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"66af2584c085b19aed7fb585fb6613e1c09c5e57","datavalue":{"value":"Bounded model checking","type":"string"},"datatype":"string"},"type":"statement","id":"Q883144$2F63358E-3CD5-4621-A638-CB84F3082586","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"0c330f2a58efc85bc92438e4c9601644a796093e","datavalue":{"value":"Hybrid systems","type":"string"},"datatype":"string"},"type":"statement","id":"Q883144$DD5A7E0E-F0F6-4ED9-B6BD-84CAC49F3BAB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f59730cf7818c892312636bed117bd3460e24595","datavalue":{"value":"Infinite-state systems","type":"string"},"datatype":"string"},"type":"statement","id":"Q883144$F064140F-176D-4008-ABCD-52F17C3B8F35","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"20a1d8b3158c8e54d3eb6dc847ad8b1b709f4bfa","datavalue":{"value":"Decision procedures","type":"string"},"datatype":"string"},"type":"statement","id":"Q883144$25D5F62B-0FC2-440C-9302-CA3E3A9F25F6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c95393006136a65861f345d17e00540c09d9d258","datavalue":{"value":"Satisfiability","type":"string"},"datatype":"string"},"type":"statement","id":"Q883144$088051FE-49D8-448A-A2F0-503D6DB27C69","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"d8159bf0a919a0b8aef1e30e19d8f9c6cbe3ba79","datavalue":{"value":{"entity-type":"item","numeric-id":16793,"id":"Q16793"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q883144$D6AA58E9-ABB6-4941-BEF7-7FF68AEA5277","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"68889b620f959d2410d5024f9adee923736e93c3","datavalue":{"value":{"entity-type":"item","numeric-id":16818,"id":"Q16818"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q883144$C6C2A83C-351A-4843-9A9F-DE5D4E4FC607","rank":"normal"},{"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":"Q883144$EE44F6D1-A038-4352-8EAC-C19EC7B394D4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"842bcffb0bb918fd12447e4f670f8dc61d68f929","datavalue":{"value":{"entity-type":"item","numeric-id":21432,"id":"Q21432"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q883144$D6B4F9C7-F275-44F0-B71E-159531B864A9","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":"Q883144$1F9CA0E0-19BF-43B5-9EE2-35EF399FF624","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"1cf08d148731824a557280127de6d21b1ec3fe5a","datavalue":{"value":"https://doi.org/10.1007/s10703-006-0031-0","type":"string"},"datatype":"url"},"type":"statement","id":"Q883144$CCF69B34-EA61-4887-8662-D12BBDF85B71","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"7a5a2154e5f6ecc6f4eb4ccf8682b6020b8896e3","datavalue":{"value":"W2086163366","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q883144$7088303D-B496-429D-B750-07FC6068D242","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"f71dd5571a3c1c99537e11b357ad1449f45692c1","datavalue":{"value":{"entity-type":"item","numeric-id":4809056,"id":"Q4809056"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q883144$2512E425-A418-4552-A50E-9D858CC1CAA6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ca50b56de23777ce618ce7b9747f11712b65365d","datavalue":{"value":{"entity-type":"item","numeric-id":2849590,"id":"Q2849590"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q883144$E210D3FF-BFA4-4081-8F59-23C17D76256E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"663180489de8ea8d2fefa7ce5656e8c0b05d64df","datavalue":{"value":{"entity-type":"item","numeric-id":4736486,"id":"Q4736486"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q883144$11A71FA7-B115-4E98-A5FF-8363BCDDE529","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6dc64d6d31493ac74da4f6c177f509ec4a9d4b14","datavalue":{"value":{"entity-type":"item","numeric-id":4804899,"id":"Q4804899"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q883144$8F7F9EFB-3436-4513-BDEE-5D7154DD8305","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2d0b8ae8e7348fd062c74f462635039e5ce6b1db","datavalue":{"value":{"entity-type":"item","numeric-id":4249562,"id":"Q4249562"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q883144$9C10642D-B8FD-4190-8754-D419C56A64C0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b5e59694ba693ed2b8af4b0c9c848f2b45a00bcf","datavalue":{"value":{"entity-type":"item","numeric-id":4817533,"id":"Q4817533"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q883144$0B751635-4DF0-4EFA-8012-748E79FDE89A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"00ca4646d6f13a5b667ec2c36ad9a66b1ec21467","datavalue":{"value":{"entity-type":"item","numeric-id":4354937,"id":"Q4354937"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q883144$F023C967-DAE2-4A39-89F9-1E47491171A6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"351e6790b87d174878f83df2eb0842ae7e7104f3","datavalue":{"value":{"entity-type":"item","numeric-id":4025905,"id":"Q4025905"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q883144$4B28BEC9-3B8C-41EB-826C-052E2AF15BBA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"62cff4d07ffcb71b5bb9f399ad2347b51931f095","datavalue":{"value":{"entity-type":"item","numeric-id":5621961,"id":"Q5621961"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q883144$E31FF298-2BE3-471C-B3C0-D1135C99E94E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a41051290dad36879ad016b201152054fc1f7f49","datavalue":{"value":{"entity-type":"item","numeric-id":5307060,"id":"Q5307060"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q883144$48FFB6A0-6025-4C25-AD60-5C85DF3E7025","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6da6ded218db8e1aba2fc38982f0c41333c8292d","datavalue":{"value":{"entity-type":"item","numeric-id":4809077,"id":"Q4809077"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q883144$F179ECBE-B0EA-43B8-8AD8-E5B3F75E58D6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d4f7017b74dd587e92e93a287b13bccd94320a1e","datavalue":{"value":{"entity-type":"item","numeric-id":3408146,"id":"Q3408146"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q883144$318325F2-5641-4DAF-963F-219811738073","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4e221fbc27351e58da31a742ce227d7a9ea37f27","datavalue":{"value":{"entity-type":"item","numeric-id":4021366,"id":"Q4021366"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q883144$99989EBA-C826-4765-AEEE-7361765842F4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c82ad10c73e928271f482901deda0f097caa8289","datavalue":{"value":{"entity-type":"item","numeric-id":3723675,"id":"Q3723675"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q883144$1AD95FCA-38FC-481E-BBB0-D7E452B8BB12","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1c61b8df768da1a4e1cc2a85425f3f7b271a5888","datavalue":{"value":{"entity-type":"item","numeric-id":4234084,"id":"Q4234084"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q883144$96037756-7EDD-4307-A29F-A2F9B49B29FB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"679f4c7c902687185c9f78d8805406444ad0da62","datavalue":{"value":{"entity-type":"item","numeric-id":2849595,"id":"Q2849595"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q883144$C8371BD1-7F84-4E24-B46E-1521D17F4525","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4c2c1fbb42c40132bcde18b08b5d5cb2763f5bb7","datavalue":{"value":{"entity-type":"item","numeric-id":5760872,"id":"Q5760872"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q883144$FD5A580C-CC3A-4CD7-A07E-ACB2355C3A6E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"28deebb9f03725888e2cb415bbaa29688963935e","datavalue":{"value":{"entity-type":"item","numeric-id":2751358,"id":"Q2751358"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q883144$6A1144C4-BB58-4716-9ABC-DEF5328CBBAE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0a54affc94a366d98bad53a93a8139d98e5ad3f2","datavalue":{"value":{"entity-type":"item","numeric-id":3023951,"id":"Q3023951"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q883144$CC10C832-7A41-411D-A1EB-6454954CA176","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a0b3ec2ebad61e0cf6b1df8ac8c200c146db0252","datavalue":{"value":{"entity-type":"item","numeric-id":2754108,"id":"Q2754108"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q883144$993929B7-CE29-4DEC-9797-7584BB54634C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f217d7c1a8591d173f7a390567150498d1528ee2","datavalue":{"value":{"entity-type":"item","numeric-id":293409,"id":"Q293409"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q883144$54580B5F-792B-4EDB-8185-8D61E3BD613C","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"d48519e6fe177eb5bf190a7d52888e590ed7d02e","datavalue":{"value":"10.1007/S10703-006-0031-0","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q883144$D676BCF5-9A0E-480F-ADB1-822AE0D0695B","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e60d6908af4133947bcc00cf07ca518f9f650bfb","datavalue":{"value":{"entity-type":"item","numeric-id":5711504,"id":"Q5711504"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c03d53655308a4f53f3c64329dbac522e4e36f32","datavalue":{"value":{"amount":"+0.822955846786499","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":"Q883144$CEFD24FF-01E2-4F24-A9F6-B502CC6205A1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fc090f046e06c5ba7334a65d09ac894baadafbac","datavalue":{"value":{"entity-type":"item","numeric-id":2849590,"id":"Q2849590"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"bf3962323cde18d9b3e6f6c89173f9b24accb00a","datavalue":{"value":{"amount":"+0.8182752728462219","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":"Q883144$07226151-76C6-4D03-82BB-F4F3EF0B2609","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"791cf737ef7f9fd032e937bf530521a62c362abb","datavalue":{"value":{"entity-type":"item","numeric-id":3612989,"id":"Q3612989"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8eb1c3cd743535900ae75988a3dc4e6e984e1f55","datavalue":{"value":{"amount":"+0.8037108778953552","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":"Q883144$69179073-FC8F-428E-9D4C-E810CC0249D9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8c5baa1ff0d2a89f74784a86394a5feb60447cb3","datavalue":{"value":{"entity-type":"item","numeric-id":1856193,"id":"Q1856193"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3c2c9ad6bbf1bc0f1e11f2ded7c5317bbb81587b","datavalue":{"value":{"amount":"+0.767179548740387","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":"Q883144$D59EEB6A-30ED-46D6-AB8F-9934F0B7A6FC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b2359b60e58d31576d78a4b60f6627662a731341","datavalue":{"value":{"entity-type":"item","numeric-id":5897062,"id":"Q5897062"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"32d00a4d16cbb394641d97beaf476880cca2b870","datavalue":{"value":{"amount":"+0.763501763343811","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":"Q883144$26E496F1-FC6D-495C-BB99-B3D31B2B365E","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:883144","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:883144"}}}}}