393
questions
0
votes
1
answer
45
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 ...
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 ...
1
vote
1
answer
32
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 ...
0
votes
2
answers
52
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 ...
1
vote
1
answer
52
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 ...
2
votes
1
answer
65
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
46
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
73
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
10
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
32
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'...
1
vote
1
answer
38
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 ...
0
votes
2
answers
31
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 ...
1
vote
2
answers
54
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
25
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
143
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
68
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 ...
0
votes
1
answer
219
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 ...
2
votes
0
answers
55
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 ...
1
vote
1
answer
56
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 ...
2
votes
0
answers
74
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
99
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
125
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 ...
0
votes
0
answers
23
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;
...
2
votes
1
answer
77
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 ...
1
vote
0
answers
25
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 ...
0
votes
1
answer
112
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"
...
0
votes
0
answers
61
views
Dafny verification fails "post condition might not hold"
i am new here (my first question)
We are supposed to use a given code from a website and convert it into dafny code.
The code logic itself is supposedly good.
When i try to convert the code in dafny ...
2
votes
1
answer
78
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 ...
0
votes
1
answer
73
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);
...
1
vote
0
answers
100
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
84
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, ...
0
votes
0
answers
50
views
Uppaal 5.1.0-beta3 Wrong Number of process locations
I decided to reproduce the following model from the uppaal SMC tutorial
tutorial print.
When I check its syntax using UPPAAL (5.1.0-beta3) I run into the error "Wrong number of process locations&...
1
vote
1
answer
64
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 ...
1
vote
1
answer
65
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 ==> ...
1
vote
1
answer
211
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 ...
1
vote
1
answer
367
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 ...
1
vote
1
answer
196
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 ...
0
votes
0
answers
87
views
How to use Isabelle's command line commands in macOS
I have installed the Isabelle 2023 on my MacBook and I want to use command line commands to compile the proof. However, when I enter the command like isabelle jedit -d . -l the terminal just tell me ...
2
votes
1
answer
155
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 ...
0
votes
1
answer
130
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? ...
1
vote
2
answers
164
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 ...
0
votes
2
answers
45
views
Dafny: How to call 'verifcationLogger:csv'?
I'm trying to debug variable verification time in Dafny. I try to run verificationLogger, but get no output.
I'm on Windows (but would be happy with a Linux solution)
I set my path to the version of ...
1
vote
1
answer
42
views
Checked Non-Terminating Recursive Def?
The following appears to type check in Lean 4:
def len_succ {a:Type} (h:a)(t:List a) : (h::t).length = t.length+1 :=
by
induction t
repeat simp
def pop {a:Type} (st:List a)(n:Nat)(r:n <= st....
0
votes
1
answer
47
views
Why Does Rewrite Fail to Bind?
In the following, the rewrite fails because it "did not find instance of the pattern in the target expression":
example (l1:List Nat)(l2:List Nat)(n:Nat)(r:l1.length >= n)(p:l1.length = ...
0
votes
1
answer
104
views
Dafny: Why does "Math.Max" validate faster than a local "Max"?
When I use the standard library Math.Max my project validates in seconds.
include "../libraries/src/Collections/Sets/Sets.dfy"
import Dafny.Math
When I instead copy the function into by own ...
0
votes
1
answer
128
views
Dafny: Generic method on a base type and a subset type?
Can I define a generic method on a base type and subset type?
For example, we might later use the generic function by having
T0 be the sets of integers, and
T1 be the non-empty sets of integers
I ...
0
votes
1
answer
74
views
Dafny: Library of common operations such as partition?
I'd like to partition a sequence s with a predicate p, producing two sequences is_p and not_p. Post conditions would be that every element in p is now in is_p or not_p, in the appropriate order and ...
1
vote
2
answers
120
views
Trying for a little Dafny proof about "touching" integers
I'd like to prove that if integer a is less than integer b and they are touching, then a+1==b. I define touching as there not being an integer i between a and b.
Can this work? (If not, I can beg the ...