Syntactic-semantic incrementality for agile verification

• General framework to define a variety of incremental verification procedures.
• Syntactic-semantic approach based on operator-precedence grammars.
• Incremental verification procedures are encoded as attribute grammars.
• Incremental verification techniques can be integrated within agile methodologies.

Modern software systems are continuously evolving, often because systems requirements change over time. Responding to requirements changes is one of the principles of agile methodologies. In this paper we envision the seamless integration of automated verification techniques within agile methodologies, thanks to the support for incrementality. Incremental verification accommodates the changes that occur within the schedule of frequent releases of software agile processes. We propose a general approach to developing families of verifiers that can support incremental verification for different kinds of artifacts and properties. The proposed syntactic-semantic approach is rooted in operator precedence grammars and their support for incremental parsing. Incremental verification procedures are encoded as attribute grammars, whose incremental evaluation goes hand in hand with incremental parsing.