Stack Exchange Network

Stack Exchange network consists of 174 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange

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

0
votes
1answer
18 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(...
1
vote
2answers
37 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 ...
1
vote
0answers
17 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....
3
votes
2answers
60 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]\!]\...
3
votes
1answer
86 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 ...
2
votes
2answers
70 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 ...
0
votes
1answer
24 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 (...
0
votes
1answer
23 views

How to solve for the precondition give a postcondtion that must satisfy two conditions

I tried solving past exam question but there is this one that I haven't been able to solve. The question states that a suitable precondition should be found for the statement. $$ a= i +2; i++\{(a = ...
0
votes
1answer
45 views

Topics from theoretical computer science suitable for a bachelor (undergrate) thesis? [closed]

Is the field of theoretical computer science so complex, that it is just "too much" for a bachelor thesis? Unfortunately I haven't found any old thesises because the relevant chair of the university ...
1
vote
1answer
41 views

Software code generation from the (operational) semantics - reference request for automatic programming

Are there research trends that try to research code generation directly from the (operational or some other kind of) semantics? One can imagine cognitive architecture that discovers and reasons about ...
1
vote
0answers
27 views

How Model Checking works with User Interaction

In order to understand how to apply Model Checking, I am wondering how to apply it to a pseudo-realistic async program. Say I have the following pseudocode: ...
0
votes
2answers
95 views

An example of something you can formally verify with proofs in Software Development

I have been working on understanding formal verification of software. Formal methods include things like modeling your software with Petri Nets, Automata, or State-Transition Graphs. Other techniques ...
0
votes
0answers
17 views

How to combine Symbolic Model Checking with Symbolic Execution

I have started reading some textbooks and papers on Model Checking, and have run into the closely related but different Symbolic Execution. I have a few open questions on StackOverflow about the "...
2
votes
1answer
44 views

What exactly state is in Model Checking

So I finally realized the difference between transition systems and automata, and now am closer to understanding Model Checking. One of the last pieces is understanding what exactly "state" is in ...
4
votes
1answer
81 views

How does TLC check liveness properties?

The paper "Model Checking TLA+ Specifications" published in 1999 explained how TLC (Temporal Logic Checker) checks safety properties written in TLA+ developed by Lamport. At that time, TLC did not yet ...
1
vote
0answers
22 views
3
votes
1answer
56 views

High-level requirements for a Proof of “Saving to the Database”

This question is about a few sentence description of what a proof would look like (and technologies / logics involved) for a complex api call through many layers. Trying to get a sense of the ...
1
vote
1answer
19 views

How to use Hoare Logic to Prove this Assertion

Given this assertion in Hoare Logic: \begin{align} &\mathbf{\{p >= 0\}}\\ &s = 0 ; n = 1 ;\\ &\mathtt{while}\ (n <= p)\ \{\\ &\quad s = s + n ;\\ &\quad n = n + 1\\ &\}\\...
0
votes
1answer
49 views
2
votes
1answer
30 views

Any mathematical tools for analyzing mutable memory

Wondering if there are any documents, theories, or methodologies for dealing with mutable memory mathematically. Basically a formal algebraic model of how computers manipulate memory. Along the lines ...
3
votes
1answer
49 views

Single Input Single Output Sequential Circuit Explanation Required

I'm a student of Formal Methods in Software Engineering, I'm trying to study this question for two days but still haven't figured it out, I couldn't even find a similar solution or explanation, so ...
5
votes
2answers
90 views

How does automated verification of systems with infinitely many states work?

I need some help with basic definitions and intuition to understand why and how it's possible to verify systems with infinitely many states. For example, if I consider an x86 computer, and assuming ...
3
votes
1answer
50 views

Weak bisimulation up-to $\approx$

Given this definition of weak bisimilarity: A configuration relation $\mathcal{R}$ is a weak bisimulation provided that whenever $P\ \mathcal{R}\ Q$ and $\alpha$ is $\mu$ or $\tau$ action then: $...
1
vote
0answers
63 views

Most efficient unification algorithm?

I've been trying to find the most efficient unification algorithm by following reference chains on the Wikipedia article on unification. As far as I can tell, the fastest one is the one presented in "...
3
votes
0answers
48 views

Passing arrays vs functions as arguments in SMT?

In SAT Modulo Theories (SMT), with the theory of uninterpreted functions, all functions are first order, that is, they don't take functions as arguments or return functions. In the theory of arrays, ...
2
votes
1answer
44 views

Minimal Deterministic Buchi Automata Product

Problem: Let $\varphi = \varphi_1 \land \varphi_2$ be Deterministic Buchi Automata (DBA) expressible LTL formulas. Let $A$, $A_1$ and $A_2$ be translated DBAs such that ${\cal{L}}(A) = {\cal{L}}(A_1)...
0
votes
0answers
17 views

What is the name for the theory that guarantees proof for negative and not for all possible positives

I have heard of some people mentioning the general rule that says that you can only ever guarantee that a program will not capture the negative cases but you can never guarantee that it captures all ...
2
votes
0answers
95 views

Novel escape analysis algorithm for Java

Today I read a very interesting article about escape analysis in Java called Escape Analysis for Object Oriented Languages: Application to Java I think I have some grasp on how escape analysis works ...
3
votes
0answers
30 views

State-of-the-art for Set Constraints?

I've recently stumbled across the field of Set constraints for program analysis, that is, solving equations of the form $exp_1 \subseteq exp_2$, where (depending on the particular variant of the ...
1
vote
0answers
34 views

Determining when equal 2CNF has pure literal

Let us assume that we have a 2CNF $\varphi(X,y)$. Then we want to see if there is equal formula where $y$ (or $\overline y$) is pure literal. Can this be done in polynomial time? Are there some ...
2
votes
0answers
26 views

Problem with definition of bisimularity

In my model checking class we have defined a bisimulation like this: Let $K=(S,S_0,Act,R,L)$ and $K'=(S',S'_0,Act,R',L')$ be two kripke structures. A relation $B \subseteq S \times S'$ is called ...
3
votes
1answer
36 views

Cut costly functions in inter-procedural abstract interpretation

I am performing some inter-procedural abstract interpretation to capture certain program properties. Following the standard way, what I am doing is to maintain a work list of to-be-analyzed functions, ...
1
vote
1answer
78 views

Formal specification; Logical formula

* Initial Question * I'm trying to write a logical formula consists of three Boolean variable C1, C2, C3. My program takes graph as input and checks properties about them. C1 represents presence of ...
4
votes
0answers
71 views

In ontology development, where do axioms come from?

I am developing an ontology. I've got the classes, relationships and I guess I could come up with instances at this point too. But what I'm really focused on is the axioms. I've learnt that the ...
16
votes
2answers
2k views

Program Correctness, The specification

From Wikipedia: In theoretical computer science, correctness of an algorithm is asserted when it is said that the algorithm is correct with respect to a specification. But the problem is that to get ...
5
votes
1answer
56 views

Efficient Algorithm Linear Temporal Logic to Deterministic Rabin Automata

I am trying to construct an equivalent Deterministic Rabin Automata (DRA) given a Linear Temporal Logic (LTL) Formula. One (expensive) way to do this would be to construct an equivalent Non-...
3
votes
1answer
190 views

What does “AF AX p” mean in CTL?

Both Logic in Computer Science (Huth and Ryan, 2004) and Branching vs. Linear Time: Final Showdown (Vardi, 2002), state something to this effect (paraphrased): In LTL, X F p and F X p are ...
4
votes
0answers
42 views

How the $EX(f)$ is evaluated in symbolic model checking?

I was reading the symbolic model checking, So there it has mentioned that we can represent the set of states and transition relations of any transition system with the help of ROBDDs. I was trying to ...
1
vote
0answers
47 views

Operational Semantics - Include SKIP, SEQUENCE and IF?

I'm writing a paper for a programming languages workshop in which I have to describe the semantics of a new optimization for Java using Operational Semantics, small step style. I have never used ...
9
votes
3answers
862 views

Why does the state remain unchanged in the small-step operational semantics of a while loop?

Usually I see that in the structural operational semantics representation for the while loop, the program state don't change: $(while \> B \> do \>S, \sigma) \rightarrow (if \>B \> ...
1
vote
0answers
32 views

How to prove that $\lfloor{\sqrt{n}\rfloor} = \Theta(\sqrt{n})$? [duplicate]

It is quite direct to prove that $\lfloor{\sqrt{n}\rfloor} = O(\sqrt{n})$. But how can I prove that $\lfloor{\sqrt{n}\rfloor} = \Omega(\sqrt{n})$?
1
vote
1answer
117 views

How to verify a property about a certain order of events in TCTL / UPPAAL?

I'd like to check if a certain order of events happens if another property holds true using UPPAAL and TCTL. ...
17
votes
2answers
1k views

What is this fraction-like “discrete mathematics”–style notation used for formal rules?

In the paper "A Conflict-Free Replicated JSON Datatype", I encountered this notation for formally defining "rules": What is this notation called? How do I read it? For example: the ...
2
votes
1answer
44 views

Where in the toolchain does formal specification come in?

Where is the formal spec located? Like this? Are tests made from formal or informal spec? I saw a project where they where generated from a the formal spec and that never made sense to me. Is the ...
1
vote
0answers
37 views

How to prevent the change of other objects in Z specification?

I have Z specification of Banking system, whose fragments are: and I think that the specification is OK, but my professor says that this specifiction is completely wrong, because AddAccount ...
1
vote
2answers
100 views

Efficient algorithms for checking non-emptiness of the language of a Turing machine

I know that language non-emptiness is TM recognizable, and one can perform a BFS to find an input string that TM accepts, if there is any. But, what is the most efficient algorithm for that?
2
votes
1answer
54 views

What are these questions in the PoplMark challenge asking?

I was reading the paper Mechanized Metatheory for the Masses: the PoplMark Challenge by Aydemir et al (PDF) and I found the following three questions on page 13 of the PDF a bit confusing. ...
1
vote
2answers
56 views

How to prevent deletion in an array in the B method

I have created a very basic model of an array list in the B method as shown below ...
2
votes
0answers
97 views

Proving weak simulation

I want to prove something but I am not sure if it is the right way to do it. I have two LTS that define different semantics. A=($Q_a,Λ,\to)$, and B=$(Q_b,Λ\cup\{\beta\},\leadsto)$, where $\beta$ is ...
1
vote
1answer
158 views

Using B-method, and formal methods in general, to model and verify a reverse linked list

I am trying to do some formal modeling of a linked list, however instead of referencing the next block, each block needs to reference the previous block instead. Is there already any formal methods ...