| IJCAR 2006 | 3rd International Joint Conference on Automated Reasoning Seattle, August 17 - 20, 2006 |
Program
Wednesday, August 16th
Wednesday's program is also available side by side with other meetings.
19:00‑21:00 CAV-ICLP-IJCAR Joint Reception
Location:
Grand Ballroom A/B
Thursday, August 17th
Thursday's program is also available with abstracts or side by side with other meetings.
08:45‑10:00 FLoC Second Opening and Plenary Session
Chair:
Moshe Vardi, Thomas Ball, Wolfram Schulte, Ken McMillan
Location:
Metropolitan A/B
| 08:45 | Introduction and Welcome |
| 09:00 | David Dill
(Stanford University) I Think I Voted: E-voting vs. Democracy [ppt] |
10:00‑10:30 Break
10:30‑12:30 Session 1: Proofs
Chair:
Dieter Hutter
Location:
Metropolitan B
12:30‑14:00 Lunch break
14:00‑16:00 Session 2: Search
Chair:
Deepak Kapur
Location:
Metropolitan B
16:00‑16:30 Break
16:30‑17:30 Invited Talk
Chair:
John Harrison
Location:
Metropolitan B
| 16:30 | Bruno Buchberger
(Research Institute for Symbolic Computation, Johannes Kepler University, Linz, Austria) Mathematical Theory Exploration [pdf] |
Friday, August 18th
Friday's program is also available with abstracts or side by side with other meetings.
09:00‑10:00 Session 3: System Description 1
Chair:
Mark Stickel
Location:
Metropolitan B
10:00‑10:30 Break
10:30‑12:30 Session 4: Higher-Order Logic
Chair:
Michael Kohlhase
Location:
Metropolitan B
12:30‑14:00 Lunch break
14:00‑16:00 Session 5: Proof Theory
Chair:
Matthias Baaz
Location:
Metropolitan B
16:00‑16:30 Break
16:30‑17:30 Invited Talk
Chair:
Ulrich Furbach
Location:
Metropolitan B
| 16:30 | Adnan Darwiche
(University of California, Los Angeles) Searching While Keeping a Trace: The Evolution from Satisfiability to Knowledge Compilation [ppt] |
19:00‑22:30 CAV-IJCAR Joint Cruise/Banquet
Location:
depart Spirit of Seattle from Pier 55
| 19:00 |
CAV-IJCAR Joint Cruise/Banquet Boarding from Pier 55 (walking distance from hotel) |
| 19:30 | CAV-IJCAR Joint Cruise/Banquet |
Saturday, August 19th
Saturday's program is also available with abstracts or side by side with other meetings.
08:45‑09:30 Herbrand Award: Wolfgang Bibel
Chair:
Franz Baader
Location:
Grand Ballroom B
09:30‑10:30 Session 6: System Description 2
Chair:
Bernhard Beckert
Location:
Grand Ballroom B
| 09:30 | Juergen Giesl
, Peter Schneider-Kamp
and Rene Thiemann
AProVE 1.2: Automatic Termination Proofs in the Dependency Pair Framework |
| 09:45 | Boontawee Suntisrivaraporn
, Franz Baader
and Carsten Lutz
CEL---A Practical Reasoner for Life Science Ontologies |
| 10:00 | Dmitry Tsarkov and Ian Horrocks
FaCT++ Description Logic Reasoner: System Description |
| 10:15 | Steven Obua
and Sebastian Skalberg Importing HOL into Isabelle/HOL |
10:30‑11:00 Break
11:00‑12:30 Session 7: Search
Chair:
Chris Lynch
Location:
Willow A
11:00‑12:30 Session 8: Proof Theory
Chair:
Jason Hickey
Location:
Grand Ballroom B
12:30‑14:00 Lunch (in hotel)
Location:
Grand Ballroom D
14:00‑16:00 Session 9: Proof Checking
Chair:
John Harrison
Location:
Willow A
14:00‑16:00 Session 10: Combination
Chair:
Aaron Stump
Location:
Grand Ballroom B
| 14:00 | Erik Reeber
and Warren A. Hunt, Jr.
A SAT-Based Decision Procedure for the Subclass of Unrollable List Formulas in ACL2 (SULFA) |
| 14:30 | Shuvendu Lahiri
and Madanlal Musuvathi Solving Sparse Linear Constraints |
| 15:00 | Olga Grinchtein, Martin Leucker
and Nir Piterman
Inferring Network Invariants Automatically |
| 15:30 | Christian Urban
and Stefan Berghofer
A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL |
16:00‑16:30 Break
16:30‑17:30 Keynote Session
Chair:
Wolfram Schulte, Moshe Vardi
Location:
Grand Ballroom B/C
| 16:30 | David Harel
(Weizmann Institute) Playing with Verification, Planning and Aspects: Unusual Methods for Running Scenario-Based Programs [ppt] |
18:00‑20:00 IJCAR Business Meeting
Location:
Grand Ballroom B
Sunday, August 20th
Sunday's program is also available with abstracts or side by side with other meetings.
09:00‑10:00 Invited Talk
Chair:
Natarajan Shankar
Location:
Grand Ballroom B
| 09:00 | Dale Miller
(INRIA and LIX/Ecole Polytechnique) Representing and Reasoning With Operational Semantics [pdf] |
10:00‑10:30 Break
10:30‑12:30 Session 11: Decision Procedures
Chair:
Maria Paola Bonacina
Location:
Grand Ballroom B
| 10:30 | Maria Paola Bonacina, Silvio Ghilardi
, Enrica Nicolini, Silvio Ranise
and Daniele Zucchelli Decidability and Undecidability Results for Nelson-Oppen and Rewrite-based Decision Procedures |
| 11:00 | Amine Chaieb Verifying mixed real-integer quantifier elimination |
| 11:30 | Stephane Demri
and Denis Lugiez
Presburger Modal Logic is Only PSPACE-complete |
| 12:00 | Florent Jacquemard, Michael Rusinowitch and Laurent Vigneron
Tree automata with equality constraints modulo equational theories |
10:30‑11:30 Session 12: CASC Results
Chair:
Geoff Sutcliffe
Location:
Willow A
12:30‑14:00 Lunch break
14:00‑15:30 Session 13: Description Logic
Chair:
Ian Horrocks
Location:
Grand Ballroom B
| 14:00 | Daniel Dougherty
, Kathi Fisler and Shriram Krishnamurthi Specifying and Reasoning about Dynamic Access-Control Policies |
| 14:30 | David Toman and Grant Weddell On Keys and Functional Dependencies as First-class Citizens in Description Logics |
| 15:00 | Yevgeny Kazakov
and Boris Motik
A Resolution-Based Decision Procedure for SHOIQ |
15:30‑16:00 Break
16:00‑18:00 Session 14: Rewriting
Chair:
Aart Middeldorp
Location:
Grand Ballroom B
