LeventErkok/sbv
SMT Based Verification in Haskell. Express properties about Haskell programs and automatically prove them using SMT solvers.
HaskellNOASSERTION
Issues
- 8
- 2
Q: Results of 'wpProveWith'
#697 opened by ocramz - 0
Tower example
#696 opened by LeventErkok - 5
Zombie process fixes
#694 opened by LeventErkok - 1
ExtractIO
#692 opened by LeventErkok - 0
Create `NonEmpty` instances for `EqSymbolic`, `OrdSymbolic`, `Mergeable`, etc.
#688 opened by recursion-ninja - 1
Set support for cvc5
#690 opened by paulbrauner-da - 1
GH pages link leads to 404
#686 opened by fabeulous - 3
CrackNum decimal printing
#685 opened by LeventErkok - 2
Fix CVC5 list parsing
#683 opened by LeventErkok - 0
- 5
- 4
Re-enable sbv on stackage
#680 opened by lsrcz - 6
SArray scoping issue / weird SMT error
#679 opened by Torrencem - 1
SBV 10.3 release
#678 opened by LeventErkok - 1
Add an implementation of SHA3/Keccak
#640 opened by LeventErkok - 27
Bizarre performance issue
#642 opened by LeventErkok - 1
New overflow predicates
#657 opened by LeventErkok - 0
allSat/skolemize incompatibility
#672 opened by LeventErkok - 6
- 0
Tables/arrays in lambdas
#675 opened by LeventErkok - 0
C: Code-generation for bvExtract
#677 opened by LeventErkok - 3
Create dedicated cabal target for examples
#676 opened by 414owen - 12
Build fails on GHC 9.8.1
#674 opened by noughtmare - 1
SMTDefinable for functions beyond 7 arguments?
#670 opened by octalsrc - 2
Tables in lambda functions?
#664 opened by LeventErkok - 0
Arrays in lambda functions
#665 opened by LeventErkok - 0
Tables in smtFunction
#666 opened by LeventErkok - 0
Partition example
#671 opened by LeventErkok - 0
New example
#668 opened by LeventErkok - 9
Mourning for sbvExists/sbvForall
#658 opened by arrowd - 1
Bizarre output from observe
#667 opened by LeventErkok - 0
Improve renderSMTFunction
#663 opened by LeventErkok - 2
Feature: Partitioning all-sat results
#662 opened by LeventErkok - 2
Consider splitting examples in to separate package
#659 opened by georgefst - 2
AES improvements
#638 opened by LeventErkok - 2
Add an implementation of Prince
#639 opened by LeventErkok - 5
Version 10.0+ does not build with GHC 9.0
#655 opened by lsrcz - 1
Tactics and probes
#652 opened by LeventErkok - 2
Quantification over user-defined types
#653 opened by LeventErkok - 1
- 2
Can't compile SBVBench
#649 opened by LeventErkok - 1
Add support for special-relations
#646 opened by LeventErkok - 0
Can we separate Provable from Satisfiable
#648 opened by LeventErkok - 2
Support abduction in CVC5
#643 opened by LeventErkok - 1
Unify addAxiom and constraint, possibly?
#645 opened by LeventErkok - 32
- 3
Make folds easier to use?
#641 opened by LeventErkok - 0
Make EqSymbolic derivable
#636 opened by LeventErkok - 0
Puzzle example
#637 opened by LeventErkok