Last call to make your voice heard! Our 2022 Developer Survey closes in less than a week. Take survey.

Questions tagged [formal-methods]

a particular kind of mathematically-based technique for the specification, development and verification of software and hardware systems.

Filter by
Sorted by
Tagged with
1 vote
1 answer
38 views

What is the difference between type inhabitant and subtyping?

I am confused with the terms inhabitant vs. subtyping. For example, We usually think that "john is an inhabitant of Human". This sentence is correct, because john is an individual, and an ...
user avatar
  • 247
1 vote
1 answer
57 views

Are there invariants in text processing problems?

I have read that when programming it is good to identify relations -- invariants -- that should hold true throughout the program, and it is good to insert assertions throughout the code to check that ...
user avatar
1 vote
1 answer
112 views

Proving a predicate assignment is correct

I am currently reading Formal Methods - An Appetizer and am stuck in chapter 3 (Program Verification). I am unfamiliar with logic and I do not think I understand the $\vDash$ notation correctly. I ...
user avatar
1 vote
0 answers
23 views

What is known about the possibility of making a program to validate another program for correctness?

I'm having a question inspired by exercise 14 from section 1.2.1 of Donald Knuth's The Art of Computer Programming. It's phrased in the following way: (R. W. Floyd) Prepare a computer program that ...
user avatar
2 votes
1 answer
38 views

Abstract Interpretation: Connection between soundness relation and a Galois connection

I am currently studying the paper "Abstract Interpretation Frameworks" by Cousot and Cousot from 1992 (https://doi.org/10.1093/logcom/2.4.511) to gain an understanding of the theory behind ...
user avatar
0 votes
1 answer
41 views

Logic foundation for formal verification

What types of logic should one study as foundation before diving into the area of software verification? What I can think of are: Hoare Logic (for proving correctness of imperative programs) Linear ...
user avatar
  • 101
1 vote
0 answers
47 views

SMT validity solvers/ quantifier elimination in Ocaml

I am working on my own expression package in Ocaml and have to perform both validity queries and quantifier elimination. I have already implemented Cooper's procedure (for Presburger and Linear ...
user avatar
  • 113
1 vote
1 answer
35 views

How are pointers interpreted differently to variables in a control flow graph (CFG)?

I have been working with control flow graphs and believe I understand how they function when describing dependencies between variables. For example, given the operations: ...
user avatar
0 votes
0 answers
15 views

Intro to basic automated proof search for theorems in equational theories

I have heard about this topic, and I'm merely looking for a reference that I can read through: I know about formal logic as a proof-checking system, but I haven't yet learned about actual algorithms ...
user avatar
  • 3,464
3 votes
0 answers
24 views

Formal instruments to check properties of SQL queries

I have some operations defined as SQL queries which takes data from various tables combines it with the data from a base table and generates new rows, which are written back to the base table. In the ...
user avatar
1 vote
0 answers
25 views

Is assignment atomic in Promela?

Is assignment atomic is Promela? That is, can concurrent x = value1; and x = value2; produce anything different from value1 ...
user avatar
0 votes
0 answers
30 views

Hoare Triple Logic

I'm having trouble understanding the logic behind Hoare Triples. The question asks for the missing value of the precondition {X} ...
user avatar
2 votes
1 answer
93 views

Why sequential consistency model is widely used if it is unsound

From this talk and these lecture notes here and here I learned that sequential consistency does not actually model what really happens in practice. However, it is also pointed out that most of the ...
user avatar
  • 473
2 votes
1 answer
70 views

Is a system of equations derived from mutually recursive ADTs always uniquely solvable?

After looking at Can a computer determine whether a mathematical statement is true or not? for a while, I worry we may be into incompleteness/halting problem territory with this question, so an answer ...
user avatar
1 vote
1 answer
66 views

Z Notation: sequence of sequences - find sum

Let me just say that this is for a university project. I do not expect an answer but more of a "hint". I have a schema of a Supermarket that holds a sequence of queues: ...
user avatar
  • 111
1 vote
1 answer
48 views

Where should "imply" be placed in this formalisation?

I have to formalize the following sentence: If any house is green then there exists a horse that is white. I have formalized it the following way: $$\forall(x)(\mathit{house}(x)\rightarrow \mathit{...
user avatar
  • 113
2 votes
0 answers
50 views

Does Rice's theorem apply to sequential logic circuits?

I am wondering if Rice's theorem (or something similar to that) applies also to sequential circuits. I.e. given any finite sequential circuit, can there be an algorithm that can formally verify any ...
user avatar
  • 121
1 vote
2 answers
97 views

Interpreting a proof of $2^\mathbb{N}$ being uncountable

Suppose I have the following proof: ...
user avatar
2 votes
2 answers
352 views

A general picture of formal verification in software

I'm trying to piece together a general picture of the state of formal software verification, and I'm having a good bit of trouble. For context, I come from mostly a math background. I'm quite familiar ...
user avatar
3 votes
1 answer
80 views

How to prove that replacing a character in a string in both C and JavaScript is equivalent?

I would like to try some different proofs, specifically in proving equivalence of the implementation of some feature in two different programming languages (C and JS in this question). This is about ...
user avatar
  • 1,873
1 vote
3 answers
104 views

is (infinitely often p) ∨ (infinitely often ¬p) valid?

i'm trying to prove every trace over PROP = {p} is a model of the formula. I am very stuck in figuring out a model pi that satisfies this formula, can anyone point me in the right direction?
user avatar
  • 39
0 votes
1 answer
65 views

Z-Specification = Routes

Im trying to make an invariant for this Z schema about routes. 1) The invariant should express that each route should contain at least 20 different places. First of all i thought of doing a universal ...
user avatar
  • 39
1 vote
1 answer
111 views

LTL Model of (infinitely often p) ∧ ( infinitely often q) ∧ (¬ Eventually (p ∧ q))?

Can anyone give a model of the following LTL formula? $$ \Box\Diamond p \land \Box\Diamond q \land \lnot \Diamond (p \land q). $$ That is, we want each of $p$ and $q$ to hold infinitely often, but $p \...
user avatar
  • 39
5 votes
2 answers
155 views

proving program equivalence

I understand that the general problem of program equivalence is undecidable, but I'm wondering what approaches exist to tackle the problem? I am familiar with Hoare-style verification, but are there ...
user avatar
38 votes
5 answers
6k views

Do theorem provers demonstrate their own correctness?

I am not very well-versed in the world of theorem proving, much less automated theorem proving, so please correct me if anything I say or assume in my question is wrong. Basically, my question is: are ...
user avatar
  • 493
2 votes
2 answers
60 views

Modeling a set of probabilistic concurrent processes

I'm looking into discrete-time Markov chains (DTMCs) for use in analyzing a probabilistic consensus protocol. One basic thing I haven't been able to figure out is how to model a set of independent ...
user avatar
  • 145
0 votes
1 answer
23 views

What's the meaning of this service specification

What's the meaning of the example statement here? "A service specification S describes an interface: it specifies the behavior of certain program elements (functions or subprograms) through ...
user avatar
  • 103
4 votes
1 answer
125 views

Proving with co-induction principles

I'm going through Adam Chlipala's "Certified Programming with Dependent Types" (available here for convenience), and I'm a bit stuck at internalizing the introduction of co-induction principle for the ...
user avatar
3 votes
1 answer
46 views

Having a formal ISA specification - What does correctness mean?

Does this always mean that a program can be correct in regard to that spec or is there any correctness of the spec itself ?
user avatar
  • 31
1 vote
1 answer
66 views

Are the two LTL properties $GF(\psi_1 \land F\psi_2 )$ and $GF(\psi_2 \land F\psi_1 )$ equivalent?

Is $GF(\psi_1 \land F\psi_2 )$ equivalent to the property $GF(\psi_2 \land F\psi_1 )$? Attempt: In the first property each state must eventually see $\psi_1$ and $\psi_2$, in the second property as ...
user avatar
  • 509
2 votes
1 answer
360 views

Hoare logic, proving conjunction rule from basic rules, possible or not?

(This is HW.) Suppose I have these following proof rules given. I am currently considering if I can prove the conjunction rule (given below) from the above given Hoare logic rules. My answer would ...
user avatar
  • 179
2 votes
2 answers
62 views

(Generally) How to specify asynchronous action with side effects using logic equations

Say you have this function call sequence: function all() { fn1() fn2() fn3() } And say that fn2 was asynchronous and ...
user avatar
  • 1,873
1 vote
0 answers
50 views

Prove that set of operations form a commutative Monoid

this is my first post on this exchange. I am looking for some help with defining a proof that a set of operations I have designed forms a commutative monoid. (Disclaimer: I am not sure that I have ...
user avatar
  • 111
0 votes
0 answers
36 views

Formal language representation of program

I have numerous records, composed of words. Each word gets translated into vectors, with a variable number of channels, provided that that word exists in a specific lookup dictionary. For n number of ...
user avatar
  • 101
0 votes
1 answer
51 views

Effective Procedures and P vs NP Problem

If, suppose, P doesn't equal NP. Implication of this statement is that there is no effective procedure to solve a hard problem; however there exists an acceptable solution S. I have following two ...
user avatar
  • 135
1 vote
2 answers
218 views

Buchi automata in formal software verification

As I am studying the application of Buchi automata in formal software verification, I am interested in the computational complexity (or links to papers) for the algorithms used to solve the problem in ...
user avatar
  • 227
5 votes
1 answer
310 views

The definition of weakest precondition for a non-deterministic language

In the classical IMP language, the definition of weakest precondition is: definition "wp c Q s ≡ ∃t. (c,s) ⇒ t ∧ Q t" This is stating that from state s, after ...
user avatar
  • 2,220
3 votes
1 answer
344 views

The Law of Excluded Miracle in the language of guarded commands

The definition of weakest precondition is familiar (let me use Isabelle's syntax here): definition "wp c Q s ≡ ∃t. (c,s) ⇒ t ∧ Q t" the weakest precondition ...
user avatar
  • 2,220
2 votes
1 answer
164 views

How to prove a LTL formula correct in a specific model?

I have been learning Verification by model checking recently and I get the following question: $Whether\ the\ LTL\ formula\ M, q_3\ \models (X\ \lnot a) \rightarrow (F\ G\ \lnot a)\ is\ established\ ...
user avatar
10 votes
0 answers
110 views

Can we say McCarthy and Hoare had the same objective in the 60s regarding a mathematical theory of computation?

I don't think there's any way to ask a very precise question here, so this might be considered opinion based. Nevertheless, it seems the question is clear enough because I'm asking whether these two ...
user avatar
  • 237
6 votes
1 answer
233 views

Roadmap to formal verification

I would like to learn about different approaches to formal verification of software programs that goes beyond what Wikipedia has to offer. Ideally one would not only get an overview but also ...
user avatar
  • 161
2 votes
0 answers
125 views

Relation between “formal verification”, “formal proof”, and “type systems” for software verification?

I have a vague understanding what formal verification is about, a vague understanding of what the cutting edge is of type theory for programming languages, and a better understanding of formal proofs. ...
user avatar
  • 3,464
5 votes
2 answers
538 views

Is there a way to convert a program into a Boolean formula?

Let's say I have a program P, in form of a binary code for x86 architecture. I want to find a Boolean formula F (in form of CNF, or something like that), such ...
user avatar
  • 153
1 vote
1 answer
33 views

Define a length function over $A^{*} \leftarrow{N}$ such that $length(l)$ outputs the length of $l$

Consider the following definitions LIST: $\overline{nil} \ \ \ \ \ \frac{l}{a \ l}$ $a \in A$ $A^* = \mu \widehat{LIST}, \ A^{\infty} = v \widehat{LIST}$ NAT: $\overline{0} \ \ \ \ \ \frac{x}{s(...
user avatar
  • 143
1 vote
2 answers
78 views

How can MLTT etc encode computability?

I am recently thinking about proving the undecidability of some problem. This problem has been formalized in Coq and by staring at it, people including me think "for sure" this is undecidable. "For ...
user avatar
  • 553
3 votes
0 answers
78 views

What is the difference between the choice operator and nondeterminism in CSP?

I'm learning CSP now for my research. First time doing formal work in CS. I'm having a hard time understanding the difference between choice $\square$ operator and the nondeterminism $\sqcap$ operator....
user avatar
3 votes
2 answers
196 views

Why does the denotational semantics for a while loop have a existence quantifier?

I was going through these notes and they have the following operator on partial functions: $$ \mathcal F^{k}(\bot)(\sigma) = \left\{ \begin{array}{ll} \alpha( [\![s]\!]\sigma ) & [\![b]\!]\...
user avatar
3 votes
1 answer
237 views

Relating a proof to a Haskell program

I am trying to relate the following integer square root theorem $\forall x: \mathbb{N}, \exists y : \mathbb{N}((y^2 \leq x) \land (x < (y+1)^2))$ and its proof to its role as a specification of ...
user avatar
2 votes
2 answers
105 views

How to express the existence of winning strategy of the starter of a game in temporal logic?

Consider a two-player game. A winning strategy of a player is a strategy following which the player can always beat his opponent, no matter how his opponent responds. A game can be unfolded to a ...
user avatar
  • 9,179
0 votes
1 answer
188 views

How to collect all states of a behavior in TLA+?

Description of the problem: I am modeling checking a distributed protocol against a global property with TLA+ developed by Leslie Lamport. The global property is defined on all states of a behavior (...
user avatar
  • 9,179