{"entities":{"Q2233532":{"pageid":2244275,"ns":120,"title":"Item:Q2233532","lastrevid":73842654,"modified":"2026-04-14T17:27:36Z","type":"item","id":"Q2233532","labels":{"en":{"language":"en","value":"Counterexample- and simulation-guided floating-point loop invariant synthesis"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7410589"}},"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":"Q2233532$D7CC93E4-6735-4777-AA6A-8CA974995690","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"6abec68c621713aaabc3cd6e13e3f5b0d06141f6","datavalue":{"value":{"text":"Counterexample- and simulation-guided floating-point loop invariant synthesis","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2233532$326270F7-BC88-4F0C-8185-8AC8807A6E88","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"344457a84bcf3accd0a7fba8e4ac76c2bf633ef0","datavalue":{"value":"1474.68055","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2233532$0AE926E3-2F23-49F6-B8D6-4A6B38B2DA64","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"1fadb9a24ba55ae449da53ede0a7f5f2bca40498","datavalue":{"value":"10.1007/978-3-030-65474-0_8","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2233532$60A39D5E-F15B-4853-8BD5-42753879E0AF","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"6b09a69fa7ba8f251dfbed5c978762c5792862d2","datavalue":{"value":{"entity-type":"item","numeric-id":2233531,"id":"Q2233531"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2233532$CCF2188E-F1AE-4A3C-BEB5-CC577D6683A2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"bc64b0431d237d2cb162de6a38437bcb6b852e6d","datavalue":{"value":{"entity-type":"item","numeric-id":2024355,"id":"Q2024355"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2233532$2175D543-BE08-4D57-885A-2FC1FEE0C7B9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"0d8846866e0f2e2874e781dfcefe3a000615efed","datavalue":{"value":{"entity-type":"item","numeric-id":435967,"id":"Q435967"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2233532$03AC6E00-3F61-4FAE-A3E9-9CC74FAD034E","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"899d672926fe97cd87f3708d91dc74172e4f3b51","datavalue":{"value":{"time":"+2021-10-18T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2233532$00841889-A95B-4C07-93BD-76A9D6D58CBB","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2233532$75466423-10A3-4526-8BA0-7EEC2926FFEB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"224133dd68a4f3b66ddf7d50fd627018c06684e4","datavalue":{"value":"65G50","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2233532$1BB7EBEC-CB34-4989-8443-3E61A4A5E387","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"7c139021c17cd719fd5a8e3c44bb55ff55f9d5db","datavalue":{"value":"7410589","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2233532$85DD1D92-5F96-4B44-AABD-ED294F26CB36","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"535f65541f41a57140701ba196c6989224dff34b","datavalue":{"value":"invariant synthesis","type":"string"},"datatype":"string"},"type":"statement","id":"Q2233532$4AAF3428-3700-46D5-973A-5DDE5B5E0348","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"00216556e27ad3bbc2d642874d0693b52d5f53d1","datavalue":{"value":"floating-point arithmetic","type":"string"},"datatype":"string"},"type":"statement","id":"Q2233532$0A9AA664-6A57-44CA-A896-EC1B79FA2C32","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a613ce2db29d671b98d38923817faac993619cb6","datavalue":{"value":"CEGIS","type":"string"},"datatype":"string"},"type":"statement","id":"Q2233532$842E858F-3746-49F5-A9AA-0A759C7CB9B2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f828563fee5a57e5f16da87a79378ac587cea3ac","datavalue":{"value":"simulation","type":"string"},"datatype":"string"},"type":"statement","id":"Q2233532$936DBFCA-6377-446A-A9F2-BEDA487F3E88","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":"Q2233532$0B7FCC0A-3F0E-4B01-8854-CF1F1AB6BA2F","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"a1767fde19b3243f2a12824f999ffb6f7b2330b0","datavalue":{"value":"https://doi.org/10.1007/978-3-030-65474-0_8","type":"string"},"datatype":"url"},"type":"statement","id":"Q2233532$FEAEB52A-36F0-40F5-B0C0-B4B5F7B69C2D","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"2e3ab0bcb238c27ad6a719da31d8d3f99ae1f429","datavalue":{"value":"W3118905376","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2233532$A81FB41A-4B53-4509-9C29-E8ED96CD7F26","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"67945448a4fab3cfd00464aeec20d1302b90e6cd","datavalue":{"value":{"entity-type":"item","numeric-id":3558213,"id":"Q3558213"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2233532$09114A0B-FE5C-4959-B385-915A7EF2BF29","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"455bef0a895b2ab0cd666a83d671b01a85c607a6","datavalue":{"value":{"entity-type":"item","numeric-id":3503410,"id":"Q3503410"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2233532$7906FEE2-3703-4D12-A73A-4ADFAFA76CC1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ad90f6cec38c35afe0de2280ea56854eb9819aaf","datavalue":{"value":{"entity-type":"item","numeric-id":5897426,"id":"Q5897426"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2233532$3C7CE160-4016-446F-8452-89131FB12308","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ef9a85754f10c794d7ea794155cce4bd2f066956","datavalue":{"value":{"entity-type":"item","numeric-id":3075471,"id":"Q3075471"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2233532$1BDB64BC-FF36-42BD-ACBE-39ABB9EDAF18","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ea995edccac5da0953e656bb0c95a322b8422b8c","datavalue":{"value":{"entity-type":"item","numeric-id":3593074,"id":"Q3593074"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2233532$EE6FED06-E6AA-4D15-8123-FC1757611639","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f0a1cfc1d9554fd0578fb57504fa04de62a62197","datavalue":{"value":{"entity-type":"item","numeric-id":4174789,"id":"Q4174789"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2233532$211CDAD0-8C63-43B3-81AB-83541A19635D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"358a4e09d6cbdccb0a6a97551bee24c6efb9d080","datavalue":{"value":{"entity-type":"item","numeric-id":5326338,"id":"Q5326338"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2233532$635AC446-0587-4A49-AC20-36424EEA300B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7c4cf2cc00850270a28614888dcd0fd49d3c89ac","datavalue":{"value":{"entity-type":"item","numeric-id":2225478,"id":"Q2225478"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2233532$840D0891-60DE-4039-B7C4-78DD416E657C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"586fae6e49225b59a9454fd3e5d7bea4f9f2b19c","datavalue":{"value":{"entity-type":"item","numeric-id":5308687,"id":"Q5308687"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2233532$9C6243F3-C72A-4728-9A5D-FA259CCF0EA8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1e0e2934c30f090bd35ac45b457b5570f000b5f1","datavalue":{"value":{"entity-type":"item","numeric-id":2248100,"id":"Q2248100"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2233532$8FA7A0A7-1EE2-44CB-BDF4-05386B423B09","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d77121ca06023666fb3b31fe1611bc7b34ff56df","datavalue":{"value":{"entity-type":"item","numeric-id":2908506,"id":"Q2908506"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2233532$85347DD2-96D4-4FE3-96BA-BCA88AEA3539","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d88a4d21f9c10003cdb38349b5ebb6aa4815e0e5","datavalue":{"value":{"entity-type":"item","numeric-id":5458331,"id":"Q5458331"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2233532$0D89695B-DD8B-4169-9BDA-66D3A97C146A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e61caeb9ccf34c77ec2a456b135b01b408ce9535","datavalue":{"value":{"entity-type":"item","numeric-id":853733,"id":"Q853733"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2233532$70C2B6C9-CC31-4C2C-9B65-41A9C8ACEA98","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"68a03cf3fe2a1c71ae3be31db8c6cbe7b5bc8c34","datavalue":{"value":{"entity-type":"item","numeric-id":5096093,"id":"Q5096093"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2233532$38D5CC40-1320-4E5A-B389-ADEA243C7805","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1adaabe77fae7e58bd068065a122d5510bf1aada","datavalue":{"value":{"entity-type":"item","numeric-id":1702927,"id":"Q1702927"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2233532$CAD7CA7C-CA31-470C-88C6-9745F5CF7EE7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2dd2c11b2a2bcd992c004f592e948dc3927627ea","datavalue":{"value":{"entity-type":"item","numeric-id":5166691,"id":"Q5166691"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2233532$79CC482B-86C7-4D74-A4CB-E47F18DAB3A4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8c99e7be4209b5184c2cb47a84230803bbe72743","datavalue":{"value":{"entity-type":"item","numeric-id":888469,"id":"Q888469"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2233532$ACFE8D96-851D-441C-8849-7D3453A21EAF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"632143a12812e0e87ca17f511a00c35f2ee01dd5","datavalue":{"value":{"entity-type":"item","numeric-id":3452270,"id":"Q3452270"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2233532$EB162BE1-E645-469C-9E1B-04BFCA3ED2FB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5543be9943ed5afa4e775fa2b368abaa7788d4fe","datavalue":{"value":{"entity-type":"item","numeric-id":5326308,"id":"Q5326308"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2233532$E89797B5-3CD8-487A-BD16-EAD26F39B9B7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"83c978ed0eb834f46527acd6a93f4b47491cfbfd","datavalue":{"value":{"entity-type":"item","numeric-id":5206960,"id":"Q5206960"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2233532$6D6B3409-DC42-4198-AA26-271FB72F915F","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"688dc3a554669b3a1e0ced4ab92a8787af0109bc","datavalue":{"value":{"entity-type":"item","numeric-id":2233493,"id":"Q2233493"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"947ede83b3814f6f6ebfc56b09ff547322e6666b","datavalue":{"value":{"amount":"+0.86376125","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2233532$9E09EED2-52C4-49B0-B7FE-9AE5351DF911","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c1e52ff3503169fff6ea55799525db57e03fb434","datavalue":{"value":{"entity-type":"item","numeric-id":6487299,"id":"Q6487299"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a168d0ffd9652b918120dcc172eec8247fffbe6e","datavalue":{"value":{"amount":"+0.858633","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2233532$02AF8AD0-C95C-4DD9-B162-AC66884F7CB2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"49c0798fbf24a75ad9cc6ad36cf119d793a19e9a","datavalue":{"value":{"entity-type":"item","numeric-id":685861,"id":"Q685861"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"763e680b63ee6b87ea3e6df471c1a306e85dafa0","datavalue":{"value":{"amount":"+0.8566371","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2233532$ABD13EB0-1B4A-46A6-8CA5-002F53DDB967","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a4042647b40b7232d9e5d270d53453de771416c9","datavalue":{"value":{"entity-type":"item","numeric-id":5159259,"id":"Q5159259"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"67bc104f93f828c03fba9b4d6996c75cdb68d121","datavalue":{"value":{"amount":"+0.85411716","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2233532$1E6F9789-D1D5-4BB5-A122-0A95B551FEFA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5b912041c0bb4b6bf2910ba2468279c5a6153e1e","datavalue":{"value":{"entity-type":"item","numeric-id":5308361,"id":"Q5308361"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a338d9bfa6ad9a41c7913ab66a7157226e9aba35","datavalue":{"value":{"amount":"+0.8526963","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2233532$9AAC94BD-8454-40A3-9F1B-52C6FDED2AD9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"39543e823be30e37369ab04509198db83e3988ed","datavalue":{"value":{"entity-type":"item","numeric-id":2352505,"id":"Q2352505"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3207694a1e1c2ef6f56ee9eb535a5114585b7374","datavalue":{"value":{"amount":"+0.8494663","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2233532$95C249B5-7352-4344-8466-A83BA0DC9F2A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e2456a4221f4f4afd5cdaf689ddf8012c09f5d13","datavalue":{"value":{"entity-type":"item","numeric-id":1630033,"id":"Q1630033"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"010d01aecc57efaac432300f31ea7aa3cd6afb8b","datavalue":{"value":{"amount":"+0.8466115","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2233532$DB7285E0-15A9-48F7-8D9B-B910A80CC436","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4ab5af0b01032fe41b463bb1909a4831e2c66566","datavalue":{"value":{"entity-type":"item","numeric-id":816201,"id":"Q816201"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5d051dcf6d513fcbe3e314ebbcc4d647849420ff","datavalue":{"value":{"amount":"+0.845366","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2233532$4927C40B-4718-40C0-8F82-8D4E15C57474","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":"Q2233532$63F9CDD6-02A0-49F4-807B-E3B3CC2E1979","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Counterexample- and simulation-guided floating-point loop invariant synthesis","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Counterexample-_and_simulation-guided_floating-point_loop_invariant_synthesis"}}}}}