The tag has no wiki summary.

learn more… | top users | synonyms

0
votes
0answers
20 views

Modelling Non-deterministic Finite automata In CBMC [closed]

A non-deterministic finite automaton is a 5-tuple Q, Σ, δ, I, F as Usual . I have to model a non-deterministic finite automaton accepting all strings ending with the letter b . Automaton is ...
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 ...
0
votes
1answer
87 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 ...
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 ...
4
votes
3answers
310 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 ...