Entries by 'Arie Gurfinkel'

Verifying Evolving Software

No Comments »

By Arie Gurfinkel
Senior Member of the Technical Staff   
Software Solutions Division

Arie GurfinkelWhen we verify a software program, we increase our confidence in its trustworthiness. We can be confident that the program will behave as it should and meet the requirements it was designed to fulfill. Verification is an ongoing process because software continuously undergoes change. While software is being created, developers upgrade and patch it, add new features, and fix known bugs. When software is being compiled, it evolves from program language statements to executable code. Even during runtime, software is transformed by just-in-time compilation. Following every such transformation, we need assurance that the change has not altered program behavior in some unintended way and that important correctness and security properties are preserved. The need to re-verify a program after every change presents a major challenge to practitioners—one that is central to our research. This blog post describes solutions that we are exploring to address that challenge and to raise the level of trust that verification provides.

Read more...

Regression Verification for Real-time Embedded Software Systems

No Comments »

By Arie Gurfinkel
Senior Member of the Technical Staff
Research, Technology, & System Solutions

Arie GurfinkelThe DoD relies heavily on mission- and safety-critical real-time embedded software systems (RTESs), which play a crucial role in controlling systems ranging from airplanes and cars to infusion pumps and microwaves. Since RTESs are often safety-critical, they must undergo an extensive (and often expensive) certification process before deployment. This costly certification process must be repeated after any significant change to the RTES, such as migrating a single-core RTES to a multi-core platform, significant code refactoring, or performance optimizations, to name a few. Our initial approach to reducing re-certification effort—described in a previous blog post—focused on the parts of a system whose behavior was affected by changes using a technique called regression verification, which involves deciding the behavioral equivalence of two, closely related programs. This blog posting describes our latest research in this area, specifically our approach to building regression verification tools and techniques for static analysis of RTESs.

Read more...

Regression Verification of Real-time Embedded Software

No Comments »

By Arie Gurfinkel,
Senior Member of the Technical Staff, Research Technology and System Solutions (RTSS)


Arie GurfinkelContinuous technological improvement is the hallmark of the hardware industry. In an ideal world—one without budgets or schedules—software would be redesigned and redeveloped from scratch to leverage each such improvement. But applying this process for software is often infeasible—if not impossible—due to economic constraints and competition. This posting discusses our research in applying verification, namely regression verification, to help the migration of real-time embedded systems from single-core to multi-core platforms.

Read more...