Date: Sun, 11 Feb 2001 19:31:34 -0800 (PST)
From: Westley Weimer <weimer@EECS.Berkeley.EDU>
Subject: Model Checking & Theorem Proving
Message-ID: <Pine.SOL.4.30.0102111925400.4173-100000@york.CS.Berkeley.EDU>
Is this Tomás Uribe the same person who came and spoke last semester (you
must forgive my appaling memory for names) about combining PVS and model
checking? His webpage lists his research interests as "formal methods,
temporal verification of reactive systems, automated deduction
(theorem-proving), model checking, constraints." While "constraints" is
hardly the same as "program analysis", he would seem to cover a lot of our
interests.
- Wes
---------- Forwarded message ----------
SRI AI SEMINAR SERIES
on Wednesday, 7 February 2001, 2:00pm - 3:00pm
EJ228, SRI International
http://www.ai.sri.com/ai-seminars/
Combinations of Model Checking and Theorem Proving
Tomas E. Uribe
Stanford University
http://theory.stanford.edu/~uribe/
The two main approaches to the formal verification of reactive systems
are based, respectively, on model checking (algorithmic verification)
and theorem proving (deductive verification).
These two approaches have complementary strengths and weaknesses, and
their combination promises to enhance the capabilities of each. This
talk surveys a number of methods for doing so. As is often the case,
the combinations can be classified according to how tightly the
different components are integrated, their range of application, and
their degree of automation.
This archive was generated by hypermail 2b30 : 11/04/02 PST