Syntactic-Semantic Incrementality for Agile Verification

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.