Conference Report
Software Verification and Validation
(SVV'06)

Abhik Roychoudhury National University of Singapore Singapore	Zijiang Yang Western Michigan University USA
Editor: Enrico Pontelli

The fourth International Workshop on Software verification and Validation was held as an ICLP'06 workshop as part of the Federated Logic Conferences (FLoC) 2006. Since its inception in 2003 as an ICLP workshop, SVV has grown to be a forum for discussing combinations of various software validation methods (automated or manual, formal or informal). This year, we received 12 papers out of which 7 were selected for presentation by the Program Committee.

The workshop was held on August 21. It started with an invited presentation, Automatic Termination Proofs for Systems-level Code, by Byron Cook from Microsoft Research. In the talk Dr. Cook described recent advances in the area of automatic program termination analysis. In particular, he presented the development of several new automatic tools, called TERMINATOR and MUTANT, which implement new termination analysis algorithms.

The first presentation of accepted papers was given by Ganna Zaks from New York University. She presented the paper “Translation Validation of Interprocedural Optimizations”, co-authored with her advisor Amir Pnueli. Translation Validation is an approach of ensuring compilation correctness in which each compiler run is followed by a validation pass that proves that the target code of the program produced by the compiler is a correct translation  of the source code. In their work, they extended the existing framework for translation validation of optimizing compilers to deal with procedural programs and define the notion of correct translation for reactive programs with intermediate inputs and outputs.

The second presentation was given by Dr. Luke Simon from the University of Texas at Dallas. Two of his co-authors, Ajay Mallya and Ajay Bansal, also attended the workshop.  In the talk paper Dr. Simon presented the theory and practice of co-logic programming, a paradigm that combines both inductive and coinductive logic programming. An outline of a prototype implementation realized by modifying YAP Prolog's engine at the WAM level was described.

After the lunch break, Aleks Zaks from New York University presented his paper on Using Range Analysis for Software Verification, co-authored with seven other researchers from NEC, Western Michigan University, and Real Intent. Two of his co-authors, Drs. Ilya Shlyakhter and Zijiang Yang, attended the workshop. The main contributions of their paper are two light-weight range analysis techniques for determining lower and upper bounds for program variables, and their application in improving various software model checking techniques.

Dr.  Elvira Albert  from Complutense University of Madrid presented his paper next on Java Bytecode Verification using Analysis and Transformation of Logic Programs. The aim of their work is to automatically transfer the power of analysis tools for LP to the analysis and verification of Java bytecode. In order to achieve our goal, they rely on well-known techniques for meta- programming and program specialization.

The fifth presentation was given by Stefano Tonetta  from University of Lugano. His co-author, Dr. Natasha Sharygina from UNISI, was present during the presentation. Mr. Tonetta presented a uniform framework for predicate abstraction approximation. The mapping among various abstraction techniques provides a conceptual basis for the development of new algorithms.

After a short coffee break, the last session started at 4pm. Dr. Burkhart Wolff from ETH Zurich presented a package for extensible object-oriented data models with an application to imp++. They implemented a datatype package that enabled the shallow embedding technique to object-oriented specification and programming languages.

The last presentation was given by Mr. Ossami from LORIA. Mr. Ossami and his two coauthors proposed a process model for the development of formal and semi-formal specifications based on the notions of multi-view state and of development operators.

Besides the invited speaker and authors of accepted papers mentioned above, the attendees of SVV include  Dr. Hill from University of Leeds, Dr. Koprowski from Eindhoven University of Technology, Dr. Lukácsy from Budapest University of Technology and Economics, and Dr. Veith from TU Munich. The workshop was adjourned at 5:30pm.