formal-verification

31 Questions
Newest Active Unanswered Frequent
Score
View
Card Compact
Do pre and post conditions take the place of in function validation?
user_70616120
•
3
3
287
spark-formal-verification spark-ada formal-methods ada formal-verification
Is it possible to call a function inside of a constructor in dafny?
user_94293750
•
2
1
113
dafny formal-verification
Can SPARK be used to prove that Quicksort actually sorts?
user_19371970
•
2
1
222
spark-formal-verification spark-ada spark-2014 ada formal-verification
Uppaal - How to force a transition when a condition becomes true?
user_123755680
•
1
2
265
uppaal model-checking formal-verification
How to convert number to string in TLA+
user_9290950
•
3
1
137
tla+ formal-verification
Coffee Can Problem in TLA+ : cannot express a task
user_20568780
•
1
1
85
tla+ formal-methods formal-verification language-specifications
While loop termination with null references in Dafny linked list implementation
user_151973130
•
4
1
172
dafny formal-verification
Potential aliasing violation in swap array indexes SPARK-Ada
user_37788920
•
4
1
161
spark-formal-verification spark-ada formal-methods ada formal-verification
Why this dafny post-condition is not inferred?
user_114501660
•
2
1
201
formal-methods dafny formal-verification formal-languages assert
If two constructor expressions of an inductive type are equal in Coq, can I do rewriting based on their corresponding arguments?
user_143634230
•
2
1
214
coq-tactic coq formal-verification proof
Hot Questions