4 ms·

I get what you're saying about the state explosion problem, but the article specifically calls out the idea of proving a lack of negative behaviors. It seems to

I get what you're saying about the state explosion problem, but the article specifically calls out the idea of proving a lack of negative behaviors. It seems to me it might be quite useful to be able to prove, for example, that a program never reads memory at random, or that it never exceeds the bounds of any allocated buffer. That's a different problem scale than "prove the whole thing works as specified".

gsnedders 13y ago
Sadly, it's not a different problem scale — the typical model is something similar to "for each state, does the property P hold?". Hence no matter the property (or complexity thereof), one must still enumerate all states.
- CHY872 13y ago
  Of course, one will attempt to also find equivalence classes for the states! The code long x = user_input(); if (x == 0) { violate_model(); } else { do_something(); } you would expect by any reasonable implementation to collapse the system into just two equivalent states that can be tested.
  - wsxcde 13y ago
    Ah, but finding equivalence classes of states is quite tricky! Obviously the naive approach of enumerating states and assigning them to equivalence classes is dead on arrival. You might be hinting at examining control flow predicates with your example. This technique is called predicate abstraction and underlies a lot of the SLAM effort. It works in certain scenarios - A statement which more or less captures the state of the field itself.
    - CHY872 13y ago
      What I'm personally hinting at is symbolic/concolic execution. Essentially, each variable has a set of constraints associated with it - initially left blank for an input variable, for example. Then, the program can be executed, with assignments producing new constraints and replacing old ones. At each point in control flow, the executor chooses a path, and adds new constraints. When a dangerous statement (assertion, pointer dereference etc) is reached, the constraints can be solved by z3 or some other SMT solver, and if it can find a satisfying result you automatically have a test case that will produce erroneous or undefined behaviour. It works quite well for short programs, actually - the KLEE people (or maybe it was DART) found bugs in busybox, GNU Coreutils etc. The current approach is to instead of traversing your control flow tree explicitly (which means you're doing a tree search over a potentially infinite tree), converting the program such that it produces a logical statement that can be solved by an SMT solver, that is satisfiable iff there is an input that leads to a bug within that bounded number of loop unwindings. With fun C++ metaprogramming, you can actually get this to happen natively (i.e. the parts that aren't reliant on input get run natively) which leads to a massive speedup o I don't believe it to be model checking, although it might use model checking techniques. I could be wrong, I'm only familiar with a few aspects.
wsxcde 13y ago
Model checking deals with two kinds of properties - safety and liveness. Safety properties effectively say nothing bad ever happens while liveness properties say that something good will eventually happen. For example, "my program will never crash due to a null point dereference" is a safety property. "My arbiter module will output a grant for every input request" is a liveness property. It is true that model checkers are much better are proving safety properties than liveness properties. I think it's not too far from the truth to say that model checkers are no good at proving liveness properties in real designs and that only safety properties work (somewhat well) in practice. An alternative here is to abandon model checking altogether and focus on a powerful static analysis. I think the main challenge here is coming up with effective property specification schemes. A powerful type system like Haskell does in fact enable you to prove quite strong statements about your program. But you are inherently limited in terms of what you can prove to whatever it is that the type system can express. To me, it seems that model checkers allow more flexibility in specifying your property, especially when you take into account the fact that you can do your model checking on an augmented/instrumented version of your design. > That's a different problem scale than "prove the whole thing works as specified". On a vaguely related note, equivalence checking between designs, especially in the hardware context, is one thing that formal tools have had a lot of success with.
- lmm 13y ago
  > you are inherently limited in terms of what you can prove to whatever it is that the type system can express Does that actually limit you? E.g. I can imagine using a monad-like structure in Haskell to construct things like "procedure guaranteed to terminate in <k primitive steps".
  - chriswarbo 13y ago
    Well, considering that the article talks about Coq, which is completely built around a type system (plus a termination checker), it's not that limiting.
  - wsxcde 13y ago
    It's not just about whether it is possible in theory though. I'm sure it is, but if it's too complicated, it won't see adoption. The point I was making is that expressibility isn't just important in your programming language, it's important for your verification scheme as well.

gsnedders 13y ago

Sadly, it's not a different problem scale — the typical model is something similar to "for each state, does the property P hold?". Hence no matter the property (or complexity thereof), one must still enumerate all states.

CHY872 13y ago
Of course, one will attempt to also find equivalence classes for the states! The code long x = user_input(); if (x == 0) { violate_model(); } else { do_something(); } you would expect by any reasonable implementation to collapse the system into just two equivalent states that can be tested.
- wsxcde 13y ago
  Ah, but finding equivalence classes of states is quite tricky! Obviously the naive approach of enumerating states and assigning them to equivalence classes is dead on arrival. You might be hinting at examining control flow predicates with your example. This technique is called predicate abstraction and underlies a lot of the SLAM effort. It works in certain scenarios - A statement which more or less captures the state of the field itself.
  - CHY872 13y ago
    What I'm personally hinting at is symbolic/concolic execution. Essentially, each variable has a set of constraints associated with it - initially left blank for an input variable, for example. Then, the program can be executed, with assignments producing new constraints and replacing old ones. At each point in control flow, the executor chooses a path, and adds new constraints. When a dangerous statement (assertion, pointer dereference etc) is reached, the constraints can be solved by z3 or some other SMT solver, and if it can find a satisfying result you automatically have a test case that will produce erroneous or undefined behaviour. It works quite well for short programs, actually - the KLEE people (or maybe it was DART) found bugs in busybox, GNU Coreutils etc. The current approach is to instead of traversing your control flow tree explicitly (which means you're doing a tree search over a potentially infinite tree), converting the program such that it produces a logical statement that can be solved by an SMT solver, that is satisfiable iff there is an input that leads to a bug within that bounded number of loop unwindings. With fun C++ metaprogramming, you can actually get this to happen natively (i.e. the parts that aren't reliant on input get run natively) which leads to a massive speedup o I don't believe it to be model checking, although it might use model checking techniques. I could be wrong, I'm only familiar with a few aspects.

wsxcde 13y ago

Model checking deals with two kinds of properties - safety and liveness. Safety properties effectively say nothing bad ever happens while liveness properties say that something good will eventually happen. For example, "my program will never crash due to a null point dereference" is a safety property. "My arbiter module will output a grant for every input request" is a liveness property. It is true that model checkers are much better are proving safety properties than liveness properties. I think it's not too far from the truth to say that model checkers are no good at proving liveness properties in real designs and that only safety properties work (somewhat well) in practice. An alternative here is to abandon model checking altogether and focus on a powerful static analysis. I think the main challenge here is coming up with effective property specification schemes. A powerful type system like Haskell does in fact enable you to prove quite strong statements about your program. But you are inherently limited in terms of what you can prove to whatever it is that the type system can express. To me, it seems that model checkers allow more flexibility in specifying your property, especially when you take into account the fact that you can do your model checking on an augmented/instrumented version of your design. > That's a different problem scale than "prove the whole thing works as specified". On a vaguely related note, equivalence checking between designs, especially in the hardware context, is one thing that formal tools have had a lot of success with.

lmm 13y ago
> you are inherently limited in terms of what you can prove to whatever it is that the type system can express Does that actually limit you? E.g. I can imagine using a monad-like structure in Haskell to construct things like "procedure guaranteed to terminate in <k primitive steps".
- chriswarbo 13y ago
  Well, considering that the article talks about Coq, which is completely built around a type system (plus a termination checker), it's not that limiting.
- wsxcde 13y ago
  It's not just about whether it is possible in theory though. I'm sure it is, but if it's too complicated, it won't see adoption. The point I was making is that expressibility isn't just important in your programming language, it's important for your verification scheme as well.