{"entities":{"Q746778":{"pageid":748627,"ns":120,"title":"Item:Q746778","lastrevid":64031028,"modified":"2026-04-11T17:10:37Z","type":"item","id":"Q746778","labels":{"en":{"language":"en","value":"Quantified data automata for linear data structures: a register automaton model with applications to learning invariants of programs manipulating arrays and lists"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6496667"}},"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":"Q746778$542E29B7-1EB2-41D6-9933-9B52DDFE1BBA","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"4293b2a5c3356a549128491b22f9e9bb5eaadbac","datavalue":{"value":{"text":"Quantified data automata for linear data structures: a register automaton model with applications to learning invariants of programs manipulating arrays and lists","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q746778$EA72019D-7CFB-4974-B029-B286D43B91BB","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"bd86d365da938cbafe6351c60d3326c0bf97a1a8","datavalue":{"value":"1322.68121","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q746778$E9DB660C-E0C2-4DA5-92E5-463C489F9F07","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"0c7db51a0f04b9f0d6e4008fbb01a7a758126343","datavalue":{"value":{"entity-type":"item","numeric-id":746777,"id":"Q746777"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q746778$46714050-F319-47E0-BA4E-77E64BDC944E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"0725b78a7cc86600064fbe63488e61e381f5862f","datavalue":{"value":{"entity-type":"item","numeric-id":436609,"id":"Q436609"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q746778$E0647521-2D5C-41A9-ACAE-5BB1FF22CB77","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"ed7ae23aa61a0d3617ed945c3a7817f6e39ebeb8","datavalue":{"value":{"entity-type":"item","numeric-id":236078,"id":"Q236078"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q746778$20FE8233-6960-4A13-912E-9C19B2F64463","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"985ba93433527f6d082a450a60d069993898369d","datavalue":{"value":{"entity-type":"item","numeric-id":477196,"id":"Q477196"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q746778$A5719CA2-DE45-473F-90CA-634114791F37","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":"Q746778$38589A95-B091-416A-A742-41D62B70ABB3","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"0ca124807d665f1ac71f73d3aada45c27dfaabea","datavalue":{"value":{"time":"+2015-10-20T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q746778$5C34F834-74AC-473C-BEEC-919865355A49","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"9b78776a56fc28cdd893baa47605a105412b838a","datavalue":{"value":"68Q45","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q746778$3F77A8CA-62D2-419B-A91D-34C7C7CCCB2C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"14cf74de25853c940589b125137b792dfb2d092b","datavalue":{"value":"68P05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q746778$058432CE-1747-4704-8A9B-E4AE7E2DD4BB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"c189c45b466f89dd188bd061df8c45f23f05da60","datavalue":{"value":"68Q32","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q746778$B16ED123-C338-4B73-ACA5-DEF76D7FB946","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"272ed8d576f1143df57605d69439d871c7e8e3da","datavalue":{"value":"6496667","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q746778$A41012BC-FB32-41A1-A46F-037C0CB5A5FA","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"63467bf16b953efa969cb4a512af0da42bc7d580","datavalue":{"value":"quantified data automata","type":"string"},"datatype":"string"},"type":"statement","id":"Q746778$E4E7D253-A265-4FED-9893-40D1D21ECE84","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e5a87656c643f17b9d18de57480a720b063c65ed","datavalue":{"value":"register automata","type":"string"},"datatype":"string"},"type":"statement","id":"Q746778$70D39E4F-9397-41F6-A2C1-5D765585A9CF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"09ca32413f1d623ef3eb8d4a14ac759e926ea85f","datavalue":{"value":"invariants","type":"string"},"datatype":"string"},"type":"statement","id":"Q746778$CC7858E1-C8B4-40DD-AA1E-D2E324467D20","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"fb8aa42c7ebc44ad6e6d7ced557d579005c61f07","datavalue":{"value":"linear data structures","type":"string"},"datatype":"string"},"type":"statement","id":"Q746778$5DDD8A49-1E36-43D9-BDB6-2A100F627603","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"dce61f7956ba8734ccfeae6356632abdd5389e5d","datavalue":{"value":{"entity-type":"item","numeric-id":21859,"id":"Q21859"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q746778$FF8483EC-D050-4DBB-A195-E68465222A11","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"875fd2341d7eaef60a26a549ea0c9adfdf328e2e","datavalue":{"value":{"entity-type":"item","numeric-id":17039,"id":"Q17039"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q746778$CB6E12E3-5FA5-4A09-B904-0C68781CBFEE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"d5dcb486ea2ffc39531287854f4a7be9ffb011b4","datavalue":{"value":{"entity-type":"item","numeric-id":17045,"id":"Q17045"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q746778$A7636302-75DB-407D-B8C0-A6EE875876AA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"14bcb78167ecbe13d976fd586e0b21100a3bf946","datavalue":{"value":{"entity-type":"item","numeric-id":31317,"id":"Q31317"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q746778$94BD4490-E94C-4324-9D6D-729F052F1E56","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":"Q746778$CFC2BD06-C416-4B48-B577-E56131AFA1C0","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"a14dad5c609027afe0644915b7d3837164495270","datavalue":{"value":"https://doi.org/10.1007/s10703-015-0231-6","type":"string"},"datatype":"url"},"type":"statement","id":"Q746778$D0D7D13F-20C9-4A13-A8E7-D0E0E45227CF","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"3c81564d0965b62666e44825abbcd61922ab773e","datavalue":{"value":"W1424940833","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q746778$ECA285A3-4D07-4427-996F-C7F40826DB15","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"6a257ff0958ba2ab18651e0ae0e647b82a1a678f","datavalue":{"value":{"entity-type":"item","numeric-id":2891439,"id":"Q2891439"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q746778$5E430C13-1CEC-4CF3-AFD6-9BBF1C5B477C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6cf99323ae98ac6a76131488eacedcd6861e15fa","datavalue":{"value":{"entity-type":"item","numeric-id":5716596,"id":"Q5716596"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q746778$486D8605-0541-44E2-8A50-3B4577B96AEC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c55114ff063225064064e30c2c7ef5bef45a55b0","datavalue":{"value":{"entity-type":"item","numeric-id":1098326,"id":"Q1098326"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q746778$77947342-DBAF-4249-910C-735AA6AC9D12","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"81b832e08fea72805ceb452844918f41c978f3e9","datavalue":{"value":{"entity-type":"item","numeric-id":2891398,"id":"Q2891398"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q746778$462717F0-9234-4FDF-9E8F-89A1AF44B25B","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":"Q746778$CCAFB725-EB92-444C-8F74-5EE106F3C0AE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2f2b1ebc1ae7ffc3042b5e838a24da8662374478","datavalue":{"value":{"entity-type":"item","numeric-id":5898633,"id":"Q5898633"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q746778$3222C365-6A9A-4D16-9538-CBB081E2A342","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7339bf9b2529ffb9a27c9cdd0542578668a99679","datavalue":{"value":{"entity-type":"item","numeric-id":3617752,"id":"Q3617752"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q746778$E79265BB-DAB9-4F15-B353-304E8292E7B2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"27d82d8fbef7207e3a8c855b494fb9281aee4749","datavalue":{"value":{"entity-type":"item","numeric-id":2365762,"id":"Q2365762"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q746778$B0AAED5C-4D38-42BD-B120-A8EF0B3193E7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"600d8a1514e6fed4e4c66ebeb9b62bee4bc86b61","datavalue":{"value":{"entity-type":"item","numeric-id":4417936,"id":"Q4417936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q746778$B544966C-408D-4DC9-956F-18A07E81F9D5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2e24ed71623d6e24c8ca66fec437f2e2cbe4112f","datavalue":{"value":{"entity-type":"item","numeric-id":5899065,"id":"Q5899065"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q746778$A56863AA-6194-42B7-9F47-AE9B6883DA28","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8fac60edc46b96d391fd19f103e4a89f46a0a07b","datavalue":{"value":{"entity-type":"item","numeric-id":5674988,"id":"Q5674988"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q746778$9C46EED0-3D91-45C8-BD33-84E023FE2B40","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4bd9b88bb298728fba36d6cb290ee95ccae0a7ca","datavalue":{"value":{"entity-type":"item","numeric-id":2763999,"id":"Q2763999"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q746778$3439F230-9AAF-43B1-A792-9DD4E483D88B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a346b0d1d8d58eca29ba3d568dd9754ed71fd2e5","datavalue":{"value":{"entity-type":"item","numeric-id":1866725,"id":"Q1866725"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q746778$3F200E23-B0AF-42C3-A8D5-3821FF35A130","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f9d0dd7bb6db6a4c0ce328175c5c1c2e0bc50527","datavalue":{"value":{"entity-type":"item","numeric-id":5429322,"id":"Q5429322"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q746778$34B399CD-E134-42B9-9338-CB710A1BDA0A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4864c48578bc17fdc12bcc55684bf742669ee818","datavalue":{"value":{"entity-type":"item","numeric-id":5936849,"id":"Q5936849"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q746778$76709DC2-BA04-4324-9086-4CF66F0AD3F6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2ce3fdb25869b2331ba7a9099e1dd155ad2fca1d","datavalue":{"value":{"entity-type":"item","numeric-id":5606985,"id":"Q5606985"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q746778$FED4FFA9-76DB-42AF-89EE-D577B42820AF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4fe3e421d6e27edd88e225f74f1b132c62664aca","datavalue":{"value":{"entity-type":"item","numeric-id":5408581,"id":"Q5408581"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q746778$73121D6B-E4C5-40F1-9BD4-214FF56915F4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"348369ca3fccbe91226809a75cbf31afd7f3186d","datavalue":{"value":{"entity-type":"item","numeric-id":5900666,"id":"Q5900666"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q746778$5339B9A1-625B-4A3E-8F16-5C3DDEAEAACA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1f1a62c24cddf605dd86a399f231d937d5444e0b","datavalue":{"value":{"entity-type":"item","numeric-id":5458341,"id":"Q5458341"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q746778$AA6CF354-7461-4928-98F2-6DF1CBB788FD","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":"Q746778$8C74EA9E-6208-4503-839A-545F8B21BF9D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e5a574ab536b9912335aad961dffa8e10e5de9c9","datavalue":{"value":{"entity-type":"item","numeric-id":3392917,"id":"Q3392917"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q746778$945C2035-9352-40C3-9C62-8F332894ADB9","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"bac33e02dd5684029dff21890130dedfafa64a08","datavalue":{"value":"10.1007/S10703-015-0231-6","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q746778$95B3271D-88EC-4FC4-8D0B-2705DF18CB28","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5631e06bb919f640a7ee184e157cdc880a5765c8","datavalue":{"value":{"entity-type":"item","numeric-id":5166760,"id":"Q5166760"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"20e095ca2e0543387bd98c315b31afca1849d159","datavalue":{"value":{"amount":"+0.7893602848052979","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":"Q746778$29B2B397-333C-4DF3-96C2-6C4FAA695932","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"dec9633d04db8cff8795190b36a98a9ec14a0c47","datavalue":{"value":{"entity-type":"item","numeric-id":2891417,"id":"Q2891417"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c9bf90c711d1b296941595fe17910baf68b560c7","datavalue":{"value":{"amount":"+0.7417765259742737","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":"Q746778$8668E86A-185B-4F50-B4CB-BE25A6B8B4D2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ce1abcd28212359b17461bb1a44a21bd9b2b2a25","datavalue":{"value":{"entity-type":"item","numeric-id":2938772,"id":"Q2938772"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ec75fc0b4870ce6223d2fa6b2cd86239d4ffd55e","datavalue":{"value":{"amount":"+0.7272471189498901","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":"Q746778$FEFDC92F-B7B9-41A9-9FB6-FE69624D744A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"60246da0c1f1273fefc043f6fdf356f6bc2246e4","datavalue":{"value":{"entity-type":"item","numeric-id":5300834,"id":"Q5300834"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"168e806d77a70c9902345bd248ed75aabee6cbf7","datavalue":{"value":{"amount":"+0.7260233163833618","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":"Q746778$3B063ACC-001D-49D7-968D-99C3B1F780B7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"56b1ff0a0d692ffae2fe3f33b2bf8a10b2ec6ef9","datavalue":{"value":{"entity-type":"item","numeric-id":5144658,"id":"Q5144658"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ab7627c31cd8f0dbbcca9dd6d96ceccc66155e28","datavalue":{"value":{"amount":"+0.7181792259216309","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":"Q746778$8CFBC8C8-1EE7-45B8-974F-9C2A3128FF7D","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Quantified data automata for linear data structures: a register automaton model with applications to learning invariants of programs manipulating arrays and lists","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Quantified_data_automata_for_linear_data_structures:_a_register_automaton_model_with_applications_to_learning_invariants_of_programs_manipulating_arrays_and_lists"}}}}}