# Tagged Questions

The tag has no usage guidance.

37 views

### “taintedness” vs. “taintness”

In the context of information flow, when you talk about the property of variables being tainted, do you speak about "taintness" or "taintedness"? Both occur online, both sound weird to me. An example ...
342 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 ...
22 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 ...
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 ...
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 ...
65 views

### Proving correctness of an exponentiation routine

I have the following exponentiation routine, which takes $O(\log n)$ steps ...
48 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. ...
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 ...
106 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: ...
159 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 ...
80 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 ...
58 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 ...
151 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?
68 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, ...
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 ...
193 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 ...
107 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: ...
94 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 ...
162 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 ...
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 ...