{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":33259867,"defaultBranch":"master","name":"boogie","ownerLogin":"boogie-org","currentUserCanPush":false,"isFork":false,"isEmpty":false,"createdAt":"2015-04-01T16:46:31.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/11760572?v=4","public":true,"private":false,"isOrgOwned":true},"refInfo":{"name":"","listCacheKey":"v0:1715908571.0","currentOid":""},"activityList":{"items":[{"before":"1bbfbdc89fdc0e7621db4fcbb8e8909cf80df011","after":"8bb34c0b9985f3e8acfb7cce96ab19761a03b664","ref":"refs/heads/IS2","pushedAt":"2024-05-20T11:34:07.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"NamrathaG","name":"NamrathaG","path":"/NamrathaG","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/26926142?s=80&v=4"},"commit":{"message":"added TT checker","shortMessageHtmlLink":"added TT checker"}},{"before":"0558613f6bee8b24b12c790fb0f8f429d1a62058","after":"44a7a93dac747285f73056b36ad0e3a4a3c4f3c6","ref":"refs/heads/master","pushedAt":"2024-05-17T05:54:43.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"shazqadeer","name":"Shaz Qadeer","path":"/shazqadeer","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/7672086?s=80&v=4"},"commit":{"message":"[Civl] Fix signature of Fractions APIs (#886)\n\nCo-authored-by: Shaz Qadeer ","shortMessageHtmlLink":"[Civl] Fix signature of Fractions APIs (#886)"}},{"before":null,"after":"89a32bb919d41524de0f52aefd767e01f90feda1","ref":"refs/heads/fix-frac-sig","pushedAt":"2024-05-17T01:16:11.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"shazqadeer","name":"Shaz Qadeer","path":"/shazqadeer","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/7672086?s=80&v=4"},"commit":{"message":"first commit","shortMessageHtmlLink":"first commit"}},{"before":"3583ebb1c0233583669748c7b6061c68099f022e","after":"0558613f6bee8b24b12c790fb0f8f429d1a62058","ref":"refs/heads/master","pushedAt":"2024-05-14T02:52:22.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"shazqadeer","name":"Shaz Qadeer","path":"/shazqadeer","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/7672086?s=80&v=4"},"commit":{"message":"[Civl] Fixed treiber stack (#885)\n\nThis PR fixes the Treiber stack sample.\r\n- new feature to split One T with respect to a given Set K using new\r\ntype Fraction T K and new APIs to go between One T and Fraction T K\r\n- use the feature to fix the proof\r\n\r\n---------\r\n\r\nCo-authored-by: Shaz Qadeer ","shortMessageHtmlLink":"[Civl] Fixed treiber stack (#885)"}},{"before":"fda7ef92473758f9ab3ae1705875cdcb1bda0552","after":"883a9f99498ab189a3632f6792d691a76d8fc332","ref":"refs/heads/treiber-v2","pushedAt":"2024-05-14T02:40:34.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"shazqadeer","name":"Shaz Qadeer","path":"/shazqadeer","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/7672086?s=80&v=4"},"commit":{"message":"update","shortMessageHtmlLink":"update"}},{"before":"7d895cc1e85bd1aa6e93ab0a1cbbc01a041b719d","after":"fda7ef92473758f9ab3ae1705875cdcb1bda0552","ref":"refs/heads/treiber-v2","pushedAt":"2024-05-14T02:29:54.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"shazqadeer","name":"Shaz Qadeer","path":"/shazqadeer","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/7672086?s=80&v=4"},"commit":{"message":"deleted old files","shortMessageHtmlLink":"deleted old files"}},{"before":"0f767080f84a558e03c33771801aa0fc34c3366f","after":"7d895cc1e85bd1aa6e93ab0a1cbbc01a041b719d","ref":"refs/heads/treiber-v2","pushedAt":"2024-05-14T02:28:29.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"shazqadeer","name":"Shaz Qadeer","path":"/shazqadeer","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/7672086?s=80&v=4"},"commit":{"message":"added comments","shortMessageHtmlLink":"added comments"}},{"before":"29a0136b3a3eb7fb76d261284ed146717817437e","after":"0f767080f84a558e03c33771801aa0fc34c3366f","ref":"refs/heads/treiber-v2","pushedAt":"2024-05-14T02:17:41.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"shazqadeer","name":"Shaz Qadeer","path":"/shazqadeer","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/7672086?s=80&v=4"},"commit":{"message":"fixed it","shortMessageHtmlLink":"fixed it"}},{"before":"069a2a6e53db9bf0731c9cdc2ce10feeac63ec43","after":"29a0136b3a3eb7fb76d261284ed146717817437e","ref":"refs/heads/treiber-v2","pushedAt":"2024-05-13T13:59:34.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"shazqadeer","name":"Shaz Qadeer","path":"/shazqadeer","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/7672086?s=80&v=4"},"commit":{"message":"completed the code","shortMessageHtmlLink":"completed the code"}},{"before":"82a1b5a0b71360b5a1f30b210ecec1ef6f74206a","after":"069a2a6e53db9bf0731c9cdc2ce10feeac63ec43","ref":"refs/heads/treiber-v2","pushedAt":"2024-05-13T05:36:55.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"shazqadeer","name":"Shaz Qadeer","path":"/shazqadeer","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/7672086?s=80&v=4"},"commit":{"message":"added more layers and one splitting","shortMessageHtmlLink":"added more layers and one splitting"}},{"before":null,"after":"82a1b5a0b71360b5a1f30b210ecec1ef6f74206a","ref":"refs/heads/treiber-v2","pushedAt":"2024-05-12T14:08:40.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"shazqadeer","name":"Shaz Qadeer","path":"/shazqadeer","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/7672086?s=80&v=4"},"commit":{"message":"first commit","shortMessageHtmlLink":"first commit"}},{"before":"ed4339c967c9d21db1eb2a52a2f2239608c76087","after":"3583ebb1c0233583669748c7b6061c68099f022e","ref":"refs/heads/master","pushedAt":"2024-05-12T04:42:45.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"shazqadeer","name":"Shaz Qadeer","path":"/shazqadeer","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/7672086?s=80&v=4"},"commit":{"message":"[Civl] refactored treiber stack (#884)\n\nMade Node type more reusable by adding another type parameter.","shortMessageHtmlLink":"[Civl] refactored treiber stack (#884)"}},{"before":"850d500b6865b61b8cef2b0aa1902e4cddff11d8","after":"303806a555e7f7d9d6771cf921702ae5ab35a639","ref":"refs/heads/ts-refactor","pushedAt":"2024-05-12T04:34:23.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"shazqadeer","name":"Shaz Qadeer","path":"/shazqadeer","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/7672086?s=80&v=4"},"commit":{"message":"second commit","shortMessageHtmlLink":"second commit"}},{"before":null,"after":"850d500b6865b61b8cef2b0aa1902e4cddff11d8","ref":"refs/heads/ts-refactor","pushedAt":"2024-05-12T04:21:57.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"shazqadeer","name":"Shaz Qadeer","path":"/shazqadeer","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/7672086?s=80&v=4"},"commit":{"message":"first commit","shortMessageHtmlLink":"first commit"}},{"before":null,"after":"1bbfbdc89fdc0e7621db4fcbb8e8909cf80df011","ref":"refs/heads/IS2","pushedAt":"2024-05-10T07:28:23.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"NamrathaG","name":"NamrathaG","path":"/NamrathaG","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/26926142?s=80&v=4"},"commit":{"message":"counting movers to decide IS1 or IS2","shortMessageHtmlLink":"counting movers to decide IS1 or IS2"}},{"before":"0b805ca96719fc51ecac137ff02d1176c6d551f4","after":"ed4339c967c9d21db1eb2a52a2f2239608c76087","ref":"refs/heads/master","pushedAt":"2024-05-05T23:04:53.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"shazqadeer","name":"Shaz Qadeer","path":"/shazqadeer","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/7672086?s=80&v=4"},"commit":{"message":"[Civl] small fixes to Treiber stack example (#883)\n\nThis PR updates the primitive atomic actions in treiber stack so that\r\nthey uniformly follow the pattern of Map_Get, Map_Put, Cell_Unpack,\r\nCell_Pack, etc.\r\n\r\nThe outstanding problems are as follows:\r\n- Most primitive atomic actions do Map_Get on ts at the beginning and\r\nMap_Put on ts at the end. The proof would be better if each primitive\r\natomic action did at most one Map_Get or Map_Put.\r\n- There is a problematic assume in AtomicLoadNode#0 without which the\r\nproof does not succeed. The issue seems related to the first point. To\r\nclean up the proof, it seems that we need to maintain and prove an\r\ninvariant at the lowest level---either top is nil or top is a member of\r\nstack.","shortMessageHtmlLink":"[Civl] small fixes to Treiber stack example (#883)"}},{"before":null,"after":"5532c7b821d5902f7a5698291b8aa7d7ac93c246","ref":"refs/heads/small-fixes","pushedAt":"2024-05-05T22:53:20.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"shazqadeer","name":"Shaz Qadeer","path":"/shazqadeer","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/7672086?s=80&v=4"},"commit":{"message":"update","shortMessageHtmlLink":"update"}},{"before":"1f5cb83de135d747283b7cdf7d010e88e68d8860","after":"0b805ca96719fc51ecac137ff02d1176c6d551f4","ref":"refs/heads/master","pushedAt":"2024-05-04T22:48:16.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"shazqadeer","name":"Shaz Qadeer","path":"/shazqadeer","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/7672086?s=80&v=4"},"commit":{"message":"[Civl] Add Cell type (#882)\n\nThis PR adds the Cell type to capture a singleton map. \r\n- Map_Pack and Map_Unpack are replaced with Cell_Pack and Cell_Unpack\r\nrespectively.\r\n- The signatures of Map_Get and Map_Put are updated to use Cell.","shortMessageHtmlLink":"[Civl] Add Cell type (#882)"}},{"before":"50a6de91a7a063955ee8a2e738e74a477889dd3c","after":"dbe291832e668b31a2d5a6efca198cddc20a441e","ref":"refs/heads/add-cell","pushedAt":"2024-05-04T20:43:18.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"shazqadeer","name":"Shaz Qadeer","path":"/shazqadeer","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/7672086?s=80&v=4"},"commit":{"message":"replaced the use of type Cell with type Foo in these tests","shortMessageHtmlLink":"replaced the use of type Cell with type Foo in these tests"}},{"before":null,"after":"50a6de91a7a063955ee8a2e738e74a477889dd3c","ref":"refs/heads/add-cell","pushedAt":"2024-05-04T20:31:31.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"shazqadeer","name":"Shaz Qadeer","path":"/shazqadeer","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/7672086?s=80&v=4"},"commit":{"message":"first commit","shortMessageHtmlLink":"first commit"}},{"before":"fdb0883072622d0a6a63a7f709bdbb36943c69e4","after":"1f5cb83de135d747283b7cdf7d010e88e68d8860","ref":"refs/heads/master","pushedAt":"2024-05-02T19:23:07.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"shazqadeer","name":"Shaz Qadeer","path":"/shazqadeer","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/7672086?s=80&v=4"},"commit":{"message":"IS1 test for prover died exception (#881)\n\nRelated to https://github.com/boogie-org/boogie/issues/879","shortMessageHtmlLink":"IS1 test for prover died exception (#881)"}},{"before":null,"after":"8a31286910f1671b2231f9250a0072ccfe35fb54","ref":"refs/heads/rec-IS1","pushedAt":"2024-05-02T12:09:35.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"NamrathaG","name":"NamrathaG","path":"/NamrathaG","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/26926142?s=80&v=4"},"commit":{"message":"IS1 test for prover died exception","shortMessageHtmlLink":"IS1 test for prover died exception"}},{"before":"b7426be30a8ba93999357d5c2d24358517139171","after":"fdb0883072622d0a6a63a7f709bdbb36943c69e4","ref":"refs/heads/master","pushedAt":"2024-04-30T23:15:34.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"shazqadeer","name":"Shaz Qadeer","path":"/shazqadeer","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/7672086?s=80&v=4"},"commit":{"message":"Naming bug in is-constructor (#880)\n\nFixes #879\r\n\r\nCo-authored-by: Shaz Qadeer ","shortMessageHtmlLink":"Naming bug in is-constructor (#880)"}},{"before":null,"after":"47b5649e8f12ed164662eb7e8c6e7d642dca33da","ref":"refs/heads/namer-fix","pushedAt":"2024-04-30T23:07:18.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"shazqadeer","name":"Shaz Qadeer","path":"/shazqadeer","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/7672086?s=80&v=4"},"commit":{"message":"first commit","shortMessageHtmlLink":"first commit"}},{"before":"83a8f7272f803a980e5eac338f4998fc101962a5","after":"b7426be30a8ba93999357d5c2d24358517139171","ref":"refs/heads/master","pushedAt":"2024-04-28T04:03:38.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"shazqadeer","name":"Shaz Qadeer","path":"/shazqadeer","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/7672086?s=80&v=4"},"commit":{"message":"Added sample for snaphot (#878)\n\nAdded a sample for the snapshot algorithm which returns an atomic\r\nsnapshot using the double collect trick without using locks.","shortMessageHtmlLink":"Added sample for snaphot (#878)"}},{"before":"b5b7b86eda22264f8d2eb3af6e0ec830805d95b1","after":"4d089806a414eaecd252aed471fd4adc90d591b2","ref":"refs/heads/snapshot","pushedAt":"2024-04-27T23:07:02.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"NamrathaG","name":"NamrathaG","path":"/NamrathaG","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/26926142?s=80&v=4"},"commit":{"message":"layer fixes","shortMessageHtmlLink":"layer fixes"}},{"before":"f5c7a8af501d4d326b45814b14bab51b2403b566","after":"b5b7b86eda22264f8d2eb3af6e0ec830805d95b1","ref":"refs/heads/snapshot","pushedAt":"2024-04-26T16:54:18.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"NamrathaG","name":"NamrathaG","path":"/NamrathaG","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/26926142?s=80&v=4"},"commit":{"message":"updated reads to return","shortMessageHtmlLink":"updated reads to return"}},{"before":null,"after":"f5c7a8af501d4d326b45814b14bab51b2403b566","ref":"refs/heads/snapshot","pushedAt":"2024-04-26T13:28:54.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"NamrathaG","name":"NamrathaG","path":"/NamrathaG","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/26926142?s=80&v=4"},"commit":{"message":"Added sample for snaphot","shortMessageHtmlLink":"Added sample for snaphot"}},{"before":"fa6624ea749b82b190b99ca9f64a7f85efc017f4","after":"83a8f7272f803a980e5eac338f4998fc101962a5","ref":"refs/heads/master","pushedAt":"2024-04-26T12:35:42.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"keyboardDrummer","name":"Remy Willems","path":"/keyboardDrummer","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3121201?s=80&v=4"},"commit":{"message":"Move classes into separate files (#875)\n\n### Changes\r\n\r\nThis PR moves some classes from the VCExpr project, that were in large\r\nfiles, into separate files.","shortMessageHtmlLink":"Move classes into separate files (#875)"}},{"before":"443683c51e98a8706a9e70f1c9289b209261537a","after":"fa6624ea749b82b190b99ca9f64a7f85efc017f4","ref":"refs/heads/master","pushedAt":"2024-04-25T20:04:59.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"shazqadeer","name":"Shaz Qadeer","path":"/shazqadeer","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/7672086?s=80&v=4"},"commit":{"message":"[Civl] Fixed bug in typechecking of yielding loops (#877)\n\nCo-authored-by: Shaz Qadeer ","shortMessageHtmlLink":"[Civl] Fixed bug in typechecking of yielding loops (#877)"}}],"hasNextPage":true,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"djE6ks8AAAAETrlajwA","startCursor":null,"endCursor":null}},"title":"Activity ยท boogie-org/boogie"}