soteria
READ-ONLY MIRROR of the previous soteria repo
Star
Fork
Watch

Commits on thread-safe

Sacha Ayoun
test: add a multi-domain thread-safety stress test
committed
Sacha Ayoun
soteria-rust: guard the temp-file cleanup registry with a mutex
committed
Sacha Ayoun
z3: serialise the shared SMT-dump channel with a mutex
committed
Sacha Ayoun
logs: make logging/trace state thread-safe
committed
Sacha Ayoun
Make global ID counters atomic
committed
Sacha Ayoun
bv_solver: use a domain-local RNG for trivial-model search
committed
Sacha Ayoun
bv/tiny solvers: share sat-check & encode memo caches across domains
committed
Sacha Ayoun
bv/tiny values: use thread-safe hash-consing
committed
Sacha Ayoun
soteria_std: add Dls and Concurrent_tbl thread-safety helpers
committed
Sacha Ayoun
Simplify README (#342)
committed
opale
Bump Charon, fixes, Rust improvements (#340)
committed
Sacha Ayoun
Remove the VSCode plugin for Soteria-C (#339)
committed
Sacha Ayoun
Deploy linux package (#337)
committed
Sacha Ayoun
Automatically balance the TreeBlocks (#335)
committed
opale
Nicer CI (#334)
committed
opale
Better symex run (#327)
committed
opale
Clean up tech debt (#326)
committed
Pedro Carrott
Consumption of non-consumable pure atoms via existential quantification (#328)
committed
opale
Automate wrappers around stubs (#325)
committed
Sacha Ayoun
Fix and test the import of Soteria as a library (#329)
committed
Sacha Ayoun
Generate flamegraphs during Symex (#259)
committed
Pedro Carrott
Existential quantifiers as symbolic values (#147)
committed
Sacha Ayoun
More stubs: `unix::time`, `env::_var`, `thread::available_parallelism`, `tokio::RngSeed::new` (#324)
committed
opale
Parametric Tree Borrows (#308)
committed
Sacha Ayoun
A few fixes on how learning of variables work (#323)
committed
Sacha Ayoun
Add callgraph support for Soteria-Rust (#321)
committed
Sacha Ayoun
atomic_xadd and overflow check (#320)
committed
Sacha Ayoun
Use released version of ppx_mixins (#319)
committed
Sacha Ayoun
Improve simplification fuzzer (shrinker, checked operators) (#274)
committed
opale
Bump Charon and Obol (#312)
committed
Sacha Ayoun
Use ppx_mixins (#317)
committed
opale
Add `[@@deriving sym_state]` (#299)
committed
Sacha Ayoun
`x * (y / x)` cannot overflow with unsigned ops (#316)
committed
opale
Add `[%l.debug ...]` PPX for logging (#310)
committed
opale
Small state improvements (#309)
committed
opale
Add `[@@deriving reversible]` (#297)
committed
Sacha Ayoun
Tutorial for Logs and Stats (#296)
committed
opale
Use indexed dynarrays rather than nested dynarrays (#298)
committed
Sacha Ayoun
Add producers and consumers with substitution to Soteria (#302)
committed
opale
Add sections to CLI arguments (#291)
committed
opale
Fix scripts for artifact (#287)
committed
opale
Symbolic Abstraction (#284)
committed
opale
Cleanup Validity in Rust (#281)
committed
opale
Support Cargo tests: `--test` (#283)
committed
Sacha Ayoun
Nightly + modularize CI (#282)
committed
opale
Re-organise Soteria Rust (#277)
committed
opale
Rust: nicer UX, add `--recursive-validity` (#273)
committed
Sacha Ayoun
Minor changes (#279)
committed
Sacha Ayoun
Improvements on Soteria on user experience for Soteria-C scripts (#276)
committed
Sacha Ayoun
Bump Grace (#261)
committed
opale
Nicer Soteria root documentation (#275)
committed
opale
Document `solvers` and some of `symex` (#266)
committed
Sacha Ayoun
Fuzzer for simplifying constructors (#272)
committed
Sacha Ayoun
fix merging of statistics in experiments script (#269)
committed
Sacha Ayoun
Update readme for "install from source" instructions (#270)
committed
Sacha Ayoun
Fixing the C package (#268)
committed
Sacha Ayoun
Create a Rust package (#265)
committed
Sacha Ayoun
Add CI check that opam files were up to date (#264)
committed
Sacha Ayoun
Rust: Make Rustsymex state carry the entire current stack trace (#263)
committed
Sacha Ayoun
Add `versionsync pull` command (#262)
committed