Semi-automatic verification of SequenceL programs

Dr. Nelson Rushton

What if a programmer could verify programs using the same language and interface used to write code? While developing SequenceL, we happily noticed it has distinctive features which allow this to be done. Specifically,

  1. Function definitions are inherently easier to verify than procedural programs (compare, say, induction on integers with Hoare's triples).
  2. Assertions about SequenceL programs are themselves Boolean terms in SequenceL.

As a result of these observations, we are developing a verification logic, in which the proof of an assertion consists of interactively tracing its evaluation to 'true', using the same method as tracing a function call. The solitary (though substantial) difference between proof and tracing is that the proof process is nondeterminstic: the programmer must choose subexpressions to evaluate, and reduction rules to apply at each step (ideally from a menu). Once chosen, proof steps can be checked automatically as they are carried out by the development environment.

This talk will explain and demonstrate the methods we are developing, and compare them with related work such as PVS.

Nelson Rushton received his Ph.D. in Mathematics from the University of Georgia in 1997, and a masters degree in artificial intelligence from the University of Georgia in 2002, Since 2002 he has served as an assistant professor of computer science at Texas Tech University. His major research interests are knowledge representation, artificial intelligence, and computer language design. He has developed intelligent systems for prediction and control under funding from NASA, the Office of Naval Research, and the U.S. Forest service.