400 questions
0
votes
0
answers
40
views
Dafny for loop is inconsistent with forall
assert (forall i, j :: 0 <= i <= j <= end ==> monotonic(arr, i, j) ==> j - i <= endFinal - startFinal) by {
for (int i = 0; i <= end; i++) {
for (int j = i; j <= ...
- 1
0
votes
1
answer
57
views
Why is the ensures clause in my Dafny method for finding the largest monotonic subarray not provable?
I am working on a Dafny program to find the largest monotonic island (strictly increasing or strictly decreasing subarray) in an array. My code defines helper functions to check if a subarray is ...
0
votes
1
answer
28
views
Verifying a type-punning, multibyte optimization
I am trying to verify a modified version of musl libc memchr which uses a type-punned optimization: it looks for the value in the prefix of the buffer until it is aligned on sizeof(size_t), then uses ...
- 1,243
0
votes
0
answers
37
views
Is verification of pointer arithmetic less difficult than pointer modification?
I was attempting to use WP to verify memchr from musl libc, which fundamentally boils down to:
void *memchr(const void *src, int c, size_t n)
{
const unsigned char *s = src;
for (; n && *s ...
- 1,243
0
votes
1
answer
87
views
Dafny method does not verify
I have a method that returns the lowest index of the first bad neighbour or -1 if there are none.
If a neighbouring pair of elements have a negative sum then the right neighbour is said to be bad. For ...
- 1
0
votes
1
answer
39
views
How to prove sequential commands C1; C2 can always execute to C2 if we know C1 always terminates?
I am using a theorem prover to demonstrate the progress of programs.
The semantics of a program are defined using a small-step relation, denoted as
ctran, between program configurations. A program ...
- 167
0
votes
1
answer
41
views
About Dafny loop invariant errors
The following code is the answer I came up with for the following problem. However, there are two main errors. By the way, this problem is problem 17 in Chapter 13 of the book "PROGRAM PROOFS&...
0
votes
2
answers
44
views
Proving correctness of Matrix Addition
I want to prove the correctness of 2D matrix addition in Dafny (using the VSCode extension) with the aim of identifying SMT-proveable loop invariants. I believe this should be fairly straight forward ...
0
votes
1
answer
62
views
accessing members of constrained type parameters in Dafny
Dafny neophyte here (again!). Below, Scope is fine, but the 'generic' version ScopeG fails with type T does not have a member id on the line forall id :: id in id2Items ==> id == id2Items[id].id. I'...
- 1,608
0
votes
1
answer
76
views
establishing facts about constants in Dafny
Dafny neophyte here. I was expecting the assertion in use_a to pass:
class A {
const a: int
constructor(a0: int)
requires a0 > 100
ensures a > 100
{
a := a0;
}
function ...
- 1,608
0
votes
1
answer
49
views
Issues with converting 2D matrix indices to 1D array index
I am trying to write a Dafny function that converts 2D matrix indices to a 1D array index. Below contains my current code.
The issue I face is that Dafny's verification times out after 20 seconds.
Is ...
0
votes
1
answer
54
views
Turn `P(?x)` into `exists x,P(x)` to give different instantiations for different subgoals in Coq
I have a goal with an existential variable ?x. In order to prove it, I need to destruct a term t, and under the different cases generated from destructing t, the term for instantiating ?x should be ...
- 81
0
votes
0
answers
24
views
Exposing local pointers in trace and producing load event in case of non-volatile load in CompCert
CompCert only exposes global pointers in trace. How difficult would be to change the overall development to expose the local pointers in trace? I understand preservation of the trace would be the ...
- 89
1
vote
1
answer
43
views
Copy a singly linked list with Frama-C
I am trying to verify the above with Frama-C. From the manuals, it seems like Frama-C isn't well suited for malloc, and function pointers. I was wondering if I am missing something in my verification ...
- 75
0
votes
2
answers
72
views
Lightweight ways to prove an assembly language steps from a certain state to another state after variable number of instructions in Coq
I want to prove that a compiler that I wrote for a toy language is correct. I defined a predicate P which relates the runtime configuration of the source toy language and the target toy assembly.
The ...
- 81
1
vote
1
answer
55
views
How to add an element to a total function while making sure no other mapping to this element exists?
I am trying to formally specify a railway interlocking system with the B method in Atelier B. The most basic underlying concept is very simple: trains can be assigned a location and an area. There can ...
- 281
2
votes
1
answer
73
views
WP Plugin: Why does the following simplified code fail to verify
I am a new Frama-C User and I am trying to prove certain properties for a large project. I was seeing a particular proof fail, and tried reducing the problem to a minimum reproducible example, and the ...
0
votes
1
answer
82
views
Why do I get "closeparen expected" error in Dafny?
I am struggling with Dafny's syntax, and I get an error that I don't know how to deal with. Here is the code:
function pow(base: int, exp: nat): int {
if exp == 0 then 1 else base * pow(base, exp -...
0
votes
1
answer
83
views
Proving the linear count slope-search algorithm in Dafny
I've been working to implement a slope search algorithm in Dafny where I have a double ascending matrix, and I want to calculate the amount of elements strictly less than a given value. Besides the O(...
0
votes
0
answers
13
views
UPPAAL SMC - How to provide a time distribution data as an input for invariant at a location and/or a guard in a transition?
I currently have information of time in the form of a distribution as shown in the image below.
I want to provide this time information(which is in the form of a distribution) as invariant in a ...
0
votes
1
answer
42
views
How to create a constant reference to an object in Dafny
I am trying to create a model of a multicore system in Dafny. Usually, in multicore systems (and in the system I'm modelling), there is an idle task -- a placeholder task that is run when a core doesn'...
- 27
1
vote
1
answer
55
views
Alloy does not find a solution (instance) for my specification
I've been following the Alloy docs and writing the spec at the same time, but I get a different result from what the docs say:
Recall that without any temporal operator, the added constrain applies ...
- 1,171
0
votes
2
answers
37
views
How to revers a seq relation in Alloy
sig Customer {
orders: seq RecordedOrder,
}
sig RecordedOrder {}
fact "example fact" {
all o:RecordedOrder |
#o.~orders > 0;
}
How can I revers the orders relation, the ...
- 3
1
vote
2
answers
55
views
How do I check if the result of symTake is equal to a concrete list?
This is my code:
{-# LANGUAGE GADTs #-}
{-# LANGUAGE OverloadedStrings #-}
import Grisette
x :: SymInteger
x = "x"
y :: SymInteger
y = "y"
numbers :: [SymInteger]
numbers = [x, ...
0
votes
0
answers
34
views
Invariants of nested loops
I have to fully annote the following program and I currently have a hard time with finding the invariants for the loops:
{ 0 <= n }
r := 0;
x := 0;
do[false] // find invariant for the outer loop
...
0
votes
2
answers
247
views
Understanding Verification Steps in Dafny when Using Recursive Functions
I am currently learning Dafny and program verification from the book Program Proofs by K. Rustan M. Leino. I came across this example in the book and I am having a hard time understanding some ...
0
votes
1
answer
83
views
Unclear behaviour of variable signatures in alloy models
I'm currently learning Alloy, and I'm struggling to understand the behaviour of variable signatures. I'm attempting to model a straightforward rental system where all items are initially available and ...
- 3
0
votes
1
answer
277
views
Formal verification of state machine with SymbiYosys not giving expected results
I'm trying to verify a very simple state machine written in verilog with SymbiYosys. It is failing and I cannot figure out what I am doing incorrectly, and would like some help in figuring it out. I ...
3
votes
1
answer
80
views
Termination for Wrapped `Fin n` in Lean4
The following example type checks in Lean 4, but I am confused why the termination_by declaration is required.
import Mathlib.Tactic.Linarith
def Idx (n:Nat) := Fin n
def sum(k:Idx n) : Nat :=
if ...
- 761
1
vote
1
answer
80
views
Dafny issue modifying array member of class
I'm trying to modify an array member of a class in Dafny. These modifications may include re-assigning the array member, modifying elements of the array member, or both. For example, consider the ...
- 95
2
votes
0
answers
93
views
How to make Spoq generate high-level specifications in Coq (not just AST) for the functions in LLVM IR
I am trying to use Spoq framework (and on GitHub) to translate code from C to Coq.
I faced problem - I am getting only low-level specifications for my functions (just AST), but I want to get high-...
0
votes
1
answer
132
views
Visualize the verification conditions in Dafny
We are doing some academic experiments in Dafny and were wondering if there is a way to see the generated verification conditions in Dafny?
We searched the literature, websites and blogs but did not ...
1
vote
1
answer
139
views
How to verify C functions with array parameters using Isabelle
I am using Isabelle to verify a C program. During the verification process, I used the c-parser install-C-file to load the code, but the following issue occurred：
attempt to cause decay to pointer on ...
0
votes
0
answers
30
views
how to model and verify model
I have written several requirements formally for modeling a real-time system. One of these requirements is as follows:
If sensor1.value is less than or equal to -5 and sensor2.value is less than or ...
- 31
0
votes
0
answers
26
views
Use NuXMV to calculate exponentiation
I want to use operator exp in NuXMV to calculate exponentiation. But the result is always 0.
I have written a simple program. The following is my program.
MODULE main
VAR
exponentiation : real;
...
- 11
2
votes
1
answer
93
views
`agda`: how to specify that a step in equational reasoning is by definition of a function?
I'm new to agda. How can I specify, when I do equational reasoning, that a specific step is by definition of a function?
For example, take the following definition of natural numbers:
open import ...
- 651
1
vote
0
answers
26
views
Do I need to install Zchaff before using NuXMV to do verification by BMC
I just install NuXMV and want to use it to do Bounded Model Checking. But in user-mannual, the writer says NuXMV doesn't contain Zchaff of minisat. So do i need to install them before starting the ...
- 11
0
votes
1
answer
126
views
Can't compile Hello World in F*
Both OCaml and F* have been successfully installed. The only thing resembling a Hello World example I was able to find was:
module Hello
open FStar.IO
let main = print_string "Hello F*!\n"
...
2
votes
1
answer
83
views
How to prove properties of non-linear operators involved in LEB128 algorithm in Dafny?
I'm trying to prove that encoding/decoding a (signed) LEB128 algorithm is lossless.
https://en.wikipedia.org/wiki/LEB128
What's got me stuck is the "Sign Extension" operation for the ...
- 31
0
votes
1
answer
92
views
SymbiYosys cover mode fails on checks that aren't covers
I am learning formal verification using PSL and VHDL with SymbiYosys.
I have the following test in Formal.psl:
vunit f_top_asm_verify(TopAssembly(Rtl))
{
default clock is rising_edge(i_clk);
...
- 31
1
vote
0
answers
120
views
Proving a counting slope search algorithm with Dafny
I've been working to implement a slope search algorithm in Dafny where I have a double ascending matrix, and I want to calculate the amount of elements strictly less than a given value. Besides the O(...
-1
votes
1
answer
102
views
How to integrate Regex into Alloy Analyzer?
I am currently modeling a container orchestrator using Alloy. It turns out that many of the facts I need to write involve regular expressions (regex). Since regex is not supported by default in Alloy, ...
- 1
1
vote
1
answer
75
views
How to capture a change in an element of an array in TLA+
I am specifying a system whose state consists of a sequence:
VARIABLE Seq
The sequence is constrained to be of a certain type:
TypeInvariant == Seq \in [Nat -> [v1: {0,1}, v2: {0,1}]]
I want to ...
- 16.8k
1
vote
1
answer
74
views
how to give a bound when traverse infinite map (imap) in Dafny?
here is an example:
type temporal = imap<int, bool>
type Behavior<S> = imap<int, S>
function stepmap(f:imap<int, bool>):temporal
ensures forall i:int :: i in f ==> ...
- 21
1
vote
1
answer
247
views
Dafny method will not verify
I have this method that returns the number of trailing zeros, and modifies the array a to replace all the trailing zeros with -1. Currently I am getting assertion might not hold error on assert s == 1 ...
- 159
1
vote
1
answer
423
views
Dafny Method to find Max fails to verify
I'm working on a Dafny program that finds the maximum element in a sequence of integers. The method Strictmax should return the maximum element and its index. If the maximum element is not unique, the ...
- 159
1
vote
1
answer
222
views
Has Frama-C been verified?
I am curious as to whether Frama-C has been formally verified using Frama-C or another verification framework, since bugs in Frama-C could possibly result in bugs in programs verified by Frama-C going ...
2
votes
1
answer
174
views
SVA assertion compile syntax errors
assert property @(posedge(clk)) !rstN |-> n==0 && full==0 && empty==1;
assert property @(posedge clk) disable iff(!rstN) ( full |=>(wr_en && $stable (n) ) );
assert ...
- 21
0
votes
1
answer
161
views
Is Symbolic Execution a formal Verification technique?
I have spent two days researching on Formal Methods and formal Verification to be more specific. I also came across Symbolic Execution and I don't know whether this is a formal verification technique? ...
user4686130
1
vote
2
answers
171
views
How to use logging to reduce verification variability
I have a project with great variabilities in verification times. I can now call the Dafny logger (see below), but I don't know
How to use the text or csv format to improve the verification.
Should I ...
- 373