header_image

JML4, An Eclipse-Based Verifying Compiler For Java That Can Prove Your Code Correct!

Dr. Patrice Chalin
Friday, February 22, 2008
10:30AM ~ 12:00PM, Harris Center 104

Abstract


This talk provides a brief glimpse of the history of program verification leading up to Sir Tony Hoare's "Dependable Systems Evolution" Grand Challenge (GC6) for Computer Science and Software Engineering. One of the key components of this Grand Challenge is a Verifying Compiler: a tool that can automatically prove the correctness of code while compiling it. Correctness is defined relative to a specification. Program assertions are the basic building block used to express the contracts (preconditions, postconditions and invariants) used to write program specifications-in a style often referred to as Design by Contract (DBC). Finally we present JML4, is an Eclipse-based Verifying Compiler that understands specifications written in the Java Modeling Language (JML), one of the most popular Behavioral Interface Specification Languages (BISLs).

Short Bio


Dr. Patrice Chalin is Associate Professor and Director of the Software Engineering Undergraduate Program in the Department of Computer Science and Software Engineering of Concordia University, Montreal, Canada. He completed his Ph.D. (1995, Concordia) in the area of language design and semantics of Behavioral Interface Specification Languages. In 1996, Dr. Chalin joined Bell Northern Research (Nortel) working in the areas of telecommunications, network management software and software quality management. Returning to Concordia in 2002, Dr. Chalin founded the Dependable Software Research Group (DSRG) and leads research is several areas of software engineering including requirements specification, model-driven design and forma program verification.

FEEDBACK | Webmaster | EECS | FSI | CECS | UCF
University Of Central Florida | Orlando, Florida 32816-2362 Phone: 407-823-2341