|
|
|||||||||||||||||||||||||
Current Research
|
Abstract: Error diagnosis, which is the process of
identifying the root causes of bugs in software, is a time-consuming process.
In general, it is hard to automate error diagnosis due to the unavailability
of a full “golden” specification of the system behavior in
realistic software development. We propose a repair-based proof-guided error diagnosis (PED) framework,
that provides a first-line attack to find the root causes of the errors in
programs by pin-pointing the possible error-sites (buggy statements), and
suggesting possible repair fixes. Our framework does not need a complete
system specification. Instead, it automatically “mines” partial
specifications of the intended program behavior from the proofs obtained by
static program analysis for standard safety checkers. It uses these partial
specifications along with the multiple error traces provided by a model
checker to narrow down the possible error sites. It also exploits inherent
correlations among the program statements. To capture common programming
mistakes, it directs the search to those statements that could be buggy due
to simple copy paste operations or syntactic mistakes such as using ≤ instead of <. To further improve debugging, it
prioritizes the repair solutions. We implemented and integrated the PED tool
as a plug-in module to a software verification framework. We show the
efficacy of such a framework on public benchmarks. Follow
the link
for related papers. Model Checking
Concurrent System Abstract: We present an efficient method for modeling multi-threaded
concurrent systems with shared variables and locks in Bounded Model Checking
(BMC), and use it to improve the detection of safety properties such as data
races. Previous approaches based on synchronous modeling of interleaving
semantics do not scale up well due to the inherent asynchronism in those
models. Instead, in our approach, we first create independent (uncoupled)
models for each individual thread in the system, then explicitly add
additional synchronization variables and constraints, incrementally, and only
where such synchronization is needed to guarantee the (chosen) concurrency
semantics (based on sequential consistency). The main novelty of our approach
is that we do not introduce wait-cycles in our symbolic models for the
individual threads, which are typically required for considering an
interleaved execution of the threads. These wait-cycles are detrimental to
the performance of BMC. Furthermore, our lazy modeling approach improves the
effectiveness of other methods to accelerate the performance of BMC, such as
use of control state reachability and property-preserving model
transformations to reduce BMC problem size, and use of static lockset
analysis to reduce number of context switches to be considered. In our lazy
modeling paradigm, we specifically address the scalability of the concurrent
verification by reducing the size of the BMC problem, thereby, improving the
performance of BMC, in both runtime and memory. We have implemented our
techniques in a prototype SMT-based BMC framework, and demonstrate its
effectiveness through controlled experiments on a concurrency benchmark
example. Follow the link
for related papers. SMT-based BMC and
Acceleration Techniques Abstract: SAT-based Bounded Model
Checking (BMC) has been found promising in finding deep bugs in industry
designs and scaling well with design sizes. However, it has limitations due
to requirement of finite data paths, inefficient translations and loss of
high-level design information during the BMC problem formulation. These
shortcomings inherent in Boolean-level BMC can be avoided by using high-level
BMC. We propose a novel framework for high-level BMC, which includes several
techniques that extract high-level design information from EFSM models to
make the verification model “BMC friendly”, and use it on-the-fly
to simplify the BMC problem instances. Such techniques overcome the inherent limitations of Boolean-level
BMC, while allowing integration of state-of-the-art techniques for BMC. We also propose a novel scalable approach
to decompose disjunctively a BMC instance, into simpler and independent
subproblems, based on tunnels i.e., a set of control paths. We simplify each
subproblem using slicing, data path simplification and tunnel specific
control flow constraints, and solve them independently. We implemented such a
tunneling and slicing-based reduction (TSR) approach in
Satisfiability-Modulo-Theory (SMT)-based BMC framework. Such a TSR-based
approach improves the overall performance of BMC when applied to verification
of low-level embedded industry programs. Using TSR decomposition, we present a tool
D-TSR for parallelizing SMT-based BMC over a distributed environment targeted
for checking safety properties in low-level embedded (sequential) software.
We exploit such a decomposition to cut down communication cost and idle time
of CPUs during synchronization while solving BMC instances. Our approach
scales almost linearly with number of CPUs, as demonstrated in our
experimental results. Follow the link for related papers. SMT-solvers
for Non-linear operations Abstract: For the verification of complex designs, one often needs to solve
decision problems containing integer non-linear constraints. Due to the
undecidability of the problem, one usually considers bounded integers and
then either linearizes the problem into a SMT(LIA) problem (i.e., the theory of linear integer arithmetic with
Boolean constraints) or bit-blasts into a SAT problem. We present a novel way
of linearizing those constraints, and then show how the proposed encoding to
a SMT(LIA) problem can be
integrated into an incremental lazy bounding and refinement procedure (LBR)
that leverages on the success of the state-of-the-art SMT(LIA) solvers. The most
important feature of our LBR procedure is that the formula need not be
re-encoded at every step of the procedure but rather, only bounds on
variables need to be asserted/retracted, which are very efficiently supported
by the recent SMT(LIA)
solvers. In a series of controlled experiments, we show the effectiveness of
our linearization encoding and LBR procedure in reducing the SMT solve time.
We observe similar effectiveness of LBR procedure when used in a software
verification framework applied on industry benchmarks. Follow the link for related papers. Verification
Methodology: Synthesis for Verification Abstract: Design-For-Verification
(DFV) methodology i.e., exporting designer’s intent to verification
tools has been quite effective in improving verification efforts, but
requires designers’ reliable insights. We take one step further in
improving the verification efforts, by separating the design optimized for
performance, area and power from the design optimized for correctness,
thereby reducing the verification burden. We propose a new paradigm
Synthesis-For-Verification (SFV) which involves automatic synthesis of
“verification-aware” designs that are more suitable for
functional verification. SFV methodology should be applied along with DFV
methodology to obtain the full benefit of verification efforts. Follow the link
for related papers. VeriSol (formerly known as DiVer): SAT-based Model Checking
Platform for Verifying Large Scale Systems Abstract: Verifying
modern designs requires robust and scalable approaches in order to meet more-demanding
time-to-market requirements. Compared to symbolic model checking based on
Binary Decision Diagrams, SAT-based model checking techniques have been able
to scale and perform well due to the many recent advances in DPLL-style SAT
solvers. We have built a SAT-based model checking platform, VeriSol based on robust and scalable
algorithms that are tightly integrated for verifying large scale industry
designs. VeriSol has matured over 4
years and is being used extensively by the designers in our company. VeriSol
is commercially available as C-based Property Checker in NEC’s Cyber
Work Bench, C-based design environment. Following
book provides an insight of the tool and references to various algorithms
used. Malay K. Ganai and Aarti Gupta. SAT-based Scalable Formal
Verification Solutions. Springer. 2007 (Book) Follow
the link
for related papers. |
||||||||||||||||||||||||
|
NEC Laboratories America, Inc. |
|
||||||||||||||||||||||||
