PROGRAM
Days: Wednesday, July 9th Thursday, July 10th Friday, July 11th Saturday, July 12th Sunday, July 13th Monday, July 14th Tuesday, July 15th Wednesday, July 16th Thursday, July 17th Friday, July 18th Saturday, July 19th Sunday, July 20th Monday, July 21st Tuesday, July 22nd Wednesday, July 23rd Thursday, July 24th
Wednesday, July 9th, 2014
View this program: with abstractssession overviewtalk overview
14:00-15:00 Session 1: Models and Sets Session - Invited Talk (INFINITY)
Location: Kurt Gödel Research Center
| 14:00 | Interactions of Set Theory, $L_{\omega_1,\omega}$, and AEC (abstract) |
15:15-16:15 Session 2: Computations and Sets Session - Invited Talk (INFINITY)
Location: Kurt Gödel Research Center
| 15:15 | Proof Theoretic Characterisations of Feasible Set Functions (abstract) |
16:45-17:45 Session 3: Proofs and Sets Session - Invited Talk (INFINITY)
Location: Kurt Gödel Research Center
| 16:45 | Systems of Strength H(1) (abstract) |
Thursday, July 10th, 2014
View this program: with abstractssession overviewtalk overview
08:30-09:30 Session 4: Computations and Sets Session - Invited Talk (INFINITY)
Location: Kurt Gödel Research Center
| 08:30 | Cobham Recursive Set Functions (abstract) |
09:45-10:45 Session 5: Models and Sets Session - Invited Talk (INFINITY)
Location: Kurt Gödel Research Center
| 09:45 | Infinitely deep languages and neighbors (abstract) |
11:15-12:15 Session 6: Computations and Models Session - Invited Talk (INFINITY)
Location: Kurt Gödel Research Center
| 11:15 | Computing a floor function (abstract) |
14:00-15:00 Session 7: Models and Sets Session - Invited Talk (INFINITY)
Location: Kurt Gödel Research Center
| 14:00 | When excellence and local finiteness collide (abstract) |
15:15-16:15 Session 8: Computations and Models Session - Invited Talk (INFINITY)
Location: Kurt Gödel Research Center
| 15:15 | Functors in Computable Model Theory (abstract) |
16:45-17:45 Session 9: Computations and Models Session - Invited Talk (INFINITY)
Location: Kurt Gödel Research Center
| 16:45 | Classes of structures with no intermediate isomorphism problems (abstract) |
Friday, July 11th, 2014
View this program: with abstractssession overviewtalk overview
08:30-09:30 Session 10: Proofs and Sets Session - Invited Talk (INFINITY)
Location: Kurt Gödel Research Center
| 08:30 | Power Kripke-Platek set theory, ordinal analysis and global choice (abstract) |
09:45-10:45 Session 11: Computations and Sets Session - Invited Talk (INFINITY)
Location: Kurt Gödel Research Center
| 09:45 | Set functions with small circuits (abstract) |
11:15-12:15 Session 12: Proofs and Sets Session - Invited Talk (INFINITY)
Location: Kurt Gödel Research Center
| 11:15 | Analytic combinatorics of the transfinite (abstract) |
Saturday, July 12th, 2014
View this program: with abstractssession overviewtalk overview
08:45-10:15 Session 13A: LCC Opening and Invited Talk (Moser) (LCC)
Location: FH, Zeichensaal 3
| 08:45 | LCC'14 Opening Remarks (abstract) |
| 08:50 | Weighted Automata Theory for Complexity Analysis of Rewrite Systems (abstract) |
| 09:45 | Non-uniform Polytime Computation in the Infinitary Affine Lambda-calculus (abstract) |
08:45-10:15 Session 13B: Calculi (HOR)
Chair:
Location: FH, Seminarraum 101C
| 08:45 | The dynamic pattern calculus as a higher-order pattern rewriting system (abstract) |
| 09:15 | Distilling Abstract Machines (abstract) |
| 09:45 | Experience with Higher Order Rewriting from the Compiler Teaching Trenches (abstract) |
09:00-10:15 Session 14: Improvements to ACL2 (ACL2)
Location: FH, Hörsaal 7
| 09:00 | Industrial-Strength Documentation for ACL2 (abstract) |
| 09:30 | Enhancements to ACL2 in Versions 6.2, 6.3, and 6.4 (abstract) |
09:10-10:15 Session 15: Lambda Calculus (SD)
Location: FH, Zeichensaal 1
| 09:10 | Opening Remarks (abstract) |
| 09:15 | Simply Typed Lambda-Calculus Modulo Type Isomorphisms (abstract) |
10:15-10:45Coffee Break
10:45-12:00 Session 16A: PC Opening and Invited Talk (Pavel Pudlak) (PC)
Chair:
Location: FH, Seminarraum 101B
| 10:45 | Opening (abstract) |
| 11:00 | On Some Conjectures in Proof Complexity (abstract) |
10:45-12:45 Session 16B: Contributed Talks (LCC)
Location: FH, Zeichensaal 3
| 10:45 | Towards recursion schemata for the probablistic class PP (abstract) |
| 11:15 | Closing a Gap in the Complexity of Refinement Modal Logic (abstract) |
| 11:45 | On the Complexity of Symbolic Verification and Decision Problems in Bit-Vector Logic (abstract) |
| 12:15 | First-Order Logic of Order and Metric has the Three-Variable Property (abstract) |
10:45-13:00 Session 16C: Datatypes and machine learning (ACL2)
Location: FH, Hörsaal 7
| 10:45 | Experiments with TPTP-style Automated Theorem Provers on ACL2 Problems (abstract) |
| 11:15 | Polymorphic Types In ACL2 (abstract) |
| 11:45 | Data Definitions in ACL2 Sedan (abstract) |
| 12:15 | ACL2(ml): Machine-Learning for ACL2 (abstract) |
10:45-12:00 Session 16D: Foundations (HOR)
Chair:
Location: FH, Seminarraum 101C
| 10:45 | The Higher-order Dependency Pair Framework (abstract) |
| 11:15 | Feebly not weakly (abstract) |
| 11:45 | Report from the HOR 2014 Chair & Discussion (abstract) |
10:45-12:45 Session 16E: Sequent Calculus and Proof Nets (SD)
Location: FH, Zeichensaal 1
| 10:45 | Completions and the Schuette method (abstract) |
| 11:45 | A Correctness Criterion Free from Switchings (abstract) |
| 12:15 | First-order Proofs Without Syntax: Summary of Work in Progress (abstract) |
12:00-13:00 Session 17A: HOR/WIR Invited Talk (HOR and WIR)
Chair:
Location: FH, Seminarraum 101C
| 12:00 | On Infinitary Affine Lambda-Calculi (abstract) |
12:00-13:00 Session 17B: Contributed Talks: SAT and QBF (PC)
Chair:
Location: FH, Seminarraum 101B
| 12:00 | Size-Space Bounds and Trade-offs for CDCL Proofs (abstract) |
| 12:30 | Beyond Q-Resolution and Prenex Form: A Proof System for Quantified Constraint Satisfaction (abstract) |
13:00-14:30Lunch Break
14:30-15:30 Session 18A: Invited Talk (Jakob Nordström) (PC)
Chair:
Location: FH, Seminarraum 101B
| 14:30 | A (Biased) Survey of Space Complexity and Time-Space Trade-offs in Proof Complexity (abstract) |
14:30-16:00 Session 18B: Invited Talk (Buss) and Contributed Talks (LCC)
Location: FH, Zeichensaal 3
| 14:30 | Search problems, proof complexity, and second-order bounded arithmetic (abstract) |
| 15:30 | Infinite AC0 Circuits for Parity (abstract) |
14:30-16:00 Session 18C: Keynote Mike Gordon (ACL2)
Location: FH, Hörsaal 7
| 14:30 | Linking ACL2 and HOL: past achievements and future prospects (abstract) |
14:30-16:00 Session 18D (WIR)
Location: FH, Seminarraum 101C
| 14:30 | Dynamical systems, attractors and well-behaved infinitary rewriting (abstract) |
| 15:00 | From the finite to the transfinite: Λμ-terms and streams. (abstract) |
| 15:30 | Normal Forms and Infinity (abstract) |
14:30-16:00 Session 18E: Algebra and Topology (SD)
Location: FH, Zeichensaal 1
| 14:30 | Proof theory for ordered algebra: amalgamation and densification (abstract) |
| 15:30 | Weak topologies for Linear Logic (abstract) |
14:30-16:00 Session 18F (2FC)
Chair:
Location: FH, Dissertantenraum E104
| 14:30 | A cubical representation of local states (abstract) |
| 15:00 | Computational complexity in the lambda-calculus: what's new? (abstract) |
| 15:30 | On the parallel reduction and complexity of interaction-net systems (abstract) |
15:30-16:00 Session 19: Contributed Talk: Polynomial Calculus (PC)
Chair:
Location: FH, Seminarraum 101B
| 15:30 | Towards an Understanding of Polynomial Calculus: New Separations and Lower Bounds (abstract) |
16:00-16:30Coffee Break
16:30-18:00 Session 20A: Contributed Talks: Bounded Arithmetic (PC)
Chair:
Location: FH, Seminarraum 101B
| 16:30 | Provably Total Search Problems in Fragments of Bounded Arithmetic Below Polynomial-time (abstract) |
| 17:00 | Parameter-free induction in bounded arithmetic (abstract) |
| 17:30 | Logical strength of complexity theory and a formalization of the PCP theorem in bounded arithmetic (abstract) |
16:30-18:00 Session 20B: Contributed Talks (LCC)
Location: FH, Zeichensaal 3
| 16:30 | Descriptive Complexity and CSP (abstract) |
| 17:00 | Capturing Bisimulation-Invariant Complexity Classes with Higher-Order Modal Fixpoint Logic (abstract) |
| 17:30 | Small Dynamic Descriptive Complexity Classes (abstract) |
16:30-19:00 Session 20C: Economics, Rump Sessions and Business Meeting (ACL2)
Location: FH, Hörsaal 7
| 16:30 | On Vickrey's Theorem and the Use of ACL2 for Formal Reasoning in Economics (abstract) |
16:30-18:00 Session 20D: WIR Contributed Talks (WIR)
Location: FH, Seminarraum 101C
| 16:30 | An Introduction to the Clocked Lambda Calculus (abstract) |
| 17:00 | Work in Progress: Algebraic Abstract Reduction Systems (abstract) |
| 17:30 | Turtle graphics of morphic streams (abstract) |
16:30-17:30 Session 20E: Normalisation and Ludics (SD)
Location: FH, Zeichensaal 1
| 16:30 | Substructural Cut Elimination (abstract) |
| 17:00 | Multiplicative Decomposition of Behaviours in Ludics (abstract) |
16:30-18:00 Session 20F (2FC)
Chair:
Location: FH, Dissertantenraum E104
| 16:30 | On the Value of Variables (abstract) |
| 17:00 | Automated Complexity Analysis of Term Rewrite Systems (abstract) |
| 17:30 | Subrecursive Linear Dependent Types and Computational Security (abstract) |
18:15-19:15 Session 21 (2FC)
Chair:
Location: FH, Dissertantenraum E104
| 18:15 | Proof theoretic approaches to rewriting (abstract) |
Sunday, July 13th, 2014
View this program: with abstractssession overviewtalk overview
08:45-10:15 Session 22A (Linearity)
Chair:
Location: FH, Seminarraum 136
| 08:45 | Modalities and Linearity (abstract) |
| 09:45 | The inhabitation problem for non-idempotent intersection (abstract) |
08:45-10:15 Session 22B: Isabelle tutorial for beginners I (Isabelle)
Location: FH, Zeichensaal 1
| 08:45 | Isabelle tutorial for beginners (part 1) (abstract) |
08:45-10:15 Session 22C: Isabelle workshop (Isabelle)
Chair:
Location: FH, Seminarraum 138C
| 08:45 | A formally verified proof of the Central Limit Theorem (abstract) |
| 09:15 | Primitively (Co)recursive Definitions for Isabelle/HOL (abstract) |
| 09:45 | Pattern-based Subterm Selection In Isabelle (abstract) |
08:45-10:15 Session 22D: Novel Directions in QBF Research (QBF)
Location: FH, Hörsaal 2
| 08:45 | A Unified Proof System for QBF Preprocessing (abstract) |
| 09:30 | On Instantiation-Based Calculi for QBF (abstract) |
08:45-10:15 Session 22E: HOL Workshop (HOL)
Location: FH, CAD 2
| 08:45 | Welcome (abstract) |
| 09:00 | Using HOL4 to Formalize Physical Systems (abstract) |
| 09:30 | Modernising HOL's documentation (abstract) |
08:45-10:15 Session 22F: Induction and Disscusion on ISR (IFIP-WG16)
Location: FH, Seminarraum 101C
| 08:45 | Decision Procedures for Proving Inductive Theorems without Induction (abstract) |
| 09:15 | Discussion on the International School on Rewriting (ISR) (abstract) |
08:45-09:00 Session 22G: Welcome (CLC)
Location: FH, Dissertantenraum E104
09:00-10:15 Session 23A: WPTE Opening and Invited Talk by Andy Gill on HERMIT (WPTE)
Location: FH, Hörsaal 4
| 09:00 | Opening (abstract) |
| 09:15 | HERMIT: An Equational Reasoning Model to Implementation Rewrite System for Haskell (abstract) |
09:00-10:15 Session 23B: Opening, Invited Talk, and Contributed Talk (GSB)
Chair:
Location: FH, Seminarraum 138A
| 09:00 | Welcome (abstract) |
| 09:05 | Semantics and Proof Theory in Team Play: the case of Paraconsistent Logics (abstract) |
| 09:50 | On the Construction of Analytic Sequent Calculi for Sub-classical Logics (abstract) |
09:00-10:15 Session 23C: Opening and Invited Talk 1 (UNIF)
Location: FH, Seminarraum 104
| 09:00 | Opening (abstract) |
| 09:15 | Extensible Symbolic System Analysis (abstract) |
09:00-10:15 Session 23E: Non-standard Analysis (ACL2)
Location: FH, Hörsaal 7
| 09:00 | Formal Verification of Medina's Sequence of Polynomials for Approximating Arctangent (abstract) |
| 09:30 | Equivalence of the Traditional and Non-Standard Definitions of Concepts from Real Analysis (abstract) |
09:00-10:15 Session 23F: ImmermanFest Opening and Invited Talk (LCC)
Location: FH, Zeichensaal 3
| 09:00 | ImmermanFest Opening Remarks (abstract) |
| 09:15 | 27 and still counting: Iterated product, inductive counting, and the structure of P (abstract) |
09:00-10:15 Session 23G: Invited Talk (DTP)
Location: FH, Seminarraum 325/1
| 09:00 | FRP, LTL and GUIs (abstract) |
09:00-10:15 Session 23H: Opening and Invited Talk (FWFM)
Location: FH, Seminarraum 134
| 09:00 | Fun With Formal Methods 2014: Opening Remarks (abstract) |
| 09:15 | Algebraic description of restricted programming and elements of its logics (abstract) |
09:00-10:20 Session 23I (CLC)
Location: FH, Dissertantenraum E104
| 09:00 | TBC (abstract) |
| 10:00 | Extensional Models of Typed Lambda-mu Calculus (abstract) |
09:15-10:15 Session 24A: Joint DCM / TermGraph Invited Talk (DCM and TermGraph)
Chair:
Location: FH, Seminarraum 325/2
| 09:15 | Numeral Systems in the Lambda Calculus (abstract) |
09:15-10:15 Session 24B: Parallel SAT (POS)
Location: FH, Hörsaal 3
| 09:15 | Dolius: A Distributed Parallel SAT Solving Framework (abstract) |
| 09:45 | Validating Unsatisfiability Results of Clause Sharing Parallel SAT Solvers (abstract) |
09:15-10:15 Session 24C: Contributed Talks: Proof Complexity (PC)
Chair:
Location: FH, Seminarraum 101B
| 09:15 | Quasipolynomial Size Frege Proofs of Frankl's Theorem on the Trace of Finite Sets (abstract) |
| 09:45 | n^O(log log n) size monotone proofs of the weak pigeonhole principle (abstract) |
09:15-10:15 Session 24D (LSB)
Location: FH, Seminarraum 134A
| 09:15 | An algebraic approach for inferring and using symmetries in rule-based models (abstract) |
09:15-10:15 Session 24E: Invited talk (LOLA)
Location: FH, Seminarraum 107
| 09:15 | De haut en bas: relating high-level and low-level abstractions (abstract) |
09:25-10:15 Session 25: Opening and invited talk (IWC)
Location: FH, Seminarraum 303
| 09:25 | On the Formalization of Lambda-Calculus Confluence and Residuals (abstract) |
10:15-10:45Coffee Break
10:45-12:45 Session 26A: Invited Talks (LCC)
Location: FH, Zeichensaal 3
| 10:45 | Some Reflections on Definability and Complexity (abstract) |
| 11:45 | Crane Beach Revisited (abstract) |
10:45-12:45 Session 26B (Linearity)
Chair:
Location: FH, Seminarraum 136
| 10:45 | Undecidability of Multiplicative Subexponential Logic (abstract) |
| 11:15 | Superstructural Reversible Logic (abstract) |
| 11:45 | A Linear/Producer/Consumer model of Classical Linear Logic (abstract) |
| 12:15 | Cut Elimination in Multifocused Linear Logic (abstract) |
10:45-13:00 Session 26C: Concurrency, Unfolding, Pi-Calculus, Reaction Networks (WPTE)
Location: FH, Hörsaal 4
| 10:45 | Verifying Optimizations for Concurrent Programs (abstract) |
| 11:15 | Inverse Unfold Problem and Its Heuristic Solving (abstract) |
| 11:45 | Short break (abstract) |
| 12:00 | Structural Rewriting in the Pi-Calculus (abstract) |
| 12:30 | Attractor Equivalence: An Observational Semantics for Reaction Networks (abstract) |
10:45-12:45 Session 26D: Isabelle tutorial for beginners II (Isabelle)
Location: FH, Zeichensaal 1
| 10:45 | Isabelle tutorial for beginners (part 2) (abstract) |
10:45-12:45 Session 26E: Isabelle workshop (Isabelle)
Chair:
Location: FH, Seminarraum 138C
| 10:45 | The CoCon Experiment (abstract) |
| 10:55 | The CAVA Automata Library (abstract) |
| 11:20 | From Types to Sets in Isabelle/HOL (abstract) |
| 11:45 | Towards abstract and executable multivariate polynomials in Isabelle (abstract) |
| 12:15 | Tutorial: Isabelle/jEdit for seasoned Isabelle users (abstract) |
10:45-12:15 Session 26F: Computing with Graphs (TermGraph)
Chair:
Location: FH, Seminarraum 325/2
| 10:45 | Needed Computations Shortcutting Needed Steps (abstract) |
| 11:15 | Proving Termination of Unfolding Graph Rewriting for General Safe Recursion (abstract) |
| 11:45 | Nested Term Graphs (abstract) |
10:45-12:50 Session 26G: Contributed Talks (GSB)
Chair:
Location: FH, Seminarraum 138A
| 10:45 | Comparing Sequent Calculi via Hilbert-style Axioms (abstract) |
| 11:10 | Sequent Systems for Classical Modal Logics (abstract) |
| 11:35 | Lyndon Interpolation for the Modal Mu-Calculus (abstract) |
| 12:00 | On cuts and cut-elimination in modal fixed point logics (abstract) |
| 12:25 | Display-type calculi and their cut elimination metatheorem (abstract) |
10:45-13:00 Session 26H: QBF Proofs and Certificates, DQBF (QBF)
Location: FH, Hörsaal 2
| 10:45 | On the Relation between Resolution Calculi for QBFs and First-order Formulas (abstract) |
| 11:15 | Resolution Paths and Term Resolution (abstract) |
| 11:45 | Efficient Extraction of QBF (Counter)models from Long-Distance Resolution Proofs (abstract) |
| 12:15 | Dependency Quantified Boolean Formulas - Challenges, Applications, First Lines of Attack (abstract) |
10:45-13:00 Session 26I: HOL Workshop (HOL)
Location: FH, CAD 2
| 10:45 | Writing proof automation for HOL4 (abstract) |
| 11:15 | Hack Session 1 (abstract) |
10:45-11:45 Session 26J: Regular talks (IWC)
Location: FH, Seminarraum 303
| 10:45 | Certification of Confluence Proofs using CeTA (abstract) |
| 11:15 | Confluence and Critical-Pair-Closing Systems (abstract) |
10:45-13:00 Session 26L (UNIF)
Location: FH, Seminarraum 104
| 10:45 | Unification Modulo Common List Functions (abstract) |
| 11:15 | Matching with respect to general concept inclusions in the Description Logic EL (abstract) |
| 11:45 | Unification in the normal modal logic Alt1 (abstract) |
| 12:15 | On Asymmetric Unification and the Combination Problem in Disjoint Theories (Extended Abstract) (abstract) |
| 12:35 | Hierarchical Combination of Matching Algorithms (Extended Abstract) (abstract) |
10:45-13:00 Session 26M: Analysis (POS)
Location: FH, Hörsaal 3
| 10:45 | Post Mortem Analysis of SAT Solver Proofs (abstract) |
| 11:15 | Formula partitioning revisited (abstract) |
| 11:45 | New CNF Features and Formula Classification (abstract) |
| 12:15 | Typical-case complexity and the SAT competitions (abstract) |
10:45-11:45 Session 26N: Invited Talk (Albert Atserias) (PC)
Chair:
Location: FH, Seminarraum 101B
| 10:45 | Weak Pigeonhole Principles, Circuits for Approximate Counting, and Bounded-Depth Proofs (abstract) |
10:45-13:00 Session 26P: Theorem Proving and MOOCs (IFIP-WG16)
Location: FH, Seminarraum 101C
| 10:45 | Rewriting, Proofs and Transition Systems (abstract) |
| 11:30 | Semantically-Guided Goal-Sensitive Theorem Proving (abstract) |
| 12:00 | Impacts of the Digital Revolution on two Main Activities of Scientists: Teaching and Publishing (abstract) |
| 12:30 | Discussion on Massive Open Online Courses and Overlay Journals (abstract) |
10:45-13:00 Session 26Q (LSB)
Location: FH, Seminarraum 134A
| 10:45 | Using answer set programming to integrate large-scale heterogeneous information about the response of a biological system (abstract) |
| 11:30 | Attractor equivalence: An observational semantics for reaction networks (abstract) |
| 12:15 | A Logical Framework for Systems Biology (abstract) |
10:45-13:00 Session 26R: Verification (ACL2)
Location: FH, Hörsaal 7
| 10:45 | Modeling Algorithms in SystemC and ACL2 (abstract) |
| 11:15 | Development of a Translator from LLVM to ACL2 (abstract) |
| 11:45 | An ACL2 Mechanization of an Axiomatic Framework for Weak Memory (abstract) |
| 12:15 | Using ACL2 to Verify Loop Pipelining in Behavioral Synthesis (abstract) |
10:45-13:00 Session 26S: Contributed Talks (DTP)
Location: FH, Seminarraum 325/1
| 10:45 | Terminal semantics for codata types in intensional Martin-Löf type theory (abstract) |
| 11:15 | A Unifying Framework for Primitive Ontological Relations in Dependent Type Theory (abstract) |
| 11:45 | Domain Specific Languages of Mathematics (abstract) |
| 12:15 | Relational ornaments (abstract) |
10:45-11:45 Session 26T (DCM)
Location: FH, Seminarraum 138B
| 10:45 | A Simple Parallel Implementation of Interaction Nets in Haskell (abstract) |
| 11:15 | Some observations for the parallel implementation of interaction nets (abstract) |
10:45-12:45 Session 26U: Contributed talks (LOLA)
Location: FH, Seminarraum 107
| 10:45 | Abstract Self Modifying Machines (abstract) |
| 11:15 | Programming and Verifying with Effect Handling and Iteration (abstract) |
| 11:45 | Tensorial logic with algebraic effects (abstract) |
| 12:15 | Compiling Effectful Terms to Transducers: Prototype Implementation of Memoryful Geometry of Interaction (abstract) |
10:50-13:00 Session 27 (CLC)
Location: FH, Dissertantenraum E104
| 10:50 | A Translation of Intersection and Union Types for the lambda-mu Calculus (abstract) |
| 11:10 | Dualized Type Theory (abstract) |
| 11:30 | A proof-theoretic view on scheduling in concurrency (abstract) |
| 12:00 | A type system for Continuation Calculus (abstract) |
| 12:30 | Confluence for classical logic through the distinction between values and computations (abstract) |
11:00-13:00 Session 28A: Evaluation and Benchmarks (ORE)
Chair:
Location: FH, Seminarraum 101A
| 11:00 | TROvE: a Graphical Tool to Evaluate OWL Reasoners (abstract) |
| 11:20 | Using OpenStreetMap Data to Create Benchmarks for Description Logic Reasoners (abstract) |
| 11:40 | A Scalable Benchmark for OBDA Systems: Preliminary Report (abstract) |
| 12:00 | Evaluating OWL 2 Reasoners in the Context Of Checking Entity-Relationship Diagrams During Software Development (abstract) |
| 12:20 | Just: a Tool for Computing Justifications w.r.t. ELH Ontologies (abstract) |
| 12:40 | Android Went Semantic: Time for Evaluation (abstract) |
11:00-13:00 Session 28B: Technical session (FWFM)
Location: FH, Seminarraum 134
| 11:00 | Chekofv: Crowd-sourced Formal Verification (abstract) |
| 11:30 | Using Esoteric Language for Teaching Formal Semantics (abstract) |
| 12:00 | Introducing Formal Verification with Lego (abstract) |
| 12:30 | Explaining the decompositionality of MSO using applications to combinatorics (abstract) |
12:00-13:00 Session 29A: Regular talks (IWC)
Location: FH, Seminarraum 303
| 12:00 | Critical Pairs in Network Rewriting (abstract) |
| 12:30 | On Proving Confluence of Conditional Term Rewriting Systems via the Computationally Equivalent Transformation (abstract) |
12:00-13:00 Session 29B: Contributed Talks: Resolution (PC)
Chair:
Location: FH, Seminarraum 101B
| 12:00 | Total Space in Resolution (abstract) |
| 12:30 | From Small Space to Small Width in Resolution (abstract) |
12:00-13:00 Session 29C (DCM)
Location: FH, Seminarraum 138B
| 12:00 | Quantitative semantics for higher-order probabilistic and quantum computation (abstract) |
13:00-14:30Lunch Break
14:00-16:00 Session 30: Invited Talks (LCC)
Location: FH, Zeichensaal 3
| 14:00 | On the power of fixed-point logic with counting (abstract) |
| 15:00 | Reasoning about transitive closure in Immerman's style (abstract) |
14:30-16:00 Session 31A (Linearity)
Chair:
Location: FH, Seminarraum 136
| 14:30 | Continuations, closed reduction and process networks (abstract) |
| 15:30 | Type Classes for Lightweight Substructural Types (abstract) |
14:30-16:00 Session 31B: Conditional Rewriting, Polymorphic Calculi (WPTE)
Location: FH, Hörsaal 4
| 14:30 | On Proving Soundness of the Computationally Equivalent Transformation for Normal Conditional Term Rewriting Systems by Using Unravelings (abstract) |
| 15:00 | Contextual Equivalences in Call-by-Need and Call-By-Name Polymorphically Typed Calculi (Preliminary Report) (abstract) |
| 15:30 | Verifying the Correctness of Tupling Transformations based on Conditional Rewriting (abstract) |
14:30-16:00 Session 31C: Isabelle workshop (Isabelle)
Chair:
Location: FH, Seminarraum 138C
| 14:30 | Proving Gödel’s Incompleteness Theorems (abstract) |
| 15:00 | Isabelle/jEdit NEWS (abstract) |
| 15:30 | Programming TLS in Isabelle/HOL (abstract) |
14:30-15:30 Session 31D: Joint IWC / TermGraph Invited Talk (IWC and TermGraph)
Chair:
Location: FH, Seminarraum 325/2
| 14:30 | An Introduction to Higher-Dimensional Rewriting Theory (abstract) |
14:30-16:05 Session 31E: Invited Talk and Contributed Talks (GSB)
Chair:
Location: FH, Seminarraum 138A
| 14:30 | Cyclic proof for quantitative logics (abstract) |
| 15:15 | Modular Systems for Intuitionistic Modal Logics in Nested Sequents (abstract) |
| 15:40 | An Intuitionisticaly based Description Logic (abstract) |
14:30-16:00 Session 31F: QBF Applications (1): Incremental QBF Solving (QBF)
Location: FH, Hörsaal 2
| 14:30 | Incremental QBF Reasoning for the Verification of Partial Designs (abstract) |
| 15:00 | Reactive Synthesis using (Incremental) QBF Solving (abstract) |
| 15:30 | Conformant Planning as a Case Study of Incremental QBF Solving (abstract) |
14:30-16:00 Session 31G: HOL Workshop (HOL)
Location: FH, CAD 2
| 14:30 | HOL4 Hidden Features (abstract) |
| 15:00 | New Styles of Proof (abstract) |
| 15:30 | Hack Session 2 (abstract) |
14:30-15:30 Session 31H: Ontologies (ORE)
Chair:
Location: FH, Seminarraum 101A
| 14:30 | Exploring Reasoning with the DMOP Ontology (abstract) |
| 14:50 | An update on Genomic CDS, a complex ontology for pharmacogenomics and clinical decision support (abstract) |
| 15:10 | A Family History Knowledge Base in OWL 2 (abstract) |
14:30-16:00 Session 31I: Invited Talk 2 and Regular Talk (UNIF)
Location: FH, Seminarraum 104
| 14:30 | On the Limits of Second-Order Unification (abstract) |
| 15:30 | From Admissibility to a New Hierarchy of Unification Types (abstract) |
14:30-15:30 Session 31J: Invited talk (POS)
Chair:
Location: FH, Hörsaal 3
| 14:30 | Lingeling Essentials, A Tutorial on Design and Implementation Aspects of the the SAT Solver Lingeling (abstract) |
14:30-15:30 Session 31K: Invited Talk (Iddo Tzameret) (PC)
Chair:
Location: FH, Seminarraum 101B
| 14:30 | Are matrix identities hard instances for strong proof systems? (abstract) |
14:30-16:00 Session 31L: Normalization and Music (IFIP-WG16)
Location: FH, Seminarraum 101C
| 14:30 | Basic Normalization (abstract) |
| 15:15 | Rhythm Tree Rewriting (abstract) |
14:30-16:00 Session 31M (LSB)
Location: FH, Seminarraum 134A
| 14:30 | TBA (abstract) |
| 15:15 | Model Checking the Evolution of Gene Regulatory Networks (abstract) |
14:30-16:00 Session 31N: Keynote Magnus Myreen (ACL2)
Location: FH, Hörsaal 7
| 14:30 | Machine-code verification: experience of tackling medium-sized case studies using 'decompilation into logic’ (abstract) |
14:30-16:00 Session 31P: Contributed Talks (DTP)
Location: FH, Seminarraum 325/1
| 14:30 | An Embedded Hardware Description Language using Dependent Types (abstract) |
| 15:00 | Type-Directed Editing for Dependently-Typed Programs. (abstract) |
| 15:30 | Tool Demonstration: An IDE for Programming and Proving in Idris (abstract) |
14:30-15:30 Session 31Q: Technical session (FWFM)
Location: FH, Seminarraum 134
| 14:30 | Towards the Application of Formal Methods in Process Engineering (abstract) |
| 15:00 | An Example Demonstrating the Requirement of Fully Formal Verification Method (abstract) |
14:30-16:00 Session 31R (DCM)
Location: FH, Seminarraum 138B
| 14:30 | Cellular Automata are Generic (abstract) |
| 15:00 | Quantum Circuits for the Unitary Permutation Problem (abstract) |
| 15:30 | Propositional Logics Complexity and the sub-formula Property (abstract) |
14:30-16:00 Session 31S (CLC)
Location: FH, Dissertantenraum E104
| 14:30 | Infinitary Classical Logic: Recursive Equations and Interactive Semantics (abstract) |
| 15:00 | Separable Sequent Calculus for First-order Classical Logic (Work in Progress) (abstract) |
| 15:20 | Cut-Elimination in Schematic Proofs and Herbrand Sequents (abstract) |
| 15:40 | Stratified Nested Linear Logic (abstract) |
15:00-16:00 Session 32: Invited talk (LOLA)
Location: FH, Seminarraum 107
| 15:00 | On Machines, Virtual Memory and Successful System Verification (abstract) |
15:30-16:00 Session 33B: Regular talk (IWC)
Location: FH, Seminarraum 303
| 15:30 | Confluence of linear rewriting and homology of algebras (abstract) |
15:30-16:00 Session 33C: Formalization (POS)
Location: FH, Hörsaal 3
| 15:30 | Generic CDCL -- A Formalization of Modern Propositional Satisfiability Solvers (abstract) |
15:30-16:00 Session 33D: Panel Discussion (FWFM)
Location: FH, Seminarraum 134
15:30-16:00 Session 33E: Contributed Talk: Complexity of SAT algorithms (PC)
Chair:
Location: FH, Seminarraum 101B
| 15:30 | Lower bounds for splittings by linear combinations (abstract) |
15:30-16:00 Session 33F: Proof Nets (TermGraph)
Chair:
Location: FH, Seminarraum 325/2
| 15:30 | Injectivity of Relational Semantics for (Connected) MELL Proof-Nets via Taylor Expansion (abstract) |
16:00-16:30Coffee Break
16:30-17:45 Session 34A: Invited Talk and Closing (LCC)
Location: FH, Zeichensaal 3
| 16:30 | The Variable Hierarchy on Ordered Graphs (abstract) |
| 17:30 | Closing Remarks (abstract) |
16:30-18:30 Session 34B (Linearity)
Chair:
Location: FH, Seminarraum 136
| 16:30 | Ludics without Designs I: Triads (abstract) |
| 17:00 | Wave-Style Token Machines and Quantum Lambda Calculi (abstract) |
| 17:30 | Geometry of Resource Interaction – A Minimalist Approach (abstract) |
| 18:00 | A new point of view on the Taylor expansion of proof-nets and uniformity (abstract) |
16:30-18:00 Session 34C: Conditional Term Rewriting, Complexity and WPTE Closing (WPTE)
Location: FH, Hörsaal 4
| 16:30 | Notes on Structure-Preserving Transformations of Conditional Term Rewrite Systems (abstract) |
| 17:00 | A Complexity Preserving Transformation from Jinja Bytecode to Rewrite Systems (abstract) |
| 17:30 | Closing (abstract) |
16:30-18:00 Session 34D: Isabelle workshop (Isabelle)
Chair:
Location: FH, Seminarraum 138C
| 16:30 | Using Isabelle/HOL to Develop and Maintain Separation Invariants for an Operating System (Extended Abstract) (abstract) |
| 17:00 | A Simpl Shortest Path Checker Verification (abstract) |
| 17:20 | Towards Structured Proofs for Program Verification (Ongoing Work) (abstract) |
| 17:40 | Amortized Complexity Verified (abstract) |
16:30-17:30 Session 34E: Implementations (TermGraph)
Chair:
Location: FH, Seminarraum 325/2
| 16:30 | An Implementation Model for Interaction Nets (abstract) |
| 17:00 | Fixed Point Theory for Consistent Rewriting in Logic of Action with Reverse (abstract) |
16:30-18:10 Session 34F: Contributed Talks (GSB)
Chair:
Location: FH, Seminarraum 138A
| 16:30 | Link formulas in implication fragments of substructural logics (abstract) |
| 16:55 | A proof theoretic approach to standard completeness (abstract) |
| 17:20 | On Affine Logic and Łukasiewicz Logic (abstract) |
| 17:45 | Simpler Proof Net Quantifiers: Unification Nets (Work in Progress) (abstract) |
16:30-18:00 Session 34G: QBF Applications (2), The QBF Gallery 2014 (QBF)
Location: FH, Hörsaal 2
| 16:30 | Synthesis of distributed systems using QBF (abstract) |
| 17:00 | The QBF Gallery 2014 (abstract) |
16:30-18:30 Session 34H (HOL)
Location: FH, CAD 2
| 16:30 | Discussion Session (abstract) |
| 17:00 | Hack Session 3 (abstract) |
16:30-18:15 Session 34I: Regular talks, confluence competition (CoCo) and closing (IWC)
Location: FH, Seminarraum 303
| 16:30 | Normalization Equivalence of Rewrite Systems (abstract) |
| 17:00 | Non-E-overlapping and weakly shallow TRSs are confluent (Extended abstract) (abstract) |
| 17:30 | Confluence Competition (abstract) |
16:30-17:10 Session 34J: Reasoners (ORE)
Chair:
Location: FH, Seminarraum 101A
| 16:30 | Mini-ME 2.0: powering the Semantic Web of Things (abstract) |
| 16:50 | Incremental and Persistent Reasoning in FaCT++ (abstract) |
16:30-18:00 Session 34K (UNIF)
Location: FH, Seminarraum 104
| 16:30 | Constraint Manipulation in SGGS (abstract) |
| 17:00 | Two-sided unification is NP-complete (abstract) |
| 17:30 | Nominal Anti-Unification (abstract) |
16:30-18:00 Session 34L: Applications and closing (POS)
Location: FH, Hörsaal 3
| 16:30 | iDQ: Instantiation-Based DQBF Solving (abstract) |
| 17:00 | Instance-based Selection of CSP Solvers using Short Training (abstract) |
| 17:30 | Incremental SAT-based Method with Native Boolean Cardinality Handling for the Hamiltonian Cycle Problem (abstract) |
16:30-17:30 Session 34M: Contributed Talks: Proof Complexity (PC)
Chair:
Location: FH, Seminarraum 101B
| 16:30 | Narrow Proofs May Be Maximally Long (abstract) |
| 17:00 | Parity games and propositional proofs (abstract) |
16:30-18:00 Session 34N: Discussion on RTA, Open Problems, and Business Meeting (IFIP-WG16)
Location: FH, Seminarraum 101C
| 16:30 | Discussion on the Future of RTA (+ TLCA) (abstract) |
| 17:00 | Discussion on the Open Problems List in Rewriting (abstract) |
| 17:30 | Business Meeting (abstract) |
16:30-17:30 Session 34P (LSB)
Location: FH, Seminarraum 134A
| 16:30 | The role of domain specific languages in simulation studies - Analyzing the impact of membrane dynamics on the Wnt signaling pathway (abstract) |
16:30-18:00 Session 34Q: Panel Discussion about low-level code verification (ACL2)
Location: FH, Hörsaal 7
16:30-18:00 Session 34R: Contributed Talks (DTP)
Location: FH, Seminarraum 325/1
| 16:30 | Scrapping Your Dependently-Typed Boilerplate is Hard (abstract) |
| 17:00 | On a style of presentation of type systems (abstract) |
| 17:30 | Sequential decision problems and a computational theory of avoidability (abstract) |
16:30-18:00 Session 34S (DCM)
Location: FH, Seminarraum 138B
| 16:30 | Probabilistic Types and Function Overloading (abstract) |
| 17:00 | Differential privacy at work: Verification of approximate probabilistic programs and models for choosing epsilon (abstract) |
| 17:30 | Interactive Particle Systems and Random Walks on Hypergraphs (abstract) |
16:30-17:30 Session 34T: Contributed talks (LOLA)
Location: FH, Seminarraum 107
| 16:30 | A Cross-Language Framework for Verifying Compiler Optimizations (abstract) |
| 17:00 | Call-by-Value in a Basic Logic for Interaction (abstract) |
16:30-18:00 Session 34U (CLC)
Location: FH, Dissertantenraum E104
| 16:30 | A sheaf model of the algebraic closure (abstract) |
| 17:00 | A "Game Semantical" Intuitionistic Realizability Validating Markov's Principle (abstract) |
| 17:20 | Relative Computability and Uniform Continuity of Non-Extensional (aka Multivalued) 'Functions' (abstract) |
| 17:40 | Negative Translations and Heyting Algebra Expansions (abstract) |
18:00-19:00 Session 36 (UNIF)
Location: FH, Seminarraum 104
| 18:00 | A Categorical Perspective on Pattern Unification (Extended Abstract) (abstract) |
| 18:30 | Towards a better-behaved unification algorithm for Coq (abstract) |
Monday, July 14th, 2014
View this program: with abstractssession overviewtalk overview
08:45-09:15 Session 37: VSL Opening (VSL)
Chair:
Location: EI, EI 7 + EI 9, EI 10 + FH, Hörsaal 1
| 08:45 | Welcome Address by the Rector (abstract) |
| 08:50 | Welcome Address by the Organizers (abstract) |
| 08:55 | VSL Opening (abstract) |
09:15-10:15 Session 38: VSL Keynote Talk (VSL)
Chair:
Location: EI, EI 7 + EI 9, EI 10 + FH, Hörsaal 1
| 09:15 | VSL Keynote Talk: Computational Ideas and the Theory of Evolution (abstract) |
10:15-10:45Coffee Break
10:45-13:00 Session 38A: Tutorial by Assia Mahboubi (CSL-LICS)
Chair:
Location: FH, Hörsaal 1
| 10:45 | Computer-checked mathematics: a formal proof of the Odd Order theorem (abstract) |
10:45-13:00 Session 38B: Computability (CSL-LICS)
Chair:
Location: FH, Hörsaal 5
| 10:45 | A quest for algorithmically random infinite structures (abstract) |
| 11:15 | On the Total Variation Distance of Labelled Markov Chains (abstract) |
| 11:45 | A domain-theoretic approach to Brownian motion and general continuous stochastic processes (abstract) |
| 12:15 | On the Computing Power of +, −, and × (abstract) |
10:45-13:00 Session 38C: Verified Theorem Provers (ITP)
Location: FH, Hörsaal 8
| 10:45 | Towards a Formally Verified Proof Assistant (abstract) |
| 11:15 | The reflective Milawa theorem prover is sound (down to the machine code that runs it) (abstract) |
| 11:45 | HOL with Definitions: Semantics, Soundness, and a Verified Implementation (abstract) |
| 12:15 | Proof Pearl: Proving a Simple Von Neumann Machine Turing Complete (abstract) |
| 12:45 | Rough Diamond: An Extension of Equivalence-based Rewriting (abstract) |
10:45-13:00 Session 38D (RTA-TLCA)
Location: Informatikhörsaal
| 10:45 | Implicational Relevance Logic is 2-ExpTime-Complete (abstract) |
| 11:15 | An Implicit Characterization of the Polynomial-Time Decidable Sets by Cons-Free Rewriting (abstract) |
| 11:45 | Unification and Logarithmic Space (abstract) |
| 12:15 | Automated Complexity Analysis Based on Context-Sensitive Rewriting (abstract) |
| 12:45 | Automatic Evaluation of Context-Free Grammars (System Description) (abstract) |
10:45-12:05 Session 38E: Maximum Satisfiability (SAT)
Location: FH, Hörsaal 6
| 10:45 | Solving Sparse Instances of Max SAT via Width Reduction and Greedy Restriction (abstract) |
| 11:15 | Solving MaxSAT and #SAT on structured CNF formulas (abstract) |
| 11:45 | Cores in Core based MaxSat Algorithms: an Analysis (abstract) |
11:00-13:00 Session 39: Tutorial and invited talk (LC)
Location: MB, Prechtlsaal
| 11:00 | Tutorial on Stategic and Extensive Games 1 (abstract) |
| 12:00 | Applications of admissible computability (abstract) |
12:10-13:00 Session 40: Minimal Unsatisfiability (SAT)
Location: FH, Hörsaal 6
| 12:10 | On Computing Preferred MUSes and MCSes (abstract) |
| 12:40 | MUS Extraction using Clausal Proofs (abstract) |
13:00-14:30Lunch Break
14:30-16:00 Session 41A: Tutorial by Jasmin Fisher (CSL-LICS)
Chair:
Location: FH, Hörsaal 1
| 14:30 | Understanding Biology through Logic (abstract) |
14:30-16:00 Session 41B: Invited Talk (ITP)
Location: FH, Hörsaal 8
| 14:30 | From Operational Models to Information Theory - Side-Channels in pGCL with Isabelle (abstract) |
| 15:00 | Invited talk: Microcode Verification - Another Piece of the Microprocessor Verification Puzzle (abstract) |
14:30-16:00 Session 41C (RTA-TLCA)
Location: Informatikhörsaal
| 14:30 | Process types as a descriptive tool for distributed protocols (abstract) |
| 15:30 | Applicative May- and Should-Simulation in the Call-by-Value Lambda Calculus with AMB (abstract) |
14:30-15:50 Session 41D: Complexity and Reductions (SAT)
Location: FH, Hörsaal 6
| 14:30 | Fixed-parameter tractable reductions to SAT (abstract) |
| 15:00 | On Reducing Maximum Independent Set to Minimum Satisfiability (abstract) |
| 15:30 | Conditional Lower Bounds for Failed Literals and Related Techniques (abstract) |
14:30-16:00 Session 41E: Special session: Logic of Games and Rational Choice (LC)
Location: MB, Hörsaal 15
| 14:30 | The DNA of logic and games. (abstract) |
| 15:15 | Dependence and independence - a logical approach (abstract) |
14:30-16:00 Session 41F: Special session: Model Theory (LC)
Location: MB, Aufbaulabor
| 14:30 | Pregeometries and definable groups (abstract) |
| 15:15 | Quasiminimal structures and excellence (abstract) |
14:30-16:00 Session 41G: Special session: Recursion Theory (LC)
Location: MB, Seminarraum 212/232
| 14:30 | Uniform and non-uniform reducibilities of algebraic structures (abstract) |
| 15:15 | Randomness in the Weihrauch degrees (abstract) |
14:30-16:00 Session 41H: Special session: Perspectives on Induction (CSL-LICS and LC)
Location: MB, Prechtlsaal
| 14:30 | Inductive Proofs & the Knowledge They Represent (abstract) |
| 15:15 | Decidable languages for knowledge representation and inductive definitions: From Datalog to Datalog+/- (abstract) |
16:00-16:30Coffee Break
16:30-18:30 Session 42A: Computability (CSL-LICS)
Chair:
Location: FH, Hörsaal 1
| 16:30 | Turing Machines with Atoms, Constraint Satisfaction Problems, and Descriptive Complexity (abstract) |
| 17:00 | Beta Reduction is Invariant, Indeed (abstract) |
| 17:30 | On the Pigeonhole and Related Principles in Deep Inference and Monotone Systems (abstract) |
| 18:00 | Faster decision of first-order graph properties (abstract) |
16:30-18:30 Session 42B: Concurrency (CSL-LICS)
Chair:
Location: FH, Hörsaal 5
| 16:30 | Logic for Communicating Automata with Parameterized Topology (abstract) |
| 17:00 | Equilibria of Concurrent Games on Event Structures (abstract) |
| 17:30 | Compositional Verification of Termination-Preserving Refinement of Concurrent Programs (abstract) |
| 18:00 | Symmetry in Concurrent Games (abstract) |
16:30-18:00 Session 42C: Codatatypes (ITP)
Location: FH, Hörsaal 8
| 16:30 | Truly Modular (Co)datatypes for Isabelle/HOL (abstract) |
| 17:00 | Recursive Functions on Codatatypes via Domains and Topologies (abstract) |
| 17:30 | Experience Implementing a Performant Category-Theory Library in Coq (abstract) |
16:30-18:15 Session 42D (RTA-TLCA)
Location: Informatikhörsaal
| 16:30 | A Coinductive Confluence Proof for Infinitary Lambda-Calculus. (abstract) |
| 17:00 | Confluence by Critical Pair Analysis (abstract) |
| 17:30 | Proving Confluence of Term Rewriting Systems via Persistency and Decreasing Diagrams (abstract) |
| 18:00 | Conditional Confluence (System Description) (abstract) |
16:30-18:00 Session 42E: Tool Papers (SAT)
Location: FH, Hörsaal 6
| 16:30 | MPIDepQBF: Towards Parallel QBF Solving without Knowledge Sharing (abstract) |
| 16:50 | DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs (abstract) |
| 17:10 | Automatic Evaluation of Reductions between NP-complete Problems (abstract) |
| 17:30 | Open-WBO: a Modular MaxSAT Solver (abstract) |
16:30-18:30 Session 42F: Contributed talks A1 (LC)
Location: MB, Hörsaal 14
| 16:30 | Natural deduction for intuitionistic differential linear logic (abstract) |
| 16:50 | An outline of intuitionistic epistemic logic (abstract) |
| 17:10 | Some properties related to the existence property in intermediate predicate logics (abstract) |
| 17:30 | On Hallden complete modal logics determined by homogeneous frames (abstract) |
| 17:50 | A universal diagonal schema by fixed-points and Yablo’s paradox (abstract) |
| 18:10 | Canonical extensions and prime filter completions of poset expansions. (abstract) |
16:30-18:30 Session 42G: Contributed talks B1 (LC)
Location: MB, Hörsaal 15
| 16:30 | On the compactness theorem in many valued logics (abstract) |
| 16:50 | Formalizing vagueness as a doxastic, relational concept (abstract) |
| 17:10 | Two Formalisms for a Logic of Generalized Truth Values (abstract) |
| 17:30 | Characterising Logics through their Admissible Rules (abstract) |
| 17:50 | Models for the probabilistic sequent calculus (abstract) |
| 18:10 | Display-type calculi for non classical logics (abstract) |
16:30-18:30 Session 42H: Contributed talks C1 (LC)
Location: MB, Zeichensaal 15
| 16:30 | Complexity bounds for Multiagent Justification Logic (abstract) |
| 16:50 | The relation between the graphs structures and proof complexity of corresponding Tseitin graph tautologies (abstract) |
| 17:10 | The algorithmic complexity of decomposability in fragments of first-order logic (abstract) |
| 17:30 | Type equations and second order logic (abstract) |
| 17:50 | An intuitive semantics for {Full Intuitionistic Linear Logic} (abstract) |
| 18:10 | Argumentation Logic (abstract) |
16:30-18:30 Session 42I: Contributed talks D1 (LC)
Location: MB, Seminarraum 5
| 16:30 | On the existential interpretability of structures (abstract) |
| 16:50 | The isomorphism problem for computable projective planes (abstract) |
| 17:10 | Coding graphs into fields (abstract) |
| 17:30 | Uniformization in the hereditarily finite list superstructure over the real exponential field (abstract) |
| 17:50 | Dynamic logic on approximation spaces (abstract) |
| 18:10 | On limitwise monotonic reducibility of Σ^0_2-sets. (abstract) |
16:30-18:30 Session 42J: Contributed talks E1 (LC)
Location: MB, Seminarraum 2
| 16:30 | Relativized universal numberings (abstract) |
| 16:50 | Ideals without minimal numberings in the Rogers semilattice (abstract) |
| 17:10 | Computable numberings in Analytical Hierarchy (abstract) |
| 17:30 | Definability of 0' in the structure of $\omega$-enumeration degrees (abstract) |
| 17:50 | Embedding the omega-enumeration degrees into the Muchnik degrees generated by spectra of structures (abstract) |
| 18:10 | Limitwise monotonic sets of reals (abstract) |
16:30-18:30 Session 42K: Contributed talks F1 (LC)
Location: MB, Seminarraum 212/232
| 16:30 | An Intuitionistic Interpretation of Classical Implication (abstract) |
| 16:50 | Predicate Glivenko theorems and substructural aspects of negative translations (abstract) |
| 17:10 | Adding a Conditional to Kripke's Theory of Truth (abstract) |
| 17:30 | Constructive completeness and Joyal's theorem (abstract) |
| 17:50 | Algorithmic-algebraic canonicity for mu-calculi (abstract) |
| 18:10 | Proof-Theoretic Analysis of Brouwer's Argument of the Bar Induction (abstract) |
16:30-18:30 Session 42L: Contributed talks G1 (LC)
Location: MB, Seminarraum 3
| 16:30 | On Explicit-Implicit Reflection Principles. (abstract) |
| 16:50 | Ordinal Notations and Fundamental Sequences in Caucal Hierarchy (abstract) |
| 17:10 | The maximal order type of the trees with the gap-embeddability relation (abstract) |
| 17:30 | Computational reverse mathematics and foundational analysis (abstract) |
| 17:50 | Semantic completeness of first order theories in constructive reverse mathematics (abstract) |
| 18:10 | Reverse Mathematics, more explicitly (abstract) |
16:30-18:30 Session 42M: Contributed talks H1 (LC)
Location: MB, Seminarraum 4
| 16:30 | A computability approach to three hierarchies (abstract) |
| 16:50 | A generalization of Solovay's Sigma-construction with application to intermediate models (abstract) |
| 17:10 | A new lower bound for the length of the hierarchy of norms (abstract) |
| 17:30 | Unraveling $\Sigma^0_\alpha(\Pi^1_1)$-Determinacy (abstract) |
| 17:50 | Determinacy of Refinements to the Difference Hierarchy of Co-analytic sets (abstract) |
| 18:10 | On proof complexities of strong equal modal tautologies. (abstract) |
16:30-18:30 Session 42N: Contributed talks I1 (LC)
Location: MB, Seminarraum 6
| 16:30 | Reducts of simple (non-collapsed) Fraisse-Hrushovski constructions (abstract) |
| 16:50 | On Jonsson sets and some their properties. (abstract) |
| 17:10 | Ultraproduct construction of representative utility functions with infinite-dimensional domain (abstract) |
| 17:30 | An axiomatic approach to modelling of orders of magnitude (abstract) |
| 17:50 | Elementary numerosities and measures. (abstract) |
16:30-18:30 Session 42P: Contributed talks J1 (LC)
Location: MB, Seminarraum 7
| 16:30 | Differential Galois theory in the class of formally real fields. (abstract) |
| 16:50 | Around n-dependent fields (abstract) |
| 17:10 | Some remarks on $\aleph_0$-categorical weakly circularly minimal structures (abstract) |
| 17:30 | Uniqueness of limit models in metric abstract elementary classes under categoricity and some consequences in domination and orthogonality of Galois types (abstract) |
| 17:50 | Amalgamation, characterizing cardinals and locally finite Abstract Elementary Classes (abstract) |
| 18:10 | Computing the number of types of infinite tuples (abstract) |
18:00-18:30 Session 43: ITP business meeting (ITP)
Location: FH, Hörsaal 8
Tuesday, July 15th, 2014
View this program: with abstractssession overviewtalk overview
08:45-10:15 Session 44: FLoC Plenary Talk (joint session of 10 meetings)
Chair:
Location: FH, Hörsaal 1
| 08:45 | FLoC Plenary Talk: From Reachability to Temporal Specifications in Game Theory (abstract) |
Monday, July 14th, 2014
View this program: with abstractssession overviewtalk overview
20:00-21:30 Session 44: VSL Opening Reception (VSL)
Location: Rathaus
Tuesday, July 15th, 2014
View this program: with abstractssession overviewtalk overview
09:00-10:15 Session 45: Logic and games from cognitive, social, and abstract perspectives (1/2) (LG)
Location: MB, Hörsaal 12
| 09:00 | Ludics and interactive completeness (abstract) |
| 09:45 | Forward and backward induction in dynamic games: Distilling the axiomatic differences on common ground (abstract) |
09:15-10:15 Session 46: Invited talk (LC)
Location: MB, Prechtlsaal
| 09:15 | Definability, automorphisms and enumeration degrees (abstract) |
10:15-10:45Coffee Break
10:45-13:00 Session 47A: Automata (CSL-LICS)
Chair:
Location: FH, Hörsaal 1
| 10:45 | Zero-Reachability in Probabilistic Multi-Counter Automata (abstract) |
| 11:15 | Senescent Ground Tree Rewrite Systems (abstract) |
| 11:45 | Abstract Interpretation from Buchi Automata (abstract) |
| 12:15 | Separating Regular Languages with First-Order Logic (abstract) |
10:45-13:00 Session 47B: Concurrency and Games (CSL-LICS)
Chair:
Location: FH, Hörsaal 5
| 10:45 | Coinduction Up-To in a Fibrational Setting (abstract) |
| 11:15 | Deadlock and lock freedom in the linear pi-calculus (abstract) |
| 11:45 | Secure Equilibria in Weighted Games (abstract) |
| 12:15 | Infinite sequential games with real-valued payoffs (abstract) |
10:45-13:00 Session 47C (ITP)
Location: FH, Hörsaal 8
| 10:45 | A Formal Library for Elliptic Curves in the Coq Proof Assistant (abstract) |
| 11:15 | A Verified Generate-Test-Aggregate Coq Library for Parallel Programs Extraction (abstract) |
| 11:45 | Verified Efficient Implementation of Gabow's Strongly Connected Component Algorithm (abstract) |
| 12:15 | Cardinals in Isabelle/HOL (abstract) |
| 12:45 | HOL Constant Definitions Done Right (abstract) |
10:45-13:00 Session 47D (RTA-TLCA)
Location: Informatikhörsaal
| 10:45 | Ramsey Theorem as an intuitionistic property of well founded relations (abstract) |
| 11:15 | Termination of Cycle Rewriting (abstract) |
| 11:45 | First-Order Formative Rules (abstract) |
| 12:15 | Formalizing monotone algebras for certification of termination- and complexity proofs (abstract) |
| 12:45 | Nagoya Termination Tool (System Description) (abstract) |
10:45-13:00 Session 47E: Logic and games from cognitive, social, and abstract perspectives (2/2) (LG)
Location: MB, Hörsaal 12
| 10:45 | Signaling in independence-friendly logic (abstract) |
| 11:30 | Game Reductions (abstract) |
| 12:00 | Game Semantics from a Cognitive Modeling Standpoint (abstract) |
| 12:30 | Emulating Diffusion and Best Response Dynamics in Social Networks using Action Models (abstract) |
10:45-11:45 Session 47F: Proof Complexity I (SAT)
Location: FH, Hörsaal 6
| 10:45 | Long Proofs of (Seemingly) Simple Formulas (abstract) |
| 11:15 | Proof complexity and the Lovasz-Kneser Theorem (abstract) |
11:00-13:00 Session 48: Tutorial and Karp prize winner (LC)
Location: MB, Prechtlsaal
| 11:00 | Tutorial on Stategic and Extensive Games 2 (abstract) |
| 12:00 | Logic meets number theory in o-minimality (abstract) |
11:50-13:00 Session 49: Parallel and Incremental (Q)SAT (SAT)
Location: FH, Hörsaal 6
| 11:50 | Ultimately Incremental SAT (abstract) |
| 12:20 | Community Branching for Parallel Portfolio SAT Solvers (abstract) |
| 12:40 | Lazy clause exchange policy for parallel SAT solvers (abstract) |
13:00-14:30Lunch Break
14:30-16:00 Session 50A: Graphs and Logic (CSL-LICS)
Chair:
Location: FH, Hörsaal 1
| 14:30 | Two-Way Cost Automata and Cost Logics over Infinite Trees (abstract) |
| 15:00 | Logical Characterization of Weighted Pebble Walking Automata (abstract) |
| 15:30 | Achieving New Upper Bounds for the Hypergraph Duality Problem through Logic (abstract) |
14:30-16:00 Session 50B: Model Checking (CSL-LICS)
Chair:
Location: FH, Hörsaal 5
| 14:30 | Decomposition Theorems and Model-Checking for the Modal mu-calculus (abstract) |
| 15:00 | Logics with Counting and Equivalence (abstract) |
| 15:30 | Local Temporal Reasoning (abstract) |
14:30-16:00 Session 50C: Invited Talk (ITP)
Location: FH, Hörsaal 8
| 14:30 | Balancing lists: a proof pearl (abstract) |
| 15:00 | Invited talk: Are We There Yet? 20 Years of Industrial Theorem Proving with SPARK (abstract) |
14:30-16:00 Session 50D (RTA-TLCA)
Location: Informatikhörsaal
| 14:30 | A unified approach to Univalent Foundations and Homotopical Algebra (abstract) |
| 15:30 | Amortised Resource Analysis and Typed Polynomial Interpretations (abstract) |
14:30-16:15 Session 50E: Games for belief revision and non-classical logic (1/2) (LG)
Location: MB, Hörsaal 12
| 14:30 | Semantic games for Łukasiewicz logic (abstract) |
| 15:15 | Game Semantics for Conditional Logic (abstract) |
| 15:45 | Multi-Agent Dialogical Games for Modal Logic (abstract) |
14:30-15:30 Session 50F: Invited Talk I (SAT)
Location: FH, Hörsaal 6
| 14:30 | A (Biased) Proof Complexity Survey for SAT Practitioners (abstract) |
14:30-16:00 Session 50G: Special session: Logic of Games and Rational Choice (LC)
Location: MB, Hörsaal 15
| 14:30 | Elections and knowledge (abstract) |
| 15:15 | Nash equilibrium semantics for Independence-Friendly Logic (abstract) |
14:30-16:00 Session 50H: Special session: Recursion Theory (LC)
Location: MB, Seminarraum 212/232
| 14:30 | UD-randomness and the Turing degrees (abstract) |
| 15:15 | On finitely presented expansions of groups and algebras (abstract) |
14:30-16:00 Session 50I: Special session: Set Theory (LC)
Location: MB, Aufbaulabor
| 14:30 | Matrix iterations and Cichoń's diagram (abstract) |
| 15:15 | Regular cross-sections of Borel flows (abstract) |
14:30-16:00 Session 50J: Special Session: The Place of Logic in Computer Science Education (LC)
Location: MB, Prechtlsaal
| 14:30 | The place of logic in computer science education (abstract) |
15:30-16:00 Session 51: Proof Complexity II / 1 (SAT)
Location: FH, Hörsaal 6
| 15:30 | Unified characterisations of resolution hardness measures (abstract) |
16:00-16:30Coffee Break
16:30-17:30 Session 52A: Invited talk by Patrick Cousot (CSL-LICS)
Chair:
Location: FH, Hörsaal 1
| 16:30 | Abstract Interpretation: Past, Present and Future (abstract) |
16:30-18:00 Session 52B: User Interfaces (ITP)
Location: FH, Hörsaal 8
| 16:30 | An Isabelle Proof Method Language (abstract) |
| 17:00 | Asynchronous User Interaction and Tool Integration in Isabelle/PIDE (abstract) |
| 17:30 | Collaborative Interactive Theorem Proving with Clide (abstract) |
16:30-18:00 Session 52C (RTA-TLCA)
Location: Informatikhörsaal
| 16:30 | Self Types for Dependently Typed Lambda Encodings (abstract) |
| 17:00 | The Structural Theory of Pure Type Systems (abstract) |
| 17:30 | Unnesting of Copatterns (abstract) |
16:30-17:45 Session 52D: Games for belief revision and non-classical logic (2/2) (LG)
Location: MB, Hörsaal 12
| 16:30 | Non-characterizability in belief revision: an application of finite model theory (abstract) |
| 17:00 | Game Semantics for Some Non-Classical Logics (abstract) |
16:30-17:00 Session 52E: Proof Complexity II / 2 (SAT)
Location: FH, Hörsaal 6
| 16:30 | QBF Resolution Systems and their Proof Complexities (abstract) |
16:30-18:30 Session 52F: Contributed talks A2 (LC)
Location: MB, Hörsaal 14
| 16:30 | Modal logic of clocks: Modalizing a first-order theory of time to get a better understanding of relativity theories (abstract) |
| 16:50 | Towards a Conditional for The Liar and the Sorites. (abstract) |
| 17:10 | On graph calculus approach to modalities (abstract) |
| 17:30 | Complexity of generalized grading with inverse relations and intersection of relations (abstract) |
| 17:50 | Fuzzy Bsimulation for Standard Godel Modal Logic (abstract) |
| 18:10 | Hybrid extensions of S4 with the finite model property (abstract) |
16:30-18:30 Session 52G: Contributed talks B2 (LC)
Location: MB, Hörsaal 15
| 16:30 | Almost structurally complete consequence operations extending S4.3 (abstract) |
| 16:50 | Truth theory for logic of self-reference statements as a quaternion structure (abstract) |
| 17:10 | A Routley-Meyer semantics for Göodel 3-valued logic G3 (abstract) |
| 17:30 | Blocking the routes to triviality with depth relevance (abstract) |
16:30-18:30 Session 52H: Contributed talks C2 (LC)
Location: MB, Zeichensaal 15
| 16:30 | On the almost sure validities in the finite in some fragments of monadic second-order logic (abstract) |
| 16:50 | Completeness of second-order separation logic for program verification (abstract) |
| 17:10 | Infinite Games Specified by 2-Tape Automata (abstract) |
| 17:30 | Circuit lower bounds in bounded arithmetics (abstract) |
| 17:50 | Model theory of bounded arithmetic and complexity theory (abstract) |
| 18:10 | Weak Arithmetical Semantics for the Logic of Proofs (abstract) |
16:30-18:30 Session 52I: Contributed talks D2 (LC)
Location: MB, Seminarraum 5
| 16:30 | Boolean algebras and degrees of autostability relative to strong constructivizations (abstract) |
| 16:50 | The $ \Delta^{0}_{\alpha} $-dimension of computable structures (abstract) |
| 17:10 | On categoricity of scattered linear orders (abstract) |
| 17:30 | A DNC function that computes no effectively bi-immune set (abstract) |
| 17:50 | Integer-valued randomness and degrees (abstract) |
| 18:10 | Effective genericity and differentiable functions (abstract) |
16:30-18:30 Session 52J: Contributed talks E2 (LC)
Location: MB, Seminarraum 2
| 16:30 | On $\Sigma^0_2$-initial segments of computable linear orders (abstract) |
| 16:50 | A non-uniqueness theorem for jumps of principal ideals (abstract) |
| 17:10 | Every non-zero honest elementary degree has the cupping property (abstract) |
| 17:30 | Degree spectra of relations on a cone (abstract) |
| 17:50 | $\Delta_2^0$-spectra of linear orderings (abstract) |
| 18:10 | Degree spectra of structures under $\Sigma_n$-equivalence. (abstract) |
16:30-18:30 Session 52K: Contributed talks F2 (LC)
Location: MB, Seminarraum 212/232
| 16:30 | Effective results on the asymptotic behavior of nonexpansive iterations (abstract) |
| 16:50 | Pi_1 induction axioms vs Pi 1 induction rules (abstract) |
| 17:10 | Reverse mathematics of WQOs and Noetherian spaces (abstract) |
| 17:30 | A characterization for diagonalized--out objects (abstract) |
| 17:50 | Some applications of the Arithmetized Completeness Theorem to second-order arithmetic (abstract) |
| 18:10 | Some properties of Intuitionistic Set Theory with the principle UP. (abstract) |
16:30-18:30 Session 52L: Contributed talks G2 (LC)
Location: MB, Seminarraum 3
| 16:30 | The complexity of computably enumerable graphs (abstract) |
| 16:50 | The order dimensions of degree structures (abstract) |
| 17:10 | Computable numberings in Ershov hierarchy (abstract) |
| 17:30 | Davies-trees in infinite combinatorics (abstract) |
| 17:50 | A descriptive set theoretical axiomatization of the Mathias model. (abstract) |
| 18:10 | Restricting Martin's axiom to a ccc ground model (abstract) |
16:30-18:30 Session 52M: Contributed talks H2 (LC)
Location: MB, Seminarraum 4
| 16:30 | Elementary epimorphisms between models of set theory (abstract) |
| 16:50 | Generalized Ellentuck spaces and initial Tukey chains of non-p-points (abstract) |
| 17:10 | Co-analytic ideals on $\omega$ (abstract) |
| 17:30 | Budding Trees (abstract) |
| 17:50 | Finite Inseparability of Elementary Theories Based on Connection (abstract) |
16:30-18:30 Session 52N: Contributed talks I2 (LC)
Location: MB, Seminarraum 6
| 16:30 | On various strengthenings of the notion of indivisibility (abstract) |
| 16:50 | An ordinal rank characterising when Forth suffices (abstract) |
| 17:10 | Extreme amenability of precompact expansions of countably categorical structures (abstract) |
| 17:30 | Weak Beth definability property for finite variable fragments. (abstract) |
| 17:50 | Non-monotonic extensions of the weak Kleene clone with constants (abstract) |
| 18:10 | A sheaf model of randomness (abstract) |
16:30-18:30 Session 52P: Contributed talks J2 (LC)
Location: MB, Seminarraum 7
| 16:30 | A Defense of Information Economy Principle (abstract) |
| 16:50 | Prospects for a Naive Theory of Classes (abstract) |
| 17:10 | On the logical use of implicit contradictions (abstract) |
| 17:30 | Definable topological dynamics and real Lie groups (abstract) |
| 17:50 | Topologies on Polish structures (abstract) |
| 18:10 | Explosiveness, Model Existence, and Incompatible Paraconsistencies (abstract) |
17:00-18:00 Session 53: SAT Association General Assembly (SAT)
Location: FH, Hörsaal 6
18:00-19:00 Session 54: SIGLOG Meeting (FLoC and VSL)
Location: FH, Hörsaal 5
19:00-20:00 Session 55A: Annual meeting of the EACSL (CSL-LICS)
Location: FH, Hörsaal 1
Wednesday, July 16th, 2014
View this program: with abstractssession overviewtalk overview
10:45-13:00 Session 56A: Models and Expressiveness (CSL-LICS)
Chair:
Location: FH, Hörsaal 1
| 10:45 | Graph Logics with Rational Relations: The Role of Word Combinatorics (abstract) |
| 11:15 | Model Checking Existential Logic on Partially Ordered Sets (abstract) |
| 11:45 | Infinite-State Energy Games (abstract) |
| 12:15 | Weak MSO: Automata and Expressiveness Modulo Bisimilarity (abstract) |
Tuesday, July 15th, 2014
View this program: with abstractssession overviewtalk overview
19:00-20:00 Session 56A: VSL Public Lecture 1 (VSL)
Location: MB, Kuppelsaal
| 19:00 | VSL Public Lecture: Gödel in Vienna (abstract) |
Wednesday, July 16th, 2014
View this program: with abstractssession overviewtalk overview
10:45-13:00 Session 56B: Proofs and Verification (CSL-LICS)
Chair:
Location: FH, Hörsaal 5
| 10:45 | Axioms and Decidability for Type Isomorphism in the Presence of Sums (abstract) |
| 11:15 | A functional functional interpretation (abstract) |
| 11:45 | Symmetric Normalisation for Intuitionistic Logic (abstract) |
| 12:15 | Satisfiability Modulo Counting: A New Approach for Analyzing Privacy Properties (abstract) |
10:45-13:00 Session 56C: Mathematics (ITP)
Location: FH, Hörsaal 8
| 10:45 | A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3) (abstract) |
| 11:15 | A Coq Formalization of Finitely Presented Modules (abstract) |
| 11:45 | Formal Verification of Optical Quantum Flip Gate (abstract) |
| 12:15 | On the Formalization of Z-Transform in HOL (abstract) |
| 12:45 | Mechanical Certification of Loop Pipelining Transformations: A Preview (abstract) |
10:45-13:00 Session 56D (RTA-TLCA)
Location: Informatikhörsaal
| 10:45 | Cut Admissibility by Saturation (abstract) |
| 11:15 | Predicate Abstraction of Rewrite Theories (abstract) |
| 11:45 | All-Path Reachability Logic (abstract) |
| 12:15 | Construction of retractile proof structures (abstract) |
10:45-11:55 Session 56E: Applications (SAT)
Location: FH, Hörsaal 6
| 10:45 | A SAT Attack on the Erdos Discrepancy Conjecture (abstract) |
| 11:05 | Dominant Controllability Check Using QBF-Solver and Netlist Optimizer (abstract) |
| 11:35 | Fast DQBF Refutation (abstract) |
10:45-12:45 Session 56F: Invited Talk (Urquhart) and Tutorial (Marra) (LATD)
Location: MB, Festsaal
| 10:45 | Relevance Logic: Problems Open and Closed (abstract) |
| 11:45 | Tutorial 1/2: The more, the less, and the much more: An introduction to Lukasiewicz logic as a logic of vague propositions, and to its applications (abstract) |
11:00-13:00 Session 57: Tutorial and invited talk (LC)
Location: MB, Prechtlsaal
| 11:00 | Tutorial on Stategic and Extensive Games 3 (abstract) |
| 12:00 | The Birth of Semantic Entailment (abstract) |
08:45-10:15 Session 57: VSL Keynote Talk (VSL)
Chair:
Location: EI, EI 7 + EI 9, EI 10 + FH, Hörsaal 1
| 08:45 | VSL Keynote Talk: The theory and applications of o-minimal structures (abstract) |
10:15-10:45Coffee Break
12:00-13:00 Session 58: Structure (SAT)
Location: FH, Hörsaal 6
| 12:00 | Variable Dependencies and Q-Resolution (abstract) |
| 12:30 | Impact of Community Structure on SAT Solver Performance (abstract) |
13:00-14:30Lunch Break
14:30-16:00 Session 59A: Graphs and Logic (CSL-LICS)
Chair:
Location: FH, Hörsaal 1
| 14:30 | On Hanf-equivalence and the number of embeddings of small induced subgraphs (abstract) |
| 15:00 | One Hierarchy Spawns Another: Graph Deconstructions and the Complexity Classification of Conjunctive Queries (abstract) |
| 15:30 | The Tractability Frontier of Graph-Like First-Order Query Sets (abstract) |
14:30-16:00 Session 59B: Types and Specifications (CSL-LICS)
Chair:
Location: FH, Hörsaal 5
| 14:30 | System F with Coercion Constraints (abstract) |
| 15:00 | Anchored LTL Separation (abstract) |
| 15:30 | Probably Safe or Live (abstract) |
14:30-16:00 Session 59C: Invited Talk (ITP)
Location: FH, Hörsaal 8
| 14:30 | Showing invariance compositionally for a process algebra for network protocols (abstract) |
| 15:00 | Invited talk: Retrofitting Rigour (abstract) |
14:30-16:00 Session 59D (RTA-TLCA)
Location: Informatikhörsaal
| 14:30 | Concurrent Programming Languages and Methods for Semantic Analyses (abstract) |
| 15:30 | A Model of Countable Nondeterminism in Guarded Type Theory (abstract) |
14:30-15:30 Session 59E: Invited Talk II (SAT)
Location: FH, Hörsaal 6
| 14:30 | A Model-Constructing Satisfiability Calculus (abstract) |
14:30-16:00 Session 59G: Contributed Talks (LATD)
Location: MB, Festsaal
| 14:30 | Axiomatising a fuzzy modal logic over the standard product algebra (abstract) |
| 15:00 | Decidability of order-based modal logics (abstract) |
| 15:30 | Many-valued modal logic over residuated lattices via duality (abstract) |
14:30-16:00 Session 59H: Contributed Talks (LATD)
Location: MB, Hörsaal 15
| 14:30 | Semantic information and fuzziness (abstract) |
| 15:00 | Qualified Syllogisms with Fuzzy Predicates (abstract) |
| 15:30 | Connecting Fuzzy Sets and Pavelka's Fuzzy Logic (abstract) |
15:30-16:00 Session 60: Simplification and Solving I / 1 (SAT)
Location: FH, Hörsaal 6
| 15:30 | Efficient implementation of SLS solvers and new heuristics for k-SAT with long clauses (abstract) |
16:00-16:30Coffee Break
16:30-18:30 Session 61A: Guarded and Separation Logics (CSL-LICS)
Chair:
Location: FH, Hörsaal 1
| 16:30 | Effective Interpolation and Preservation in Guarded Logics (abstract) |
| 17:00 | Expressive Completeness of Separation Logic With Two Variables and No Separating Conjunction (abstract) |
| 17:30 | A Decision Procedure for Satisfiability in Separation Logic with Inductive Predicates (abstract) |
16:30-18:30 Session 61B: Proof Theory (CSL-LICS)
Chair:
Location: FH, Hörsaal 5
| 16:30 | Substitution, jumps, and algebraic effects (abstract) |
| 17:00 | No proof nets for MLL with units: Proof equivalence in MLL is PSPACE-complete (abstract) |
| 17:30 | Equality and Fixpoints in the Calculus of Structures (abstract) |
16:30-18:00 Session 61C: Automation (ITP)
Location: FH, Hörsaal 8
| 16:30 | A heuristic prover for real inequalities (abstract) |
| 17:00 | Unified Decision Procedures for Regular Expression Equivalence (abstract) |
| 17:30 | Verified Abstract Interpretation Techniques for Disassembling Low-level Self-modifying Code (abstract) |
16:30-18:00 Session 61D (RTA-TLCA)
Location: Informatikhörsaal
| 16:30 | Abstract datatypes for real numbers in type theory (abstract) |
| 17:00 | Local stores in string diagrams (abstract) |
| 17:30 | Preciseness of subtyping on intersection and union types (abstract) |
16:30-18:00 Session 61E: Simplification and Solving I / 2 (SAT)
Location: FH, Hörsaal 6
| 16:30 | Everything You Always Wanted to Know About Blocked Sets (But Were Afraid to Ask) (abstract) |
| 17:00 | Simplifying Pseudo-Boolean Constraints in Residual Number Systems (abstract) |
| 17:30 | Detecting cardinality constraints in CNF (abstract) |
16:30-18:00 Session 61F: Contributed Talks (LATD)
Location: MB, Festsaal
| 16:30 | Embedding partially ordered sets into distributive lattices (abstract) |
| 17:00 | Bitopological Duality and Three-valued Logic (abstract) |
| 17:30 | De Morgan logics with a notion of inconsistency (abstract) |
16:30-18:00 Session 61G: Contributed Talks (LATD)
Location: MB, Hörsaal 15
| 16:30 | Chaotic Fuzzy Liars, Degrees of Truth, and Fractal Images of Paradox (abstract) |
| 17:00 | Truth degrees in the interval [-1,1] for the librationist system $\pounds$. (abstract) |
| 17:30 | A semantic approach to conservativity (abstract) |
Thursday, July 17th, 2014
View this program: with abstractssession overviewtalk overview
08:45-10:15 Session 62A: FLoC Panel (joint session of 10 meetings)
Chair:
Location: FH, Hörsaal 1
| 08:45 | FLoC Panel: Publication Models in Computing Research: Is a Change Needed? Are We Ready for a Change? (abstract) |
08:45-10:15 Session 62B: Non-Termination (WST)
Location: FH, Seminarraum 101B
| 08:45 | Non-termination of Dalvik bytecode via compilation to CLP (abstract) |
| 09:15 | Geometric Series as Nontermination Arguments for Linear Lasso Programs (abstract) |
| 09:45 | Non-termination using Regular Languages (abstract) |
08:45-10:15 Session 62C: Invited Talk I (CICLOPS-WLPE)
Chair:
Location: FH, Hörsaal 7
| 08:45 | Proofs for Optimality of Sorting Networks by Logic Programming (abstract) |
| 09:45 | Discussion (abstract) |
08:45-10:15 Session 62D: Contributed Talks (LATD)
Location: MB, Festsaal
| 08:45 | Undecidability of consequence relation in Full Non-associative Lambek Calculus (abstract) |
| 09:15 | Canonical formulas for k-potent residuated lattices (abstract) |
| 09:45 | On satisfiability of terms in FLew-algebras (abstract) |
08:45-10:15 Session 62E: Contributed Talks (LATD)
Location: MB, Hörsaal 15
| 08:45 | Five-valued LTL for Runtime Verification (abstract) |
| 09:15 | A method for generalizing finite automata arising from Stone-like dualities (abstract) |
| 09:45 | An application of distance-based approximate reasoning for diagnostic questionnaires in healthcare (abstract) |
08:45-10:15 Session 62F: Technical session (EC2)
Location: FH, Seminarraum 101C
| 08:45 | Atomicity Refinement for Verified Compilation (abstract) |
| 09:45 | Concolic Testing of Concurrent Programs (abstract) |
08:45-10:15 Session 62G: Invited Talk & Welcome (PLP)
Chair:
Location: FH, Seminarraum 134
| 08:45 | Welcome (abstract) |
| 08:55 | First-order representations for integer programming (abstract) |
| 09:50 | PageRank, ProPPR and Stochastic Logic Programs (abstract) |
08:45-10:15 Session 62H (VEMDP)
Location: FH, Seminarraum 136
| 08:45 | Opening remarks (abstract) |
| 09:00 | Computational design of DNA strand displacement systems (abstract) |
| 09:50 | A domain-level DNA strand displacement reaction enumerator allowing arbitrary non-pseudoknotted secondary structures (abstract) |
08:45-10:15 Session 62I: Contributed Talks: Uncertainty 1 (NMR)
Location: EI, EI 9
| 08:45 | Nonmonotonic Reasoning as a Temporal Activity (abstract) |
| 09:15 | Probabilistic Inductive Logic Programming based on Answer Set Programming (abstract) |
| 09:45 | A Plausibility Semantics for Abstract Argumentation Frameworks (abstract) |
08:45-10:15 Session 62J: Summer School on Computational Logic: Constraint Logic Programming I (ICLP)
Location: Seminarraum 1/3 OPG
| 08:45 | Summer School Opening (abstract) |
| 08:50 | Constraint Logic Programming I (abstract) |
08:50-10:15 Session 63: Technical Session (LFMTP)
Chair:
Location: FH, Zeichensaal 1
| 08:50 | Welcome Remarks (abstract) |
| 09:00 | Proof-Theoretic Foundations of Indexing in Logic Programming (abstract) |
| 09:25 | Hybrid Extensions in a Logical Framework (abstract) |
| 09:50 | Variable Arity for LF (abstract) |
Wednesday, July 16th, 2014
View this program: with abstractssession overviewtalk overview
19:00-21:30 Session 64: VSL Banquet 1 (VSL)
Location: Schönbrunn
Thursday, July 17th, 2014
View this program: with abstractssession overviewtalk overview
09:00-10:15 Session 64A: Opening + Invited Talk 1 (HCVS)
Location: FH, Seminarraum 134A
| 09:00 | Invited talk: Proof and Refutations for Horn-clause Encodings of Reachability Problems (abstract) |
09:00-10:15 Session 64B (REORDER)
Location: FH, Hörsaal 4
| 09:00 | Digging deeper: mole looking for potential weak memory related bugs in Debian (abstract) |
09:00-10:15 Session 64C: Opening + Invited Talk by Viorica Sofronie-Stokkermans (PAS)
Location: FH, Seminarraum 138A
| 09:00 | Hierarchical reasoning and quantifier elimination for the verification of parametric reactive and hybrid systems (abstract) |
09:00-10:15 Session 64D: Invited talk: Laure Vieu (NLCS)
Chair:
Location: FH, CAD 2
| 09:00 | TBA (abstract) |
09:00-10:15 Session 64E: Welcome and Invited Talk (SMT)
Chair:
Location: FH, Seminarraum 104
| 09:00 | Welcome (abstract) |
| 09:15 | SMT: Where do we go from here? (abstract) |
09:15-10:15 Session 65A: NSV Invited Talk: Jean-Michel Muller (NSV)
Chair:
Location: FH, Hörsaal 2
| 09:15 | Getting tight error bounds in floating-point arithmetic: illustration with complex functions, and the real x^n function (abstract) |
09:15-10:15 Session 65B: Invited talk (LC)
Location: MB, Prechtlsaal
| 09:15 | Definable cardinals just beyond R / Q (abstract) |
09:15-10:15 Session 65C: UITP Invited Talk 1 (Geoff Sutcliffe: "TPTP Process Instruction Language") (UITP)
Location: FH, Seminarraum 107
| 09:15 | The TPTP Process Instruction Language, with Applications (abstract) |
09:15-10:15 Session 65D: Invited Talk by Martín Escardó: Excluded Middle Considered as a Mathematical Problem (PSC)
Chair:
Location: FH, CAD 1
| 09:15 | Excluded Middle Considered as a Mathematical Problem (Invited Talk) (abstract) |
10:15-10:45Coffee Break
10:45-13:00 Session 66AA: Model Theory and Complexity (CSL-LICS)
Chair:
Location: FH, Hörsaal 1
| 10:45 | Hyper-Ackermannian Bounds for Pushdown Vector Addition Systems (abstract) |
| 11:15 | Preservation and Decomposition Theorems for Bounded Degree Structures (abstract) |
| 11:45 | On the Succinctness of Query Rewriting over OWL 2 QL Ontologies with Bounded Chase (abstract) |
| 12:15 | MSO Queries on Trees: Enumerating Answers under Updates (abstract) |
10:45-13:00 Session 66AB: Semantics and Verification (CSL-LICS)
Chair:
Location: FH, Hörsaal 5
| 10:45 | Transition systems over games (abstract) |
| 11:15 | Memoryful Geometry of Interaction: From Coalgebraic Components to Algebraic Effects (abstract) |
| 11:45 | Compositional Higher-Order Model Checking via Omega-Regular Games over Boehm Trees (abstract) |
| 12:15 | On the Hoare Theory of Monadic Recursion Schemes (abstract) |
10:45-13:00 Session 66AC (ITP)
Location: FH, Hörsaal 8
| 10:45 | Formalized, effective domain theory in Coq (abstract) |
| 11:15 | Completeness and Decidability Results for CTL in Coq (abstract) |
| 11:45 | Universe Polymorphism in Coq (abstract) |
| 12:15 | Compositional Computational Reflection (abstract) |
| 12:45 | Formal C semantics: CompCert and the C standard (abstract) |
10:45-12:45 Session 66AD (RTA-TLCA)
Location: Informatikhörsaal
| 10:45 | Tree Automata with Height Constraints between Brothers (abstract) |
| 11:15 | Reduction System for Extensional Lambda-mu Calculus (abstract) |
| 11:45 | Proof terms for infinitary rewriting (abstract) |
| 12:15 | Near semi-rings and lambda calculus (abstract) |
10:45-13:00 Session 66AE: Summer School on Computational Logic: Constraint Logic Programming II (ICLP)
Location: Seminarraum 1/3 OPG
| 10:45 | Constraint Logic Programming II (abstract) |
10:45-11:15 Session 66AF: Simplification and Solving II (SAT)
Location: FH, Hörsaal 6
| 10:45 | Minimal-Model-Guided Approaches to Solving Polynomial Constraints and Extensions (abstract) |
10:45-12:45 Session 66AG: NSV Contributed Talks: Formal Methods in Numerical Programs (NSV)
Chair:
Location: FH, Hörsaal 2
| 10:45 | Theorem-Proving Analysis of Digital Control Logic Interacting with Continuous Dynamics (abstract) |
| 11:15 | Transformation of a PID Controller for Numerical Accuracy (abstract) |
| 11:45 | Policy iteration in finite templates domain (abstract) |
10:45-13:00 Session 66AH: UITP Contributed Talks (Proof Strategies, HCI Focus Groups, Proof Visualization, Term Rewriting) (UITP)
Location: FH, Seminarraum 107
| 10:45 | Tinker, tailor, solver, proof (abstract) |
| 11:15 | How to Put Usability into Focus: Using Focus Groups to Evaluate the Usability of Interactive Theorem Provers (abstract) |
| 11:45 | Advanced Proof Viewing in PROOFTOOL (abstract) |
| 12:15 | The Certification Problem Format (abstract) |
10:45-13:00 Session 66AI: Invited Talk and Imperative Programs (WST)
Location: FH, Seminarraum 101B
| 10:45 | Termination of Biological Programs (abstract) |
| 11:45 | On Improving Termination Preservability of Transformations from Procedural Programs into Rewrite Systems by Using Loop Invariants (abstract) |
| 12:15 | Automatic Termination Analysis for GPU Kernels (abstract) |
| 12:45 | Discussion (abstract) |
10:45-11:35 Session 66AJ: Invited Talk (LFMTP)
Chair:
Location: FH, Zeichensaal 1
| 10:45 | Session Types Meet Separation Logic (abstract) |
10:45-13:00 Session 66AK: Program Transformation (CICLOPS-WLPE)
Chair:
Location: FH, Hörsaal 7
| 10:45 | Refining definitions with unknown opens using XSB for IDP3 (abstract) |
| 11:15 | A Lambda Prolog Based Animation of Twelf Specifications (abstract) |
| 11:45 | A System for Embedding Global Constraints into SAT (abstract) |
| 12:15 | Towards Pre-Indexed Terms (abstract) |
| 12:45 | Discussion (abstract) |
10:45-13:00 Session 66AL: Technical Session (HCVS)
Location: FH, Seminarraum 134A
| 10:45 | Please consult the program at http://vsl2014.at/hcvs (abstract) |
10:45-12:45 Session 66AM: Technical Session (EC2 and REORDER)
Location: FH, Hörsaal 4
| 10:45 | Reordering and Verification in the Linux Kernel (abstract) |
| 11:45 | Reasoning about the C/C++ Weak Memory Model (abstract) |
10:45-12:30 Session 66AN: Automated Debugging (PAS)
Location: FH, Seminarraum 138A
| 10:45 | An Attempt to Formalize Popper's Logic of Scientific Discovery (abstract) |
| 11:30 | A Model Theory for R-calculus without Cut (abstract) |
| 12:00 | RCK: A Software Toolkit for R-calculus (abstract) |
10:45-13:00 Session 66AP: Analysis: Understanding and Explanation (VSTTE)
Location: FH, Zeichensaal 3
| 10:45 | Finding Security Vulnerabilities in a Network Protocol using Parameterized Systems (abstract) |
| 11:45 | A Model for Capturing and Replaying Proof Strategies (abstract) |
| 12:10 | A Verification Condition Visualizer (abstract) |
| 12:35 | What Gives? A Hybrid Algorithm for Error Explanation (abstract) |
10:45-13:00 Session 66AQ: Invited Talk, Contributed Talks, and Poster Announcements (DL)
Location: EI, EI 7
| 10:45 | Invited Talk: New Perspectives on Query Reformulation (abstract) |
| 11:45 | Acyclic Query Answering under Guarded Disjunctive Existential Rules and Consequences to DLs (abstract) |
| 12:10 | Complexities of Nominal Schemas (abstract) |
| 12:35 | Comparing the Expressiveness of Description Logics (abstract) |
| 12:38 | An Empirical Investigation of Difficulty of Subsets of Description Logic Ontologies (abstract) |
| 12:41 | Predicting OWL Reasoners: Locally or Globally? (abstract) |
| 12:44 | Bridging the Gap between Tableau and Consequence-Based Reasoning (abstract) |
| 12:47 | Towards a Description Logic for Program Analysis: Extending ALCQIO with Reachability (abstract) |
| 12:50 | How to Best Nest Regular Path Queries (abstract) |
| 12:53 | Typed Higher-Order Variant of SROIQ - Why Not? (abstract) |
| 12:56 | Practical query answering over Hi (DL-LiteR) knowledge bases (abstract) |
10:45-12:45 Session 66AR: Contributed talks to NLCS (NLCS)
Chair:
Location: FH, CAD 2
| 10:45 | How to do things with types (abstract) |
| 11:15 | Mereological Comparatives in Delineation Semantics (abstract) |
| 11:45 | Proof-Theoretic Semantics for intensional transitive verbs (abstract) |
| 12:15 | Grice, Hoare and Nash: some comments on conversational implicature (abstract) |
10:45-12:45 Session 66AS: Invited Talk (Miller) and Tutorial (Marra) (LATD)
Location: MB, Festsaal
| 10:45 | Combining Intuitionistic and Classical Logic: a proof system and semantics (abstract) |
| 11:45 | Tutorial 2/2: The more, the less, and the much more: An introduction to Lukasiewicz logic as a logic of vague propositions, and to its applications (abstract) |
10:45-13:00 Session 66AT: Program Analysis and Sets (SMT)
Chair:
Location: FH, Seminarraum 104
| 10:45 | Speeding Up SMT-Based Quantitative Program Analysis (abstract) |
| 11:15 | Multi-solver Support in Symbolic Execution (abstract) |
| 11:45 | Protocol log analysis with constraint programming (abstract) |
| 12:15 | Reasoning About Set Comprehensions (abstract) |
10:45-12:15 Session 66AU: Contributed Talks: Completeness and Computation (PSC)
Chair:
Location: FH, CAD 1
| 10:45 | Constructive completeness and exploding models (abstract) |
| 11:30 | Computing with Gödel’s completeness theorem (abstract) |
10:45-13:00 Session 66AV: Invited Talk by Orna Grumberg and Regular Talks (iPRA)
Chair:
Location: FH, Seminarraum 101A
| 10:45 | SAT-Based Model Checking with Interpolation (abstract) |
| 12:00 | Interpolants in Two-Player Games (abstract) |
| 12:30 | Fault Localization using Interpolation (abstract) |
10:45-11:00 Session 66AW: Opening (PCCR)
Location: FH, Hörsaal 3
10:45-13:00 Session 66AX: Algorithms & Semantics (PLP)
Chair:
Location: FH, Seminarraum 134
| 10:45 | Prefix and infix probability computation in PRISM (abstract) |
| 11:15 | Compiling Probabilistic Logic Programs into Sentential Decision Diagrams (abstract) |
| 11:45 | cProbLog: Restricting the Possible Worlds of Probabilistic Logic Programs (abstract) |
| 12:15 | Approximated Probabilistic Answer Set Programming (abstract) |
10:45-13:00 Session 66AY (VEMDP)
Location: FH, Seminarraum 136
| 10:45 | Molecular computers for molecular robots as hybrid systems (abstract) |
| 11:40 | DNA-based circuits in well-mixed and spatially organized systems (abstract) |
| 12:10 | Verifying Polymer Reaction Networks using Bisimulation (abstract) |
| 12:35 | Modeling and Analysis of Genetic Boolean Gates Using the Infobiotics Workbench (abstract) |
10:45-13:00 Session 66AZ: Opening and Contributed talks (VPT)
Location: FH, Dissertantenraum E104
| 10:45 | Verification of Multi-Party Ping-Pong Protocols via Program Transformation (abstract) |
| 11:30 | Program Verification using Constraint Handling Rules and Array Constraint Generalizations (abstract) |
| 12:15 | A Note on Program Specialization. What Syntactical Properties of Residual Programs Can Reveal? (abstract) |
10:45-12:15 Session 66BA: Contributed Talks: Declarative Programming 1 (NMR)
Location: EI, EI 9
| 10:45 | An Approach to Forgetting in Disjunctive Logic Programs that Preserves Strong Equivalence (abstract) |
| 11:15 | Three Semantics for Modular Systems (abstract) |
| 11:45 | Generalising Modular Logic Programs (abstract) |
10:50-12:10 Session 67: Propositional Satisfiability (RCRA)
Location: MB, Hörsaal 12
| 10:50 | Optimal Neighborhood Preserving Visualization by Maximum Satisfiability (abstract) |
| 11:20 | Maximal Falsifiability: Definitions, Algorithms, and Applications (abstract) |
| 11:50 | Latin Squares with Graph Properties (abstract) |
11:00-13:00 Session 68A: Tutorial and invited talk (LC)
Location: MB, Prechtlsaal
| 11:00 | Tutorial on classical realizability and forcing 1 (abstract) |
| 12:00 | Cardinal invariants and template iterations (abstract) |
11:00-12:00 Session 68B: Invited talk (PCCR)
Location: FH, Hörsaal 3
| 11:00 | Fixed-Parameter Algorithms for Reasoning Problems in NP and Beyond (abstract) |
11:15-12:45 Session 69: Analysis (SAT)
Location: FH, Hörsaal 6
| 11:15 | An Ising Model inspired Extension of the Product-based MP Framework for SAT (abstract) |
| 11:45 | Approximating highly satisfiable random 2-SAT (abstract) |
| 12:15 | Hypergraph Acyclicity and Propositional Model Counting (abstract) |
11:45-13:00 Session 70: Technical Session (LFMTP)
Chair:
Location: FH, Zeichensaal 1
| 11:45 | Internal Adequacy of Bookkeeping in Coq (abstract) |
| 12:10 | A Generic Approach to Proofs about Substitution (abstract) |
| 12:35 | A Framework for Implementing Logical Frameworks (abstract) |
12:00-13:00 Session 71: Contributed talks (PCCR)
Location: FH, Hörsaal 3
| 12:00 | A Parameterized Complexity Analysis of Generalized CP-Nets (abstract) |
| 12:30 | Backdoors to Planning (abstract) |
12:10-13:00 Session 72: Answer Set Programming (RCRA)
Location: MB, Hörsaal 12
| 12:10 | Efficient Computation of the Well-Founded Semantics over Big Data (abstract) |
| 12:40 | Declarative Specification of Benchmark Sessions via ASP (abstract) |
12:15-13:00 Session 73: Contributed Talks: Systems 1 (NMR)
Location: EI, EI 9
| 12:15 | The Multi-engine ASP Solver ME-ASP: Progress Report (abstract) |
| 12:37 | Preliminary Report on WASP 2 (abstract) |
13:00-14:30Lunch Break
14:00-16:00 Session 74 (REORDER)
Location: FH, Hörsaal 4
| 14:00 | Reasoning about Fences in C11 Weak Memory Model (abstract) |
| 14:30 | Robustness against Power is PSpace-complete (abstract) |
| 15:00 | Simulating, exploring and formalising the OpenCL 2.0 memory model (abstract) |
| 15:30 | Testing GPU Memory Models (abstract) |
14:30-16:00 Session 75AA: Models and Games (CSL-LICS)
Chair:
Location: FH, Hörsaal 1
| 14:30 | Decidability of Weak Logics with Deterministic Transitive Closure (abstract) |
| 15:00 | The Complexity of Admissibility in Omega-Regular Games (abstract) |
| 15:30 | Pattern Logics and Auxiliary Relations (abstract) |
14:30-16:00 Session 75AB: Programming Language Semantics (CSL-LICS)
Chair:
Location: FH, Hörsaal 5
| 14:30 | KAT + B! (abstract) |
| 15:00 | On the characterization of models of H* (abstract) |
| 15:30 | Functional Reactive Types (abstract) |
14:30-16:00 Session 75AC (ITP)
Location: FH, Hörsaal 8
| 14:30 | A New and Formalized Proof of Abstract Completion (abstract) |
| 15:00 | Hypermap Specification and Certified Linked Implementation using Orbits (abstract) |
| 15:30 | Implicational Rewriting Tactics in HOL (abstract) |
14:30-16:00 Session 75AD: RTA/TLCA business meeting (RTA-TLCA)
Location: Informatikhörsaal
14:30-16:00 Session 75AE: Summer School on Computational Logic: Horn Clauses and Verification I (ICLP)
Location: Seminarraum 1/3 OPG
| 14:30 | Horn Clauses and Verification I (abstract) |
14:30-16:00 Session 75AF: Report on Competitions (SAT)
Location: FH, Hörsaal 6
14:30-16:00 Session 75AG: NSV Contributed Talks: Certified Numerical Computation (NSV)
Chair:
Location: FH, Hörsaal 2
| 14:30 | Certifying Square Root and Division Elimination (abstract) |
| 15:00 | Computational complexity of iterated maps on points and sets (abstract) |
| 15:30 | SetBased Decorated Intervals (abstract) |
14:30-15:30 Session 75AH: UITP Invited Talk 2 (Enrico Tassi: "Asynchronous Processing in Coq") (UITP)
Location: FH, Seminarraum 107
| 14:30 | Asynchronous Processing of Formal Documents in Coq (abstract) |
14:30-16:00 Session 75AI: Ranking Functions and Complexity (WST)
Location: FH, Seminarraum 101B
| 14:30 | To Infinity... and Beyond! (abstract) |
| 15:00 | Real-world loops are easy to predict : a case study (abstract) |
| 15:30 | Type Introduction for Runtime Complexity Analysis (abstract) |
14:30-15:20 Session 75AJ: Invited Talk (LFMTP)
Chair:
Location: FH, Zeichensaal 1
| 14:30 | A Framework for the Verified Transformation of Functional Programs (abstract) |
14:30-16:00 Session 75AK: Prolog Extensions (CICLOPS-WLPE)
Chair:
Location: FH, Hörsaal 7
| 14:30 | Extending the Finite Domain Solver of GNU Prolog (abstract) |
| 15:00 | SWI-Prolog version 7 extensions (abstract) |
| 15:30 | A Portable Prolog Predicate for Printing Rational Terms (abstract) |
14:30-15:30 Session 75AL: Invited Talk (HCVS and VPT)
Location: FH, Seminarraum 134A
| 14:30 | Invited talk: Towards Constraint-Solving over Higher-Order Unbounded Datatypes using Formal Methods Tools (abstract) |
14:30-16:00 Session 75AM: Invited Talk by Bruno Buchberger (PAS)
Location: FH, Seminarraum 138A
| 14:30 | The Theorema Approach to Mathematics (abstract) |
| 15:00 | A note on real quantifier elimination by virtual term substitution of unbounded degree (abstract) |
14:30-16:00 Session 75AN: Verification Frameworks and Applications (VSTTE)
Location: FH, Zeichensaal 3
| 14:30 | Efficient Refinement Checking in VCC (abstract) |
| 14:55 | Formalizing Semantics with an Automatic Program Verifier (abstract) |
| 15:20 | The KeY Platform for Verification and Analysis of Java Programs (abstract) |
| 15:45 | Using Promela in a Fully Verified Executable LTL Model Checker (SHORT) (abstract) |
14:30-16:00 Session 75AP: Contributed Talks and Poster Announcements (DL)
Location: EI, EI 7
| 14:30 | Is Your Ontology as Hard as You Think? Rewriting Ontologies into Simpler DLs (abstract) |
| 14:55 | Abstraction Refinement for Ontology Materialization (abstract) |
| 15:20 | Shape and Content: Incorporating Domain Knowledge into Shape Analysis (abstract) |
| 15:45 | An ABox Revision Algorithm for the Description Logic EL_\bot (abstract) |
| 15:48 | Instance-driven TBox Revision in DL-Lite (abstract) |
| 15:51 | Rational Elimination of DL-Lite TBox Axioms (abstract) |
| 15:54 | Rational closure in SHIQ (abstract) |
| 15:57 | DIP: A Defeasible-Inference Platform for OWL Ontologies (abstract) |
14:30-16:00 Session 75AQ: Invited talk: Anne Abeille, then a talk contributed to NLCS (NLCS)
Chair:
Location: FH, CAD 2
| 14:30 | TBA (abstract) |
| 15:30 | Computing Italian clitic and relative clauses with tupled pregroups (abstract) |
14:30-16:00 Session 75AR: Contributed Talks (LATD)
Location: MB, Festsaal
| 14:30 | Embeddings into BiFL-algebras and conservativity (abstract) |
| 15:00 | The lattice of varieties generated by small residuated lattices (abstract) |
| 15:30 | Quasivarieties of MV-algebras and structurally complete Lukasiewicz logics (abstract) |
14:30-16:00 Session 75AS: Contributed Talks (LATD)
Location: MB, Hörsaal 15
| 14:30 | Boolean-valued judgment aggregation (abstract) |
| 15:00 | Constructing many-valued logical functions with small influence of their variables (abstract) |
| 15:30 | Coupling games for Lukasiewicz logic (abstract) |
14:30-16:00 Session 75AT: Technical session (EC2)
Location: FH, Seminarraum 101C
| 14:30 | Abstractions for Relaxed Memory Models (abstract) |
| 15:30 | Group Communication Patterns for High Performance Computing in Scala (abstract) |
14:30-16:00 Session 75AU: Arrays and Polymorphism (SMT)
Chair:
Location: FH, Seminarraum 104
| 14:30 | Weakly Equivalent Arrays (abstract) |
| 15:00 | Decision Procedures for Flat Array Properties (abstract) |
| 15:30 | Extending SMT-LIB v2 with lambda-terms and polymorphism (abstract) |
14:30-16:00 Session 75AV: Contributed Talks: Calculus and Termination (PSC)
Chair:
Location: FH, CAD 1
| 14:30 | A typed lambda-calculus with call-by-name and call-by-value iteration (abstract) |
| 15:15 | Effective Bounds on the Podelski-Rybalchenko Termination Theorem (abstract) |
14:30-16:00 Session 75AW: Invited Talk by Pavel Pudlak, Discussions (iPRA)
Chair:
Location: FH, Seminarraum 101A
| 14:30 | Feasible Interpolation in Proof Systems based on Integer Linear Programming (abstract) |
| 15:45 | Discussions (abstract) |
14:30-15:00 Session 75AX: Contributed talk (PCCR)
Location: FH, Hörsaal 3
| 14:30 | Intuitionistic modal logics: efficient fragments and parameterized complexity (abstract) |
14:30-16:00 Session 75AY: Applications & Implementation (PLP)
Chair:
Location: FH, Seminarraum 134
| 14:30 | Exploring probabilistic grammars of symbolic music using PRISM (abstract) |
| 15:00 | An OpenCL implementation of a forward sampling algorithm for CP-logic (abstract) |
| 15:30 | Lifted Inference for Probabilistic Logic Programs (abstract) |
14:30-16:00 Session 75AZ (VEMDP)
Location: FH, Seminarraum 136
| 14:30 | Morphisms of reaction networks that couple structure to function (abstract) |
| 15:20 | Verifying CRN Implementations: A Pathway Decomposition Approach (abstract) |
| 15:45 | Lightning talks for posters/demos (abstract) |
14:30-16:00 Session 75BA: Planning & Scheduling (RCRA)
Location: MB, Hörsaal 12
| 14:30 | A Systematic Analysis of Levels of Integration between High-Level Task Planning and Low-Level Feasibility Checks (abstract) |
| 15:00 | A Discrete Differential Evolution Algorithm for the Total Flowtime Flowshop Scheduling Problem (abstract) |
14:30-15:30 Session 75BB: Invited Talk (NMR)
Location: EI, EI 9
| 14:30 | Four Floors for the Theory of Theory Change (abstract) |
15:00-16:00 Session 76A: Invited talk (LC)
Location: MB, Prechtlsaal
| 15:00 | Generalizations of Hilbert's Tenth Problem (abstract) |
15:00-16:00 Session 76B: Open problems (PCCR)
Location: FH, Hörsaal 3
15:20-15:45 Session 77: Technical Session (LFMTP)
Chair:
Location: FH, Zeichensaal 1
| 15:20 | Automatically Deriving Schematic Theorems for Dynamic Contexts (abstract) |
15:30-16:00 Session 78A: UITP Contributed Talks - (Coq) (UITP)
Location: FH, Seminarraum 107
| 15:30 | PIDE for Asynchronous Interaction with Coq (abstract) |
15:30-16:00 Session 78B: Contributed Talk: Declarative Programming 2 (NMR)
Location: EI, EI 9
| 15:30 | On Strong and Default Negation in Logic Program Updates (abstract) |
15:30-16:00 Session 78C: Technical Session (HCVS)
Location: FH, Seminarraum 134A
| 15:30 | Please consult the program at http://vsl2014.at/hcvs (abstract) |
16:00-16:50 Session 79: Poster Session (with coffee break) (DL)
Location: EI, Foyer
16:00-16:30Coffee Break
16:30-19:00 Session 79A: VSL Joint Award Ceremony 1 (VSL)
Chair:
Location: MB, Kuppelsaal
| 16:30 | Foundations and Technology Competitions Award Ceremony (abstract) |
| 17:30 | FLoC Olympic Games Award Ceremony 1 (abstract) |
| 18:15 | FLoC Closing Week 1 (abstract) |
16:30-18:00 Session 80A: NSV Invited Talk: Sumit Kumar Jha (NSV)
Chair:
Location: FH, Hörsaal 2
| 16:30 | Verifying Parameterized Software Models in Computational Data Science against Behavioral Specifications (abstract) |
16:30-18:00 Session 80B: UITP Contributed Talks - (Isabelle, IDE, Equational Reasoning) (UITP)
Location: FH, Seminarraum 107
| 16:30 | System description: Isabelle/jEdit in 2014 (abstract) |
| 17:00 | A Logic-Independent IDE (abstract) |
| 17:30 | UTP2: Higher-Order Equational Reasoning by Pointing (abstract) |
16:30-18:00 Session 80C: New Frontiers (WST)
Location: FH, Seminarraum 101B
| 16:30 | Ordering Networks (abstract) |
| 17:00 | Discussion (abstract) |
16:30-17:20 Session 80D: Invited Talk (LFMTP)
Chair:
Location: FH, Zeichensaal 1
| 16:30 | Idris: Implementing a Dependently Typed Programming Language (abstract) |
16:30-18:00 Session 80E: Technical Session + Discussion (HCVS)
Location: FH, Seminarraum 134A
| 16:30 | Please consult the program at http://vsl2014.at/hcvs (abstract) |
16:30-18:30 Session 80G: Program Analysis (PAS)
Location: FH, Seminarraum 138A
| 16:30 | Successfully Coping with Scalability of Symbolic Analysis in Timing Analysis (abstract) |
| 17:00 | Confluence of Pattern-Based Calculi with Finitary Matching (abstract) |
| 17:30 | The Verification of Conversion Algorithms between Finite Automata (abstract) |
| 18:00 | Source code profiling and classification for automated detection of logical errors (abstract) |
16:30-18:00 Session 80H: Contributed talks to NLCS (NLCS)
Chair:
Location: FH, CAD 2
| 16:30 | Algebraic Effects and Handlers in Natural Language Interpretation (abstract) |
| 17:00 | Solving Partee's Temperature Puzzle in an EFL-Ontology (abstract) |
| 17:30 | Toward a Logic of Cumulative Quantification (abstract) |
16:30-18:00 Session 80I: Contributed Talks (LATD)
Location: MB, Festsaal
| 16:30 | Densification via polynomial extensions (abstract) |
| 17:00 | Introducing an exotic MTL-chain (abstract) |
| 17:30 | On Pocrims and Hoops (abstract) |
16:30-18:00 Session 80J: Contributed Talks (LATD)
Location: MB, Hörsaal 15
| 16:30 | Ordinal foundation for Lukasiewicz semantics (abstract) |
| 17:00 | Advances on elementary equivalence in model theory of fuzzy logics (abstract) |
| 17:30 | Trakhtenbrot theorem and first-order axiomatic extensions of MTL (abstract) |
16:30-17:30 Session 80K: Invited talk (EC2)
Location: FH, Seminarraum 101C
| 16:30 | Verifiable Concurrent Systems Programming: A Garbage Collector Case Study (abstract) |
16:30-18:00 Session 80L: Contributed Talks: Observation and Justification (PSC)
Chair:
Location: FH, CAD 1
| 16:30 | Observational Equivalence for Behavioural Differential Equations (abstract) |
| 17:15 | Multi-agent justification logic (abstract) |
16:30-18:00 Session 80N: iPrA Regular talks (iPRA)
Chair:
Location: FH, Seminarraum 101A
| 16:30 | On Enumerating Query Plans via Interpolants from Tableau Proofs (abstract) (abstract) |
| 17:00 | Application Patterns of Projection/Forgetting (abstract) |
| 17:30 | Generalized Craig Interpolation for Stochastic Satisfiability Modulo Theory Problems (abstract) |
16:30-19:00 Session 80P: Perspectives - Invited Perspectives (CICLOPS-WLPE and PLP)
Chair:
Location: FH, Hörsaal 7
| 16:30 | A unified approach to generative and discriminative modeling (abstract) |
| 17:00 | Inference and learning for PLP (abstract) |
| 17:30 | TBA (abstract) |
| 18:00 | TBA (abstract) |
| 18:30 | Discussion on the implementation of PLP systems. (abstract) |
16:30-17:45 Session 80Q (VEMDP)
Location: FH, Seminarraum 136
| 16:30 | Boolean modelling and formal verification of tiered-rate chemical reaction networks (abstract) |
| 16:55 | Formal mean field theories for graph rewriting (abstract) |
| 17:20 | Rule based modelling of DNA repair (abstract) |
16:30-18:30 Session 80R: Contributed Talks: Belief Change (NMR)
Location: EI, EI 9
| 16:30 | Inference in the FO(C) Modelling Language (abstract) |
| 17:00 | FO(C) and Related Modelling Paradigms (abstract) |
| 17:30 | Belief merging within fragments of propositional logic (abstract) |
| 18:00 | Belief Revision and Trust (abstract) |
16:30-18:30 Session 80S: Summer School on Computational Logic: Horn Clauses and Verification II (ICLP)
Location: Seminarraum 1/3 OPG
| 16:30 | Horn Clauses and Verification II (abstract) |
16:50-18:30 Session 81: Contributed Talks (DL)
Location: EI, EI 7
| 16:50 | Goal-Directed Tracing of Inferences in EL Ontologies (abstract) |
| 17:15 | Brave and Cautious Reasoning in EL (abstract) |
| 17:40 | Matching with respect to general concept inclusions in the Description Logic EL (abstract) |
| 18:05 | Contextualized Knowledge Repositories with Justifiable Exceptions (abstract) |
17:20-18:10 Session 82: Technical Session (LFMTP)
Chair:
Location: FH, Zeichensaal 1
| 17:20 | Some constructions on ω-groupoids (abstract) |
| 17:45 | Gentle Formalisation of Stoughton’s Lambda Calculus Substitution (abstract) |
17:45-18:30 Session 83: Poster and demo session (VEMDP)
Location: FH, Seminarraum 136
| 17:45 | DyNAMiC Workbench: Automated design and verification of dynamic DNA nanosystems (abstract) |
| 17:45 | An Aspect Oriented Design and Modelling Framework for Synthetic Biology (abstract) |
| 17:45 | Guiding the development of DNA walker systems to guarantee reliability and performance (abstract) |
| 17:45 | Software tools for analysing the chemical master equation (abstract) |
| 17:45 | Identification of Components and Modular Verification of Biochemical Pathways (abstract) |
19:00-20:00 Session 84A: LICS Business Meeting (CSL-LICS)
Location: FH, Hörsaal 1
Friday, July 18th, 2014
View this program: with abstractssession overviewtalk overview
08:45-10:15 Session 86A: New and advanced Coq features (Coq)
Chair:
Location: MB, Hörsaal 14A
| 08:45 | Presentation of Three Neat Tricks in Coq 8.5 (abstract) |
| 09:15 | Towards a better-behaved unification algorithm for Coq (abstract) |
| 09:45 | Proof-relevant rewriting strategies in Coq (abstract) |
08:45-10:15 Session 86B: Tutorial: How do we get inductive invariants? (CAV)
Chair:
Location: FH, Hörsaal 6
| 08:45 | How do we get inductive invariants? (Part A) (abstract) |
08:45-10:15 Session 86C: Summer School on Computational Logic: Probabilistic Logic Programming I (ICLP)
Location: Seminarraum 1/3 OPG
| 08:45 | Summer School Opening (abstract) |
| 08:50 | Probabilistic Logic Programming I (abstract) |
08:45-10:15 Session 86D: CAV Tutorial: How do we get inductive invariants? (NSV)
Location: FH, Hörsaal 2
08:45-10:15 Session 86E: Fairness and Liveness (WST)
Location: FH, Seminarraum 101B
| 08:45 | Fairness for Infinite-State Systems (abstract) |
| 09:15 | Reducing Deadlock and Livelock Freedom to Termination (abstract) |
| 09:45 | Specifying and verifying liveness properties of QLOCK in CafeOBJ (abstract) |
08:45-10:15 Session 86F: Hypervisors and dynamic data structures (VSTTE)
Location: FH, Zeichensaal 3
| 08:45 | Store Buffer Reduction with MMUs (abstract) |
| 09:10 | Separation Kernel Verification: the XtratuM Case Study (abstract) |
| 09:35 | Separation algebras for C verification in Coq (abstract) |
| 10:00 | Automatically verified implementation of data structures based on AVL trees (SHORT) (abstract) |
08:45-10:15 Session 86G: Opening and Invited Talk (LaSh and QUANTIFY)
Chair:
Location: MB, Aufbaulabor
| 08:45 | LaSh and QUANTIFY Openings (abstract) |
| 09:00 | Instantiation-based reasoning, EPR encodings and all that (abstract) |
08:45-10:15 Session 86H: Tutorial and a contributed talk (CSPSAT)
Location: MB, Zeichensaal 15
| 08:45 | Tutorial (tentative): TBA (abstract) |
| 09:45 | SAT Compilation for Constraints over Finite Structured Domains (abstract) |
08:45-10:15 Session 86I: Contributed Talks (LATD)
Location: MB, Festsaal
| 08:45 | Relatively filtral quasivarieties (abstract) |
| 09:15 | On logics of varieties and logics of semilattices (abstract) |
| 09:45 | Congruential deductive systems associated with equationally orderable varieties (abstract) |
08:45-10:15 Session 86J: Contributed Talks (LATD)
Location: MB, Hörsaal 15
| 08:45 | Semantial and syntactial charaterisation of some extensions of the class of MV-algebras (abstract) |
| 09:15 | The space of directions of a polyhedron (abstract) |
| 09:45 | Interpreting Lukasiewicz logic into Intuitionistic logic (abstract) |
08:45-10:15 Session 86K: Workshop Opening and Invited Talk (ParSearchOpt)
Location: MB, Hörsaal 4
| 08:45 | Invited Talk (abstract) |
08:45-09:45 Session 86L: Invited Speaker (ASA and FCS-FCC)
Chair:
Location: MB, Hörsaal 7
| 08:45 | Cryptosense: Formal Analysis of Security APIs from Research to Spin-Off (abstract) |
08:45-10:15 Session 86M: Invited Talk and Contributed Talk (DL and NMR)
Location: EI, EI 7
| 08:45 | Invited Talk: Fragments of Logic, Language, and Computation (abstract) |
| 09:45 | On the Non-Monotonic Description Logic ALC+Tmin (abstract) |
08:45-09:00 Session 86N: Workshop Opening (STAST)
Location: MB, Seminarraum 212/232
08:45-10:15 Session 86P: Invited speaker (A. Rybalchenko) (VPT)
Location: FH, Dissertantenraum E104
| 08:45 | Towards Automated Proving of Relational Properties of Probabilistic Programs (Invited Talk) (abstract) |
09:00-10:15 Session 87B: Invited Talk (CHR and CICLOPS-WLPE)
Chair:
Location: FH, Hörsaal 7
| 09:00 | Coherent Logic and Applications (abstract) |
09:00-10:00 Session 87C (AISS)
Location: FH, Seminarraum 134
| 09:00 | Decision Problems for Linear Recurrence Sequences (abstract) |
09:00-18:00 Session 87D: FLoC Olympic Games Big Screen: OWL Reasoner Evaluation (ORE 2014) (joint session of 10 meetings)
Location: EI, Foyer
| 09:00 | FLoC Olympic Games Big Screen: OWL Reasoner Evaluation (ORE 2014) (abstract) |
09:00-18:00 Session 87E: FLoC Olympic Games Big Screen: Satisfiability Modulo Theories solver competition (SMT-COMP 2014) (joint session of 10 meetings)
Location: FH, 2nd floor
| 09:00 | FLoC Olympic Games Big Screen: Satisfiability Modulo Theories solver competition (SMT-COMP 2014) (abstract) |
09:00-10:15 Session 87F: Invited Tutorials (SAT- and SMT-Solvers) (APPA)
Location: FH, Seminarraum 325/1
| 09:00 | Satisfiability Solvers (abstract) |
| 09:30 | Proofs in Satisfiability Modulo Theories (abstract) |
09:00-10:15 Session 87G: Invited Talk by Frank Wolter (iPRA)
Chair:
Location: FH, Seminarraum 101A
| 09:00 | Interpolation in Description Logic: A Survey (abstract) |
09:00-10:15 Session 87H: Invited talk: Aarne Ranta (NLCS and NLSR)
Chair:
Location: FH, CAD 2
| 09:00 | Machine Translation: Green, Yellow, and Red (abstract) (abstract) |
09:00-10:15 Session 87I: Keynote Talk (STAST)
Location: MB, Seminarraum 212/232
| 09:00 | Tackling the Awareness-Behaviour Divide in Security: (step 1) Understand the User (abstract) |
09:00-10:15 Session 87J (QED)
Location: FH, Hörsaal 4
| 09:00 | QED: a grand unified theory? (abstract) |
| 09:35 | How to prove the odd order from the four color theorem (abstract) |
09:15-10:15 Session 88A: Invited Talk by Christel Baier (CSL-LICS)
Chair:
Location: FH, Hörsaal 1
| 09:15 | Trade-Off Analysis Meets Probabilistic Model Checking (abstract) |
09:15-10:15 Session 88B: Invited talk (ITRS)
Chair:
Location: MB, Zeichensaal 14
| 09:15 | Intersection Types, Game Semantics and Higher-Order Model Checking (abstract) |
09:15-10:15 Session 88C: Invited talk (LC)
Location: MB, Prechtlsaal
| 09:15 | Synthesis for monadic logic over the reals (abstract) |
09:15-10:15 Session 88D: Invited Talk by Hoon Hong (PAS)
Location: FH, Seminarraum 138A
| 09:15 | Test-Input Generation using Computational Real Algebraic Geometry (abstract) |
09:15-10:15 Session 88E: Invited talk (EC2)
Location: FH, Seminarraum 101C
| 09:15 | Does Wait-Freedom Matter? (abstract) |
09:15-10:15 Session 88F: Invited Talk (SMT)
Chair:
Location: FH, Seminarraum 104
| 09:15 | Automating the verification of floating-point algorithms (abstract) |
09:15-10:15 Session 88G: Invited Talk by Ulrich Berger (joint work with Tie Hou): Program Extraction in Church's Simple Theory of Types (PSC)
Chair:
Location: FH, CAD 1
| 09:15 | Program extraction in Church's simple theory of types (invited talk) (abstract) |
09:15-10:15 Session 88H: Invited talk (PCCR)
Location: FH, Hörsaal 3
| 09:15 | CSPs and fixed-parameter tractability (abstract) |
09:15-10:15 Session 88I: Constraints (RCRA)
Location: MB, Hörsaal 12
| 09:15 | A compression algorithm to improve generalized hypertree decomposition-based solving approaches for large extensional non binary CSP (abstract) |
| 09:45 | Dispensable Instantiations in Constraint Satisfaction Problems (abstract) |
09:15-10:15 Session 88J: Invited Talk: Matching Logic (HOPA)
Location: FH, Seminarraum 138C
| 09:15 | TBA (abstract) |
Thursday, July 17th, 2014
View this program: with abstractssession overviewtalk overview
21:00-23:59 Session 89: VSL Student Reception 1 (VSL)
Location: Transporter
Friday, July 18th, 2014
View this program: with abstractssession overviewtalk overview
09:45-10:25 Session 89A: Technical Session (ASA)
Location: MB, Zeichensaal 13
| 09:45 | Nuances of the JavaCard API on the cryptographic smart cards - JCAlgTest project (abstract) |
09:45-10:15 Session 89B: Technical Session (FCS-FCC)
Chair:
Location: MB, Hörsaal 7
| 09:45 | A Hybrid Analysis for Security Protocols with State (abstract) |
10:15-10:45Coffee Break
10:45-13:00 Session 90AA: Programming Logics (CSL-LICS)
Chair:
Location: FH, Hörsaal 1
| 10:45 | Subclasses of Presburger Arithmetic and the Weak EXP Hierarchy (abstract) |
| 11:15 | On the Discriminating Power of Passivation and Higher-Order Interaction (abstract) |
| 11:45 | Asymptotic behaviour in temporal logic (abstract) |
| 12:15 | Weight Monitoring with Linear Temporal Logic: Complexity and Decidability (abstract) |
10:45-13:00 Session 90AB: Proof Theory (CSL-LICS)
Chair:
Location: FH, Hörsaal 5
| 10:45 | On Context Semantics for Interaction Nets (abstract) |
| 11:15 | The Geometry of Synchronization (abstract) |
| 11:45 | A new correctness criterion for MLL proof nets (abstract) |
| 12:15 | Non-Elementary Complexities for Branching VASS, MELL, and Extensions (abstract) |
10:45-12:45 Session 90AC: Invited talk & useful tools (Coq)
Chair:
Location: MB, Hörsaal 14A
| 10:45 | What is Homotopy Type Theory? (abstract) |
| 11:45 | QuickChick: Property-Based Testing for Coq (abstract) |
| 12:15 | Proof-Pattern Search in Coq/SSReflect (abstract) |
10:45-12:15 Session 90AD: Tutorial: How do we get inductive invariants? (CAV)
Chair:
Location: FH, Hörsaal 6
| 10:45 | How do we get inductive invariants? (Part B) (abstract) |
10:45-13:00 Session 90AE: Summer school on Computational Logic: Probabilistic Logic Programming II (ICLP)
Location: Seminarraum 1/3 OPG
| 10:45 | Probabilistic Logic Programming II (abstract) |
10:45-12:45 Session 90AF: CAV Tutorial: How do we get inductive invariants? (NSV)
Location: FH, Hörsaal 2
10:45-11:45 Session 90AG (ITRS)
Chair:
Location: MB, Zeichensaal 14
| 10:45 | A Finite Model Property for Intersection Types (abstract) |
| 11:15 | On Isomorphism of "Functional'' Intersection and Union Types (abstract) |
10:45-13:00 Session 90AH: SAT Encodings and Semantic Labelling (WST)
Location: FH, Seminarraum 101B
| 10:45 | Automating Elementary Interpretations (abstract) |
| 11:15 | A Satisfiability Encoding of Dependency Pair Techniques for Maximal Completion (abstract) |
| 11:45 | Automated SAT Encoding for Termination Proofs with Semantic Labelling and Unlabelling (abstract) |
| 12:15 | A Solution to Endrullis-08 and Similar Problems (abstract) |
| 12:45 | Discussion (abstract) |
10:45-13:00 Session 90AI: EPR, QBF, and QCSP (QUANTIFY)
Location: FH, Seminarraum 136
| 10:45 | Quantifier handling in calculi for quantified Boolean formulas (abstract) |
| 11:30 | Encoding Reachability with Quantification (abstract) |
| 12:00 | EPR Encodings of Bit-Vector Problems Even With Quantifiers (abstract) |
| 12:30 | Beyond Q-Resolution and Prenex Form: A Proof System for Quantified Constraint Satisfaction (abstract) |
10:45-12:45 Session 90AJ (AISS)
Location: FH, Seminarraum 134
| 10:45 | Parameterized Model Checking of Rendezvous Systems (abstract) |
| 11:15 | Model Checking Communicating Finite-State Machines using Local Temporal Logics (abstract) |
| 11:45 | Unary Pushdown Automata and Straight-Line Programs (abstract) |
| 12:15 | Of stacks (of stacks (...) with blind counters) with blind counters (abstract) |
10:45-11:45 Session 90AK: Invited Tutorials (First- and Higher-order Automated Theorem Provers) (APPA)
Location: FH, Seminarraum 325/1
| 10:45 | First-Order Automated Theorem Provers (abstract) |
| 11:15 | Higher-Order Automated Theorem Provers (abstract) |
10:45-12:45 Session 90AL: Symbolic Computation (PAS)
Location: FH, Seminarraum 138A
| 10:45 | Synthesis of Algorithms on Sets Represented as Monotone Lists (abstract) |
| 11:15 | New predicate transformer for symbolic modeling (abstract) |
| 11:45 | VTOS: A Finite State Machine Model of OS and Formalized Verification of Its Microkernel (abstract) |
| 12:15 | Symbolic Problem Solving With Bidirectional Executable Representations (abstract) |
10:45-13:00 Session 90AM: Certification (VSTTE)
Location: FH, Zeichensaal 3
| 10:45 | Up and Out: Scaling Formal Analysis Using Model-Based Development and Architecture Modeling (abstract) |
| 11:45 | A logical analysis of framing for specifications with pure method calls (abstract) |
| 12:10 | A certifying frontend for (sub)polyhedral abstract domains (abstract) |
| 12:35 | Certification of Nontermination Proofs using Strategies and Nonlooping Derivations (abstract) |
10:45-13:00 Session 90AN: LaSh morning 2: Contributed Talks (LaSh)
Chair:
Location: MB, Aufbaulabor
| 10:45 | Meta-level Representations in the IDP Knowledge Base System: Bootstrapping Inference Engine Development (abstract) |
| 11:15 | Logical Machinery of Heuristics (Preliminary Report) (abstract) |
| 11:45 | Modeling High School Timetabling as PartialWeighted maxSAT (abstract) |
| 12:15 | Learning Optimal Bounded Treewidth Bayesian Networks via Maximum Satisfiability (abstract) |
| 12:45 | Depart for Workshop Lunch (abstract) |
10:45-12:45 Session 90AP: Invited talk and two contributed talks (CSPSAT)
Location: MB, Zeichensaal 15
| 10:45 | Invited talk: MaxSat and SoftCSPs (abstract) |
| 11:45 | Some New Tractable Classes of CSPs and their Relations with Backtracking Algorithms (abstract) |
| 12:15 | BreakIDGlucose: on the importance of row symmetry (abstract) |
10:45-12:45 Session 90AQ: Invited Talk (Fitting) and Tutorial (Baader) (LATD)
Location: MB, Festsaal
| 10:45 | The Range of Realization Which modal logics have explicit counter parts (abstract) |
| 11:45 | Tutorial: Fuzzy Description Logics (Part 1) (abstract) |
10:45-11:45 Session 90AR: Contributed talks to NLSR (NLSR)
Location: FH, CAD 2
| 10:45 | Exposing Predictive Analytics through Natural Language Dialog (abstract) |
| 11:15 | Natural Language Access to Data (abstract) |
10:45-13:00 Session 90AS (ParSearchOpt)
Location: MB, Hörsaal 4
| 10:45 | A Portfolio Based Parallel SAT Solver with Multiple Deletion Strategies (abstract) |
| 11:15 | Towards a Parallel Hierarchical Adaptive Solver Tool (abstract) |
| 11:45 | On the Parallelization of Randomized Propagation-based Constraint Solving (abstract) |
| 12:15 | A Constraint-based Parallel Local Search for Disjoint Rooted Distance-Constrained Minimum Spanning Tree Problem (abstract) |
10:45-12:45 Session 90AT: Technical Session (ASA)
Location: MB, Zeichensaal 13
| 10:45 | Banking security Wish list: notes from the edge (abstract) |
| 11:25 | Well-typed generic smart-fuzzing for APIs (abstract) |
| 12:05 | Caetus tool (abstract) |
10:45-12:00 Session 90AU: Contributed Talks (DL and NMR)
Location: EI, EI 7
| 10:45 | Towards Practical Deletion Repair of Inconsistent DL-programs (abstract) |
| 11:10 | An Argumentation System for Reasoning with Conflict-minimal Paraconsistent ALC (abstract) |
| 11:35 | Querying Inconsistent Description Logic Knowledge Bases under Preferred Repair Semantics (abstract) |
10:45-12:15 Session 90AV: Technical session (EC2)
Location: FH, Seminarraum 101C
| 10:45 | Wait-Freedom Made Practical (abstract) |
| 11:45 | A new reduction for event-driven distributed programs (abstract) |
10:45-13:00 Session 90AW: Arithmetic (SMT)
Chair:
Location: FH, Seminarraum 104
| 10:45 | Leveraging Linear and Mixed Integer Programming for SMT (abstract) |
| 11:15 | raSAT: SMT for Polynomial Inequality (abstract) |
| 11:45 | Better Answers to Real Questions (abstract) |
| 12:15 | Towards Conflict-Driven Learning for Virtual Substitution (abstract) |
10:45-12:15 Session 90AX: Contributed Talks: Extracting Parsers and Ancestral Logic (PSC)
Chair:
Location: FH, CAD 1
| 10:45 | Extracting Monadic Parsers from Proofs (abstract) |
| 11:30 | Intuitionistic Ancestral Logic (abstract) |
10:45-13:00 Session 90AY: iPrA Regular Talks (iPRA)
Chair:
Location: FH, Seminarraum 101A
| 10:45 | Resolution Based Uniform Interpolation for Expressive Description Logics (abstract) |
| 11:15 | Practical CNF Interpolants Via BDDs (abstract) |
| 11:45 | Interpolation and Domain Independence applied to Databases (abstract) |
| 12:15 | Tree-based Modular SMT Solving (abstract) |
10:45-11:45 Session 90AZ: Invited Speaker (FCS-FCC)
Chair:
Location: MB, Hörsaal 7
| 10:45 | Constructive Cryptography and Security Proofs (abstract) |
10:45-11:45 Session 90BA: Contributed talks (PCCR)
Location: FH, Hörsaal 3
| 10:45 | Connection matrices of finite rank instead of definability in Monadic Second Order Logic (abstract) |
| 11:15 | Backdoors into Two Occurrences (abstract) |
10:45-13:00 Session 90BB: Security Ceremonies and Policies (STAST)
Location: MB, Seminarraum 212/232
| 10:45 | Decision justifications for wireless network selection (abstract) |
| 11:30 | Reflecting on the Ability of Enterprise Security Policy to Address Accidental Insider Threat (abstract) |
| 12:15 | Modelling User Devices in Security Ceremonies (abstract) |
10:45-11:15 Session 90BC: Constraints (continued) (RCRA)
Location: MB, Hörsaal 12
| 10:45 | Neighbourhood SAC for Preprocessing and Search (abstract) |
10:45-12:00 Session 90BD: Invited talk (ADDCT)
Location: FH, Zeichensaal 1
| 10:45 | A Superposition-Based Approach to Abductive Reasoning in Equational Clausal Logic (abstract) |
10:45-12:45 Session 90BE: Contributed Talks (CHR and CICLOPS-WLPE)
Chair:
Location: FH, Hörsaal 7
| 10:45 | Automated Test Case Generation and Model Checking with CHR (abstract) |
| 11:15 | From XML Schema to JSON Schema: Translation with CHR (abstract) |
| 11:45 | Constraint Handling Rules with Multiset Comprehension Patterns (abstract) |
| 12:15 | Discussion (abstract) |
10:45-13:00 Session 90BF: Contributed Talks (VPT)
Location: FH, Dissertantenraum E104
| 10:45 | On Unfolding for Programs Using Strings as a Data Type (abstract) |
| 11:30 | Branching Processes of Conservative Nested Petri Nets (abstract) |
| 12:15 | Local Driving in Higher-Order Positive Supercompilation via the Omega-theorem (abstract) |
10:45-13:00 Session 90BG (QED)
Chair:
Location: FH, Hörsaal 4
| 10:45 | 25 years of the Mizar Mathematical Library (abstract) |
| 11:20 | The seL4 microkernel verification (abstract) |
| 11:55 | Towards Formally Verified Theorem Provers - Part I (abstract) |
| 12:15 | Towards Formally Verified Theorem Provers - Part II (abstract) |
| 12:30 | TBA (abstract) |
10:45-12:45 Session 90BH: Invited Talk 2 and Submitted Talks: Javascript and Concurrency (HOPA)
Location: FH, Seminarraum 138C
| 10:45 | Program Analysis for JavaScript Web Applications (abstract) |
| 11:45 | Analyzing JavaScript: The Bad Parts (abstract) |
| 12:15 | Saturation of Concurrent Collapsible Pushdown Systems (Extended Abstract) (abstract) |
11:00-13:00 Session 91: Tutorial and invited talk (LC)
Location: MB, Prechtlsaal
| 11:00 | On local induction schemes (abstract) |
| 12:00 | Tutorial on Classical Realizability and Forcing 2 (abstract) |
11:20-13:00 Session 92: Heuristic, randomised and probabilistic approaches (RCRA)
Location: MB, Hörsaal 12
| 11:20 | Concept Learning by a Monte-Carlo Tree Search of Argumentations (abstract) |
| 11:50 | Evaluating Probabilistic Model Checking Tools for Verification of Robot Control Policies (abstract) |
| 12:20 | Self Regulating Mechanisms for Network Immunization (abstract) |
| 12:40 | An Enhanced Genetic Algorithm of the BLF2G Guillotine Placement Heuristic for the Orthogonal Cutting-Stock Problem (abstract) |
11:45-12:45 Session 93B: talks after an invited NLCS/NLSR lecture by Aarne Ranta (NLCS)
Chair:
Location: FH, CAD 2
| 11:45 | Transfer Semantics for the Clear Parser (abstract) |
| 12:15 | Analyzing and Modelling the Structure of Argument Compounds in Logic: the case of technical texts (abstract) |
12:00-13:00 Session 94A (ITRS)
Chair:
Location: MB, Zeichensaal 14
| 12:00 | Uniform Proofs of Normalisation and Approximation for Intersection Types (abstract) |
| 12:30 | Indexed linear logic and higher-order model checking (abstract) |
12:00-13:00 Session 94B: Invited Tutorials (Interactive Theorem Provers and Calculus of Inductive Constructions) (APPA)
Location: FH, Seminarraum 325/1
| 12:00 | Interactive Theorem Provers from the perspective of Isabelle/Isar (abstract) |
| 12:30 | Calculus of Inductive Constructions (abstract) |
12:00-13:00 Session 94C: Contributed Talks and Poster Announcements (DL)
Location: EI, EI 7
| 12:00 | Temporal OBDA with LTL and DL-Lite (abstract) |
| 12:25 | Complexity of Temporal Query Abduction in DL-Lite (abstract) |
| 12:50 | Temporalising EL Concepts with Time Intervals (abstract) |
| 12:53 | Transition Constraints for Temporal Attributes (abstract) |
| 12:56 | A Stream-Temporal Query Language for Ontology Based Data Access (abstract) |
12:00-13:00 Session 94D: Technical Session (FCS-FCC)
Chair:
Location: MB, Hörsaal 7
| 12:00 | A tool for automating the computationally complete symbolic attacker (abstract) |
| 12:20 | Towards a Coinductive Characterization of Computational Indistinguishability (abstract) |
| 12:40 | Actual Causes of Security Violations (abstract) |
12:00-12:30 Session 94E: Contributed talk (PCCR)
Location: FH, Hörsaal 3
| 12:00 | Discovering Archipelagos of Tractability: Split-Backdoors to Constraint Satisfaction (abstract) |
12:00-13:00 Session 94F: Satisfiability Modulo Theories and Applications (ADDCT)
Location: FH, Zeichensaal 1
| 12:00 | Satisfiability Modulo Non-Disjoint Combinations of Theories Connected via Bridging Functions (abstract) |
| 12:30 | Finding Minimum Type Error Sources (abstract) |
12:00-13:00 Session 94G: Contributed Talks: Benchmarks (NMR)
Location: EI, EI 9
| 12:00 | Some thoughts about benchmarks for NMR (abstract) |
| 12:30 | Towards a Benchmark of Natural Language Arguments (abstract) |
12:15-13:00 Session 95: Discussion (EC2)
Location: FH, Seminarraum 101C
13:00-14:30Lunch Break
14:30-16:00 Session 96AA: Formalizations in Coq (Coq)
Chair:
Location: MB, Hörsaal 14A
| 14:30 | Formalization of Error-correcting Codes using SSReflect (abstract) |
| 15:00 | Autosubst: Automation for de Bruijn Substitutions (abstract) |
| 15:30 | Automating Abstract Logics (abstract) |
14:30-16:00 Session 96AB: Games and Finite Models (CSL-LICS)
Chair:
Location: FH, Hörsaal 1
| 14:30 | Regular Combinators for String Transformations (abstract) |
| 15:00 | On Periodically Iterated Morphisms (abstract) |
| 15:30 | Finite-Memory Strategy Synthesis for Robust Multidimensional Mean-Payoff Objectives (abstract) |
14:30-16:00 Session 96AC: Types (CSL-LICS)
Chair:
Location: FH, Hörsaal 5
| 14:30 | A type theory for productive coprogramming via guarded recursion (abstract) |
| 15:00 | Formulae-as-Types for an Involutive Negation (abstract) |
| 15:30 | Eilenberg-MacLane Spaces in Homotopy Type Theory (abstract) |
14:30-16:00 Session 96AD: Tutorial: Hardware Model Checking (CAV)
Chair:
Location: FH, Hörsaal 6
| 14:30 | Hardware Model Checking (Part A) (abstract) |
14:30-16:00 Session 96AE: Summer School on Computational Logic: Answer Set Programming I (ICLP)
Location: Seminarraum 1/3 OPG
| 14:30 | Answer Set Programming I (abstract) |
14:30-15:30 Session 96AF (ITRS)
Chair:
Location: MB, Zeichensaal 14
| 14:30 | Lucretia — intersection type polymorphism for scripting languages (abstract) |
| 15:00 | Liquid Intersection Types (abstract) |
14:30-16:00 Session 96AG: Special session: Philosophy of Mathematics (LC)
Location: MB, Hörsaal 14
| 14:30 | Frege on mathematical progress (abstract) |
| 15:15 | On Bernays' Generalization of Cantor's Theorem (abstract) |
14:30-16:00 Session 96AH: Special session: Set Theory (LC)
Location: MB, Seminarraum 225
| 14:30 | Large cardinals, forcing axioms, and the theory of subsets of \omega_1 (abstract) |
| 15:15 | Locally definable well-orders (abstract) |
14:30-16:00 Session 96AI: Term Rewriting Revisited (WST)
Location: FH, Seminarraum 101B
| 14:30 | On the derivational complexity of Kachinuki orderings (abstract) |
| 15:00 | Kurth's Criterion H Revisited (abstract) |
| 15:30 | Another Proof for the Recursive Path Ordering (abstract) |
14:30-16:00 Session 96AJ: QBF and First-Order Logic (QUANTIFY)
Location: FH, Seminarraum 136
| 14:30 | Algorithmic Paradigms for Solving QBF (abstract) |
| 15:30 | Projective Quantifier Elimination for Equational Constraint Solving (abstract) |
14:30-16:00 Session 96AK (AISS)
Location: FH, Seminarraum 134
| 14:30 | Playing with Automata and Trees (abstract) |
| 15:30 | Quantitative Automatic Structures (abstract) |
14:30-16:00 Session 96AL: Invited Talk (CHR and CICLOPS-WLPE)
Chair:
Location: FH, Hörsaal 7
| 14:30 | Symbolic Evaluation Graphs and Term Rewriting - A General Methodology for Analyzing Logic Programs (abstract) |
| 15:30 | Discussion (abstract) |
14:30-16:00 Session 96AM: Invited Tutorials (Foundational Proof Certificates, Deduction Modulo and Proof Analysis) (APPA)
Location: FH, Seminarraum 325/1
| 14:30 | Foundational Proof Certificates (abstract) |
| 15:00 | Deduction Modulo (abstract) |
| 15:30 | Mathematical Proof Analysis (abstract) |
14:30-16:00 Session 96AN: Invited Talk by Michael Rusinowitch (PAS)
Location: FH, Seminarraum 138A
| 14:30 | Automated verification of security protocols and services (abstract) |
| 15:30 | Building explicit induction schemas for cyclic induction reasoning (abstract) |
14:30-16:00 Session 96AP: Real Time and Security (VSTTE)
Location: FH, Zeichensaal 3
| 14:30 | Model Checking Parameterized Timed Systems (abstract) |
| 14:55 | Timed Refinements for Verification of Real-Time Object Code Programs (abstract) |
| 15:20 | Formal Modeling and Verification of CloudProxy (abstract) |
14:30-16:10 Session 96AQ: LaSh afternoon 1: Invited Talks - Lazy Grounding (LaSh)
Chair:
Location: MB, Aufbaulabor
| 14:30 | Laziness is next to Godliness (abstract) |
| 15:30 | Lazy Model Expansion: Interleaving Grounding with Search (abstract) |
14:30-16:00 Session 96AR: NLCS contributed talks (NLCS)
Chair:
Location: FH, CAD 2
| 14:30 | A low-level treatment of quantifiers in categorical compositional distributional semantics (abstract) |
| 15:00 | Divergence in Dialogues (abstract) |
| 15:30 | Modelling implicit dynamic introduction of function symbols in mathematical texts (abstract) |
14:30-16:00 Session 96AS: Invited Talk (Metcalfe) and Contributed Talk (LATD)
Location: MB, Festsaal
| 14:30 | First-Order Logics and Truth Degrees (abstract) |
| 15:30 | Classification of germinal MV-algebras (abstract) |
14:30-16:00 Session 96AT: Talk and Panel Discussion (ParSearchOpt)
Location: MB, Hörsaal 4
| 14:30 | General Panel Discussion (abstract) |
| 15:30 | Towards a complete constraint solver on GPU (abstract) |
14:30-15:50 Session 96AU: Technical session (ASA)
Location: MB, Zeichensaal 13
| 14:30 | Application Oriented Low Cost Security Modules (abstract) |
| 15:10 | Security APIs for Device Enrolment (abstract) |
14:30-15:50 Session 96AV: Contributed Talks and Poster Announcements (DL)
Location: EI, EI 7
| 14:30 | Gödel FL_0 with Greatest Fixed-Point Semantics (abstract) |
| 14:55 | Fuzzy DLs over Finite Lattices with Nominals (abstract) |
| 15:20 | A MILP-based decision procedure for the (Fuzzy) Description Logic ALCB (abstract) |
| 15:23 | Complexity sources in FDL (abstract) |
| 15:26 | Gödel Description Logics with General Models (abstract) |
| 15:29 | Certain Answers in a Rough World (abstract) |
| 15:32 | Bayesian Description Logics (abstract) |
| 15:35 | Reasoning about Belief Uncertainty in DL-Lite N bool (abstract) |
| 15:38 | Obfuscation of Semantic Data: Restricting the Spread of Sensitive Information (abstract) |
| 15:41 | Measuring Conceptual Similarity in Ontologies: How Bad is a Cheap Measure? (abstract) |
| 15:44 | Mary, What's Like All Cats? (abstract) |
14:30-16:00 Session 96AW: SMT-COMP and SMT-EVAL Presentations (SMT)
Chair:
Location: FH, Seminarraum 104
14:30-16:00 Session 96AX: Contributed Talks: Proof Search and Proof Relevance (PSC)
Chair:
Location: FH, CAD 1
| 14:30 | Proof-search in natural deduction calculi for IPL (abstract) |
| 15:15 | A joint logic of problems and propositions, a modified BHK-interpretation and proof-relevant topological models of intuitionistic logic (abstract) |
14:30-16:00 Session 96AY: iPrA Regular Talks (iPRA)
Chair:
Location: FH, Seminarraum 101A
| 14:30 | Using Interpolation for the Verification of Security Protocols (Extended Abstract) (abstract) |
| 15:00 | Interpolation Strategies (abstract) |
| 15:30 | Towards Craig Interpolation for String Constraints (abstract) |
14:30-16:00 Session 96AZ: Technical Session (FCS-FCC)
Chair:
Location: MB, Hörsaal 7
| 14:30 | Adversary Gain vs. Defender Loss in Quantified Information Flow (abstract) |
| 15:00 | Generalizing Permissive-Upgrade in Dynamic Information Flow Analysis (abstract) |
| 15:30 | Micro-Policies: Formally Verified Low-Level Tagging Schemes for Safety and Security (Short Paper) (abstract) |
14:30-15:30 Session 96BA: Invited talk (PCCR)
Location: FH, Hörsaal 3
| 14:30 | Structural Decomposition Methods: How They Matter (abstract) |
14:30-16:00 Session 96BB: Security and Human Behaviour (STAST)
Location: MB, Seminarraum 212/232
| 14:30 | The Social Engineering Personality Framework (abstract) |
| 15:15 | Modeling Human Behaviour with Higher Order Logic: Insider Threats (abstract) |
14:30-16:00 Session 96BC: Dynamic and Modal Logic (ADDCT)
Location: FH, Zeichensaal 1
| 14:30 | Decidability of Iteration-free PDL with Parallel Composition (abstract) |
| 15:00 | Axiomatic and Tableau-Based Reasoning for Kt(H,R) (abstract) |
| 15:30 | On dual tableau-based decision procedures for relational fragments (abstract) |
14:30-16:00 Session 96BD: Special Session: Decidability with Numerical Methods (NSV)
Location: FH, Hörsaal 2
| 14:30 | Epsilon-semantics and hybrid automata (abstract) |
| 15:00 | Verifying Floating-Point Implementations of Nonlinear Functions (abstract) |
| 15:30 | Correctness of Parallel Interval Computations (abstract) |
14:30-16:00 Session 96BE (QED)
Chair:
Location: FH, Hörsaal 4
| 14:30 | TBA (abstract) |
| 15:00 | Mixing proofs and computations (abstract) |
| 15:30 | The Naproche system: Proof-checking mathematical texts in controlled natural language (abstract) |
14:30-16:00 Session 96BF: Special session: Perspectives on Induction (CSL-LICS and LC)
Location: MB, Prechtlsaal
| 14:30 | Weak well orders and related inductions (abstract) |
| 15:15 | Automating inductive proof (abstract) |
14:30-16:00 Session 96BG: Invited talk by Josep Silva (VPT and WWV)
Location: FH, Seminarraum 107
| 14:30 | Automatic Detection of Webpage Candidates for Site-Level Web Template Extraction (abstract) |
14:30-16:00 Session 96BH: Contributed Talks: Argumentation 1 (NMR)
Location: EI, EI 9
| 14:30 | Analysis of Dialogical Argumentation via Finite State Machines (abstract) |
| 15:00 | Abduction in Argumentation: Dialogical Proof Procedures and Instantiation (abstract) |
| 15:30 | Non-Monotonic Reasoning and Story Comprehension (abstract) |
14:30-16:00 Session 96BI: Abstract Interpretation and Linear Logic (HOPA)
Location: FH, Seminarraum 138C
| 14:30 | Environment Unrolling (abstract) |
| 15:00 | Strong Function Call (abstract) |
| 15:30 | The modal nature of colors in higher-order model-checking (abstract) |
15:30-16:00 Session 97: Contributed talk (PCCR)
Location: FH, Hörsaal 3
| 15:30 | Backdoors into Heterogeneous Classes of SAT and CSP (abstract) |
15:50-16:40 Session 98: Poster Session (with coffee break) (DL)
Location: EI, Foyer
16:00-16:30Coffee Break
16:30-18:00 Session 99AA: New IDEs & Coq 8.5 update (Coq)
Chair:
Location: MB, Hörsaal 14A
| 16:30 | Asynchronous interaction for Coq (abstract) |
| 17:00 | Coqoon: towards a modern IDE for Coq (abstract) |
| 17:30 | Update on Coq 8.5 (abstract) |
16:30-18:00 Session 99AB: Tutorial: Hardware Model Checking (CAV)
Chair:
Location: FH, Hörsaal 6
| 16:30 | Hardware Model Checking (Part B) (abstract) |
16:30-17:00 Session 99AC: Test-of-Time Award Presentations and Lectures (CSL-LICS)
Location: FH, Hörsaal 1
| 16:30 | Citations for the Test-of-Time Award from 1994 (abstract) |
16:30-18:35 Session 99AD: Summer School on Computational Logic: Answer Set Programming II (ICLP)
Location: Seminarraum 1/3 OPG
| 16:30 | Answer Set Programming II (abstract) |
| 18:30 | Summer School Closing (abstract) |
16:30-17:30 Session 99AE (ITRS)
Chair:
Location: MB, Zeichensaal 14
| 16:30 | Semantic Types for Classes and Mixins (abstract) |
| 17:00 | Delegation-based Mixin Composition Synthesis (abstract) |
16:30-18:00 Session 99AF: Special session: Philosophy of Mathematics (LC)
Location: MB, Hörsaal 14
| 16:30 | Restrictiveness relative to notions of interpretation (abstract) |
| 17:15 | Reflection, Trust, Entitlement (abstract) |
16:30-18:00 Session 99AG: Special session: Model Theory (LC)
Location: MB, Seminarraum 225
| 16:30 | Definable valuation rings (abstract) |
| 17:15 | The Fitting subgroup of a supersimple group (abstract) |
16:30-18:00 Session 99AH: Discussion and Business Meeting (WST)
Location: FH, Seminarraum 101B
| 16:30 | Discussion and Business Meeting (abstract) |
16:30-18:00 Session 99AI: Satisfiability Modulo Theories (QUANTIFY)
Location: FH, Seminarraum 136
| 16:30 | Efficiently Solving Quantified Bit-Vectors (abstract) |
| 17:00 | Quantifier Projection (abstract) |
| 17:30 | Finding Conflicting Instances of Quantified Formulas in SMT (abstract) |
16:30-18:00 Session 99AJ (AISS)
Location: FH, Seminarraum 134
| 16:30 | Simulation for infinite state systems. (abstract) |
| 17:30 | Simulation Over One-Counter Nets is PSPACE-Complete (abstract) |
16:30-18:00 Session 99AK: Implementation Issues (CHR and CICLOPS-WLPE)
Chair:
Location: FH, Hörsaal 7
| 16:30 | Intelligent Visual Surveillance Logic Programming: Implementation Issues (abstract) |
| 17:00 | A Parallel Virtual Machine for Executing Forward-Chaining Linear Logic Programs (abstract) |
| 17:30 | Discussion (abstract) |
16:30-18:00 Session 99AL: Invited Tutorials (Verification, Security and Deep Inference) (APPA)
Location: FH, Seminarraum 325/1
| 16:30 | Program Verification (B Method) (abstract) |
| 17:00 | Security (abstract) |
| 17:30 | Deep Inference (abstract) |
16:30-18:10 Session 99AM: Program Verification (PAS)
Location: FH, Seminarraum 138A
| 16:30 | A hybrid path constraint solver combined with meta-heuristic search (abstract) |
| 17:00 | Automatic App Testing of LTL Properties (abstract) |
| 17:30 | Programming Language Aggregation with Applications in Equivalence Checking (abstract) |
16:30-18:00 Session 99AN: Verified Software Competition (VSCOMP 2014) (VSTTE)
Location: FH, Zeichensaal 3
16:30-18:00 Session 99AP: LaSh afternoon 2: Invited Talks - Answer Set Programming (LaSh)
Chair:
Location: MB, Aufbaulabor
| 16:30 | The D-FLAT System for Dynamic Programming on Tree Decompositions (abstract) |
| 17:10 | Cross-Translating Answer Set Programs (abstract) |
16:30-18:00 Session 99AQ: NLCS contributed talks (NLCS)
Chair:
Location: FH, CAD 2
| 16:30 | Program Extraction Applied to Monadic Parsing (abstract) |
| 17:00 | On Translating Context-Free Grammars into Lambek Categorial Grammars (abstract) |
16:30-18:00 Session 99AR: Contributed Talks (LATD)
Location: MB, Festsaal
| 16:30 | Cut-free calculus for second-order {G\"odel} logic (abstract) |
| 17:00 | Poof Search and Co-NP completeness for Many-Valued Logics (abstract) |
| 17:30 | Cut and completion? (abstract) |
16:30-18:00 Session 99AS: Contributed Talks (LATD)
Location: MB, Hörsaal 15
| 16:30 | Definability of truth predicates in abstract algebraic logic (abstract) |
| 17:00 | Generalizing the Leibniz and Suszko operators (abstract) |
| 17:30 | Church-style type theories over finitary weakly implicative logics (abstract) |
16:30-18:00 Session 99AT: SMT-LIB Discussion and Business Meeting (SMT)
Chair:
Location: FH, Seminarraum 104
16:30-18:00 Session 99AU: iPrA Regular Talks, Discussions, Closing (iPRA)
Chair:
Location: FH, Seminarraum 101A
| 16:30 | Specification Synthesis via Generalized Abduction (abstract) |
| 17:00 | Interpolation from Clausal Proofs (abstract) |
| 17:30 | Concluding discussions (abstract) |
16:30-18:00 Session 99AV: Technical Session (FCS-FCC)
Chair:
Location: MB, Hörsaal 7
| 16:30 | Protocol Indistinguishability and the Computationally Complete Symbolic Attacker (abstract) |
| 16:50 | On Well-Founded Security Protocols (abstract) |
| 17:10 | Fitting's Embedding of Classical Logic in S4 and Trace Properties in the Computational Model (abstract) |
| 17:30 | Towards Timed Models for Cyber-Physical Security Protocols (abstract) |
16:30-17:30 Session 99AW: PCCR panel (PCCR)
Location: FH, Hörsaal 3
16:30-18:00 Session 99AX: Socio-Technical Security (STAST)
Location: MB, Seminarraum 212/232
| 16:30 | What You Enter Is What You Sign: input integrity in an online banking environment (abstract) |
| 17:15 | Using Statistical Information to Communicate Android Permission Risks to Users (abstract) |
16:30-18:00 Session 99AY: NSV Invited Talk: Jim Kapinski (NSV)
Location: FH, Hörsaal 2
| 16:30 | Numerical Challenges in Simulation-guided Dynamical System Analysis (abstract) |
16:30-18:00 Session 99AZ (QED)
Location: FH, Hörsaal 4
| 16:30 | QED and the TPTP World (abstract) |
| 17:00 | MathHub.info: Active Mathematics (abstract) |
| 17:30 | Hammering towards QED (abstract) |
16:30-18:00 Session 99BA: Joint session with VPT: Web systems (WWV)
Location: FH, Seminarraum 107
| 16:30 | Static Enforcement of Role-Based Access Control (abstract) |
| 17:00 | A Local Logic for Realizability in Web Service Choreographies (abstract) |
16:30-17:30 Session 99BB: Panel Session: The W3C Web Crypto API (ASA)
Location: MB, Zeichensaal 13
16:40-17:30 Session 100: Contributed Talks (DL)
Location: EI, EI 7
| 16:40 | Datalog Rewriting Techniques for Non-Horn Ontologies (abstract) |
| 17:05 | Succinctness of Query Rewriting in OWL 2 QL: The Case of Tree-like Queries (abstract) |
17:00-18:00 Session 101A: Ackermann Award Presentation and Lecture (CSL-LICS)
Location: FH, Hörsaal 1
| 17:00 | The Ackermann Award 2014 (abstract) |
17:30-17:45 Session 102B: Workshop closing (PCCR)
Location: FH, Hörsaal 3
17:30-18:00 Session 102C: Joint session with WWV (VPT)
Location: FH, Seminarraum 107
| 17:30 | Formal Replay of Translation Validation for Highly Optimised C (abstract) |
18:00-18:10 Session 103A: Workshop Closing (STAST)
Location: MB, Seminarraum 212/232
18:15-19:15 Session 104A: Contributed talks A3 (LC)
Location: MB, Seminarraum 225
| 18:15 | A completeness theorem for general relativity (abstract) |
| 18:35 | More On Completion with Horn Filters (abstract) |
18:15-19:15 Session 104B: Contributed talks B3 (LC)
Location: MB, Prechtlsaal
| 18:15 | Predicative Mathematics via Safety Relations (abstract) |
| 18:35 | Natural Deduction in Renaissance Geometry (abstract) |
| 18:55 | Aristotle’s conception of demonstration and modern proof theory (abstract) |
18:15-19:15 Session 104C: Contributed talks C3 (LC)
Location: MB, Hörsaal 14
| 18:15 | Modelling Inference in Fiction (abstract) |
| 18:35 | Metalogical Extensions--Part II: First-order Consequences and Gödel (abstract) |
Saturday, July 19th, 2014
View this program: with abstractssession overviewtalk overview
08:30-09:30 Session 105: Invited Talk (Scott) (LATD and LC)
Location: MB, Festsaal
| 08:30 | Geometry without points (abstract) |
08:45-10:15 Session 106A: FLoC Panel (joint session of 10 meetings)
Chair:
Location: FH, Hörsaal 1
| 08:45 | FLoC Panel: Computational Complexity and Logic: Theory vs. Experiments (abstract) |
08:45-10:15 Session 106B: Contributed Talks: Causality and Inference (NMR)
Location: EI, EI 9
| 08:45 | Tableau vs. Sequent Calculi for Minimal Entailment (abstract) |
| 09:15 | Revisiting Chase Termination for Existential Rules and their Extension to Nonmonotonic Negation (abstract) |
| 09:45 | Causality in Databases: The Diagnosis and Repair Connections (abstract) |
09:35-10:15 Session 107A: Contributed talks A4 (LC)
Location: MB, Aufbaulabor
| 09:35 | Provability logics and proof-theoretic ordinals (abstract) |
| 09:55 | On Uniform Interpolation for the Guarded Fragment (abstract) |
09:35-10:15 Session 107B: Contributed talks B4 (LC)
Location: MB, Hörsaal 14A
| 09:35 | Degree spectra of sequences of structures (abstract) |
| 09:55 | Computability in generic extensions (abstract) |
09:35-10:15 Session 107C: Contributed talks C4 (LC)
Location: MB, GUT Schulungsraum
| 09:35 | Forcing with finite conditions and preserving CH (abstract) |
| 09:55 | Reflection principle of list-chromatic number of graphs (abstract) |
09:35-10:15 Session 107D: Contributed talks D4 (LC)
Location: MB, Seminarraum Kuppel
| 09:35 | Justifying proof-theoretic reflection principles (abstract) |
| 09:55 | C. I. Lewis' Influence on the Early Work of Emil Post (abstract) |
09:35-10:15 Session 107E: Contributed talks E4 (LC)
Location: MB, Hörsaal 14
| 09:35 | Indiscernible extraction and Morley sequences (abstract) |
| 09:55 | Consequences of the existence of ample generics and automorphism groups of homogeneous metric structures (abstract) |
09:45-10:15 Session 108A: Contributed Talk (LATD)
Location: MB, Festsaal
| 09:45 | A Semi-relevant, Paraconsistent Dual of {\L}ukasiewicz Logic (abstract) |
09:45-10:15 Session 108B: Contributed Talk (LATD)
Location: MB, Hörsaal 15
| 09:45 | Recent advances in the structural description of involutive FL$_e$-chains (abstract) |
10:15-10:45Coffee Break
10:45-13:05 Session 109A: Software Verification (CAV)
Chair:
Location: FH, Hörsaal 1
| 10:45 | The Spirit of Ghost Code (abstract) |
| 11:05 | SMT-based Model Checking for Recursive Programs (abstract) |
| 11:25 | Property-Directed Shape Analysis (abstract) |
| 11:45 | Shape Analysis via Second-Order Bi-Abduction (abstract) |
| 12:05 | ICE: A Robust Learning Framework for Synthesizing Invariants (abstract) |
| 12:25 | From Invariant Checking to Invariant Inference Using Randomized Search (abstract) |
| 12:45 | SMACK: Decoupling Source Language Details from Verifier Implementations (abstract) |
| 12:55 | Syntax-Guided Synthesis Competition Results (abstract) |
10:45-13:00 Session 109B: Conference Opening / Technical Session - Languages and Logic (ICLP)
Chair:
Location: FH, Hörsaal 8
| 10:45 | Conference Opening (abstract) |
| 11:00 | A Linear Logic Programming Language for Concurrent Programming over Graph Structures (abstract) |
| 11:30 | Lifted Variable Elimination for Probabilistic Logic Programming (abstract) |
| 12:00 | Minimum Model Semantics for Extensional Higher-order Logic Programming with Negation (abstract) |
| 12:30 | Abstract Diagnosis for tccp using a Linear Temporal Logic (abstract) |
10:45-13:00 Session 109C: Invited Talk & Higher-Order Logic (IJCAR)
Chair:
Location: FH, Hörsaal 5
| 10:45 | And-Or Tableaux for Fixpoint Logics with Converse: LTL, CTL, PDL and CPDL (abstract) |
| 11:45 | Unified Classical Logic Completeness: A Coinductive Pearl (abstract) |
| 12:15 | A Focused Sequent Calculus for Higher-Order Logic (abstract) |
10:45-12:45 Session 109D: FLoC Inter-Conference Topic: Security. Software Security (CAV and CSF)
Location: FH, Hörsaal 6
| 10:45 | Declarative Policies for Capability Control (abstract) |
| 11:15 | Portable Software Fault Isolation (abstract) |
| 11:45 | Certificates for Verifiable Forensics (abstract) |
| 12:15 | Information flow monitoring as abstract interpretation for relational logic (abstract) |
10:45-13:00 Session 109E: Invited Talk, Contributed Talks, and Poster Announcements (DL)
Location: EI, EI 7
| 10:45 | Invited Talk: Structured Data on the Web (or, a Personal Journey Away From and Back To Ontologies) (abstract) |
| 11:45 | On Faceted Search over Knowledge Bases (abstract) |
| 12:10 | Pushing the CFDnc Envelope (abstract) |
| 12:35 | OptiqueVQS: Visual Query Formulation for OBDA (abstract) |
| 12:38 | Visualization and management of mappings in ontology-based data access (progress report) (abstract) |
| 12:41 | Graphol: Ontology representation through diagrams (abstract) |
| 12:44 | Reducing global consistency to local consistency in Ontology-based Data Access - Extended Abstract (abstract) |
| 12:47 | Expressive Identification Constraints to Capture Functional Dependencies in Description Logics (abstract) |
| 12:50 | OBDA Using RL Reasoners and Repairing (abstract) |
| 12:53 | A Method to Develop Description Logic Ontologies Iteratively with Automatic Requirement Traceability (abstract) |
| 12:56 | Evaluation of Extraction Techniques for Ontology Excerpts (abstract) |
10:45-12:45 Session 109F: Invited Talk (Ghilardi) and Tutorial (Baader) (LATD)
Location: MB, Festsaal
| 10:45 | Step frames analysis in single- and multi-conclusion calculi (abstract) |
| 11:45 | Tutorial: Fuzzy Description Logics (Part 2) (abstract) |
10:45-12:15 Session 109G: Contributed Talks: Declarative Programming 3 (NMR)
Location: EI, EI 9
| 10:45 | Interactive Debugging of ASP Programs (abstract) |
| 11:15 | Semantics and Compilation of Answer Set Programming with Generalized Atoms (abstract) |
| 11:45 | A Family of Descriptive Approaches To Preferred Answer Sets (abstract) |
11:00-13:00 Session 110: Tutorial and invited talk (LC)
Location: MB, Prechtlsaal
| 11:00 | Tutorial on Classical Realizability and Forcing 3 (abstract) |
| 12:00 | Reductions in computability theory from a constructive point of view (abstract) |
12:15-13:00 Session 111: Contributed Talks: Systems 2 (NMR)
Location: EI, EI 9
| 12:15 | Integrating Declarative Programming and Probabilistic Graphical Models for Knowledge Representation and Reasoning in Robotics (abstract) |
| 12:37 | An ASP-Based Architecture for Autonomous UAVs in Dynamic Environments: Progress Report (abstract) |
13:00-14:30Lunch Break
14:00-16:00 Session 112: Invited talk and Karp prize winner (LC)
Location: MB, Prechtlsaal
| 14:00 | On a theorem of McAloon (abstract) |
| 15:00 | The Singular Cardinals Problem after 130 years or so (abstract) |
14:30-16:00 Session 113A: FLoC Inter-Conference Topic: Security (CAV and CSF)
Chair:
Location: FH, Hörsaal 1
| 14:30 | Synthesis of Masking Countermeasures against Side Channel Attacks (abstract) |
| 14:50 | Temporal Mode-Checking for Runtime Monitoring of Privacy Policies (abstract) |
| 15:10 | Program Verification through String Rewriting (abstract) |
| 15:30 | A Conference Management System with Verified Document Confidentiality (abstract) |
| 15:50 | VAC - Verifier of Administrative Role-based Access Control Policies (abstract) |
14:30-16:00 Session 113B: Invited Talk / Technical Session: Domain Specific Languages (ICLP)
Chair:
Location: FH, Hörsaal 8
| 14:30 | A Module System for Domain-Specific Languages (abstract) |
| 15:00 | Combinatorial Search With Picat (abstract) |
14:30-16:00 Session 113C: FLoC Inter-Conference Topic: SAT/SMT/QBF (CAV and IJCAR)
Chair:
Location: FH, Hörsaal 5
| 14:30 | SAT-based Decision Procedure for Analytic Pure Sequent Calculi (abstract) |
| 15:00 | A Unified Proof System for QBF Preprocessing (abstract) |
| 15:30 | The Fractal Dimension of SAT Formulas (abstract) |
14:30-16:00 Session 113D: Contributed Talks and Poster Announcements (DL)
Location: EI, EI 7
| 14:30 | Query Inseparability by Games (abstract) |
| 14:55 | Detecting Conjunctive Query Differences between ELHr-Terminologies using Hypergraphs (abstract) |
| 15:20 | Forgetting and Uniform Interpolation for ALC-Ontologies with ABoxes (abstract) |
| 15:45 | TBox abduction in ALC using a DL tableau (abstract) |
| 15:48 | Understandable Explanations in Description Logic (abstract) |
| 15:51 | WApproximation: computing approximate answers for ontological queries (abstract) |
| 15:54 | Towards Parallel Repair: An Ontology Decomposition-based Approach (abstract) |
| 15:57 | Analyzing the Complexity of Consistent Query Answering under Existential Rules (abstract) |
14:30-16:00 Session 113E: Contributed Talks (LATD)
Location: MB, Festsaal
| 14:30 | MV-algebras with product and the Pierce-Birkhoff conjecture (abstract) |
| 15:00 | On tensor product in Lukasiewicz logic (abstract) |
| 15:30 | On the Logic of Perfect MV-algebras (abstract) |
14:30-16:00 Session 113F: Contributed Talks (LATD)
Location: MB, Hörsaal 15
| 14:30 | Bases for admissible rules for fragments of RMt (abstract) |
| 15:00 | The Admissible Rules of Subframe Logics (abstract) |
| 15:30 | Admissible rules and almost structural completeness in some first-order modal logics (abstract) |
14:30-15:30 Session 113G: Invited Talk (NMR)
Location: EI, EI 9
| 14:30 | Revisiting Postulates for Inconsistency Measures (abstract) |
15:30-16:00 Session 114: Contributed Talk: Nonmonotonic Logics (NMR)
Location: EI, EI 9
| 15:30 | Implementing Default and Autoepistemic Logics via the Logic of GK (abstract) |
16:00-16:50 Session 115: Poster Session (with coffee break) (DL)
Location: EI, Foyer
16:00-16:30Coffee Break
16:30-17:10 Session 116A: Automata (CAV)
Chair:
Location: FH, Hörsaal 1
| 16:30 | From LTL to Deterministic Automata: A Safraless Compositional Approach (abstract) |
| 16:50 | Symbolic Visibly Pushdown Automata (abstract) |
16:30-18:00 Session 116B: Technical Session: Tabling and the Web (ICLP)
Chair:
Location: FH, Hörsaal 8
| 16:30 | Pengines: Web Logic Programming Made Easy (abstract) |
| 17:00 | Incremental Tabling for Knowledge Representation and Reasoning (abstract) |
| 17:30 | Tabling, Rational Terms, and Coinduction Finally Together! (abstract) |
16:30-17:00 Session 116C: FLoC Inter-Conference Topic: SAT/SMT/QBF (CAV and IJCAR)
Chair:
Location: FH, Hörsaal 5
| 16:30 | A Gentle Non-Disjoint Combination of Satisfiability Procedures (abstract) |
16:30-18:30 Session 116D: Invited talk and Gödel lecture (LC)
Location: MB, Prechtlsaal
| 16:30 | The problem of a model without collection and without exponentiation (abstract) |
| 17:30 | Computable structure theory and formulas of special forms (abstract) |
16:30-17:30 Session 116E: Invited Talk (CSF)
Location: FH, Hörsaal 6
| 16:30 | Towards a Zero-Software Trusted Computing Base for Extensible Systems (abstract) |
16:30-17:00 Session 116F: Contributed Talk (LATD)
Location: MB, Festsaal
| 16:30 | Separating intermediate predicate logics of well-founded and dually well-founded structures by monadic sentences (abstract) |
16:30-17:00 Session 116G: Contributed Talk (LATD)
Location: MB, Hörsaal 15
| 16:30 | A meta-Logic of multiple-conclusion rules (abstract) |
16:30-18:30 Session 116H: Contributed Talks: Argumentation 2 (NMR)
Location: EI, EI 9
| 16:30 | Compact Argumentation Frameworks (abstract) |
| 17:00 | Extension--based Semantics of Abstract Dialectical Frameworks (abstract) |
| 17:30 | Credulous and Skeptical Argument Games for Complete Semantics in Conflict Resolution based Argumentation (abstract) |
| 18:00 | On the Relative Expressiveness of Argumentation Frameworks, Normal Logic Programs and Abstract Dialectical Frameworks (abstract) |
16:50-18:30 Session 117: Contributed Talks (DL)
Location: EI, EI 7
| 16:50 | Pay-as-you-go Ontology Query Answering Using a Datalog Reasoner (abstract) |
| 17:15 | Hybrid Query Answering Over DL Ontologies (abstract) |
| 17:40 | Optimised Absorption for Expressive Description Logics (abstract) |
| 18:05 | Planning Problems for Graph Structured Data in Description Logics (abstract) |
17:10-18:00 Session 119A: Invited Talk (CAV)
Chair:
Location: FH, Hörsaal 1
| 17:10 | Designing and verifying molecular circuits and systems made of DNA (abstract) |
17:30-18:30 Session 120: FLoC Inter-Conference Topic: Security. Information Flow 1 (CAV and CSF)
Location: FH, Hörsaal 6
| 17:30 | On Dynamic Flow-sensitive Floating-Label Systems (abstract) |
| 18:00 | Noninterference under Weak Memory Models (abstract) |
18:30-18:45 Session 122: ORE Competition Results (DL)
Location: EI, EI 7
19:00-21:30 Session 122: VSL Reception 2 (VSL)
Location: University of Vienna, Arkadenhof
Sunday, July 20th, 2014
View this program: with abstractssession overviewtalk overview
08:45-10:15 Session 123: FLoC Plenary Talk (joint session of 10 meetings)
Chair:
Location: FH, Hörsaal 1
| 08:45 | FLoC Plenary Talk: Electronic voting: how logic can help? (abstract) |
Saturday, July 19th, 2014
View this program: with abstractssession overviewtalk overview
22:00-23:59 Session 123: VSL Student Reception 2 (VSL)
Location: Säulenhalle (Volksgarten)
Sunday, July 20th, 2014
View this program: with abstractssession overviewtalk overview
09:00-10:15 Session 124: Contributed Talks (DL)
Location: EI, EI 7
| 09:00 | Lower and Upper Approximations for Depleting Modules of Description Logic Ontologies (abstract) |
| 09:25 | Axiom Dependency Hypergraphs for Fast Modularisation and Atomic Decomposition (abstract) |
| 09:50 | DeaLing with Ontologies using CODs (abstract) |
09:15-10:15 Session 125A: Tutorial 1 - Ekaterina Ovchinnikova: Natural Language Understanding with World Knowledge and Inference (KR)
Location: EI, EI 10
| 09:15 | Natural Language Understanding with World Knowledge and Inference (Part I) (abstract) |
09:15-10:15 Session 125B: Tutorial 2 - Lawrence S. Moss: Dynamic Epistemic Logic and its Interaction with Knowledge Representation (KR)
Location: EI, EI 9
| 09:15 | Dynamic Epistemic Logic and Its Interaction with Knowledge Representation (Part I) (abstract) |
10:15-10:45Coffee Break
10:15-18:00 Session 126A: FLoC Olympic Games Big Screen: CASC Automated Theorem Proving System Competition (CASC-J7) (joint session of 10 meetings)
Location: FH, 2nd floor
| 10:15 | FLoC Olympic Games Big Screen: 7th IJCAR ATP System Competition (CASC-J7) (abstract) |
10:15-18:00 Session 126B: FLoC Olympic Games Big Screen: Termination Competition (termComp) (joint session of 10 meetings)
Location: FH, 2nd floor
| 10:15 | FLoC Olympic Games Big Screen: Termination Competition (termCOMP 2014) (abstract) |
10:45-12:45 Session 127A: Tutorial 1 (Continued) - Ekaterina Ovchinnikova: Natural Language Understanding with World Knowledge and Inference (KR)
Location: EI, EI 10
| 10:45 | Natural Language Understanding with World Knowledge and Inference (Part II) (abstract) |
10:45-12:45 Session 127B: Tutorial 2 (Continued) - Lawrence S. Moss: Dynamic Epistemic Logic and its Interaction with Knowledge Representation (KR)
Location: EI, EI 9
| 10:45 | Dynamic Epistemic Logic and Its Interaction with Knowledge Representation (Part II) (abstract) |
10:45-13:05 Session 127C: Model Checking and Testing (CAV)
Chair:
Location: FH, Hörsaal 1
| 10:45 | Engineering a Static Verification Tool for GPU Kernels (abstract) |
| 11:05 | Lazy Annotation Revisited (abstract) |
| 11:25 | Interpolating Property Directed Reachability (abstract) |
| 11:45 | Verifying Relative Error Bounds using Symbolic Simulation (abstract) |
| 12:05 | Regression Test Selection for Distributed Software Histories (abstract) |
| 12:25 | GPU-Based Graph Decomposition into Strongly Connected and Maximal End Components (abstract) |
| 12:45 | Software Verification in the Google App-Engine Cloud (abstract) |
| 12:55 | The nuXmv Symbolic Model Checker (abstract) |
10:45-13:00 Session 127D: Test of Time Award: 10 Years / Technical Session: Constraints and Constraint Handling Rules (ICLP)
Chair:
Location: FH, Hörsaal 8
| 10:45 | Test of Time Award: 10 Years - The Refined Operational Semantics of Constraint Handling Rules (abstract) |
| 11:30 | On Termination, Confluence and Consistent CHR-based Type Inference (abstract) |
| 12:00 | Exchanging Conflict Resolution in an Adaptable Implementation of ACT-R (abstract) |
| 12:30 | The P-Box CDF-Intervals: Reliable Constraint Reasoning with Quantifiable Information (abstract) |
10:45-13:00 Session 127E: Equational Reasoning (IJCAR)
Chair:
Location: FH, Hörsaal 5
| 10:45 | A Rewriting Strategy to Generate Prime Implicates in Equational Logic (abstract) |
| 11:15 | Finite Quantification in Hierarchic Theorem Proving (abstract) |
| 11:45 | Computing All Implied Equalities via SMT-based Partition Refinement (abstract) |
| 12:15 | Proving Termination of Programs Automatically with AProVE (abstract) |
10:45-12:45 Session 127F: Usable Security (CSF)
Location: FH, Hörsaal 6
| 10:45 | Who’s Afraid of Which Bad Wolf? A Survey of IT Security Risk Awareness (abstract) |
| 11:15 | How task familiarity and cognitive predispositions impact behavior in a security game of timing (abstract) |
| 11:45 | Panel: Usability (abstract) |
10:45-13:00 Session 127G: Contributed Talks (DL)
Location: EI, EI 7
| 10:45 | Controlled Query Evaluation over Lightweight Ontologies (abstract) |
| 11:10 | Query Rewriting under EL TBoxes: Efficient Algorithms (abstract) |
| 11:35 | Parallel OWL 2 RL Materialisation in Centralised, Main-Memory RDF Systems (abstract) |
| 12:00 | SPARQL Update for Materialized Triple Stores under DL-Lite_RDFS Entailment (abstract) |
| 12:25 | XPath for DL-Lite Ontologies (abstract) |
10:45-13:00 Session 127H (ICLP)
Location: FH, Seminarraum 107
| 10:45 | Test of Time Award: 10 Years (Talk presented at ICLP Main Conference) (abstract) |
| 11:45 | The Impact of Disjunction on Reasoning under Existential Rules (abstract) |
| 12:10 | Visualization of Constraint Handling Rules (abstract) |
| 12:35 | Reasoning with Probabilistic Logics (abstract) |
10:45-12:45 Session 127I (NCPROOFS)
Chair:
Location: FH, Seminarraum 104
| 10:45 | Construction and meaning (abstract) |
| 11:15 | Proof theory for ordered algebra: amalgamation and densification (abstract) |
| 11:45 | The Epsilon Calculus and Nonclassical Logics (abstract) |
| 12:15 | Automated and Interactive Theorem Proving for Modal Logics via embedding into Classical Higher-Order Logic (abstract) |
13:00-14:30Lunch Break
13:30-14:30 Session 128: DL Business Meeting (DL)
Location: EI, EI 7
14:30-16:00 Session 129A: Tutorial 3 - Alessio Lomuscio: Verification of Multi-Agent Systems against Epistemic Specifications (KR)
Location: EI, EI 10
| 14:30 | Verification of Multi-Agent Systems against Epistemic Specifications (Part I) (abstract) |
14:30-16:00 Session 129B: Tutorial 4 - Riccardo Rosati: Query Answering and Rewriting in Ontology-Based Data Access (KR)
Location: EI, EI 9
| 14:30 | Query Answering and Rewriting in Ontology-Based Data Access (Part I) (abstract) |
14:30-16:00 Session 129C: Biology and Hybrid Systems (CAV)
Chair:
Location: FH, Hörsaal 1
| 14:30 | Hardware Model Checking Competition 2014 CAV Edition (abstract) |
| 14:40 | Analyzing and Synthesizing Genomic Logic Functions (abstract) |
| 15:00 | Finding instability in biological models (abstract) |
| 15:20 | Invariant verification of nonlinear hybrid automata networks of cardiac cells (abstract) |
| 15:40 | Diamonds are a Girl's Best Friend: Partial Order Reduction for Timed Automata With Abstractions (abstract) |
14:30-16:00 Session 129D: Technical Session: Semantics (ICLP)
Chair:
Location: FH, Hörsaal 8
| 14:30 | On Cascade Products of Answer Set Programs (abstract) |
| 15:00 | Vicious Circle Principle and Logic Programs with Aggregates (abstract) |
| 15:30 | Causal Graph Justifications of Logic Programs (abstract) |
14:30-16:00 Session 129E: Verification (IJCAR)
Chair:
Location: FH, Hörsaal 5
| 14:30 | Locality Transfer: From Constrained Axiomatizations to Reachability Predicates (abstract) |
| 15:00 | Proving Termination and Memory Safety for Programs with Pointer Arithmetic (abstract) |
| 15:30 | QBF Encoding of Temporal Properties and QBF-Based Verification (abstract) |
14:30-16:00 Session 129F: Cryptography 1 (CSF)
Location: FH, Hörsaal 6
| 14:30 | Attribute-based Encryption for Access Control Using Elementary Operations (abstract) |
| 15:00 | Automated Analysis and Synthesis of Block-Cipher Modes of Operation (abstract) |
| 15:30 | Certified Synthesis of Efficient Batch Verifiers (abstract) |
14:30-16:00 Session 129G: FLoC Olympic Games: Answer Set Programming Modeling Competition 2014 (joint session of 10 meetings)
Location: FH, Hörsaal 2
| 14:30 | FLoC Olympic Games: Answer Set Programming Modeling Competition 2014 (abstract) |
14:30-16:00 Session 129H (ICLP)
Location: FH, Seminarraum 107
| 14:30 | Application of Methods for Syntax Analysis of Context-Free Languages to Query Evaluation of Logic Programs (abstract) |
| 14:55 | Bound Founded Answer Set Programming (abstract) |
| 15:20 | CDF-Intervals: A Reliable Framework to Reason about Data with Uncertainty (abstract) |
14:30-16:00 Session 129I (NCPROOFS)
Chair:
Location: FH, Seminarraum 104
| 14:30 | Introducing Substitution in Proof Theory (abstract) |
| 15:00 | Conditional logics: the quest for internal proof systems (abstract) |
| 15:30 | From Frame Properties to Hypersequent Rules in Modal Logics (abstract) |
16:00-16:30Coffee Break
16:30-18:00 Session 130A: Tutorial 3 (Continued) - Alessio Lomuscio: Verification of Multi-Agent Systems against Epistemic Specifications (KR)
Location: EI, EI 10
| 16:30 | Verification of Multi-Agent Systems against Epistemic Specifications (Part II) (abstract) |
16:30-18:00 Session 130B: Tutorial 4 (Continued) - Riccardo Rosati: Query Answering and Rewriting in Ontology-Based Data Access (KR)
Location: EI, EI 9
| 16:30 | Query Answering and Rewriting in Ontology-Based Data Access (Part II) (abstract) |
16:30-17:10 Session 130C: Hybrid Systems (CAV)
Chair:
Location: FH, Hörsaal 1
| 16:30 | Reachability Analysis of Hybrid Systems Using Symbolic Orthogonal Projections (abstract) |
| 16:50 | Verifying LTL properties of hybrid systems with K-liveness (abstract) |
16:30-18:00 Session 130D: ASP Competition Report / Technical Session - Knowledge Representation and Reasoning (ICLP)
Chair:
Location: FH, Hörsaal 8
| 16:30 | The Design of the Fifth Answer Set Programming Competition (abstract) |
| 17:00 | Simulating Dynamic Systems Using Linear Time Calculus Theories (abstract) |
| 17:30 | claspfolio 2: Advances in Algorithm Selection for Answer Set Programming (abstract) |
16:30-18:00 Session 130E: Proof Theory (IJCAR)
Chair:
Location: FH, Hörsaal 5
| 16:30 | Introducing quantified cuts in logic with equality (abstract) |
| 17:00 | Quati: An Automated Tool for Proving Permutation Lemmas (abstract) |
| 17:20 | A History-Based Theorem Prover for Intuitionistic Propositional Logic using Global Caching: IntHistGC System Description (abstract) |
| 17:40 | MleanCoP: A Connection Prover for First-Order Modal Logic (abstract) |
16:30-18:00 Session 130F: Cryptography 2 (CSF)
Location: FH, Hörsaal 6
| 16:30 | A Peered Bulletin Board for Robust Use in Verifiable Voting Systems (abstract) |
| 17:00 | From input private to universally composable secure multiparty computation primitives (abstract) |
| 17:30 | Malleable Signatures: New Definitions and Delegatable Anonymous Credentials (abstract) |
16:30-17:20 Session 130G (ICLP)
Location: FH, Seminarraum 107
| 16:30 | Model Revision Inference for Extensions of First Order Logic (abstract) |
| 16:55 | Logic Programming as Scripting Language for Bots in Computer Games (abstract) |
16:30-18:00 Session 130H (NCPROOFS)
Chair:
Location: FH, Seminarraum 104
| 16:30 | Admissibility and Exact Unification (abstract) |
| 17:00 | What can semantics do for proof theory: the case of Paraconsistent Logics (abstract) |
| 17:30 | Applications of Nested-Sequent Proof Systems for Modal Logics to the Craig Interpolation Property (abstract) |
17:10-18:00 Session 131: Invited Talk (CAV)
Chair:
Location: FH, Hörsaal 1
| 17:10 | Automated Testing (preliminary title) (abstract) |
17:20-18:00 Session 132: Panel Discussion (ICLP)
Location: FH, Seminarraum 107
18:00-19:00 Session 133: Business Meeting (CSF)
Location: FH, Hörsaal 6
18:30-21:30 Session 134: KR Reception followed by VSL Banquet 2 (KR)
Location: Schönbrunn
Monday, July 21st, 2014
View this program: with abstractssession overviewtalk overview
08:30-08:40 Session 135: KR Opening (KR)
Location: EI, EI 7
09:00-10:15 Session 137: Modeling Clinical Guidelines (KR4HC)
Chair:
Location: EI, EI 8
| 09:00 | Preliminary Result on Finding Treatments for Patients with Comorbidity (abstract) |
| 09:25 | Towards a Conceptual Model for Enhancing Reasoning about Clinical Guidelines: A case-study on Comorbidity (abstract) |
| 09:50 | Using First-Order Logic to Represent Clinical Practice Guidelines and to Mitigate Adverse Interactions (abstract) |
10:45-12:45 Session 138A: Description Logic 1 (KR)
Chair:
Location: EI, EI 7
| 10:45 | Polynomial Combined Rewritings for Existential Rules (abstract) |
| 11:15 | Nested Regular Path Queries in Description Logics (abstract) |
| 11:45 | Query Inseparability for Description Logic Knowledge Bases (abstract) |
| 12:15 | Answering Instance Queries Relaxed by Concept Similarity (abstract) |
10:45-12:45 Session 138B: Argumentation (KR)
Chair:
Location: EI, EI 9
| 10:45 | Characteristics of Multiple Viewpoints in Abstract Argumentation (abstract) |
| 11:15 | On the Revision of Argumentation Systems: Minimal Change of Arguments Statuses (abstract) |
| 11:45 | An SCC Recursive Meta-Algorithm for Computing Preferred Labellings in Abstract Argumentation (abstract) |
| 12:15 | A Dynamic Logic Framework for Abstract Argumentation (abstract) |
10:45-13:05 Session 138C: Games and Synthesis (CAV)
Chair:
Location: FH, Hörsaal 1
| 10:45 | Safraless Synthesis for Epistemic Temporal Specifications (abstract) |
| 11:05 | Minimizing Running Costs in Consumption Systems (abstract) |
| 11:25 | CEGAR for Qualitative Analysis of Probabilistic Systems (abstract) |
| 11:45 | Optimal Guard Synthesis for Memory Safety (abstract) |
| 12:05 | Don't sit on the fence: A static analysis approach to automatic fence insertion (abstract) |
| 12:25 | MCMAS-SLK: A Model Checker for the Verification of Strategy Logic Specifications (abstract) |
| 12:35 | Solving Games without Controllable Predecessor (abstract) |
| 12:45 | G4LTL-ST: Automatic Generation of PLC Programs (abstract) |
| 12:55 | SYNTCOMP - Synthesis Competition for Reactive Systems (abstract) |
10:45-13:00 Session 138D: Technical Communications: Track 1 - Knowledge Representation (ICLP)
Chair:
Location: FH, Hörsaal 8
| 10:45 | Transaction Logic with (Complex) Events (abstract) |
| 11:00 | Properties of Stable Model Semantics Extensions (abstract) |
| 11:15 | A Well-Founded Semantics for FOL-Programs (abstract) |
| 11:30 | On Strong and Default Negation in Answer-Set Program Updates (abstract) |
| 11:45 | C-Log: A Knowledge Representation Language of Causality (abstract) |
| 12:00 | ESmodels: An Epistemic Specification Solver (abstract) |
| 12:15 | Grounding Bound Founded Answer Set Programs (abstract) |
| 12:30 | An ASP-Based Architecture for Autonomous UAVs in Dynamic Environments (abstract) |
10:45-13:05 Session 138E: Modal and Temporal Reasoning (IJCAR)
Chair:
Location: FH, Hörsaal 5
| 10:45 | Optimal tableaux-based decision procedure for testing satisfiability in the Alternating-time temporal logic ATL+ (abstract) |
| 11:15 | dTL²: Differential Temporal Dynamic Logic with Nested Modalities for Hybrid Systems (abstract) |
| 11:45 | Axioms vs Hypersequent Rules with Context Restrictions: Theory and Applications (abstract) |
| 12:15 | Clausal Resolution for Modal Logics of Confluence (abstract) |
| 12:45 | Implementing Tableaux Calculi Using BDDs: BDDTab System Description (abstract) |
10:45-12:45 Session 138F: Protocol Verification (CSF)
Location: FH, Hörsaal 6
| 10:45 | Decidability for Lightweight Diffie-Hellman Protocols (abstract) |
| 11:15 | Modeling Diffie-Hellman Derivability for Automated Analysis (abstract) |
| 11:45 | Actor Key Compromise: Consequences and Countermeasures (abstract) |
| 12:15 | A Sound Abstraction of the Parsing Problem (abstract) |
10:45-13:00 Session 138G: Technical Communications: Track 2 - Systems and Paradigms (ICLP)
Chair:
Location: FH, Seminarraum 134
| 10:45 | Multi-criteria optimal planning for Energy policies in CLP (abstract) |
| 11:00 | Numerical Properties of Min-closed CSPs (abstract) |
| 11:15 | Clingo = ASP + Control (abstract) |
| 11:30 | Logic and Constraint Logic Programming for Distributed Constraint Optimization (abstract) |
| 11:45 | Guarding Corecursion in Logic Programming (abstract) |
| 12:00 | Adaptive MCMC-Based Inference in Probabilistic Logic Programs (abstract) |
| 12:15 | A Framework for Bottom-Up Simulation of SLD-Resolution (abstract) |
10:45-13:00 Session 138H: Technical Communications: Track 3 - Prolog (ICLP)
Chair:
Location: FH, Seminarraum 134A
| 10:45 | Joint Tabling of Logic Program Abductions and Updates (abstract) |
| 11:00 | A Simple and Efficient Lock-Free Hash Trie Design for Concurrent Tabling (abstract) |
| 11:15 | Towards Assertion-based Debugging of Higher-Order (C)LP Programs (abstract) |
| 11:30 | Analysis and Transformation Tools for Constrained Horn Clause Verification (abstract) |
| 11:45 | Towards an Efficient Prolog System by Code Introspection (abstract) |
| 12:00 | Customisable Handling of Java References in Prolog Programs (abstract) |
| 12:15 | Entanglement Patterns and Logic Programming Language Constructs (abstract) |
10:45-13:00 Session 138I: Exploring and Assessing Clinical Guidelines (KR4HC)
Chair:
Location: EI, EI 8
| 10:45 | Conformance Analysis of the Execution of Clinical Guidelines with Basic Medical Knowledge and Clinical Terminology (abstract) |
| 11:10 | Semantic Representation of Evidence-based Clinical Guidelines (abstract) |
| 11:35 | Real Rules, Real Data -- Addressing Challenges of Reasoning HIPAA Privacy Rule in Health Information Exchange (HIE) (abstract) |
| 12:00 | META-GLARE: a meta-system for defining your own CIG system: Architecture and Acquisition (abstract) |
| 12:15 | Assessment of Clinical Guideline Models Based on Metrics for Business Process Models (abstract) |
| 12:30 | An Algorithm for Guideline Transformation: from BPMN to PROforma (abstract) |
| 12:45 | A Process-oriented Methodology for Modelling Cancer Treatment Trial Protocols (abstract) |
12:45-13:00 Session 139A: 3 Short presentations of 5 minutes each. (KR)
Chair:
Location: EI, EI 7
| 12:45 | Rough Set Semantics for Identity on the Web (abstract) |
| 12:50 | Predicting Performance of OWL Reasoners: Locally or Globally? (abstract) |
| 12:55 | Concept Dissimilarity with Triangle Inequality (abstract) |
12:45-13:00 Session 139B: 3 Short presentations of 5 minutes each. (KR)
Chair:
Location: EI, EI 9
| 12:45 | Interval Methods for Judgment Aggregation in Argumentation (abstract) |
| 12:50 | How to Argue for Anything: Enforcing Arbitrary Sets of Labellings Using AFs (abstract) |
| 12:55 | A Psychology-Inspired Approach to Automated Narrative Text Comprehension (abstract) |
14:30-16:00 Session 140A: Planning, Strategies, Diagnosis 1 (KR)
Chair:
Location: EI, EI 7
| 14:30 | An Abstraction Technique for the Verification of Multi-Agent Systems Against ATL Specifications (abstract) |
| 15:00 | Reasoning about Equilibria in Game-like Concurrent Systems (abstract) |
| 15:30 | A Temporal Logic of Strategic Knowledge (abstract) |
14:30-16:00 Session 140B: Belief Revision and Nonmonotonicity 1 (KR)
Chair:
Location: EI, EI 9
| 14:30 | Belief Change and Semiorders (abstract) |
| 15:00 | On Egalitarian Belief Merging (abstract) |
| 15:30 | David Poole’s Specificity Revised (abstract) |
14:30-16:00 Session 140C: Concurrency (CAV)
Chair:
Location: FH, Hörsaal 1
| 14:30 | Automatic Atomicity Verification for Clients of Concurrent Data Structures (abstract) |
| 14:50 | Regression-free Synthesis for Concurrency (abstract) |
| 15:10 | Bounded Model Checking of Multi-Threaded C Programs via Lazy Sequentialization (abstract) |
| 15:30 | An SMT-Based Approach to Coverability Analysis (abstract) |
| 15:50 | LEAP: A Tool for the Parametrized Verification of Concurrent Datatypes (abstract) |
14:30-16:00 Session 140D: Best Doctoral Consortium Talk / Technical Session - Abduction (ICLP)
Chair:
Location: FH, Hörsaal 8
| 14:30 | Best Doctoral Consortium Talk (abstract) |
| 15:00 | A Measure of Arbitrariness in Abductive Explanations (abstract) |
| 15:30 | Contextual Abductive Reasoning with Side-Effects (abstract) |
14:30-16:00 Session 140E: FLoC Inter-Conference topic: SAT/SMT/QBF (CAV and IJCAR)
Chair:
Location: FH, Hörsaal 5
| 14:30 | Approximations for Model Construction (abstract) |
| 15:00 | A Tool that Incrementally Approximates Finite Satisfiability in Full Interval Temporal Logic (abstract) |
| 15:20 | StarExec: a Cross-Community Infrastructure for Logic Solving (abstract) |
| 15:40 | Skeptik [System Description] (abstract) |
14:30-16:00 Session 140F: Information Flow 2 (CSF)
Location: FH, Hörsaal 6
| 14:30 | Compositional Information-flow Security for Interactive Systems (abstract) |
| 15:00 | Stateful Declassification Policies for Event-Driven Programs (abstract) |
| 15:30 | Additive and multiplicative notions of leakage, and their capacities (abstract) |
14:30-15:30 Session 140G: Keynote: Stefania Montani: Knowledge-Intensive Medical Process Similarity (KR4HC)
Chair:
Location: EI, EI 8
| 14:30 | Knowledge-Intensive Medical Process Similarity (abstract) |
15:30-16:00 Session 141: Training and Learning (KR4HC)
Chair:
Location: EI, EI 8
| 15:30 | Development of Digital Repositories of Multimedia Learning Modules and Guideline-Driven Interactive Case Simulation Tools for New York State HIV/HCV/STD Clinical Education Initiative (abstract) |
| 15:45 | Training residents in the application of clinical guidelines for differential diagnosis of the most frequent causes of arterial hypertension with decision tables (abstract) |
16:00-16:50 Session 142: Modal Logic (IJCAR)
Chair:
Location: FH, Hörsaal 5
| 16:00 | Terminating Minimal Model Generation Procedures for Propositional Modal Logics (abstract) |
| 16:30 | COOL -- A Generic Satisfiability Checker For Coalgebraic Logics with Global Assumptions (System Description) (abstract) |
Sunday, July 20th, 2014
View this program: with abstractssession overviewtalk overview
19:00-21:30 Session 142: VSL Banquet 2 (VSL)
Location: Schönbrunn
Monday, July 21st, 2014
View this program: with abstractssession overviewtalk overview
16:30-17:30 Session 143A: Knowledge Representation and Reasoning 1 (KR)
Chair:
Location: EI, EI 7
| 16:30 | Generalized Multi-Context Systems (abstract) |
| 17:00 | Qualitative Spatial Representation and Reasoning in Angry Birds: the Extended Rectangle Algebra (abstract) |
16:30-17:30 Session 143B: Automated Reasoning and Computation 1 (KR)
Chair:
Location: EI, EI 9
| 16:30 | On OBDDs for CNFs of Bounded Treewidth (abstract) |
| 17:00 | Probabilistic Sentential Decision Diagrams (abstract) |
16:30-17:30 Session 143C: Invited Talk (CSF)
Location: FH, Hörsaal 6
| 16:30 | New Directions in Computed-Aided Cryptography (abstract) |
16:30-17:40 Session 143D: Linking Electronic Patient Records (KR4HC)
Chair:
Location: EI, EI 8
| 16:30 | Exploiting the Relation between Environmental Factors and Diseases: A Case Study on COPD (abstract) |
| 16:55 | Towards Linked Vital Registration Data for Reconstituting Families and Creating Longitudinal Health Histories (abstract) |
| 17:10 | A Logic-Based Framework for Medical Assessment Questionnaires (abstract) |
| 17:25 | Process Information and Guidance Systems in the Hospital (abstract) |
08:45-10:15 Session 144A: VSL Keynote Talk (VSL)
Chair:
Location: EI, EI 7 + EI 9, EI 10 + FH, Hörsaal 1
| 08:45 | VSL Keynote Talk: Ontology-Based Monitoring of Dynamic Systems (abstract) |
10:15-10:45Coffee Break
13:00-14:30Lunch Break
16:00-16:30Coffee Break
17:20-18:00 Session 145: CADE / FROCOS / TABLEAUX / IJCAR Business Meetings (IJCAR)
Chair:
Location: FH, Hörsaal 5
17:30-18:30 Session 146: 5' Talks (CSF)
Location: FH, Hörsaal 6
19:00-20:00 Session 148: Public Meeting of the Association for Logic Programming (ICLP)
Chair:
Location: FH, Hörsaal 8
Tuesday, July 22nd, 2014
View this program: with abstractssession overviewtalk overview
10:45-12:15 Session 149A: Description Logic 2 (KR)
Chair:
Location: EI, EI 7
| 10:45 | Exact Learning of Lightweight Description Logic Ontologies (abstract) |
| 11:15 | Finite Model Reasoning in Horn Description Logics (abstract) |
| 11:45 | Lightweight Description Logics and Branching Time: a Troublesome Marriage (abstract) |
Monday, July 21st, 2014
View this program: with abstractssession overviewtalk overview
19:00-20:00 Session 149A: VSL Public Lecture 2 (VSL)
Location: MB, Kuppelsaal
| 19:00 | VSL Public Lecture: Vienna Circle(s) - Between Philosophy and Science in Cultural Context (abstract) |
Tuesday, July 22nd, 2014
View this program: with abstractssession overviewtalk overview
10:45-12:15 Session 149B: Belief Revision and Nonmonotonicity 2 (KR)
Chair:
Location: EI, EI 9
| 10:45 | Belief Change and Base Dependence (abstract) |
| 11:15 | Justified Beliefs by Justified Arguments (abstract) |
| 11:45 | Belief Change Operations: A Short History of Nearly Everything, Told in Dynamic Logic of Propositional Assignments (abstract) |
10:45-13:05 Session 149C: FLoC Inter-Conference Topic: SAT/SMT/QBF (CAV and IJCAR)
Chair:
Location: FH, Hörsaal 1
| 10:45 | Monadic Decomposition (abstract) |
| 11:05 | A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions (abstract) |
| 11:25 | Bit-Vector Rewriting with Automatic Rule Generation (abstract) |
| 11:45 | A Tale of Two Solvers: Eager and Lazy Approaches to Bit-vectors (abstract) |
| 12:05 | AVATAR: The New Architecture for First-Order Theorem Provers (abstract) |
| 12:25 | Automating Separation Logic with Trees and Data (abstract) |
| 12:45 | A Nonlinear Real Arithmetic Fragment (abstract) |
| 12:55 | Yices 2.2 (abstract) |
10:45-13:00 Session 149D: Test of Time Award: 20 Years / Technical Session- Constraint Programming (ICLP)
Chair:
Location: FH, Hörsaal 8
| 10:45 | Test of Time Awards: 20 Years - CLP(Intervals) Revisited (abstract) |
| 11:30 | SUNNY: a Lazy Portfolio Approach for Constraint Solving (abstract) |
| 12:00 | Using Tabled Logic Programming to Solve the Petrobras Planning Problem (abstract) |
| 12:30 | A Proof Theoretic Study of Soft Concurrent Constraint Programming (abstract) |
10:45-13:00 Session 149E: Invited talk & Complexity (IJCAR)
Chair:
Location: FH, Hörsaal 5
| 10:45 | Structured Search and Learning (abstract) |
| 11:45 | The Complexity of Theorem Proving in Circumscription and Minimal Entailment (abstract) |
| 12:15 | Visibly Linear Temporal Logic (abstract) |
10:45-12:45 Session 149F: Network Security (CSF)
Location: FH, Hörsaal 6
| 10:45 | The Complexity of Estimating Systematic Risk in Networks (abstract) |
| 11:15 | Automated Generation of Attack Trees (abstract) |
| 11:45 | Mignis: A semantic based tool for firewall configuration (abstract) |
| 12:15 | Provably Sound Browser-Based Enforcement of Web Session Integrity (abstract) |
10:45-13:00 Session 149G (GeTFun)
Location: FH, Hörsaal 4
| 10:45 | Semi-implication and matrices (abstract) |
| 11:30 | Yoneda’s embedding and Post-completeness (abstract) |
| 12:00 | On the characterization of broadly truth-functional logics (abstract) |
| 12:30 | On non-deterministic fuzzy negations (abstract) |
12:15-13:05 Session 150A: 10 short presentations of 5 minutes each. (KR)
Chair:
Location: EI, EI 7
| 12:15 | On Redundant Topological Constraints (Extended Abstract) (abstract) |
| 12:20 | Knowledge Maps of Web Graphs (abstract) |
| 12:25 | On the Progression of Knowledge in Multiagent Systems (abstract) |
| 12:30 | Heuristic Guided Optimization for Propositional Planning (abstract) |
| 12:35 | Action Theories over Generalized Databases with Equality Constraints (Extended Abstract) (abstract) |
| 12:40 | Representing and Reasoning About Time Travel Narratives: Foundational Concepts (abstract) |
| 12:45 | Canonical Logic Programs are Succinctly Incomparable with Propositional Formulas (abstract) |
| 12:50 | Using Answer Set Programming for Solving Boolean Games (abstract) |
| 12:55 | ASP Encodings of Acyclicity Properties (abstract) |
| 13:00 | Stable Models of Multi-Valued Formulas: Partial vs. Total Functions (abstract) |
12:15-13:00 Session 150B: 9 short presentations of 5 minutes each. (KR)
Chair:
Location: EI, EI 9
| 12:15 | First-Order Default Logic Revisited (abstract) |
| 12:20 | Strong Equivalence of Non-monotonic Temporal Theories (abstract) |
| 12:25 | Belief Revision in the Propositional Closure of a Qualitative Algebra (abstract) |
| 12:30 | Minimal Change in AGM Revision for Non-classical Logics (abstract) |
| 12:35 | Toward a Knowledge Level Analysis of Forgetting (abstract) |
| 12:40 | An Abductive Reasoning Approach to the Belief-Bias Effect (abstract) |
| 12:45 | Tracking Beliefs and Intentions in the Werewolf Game (abstract) |
| 12:50 | Axioms .2 and .4 as Interaction Axioms (abstract) |
| 12:55 | Aggregative Deontic Detachment for Normative Reasoning (abstract) |
14:30-16:00 Session 151A: Reasoning about Actions and Processes 1 (KR)
Chair:
Location: EI, EI 7
| 14:30 | Decidable Reasoning in a Fragment of the Epistemic Situation Calculus (abstract) |
| 15:00 | Model Checking Unbounded Artifact-Centric Systems (abstract) |
| 15:30 | State-Boundedness for Decidability of Verification in Data-Aware Dynamic Systems (abstract) |
Monday, July 21st, 2014
View this program: with abstractssession overviewtalk overview
16:30-19:00 Session 151A: VSL Joint Award Ceremony 2 (VSL)
Chair:
Location: MB, Kuppelsaal
| 16:30 | FLoC Olympic Games Award Ceremony 2 (abstract) |
| 18:00 | Lifetime Achievement Award (abstract) |
| 18:10 | Lifetime Achievement Award (abstract) |
| 18:20 | EMCL Distinguished Alumni Award (abstract) |
| 18:30 | FLoC Closing Week 2 (abstract) |
Tuesday, July 22nd, 2014
View this program: with abstractssession overviewtalk overview
14:30-16:00 Session 151B: Automated Reasoning and Computation 2 (KR)
Chair:
Location: EI, EI 9
| 14:30 | Skolemization for Weighted First-Order Model Counting (abstract) |
| 15:00 | Analyzing the Computational Complexity of Abstract Dialectical Frameworks via Approximation Fixpoint Theory (abstract) |
| 15:30 | The Parameterized Complexity of Reasoning Problems Beyond NP (abstract) |
14:30-16:10 Session 151C: Bounds and Termination (CAV)
Chair:
Location: FH, Hörsaal 1
| 14:30 | A Simple and Scalable Static Analysis for Bound Analysis and Amortized Complexity Analysis (abstract) |
| 14:50 | Symbolic Resource Bound Inference for Functional Programs (abstract) |
| 15:10 | Proving Non-termination Using Max-SMT (abstract) |
| 15:30 | Termination Analysis by Learning Terminating Programs (abstract) |
| 15:50 | Causal Termination of Multi-threaded Programs (abstract) |
14:30-16:00 Session 151D: Invited Talk / Technical Session - Program Analysis (ICLP)
Chair:
Location: FH, Hörsaal 8
| 14:30 | (Quantified) Horn Constraint Solving for Program Verification and Synthesis (abstract) |
| 15:30 | Resource Usage Analysis of Logic Programs via Abstract Interpretation Using Sized Types (abstract) |
14:30-16:00 Session 151E: Description Logic (IJCAR)
Chair:
Location: FH, Hörsaal 5
| 14:30 | Count and Forget: Uniform Interpolation of SHQ-Ontologies (abstract) |
| 15:00 | Coupling Tableau Algorithms for Expressive Description Logics with Completion-Based Saturation Procedures (abstract) |
| 15:30 | EL-ifying Ontologies (abstract) |
14:30-15:30 Session 151F: Invited Talk (CSF)
Location: FH, Hörsaal 6
| 14:30 | Privacy in the Age of Augmented Reality (abstract) |
14:30-16:00 Session 151G (GeTFun)
Location: FH, Hörsaal 4
| 14:30 | Non truth-functional bivalent logics extending classical bivalent logics (abstract) |
| 15:00 | A survey on Suszko’s Thesis and its formal developments (abstract) |
| 15:30 | Effective first-order reasoning about incomplete and inconsistent information (abstract) |
15:30-16:00 Session 152: Privacy 1 (CSF)
Location: FH, Hörsaal 6
| 15:30 | Balancing Societal Security and Individual Privacy: Accountable Escrow System (abstract) |
16:30-18:00 Session 153A: Technical Session - Answer Set Programming (ICLP)
Chair:
Location: FH, Hörsaal 8
| 16:30 | Dynamic Consistency Checking in Goal-Directed Answer Set Programming (abstract) |
| 17:00 | Anytime Computation of Cautious Consequences in Answer Set Programming (abstract) |
| 17:30 | Efficient Computation of the Well-Founded Semantics over Big Data (abstract) |
16:30-18:10 Session 153B: Knowledge Representation & Reasoning (IJCAR)
Chair:
Location: FH, Hörsaal 5
| 16:30 | The Bayesian Description Logic BEL (abstract) |
| 17:00 | Otter proofs of theorems in Tarskian geometry (abstract) |
| 17:30 | NESCOND: an Implementation of Nested Sequent Calculi for Conditional Logics (abstract) |
| 17:50 | Knowledge Engineering for Large Ontologies with Sigma KEE 3.0 (abstract) |
16:30-18:30 Session 153C: Privacy 2 (CSF)
Location: FH, Hörsaal 6
| 16:30 | TUC: Time-sensitive and Modular Analysis of Anonymous Communication (abstract) |
| 17:00 | Differential Privacy: An Economic Method for Choosing Epsilon (abstract) |
| 17:30 | Proving differential privacy in Hoare logic (abstract) |
| 18:00 | Surveillance and Privacy (abstract) |
16:30-18:00 Session 153E (GeTFun)
Location: FH, Hörsaal 4
| 16:30 | Separating truth and proof in the Logic of Proofs (abstract) |
16:40-17:30 Session 154: Abstraction (CAV)
Chair:
Location: FH, Hörsaal 1
| 16:40 | Counterexample to Induction-Guided Abstraction-Refinement (CTIGAR) (abstract) |
| 17:00 | Unbounded Scalable Verification Based on Approximate Property-Directed Reachability and Datapath Abstraction (abstract) |
| 17:20 | QUICr: A Reusable Library for Parametric Abstraction of Sets and Numbers (abstract) |
17:30-18:30 Session 156: Business Meeting (CAV)
Location: FH, Hörsaal 1
08:45-10:15 Session 156: VSL Keynote Talk (VSL)
Chair:
Location: EI, EI 7 + EI 9, EI 10 + FH, Hörsaal 1
| 08:45 | VSL Keynote Talk: Verification of Computer Systems with Model Checking (abstract) |
10:15-10:45Coffee Break
13:00-14:30Lunch Break
16:00-16:30Coffee Break
18:00-19:00 Session 157: SIGLOG Meeting (FLoC and VSL)
Location: FH, Hörsaal 8
19:30-21:30 Session 158: KR Banquet (KR)
Location: Naturhistorisches Museum
Wednesday, July 23rd, 2014
View this program: with abstractssession overviewtalk overview
08:45-10:15 Session 159A: Invited talks: Scott; Benveniste (RS)
Location: FH, Zeichensaal 3
| 08:45 | Stochastic Lambda Calculus - An Appeal (abstract) |
| 09:30 | Contracts for System Design (abstract) |
08:45-09:45 Session 159B: Partial/Semi-Formal Assurance and Verification (VeriSure)
Location: FH, Hörsaal 2
| 08:45 | Balancing the Formal and Informal in Safety Case Arguments (abstract) |
| 09:15 | Quantification of Verification Progress (abstract) |
08:45-10:15 Session 159C: Invited Talk (Guet); Contributed Talk (Stewart) (HSB)
Location: FH, Seminarraum 101A
| 08:45 | Synthetic Systems Biology (abstract) |
| 09:45 | FM-Sim : A Hybrid Protocol Simulator of Fluorescence Microscopy Neuroscience Assays with Integrated Bayesian Inference (abstract) |
08:45-10:15 Session 159D: Superposition I (PAAR)
Location: FH, Hörsaal 7
| 08:45 | A Deductive-Complete Constrained Superposition Calculus for Ground Flat Equational Clauses (abstract) |
| 09:15 | Invited talk: Hierarchic Superposition Revisited (abstract) |
08:45-10:15 Session 159E (GeTFun)
Location: FH, Hörsaal 4
| 08:45 | From display logic to nested sequents via residuated frames (abstract) |
| 09:30 | First-order non-classical logics: an order-based approach (abstract) |
08:45-10:15 Session 159F: Invited Talk and Contributed Talk (ARW-DT, VERIFY and WING)
Location: FH, Hörsaal 3
| 08:45 | Chasing the Perfect Specification (abstract) |
| 09:45 | Typed First-Order Logic (abstract) |
08:55-10:15 Session 160A: Introduction & Invited Talk 1 (SYNT)
Location: FH, Seminarraum 101B
| 08:55 | Automating Deductive Synthesis with Leon (Invited Talk) (abstract) |
08:55-09:00 Session 160B: Opening (FRIDA)
Location: FH, Seminarraum 104
09:00-10:15 Session 161A: KR Invited Talk: Tony Cohn (Knowledge Representation meets Computer Vision: From Pixels to Symbolic Activity Descriptions) (KR)
Chair:
Location: EI, EI 7
| 09:00 | Knowledge Representation Meets Computer Vision: From Pixels to Symbolic Activity Descriptions (abstract) |
09:00-10:15 Session 161B: Invited talk: Joseph Halpern (FRIDA)
Location: FH, Seminarraum 104
| 09:00 | Beyond Nash Equilibrium: Solution Concepts for the 21st Century (abstract) |
09:00-09:15 Session 161C: Opening (PRUV)
Location: FH, Seminarraum 107
09:10-09:25 Session 162: Opening Remarks (ASPOCP)
Location: FH, Seminarraum 138A
09:15-10:15 Session 163: Invited Talk (PRUV)
Location: FH, Seminarraum 107
09:25-10:15 Session 164: Theory (ASPOCP)
Location: FH, Seminarraum 138A
| 09:25 | Supported Semantics for Modular Systems (abstract) |
| 09:50 | Infinitary Equilibrium Logic (abstract) |
09:45-10:15 Session 165: Discussion (VeriSure)
Location: FH, Hörsaal 2
10:15-10:45Coffee Break
10:45-13:00 Session 166A: Description Logic 3 (KR)
Chair:
Location: EI, EI 7
| 10:45 | Stable Model Semantics for Guarded Existential Rules and Description Logics (abstract) |
| 11:15 | Practical Uniform Interpolation and Forgetting for ALC TBoxes with Applications to Logical Difference (abstract) |
| 11:45 | Nominal Schemas in Description Logics: Complexities Clarified (abstract) |
| 12:15 | Decidable Gödel Description Logics without the Finitely-Valued Model Property (abstract) |
10:45-13:00 Session 166B: Reasoning about Actions and Processes 2 (KR)
Chair:
Location: EI, EI 9
| 10:45 | A First-Order Semantics for Golog and ConGolog under a Second-Order Induction Axiom for Situations (abstract) |
| 11:15 | How To Progress Beliefs in Continuous Domains (abstract) |
| 11:45 | Transforming Situation Calculus Action Theories for Optimised Reasoning (abstract) |
| 12:15 | Forgetting in Action (abstract) |
10:45-11:35 Session 166C: Semantics (ASPOCP)
Location: FH, Seminarraum 138A
| 10:45 | A Refinement of the Language of Epistemic Specifications (abstract) |
| 11:10 | Epistemic Logic Programs with Sorts (abstract) |
10:45-13:00 Session 166D: Invited talks: Hoare; Grumberg; Kwiatkowska; Maoz (RS)
Location: FH, Zeichensaal 3
| 10:45 | A Geometric Model for Concurrent Programming (abstract) |
| 11:30 | Automated Abstraction-Refinement for the Verification of Behavioral UML Models (abstract) |
| 12:00 | Probabilistic model checking at the nanoscale: from molecular signalling to molecular walkers (abstract) |
| 12:30 | A Short Story on Scenarios (abstract) |
10:45-12:45 Session 166E: Contributed Talks 1 (SYNT)
Location: FH, Seminarraum 101B
| 10:45 | Synthesis of a simple self stabilizing system (abstract) |
| 11:15 | Program Synthesis and Linear Operator Semantics (abstract) |
| 11:45 | How to Handle Assumptions in Synthesis (abstract) |
| 12:15 | Symblicit algorithms for optimal strategy synthesis in monotonic Markov decision processes (abstract) |
10:45-13:00 Session 166F: Vampire Tutorial and Regular Talks (Vampire)
Chair:
Location: FH, Seminarraum 134
| 10:45 | First-Order Theorem Proving with Vampire (abstract) |
| 12:00 | Proofs in Vampire (abstract) |
| 12:30 | Playing with AVATAR (abstract) |
10:45-11:45 Session 166G: Making Hard Assurance Problems Feasible (VeriSure)
Location: FH, Hörsaal 2
| 10:45 | Introducing Semi-Formal Specifications into a Distributed Development Process (abstract) |
| 11:15 | Witnessing an SSA Transformation (abstract) |
10:45-13:00 Session 166H: Tutorial (Donze), Collaboration Success Stories (Fanchon, de Jong, Halasz) (HSB)
Location: FH, Seminarraum 101A
| 10:45 | Tutorial: Simulation-based Parameter Synthesis in Systems Biology (abstract) |
| 11:30 | Collaboration success stories: Modeling Iron Homeostasis in Mammalian Cells (with J.M. Moulis) (abstract) |
| 12:00 | Collaboration success stories: Control of Gene Expression in E.coli (with Hans Geiselman) (abstract) |
| 12:30 | Collaboration success stories: Membrane-bound Receptor Imaging, Data Analysis and Model Building (with J.S. Edwards) (abstract) |
10:45-13:00 Session 166I: Meta-methods for theorem proving (PAAR)
Location: FH, Hörsaal 7
| 10:45 | Automated Theorem Proving using the TPTP Process Instruction Language (abstract) |
| 11:15 | The Efficiency of Automated Theorem Proving by Translation to Less Expressive Logics (abstract) |
| 11:45 | Machine Learner for Automated Reasoning 0.4 and 0.5 (abstract) |
| 12:15 | BliStr: The Blind Strategymaker (abstract) |
10:45-13:00 Session 166J: Contributed Talks 1 (FRIDA)
Location: FH, Seminarraum 104
| 10:45 | Towards binary circuit models that faithfully reflect physical (un)solvability (abstract) |
| 11:15 | Mechanical Verification of a Constructive Proof for FLP (abstract) |
| 11:45 | Having SPASS with Pastry and TLA+ (abstract) |
| 12:15 | Concurrent Data Structures: Semantics and (Quantitative) Relaxation (abstract) |
10:45-13:00 Session 166K (GeTFun)
Location: FH, Hörsaal 4
| 10:45 | Broadly truth-functional logics through classical lenses (abstract) |
| 11:30 | Natural deduction for non-deterministic finite-valued logics (abstract) |
| 12:00 | The procedural understanding of meaning and compositionality in formal semantics (abstract) |
| 12:30 | Semi-BCI-algebras (abstract) |
10:45-12:15 Session 166L: Contributed Talks (ARW-DT, VERIFY and WING)
Location: FH, Hörsaal 3
| 10:45 | Reasoning About Vote Counting Schemes Using Light-weight and Heavy-weight Methods (abstract) |
| 11:15 | Introducing a Sound Deductive Compilation Approach (abstract) |
| 11:45 | Verifying safety properties of Artificial General Intelligence: The ultimate safety-critical system? (abstract) |
10:45-12:15 Session 166M: Vagueness to some degree (PRUV)
Location: FH, Seminarraum 107
| 10:45 | In Which Sense Is Fuzzy Logic a Logic for Vagueness? (abstract) |
| 11:15 | Stable Models of Fuzzy Propositional Formulas (abstract) |
| 11:45 | Towards a Logic of Dilation (abstract) |
10:50-11:00 Session 167: Opening (ARQNL)
Location: FH, Seminarraum 138C
| 10:50 | ARQNL Workshop - Opening (abstract) |
11:00-13:00 Session 168: First-Order Modal Logics, Quantified Dynamic and Temporal Logic, Problem Libraries (ARQNL)
Location: FH, Seminarraum 138C
| 11:00 | Coalescing: Syntactic Abstraction for Reasoning in First-Order Modal Logics (abstract) |
| 11:30 | A Logic for Verifying Metric Temporal Properties in Distributed Hybrid Systems (abstract) |
| 12:00 | Problem Libraries for Non-Classical Logics (abstract) |
| 12:30 | HOL Provers for First-order Modal Logics --- Experiments (abstract) |
11:35-11:45 Session 169: Short Break (ASPOCP)
Location: FH, Seminarraum 138A
11:45-13:00 Session 170A: Dynamic Domains and Action Languages (ASPOCP)
Location: FH, Seminarraum 138A
| 11:45 | Temporal Stable Models are LTL-representable (abstract) |
| 12:10 | Applying Action Language BC with Hierarchical Domain Abstraction to Mobile Robots (abstract) |
| 12:35 | Action Language BC+: Preliminary Report (abstract) |
11:45-12:15 Session 170B: Discussion (VeriSure)
Location: FH, Hörsaal 2
12:15-13:00 Session 171A: Human Interfaces and Medical Devices, and discussion (VeriSure)
Location: FH, Hörsaal 2
| 12:15 | Human-Computer Interaction and the Formal Certification and Assurance of Medical Devices: The CHI+MED Project (abstract) |
12:15-13:15 Session 171B: Verification: Contributed Talks (ARW-DT, VERIFY and WING)
Location: FH, Hörsaal 3
| 12:15 | Reasoning about Auctions (abstract) |
| 12:45 | Automating Regression Verification (abstract) |
13:00-14:30Lunch Break
14:30-16:00 Session 172A: Knowledge Representation and Reasoning 2 (KR)
Chair:
Location: EI, EI 7
| 14:30 | Certain Answers as Objects and Knowledge (abstract) |
| 15:00 | Tackling Winograd Schemas by Formalizing Relevance Theory in Knowledge Graphs (abstract) |
| 15:30 | Simultaneous Learning and Prediction (abstract) |
14:30-16:00 Session 172B: Reports from the Field (KR)
Chair:
Location: EI, EI 9
| 14:30 | Computing Narratives of Cognitive User Experience for Building Design Analysis: KR for Industry Scale Computer-Aided Architecture Design (abstract) |
| 15:00 | Tweety: A Comprehensive Collection of Java Libraries for Logical Aspects of Artificial Intelligence and Knowledge Representation (abstract) |
| 15:30 | SmartPM: An Adaptive Process Management System through Situation Calculus, IndiGolog, and Classical Planning (abstract) |
14:30-16:00 Session 172C: Invited talks: Henzinger; Kugler; Fisher (RS)
Location: FH, Zeichensaal 3
| 14:30 | Quantitative Reactive Modeling (abstract) |
| 15:00 | On Statecharts, Scenarios and Biological Modeling (abstract) |
| 15:30 | Cancer as Reactivity (abstract) |
14:30-16:00 Session 172D: Invited Talk by Jasmin Blanchette, Discussions (Vampire)
Chair:
Location: FH, Seminarraum 134
| 14:30 | My Life with an Automatic Theorem Prover (abstract) |
| 15:30 | Discussions (abstract) |
14:30-16:00 Session 172E: Common Logic, Higher-Order Nominal Modal Logic, First-Order Intuitionistic Logic (ARQNL)
Location: FH, Seminarraum 138C
| 14:30 | Proof Support for Common Logic (abstract) |
| 15:00 | Embedding of Quantified Higher-Order Nominal Modal Logic into Classical Higher-Order Logic (abstract) |
| 15:30 | Dialogues for proof search (abstract) |
14:30-15:30 Session 172F: Assurance for Secure Systems (VeriSure)
Location: FH, Hörsaal 2
| 14:30 | Implicit Assumptions in a Model for Separation Kernels (abstract) |
| 15:00 | Assurance and Verification of Security Properties (abstract) |
14:30-16:00 Session 172G: Tutorial (Antoniotti), Contributed Talk (Dreossi) (HSB)
Location: FH, Seminarraum 101A
| 14:30 | Tutorial: The Cellular Potts Model (abstract) |
| 15:30 | Parameter Synthesis using Parallelotopic Enclosure and Applications to Epidemic Models (abstract) |
14:30-16:00 Session 172H: Superposition II (PAAR)
Location: FH, Hörsaal 7
| 14:30 | A Model Guided Instantiation Heuristic for the Superposition Calculus with Theories (abstract) |
| 15:00 | Logtk : A Logic ToolKit for Automated Reasoning and its Implementation (abstract) |
| 15:30 | Polymorphic+Typeclass Superposition (abstract) |
14:30-15:45 Session 172I: Invited talk: Ahmed Bouajjani (FRIDA)
Location: FH, Seminarraum 104
| 14:30 | On Checking Correctness of Concurrent Data Structures (abstract) |
14:30-16:00 Session 172J: Contributed Talks (ARW-DT and WING)
Location: FH, Hörsaal 3
| 14:30 | A Theorem Prover Backed Approach to Array Abstraction (abstract) |
| 15:00 | ALICe: A Framework to Improve Affine Loop Invariant Computation (abstract) |
| 15:30 | Loop Invariants by Mutation, Dynamic Validation, and Static Checking (abstract) |
14:30-16:00 Session 172K (GeTFun)
Location: FH, Hörsaal 4
| 14:30 | An intuitionistic ALC description default logic (abstract) |
| 15:00 | An infinitary deduction system for CTL* (abstract) |
| 15:30 | Modal functions as moody truth-functions (abstract) |
14:30-16:00 Session 172L: Reasoning for Vagueness perhaps (PRUV)
Location: FH, Seminarraum 107
| 14:30 | Similarity-based Relaxed Instance Queries in EL++ (abstract) |
| 15:00 | Resolution and Clause Learning for Multi-Valued CNF Formulas (abstract) |
| 15:30 | Many-valued Horn Logic is Hard (abstract) |
14:45-16:00 Session 173A: Applications (ASPOCP)
Location: FH, Seminarraum 138A
| 14:45 | Query Answering in Resource-Based Answer Set Semantics (abstract) |
| 15:10 | Declarative Encodings of Acyclicity Properties (abstract) |
| 15:35 | Computing Secure Sets in Graphs using Answer Set Programming (abstract) |
14:45-16:00 Session 173B: Invited Talk 2 (SYNT)
Location: FH, Seminarraum 101B
| 14:45 | Synthesis using EF-SMT Solvers (Invited Talk) (abstract) |
15:30-16:00 Session 174: Discussion (VeriSure)
Location: FH, Hörsaal 2
16:00-16:30Coffee Break
16:30-18:00 Session 175A: Planning, Strategies and Diagnosis 2 (KR)
Chair:
Location: EI, EI 7
| 16:30 | Diagnostic Problem Solving via Planning with Ontic and Epistemic Goals (abstract) |
| 17:00 | A Formalization of Programs in First-Order Logic with a Discrete Linear Order (abstract) |
| 17:30 | Satisfiability of Alternating-time Temporal Epistemic Logic through Tableaux (abstract) |
16:30-18:00 Session 175B: Uncertainty (KR)
Chair:
Location: EI, EI 9
| 16:30 | Linear Programs for Measuring Inconsistency in Probabilistic Logics (abstract) |
| 17:00 | Reasoning with Uncertain Inputs in Possibilistic Networks (abstract) |
| 17:30 | Relational Logistic Regression (abstract) |
16:30-18:10 Session 175C: Systems, Tools, and Frameworks (ASPOCP)
Location: FH, Seminarraum 138A
| 16:30 | ``Are Preferences Giving You a Headache?'' - ``Take asprin!'' (abstract) |
| 16:55 | On the Implementation of Weak Constraints in WASP (abstract) |
| 17:20 | Interactive Query-based Debugging of ASP Programs (abstract) |
| 17:45 | Computing Answer Sets for Monadic Logic Programs via MapReduce (abstract) |
16:30-18:15 Session 175D: Invited talks: Clarke; Dershowitz; Vardi (RS)
Location: FH, Zeichensaal 3
| 16:30 | Model Checking Hybrid Systems (abstract) |
| 17:15 | Towards a General Model of Evolving Interaction (abstract) |
| 17:45 | Compositional Temporal Synthesis (abstract) |
16:30-18:00 Session 175E: Special Session on Competitions: SyGuS & SyntComp (SYNT)
Location: FH, Seminarraum 101B
| 16:30 | The 1st Syntax-Guided Synthesis Competition (SyGuS) (abstract) |
| 17:15 | The 1st Synthesis Competition for Reactive Systems (SyntComp) (abstract) |
16:30-18:00 Session 175F: Vampire Regular Talks (Vampire)
Chair:
Location: FH, Seminarraum 134
| 16:30 | SAT solving experiments in Vampire (abstract) |
| 17:00 | First Class Boolean Type in First-Order Theorem Proving and TPTP (abstract) |
| 17:30 | Reasoning in First-Order Theories with Extensionality (abstract) |
16:30-18:00 Session 175G: Logic with Partial Functions, First-Order Sequent Logics, Discussion (ARQNL)
Location: FH, Seminarraum 138C
| 16:30 | Theorem Proving for Logic with Partial Functions Using Kleene Logic and Geometric Logic (abstract) |
| 17:00 | Computer-oriented inference search in first-order sequent logics (abstract) |
| 17:30 | Open Discussion (abstract) |
16:30-17:30 Session 175H: Assurance and Probability (VeriSure)
Location: FH, Hörsaal 2
| 16:30 | A Graphical Notation for Probabilistic Specifications (abstract) |
| 17:00 | Assurance of some system reliability characteristics in formal design verification (abstract) |
16:30-18:00 Session 175I: Evaluation, Sets, Tableaux (ARW-DT and WING)
Location: FH, Hörsaal 3
| 16:30 | Towards Evaluating the Usability of Interactive Theorem Provers (abstract) |
| 17:00 | Combined Reasoning with Sets and Aggregation Functions (abstract) |
| 17:30 | Tableau Development for a Bi-Intuitionistic Tense Logic (abstract) |
16:30-18:00 Session 175J: Proving and Disproving (PAAR)
Location: FH, Hörsaal 7
| 16:30 | Beagle as a HOL4 external ATP method (abstract) |
| 17:00 | Razor: Provenance and Exploration in Model-Finding (abstract) |
| 17:30 | SGGS Theorem Proving: an Exposition (abstract) |
16:30-18:30 Session 175K: Contributed Talks 2 (FRIDA)
Location: FH, Seminarraum 104
| 16:30 | A Logic-based Framework for Verifying Consensus Algorithms (abstract) |
| 17:00 | Monotonic Abstraction Techniques: from Parametric to Software Model Checking (abstract) |
| 17:30 | Model Checking Distributed Consensus Algorithms (abstract) |
| 18:00 | Model-Checking of Parameterized Timed-Systems (abstract) |
16:30-18:00 Session 175L (GeTFun)
Location: FH, Hörsaal 4
| 16:30 | On subexponentials, focusing and modalities in concurrent systems (abstract) |
| 17:00 | Quantum state transformations and distributed temporal logic (abstract) |
| 17:30 | Combining non-determinism and context awareness in consistency restoration systems (abstract) |
16:30-18:00 Session 175M: Favorite reasoning procedures for preferences (PRUV)
Location: FH, Seminarraum 107
| 16:30 | Learning Preferences for Collaboration (abstract) |
| 17:00 | Computing k-Rank Answers with Ontological CP-Nets (abstract) |
| 17:30 | Multi-Attribute Decision Making using Weighted Description Logics (abstract) |
17:30-18:00 Session 176: Discussion and Closing (VeriSure)
Location: FH, Hörsaal 2
18:00-19:00 Session 177: Business Meeting (ARW-DT)
Location: FH, Hörsaal 3
18:10-18:20 Session 178: Closing (ASPOCP)
Location: FH, Seminarraum 138A
18:30-19:45 Session 179: KR Great Moments Invited Talk : Sheila McIlraith (Situation Calculus: The last 15 years) (KR)
Chair:
Location: EI, EI 7
| 18:30 | Situation Calculus: The Last 15 Years (abstract) |
19:45-20:00 Session 180: KR Awards (KR)
Location: EI, EI 7
Thursday, July 24th, 2014
View this program: with abstractssession overviewtalk overview
08:45-10:15 Session 181A: PRIVACY, SAT (ARW-DT)
Location: FH, Hörsaal 3
| 08:45 | Defining privacy is supposed to be easy (abstract) |
| 09:45 | Extended Resolution in Modern SAT Solving (abstract) |
08:45-10:15 Session 181B: nvited Talk (Harel), Contributed Talk (Brazma) (HSB)
Location: FH, Seminarraum 101A
| 08:45 | The Whole Organism Challenge (abstract) |
| 09:45 | Modeling and analysis of qualitative behavior of gene regulatory networks (abstract) |
09:00-10:15 Session 182A: KR Invited Talk: Georg Gottlob (Datalog+/- : Questions and Answers) (KR)
Location: EI, EI 7
| 09:00 | Datalog+/–: Questions and Answers (abstract) |
09:00-10:15 Session 182B: Invited Talk 3 (SYNT)
Location: FH, Seminarraum 101B
| 09:00 | Automatic Device Driver Synthesis Project: a Work-in-Progress Report (Invited Talk) (abstract) |
09:00-10:15 Session 182C: Invited talk: Alexander Shvartsman (FRIDA)
Location: FH, Seminarraum 104
| 09:00 | Specifying, Reasoning About, Optimizing, and Implementing Atomic Data Services for Distributed Systems (abstract) |
09:00-10:15 Session 182D: Invited Talk: Gabriele Kern-Isberner (PRUV)
Location: FH, Seminarraum 107
| 09:00 | TBA (abstract) |
10:15-10:45Coffee Break
10:45-12:45 Session 183A: Logic Programming and Answer Set Programming (KR)
Chair:
Location: EI, EI 7
| 10:45 | Logic Programs with Ordered Disjunction: First-order Semantics and Expressiveness (abstract) |
| 11:15 | Constructive Negation in Extensional Higher-Order Logic Programming (abstract) |
| 11:45 | The Well-Founded Semantics Is the Principle of Inductive Definition, revisited (abstract) |
| 12:15 | The Semantics of Gringo and Infinitary Propositional Formulas (abstract) |
10:45-12:45 Session 183B: Causality and Rationality (KR)
Chair:
Location: EI, EI 9
| 10:45 | Dynamic Causal Calculus (abstract) |
| 11:15 | Appropriate Causal Models and Stability of Causation (abstract) |
| 11:45 | Axiomatizing Rationality (abstract) |
| 12:15 | ∃GUARANTEENASH for Boolean Games Is NEXP-Hard (abstract) |
10:45-13:00 Session 183C: Contributed Talks 2 & Invited Talk 4 (SYNT)
Location: FH, Seminarraum 101B
| 10:45 | Parameterized Synthesis Case Study: AMBA AHB (abstract) |
| 11:15 | Are There Good Mistakes? A Theoretical Analysis of CEGIS (abstract) |
| 11:45 | Petri Games: Synthesis of Distributed Systems with Causal Memory (Invited Talk) (abstract) |
10:45-13:15 Session 183D: Planning, Deontic Logic, Herbrand (ARW-DT)
Location: FH, Hörsaal 3
| 10:45 | Using CSP Meta Variables in AI Planning (abstract) |
| 11:15 | Automated Reasoning in Deontic Logic (abstract) |
| 11:45 | (AI) Planning to Reconfigure your Robot? (abstract) |
| 12:15 | Second-Order Characterizations of Definientia in Formula Classes (abstract) |
| 12:45 | On Herbrand theorems for classical and non-classical logics (abstract) |
10:45-13:00 Session 183E: Tutorial (Grosu), Contributed Talks (Sterratt, Kyriakopoulos, Rocca) (HSB)
Location: FH, Seminarraum 101A
| 10:45 | Tutorial: Challenges and opportunities in controlling the human heart (abstract) |
| 11:30 | Integration of rule-based models and compartmental models of neurons (abstract) |
| 12:00 | Optimal Observation Time Points in Stochastic Chemical Kinetics (abstract) |
| 12:30 | Exploiting the eigenstructures of linear systems to speed up reachability computation (abstract) |
10:45-13:00 Session 183F: Contributed Talks 3 (FRIDA)
Location: FH, Seminarraum 104
| 10:45 | Verification and Validation Challenges in Smart Grids from the Industrial Perspective (abstract) |
| 11:15 | A Fast, Correct Time-Stamped Stack (abstract) |
| 11:45 | Correctness and Performance Analysis of Distributed High Performance Programs in Scala (abstract) |
| 12:15 | Models and techniques for verification of Software Defined Networks (abstract) |
10:45-12:15 Session 183G: Ontology-based reasoning, probably (PRUV)
Location: FH, Seminarraum 107
| 10:45 | Answering Ontological Ranking Queries Based on Subjective Reports (abstract) |
| 11:15 | A New DL‐Lite N Bool Probabilistic Extension Using Belief (abstract) |
| 11:45 | Generation of Parametrically Uniform Knowledge Bases in a Relational Probabilistic Logic with Maximum Entropy Semantics (abstract) |
12:50-13:50 Session 184: KR Open Discussion and Closing (KR)
Location: EI, EI 7
13:00-14:30Lunch Break
14:30-16:00 Session 185A: Non-Classical Ontologies I (ARW-DT)
Location: FH, Hörsaal 3
| 14:30 | Models Minimal Modulo Subset-Simulation for Expressive Propositional Modal Logics (abstract) |
| 15:00 | A Resolution-Based Prover for Normal Modal Logics (abstract) |
| 15:30 | Computing Uniform Interpolants of ALCH-Ontologies with Background Knowledge (abstract) |
14:30-16:00 Session 185B: Contributed Talks (Angione, Sorokin), Concluding Remarks (Maler) (HSB)
Location: FH, Seminarraum 101A
| 14:30 | Bayesian Design for Whole Cell Synthetic Biology Models (abstract) |
| 14:55 | RKappa: Statistical sampling suite for Kappa models. (abstract) |
| 15:20 | Concluding remarks: Dynamic Systems Biology (abstract) |
14:30-16:00 Session 185C: Contributed Talks 4 (FRIDA)
Location: FH, Seminarraum 104
| 14:30 | Round model for distributed algorithms: from verification to implementation. (abstract) |
| 15:00 | On the Synthesis of Mobile Robots Algorithms: the Case of Ring Gathering (abstract) |
| 15:30 | Parameterised Verification of Robot Protocols: An Automata Theoretic Approach (abstract) |
14:30-16:00 Session 185D: Demo session & closing (PRUV)
Location: FH, Seminarraum 107
14:45-16:00 Session 186: Contributed Talks 3, Wrap-up & Discussions (SYNT)
Location: FH, Seminarraum 101B
| 14:45 | AbsSynthe: abstract synthesis from succinct safety specifications (abstract) |
| 15:15 | Low-effort Specification Debugging and Analysis (abstract) |
16:00-16:30Coffee Break
16:30-18:00 Session 187A: Non-Classical Ontologies II: Higher-Order (ARW-DT)
Location: FH, Hörsaal 3
| 16:30 | The Leo-III Project (abstract) |
| 17:00 | Socratic Proofs for Propositional Linear-Time Logic (abstract) |
| 17:30 | Modular Verification of Interconnected Families of Uniform Linear Hybrid Automata (abstract) |
16:30-18:00 Session 187B: Contributed Talks 5 (FRIDA)
Location: FH, Seminarraum 104
| 16:30 | Synthesizing self-stabilizing fault-tolerant algorithms (extended abstract) (abstract) |
| 17:00 | Synthesis for Resilient Distributed Systems (abstract) |
| 17:30 | Parameterized Synthesis (abstract) |