PROGRAM
Days: Tuesday, November 24th Wednesday, November 25th Thursday, November 26th Friday, November 27th Saturday, November 28th
Tuesday, November 24th
View this program: with abstractssession overviewtalk overview
09:00-10:00 Session 1: Logic and Search (Invited Presentation.)
Invited Presentation
Speaker: Mark Wallace
Chair:
09:00 | Logic and Search ( abstract ) |
10:00-10:30Coffee Break
10:30-12:00 Session 2: Program analysis
Chair:
10:30 | Gamifying Program Analysis ( abstract ) |
10:55 | Using Program Synthesis for Program Analysis ( abstract ) |
11:20 | Verification of Concurrent Programs Using Trace Abstraction Refinement ( abstract ) |
12:00-14:00Lunch Break
14:00-15:30 Session 3: Automata Theory
Chair:
14:00 | Synchronized Recursive Timed Automata ( abstract ) |
14:25 | Decidability, Introduction Rules and Automata ( abstract ) |
14:50 | SAT-based Minimization of Deterministic ω-Automata ( abstract ) |
15:15 | Symbolic WS1S ( abstract ) |
15:30-16:00Coffee Break
16:00-17:30 Session 4: Proof Systems
Chair:
16:00 | Normalization by Completeness with Heyting Algebras ( abstract ) |
16:25 | On Subexponentials, Synthetic Connectives, and Multi-Level Delimited Control ( abstract ) |
16:50 | An adequate compositional encoding of bigraph structure in linear logic with subexponentials ( abstract ) |
17:15 | A Lightweight Double-negation Translation ( abstract ) |
18:00-20:00 Session : LPAR opening reception
Opening Reception
Wednesday, November 25th
View this program: with abstractssession overviewtalk overview
09:00-10:00 Session 5: Satisfiability: from Quality to Quantities (Invited Presentation.)
Invited Presentation
Speaker: Nikolaj Bijorner
Chair:
09:00 | Satisfiability: from Quality to Quantities ( abstract ) |
10:00-10:30Coffee Break
10:30-12:10 Session 6: Analysis of security and information flow
Chair:
10:30 | Boolean Formulas for the Static Identification of Injection Attacks in Java ( abstract ) |
10:55 | Analyzing Internet Routing Security Using Model Checking ( abstract ) |
11:20 | Value Sensitivity and Observable Abstract Values for Information Flow Control ( abstract ) |
11:45 | Cobra: A Tool for Solving General Deductive Games ( abstract ) |
12:00-14:00Lunch Break
14:00-15:30 Session 7: Program analysis
Chair:
14:00 | Automated Discovery of Simulation Between Programs ( abstract ) |
14:25 | Finding Inconsistencies in Programs with Loops ( abstract ) |
14:50 | Reasoning About Loops Using Vampire in KeY ( abstract ) |
15:15 | Compiling Hilbert's epsilon operator ( abstract ) |
15:30-16:00Coffee Break
16:00-18:00 Session 8: Automated Reasoning
Chair:
16:00 | Compositional Propositional Proofs ( abstract ) |
16:25 | There Is No Best Beta-Normalization Strategy for Higher-Order Reasoners ( abstract ) |
16:50 | Automated Benchmarking of Incremental SAT and QBF Solvers ( abstract ) |
17:15 | FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover ( abstract ) |
17:40 | Reasoning in the presence of inconsistency through Preferential ALC ( abstract ) |
Thursday, November 26th
View this program: with abstractssession overviewtalk overview
Friday, November 27th
View this program: with abstractssession overviewtalk overview
09:00-10:00 Session 9: Scaling Formal Software Verification (Invited Presentation.)
Invited Presentation
Speaker: Gerwin Klein
Chair:
09:00 | Scaling Formal Software Verification ( abstract ) |
10:00-10:30Coffee Break
10:30-12:15 Session 10: Reasoning in theories
Chair:
10:30 | Sharing HOL4 and HOL Light proof knowledge ( abstract ) |
10:55 | Abstract Domains and Solvers for Sets Reasoning ( abstract ) |
11:20 | Fine grained SMT proofs for the theory of fixed-width bit-vectors ( abstract ) |
11:45 | Playing with Quantified Satisfaction ( abstract ) |
12:00 | Automated Deduction in the B Set Theory using Typed Proof Search and Deduction Modulo ( abstract ) |
12:00-14:00Lunch Break
14:00-15:30 Session 11: Logic programming and applications
Chair:
14:00 | Modelling Moral Reasoning and Ethical Responsibility with Logic Programming ( abstract ) |
14:25 | Modular Multiset Rewriting ( abstract ) |
14:50 | A Fast Interpreter for λProlog ( abstract ) |
15:15 | On Conflicts and Strategies in QBF ( abstract ) |
15:30-16:00Coffee Break
16:00-18:00 Session
PC Dinner
16:00-18:00 Session 12: Non-classical logics and reasoning
Chair:
16:00 | A Contextual Logical Framework ( abstract ) |
16:25 | Focused labeled proof systems for modal logic ( abstract ) |
16:50 | A Labelled Sequent Calculus for Intuitionistic Public Announcement Logic ( abstract ) |
17:15 | Skolemization for Substructural Logics ( abstract ) |
17:40 | Automated Theorem Proving by Translation to Description Logic ( abstract ) |
Saturday, November 28th
View this program: with abstractssession overviewtalk overview
08:30-10:00 Session 13: Decidability results
08:30 | On the expressive power of communication primitives in parameterised systems ( abstract ) |
08:55 | Controller synthesis for MDPs and Frequency LTL\GU ( abstract ) |
09:20 | Reasoning about embedded dependencies using inclusion dependencies ( abstract ) |
10:00-10:30Coffee Break
10:30-12:00 Session 14: Complexity results
Chair:
10:30 | On CTL* with Graded Path Modalities ( abstract ) |
10:55 | Implicit Computational Complexity of Subrecursive Definitions and Applications to Cryptographic Proofs ( abstract ) |
11:20 | On Anti-Subsumptive Knowledge Enforcement ( abstract ) |
11:45 | A New Proof of P-time Completeness of Linear Lambda Calculus ( abstract ) |
12:00-14:00Lunch Break
14:00-15:30 Session 15: Reasoning in theories
14:00 | Tableau-based Revision over SHIQ TBoxes ( abstract ) |
14:25 | ConsTrained Rewriting tooL ( abstract ) |
14:50 | Relational reasoning via probabilistic coupling ( abstract ) |
15:15 | Application of Trace-Based Subjective Logic to User Preferences Modeling ( abstract ) |
15:30-16:00Coffee Break
16:00-18:00 Session 16: Automated proofs
Chair:
16:00 | SAT modulo intuitionistic implications ( abstract ) |
16:25 | Proof Search in Nested Sequent Calculi ( abstract ) |
16:50 | Enhancing Search-Based QBF Solving by Dynamic Blocked Clause Elimination ( abstract ) |
17:15 | TIP: Tools for Inductive Provers ( abstract ) |
19:00-22:00 Session : Farewell banquet
Farewell Dinner