issues
search
usi-verification-and-security
/
golem
Solver for Constrained Horn Clauses
MIT License
34
stars
7
forks
source link
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
Refactor MBP so that it does not require OpenSMT's ModelBuilder
#82
blishko
opened
2 days ago
0
Predicate abstraction: Proper refinement of the abstract reachability tree
#81
blishko
closed
4 days ago
0
TPA: Merge DAG nested loops
#80
BritikovKI
opened
1 week ago
0
Golem returns UNSAT for SAT instance
#79
jena-kling
closed
2 weeks ago
2
Provide common methods on SMTSolver wrapper
#78
blishko
closed
1 month ago
0
BMC: Simplify and improve the algorithm for solving general linear systems
#77
blishko
closed
1 month ago
0
BMC engine is slow compared to Z3
#76
blishko
opened
1 month ago
1
BMC: Support linear CHC system directly
#75
blishko
closed
1 month ago
0
CI: Replace starexec images with Fedora
#74
blishko
closed
1 month ago
0
Engines: Add new engine based on Predicate Abstraction and CEGAR
#73
blishko
closed
1 month ago
0
Engines: Refactor engine creation to an EngineFactory
#72
blishko
closed
2 months ago
0
OpenSMT update 2.6.0 -> 2.7.0
#71
blishko
closed
2 months ago
0
Interpret: Small cleanup related to witness printing and validation
#70
blishko
closed
2 months ago
0
TermUtils: Print negative numbers in accordance with SMT-LIB
#69
blishko
closed
3 months ago
0
Usage of negation in models produced not in line with smt-lib
#68
rodrigo7491
closed
3 months ago
0
Check handling of auxiliary variables after inlining
#67
blishko
opened
3 months ago
0
CI: Update OSX resource
#66
blishko
closed
4 months ago
0
PDKIND: Add engine
#65
stepanhen
closed
2 months ago
1
Spacer: Avoid creating unnecessary terms
#64
blishko
closed
4 months ago
0
Alethe: Fix handling of nullary predicates
#63
blishko
closed
5 months ago
0
Alethe: Generalize proof building to support non-normalized input
#62
blishko
closed
5 months ago
0
SingleLoopTransform: Deal with alien variables in validity witnesses in backtranslation
#61
blishko
closed
5 months ago
0
DAG Safety witness
#60
BritikovKI
closed
6 months ago
1
Make model output more compact
#59
blishko
closed
8 months ago
0
Alethe proof rejected
#58
blishko
closed
8 months ago
1
Alethe: Fix evaluation of modulo operation
#57
blishko
closed
9 months ago
0
Add more testing infrastructure
#56
blishko
opened
9 months ago
0
Alethe proofs rejected with rule mod_simplify
#55
rodrigo7491
closed
9 months ago
1
std::bad_alloc when running a SAT instance with --print-witness
#54
rodrigo7491
closed
8 months ago
1
Performance optimizations and small cleanup in Alethe proof production
#53
blishko
closed
9 months ago
0
Graph: More carefule node elimination
#52
blishko
closed
9 months ago
0
std::out_of_range when running with --print-witness
#51
rodrigo7491
closed
9 months ago
0
Options: added an option to turn off the TS DAG solving
#50
BritikovKI
closed
9 months ago
0
Fix incorrect behaviour detected on a test case
#49
blishko
closed
10 months ago
0
DAG-disj: Fixed conjunction to disjunction in "addRestrictions"
#48
BritikovKI
closed
10 months ago
1
DAG-fix: unique restrictions for every edge
#47
BritikovKI
closed
11 months ago
1
Proof length reduction
#46
m4mbo
closed
11 months ago
0
Figure out how to properly do the invariant backtranslation in transformation to single TS
#45
blishko
closed
5 months ago
0
Alethe proof generation
#44
m4mbo
closed
11 months ago
0
SimpleNodeEliminator: Allow restricted elimination of nodes with hyperedges
#43
blishko
closed
11 months ago
1
ITE support
#42
m4mbo
closed
1 year ago
0
Non-linearity Support
#41
m4mbo
closed
1 year ago
0
Alethe Proof Generation
#40
m4mbo
closed
1 year ago
0
Inv optimization
#39
BritikovKI
closed
5 months ago
0
Everywhere: Simplify typical use of SMT solver
#38
blishko
closed
1 year ago
0
TPA: Fix computation of explanations
#37
blishko
closed
1 year ago
0
Fix issues with witnesses for IMC and some transformation passes
#36
blishko
closed
1 year ago
0
Which quantifier elimination technique does TPA-QE use?
#35
dong-yf
closed
1 year ago
1
Implement tranformation from a general linear CHC system into a transition system
#34
blishko
closed
1 year ago
1
Engines: Refactor computation of witnesses for transition systems
#33
blishko
closed
1 year ago
1
Next