scholarly journals Configurable Software Verification: Concretizing the Convergence of Model Checking and Program Analysis

2007 ◽  
pp. 504-518 ◽  
Author(s):  
Dirk Beyer ◽  
Thomas A. Henzinger ◽  
Grégory Théoduloz
Keyword(s):  
Model Checking ◽  
Program Analysis ◽  
Software Verification ◽  
Configurable Software

scholarly journals A Theory of Arrays with set and copy Operations

10.29007/q58t ◽  
2018 ◽  
Author(s):  
Stephan Falke ◽  
Carsten Sinz ◽  
Florian Merz
Keyword(s):  
Model Checking ◽  
Program Analysis ◽  
Software Verification ◽  
Symbolic Execution ◽  
Bounded Model Checking ◽  
Main Memory ◽  
Basic Theory ◽  
Analysis Software

The theory of arrays is widely used in order to model main memory in program analysis, software verification, bounded model checking, symbolic execution, etc. Nonetheless, the basic theory as introduced by McCarthy is not expressive enough for important practical cases since it only supports array updates at single locations. In programs, the memory is often modified using functions such as memset or memcpy/memmove, which modify a user-specified range of locations whose size might not be known statically. In this paper we present an extension of the theory of arrays with set and copy operations which make it possible to reason about such functions. We also discuss further applications of the theory.

Bounded Verification of Multi-threaded Programs via Lazy Sequentialization

2022 ◽  
Vol 44 (1) ◽  
pp. 1-50
Author(s):  
Omar Inverso ◽  
Ermenegildo Tomasco ◽  
Bernd Fischer ◽  
Salvatore La Torre ◽  
Gennaro Parlato
Keyword(s):  
Program Analysis ◽  
High Performance ◽  
Software Verification ◽  
Bounded Model Checking ◽  
New Approach ◽  
C Programming Language ◽  
C Programming ◽  
Verification Problem ◽  
Practical Program ◽  
Verification Techniques

Bounded verification techniques such as bounded model checking (BMC) have successfully been used for many practical program analysis problems, but concurrency still poses a challenge. Here, we describe a new approach to BMC of sequentially consistent imperative programs that use POSIX threads. We first translate the multi-threaded program into a nondeterministic sequential program that preserves reachability for all round-robin schedules with a given bound on the number of rounds. We then reuse existing high-performance BMC tools as backends for the sequential verification problem. Our translation is carefully designed to introduce very small memory overheads and very few sources of nondeterminism, so it produces tight SAT/SMT formulae, and is thus very effective in practice: Our Lazy-CSeq tool implementing this translation for the C programming language won several gold and silver medals in the concurrency category of the Software Verification Competitions (SV-COMP) 2014–2021 and was able to find errors in programs where all other techniques (including testing) failed. In this article, we give a detailed description of our translation and prove its correctness, sketch its implementation using the CSeq framework, and report on a detailed evaluation and comparison of our approach.

Chapter 20. Software Verification

2021 ◽  
Author(s):  
Daniel Kroening
Keyword(s):  
Program Analysis ◽  
Software Verification ◽  
Embedded Software ◽  
Propositional Satisfiability ◽  
Low Level

This chapter covers an application of propositional satisfiability to program analysis. We focus on the discovery of programming flaws in low-level programs, such as embedded software. The loops in the program are unwound together with a property to form a formula, which is then converted into CNF. The method supports low-level programming constructs such as bit-wise operators or pointer arithmetic.

scholarly journals A Latent Implementation Error Detection Method for Software Validation

2013 ◽  
Vol 2013 ◽  
pp. 1-10
Author(s):  
Jiantao Zhou ◽  
Jing Liu ◽  
Jinzhao Wu ◽  
Guodong Zhong
Keyword(s):  
Model Checking ◽  
Error Detection ◽  
Software Verification ◽  
Conformance Testing ◽  
Software Validation ◽  
Software Model Checking ◽  
Software Model ◽  
Novel Approach ◽  
Tightly Coupled ◽  
Security Properties

Model checking and conformance testing play an important role in software system design and implementation. From the view of integrating model checking and conformance testing into a tightly coupled validation approach, this paper presents a novel approach to detect latent errors in software implementation. The latent errors can be classified into two kinds, one is called as Unnecessary Implementation Trace, and the other is called as Neglected Implementation Trace. The method complements the incompleteness of security properties for software model checking. More accurate models are characterized to leverage the effectiveness of the model-based software verification and testing combined method.

scholarly journals Transformation-Enabled Precondition Inference

2021 ◽  
pp. 1-17
Author(s):  
BISHOKSAN KAFLE ◽  
GRAEME GANGE ◽  
PETER J. STUCKEY ◽  
PETER SCHACHTE ◽  
HARALD SØNDERGAARD
Keyword(s):  
Iterative Method ◽  
Program Analysis ◽  
Experimental Evaluation ◽  
Software Verification ◽  
Termination Criteria ◽  
Initial States

Abstract Precondition inference is a non-trivial problem with important applications in program analysis and verification. We present a novel iterative method for automatically deriving preconditions for the safety and unsafety of programs. Each iteration maintains over-approximations of the set of safe and unsafe initial states, which are used to partition the program’s initial states into those known to be safe, known to be unsafe and unknown. We then construct revised programs with those unknown initial states and iterate the procedure until the approximations are disjoint or some termination criteria are met. An experimental evaluation of the method on a set of software verification benchmarks shows that it can infer precise preconditions (sometimes optimal) that are not possible using previous methods.

A Fresh Look at Zones and Octagons

2021 ◽  
Vol 43 (3) ◽  
pp. 1-51
Author(s):  
Graeme Gange ◽  
Zequn Ma ◽  
Jorge A. Navas ◽  
Peter Schachte ◽  
Harald Søndergaard ◽  
...  
Keyword(s):  
Data Structures ◽  
Program Analysis ◽  
Software Verification ◽  
State Of The Art ◽  
The State ◽  
Bound Constraints ◽  
Data Structures And Algorithms ◽  
Alternative Approaches ◽  
Abstract Domains ◽  
Automated Discovery

Zones and Octagons are popular abstract domains for static program analysis. They enable the automated discovery of simple numerical relations that hold between pairs of program variables. Both domains are well understood mathematically but the detailed implementation of static analyses based on these domains poses many interesting algorithmic challenges. In this article, we study the two abstract domains, their implementation and use. Utilizing improved data structures and algorithms for the manipulation of graphs that represent difference-bound constraints, we present fast implementations of both abstract domains, built around a common infrastructure. We compare the performance of these implementations against alternative approaches offering the same precision. We quantify the differences in performance by measuring their speed and precision on standard benchmarks. We also assess, in the context of software verification, the extent to which the improved precision translates to better verification outcomes. Experiments demonstrate that our new implementations improve the state of the art for both Zones and Octagons significantly.

Sign in / Sign up

Export Citation Format

Share Document