``TRUST but VERIFY''

                             C. R. Ramakrishnan 
                            ( cram@cs.sunysb.edu )
                         
Information about properties of programs and systems are used for a
variety of purposes. Program verification systems which perform
sophisticated analysis to prove or disprove program properties are
being used in the industry for establishing correctness of
mission-critical components.  Advanced compilers use analysis
information to perform aggressive code optimization.  Software testing
tools use data and control flow information to automatically generate
small set of test cases and/or to find potential bugs in programs.
However, program analysis systems are hard to build, maintain and
evolve, since each analysis is typically implemented from scratch, and
extraction of different properties need different analysis techniques
ranging from abstract interpretation (where the program is evaluated
over an abstract domain of properties) to automated theorem proving.

In this talk, I will describe our ongoing work on synthesizing
practical property extractors/verifiers directly from high-level
specifications, using logic as the specification language and logic
programming systems as the implementation tools.  We have thus far
built two successful prototypes, based on Stony Brook's XSB logic
programming system in two major areas: abstract interpretation-based
analyzers for compilation, and model checking-based analyzers for
program verification.  In both cases, the systems based on our
approach are competitive (in space and time) with existing analysis
systems consisting of much larger programs written in lower level
languages.  I will talk about the research problems we are currently
addressing (such as verification of infinite family of systems), as
well as problems we plan to tackle in the near future (such as
verification of mobile programs).