Introduce composable symbolic execution interface in pyx

Aperta

#4,939 aperta il 24/6/2026 0 commenti 0 reazioni 1 assegnatario Vedi su GitHub

@Stevengre ci sta già lavorando.

Dal 24/6/2026.

Valutazione

Questa issue non è ancora stata valutata.

provide CSE interface in pyk;
1. Top-down: The initial state of the specification is state that hits it during its caller's exploration.
2. Incremental: The summaries are generated when the previous summaries are not launched.
Existing Work: CSE in kontrol; jh/ksum-cse-evaluation in mir-semantics;

Leggi tutta la issue e poi la guida ai contributi del progetto.
Commenta sulla issue per dire che te ne occupi tu — evita che due persone facciano lo stesso lavoro.
Fai un fork del repository e lavora su un branch.
Apri una pull request che faccia riferimento al numero della issue.

Concolic Explorer
Aperta
- Qualcosa non va?
Difficoltà 5/5 Più di una settimana Idoneità per principianti 32/100

runtimeverification/k#4937 · Aperta il 18/6/2026
All-path reachability proof checker
Aperta
- Qualcosa non va?
Difficoltà 5/5 Più di una settimana Idoneità per principianti 30/100

runtimeverification/k#4936 · Aperta il 18/6/2026
Accelerating all-path reachability proofs with one-path reachability proofs
Forse di nuovo libera @Stevengre l’ha presa 103 giorni fa e non c’è nessuna pull request aperta. Aperta
- Qualcosa non va?
type:epic

runtimeverification/k#4934 · 4 commenti · 1 assegnatario · Aperta il 15/6/2026
Support progressive depth halving as a generic policy in `Prover.advance_proof`
Forse di nuovo libera @Stevengre l’ha presa 123 giorni fa e non c’è nessuna pull request aperta. Aperta
- Qualcosa non va?
runtimeverification/k#4924 · 1 assegnatario · Aperta il 29/5/2026
non-evaluator attribute requires manual propagation across entire call chain
Aperta
- Qualcosa non va?
area:haskell-backend area:llvm-backend priority:p2 status:icebox type:feature

Difficoltà 5/5 Più di una settimana Idoneità per principianti 25/100

runtimeverification/k#4904 · Aperta il 17/3/2026