IJCAR PROGRAM
Days: Saturday, July 14th Sunday, July 15th Monday, July 16th Tuesday, July 17th
Saturday, July 14th
View this program: with abstractssession overviewtalk overviewside by side with other conferences
09:00-10:30 Session 93A: FLoC Keynote Lecture: Georges Gonthier
Chair:
Location: Maths LT1
| 09:00 | The Logic of Real Proofs (abstract) |
10:30-11:00Coffee Break
11:00-12:30 Session 95F: SMT 1
Chair:
Location: Maths LT2
| 11:00 | Efficient Interpolation for the Theory of Arrays (abstract)  |
| 11:30 | Implicit Hitting Set Algorithms for Maximum Satisfiability Modulo Theories (abstract) |
| 12:00 | A Generic Framework for Implicate Generation Modulo Theories (abstract) |
12:30-14:00Lunch Break
14:00-15:30 Session 96E: SAT Extensions & Applications
Chair:
Location: Maths LT2
| 14:00 | An Assumption-Based Approach for Solving The Minimal S5-Satisfiability Problem (abstract) |
| 14:30 | Investigating the Existence of Large Sets of Idempotent Quasigroups via Satisfiability Testing (abstract) |
| 15:00 | A New Probabilistic Algorithm for Approximate Model Counting (abstract) |
15:30-16:00Coffee Break
16:00-17:00 Session 99F: Tools and Rewriting
Chair:
Location: Maths LT2
| 16:00 | A Coinductive Approach to Proving Reachability in Logically Constrained Term Rewriting Systems (abstract) |
| 16:30 | FAME: An Automated Tool for Semantic Forgetting in Expressive Description Logics (abstract) |
| 16:45 | Efficient Model Construction for Horn Logic with VLog: System Description (abstract) |
17:00-18:00 Session 100B: Awards
- Presentation of the IJCAR 2018 Best Paper Award
- Presentation of the 2018 Woodie Bledsoe Student Travel Awards
- Presentation of the Herbrand Award for Distinguished Contributions to Automated Reasoning to Bruno Buchberger
- Presentation by the awardee: Automated Mathematical Invention: Would Gröbner Need a PhD Student Today?
Chair:
Location: Maths LT2
19:00-21:30 FLoC reception at Oxford Town Hall
FLoC reception at Oxford Town Hall. Drinks and canapés available from 7pm (pre-booking via FLoC registration system required; guests welcome).
Location: Oxford Town Hall
Sunday, July 15th
View this program: with abstractssession overviewtalk overviewside by side with other conferences
09:00-10:30 Session 101D: Logics and Calculi
Chair:
Location: Blavatnik LT1
| 09:00 | A Resolution-Based Calculus for Preferential Logics (abstract) |
| 09:30 | Enumerating Justifications using Resolution (abstract) |
| 10:00 | A Tableaux Calculus for Reducing Proof Size (abstract) |
09:00-10:30 Session 101E: SAT
Chair:
Location: Blavatnik LT2
| 09:00 | QRAT+: Generalizing QRAT by a More Powerful QBF Redundancy Property (abstract) |
| 09:30 | Extended Resolution Simulates DRAT (abstract) |
| 10:00 | A SAT-Based Approach to Learn Explainable Decision Sets (abstract) |
10:30-11:00Coffee Break
11:00-12:30 Session 104D: Formal Proofs
Chair:
Location: Blavatnik LT1
| 11:00 | Constructive Decision via Redundancy-free Proof-Search (abstract) |
| 11:30 | Verifying Asymptotic Time Complexity of Imperative Programs in Isabelle (abstract) |
| 12:00 | Formalizing Bachmair and Ganzinger's Ordered Resolution Prover (abstract)  |
11:00-12:30 Session 104E: SMT 2
Chair:
Location: Blavatnik LT2
| 11:00 | Exploring Approximations for Floating-Point Arithmetic using UppSAT (abstract) |
| 11:30 | Datatypes with Shared Selectors (abstract) |
| 12:00 | A Reduction from Unbounded Linear Mixed Arithmetic Problems into Bounded Problems (abstract) |
12:30-14:00Lunch Break
14:00-15:00 Session 106D: IJCAR Invited Talk: Martin Giese
Chair:
Location: Blavatnik LT1
| 14:00 | Industrial Data Access – What are the Reasoning Problems? And is Reasoning the Problem? (abstract) |
15:00-15:30 Session 107B: Termination
Chair:
Location: Blavatnik LT1
| 15:00 | Well-Founded Unions (abstract) |
15:30-16:00Coffee Break
16:00-18:00 Session 108D: Logics, Frameworks and Proofs
Chair:
Location: Blavatnik LT1
| 16:00 | From Syntactic Proofs to Combinatorial Proofs (abstract) |
| 16:30 | A Logical Framework with Commutative and Non-Commutative Subexponentials (abstract) |
| 17:00 | Uniform Substitution for Differential Game Logic (abstract) |
| 17:30 | Theories as Types (abstract) |
16:00-18:00 Session 108E: Verification
Chair:
Location: Blavatnik LT2
| 16:00 | Checking Array Bounds by Abstract Interpretation and Symbolic Expressions (abstract) |
| 16:30 | A FOOLish Encoding of the Next State Relations of Imperative Programs (abstract) |
| 17:00 | Proof-Producing Synthesis of CakeML with I/O and Local State from Monadic HOL Functions (abstract) |
| 17:30 | A Why3 framework for reflection proofs and its application to GMP's algorithms (abstract) |
Monday, July 16th
View this program: with abstractssession overviewtalk overviewside by side with other conferences
09:00-10:30 Session 110D: Decidability & Complexity
Chair:
Location: Maths LT2
| 09:00 | Deciding the First-Order Theory of an Algebra of Feature Trees with Updates (abstract) |
| 09:30 | Complexity of Combinations of Qualitative Constraint Satisfaction Problems (abstract) |
| 10:00 | Focussing, MALL and the polynomial hierarchy (abstract) |
10:30-11:00Coffee Break
11:00-12:30 Session 112E: Superposition
Chair:
Location: Maths LT2
| 11:00 | Superposition with Datatypes and Codatatypes (abstract) |
| 11:30 | Superposition for Lambda-Free Higher-Order Logic (abstract) |
| 12:00 | Efficient encodings of first-order Horn formulas in equational logic (abstract) |
12:30-14:00Lunch Break
14:00-15:30 Session 115: FLoC Plenary Lecture: Byron Cook
Chair:
Location: Maths LT1
| 14:00 | Formal Reasoning about the Security of Amazon Web Services (abstract) |
15:30-16:00Coffee Break
16:00-18:00 Session 116A: Oxford Union Debate: Ethics & Morality of Robotics
Public debate on "Ethics & Morality of Robotics" with panelists specializing in ethics, law, computer science, data security and privacy:
- Prof Matthias Scheutz, Dr Sandra Wachter, Prof Jeannette Wing, Prof Francesca Rossi, Prof Luciano Floridi & Prof Ben Kuipers
See http://www.floc2018.org/public-debate/ for further details and to register.
Location: Oxford Union
17:30-18:30 Session 117: Competitions Presentations
Chair:
Location: Maths LT2
| 17:30 | IJCAR competition presentations (abstract) |
19:00-21:30 FLoC banquet at Ashmolean Museum
FLoC banquet at Ashmolean Museum. Drinks and food available from 7pm (pre-booking via FLoC registration system required; guests welcome).
Location: Ashmolean Museum
Tuesday, July 17th
View this program: with abstractssession overviewtalk overviewside by side with other conferences
09:00-10:00 Session 118E: IJCAR Invited Talk: Erika Abraham
Chair:
Location: Maths LT2
| 09:00 | Symbolic Computation Techniques in SMT Solving: Mathematical Beauty meets Efficient Heuristics (abstract) |
10:00-10:30 Session 119: SMT 3
Chair:
Location: Maths LT2
| 10:00 | A Separation Logic with Data: Small Models and Automation (abstract) |
10:30-11:00Coffee Break
11:00-12:30 Session 120D: AR Miscellanea
Chair:
Location: Maths LT2
| 11:00 | Probably Half True: Probabilistic Satisfiability over Lukasiewicz Infinitely-valued Logic (abstract) |
| 11:30 | Automated Reasoning about Key Sets (abstract) |
| 12:00 | An abstraction-refinement framework for reasoning with large theories (abstract) |
12:30-14:00Lunch Break
14:00-15:30 Session 122E: System Descriptions
Chair:
Location: Maths LT2
| 14:00 | The Higher-Order Prover Leo-III (abstract) |
| 14:15 | ATPboost: Learning Premise Selection in Binary Setting with ATP Feedback (abstract) |
| 14:30 | Cubicle-W: Parameterized Model Checking on Weak Memory (abstract) |
| 14:45 | MaedMax: A Maximal Ordered Completion Tool (abstract) |
| 15:00 | Cops and CoCoWeb: Infrastructure for Confluence Tools (abstract) |
| 15:15 | FORT 2.0 (abstract) |
15:30-16:00Coffee Break