UTCS Colloquia - Dr. Natarajan Shankar, SRI International Computer Science Laboratory, "Architectures for Logical Inference," ACE 2.302

Contact Name: 
Kevin Hendryx
ACE 2.302
Feb 5, 2013 11:00am - 12:00pm

Signup Schedule: http://apps.cs.utexas.edu/talkschedules/cgi/list_events.cgi

Talk Audience: UTCS Faculty, Grads, Undergrads, Other Interested Parties

Host:  J Strother Moore

Talk Abstract: The automation of logical inference has long been a central activity in modern computing.  Logical inference operates on formulas to produce proofs, models, or normal forms.  Inference algorithms are widely used, particularly in the testing, analysis, and verification of hardware and software systems.  We describe three different architectures for integrating different inference algorithms.  The first architecture, combines solvers for multiple (disjoint) theories into a single solver, which can be integrated with Boolean satisfiability to construct a solver for satisfiability modulo theories.  The second architecture, illustrated by the Prototype Verification System (PVS), combines disparate inference procedures for (fragments of) a single expressive logic within an interactive theorem prover.  The third architecture, realized in the Evidential Tool Bus (ETB), is a distributed framework for integrating inference services. 

The talk is a self-contained overview of the engineering challenges of building inference-based software systems.

Speaker Bio: Dr. Natarajan Shankar is a Staff Scientist at the SRI Computer Science Laboratory where he has been since 1989.  He earned a Ph.D. degree in Computer Science from the University of Texas at Austin in 1986 under the supervision of Robert Boyer and J Strother Moore.  Before joining SRI, he was a research associate at Stanford University where he has also taught at the graduate level.


Dr. Shankar's interests are in the study of formal methods for the specification and verification of hardware and software, in automated deduction, and in computational logic.  In his dissertation, he employed the Boyer-Moore theorem prover to check proofs of various metamathematical theorems, including Goedel's incompleteness theorem and the Church-Rosser theorem.  His book, Metamathematics, Machines, and Goedel's Proof, was published by Cambridge University Press in 1994.  Dr. Shankar has played a leading role in the design and implementation of several widely used verification systems including the Prototype Verification System (PVS), the Symbolic Analysis Laboratory (SAL), the ICS and Yices solvers for satisfiability modulo theories, and the Probabilistic Consistency Engine (PCE) for probabilistic inference.  He also led the Occam project on static previrtualization for creating minimized virtual appliances using partial evaluation.  He is currently developing the evidential tool bus (ETB) framework for combining reasoning tools. Dr. Shankar is past chairman of the IFIP Working Group 2.3 on Programming Methodology and current charman of IFIP Working Group 1.9/2.15 on Verified Software.  He was made an SRI Fellow in 2009, and was a co-winner of the CAV Award in 2012.