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
-
-
-
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.
-
-
-
-
-
SaaSHub
SaaSHub - Software Alternatives and Reviews. SaaSHub helps you find the best software and product alternatives
-
-
-
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).
-
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.
-
KeyToField-smt
A Kafka Connect Single Message Transform (SMT) that enables you to append the record key to the value as a named field
-
-
SaaSHub
SaaSHub - Software Alternatives and Reviews. SaaSHub helps you find the best software and product alternatives
Project mention: Lean4 helped Terence Tao discover a small bug in his recent paper | news.ycombinator.com | 2023-10-27
Another problem with LLVM I’ve heard about is that it’s intermediate language or API or something is a moving, informally-specified target. People who know LLVM internals might weigh in on that claim. If true, it’s actually easier to target C or a subset of Rust just because it’s static and well-understood.
Two projects sought to mitigate these issues by going in different directions. One was a compiler backend that aimed to be easy to learn with well-specified IL. The other aimed to formalize LLVM’s IL.
http://c9x.me/compile/
https://github.com/AliveToolkit/alive2
There have also been typed, assembly languages to support verification from groups like FLINT. One can also compile language-specific analysis with a certified to LLVM IL compiler. Integrating pieces from different languages can have risks. That (IIRC) is being mitigated by people doing secure, abstract compilation.
> 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
TLA+ has also had an SMT-based backend, Apalache [1], for a few years now. In general, you encode your system model (which would be the Rust functions for Verus, the TLA model for Apalache) and your desired properties into an SMT formula, and you let the solver have a go at it. The deal is that the SMT language is quite expressive, which makes such encodings... not easy, but not impossible. And after you're done with it, you can leverage all the existing solvers that people have built.
While there is a series of "standard" techniques for encoding particular program languages features into SMT (e.g., handling higher-order functions, which SMT solves don't handle natively), the details of how you encode the model/properties are extremely specific to each formalism, and you need to be very careful to ensure that the encoding is sound. You'd need to go and read the relevant papers to see how this is done.
[1]: https://apalache.informal.systems
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.
This might be what you’re looking for: https://nus-optimizer.com/
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?
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).
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 | 6 May 2024
Index
What are some of the best open-source SMT projects? This list will help you:
| Project | Stars | |
|---|---|---|
| 1 | manticore | 3,640 |
| 2 | FStar | 2,570 |
| 3 | liquidhaskell | 1,150 |
| 4 | alive2 | 681 |
| 5 | py2many | 599 |
| 6 | jlcparts | 491 |
| 7 | smack | 424 |
| 8 | apalache | 410 |
| 9 | stainless | 347 |
| 10 | sbv | 233 |
| 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 | 18 |
| 19 | KeyToField-smt | 16 |
| 20 | JLCDB | 4 |
| 21 | Hsmtlib | 4 |
Sponsored
SaaSHub - Software Alternatives and Reviews
SaaSHub helps you find the best software and product alternatives
www.saashub.com