Invited Speakers

José Meseguer (University of Illinois at Urbana-Champaign, USA)

Towards Extensible Symbolic Formal Methods

The use of decision procedures for theories axiomatizing data structures and functions commonly occurring in software and hardware systems is currently one of the most effective methods at the heart of state-of-the art theorem provers and model checkers. It offers the promise, and often even the reality, of scaling up such verification efforts to handle large systems used in industrial practice. In particular, from the model checking perspective a great advantage of using decision procedures is that we can perform infinite-state model checking. This is because we can define infinite sets of states symbolically as states satisfying certain constraints which are formulas whose satisfiability is decidable by some procedure.

But what other symbolic methods are there? And how extensible are they? And how can they be combined? For example, the above model checking and theorem proving methods based on decidable theories supported by an SMT solver extend to combinations of decidable theories supported by the solver (using, for example, the Nelson-Oppen (NO) combination method), but no further. And there is at the moment no straightforward way to combine the symbolic methods of the SMT solver with other symbolic methods. These questions are not academic, but eminently practical: given a formal verification task, the more extensible our symbolic methods are, the more tasks we can automate, and the more can we scale up to solve harder and bigger problems.

A useful distinction between symbolic methods is that they can be either: (i) theory-specific; or (ii) theory-generic. For example, a decision procedure for inequalities between linear polynomials over the real numbers, or a unification algorithm for associative-commutative symbols, are obviously theory-specific. Although theory-specific procedures can be combined by methods like NO, or similar methods to combine unification algorithms, their extensibility cannot go beyond such combinations, and a given tool will only support a finite number of theory-specific procedures. A key advantage of theory-generic methods is that they extend to infinite classes of theories and typically also to their combinations. Another key advantage is that, since their algorithms are generic, their application to a concrete theory becomes user-definable: a tool user, as opposed to a tool implementer, can easily instantiate the generic algorithm to his/her theory of choice, and there are unlimited possibilities for such choices.

In this talk I will:

1. briefly review folding variant narrowing for theories satisfying the finite variant property (FVP) as a theory-generic symbolic method for finitary unification modulo the given FVP theory;
2. show that folding variant narrowing can be extended under general conditions to a theory-generic SMT solving symbolic method to decide the satisfiability of quantifier-free formulas in the initial algebra of an FVP theory; and
3. show how, the recently propose rewriting modulo SMT symbolic model checking method which, until now, was only possible using theory-specific decision procedures, becomes much more widely applicable and extensible thanks to the theory-generic variant-based SMT-solving method described in (2);
4. if time permits, I will also summarize theory-generic narrowing-based symbolic model checking methods, and how they can be made even more extensible when combined with the methods described in (1)-(3).

Biographical sketch of Jose Meseguer

Jose Meseguer received his Ph.D. in Mathematics from the University of Zaragoza, Spain. He is Professor of Computer Science at the University of Illinois at Urbana-Champaign (UIUC). Prior to moving to UIUC he was a Principal Scientist as the Stanford Research Institute (SRI), after having held postdoctoral positions at the University of California at Berkeley and IBM Research. He was also an Initiator Member of Stanford University's Center for the Study of Language and Information (CSLI).

Meseguer has made fundamental contributions in the frontier between mathematical logic, executable formal specification and verification, declarative programming languages, programming methodology, programming language semantics, concurrency, and security. His work in all these areas, comprising over 350 publications, is very highly cited. His contributions to security include fundamental concepts such as nointerference, browser security verification, new algorithms and verification techniques to defend systems against Denial of Service (DoS) attacks, and new symbolic techniques to analyze cryptographic protocols modulo complex algebraic properties that have been embodied in the Maude-NPA Protocol Analyzer. He is the creator of rewriting logic, a very flexible computational logic to specify concurrent systems. The 2012 rewriting logic bibliography has over 1,000 publications. The Maude rewriting logic language is one of the most advanced and efficient executable formal specification languages worldwide. It supports a wide range of formal analyses, including symbolic simulation, search, model checking, and theorem proving. It is also an advanced declarative concurrent language with sophisticated object-oriented features and powerful module composition and reflective meta-programming capabilities. He, his collaborators, and other researchers have used Maude and its tool environment to build sophisticated systems and tools, and to specify and analyze many systems, including cryptographic protocols, network protocols, web browsers, cyber-physical systems, models of cell biology, executable formal semantics of programming and software modeling languages, formal analyzers for conventional code, theorem provers, and tools for interoperating different formal systems. He has given numerous invited lectures at international scientific meetings and has taught advanced courses on his research at leading American, British, German, Spanish, Italian, and Japanese universities and research centers. He has also served in numerous program committees of international scientific conferences and as editor of various scientific journals.