| 1. |
- Aarts, Fides, et al.
(författare)
-
Generating models of infinite-state communication protocols using regular inference with abstraction
- 2015
-
Ingår i: Formal methods in system design. - : Springer Science and Business Media LLC. - 0925-9856 .- 1572-8102. ; 46:1, s. 1-41
-
Tidskriftsartikel (refereegranskat)abstract
- In order to facilitate model-based verification and validation, effort is underway to develop techniques for generating models of communication system components from observations of their external behavior. Most previous such work has employed regular inference techniques which generate modest-size finite-state models. They typically suppress parameters of messages, although these have a significant impact on control flow in many communication protocols. We present a framework, which adapts regular inference to include data parameters in messages and states for generating components with large or infinite message alphabets. A main idea is to adapt the framework of predicate abstraction, successfully used in formal verification. Since we are in a black-box setting, the abstraction must be supplied externally, using information about how the component manages data parameters. We have implemented our techniques by connecting the LearnLib tool for regular inference with an implementation of session initiation protocol (SIP) in ns-2 and an implementation of transmission control protocol (TCP) in Windows 8, and generated models of SIP and TCP components.
|
|
| 2. |
|
|
| 3. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Budget-bounded model-checking pushdown systems
- 2014
-
Ingår i: Formal methods in system design. - : Springer Science and Business Media LLC. - 0925-9856 .- 1572-8102. ; 45:2, s. 273-301
-
Tidskriftsartikel (refereegranskat)abstract
- We address the verification problem for concurrent programs modeled as multi-pushdown systems (MPDS). In general, MPDS are Turing powerful and hence come along with undecidability of all basic decision problems. Because of this, several subclasses of MPDS have been proposed and studied in the literature (Atig et al. in LNCS, Springer, Berlin, 2005; La Torre et al. in LICS, IEEE, 2007; Lange and Lei in Inf Didact 8, 2009; Qadeer and Rehof in TACAS, LNCS, Springer, Berlin, 2005). In this paper, we propose the class of bounded-budget MPDS, which are restricted in the sense that each stack can perform an unbounded number of context switches only if its depth is below a given bound, and a bounded number of context switches otherwise. We show that the reachability problem for this subclass is Pspace-complete and that LTL-model-checking is Exptime-complete. Furthermore, we propose a code-to-code translation that inputs a concurrent program and produces a sequential program such that running under the budget-bounded restriction yields the same set of reachable states as running . Moreover, detecting (fair) non-terminating executions in can be reduced to LTL-Model-Checking of . By leveraging standard sequential analysis tools, we have implemented a prototype tool and applied it on a set of benchmarks, showing the feasibility of our translation.
|
|
| 4. |
|
|
| 5. |
|
|
| 6. |
- Ahrendt, Wolfgang, 1967, et al.
(författare)
-
Verifying data- and control-oriented properties combining static and runtime verification: theory and tools
- 2017
-
Ingår i: Formal Methods in System Design. - : Springer Science and Business Media LLC. - 0925-9856 .- 1572-8102. ; 51:1, s. 200-265
-
Tidskriftsartikel (refereegranskat)abstract
- Static verification techniques are used to analyse and prove properties about programs before they are executed. Many of these techniques work directly on the source code and are used to verify data-oriented properties over all possible executions. The analysis is necessarily an over-approximation as the real executions of the program are not available at analysis time. In contrast, runtime verification techniques have been extensively used for control-oriented properties, analysing the current execution path of the program in a fully automatic manner. In this article, we present a novel approach in which data-oriented and control-oriented properties may be stated in a single formalism amenable to both static and dynamic verification techniques. The specification language we present to achieve this that of ppDATEs, which enhances the control-oriented property language of DATEs, with data-oriented pre/postconditions. For runtime verification of ppDATE specifications, the language is translated into a DATE. We give a formal semantics to ppDATEs, which we use to prove the correctness of our translation from ppDATEs to DATEs. We show how ppDATE specifications can be analysed using a combination of the deductive theorem prover KeY and the runtime verification tool LARVA. Verification is performed in two steps: KeY first partially proves the data-oriented part of the specification, simplifying the specification which is then passed on to LARVA to check at runtime for the remaining parts of the specification including the control-oriented aspects. We show the applicability of our approach on two case studies.
|
|
| 7. |
- Backeman, Peter, et al.
(författare)
-
Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic
- 2021
-
Ingår i: Formal methods in system design. - : SPRINGER. - 0925-9856 .- 1572-8102. ; 57:2, s. 121-156
-
Tidskriftsartikel (refereegranskat)abstract
- The inference of program invariants over machine arithmetic, commonly called bit-vector arithmetic, is an important problem in verification. Techniques that have been successful for unbounded arithmetic, in particular Craig interpolation, have turned out to be difficult to generalise to machine arithmetic: existing bit-vector interpolation approaches are based either on eager translation from bit-vectors to unbounded arithmetic, resulting in complicated constraints that are hard to solve and interpolate, or on bit-blasting to propositional logic, in the process losing all arithmetic structure. We present a new approach to bit-vector interpolation, as well as bit-vector quantifier elimination (QE), that works by lazy translation of bit-vector constraints to unbounded arithmetic. Laziness enables us to fully utilise the information available during proof search (implied by decisions and propagation) in the encoding, and this way produce constraints that can be handled relatively easily by existing interpolation and QE procedures for Presburger arithmetic. The lazy encoding is complemented with a set of native proof rules for bit-vector equations and non-linear (polynomial) constraints, this way minimising the number of cases a solver has to consider. We also incorporate a method for handling concatenations and extractions of bit-vector efficiently.
|
|
| 8. |
- Chakraborty, S., et al.
(författare)
-
Symbolic trajectory evaluation for word-level verification: theory and implementation
- 2017
-
Ingår i: Formal Methods in System Design. - : Springer Science and Business Media LLC. - 1572-8102 .- 0925-9856. ; 50:2-3, s. 317-352
-
Tidskriftsartikel (refereegranskat)abstract
- Symbolic trajectory evaluation (STE) is a model checking technique that has been successfully used to verify many industrial designs. Existing implementations of STE reason at the level of bits, allowing signals in a circuit to take values from a lattice comprised of three elements: 0, 1, and X. This limits the amount of abstraction that can be achieved, and presents limitations to scaling STE to even larger designs. The main contribution of this paper is to show how much more abstract lattices can be derived automatically from register-transfer level descriptions, and how a model checker for the general theory of STE instantiated with such abstract lattices can be implemented in practice. We discuss several implementation issues, including how word-level circuits can be symbolically simulated using a new encoding for words that allows representing X values of sub-words succinctly. This gives us the first practical word-level STE engine, called STEWord. Experiments on a set of designs similar to those used in industry show that STEWord scales better than bit-level STE, as well as word-level bounded model checking.
|
|
| 9. |
- Cook, Byron, et al.
(författare)
-
Ranking function synthesis for bit-vector relations
- 2013
-
Ingår i: Formal methods in system design. - : Springer Science and Business Media LLC. - 0925-9856 .- 1572-8102. ; 43:1, s. 93-120
-
Tidskriftsartikel (refereegranskat)abstract
- Ranking function synthesis is a key component of modern termination provers for imperative programs. While it is well-known how to generate linear ranking functions for relations over (mathematical) integers or rationals, efficient synthesis of ranking functions for machine-level integers (bit-vectors) is an open problem. This is particularly relevant for the verification of low-level code. We propose several novel algorithms to generate ranking functions for relations over machine integers: a complete method based on a reduction to Presburger arithmetic, and a template-matching approach for predefined classes of ranking functions based on reduction to SAT- and QBF-solving. The utility of our algorithms is demonstrated on examples drawn from Windows device drivers.
|
|
| 10. |
- Donaldson, Alastair F., et al.
(författare)
-
Automatic analysis of DMA races using model checking and k-induction
- 2011
-
Ingår i: Formal methods in system design. - : Springer Science and Business Media LLC. - 0925-9856 .- 1572-8102. ; 39:1, s. 83-113
-
Tidskriftsartikel (refereegranskat)abstract
- Modern multicore processors, such as the Cell Broadband Engine, achieve high performance by equipping accelerator cores with small "scratch-pad" memories. The price for increased performance is higher programming complexity - the programmer must manually orchestrate data movement using direct memory access (DMA) operations. Programming using asynchronous DMA operations is error-prone, and DMA races can lead to nondeterministic bugs which are hard to reproduce and fix. We present a method for DMA race analysis in C programs. Our method works by automatically instrumenting a program with assertions modeling the semantics of a memory flow controller. The instrumented program can then be analyzed using state-of-the-art software model checkers. We show that bounded model checking is effective for detecting DMA races in buggy programs. To enable automatic verification of the correctness of instrumented programs, we present a new formulation of k-induction geared towards software, as a proof rule operating on loops. Our techniques are implemented as a tool, Scratch, which we apply to a large set of programs supplied with the IBM Cell SDK, in which we discover a previously unknown bug. Our experimental results indicate that our k-induction method performs extremely well on this problem class. To our knowledge, this marks both the first application of k-induction to software verification, and the first example of software model checking in the context of heterogeneous multicore processors.
|
|
