issues
search
flyvy-verifier
/
flyvy
An experimental framework for temporal verification based on first-order linear-time temporal logic. Our goal is to express transition systems in first-order logic and verify temporal correctness properties, including safety and liveness.
BSD 2-Clause "Simplified" License
14
stars
1
forks
source link
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
Transition system extraction
#110
Alex-Fischman
closed
1 year ago
1
Update snapshots
#109
wilcoxjay
closed
1 year ago
8
Fix a stray clippy warning
#108
tchajed
closed
1 year ago
0
Multi cartesian product fix
#107
wilcoxjay
closed
1 year ago
0
Add doc and test for the fact that a quantifier's bindings can be empty
#106
wilcoxjay
closed
1 year ago
2
Cancel solver only during `check_sat` and `get_model`
#105
tchajed
closed
1 year ago
0
Benchmark compile times and move qalpha generic instantiation into inference crate
#104
wilcoxjay
closed
1 year ago
0
Fix bdd convergence check by tracking reachable states
#103
Alex-Fischman
closed
1 year ago
0
Refactor out code to get the inits, trs, safes, and axioms from a module
#102
Alex-Fischman
closed
1 year ago
3
Fix integration tests after crate refactor
#101
Alex-Fischman
closed
1 year ago
0
Remove kissat from project
#100
Alex-Fischman
closed
1 year ago
0
Bdd convergence
#99
Alex-Fischman
closed
1 year ago
0
Fix some clippy warnings
#98
tchajed
closed
1 year ago
0
Add some missing documentation
#97
tchajed
closed
1 year ago
2
Useless wrapper in verify/error?
#96
Alex-Fischman
closed
1 year ago
1
Missing documentation for inference and temporal-verifier crates
#95
Alex-Fischman
opened
1 year ago
1
Split into crates
#94
Alex-Fischman
closed
1 year ago
6
Use `assert_killed` as implied by comment
#93
tchajed
closed
1 year ago
1
Acquire the SmtPid::terminated lock only once
#92
tchajed
closed
1 year ago
0
Update snapshots
#91
tchajed
closed
1 year ago
0
Check for errors in a robust way
#90
tchajed
closed
1 year ago
0
BDD checker should detect convergence
#89
wilcoxjay
closed
1 year ago
0
Make bounded checkers' arguments more uniform
#88
wilcoxjay
closed
1 year ago
1
Fix all missing doc warnings
#87
tchajed
closed
1 year ago
0
Improve query determinism
#86
wilcoxjay
closed
1 year ago
3
Make bdd-check and sat-check have a similar interface to set-check
#85
Alex-Fischman
closed
1 year ago
1
Add documentation for all top-level commands
#84
tchajed
closed
1 year ago
1
Only snapshot sort tests with z3
#83
tchajed
closed
1 year ago
0
Testing immutability
#82
Alex-Fischman
closed
1 year ago
0
Fix a typo in the name of a parser function
#81
wilcoxjay
closed
1 year ago
1
Sat checker
#80
Alex-Fischman
closed
1 year ago
0
Bdd checker
#79
Alex-Fischman
closed
1 year ago
0
Bump all dependencies
#78
tchajed
closed
1 year ago
0
Improvements to qAlpha algorithm
#77
edenfrenkel
closed
1 year ago
6
Save content-hashed smt2 files
#76
tchajed
closed
1 year ago
0
Document investigation into killing the solver
#75
tchajed
closed
1 year ago
0
Improve Invariant Inference (qAlpha)
#74
edenfrenkel
closed
1 year ago
0
Replace multi_cartesian_product with a correct version
#73
tchajed
closed
1 year ago
1
Set checker
#72
Alex-Fischman
closed
1 year ago
13
Z3 "incomplete quantifiers" error
#71
edenfrenkel
closed
1 year ago
2
Support for more examples
#70
edenfrenkel
closed
1 year ago
2
Draft: Add UPDR algorithm
#69
oralmer
closed
1 year ago
18
Z3 timeout during invariant inference
#68
edenfrenkel
closed
1 year ago
2
Report non-solver run time using getrusage
#67
tchajed
closed
1 year ago
0
Remember assumptions from last check_sat in get_minimal_model
#66
tchajed
closed
1 year ago
0
Remove support for --solver=cvc
#65
tchajed
closed
1 year ago
0
Run CI on pull requests
#64
tchajed
closed
1 year ago
0
running sat sovers with indicator variables produces different results
#63
oralmer
closed
1 year ago
2
Add Windows support
#62
dranov
closed
1 year ago
6
Check each invariant's consecution separately
#61
tchajed
closed
1 year ago
0
Previous
Next