Speaker: 

  N. Shankar
  SRI International Computer Science Laboratory

Title: 

  Explaining Decision Procedures

Abstract:

  Decision procedures have a wide variety of applications in theorem
  proving, program and hardware analysis, and constraint solving.  In
  these embedded applications, decision procedures must deliver
  explanations in the form of models, certificates, proofs, and
  unsatisfiable cores.  The embedding and integration of decision
  procedures also requires a flexible interface and a simple
  architecture that can be easily explained.  We present some examples
  of decision procedures, specifically congruence closure and
  simplex-based linear inequality solving, in a form that supports
  straightforward correctness arguments, convenient integration, and
  the generation of useful explanations.  We explore the implications
  of explanations for embedded applications of decision procedures
  such as interactive proof checking and automated verification.
  
  (Joint work with Leonardo de Moura and Harald Ruess.)