LPAR-22. 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning

ACTL, Algorithm Portfolios, amortized analysis, antichain-based tree automata language inclusion, API, Arithmetic Circuits, automata², automated reasoning, axiomatisation, bit-width, Boolean operations, Bounded Model Checking², cardinality constraints, CEGAR, clause learning, cognitive reasoning, complexity³, computer algebra, Constrained Uniform Sampling, constraint satisfaction, constraint solving, convex optimization, Coq, cost semantics, counterexample, counterfactual reasoning, Craig interpolation, Cyclic Graphs, cyclic proofs², d-DNNF, data streaming, deadlock, decidability, decision procedures, default logic, deontic logic, Description Logic, Description Logics, Digital Library, Distributed IC3, Distributed SMT, Divide and Conquer, Domain-agnostic, ECTL, epistemic logic, EPR, equational reasoning, Erlang, ethical decision-making, event lists, Exclusive-OR, experimental evaluation, finite model finder, finite satisfiability, first-order logic, Fluent Calculus, formal languages and automata theory, formal verification, fragments of first-order logic, Function Summaries, game theory, games, garbage collection, general satisfiability, Geometry of Interaction, gossip protocols, Graph games, graph rewriting, Gödel logics, Herbrand expansions, hierarchical systems, incremental verification, induction, inductive definitions, Infeasibility analysis, Infinite alphabets, infinite descent, infinite trees, inprocessing techniques, Integer Linear Programming, Interference, interior point method, interpolation, invariant generation, Isabelle/HOL, Kleene algebra, knowledge compilation, knowledge-based protocols, Kripke semantics, lambda calculus, Lamport clocks, lattice basis reduction, linear inequalities, LL(1) parsing, logic and computational complexity, logic programming, Lookahead Heuristic, loop, LP Solving, LTL with arithmetic, Lyndon interpolation, matching, minimal unsatisfiable subsets, modal logic, model checking², Model Predictive Control, modelling, monotonicity, Multigraphs, MUS enumeration, mutable memory, Nash equilibrium, Nonmonotonic Proof Calculus, Numerical Software Verification, Nuprl, omega-regular languages, operational semantics, parity games, path orderings, pattern matching, polymorphism, program analysis, program verification, progress measure, proof checker, propositional satisfiability, protocol verification, pushdown automata, quantified bit-vectors, Random walks and Markov chains, Rational synthesis, reachability games, read-over-write simplification, regular languages², Resource Analysis, Resource Bound Analysis, reversible computations, rewrite orderings, SAT², SAT solving², Satisfiability Modulo Theories², Satisfiability Modulo Theory², Skolemization, SMT encoding, SMT solving, software verification, static analysis, success types, succinctness, symbolic computation, tableaux system, termination², The guarded fragment, The two-variable fragment, Theory of Arrays, Three-Valued Lukasiewicz Logic, tree automata, two-variable logic with counting quantifiers, type inference, type systems, types, unranked trees/forests, Unsatisfiability analysis, Verified theorem prover backend, Weak Completion, web-based GUI, Witness, word combinatorics, YubiHSM, YubiKey