Proofs for non-terminating programs loop in `pyk prove`
Nobody has claimed this yet.
Assessment
- Difficulty
- 4/5
- Estimated time
- 3-5 days
- Newbie friendliness
- 35/100
Research direction
Reproduce the behavior from the prove-problem branch in scratch/prove-problem, using the pyk prove command and comparing it with kprove using legacy kore-exec. Investigate the proof execution path for the terminating-branch and while true {} cases; done means non-terminating proofs no longer loop silently and the user receives an appropriate warning or failure.
Written by the indexing model from the issue text.
Description
Branch prove-problem contains an example of a proof (in directory scratch/prove-problem) for a small IMP-like language.
The proof claim states a property of a while loop but the loop is not guaranteed to terminate by the given path condition.
This is not acknowledged by the pyk prove utility (nor by kprove using legacy kore-exec).
In particular:
- If there is an execution branch which terminates in the target state, the proof is considered as passing.
- If none of the execution branches are terminating (for instance, using a simple
while true {}as the program), thepyk proofcommand loops (andkproveconsiders the proof as passing).
While 1) is probably OK (considering that the proof is only partial), 2) is clearly undesirable. There might be ways to detect when the exact same state is reached again while executing a program (detecting the infinite loop), and a warning could be issued to the user, at least in simple cases.
- Dominant language
- Python
- Stars
- 591
- Forks
- 163
- PR merge metrics
- No merged PRs in 30d
Contributor guide
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
More from runtimeverification/k
-
runtimeverification/k#4939 · 1 assignee ·
-
Concolic Explorer Open
Difficulty 5/5 Over a week Newbie friendliness 32/100
runtimeverification/k#4937 ·
-
Difficulty 5/5 Over a week Newbie friendliness 30/100
runtimeverification/k#4936 ·
-
type:epic
runtimeverification/k#4934 · 4 comments · 1 assignee ·
-
runtimeverification/k#4924 · 1 assignee ·
All issues in runtimeverification/k
Similar issues
-
Difficulty 2/5 1-3 hours Newbie friendliness 74/100
bancolombia/sentinel#23 ·
-
test md OpenCI
Difficulty 2/5 1-3 hours Newbie friendliness 74/100
-
integration:quickjs org:external priority:backlog topic:code-interpreter topic:middleware type:feature
Difficulty 2/5 1-3 hours Newbie friendliness 74/100
langchain-ai/deepagents#6450 ·
-
bug client
Difficulty 2/5 1-3 hours Newbie friendliness 88/100
-
Difficulty 2/5 1-3 hours Newbie friendliness 74/100