FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
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

10:30-11:00Coffee Break
11:00-12:30 Session 60E: SMT 1
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 61E: SAT Extensions & Applications
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 63E: Rewriting & Termination
16:00
A Coinductive Approach to Proving Reachability in Logically Constrained Term Rewriting Systems ( abstract )
16:30
Well-Founded Unions ( abstract )
19:00-21:30 Session : 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).

Sunday, July 15th

View this program: with abstractssession overviewtalk overviewside by side with other conferences

09:00-10:30 Session 65D: Logics and Calculi
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 65E: SAT
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 67D: Formal Proofs
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 67E: SMT 2
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 69D: IJCAR Invited Talk: Martin Giese
14:00
Industrial Data Access – What are the Reasoning Problems? And is Reasoning the Problem? ( abstract )
15:00-15:30 Session 70B: Automated Reasoning and Data
15:00
FAME: An Automated Tool for Semantic Forgetting in Expressive Description Logics ( abstract )
15:15
Efficient Model Construction for Horn Logic with VLog: System Description ( abstract )
15:30-16:00Coffee Break
16:00-18:00 Session 71D: Logics, Frameworks and Proofs
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 71E: Verification
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 72D: Decidability & Complexity
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 74E: Superposition
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 77: FLoC Plenary Lecture: Byron Cook
14:00
Formal Reasoning about the Security of Amazon Web Services ( abstract )
15:30-16:00Coffee Break
19:00-21:30 Session : 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).

Tuesday, July 17th

View this program: with abstractssession overviewtalk overviewside by side with other conferences

09:00-10:00 Session 80E: IJCAR Invited Talk: Erika Abraham
09:00
Symbolic Computation Techniques in SMT Solving: Mathematical Beauty meets Efficient Heuristics ( abstract )
10:00-10:30 Session 81: SMT 3
10:00
A Separation Logic with Data: Small Models and Automation ( abstract )
10:30-11:00Coffee Break
11:00-12:30 Session 82D: AR Miscellanea
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 84E: System Descriptions
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