Skip to main content
Filter by
Sorted by
Tagged with
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 ...
Cs_J's user avatar
  • 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 ...
Swarn's user avatar
  • 89
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 ...
user3598542's user avatar
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 ...
Cs_J's user avatar
  • 81
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 ...
Frederic's user avatar
  • 281
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 ...
LakshyAAAgrawal's user avatar
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 -...
Costel Anghel's user avatar
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(...
The Mods Hunter's user avatar
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 ...
Michael Tesla's user avatar
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'...
user401445's user avatar
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 ...
devio's user avatar
  • 1,247
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 ...
Job's user avatar
  • 3
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, ...
Stefanos Baziotis's user avatar
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 ...
Makedoneren's user avatar
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 ...
Easton McBeth's user avatar
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 ...
Job's user avatar
  • 3
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 ...
Christopher P's user avatar
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 ...
redjamjar's user avatar
  • 751
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 ...
alex's user avatar
  • 95
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-...
Natasha Klaus's user avatar
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 ...
Costel Anghel's user avatar
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 ...
riiiiyueeeejiiiiiiuzhao's user avatar
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 ...
saghar13's user avatar
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; ...
yayi-mei's user avatar
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 ...
Ivan Perez's user avatar
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 ...
yayi-mei's user avatar
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" ...
buddingprogrammer's user avatar
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 ...
Elias Hanna's user avatar
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 ...
Hongyi Lu's user avatar
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); ...
xormapmap's user avatar
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(...
The Mods Hunter's user avatar
-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, ...
bd36's user avatar
  • 1
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&...
Caio Serra's user avatar
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 ...
Andry's user avatar
  • 16.7k
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 ==> ...
ZihaoZhang's user avatar
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 ...
FreeAntiVirus's user avatar
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 ...
FreeAntiVirus's user avatar
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 ...
Aadithyaa Eeswaran's user avatar
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 ...
Huan Sun's user avatar
  • 167
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 ...
Amala Joseph's user avatar
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? ...
Nges Brian's user avatar
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 ...
Carl's user avatar
  • 373
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 ...
Carl's user avatar
  • 373
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....
redjamjar's user avatar
  • 751
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 = ...
redjamjar's user avatar
  • 751
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 ...
Carl's user avatar
  • 373
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 ...
Carl's user avatar
  • 373
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 ...
Carl's user avatar
  • 373
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 ...
Carl's user avatar
  • 373

1
2 3 4 5
8