Stack Overflow
Stack Overflow

Questions tagged [model-checking]

Model checking refers to the following problem: Given a model of a system, test automatically whether this model meets a given specification.

Model checking refers to the following problem: Given a model of a system, test automatically whether this model meets a given specification.

Typically, the systems one has in mind are hardware or software systems, and the specification contains safety requirements such as the absence of deadlocks and similar critical states that can cause the system to crash. Model checking is a technique for automatically verifying correctness properties of finite-state systems.

An important class of model checking methods have been developed for checking models of hardware and software designs where the specification is given by a temporal logic formula.

240 questions
25
votes
3 answers

Can Coq be used (easily) as a model checker?

As the title says, can Coq be used as a model checker? Can I mix model checking with Coq proving? Is this usual? Google talks about a "µ-calculus", does anyone have experience with this or something similar? Is it advised to use Coq in this way, or…
Olle Härstedt
  • 3,799
  • 1
  • 24
  • 57
10
votes
1 answer

Relevance of model checking in strongly typed functional programming languages?

I am currently learning about model checking (modal logic, LTL, CTL, SAL model checker, etc.) and in my spare time I am learning about Idris which is a strongly typed functional programming language that supports dependent types. Since I am looking…
Michelrandahl
  • 3,365
  • 2
  • 26
  • 41
7
votes
2 answers

symbolic execution and model-checking

What is the difference between symbolic execution and model checking (for example in model transformation)? I don't understand difference of them. Are they the same?!
any
  • 325
  • 5
  • 17
7
votes
2 answers

LTL, CTL or TLA for modelling for my model (detailed description inside)?

I am currently writing my master thesis and am confronted with specifying and verifying my approach in a temporal logic. Which temporal logic would be the best to use in my circumstances? I would really like some feedback on my approach and how to…
nanoquack
  • 949
  • 2
  • 9
  • 26
6
votes
2 answers

how to show the state space in SPIN

The "Automata View" in iSpin (v. 1.1.4) shows .. exactly what? It seems it is just a graph of the control flow of one process. How would I get the full state space of the system? E.g., in Ben-Ari: Principles of the Spin Model Checker, I want Figure…
d8d0d65b3f7cf42
  • 2,597
  • 15
  • 28
6
votes
5 answers

What is your experience with software model checking?

What types of applications have you used model checking for? What model checking tool did you use? How would you summarize your experience w/ the technique, specifically in evaluating its effectiveness in delivering higher quality software? In…
user290
5
votes
1 answer

Alloy's lone vs one quantifier on river crossing

In the river crossing Alloy model, this predicate: pred crossRiver [from, from', to, to': set Object] { one x: from | { from' = from - x - Farmer - from'.eats to' = to + x + Farmer } } models the river crossing: One of the objects x…
lynaghk
  • 63
  • 3
5
votes
2 answers

SMT/SAT Solver vs Model Checker

Recently, I started to study formal verification techniques. In literature, model checker and solver are used somehow interchangeably. But, how model checker and solver are connected with each other? p.s. I would appreciate if some papers or links…
shahb0z
  • 63
  • 1
  • 7
5
votes
3 answers

Tool for model checking large, distributed C++ projects such as KDE?

Is there a tool which can handle model checking large, real-world, mostly-C++, distributed systems, such as KDE? (KDE is a distributed system in the sense that it uses IPC, although typically all of the processes are on the same machine. Yes, by the…
Robin Green
  • 32,079
  • 16
  • 104
  • 187
5
votes
1 answer

Bypassing an unsigned addition overflow detected by CBMC

CBMC detects a possible unsigned addition overflow in the following lines: l = (t + *b)&(0xffffffffL); c += (l < t); I agree that there is a possibility of an overflow in the first line, but I am taking care of the carry in the next line which CBMC…
AcidBurn
  • 199
  • 1
  • 11
4
votes
2 answers

CUDD: Quantification of ZDDs

I'm working with CUDD (https://github.com/ivmai/cudd) to use bdd and zdd functionality for model checking, and am wondering how i can quantify over zdds. For bdds there are the functions bddExistAbstract and bddUnivAbstract (see…
Daniel Miedema
  • 159
  • 7
4
votes
1 answer

Spin - Formal Verification

Has anyone have contact with model checking with this tool SPIN, even more any information of model checking (concurrent programs)
edgarmtze
  • 24,683
  • 80
  • 235
  • 386
4
votes
1 answer

PROMELA: Would this be an example of a deadlock?

Would this be an example of a deadlock? active proctype test(){ bool one; byte x; one; x = x+11; }
jdoe
  • 65
  • 4
4
votes
1 answer

Is this model of Peterson's algorithm incorrect?

I have written the following model of Peterson's algorithm: bool want[2], turn ltl { []<>P[0]@cs } active [2] proctype P() { pid me = _pid pid you = 1 - me do :: want[me] = true turn = you !want[you] || turn ==…
isekaijin
  • 19,076
  • 18
  • 85
  • 153
4
votes
1 answer

Producing an automaton image of my Promela model

I'm using the SPIN model checker GUI - iSPIN. The GUI comes with a nice Automaton view generator, however in order to see the full automaton I need to zoom in/out. Also I would like to save that automaton in a nice image (avoid using print screen)…
Anton Belev
  • 11,963
  • 22
  • 70
  • 111
1
2 3
…
15 16