Abstract: The specification of programming languages has long benefited from a powerful system, namely the context-free grammar which allows for a natural language specification and is then "compiled" into an automaton that performs the actual parsing. The same pattern (grammars for specification, automata for implementation) is manifest in the realm of formal methods. Here however tools have been essentially limited to a less powerful formalism; indeed, most process algebrae used in practice for specifying computing systems are just another name for regular grammars, which are considerably less expressive than their context-free counterparts. Using regular grammars thus limits the constructs that can be specified; recursion in particular can only be used in very limited forms, which makes the specification of complex software impossible for all practical purposes. Still, the reason regular grammars continue to be the norm in formal methods is that certain language-theoretic properties show that context-free languages are paradoxically less expressive than regular language in the context of system specification, they being able to model recursion alright, but unable to model other common scenarios such as concurrency. Recently, new tools based on context-free grammars have emerged; such a success remains however in the realm of automata, that is, they do not have any convenient associated "specification language." On-going research is currently attempting to start on the grammatical side, with the eventual goal of creating process algebrae that are capable of handling both recursion and concurrency. In turn, such algebrae will permit complete specifications for complex application software, which today are simply too complex to handle. In this talk I will present the effort of going beyond regular grammars in formal methods. I will summarize the automata side and I will also outline the grammatical approaches. We will see that such an effort is rich and interesting (hence the "fun" in the title) and also has tremendous practical applications (hence the "profit"). On the other hand, we will also see that numerous challenges (both theoretical and practical) have yet to be tackled.

Brief Biography of the Speaker:
Dr. Stefan D. Bruda has a successful career as researcher in Computer Science, with over 50 publications so far. His research has spanned at least four major areas (formal languages and automata, formal methods, parallel computation, and artificial intelligence). His main research interest is now formal methods, but he also continues to be interested in formal languages, more precisely in grammatical approaches to parallelism (which will likely be useful in the area of formal methods). Dr. Bruda's research 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. His research has also been funded by provincial agencies and other sources. Dr. Bruda acts as an editor for the Parallel Processing Letters journal. He has been active as a reviewer to several conferences, journals (including Theoretical Computer Science and Parallel Processing Letters), and funding agencies (including NSERC in Canada and the CHIST-ERA Consortium in the European Union). He has been invited two times as plenary speaker to international conferences (but had to decline one). Since December 2011 he is a Senior Member of the Association of Computing Machinery (ACM).