The tag has no usage guidance.

learn more… | top users | synonyms

7
votes
1answer
329 views

Data Flow Analysis with exceptions

Data flow analysis work over a control flow graph. When a language under consideration supports exceptions, control flow graph can explode. What are the standard techniques for dealing with this ...
0
votes
0answers
21 views

Complexity of choosing a suitable Boolean algebra domain for program analysis

Do you know the complexity class of the following problem? Input: A sequential non-deterministic program over integer variables, equipped with initial values of these variables. The exact ...
0
votes
0answers
21 views

Complexity of choosing a suitable positive domain for program analysis

Do you know the complexity class of the following problem? Input: A sequential nondeterministic program over integer variables, equipped with initial values of these variables. The exact ...
0
votes
0answers
36 views

Complexity of choosing a suitable disjunctive domain for program analysis

Do you know the complexity class of the following problem? Input: A sequential nondeterministic program over integer variables, equipped with initial values of these variables. The exact ...
2
votes
1answer
63 views

Proving correctness of an exponentiation routine

I have the following exponentiation routine, which takes $O(\log n)$ steps ...
0
votes
1answer
44 views

How is CFL-reachability solvable in exponential time and space?

I have read a paper which mentions that CFL-reachability is solvable in exponential time and space. Intuitively, I suppose that one need to explore through all the sub-paths in the PDA for a CFL. ...
3
votes
1answer
38 views

Anotation rules for while rule in deductive verification

I have been studying deductive verification of software lately, with weakest precondition, strongest postcondition, annotation calculus, and etc. I came across the following rules for the while ...
1
vote
1answer
98 views

Check whether loop invariants are correct?

I'm trying to prove some code is correct, using Hoare logic. How do I check whether my loop invariants are correct? I'm asked to prove (using Hoare Logic) that the following program is valid: ...
2
votes
1answer
147 views

LTL properties in bounded model checking via assertions

Is there a way to check LTL properties in a bounded model checker? As an example, consider a liveness property ($G F p$ - always eventually $p$)? Suppose we have the following trivial program ...
1
vote
2answers
77 views

How to prove if an algorithm is reentrant?

I think, maybe some formalism could exist for the task which makes it significantly easier. My problem to solve is that I invented a reentrant algorithm for a task. It is relative simple (its pure ...
1
vote
1answer
56 views

What's a side-effect free expression in Timed Automata?

I'm trying to get myself more familiar with Timed Automata theory. At some point I came across the expression "side-effect free" like in the following: A guard is a side-effect free expression ...
-1
votes
1answer
140 views

What are GEN and KILL statements in dataflow analysis?

In data flow analysis, is GEN statement where a variable is used and KILL statement is where variable is redefined?
0
votes
0answers
67 views

How to show equivalence of the Hoare assignment axiom vs Floyd assignment axiom?

I know from several sources that they are equivalent, but couldn't find a reasonable explanation. My first approach was to show their equivalence by using the logical consequence rule and both axioms, ...
1
vote
1answer
59 views

Double ended queue data abstraction and axioms

I am trying to show the data abstraction for a double ended queue along with the axioms. A double ended queue is a queue where items can be added to and remove from either end of the queue. I have ...
0
votes
1answer
189 views

Finding a Hoare logic correctness proof for a Repeat-Until loop

How can we prove a program in repeat until using Hoare Logic? I've found a rule like this: {P} S {R}, {R ^ ~B -> P}, {R ^ B -> Q} for ...
0
votes
1answer
105 views

Hoare logic - partial/total correctnes and strength invariant

I'm studying Hoare logic and I can't understand the relation between partial and total correctness regarding loop invariant. Suppose for example that I have the following program: ...
2
votes
1answer
92 views

Encoding the pigeonhole principle in CBMC

CBMC is a Bounded Model Checker for ANSI-C and C++ programs. It also supports SystemC using Scoot. It allows verifying array bounds (buffer overflows), pointer safety, ex­cep­tions and user-specified ...
0
votes
1answer
156 views

applying CTL/LTL model-checking on some system

I apologies if my title is vague, I'm trying to apply CTL/LTL model-checking on some system written in java, however, I still don't understand how to reach a result using either of the approaches ...
13
votes
4answers
820 views

How do you check if two algorithms return the same result for any input?

How do you check if two algorithms (say, Merge sort and Naïve sort) return the same result for any input, when the set of all inputs is infinite? Update: Thank you Ben for describing how this is ...
4
votes
3answers
588 views

Hoare triple for assignment P{x/E} x:=E {P}

I am trying to understand Hoare logic presented at Wikipedia, Hoare logic at Wikipedia Apparently, if I understand correctly, a Hoare triple $$\{P\}~ C ~\{Q\}$$ means if P just before C, then Q ...