{"payload":{"pageCount":1,"repositories":[{"type":"Public","name":"mlopt","owner":"ZJU-Automated-Reasoning-Group","isFork":false,"description":"","allTopics":[],"primaryLanguage":{"name":"Python","color":"#3572A5"},"pullRequestCount":0,"issueCount":0,"starsCount":2,"forksCount":0,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-04-05T08:15:01.650Z"}},{"type":"Public","name":"canary","owner":"ZJU-Automated-Reasoning-Group","isFork":true,"description":"A unification-based alias analysis and related tools","allTopics":[],"primaryLanguage":{"name":"C++","color":"#f34b7d"},"pullRequestCount":0,"issueCount":0,"starsCount":8,"forksCount":14,"license":"GNU Affero General Public License v3.0","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-03-21T12:51:06.881Z"}},{"type":"Public","name":"PythonStAn","owner":"ZJU-Automated-Reasoning-Group","isFork":true,"description":"A static analysis framework for Python","allTopics":[],"primaryLanguage":{"name":"Python","color":"#3572A5"},"pullRequestCount":0,"issueCount":0,"starsCount":0,"forksCount":1,"license":"BSD 3-Clause \"New\" or \"Revised\" License","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-03-18T08:52:02.536Z"}},{"type":"Public","name":"arlib","owner":"ZJU-Automated-Reasoning-Group","isFork":false,"description":"Automated Reasoning Lib","allTopics":[],"primaryLanguage":{"name":"Python","color":"#3572A5"},"pullRequestCount":0,"issueCount":0,"starsCount":6,"forksCount":1,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-01-04T11:17:16.804Z"}},{"type":"Public","name":"fuzzlib","owner":"ZJU-Automated-Reasoning-Group","isFork":false,"description":"A library for fuzzing","allTopics":[],"primaryLanguage":{"name":"Python","color":"#3572A5"},"pullRequestCount":0,"issueCount":0,"starsCount":1,"forksCount":0,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2023-12-21T14:18:29.145Z"}},{"type":"Public","name":"SVF","owner":"ZJU-Automated-Reasoning-Group","isFork":true,"description":"Static Value-Flow Analysis Framework for Source Code","allTopics":[],"primaryLanguage":{"name":"C++","color":"#f34b7d"},"pullRequestCount":0,"issueCount":0,"starsCount":0,"forksCount":421,"license":"Other","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2023-12-18T08:04:52.968Z"}},{"type":"Public","name":"sparrow","owner":"ZJU-Automated-Reasoning-Group","isFork":false,"description":"A static analyzer for building callgraphs of C/C++ programs","allTopics":[],"primaryLanguage":{"name":"C++","color":"#f34b7d"},"pullRequestCount":0,"issueCount":0,"starsCount":3,"forksCount":1,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2023-12-06T07:18:28.439Z"}},{"type":"Public","name":"EasyBC","owner":"ZJU-Automated-Reasoning-Group","isFork":true,"description":"Tool chains of EasyBC","allTopics":[],"primaryLanguage":{"name":"C","color":"#555555"},"pullRequestCount":0,"issueCount":0,"starsCount":1,"forksCount":1,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2023-11-15T11:46:11.772Z"}},{"type":"Public","name":"smt","owner":"ZJU-Automated-Reasoning-Group","isFork":false,"description":"","allTopics":[],"primaryLanguage":{"name":"C++","color":"#f34b7d"},"pullRequestCount":0,"issueCount":0,"starsCount":3,"forksCount":0,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2023-10-24T06:13:56.093Z"}},{"type":"Public","name":"z3","owner":"ZJU-Automated-Reasoning-Group","isFork":true,"description":"The Z3 Theorem Prover","allTopics":[],"primaryLanguage":{"name":"C++","color":"#f34b7d"},"pullRequestCount":0,"issueCount":0,"starsCount":0,"forksCount":1448,"license":"Other","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2023-10-20T08:54:26.779Z"}},{"type":"Public","name":"efmc","owner":"ZJU-Automated-Reasoning-Group","isFork":false,"description":"Software Model Checking via Exists-Forall Solving","allTopics":[],"primaryLanguage":{"name":"Slash","color":"#007eff"},"pullRequestCount":0,"issueCount":0,"starsCount":4,"forksCount":0,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2023-08-18T17:59:43.110Z"}},{"type":"Public","name":"TPLite","owner":"ZJU-Automated-Reasoning-Group","isFork":true,"description":"ISSTA'23 - Third-party Library Dependency for Large-scale SCA in the C/C++ Ecosystem: How Far Are We?","allTopics":[],"primaryLanguage":{"name":"Python","color":"#3572A5"},"pullRequestCount":0,"issueCount":0,"starsCount":1,"forksCount":9,"license":"Apache License 2.0","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2023-07-24T08:31:49.074Z"}},{"type":"Public","name":"smtfuzz","owner":"ZJU-Automated-Reasoning-Group","isFork":false,"description":"A fuzzer for SMT solvers","allTopics":[],"primaryLanguage":{"name":"Python","color":"#3572A5"},"pullRequestCount":0,"issueCount":1,"starsCount":18,"forksCount":2,"license":"GNU General Public License v3.0","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2023-06-14T12:24:15.228Z"}},{"type":"Public","name":"Spear","owner":"ZJU-Automated-Reasoning-Group","isFork":false,"description":"Static analysis for Python","allTopics":[],"primaryLanguage":{"name":"Python","color":"#3572A5"},"pullRequestCount":0,"issueCount":0,"starsCount":2,"forksCount":0,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2023-03-23T13:22:07.561Z"}},{"type":"Public","name":"MeGASampler","owner":"ZJU-Automated-Reasoning-Group","isFork":true,"description":"SMTSampler: Efficient Stimulus Generation from Complex SMT Constraints","allTopics":[],"primaryLanguage":{"name":"SMT","color":"#ccc"},"pullRequestCount":0,"issueCount":0,"starsCount":1,"forksCount":9,"license":"BSD 3-Clause \"New\" or \"Revised\" License","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2022-12-20T08:00:03.063Z"}},{"type":"Public","name":"jkind","owner":"ZJU-Automated-Reasoning-Group","isFork":true,"description":"JKind - An infinite-state model checker for safety properties in Lustre","allTopics":[],"primaryLanguage":{"name":"Java","color":"#b07219"},"pullRequestCount":0,"issueCount":0,"starsCount":0,"forksCount":32,"license":"Other","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2022-11-29T09:15:49.084Z"}},{"type":"Public","name":"DryadSynth","owner":"ZJU-Automated-Reasoning-Group","isFork":true,"description":"A SyGuS Solver","allTopics":[],"primaryLanguage":{"name":"C++","color":"#f34b7d"},"pullRequestCount":0,"issueCount":0,"starsCount":0,"forksCount":7,"license":"MIT License","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2022-04-15T13:31:50.352Z"}}],"repositoryCount":17,"userInfo":null,"searchable":true,"definitions":[],"typeFilters":[{"id":"all","text":"All"},{"id":"public","text":"Public"},{"id":"source","text":"Sources"},{"id":"fork","text":"Forks"},{"id":"archived","text":"Archived"},{"id":"template","text":"Templates"}],"compactMode":false},"title":"Repositories"}