Special section on advances in reachability analysis and decision procedures: contributions to abstraction-based system verification |
| |
Authors: | Michael Huth Orna Grumberg |
| |
Affiliation: | (1) Department of Computing, Imperial College London, South Kensington campus, London, SW7 2AZ, UK;(2) Computer Science Department, TECHNION, Israel Institute of Technology, 32000 Technion City, Haifa, Israel |
| |
Abstract: | Reachability analysis asks whether a system can evolve from legitimate initial states to unsafe states. It is thus a fundamental
tool in the validation of computational systems—be they software, hardware, or a combination thereof. We recall a standard
approach for reachability analysis, which captures the system in a transition system, forms another transition system as an
over-approximation, and performs an incremental fixed-point computation on that over-approximation to determine whether unsafe
states can be reached. We show this method to be sound for proving the absence of errors, and discuss its limitations for
proving the presence of errors, as well as some means of addressing this limitation. We then sketch how program annotations
for data integrity constraints and interface specifications—as in Bertrand Meyer’s paradigm of Design by Contract—can facilitate
the validation of modular programs, e.g., by obtaining more precise verification conditions for software verification supported
by automated theorem proving. Then we recap how the decision problem of satisfiability for formulae of logics with theories—e.g.,
bit-vector arithmetic—can be used to construct an over-approximating transition system for a program. Programs with data types
comprised of bit-vectors of finite width require bespoke decision procedures for satisfiability. Finite-width data types challenge
the reduction of that decision problem to one that off-the-shelf tools can solve effectively, e.g., SAT solvers for propositional
logic. In that context, we recall the Tseitin encoding which converts formulae from that logic into conjunctive normal form—the
standard format for most SAT solvers—with only linear blow-up in the size of the formula, but linear increase in the number
of variables. Finally, we discuss the contributions that the three papers in this special section make in the areas that we
sketched above. |
| |
Keywords: | Bounded reachability Abstraction Memory models Asynchronous systems Decision diagrams Decision problems Bit-vector arithmetic |
本文献已被 SpringerLink 等数据库收录! |
|