| FLoC 2006 | The 2006 Federated Logic Conference Seattle, August 10 - 22, 2006 |
Special Talks
To see the abstract of a talk, click on its title.
Plenary, Keynote and Conference Invited Talks
Saturday, August 12th
| 09:00‑10:00 |
Formal Verification of Infinite State Systems using Boolean Methods [ppt]
Randal E. Bryant (Carnegie Mellon University) |
plenary |
Sunday, August 13th
| 09:00‑10:00 |
Adapting Logics [pdf]
Andreas Blass (University of Michigan, Ann Arbor) |
LICS |
| 09:00‑10:00 |
From Propositional Satisfiability To Satisfiability Modulo Theories [ppt]
Karem Sakallah (University of Michigan, Ann Arbor) |
SAT |
| 09:00‑10:00 |
Rewriting Models of Control-Flow [pdf]
Javier Esparza (Institute for Formal Methods in Computer Science, University of Stuttgart) |
RTA |
Monday, August 14th
| 09:00‑10:00 |
Automated Termination Analysis for Haskell: From Term Rewriting to Programming Languages [pdf]
Jurgen Giesl (RWTH Aachen) |
RTA |
| 09:00‑10:00 |
Avoiding Determinization [ppt]
Orna Kupferman (Hebrew University, Israel) |
LICS |
| 09:00‑10:00 |
CSPs: Adding Structure to SAT [ppt]
Fahiem Bacchus (University of Toronto, Canada) |
SAT |
| 16:30‑17:15 |
Shaken Foundations or Groundbreaking Realignment? A Centennial Assessment of Kurt Gödel's Impact on Logic, Mathematics, and Computer Science [ppt]
John Dawson (Penn State, York Campus) |
keynote |
| 17:15‑18:00 |
The Future of Proof [pdf]
Dana Scott (Carnegie Mellon University) |
keynote |
Tuesday, August 15th
| 09:00‑10:00 |
Provable Implementations of Security Protocols [ppt]
Andy Gordon (Microsoft Research) |
LICS |
Thursday, August 17th
| 09:00‑10:00 |
I Think I Voted: E-voting vs. Democracy [ppt]
David Dill (Stanford University) |
plenary |
| 16:30‑17:30 |
Formal Specifications on Industrial-Strength Code - From Myth to Reality [ppt]
Manuvir Das (Microsoft) |
CAV |
| 16:30‑17:30 |
Mathematical Theory Exploration [pdf]
Bruno Buchberger (Research Institute for Symbolic Computation, Johannes Kepler University, Linz, Austria) |
IJCAR |
Friday, August 18th
| 09:00‑10:00 |
The Ideal of Verified Software [ppt]
Tony Hoare (Microsoft Research) |
CAV |
| 16:30‑17:30 |
Why Use Datalog to Analyze Programs? [ppt]
Monica Lam (Stanford University) |
ICLP |
| 16:30‑17:30 |
Searching While Keeping a Trace: The Evolution from Satisfiability to Knowledge Compilation [ppt]
Adnan Darwiche (University of California, Los Angeles) |
IJCAR |
Saturday, August 19th
| 09:30‑10:30 |
Semantic Web: The story of the RIFt so far
Christopher A. Welty (IBM Watson Research Center) |
ICLP |
| 16:30‑17:30 |
Playing with Verification, Planning and Aspects: Unusual Methods for Running Scenario-Based Programs [ppt]
David Harel (Weizmann Institute) |
keynote |
Sunday, August 20th
| 09:00‑10:00 |
Representing and Reasoning With Operational Semantics [pdf]
Dale Miller (INRIA and LIX/Ecole Polytechnique) |
IJCAR |
| 09:00‑10:00 |
Verification? Getting it Right the First Time [ppt]
Joe Stoy (Bluespec) |
CAV |
Workshop Invited Talks
Thursday, August 10th
| 09:30‑10:30 |
A game semantic approach to infinite structures [pdf]
Luke Ong (Oxford University) |
GALOP |
| 09:45‑10:30 |
Bounded and Unbounded Model Checking using SAT [ppt]
Ed Clarke (Carnegie Mellon University) |
SSPV |
| 11:00‑11:45 |
SAT, interpolants, and software model checking [ppt]
Ken McMillan (Cadence Labs) |
SSPV |
| 11:45‑12:30 |
Efficient SAT-based Techniques for Predicate Abstraction [ppt]
Shuvendu Lahiri (Microsoft Research) |
SSPV |
| 14:00‑14:45 |
Beyond Satisfiability: Model Counting, Quantification, and Randomization [ppt]
Carla Gomes (Cornell University) |
SSPV |
| 14:45‑15:30 |
SAT-based methods for proving properties in Reynolds/O'Hearn Separation Logic [ppt]
Daniel Kroening (ETH Zurich) |
SSPV |
| 16:00‑17:00 |
The Spectrum Problem from a Computer Science Perspective [pdf]
Neil Jones (Department of Computer Science, University of Copenhagen) |
LCC |
| 16:00‑16:45 |
Scalable Program Analysis Using Boolean Satisfiability [pdf]
Alex Aiken (Stanford University) |
SSPV |
Friday, August 11th
Tuesday, August 15th
Wednesday, August 16th
Monday, August 21st
Tuesday, August 22nd
| 09:00‑10:00 |
Program Verification using Probabilistic Techniques [ppt]
Sumit Gulwani (Microsoft Research) |
VSTTE |
| 09:30‑10:30 |
A framework for memory models and its application to X10 [ppt]
Vijay Saraswat (IBM T.J. Watson Research Center) |
TV |
| 14:30‑15:30 |
Multicore Software Development: Encouraging an Industry Transition [pdf]
Paul Petersen (Intel) |
TV |
| 14:30‑15:30 |
Challenges and Lessons for Software Verification [pdf]
Jim Grundy (Intel Strategic Cad Laboratories) |
VSTTE |
Tutorials
Wednesday, August 16th
| 11:00‑11:40 |
Answer Set Programming: Foundations, Implementation Techniques, and Applications [pdf]
Ilka Niemela (Helsinki University of Technology) |
LaSh |
| 11:40‑12:20 |
Experiences in the Research and Development of a Non-Clausal SAT Solver
John Franco (University of Cincinnati) |
LaSh |
Friday, August 18th
| 09:00‑10:00 |
Overcoming performance barriers: efficient verification techniques for logical frameworks [pdf]
Brigitte Pientka (McGill University) |
ICLP |
Monday, August 21st
| 09:00‑09:30 |
Overview of PVS, ICS, and SAL, and plans for the future [pdf]
John Rushby (SRI) |
AFM |
| 09:30‑10:30 |
AR (Action Rules): The Language, Implementation, and Applications [ppt]
Neng-Fa Zhou (City Univerity of New York at Brooklyn College and Graduate Center) |
CICLOPS |
| 09:30‑10:00 |
Recent PVS Language Developments [pdf]
Sam Owre (SRI) |
AFM |
| 10:00‑10:30 |
Recent PVS Prover Developments [pdf]
N. Shankar (SRI) |
AFM |
| 11:00‑11:30 |
Overview of ICS/Yices [pdf]
Leonardo de Moura (SRI) |
AFM |
| 11:30‑12:00 |
Overview of SAL: Model Checking and Test Generation [pdf]
John Rushby (SRI) |
AFM |
| 12:00‑12:30 |
Model Checking Infinite-state Systems in SAL [pdf]
Bruno Dutertre (SRI) |
AFM |
