Constraint solver based on coverage-guided fuzzing

SMT solver for the theory of floating-point arithmetic

A Fast Floating-Point Satisfiability Solver

CRS-自建Claude Code镜像，一站式开源中转服务，让 Claude、OpenAI、Gemini、Droid 订阅统一接入，支持拼车共享，更高效分摊成本，原生工具无缝使用。

Elegant LaTeX Template for Notes

SoftFloat release 3

ChatGPT国内版使用教程，一个让你呼吸顺畅的ChatGPT，支持gpt5-5，gpt5-5-thinking,Grok-4,Gemini模型,无降智

library for nonlinear optimization, wrapping many algorithms for global and local, constrained or unconstrained, optimization

🐱 跨平台互动桌宠 BongoCat，为桌面增添乐趣！

吉林大学硕博学位论文 LaTeX 模板——jluthesis2020

《Machine Learning Systems: Design and Implementation》 (V2 is launching soon）

AISystem 主要是指AI系统，包括AI芯片、AI编译器、AI推理和训练框架等AI全栈底层技术

DyNet: The Dynamic Neural Network Toolkit

an automatic differentiation framework with dynamic graph/支持动态图的自动求导框架

cvc5 is an open-source automatic theorem prover for Satisfiability Modulo Theories (SMT) problems.

Code for "Efficient Local Search for Nonlinear Real Arithmetic", VMCAI'2024

Artefact of Paper “Improving NLSAT for Nonlinear Real Arithmetic", ASE'2025

Python library using SAT/SMT samplers in MCMC algos

深度学习经典、新论文逐段精读

中科大凌青老师凸优化课程的课程笔记

PolytopeWalk: fast sparse and dense random walks on polytope, with C++ backend and Python interface

FuzzBench - Fuzzer benchmarking as a service.

SymCC: efficient compiler-based symbolic execution

Bitwuzla is a Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, floating-point arithmetic, arrays and uninterpreted functions and their combinations. Its name …

OL1V3R: solving floating-point constraints via stochastic local search