**Are you an EPFL student looking for a semester project?**

Work with us on data science and visualisation projects, and deploy your project as an app on top of GraphSearch.

Concept# Model checking

Summary

In computer science, model checking or property checking is a method for checking whether a finite-state model of a system meets a given specification (also known as correctness). This is typically associated with hardware or software systems, where the specification contains liveness requirements (such as avoidance of livelock) as well as safety requirements (such as avoidance of states representing a system crash).
In order to solve such a problem algorithmically, both the model of the system and its specification are formulated in some precise mathematical language. To this end, the problem is formulated as a task in logic, namely to check whether a structure satisfies a given logical formula. This general concept applies to many kinds of logic and many kinds of structures. A simple model-checking problem consists of verifying whether a formula in the propositional logic is satisfied by a given structure.
Overview
Property checking is used for verification when two des

Official source

This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.

Related publications

Loading

Related people

Loading

Related units

Loading

Related concepts

Loading

Related courses

Loading

Related lectures

Loading

Related people (7)

Related publications (45)

Loading

Loading

Loading

Related units (4)

Related concepts (27)

In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal sp

In logic, linear temporal logic or linear-time temporal logic (LTL) is a modal temporal logic with modalities referring to time. In LTL, one can encode formulae about the future of paths, e.g., a con

In logic, temporal logic is any system of rules and symbolism for representing, and reasoning about, propositions qualified in terms of time (for example, "I am always hungry", "I will eventually be h

Related lectures (13)

Related courses (7)

CS-550: Formal verification

We introduce formal verification as an approach for developing highly reliable systems. Formal verification finds proofs that computer systems work under all relevant scenarios. We will learn how to use formal verification tools and explain the theory and the practice behind them.

MATH-341: Linear models

Regression modelling is a fundamental tool of statistics, because it describes how the law of a random variable of interest may depend on other variables. This course aims to familiarize students with linear models and some of their extensions, which lie at the basis of more general regression model

MATH-710: Data Analysis for Science and Engineering

An overview course intended for scientists and engineers who need to use statistical methods as part of their research, who have already attended a course at the second-year EPFL undergraduate level, and need revision and deepening of their knowledge at a more conceptual level.

Liveness temporal properties state that something

2007`good'' eventually happens, e.g., every request is eventually granted. In Linear Temporal Logic (LTL), there is no a priori bound on the `

wait time'' for an eventually to be fulfilled. That is, $F\theta$ asserts that $\theta$ holds eventually, but there is no bound on the time when $\theta$ will hold. This is troubling, as designers tend to interpret an eventuality $\F\theta$ as an abstraction of a bounded eventuality $F^{\leq k}\theta$, for an unknown $k$, and satisfaction of a liveness property is often not acceptable unless we can bound its wait time. We introduce here \pltl, an extension of LTL with the \emph{prompt-eventually} operator $\bF$. A system $S$ satisfies a \pltl formula $\varphi$ if there is some bound $k$ on the wait time for all prompt-eventually subformulas of $\varphi$ in all computations of $S$. We study various problems related to \pltl, including realizability, model checking, and assume-guarantee model checking, and show that they can be solved by techniques that are quite close to the standard techniques for LTL.In automatic software verification, we have observed a theoretical convergence of model checking and program analysis. In practice, however, model checkers, on one hand, are still mostly concerned with precision, e.g., the removal of spurious counterexamples. Lattice-based program analyzers, on the other hand, are primarily concerned with efficiency. To achieve their respective goal, the former builds and refine reachability tress while the latter annotates location with abstract states and rely on overapproximation to accelerate convergence. In this thesis we focus on capturing within a framework existing approaches as well as new solutions with the objective of enabling a better understanding of the fundamental similarities and differences between approaches and with a strong accent on implementability. In a first step, we designed and implemented a framework and a corresponding algorithm for software verification called configurable program analysis. The algorithm can be configured to perform not only a purely tree-based or a purely lattice-based analysis, but offers many intermediate settings that have not been evaluated before. An instance of an analysis in the framework consists of one or more program analyses, such as a predicate abstraction or a shape analysis, and their execution and interaction is controlled using several parameters of our generic verification algorithm. Our experiments consider different configurations of combinations of symbolic analyses. By varying the value of parameters we were able to explore a continuous precision-efficiency spectrum and we showed that it can lead to dramatic improvements in efficiency. In a second step, we improved our framework and algorithm to enable the program analysis to dynamically (on-line) adjust its precision depending on the accumulated results. The framework of configurable program analysis offers flexible, but static, composition of program analyses. Our extension enables composite analyses to adjust the precision of each of their component analyses independently and dynamically. To illustrate, we can allow the explicit tracking of the values of a variable to be switched off in favor of a predicate abstraction when and where the number of different variable values that have been encountered has exceeded a specified threshold. We evaluated the dynamic precision adjustment mechanism by considering combinations of symbolic and explicit analyses. We analyzed code taken from an SSH client/server software as well as hand-crafted examples. We showed that the new approach offers significant gains compared with a purely symbolic, predicate-abstraction-based approach. In a third step, we consider the problem of refinement in addition to the dynamic adjustment of the precision. In contrast to precision adjustment, refinement only increases the precision of the analysis. Moreover, when a refinement occurs, states with a lower precision are discarded and replaced by states with a higher precision. Based on our framework, we present a novel refinement approach for shape analysis, a promising technique to prove program properties about recursive data structures. The challenge is to automatically determine the data-structure type, and to supply the shape analysis with the necessary information about the data structure. We present a stepwise approach to the selection of instrumentation predicates for a TVLA-based shape analysis, which takes us a step closer towards the fully automatic verification of data structure implementations. The approach uses two techniques to guide the refinement of shape abstractions. First, during program exploration, an explicit heap analysis collects sample instances of the heap structures. The samples are used to identify the data structures that are manipulated by the program. Second, during abstraction refinement along an infeasible error path, we consider different possible heap abstractions and choose the coarsest one that eliminates the infeasible path. We were able to successfully verify example programs from a data-structure library that manipulate doubly-linked lists and trees. The techniques presented in this thesis have been implemented as an extension to the BLAST model checker.

In contrast to beta-testing, formal verification can guarantee correctness of a program against a specification. Two basic verification techniques are theorem proving and model checking. Both have strengths and weaknesses. Theorem proving is powerful, but difficult to use for a software engineer. Model checking is fully automatic, but less powerful and hard to extend. This paper shows a possibility, how to combine both approaches, in order to surround the weaknesses. Concretely, we automatize the proof of while loops in the theorem prover KeY, by using the model checker BLAST.

2006