Home | Search | Help  
Home Page Università di Genova

Seminar Details

Date 16-6-2006
Time 14:00
Room/Location Aula 711-DISI-7°piano
Title Modular Static Analysis and Verification of Java Classes via Abstract Interpretation
Speaker Dott. Francesco Logozzo
Affiliation École Polytechnique
Link http://www.polytechnique.fr/
Abstract In this talk, I will present a static analysis, based on abstract interpretation, for automatic inference of class invariants in Object-Oriented languages. Class invariants are properties of classes valid before and after the execution of any public method of the class. I use this invariants for verifying the absence of runtime errors in Java programs. I will present the underlying theory, the abstract domain, and a demo of Cibai, the tool I have designed and implemented. I will discuss the benefits of my approach which, unlike analogous tools is (1) sound (unlike ESC/Java 2 or Daikon), (2) Does not require interaction with a theorem prover (unlike Jive or Loop), and (3) Does not require user annotations (unlike Jack, Jakarta or Spec# in the C# world).
Back to Seminars