Get real-time insights from all types of time series data with InfluxDB. Ingest, query, and analyze billions of data points in real-time with unbounded cardinality. Learn more →
Top 21 SMT Open-Source Projects
-
-
Project mention: Lean4 helped Terence Tao discover a small bug in his recent paper | news.ycombinator.com | 2023-10-27
-
InfluxDB
Power Real-Time Data Analytics at Scale. Get real-time insights from all types of time series data with InfluxDB. Ingest, query, and analyze billions of data points in real-time with unbounded cardinality.
-
-
Project mention: Basic SAT model of x86 instructions using Z3, autogenerated from Intel docs | news.ycombinator.com | 2023-05-15
You can use it to (mostly) validate small snippets are the same. See Alive2 for the application of Z3/formalization of programs as SMT for that [1]. As far as I'm aware there are some problems scaling up to arbitrarily sized programs due to a lack of formalization in higher level languages in addition to computational constraints. With a lot of time and effort it can be done though [2].
-
> Another problem is that there are hundreds of built-in library functions that need to be compiled from Python from C
An approach I've advocated as one of the main authors of py2many is that all of the python builtin functions be written in a subset of python[1] and then compiled into native code. This has the benefit of avoiding GIL, problems with C-API among other things.
Do checkout the examples here[2] which work out of the box for many of the 8-9 supported backends.
[1] https://github.com/py2many/py2many/blob/main/doc/langspec.md
-
-
-
WorkOS
The modern identity platform for B2B SaaS. The APIs are flexible and easy-to-use, supporting authentication, user identity, and complex enterprise features like SSO and SCIM provisioning.
-
-
-
sbv
SMT Based Verification in Haskell. Express properties about Haskell programs and automatically prove them using SMT solvers.
-
-
-
kryptonite-for-kafka
Kryptonite for Kafka is a client-side 🔒 field level 🔓 cryptography library for Apache Kafka® offering a Kafka Connect SMT, ksqlDB UDFs, and a standalone HTTP API service. It's an ! UNOFFICIAL ! community project
-
-
-
SMPT
SMPT is a SMT-based model checker for Petri nets focused on reachability problems that takes advantage of net reductions (polyhedral reductions).
I also found https://github.com/nicolasAmat/SMPT maybe it should be used because SMT, Z3 looks familiar. It's used in fancy new theorem provers.
-
nus-timetable-optimizer
Codebase for the NUS Timetable Optimizer, a tool to help students at the National University of Singapore optimize their timetables to their liking.
This might be what you’re looking for: https://nus-optimizer.com/
-
-
KeyToField-smt
A Kafka Connect Single Message Transform (SMT) that enables you to append the record key to the value as a named field
-
Cool. I also did something like this a while back that can be found here but i scratched it since i relied on csv dumps on jlcpcb and they decided to remove that. How do you get the data?
-
-
SaaSHub
SaaSHub - Software Alternatives and Reviews. SaaSHub helps you find the best software and product alternatives
NOTE:
The open source projects on this list are ordered by number of github stars.
The number of mentions indicates repo mentiontions in the last 12 Months or
since we started tracking (Dec 2020).
The latest post mention was on 2024-02-19.
SMT related posts
- What new features would you like to see in NUSMods?
- NUS Guide for Incoming Undergraduates
- If You've Got Enough Money, It's All 'Lawful'
- [ANNOUNCE] New release of SBV with support for quantifiers
- John Regehr: Alive2 LLVM optims verification
- liquidhaskell ghc9に対応したリリース出てたの知らなんだ
- [Hobby] Amateur Generalist Programmer Seeking to Put Bugfixing Skills to Good Use
-
A note from our sponsor - InfluxDB
www.influxdata.com | 18 Apr 2024
Index
What are some of the best open-source SMT projects? This list will help you:
| Project | Stars | |
|---|---|---|
| 1 | manticore | 3,631 |
| 2 | FStar | 2,558 |
| 3 | liquidhaskell | 1,147 |
| 4 | alive2 | 671 |
| 5 | py2many | 590 |
| 6 | jlcparts | 483 |
| 7 | smack | 422 |
| 8 | apalache | 401 |
| 9 | stainless | 347 |
| 10 | sbv | 235 |
| 11 | z3_tutorial | 147 |
| 12 | suslik | 121 |
| 13 | kryptonite-for-kafka | 78 |
| 14 | hz3 | 57 |
| 15 | sbvPlugin | 44 |
| 16 | SMPT | 27 |
| 17 | nus-timetable-optimizer | 18 |
| 18 | lsmtree | 17 |
| 19 | KeyToField-smt | 16 |
| 20 | JLCDB | 4 |
| 21 | Hsmtlib | 4 |
SaaSHub - Software Alternatives and Reviews
SaaSHub helps you find the best software and product alternatives
www.saashub.com