Actions for Verification of Java Programs using Symbolic Execution and Invariant Generation

Email RIS file
Bookmark
Report an Issue

Verification of Java Programs using Symbolic Execution and Invariant Generation

Author
Visser, Willem
Published
2004.
Physical Description
1 electronic document
Additional Creators
Pasareanu, Corina
Online Version

Availability

I Want It
I Want It

Finding items...

Restrictions on Access
Unclassified, Unlimited, Publicly available.
Free-to-read Unrestricted online access
Summary
Software verification is recognized as an important and difficult problem. We present a norel framework, based on symbolic execution, for the automated verification of software. The framework uses annotations in the form of method specifications an3 loop invariants. We present a novel iterative technique that uses invariant strengthening and approximation for discovering these loop invariants automatically. The technique handles different types of data (e.g. boolean and numeric constraints, dynamically allocated structures and arrays) and it allows for checking universally quantified formulas. Our framework is built on top of the Java PathFinder model checking toolset and it was used for the verification of several non-trivial Java programs.
Other Subject(s)
Collection
NASA Technical Reports Server (NTRS) Collection.
Note
Document ID: 20040068136.
11th International Spin Workshop on Model Checking of Software; 1-3 Apr. 2004; Barcelona; Spain.
Terms of Use and Reproduction
No Copyright.
View MARC record | catkey: 15965504