LPAR-20: 20TH INTERNATIONAL CONFERENCES ON LOGIC FOR PROGRAMMING, ARTIFICIAL INTELLIGENCE AND REASONING
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

09:00
Logic and Search ( abstract )
10:00-10:30Coffee Break
10:30-12:00 Session 2: Program analysis
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
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
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 )
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

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
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
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
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

09:00
Scaling Formal Software Verification ( abstract )
10:00-10:30Coffee Break
10:30-12:15 Session 10: Reasoning in theories
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
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 12: Non-classical logics and reasoning
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
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
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 )