Schedule of the 23nd International Conference on Automated Deduction

August 2 - August 5, 2011
Lecture Room 25 (Sala Wykładowa Wielka Wschodnia)
Instytut Informatyki
Ulica Joliot Curie 15, Wrocław, Poland

Tuesday, August 2

 08:55-09:00 Welcome
   Hans de Nivelle (Conference Chair)
 09:00-10:00 Session 1: Invited Talk (Chair: Andrei Voronkov)
  Proving that systems eventually do something good
   Byron Cook
  10:00-10:30 Coffee Break
 10:30-12:00 Session 2: Verification I (Chair: Maria Paola Bonacina)
 10:30 Heaps and Data Structures: A Challenge for Automated Provers
   Sascha Böhme and Michał Moskal
  11:00 Automated Cyclic Entailment Proofs in Separation Logic
   James Brotherston, Dino Distefano and Rasmus Lerchedahl Petersen
  11:30 An Efficient Decision Procedure for Imperative Tree Data Structures
   Thomas Wies, Marco Muniz and Viktor Kuncak
  12:00-13:30 Lunch
 13:30-15:15 Session 3: Theorem Proving I (Chair: Geoff Sutcliffe)
 13:30 Predicate Completion for Non-Horn Clause Sets
   Matthias Horbach
  14:00 Sine Qua Non for Large Theory Reasoning
   Krystof Hoder and Andrei Voronkov
  14:30 Experimenting with Deduction Modulo
   Guillaume Burel
  15:00 System Description: SPASS-FD
   Matthias Horbach
  15:15-15:45 Coffee Break
 15:45-17:45 Session 4: Rewriting and Termination (Chair: Chris Lynch)
 15:45 A Dependency Pair Framework for Innermost Complexity Analysis of Term Rewrite Systems
   Lars Noschinski, Fabian Emmes and Jürgen Giesl
  16:15 Backward Trace Slicing for Rewriting Logic Theories
   María Alpuente, Demis Ballis, Javier Espert and Daniel Romero
  16:45 On Transfinite Knuth-Bendix Orders
   Laura Kovacs, Georg Moser and Andrei Voronkov
  17:15 CSI - A Confluence Tool
   Harald Zankl, Bertram Felgenhauer and Aart Middeldorp
  17:30 AC Completion with Termination Tools
   Sarah Winkler and Aart Middeldorp
  17:45-18:15 Break (Walk to Oratorium Marianum)
  18:15-21:00 (In Oratorium Marianum) Herbrand Award Ceremony and Reception
 18:15 Presentation of the Herbrand Award to Nachum Dershowitz
   Franz Baader (President of CADE Inc.)
 18:30? Speech by Herbrand Award Winner
   Nachum Dershowitz
  19:30 Reception and Access to University Museum

Wednesday, August 3

 09:00-10:00 Session 5: Invited Talk (Chair: Nikolaj Bjorner)
  Verified Compilers, Verified Static Analyzers, and Certified Decision Procedures
   Xavier Leroy
  10:00-10:30 Coffee Break (with start of CASC at 10.15 in room 119)
 10:30-11:15 Session 6: Higher-Order Theorem Proving (Chair: Gert Smolka)
 10:30 Reducing Higher-Order Theorem Proving to a Sequence of SAT Problems
   Chad E. Brown
  11:00 The Matita Interactive Theorem Prover
   Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen and Enrico Tassi
 11:15-12:00 Session 7: Verification II (Chair: Viktor Kuncak)
  11:15 Stochastic Differential Dynamic Logic for Stochastic Hybrid Programs
   Andre Platzer
  11:45 Static Analysis of Android Programs
   Etienne Payet and Fausto Spoto
  12:00-13:30 Lunch
 13:30-15:30 Session 8: SMT and Applications (Chair: Christoph Weidenbach)
 13:30 Extending Sledgehammer with SMT Solvers
   Jasmin Christian Blanchette, Sascha Böhme and Lawrence C. Paulson
  14:00 Exploiting symmetry in SMT problems
   David Deharbe, Pascal Fontaine, Stephan Merz and Bruno Woltzenlogel Paleo
  14:30 Model Evolution with Equality Modulo Built-in Theories
   Peter Baumgartner and Cesare Tinelli
  15:00 Scala to the Power of Z3: Integrating SMT and Programming
   Ali Sinan Köksal, Viktor Kuncak and Philippe Suter
  15:15 ASASP: Automated Symbolic Analysis of Administrative Policies
   Francesco Alberti, Alessandro Armando and Silvio Ranise
  15:30-16:00 Coffee Break
 16:00-17:30 Session 9: Security (Chair: Christoph Benzmueller)
 16:00 Deciding security for protocols with recursive tests
   Mathilde Arnaud, Veronique Cortier and Stephanie Delaune
  16:30 Dynamic Behavior Matching: A Complexity Analysis and New Approximation Algorithms
   Matthew Fredrikson, Mihai Christodorescu and Somesh Jha
  17:00 Efficient General Unification for XOR with Homomorphism
   Zhiqiang Liu and Christopher Lynch
  17:30-18:00 In Memoriam Bill McCune
  18:00-19:00 Business Meeting
   Franz Baader (President of CADE Inc.)

Thursday, August 4

 09:00-10:00 Session 10: Invited Talk (Chair: Hans de Nivelle)
  Translating between Language and Logic: What Is Easy and What Is Difficult
   Aarne Ranta
  10:00-10:30 Coffee Break
 10:30-11:30 Session 11: Description Logics I (Chair: Renate Schmidt)
 10:30 Unification in the Description Logic EL without the Top Concept
   Franz Baader, Nguyen Thanh Binh, Stefan Borgwardt and Barbara Morawska
  11:00 A Hybrid Method for Probabilistic Satisfiability
   Pavel Klinov and Bijan Parsia
 11:30-12:30 Lunch
 12:30-19:00 Excursion to Ksiaz Castle
 19:30-24.00 Conference Banquet: Barbecue in Botanical Garden

Friday, August 5

 09:00-10:00 Session 12: Invited Talk (Chair: Viorica Sofronie-Stokkermans)
 09:00 The Anatomy of Equinox -- An Extensible Automated Reasoning Tool for First-Order Logic and Beyond
   Koen Claessen
  10:00-10:30 Coffee Break
 10:30-12:00 Session 13: Description Logics II (Chair: Franz Baader)
  10:30 Reasoning in the OWL 2 Full Ontology Language using First-Order Automated Theorem Proving
   Michael Schneider and Geoff Sutcliffe
  11:00 Optimized Query Rewriting in OWL 2 QL
   Alexandros Chortaras, Despoina Trivela and Giorgos Stamou
  11:30 Automated Reasoning in ALCQ via SMT
   Volker Haarslev, Roberto Sebastiani and Michele Vescovi
 12:00-13:30 Lunch
 13:30-15:30 Session 14: Theorem Proving II (Chair: Peter Baumgartner)
 13:30 Blocked Clause Elimination for QBF
   Armin Biere, Florian Lonsing and Martina Seidl
  14:00 Sort it Out with Monotonicity : Translating between Many-Sorted and Unsorted First-Order Logic
   Koen Claessen, Ann Lillieström and Nicholas Smallbone
  14:30 Compression of Propositional Resolution Proofs via Partial Regularization
   Pascal Fontaine, Stephan Merz and Bruno Woltzenlogel Paleo
  15:00 A Connection-Based Characterization of Bi-intuitionistic Validity
   Didier Galmiche and Daniel Mery
  15:30-16:00 Coffee Break
 16:00-17:00 Session 15: Linear Arithmetic (Chair: Aart Middeldorp)
 16:00 Cutting to the Chase: Solving Linear Integer Arithmetic
   Dejan Jovanovic and Leonardo de Moura
 16:30 Solving Systems of Linear Inequalities by Bound Propagation
   Konstantin Korovin and Andrei Voronkov
 17:00-18.00 Session 16: CASC
 17:00 Presentation of CASC results
   Geoff Sutcliffe + Winners
 18.00-18.05 End of Conference
   Hans de Nivelle (Conference Chair)