Questions tagged [key-formal-verification]
KeY is an open-source formal software verification tool, mainly for deductively proving program correctness of Java source code.
9
questions
0
votes
0
answers
35
views
Error while connecting Z3 solver to KeY 2.8.0. in command line
I am new to KeY and am trying to set everything up so that I can start verification procedures. To do so, I need to enable SMT Solver: Z3. I downloaded the Z3 file, but when filling in the directory ...
0
votes
0
answers
49
views
Key-Formal-Verification with Xtext 2.25
I am working on a project with formal verification with key in Java.
I am using the Eclipse Plugin for that.
Everything worked fine when I had Xtext Version 2.10.
For some reasons though, I hat to ...
1
vote
1
answer
48
views
Cannot prove basic functions relying only on Implementations/Inlining
I have this class Course. I can prove the passed(int i) method when I use the contract for getBar(), not without it. Besides the contract of getBar() is also proven. Why can't I prove passed with ...
1
vote
1
answer
89
views
Z3 disable assertion simplification for proofs
Is there any way to disable simplification/rewriting of assertions in Z3 (version 4.8.8)?
I am currently working on proof replay of Z3 proofs within KeY (https://www.key-project.org). However, to be ...
0
votes
1
answer
113
views
Key Java JML proover passes this algorithm that reads a specific array element which triggers a NullPointerException? it should fail instead
I'm tyring to better understand the limits of the Key proover for Java.
I have come up with a scenario where a specific array element will trigger a null pointer exception.
When I run this through the ...
0
votes
2
answers
69
views
Why does this KeY dynamic logic problem get prooved, surely incrementing a java int of 2147483647 by 1 should be -2147483648?
Below is the entry for a KeY Dynamic Logic problem file (.key).
The file is prooved when I run in using the KeY theorem proover.
Why does this KeY dynamic logic problem get prooved, surely ...
1
vote
1
answer
154
views
Formal verification with 'KeY' in Java fails to prove array reset loop
Currently I'm trying to grasp a little bit of formal verification with the KeY tool for Java programs.
Here is my key-annotated Java code:
public class Test {
public int[] a;
/*@ public ...
5
votes
1
answer
79
views
KeY struggles to handle ternary operator
I am playing around with KeY (https://www.key-project.org) for a teaching project.
On one hand I was happy that KeY easily proves correctness of the following jml annotated java code
/*@ ensures ((\...
5
votes
1
answer
272
views
Where does the KeY verification tool shine?
What are some code examples demonstrating KeY’s strength?
Details
With so many Formal Method tools available, I was wondering where KeY is better than its competition, and how? Some readable code ...