Plenary Lecture
Formal Verification with Programming-Like Tools
Professor Stefan D. Bruda
Bishop's University in Sherbrooke
Quebec, Canada
E-mail: stefan@bruda.ca
Abstract: Computing systems are constructed using programming languages which feature invocations of potentially recursive modules (such as functions or procedures). Many systems are formally verified after they are constructed. At this stage they are considered reactive systems, meaning that their internal structure becomes immaterial and the only feature of interest is their interaction with the environment.
Formal verification is traditionally accomplished by using a finite-state model of the system under test. The inherent recursive nature of the system (given by the programming language used to build it in the first place) is lost. The reason for this simplification is the fact that finite-state models are particularly "nice" mathematical objects, but the consequence of the simplification is that the number of states that need to be explored in the verification process grows quickly, which makes formal verification of complex systems impractical. Increased complexity of computing systems is however a fact of life, and so traditional, finite-state formal methods are slowly reaching their limits.
Those systems under test were however programs at the beginning, and so they are most naturally represented using pushdown models. Such models are however not suitable for formal verification because they lack various closure properties. The quest for a model that combines the expressiveness of pushdown automata and the nice mathematical properties of finite-state automata has started relatively recently. This talk will present this quest. We start with the simple, immediate models to see their shortcomings. We then continue to visibly pushdown formalisms, which are the first full pushdown models. We show however that some practical shortcomings are still present. We finally present our new effort that attempts to eliminate these shortcomings.
Brief Biography of the Speaker: Stefan D. Bruda is Professor of Computer Science with Bishop's University in Sherbrooke, Quebec, Canada. His research resulted in over 50 conference and journal papers and spans at least four major areas (formal languages and automata, formal methods, parallel computation, artificial intelligence). He has been continuously funded by a major federal funding agency (the National Science and Engineering Research Council of Canada) since the start of his professional career. Currently Dr. Bruda's main interest lies in the area of grammatical approaches to parallelism, with applications in context-free formal methods.