Questions about methods and techniques to prove correctness of programs.

learn more… | top users | synonyms

1
vote
1answer
41 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 ...
7
votes
0answers
146 views

Why aren't we researching more towards compile time guarantees?

I love all that is compile time and I love the idea that once you compile a program a lot of guarantees are made about it's execution. Generally speaking a static type system (Haskell, C++, ...) seems ...
1
vote
1answer
19 views

Model Checking: hardware vs software

In short: What is the basic difference that allows model checking for hardware to be "easily" solvable, but makes it undecidable for software? I guess it has to boil down to the difference between ...
1
vote
1answer
19 views

Determining set of states that satisfy a CTL formulae

I'm trying to understand CTL formulae, and until now I've understood everything (or at least I thought I did). I have the following Kripke strucure: Now given the following CTL formulae ...
1
vote
0answers
86 views

How does one guarantee that the commutative, associative and distributive properties hold for a type?

While most main stream programming languages allow for user defined types that can have the following properties: associative commutative distributive the only way I know of that this can ...
6
votes
5answers
138 views

Can we quantify how close a partially correct programs is to being correct?

I know that there is something called partial correctness, but I was wondering if there was a way to tell how close a semi-correct program is to a fully correct program. For example, if you had a ...
8
votes
6answers
211 views

Could program verification techniques prevent bugs of the genre of Heartbleed from occurring?

On the matter of the Heartbleed bug, Bruce Schneier wrote in his Crypto-Gram of 15th April: '"Catastrophic" is the right word. On the scale of 1 to 10, this is an 11.' I read several years ago that a ...
2
votes
0answers
39 views

Is there any open-source tools for verifying TCTL formulae over timed automata can be imported into my project?

In my project, there is one important step to automatically verify a timed automata with TCTL formulae. I briefly surveyed the tool UPPAAL that provides a GUI to construct a timed automata and to ...
8
votes
1answer
124 views

Verify correctness of quantifier elimination, using SAT

Let $x=(x_1,\dots,x_n)$ and $y=(y_1,\dots,y_n)$ be $n$-vectors of boolean variables. I have a boolean predicate $Q(x,y)$ on $x,y$. I give my friend Priscilla $Q(x,y)$. In response, she gives me ...
12
votes
3answers
725 views

Formal program verification in practice

As a software engineer, I write a lot of code for industrial products. Relatively complicated stuff with classes, threads, some design efforts, but also some compromises for performance. I do a lot of ...
3
votes
2answers
52 views

Temporal logic for interface invariants

I am looking for some sort of temporal logic for expressing invariants in interfaces. Since interfaces do not specify data representation, the invariants must rely solely on the publicly available ...
3
votes
1answer
668 views

Evaluation of reverse Polish notation

We only consider the reverse Polish notation as an arithmetic expression. Formally, RNP is a sequence consisted of numbers and arithmetic operators: $+,-,*,/$, and its syntax is: ...
7
votes
2answers
228 views

Introduction into first order logic verification

I am trying to teach myself different approaches to software verification. I have read some articles. As far as I learned, propositional logic with temporal generally uses model checking with SAT ...
9
votes
4answers
556 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 ...
9
votes
1answer
363 views

How to deal with arrays during Hoare-style correctness proofs

In the discussion around this question, Gilles mentions correctly that any correctness proof of an algorithm that uses arrays has to prove that there are no out-of-bounds array accesses; depending on ...
15
votes
6answers
1k views

Algorithm to solve Turing's “Halting problem‍​”

"Alan Turing proved in 1936 that a general algorithm to solve the halting problem for all possible program-input pairs cannot exist" Can I find a general algorithm to solve the halting problem ...