FLOC 2022: FEDERATED LOGIC CONFERENCE 2022

A
Abate, Alessandro	(VeriProp) Safe Sampling-Based Planning for Stochastic Systems with Uncertain Dynamics
Abraham, Erika	(NSV) Recent advances for hybrid systems verification with HyPro (VeriProp) Probabilistic Hyperproperties
Abrahamsson, Oskar	(ITP) Candle: A Verified Implementation of HOL Light
Abramsky, Samson	(VardiFest) From Kochen-Specker to Feder-Vardi
Accattoli, Beniamino	(LICS) Exponentials as Substitutions and the Cost of Cut Elimination in Linear Logic (LICS) Reasonable Space for the Lambda-Calculus, Logarithmically
Acclavio, Matteo	(FSCD) A Graphical Proof Theory of Logical Time
Ackerman, Nathanael	(LICS) Computable PAC Learning of Continuous Features
Adamek, Jiri	(LICS) Varieties of quantitative algebras and their monads
Adams, Michael D.	(Coq) HenBlocks: Structured Editing for Coq
Afshari, Bahareh	(iPRA) Interpolation and Completeness in the Modal Mu-Calculus
Agarwal, Chaitanya	(CAV) PAC Statistical Model Checking of Mean Payoff in Discrete- and Continuous-Time MDP
Aguilera, Juan	(KR) A Gödel calculus for Linear Temporal Logic
Ahmadpanah, Mohammad M.	(GuttmanFest) Securing Node-RED Applications
Ahrens, Benedikt	(LICS) Semantics for two-dimensional type theory (HoTT/UF) A Library of Monoidal Categories for Display and Univalence (HoTT/UF) Towards Normalization of Simplicial Type Theory via Synthetic Tait Computability (HoTT/UF) Semantics for two-dimensional type theory
Aiswarya, C.	(LICS) On the Satisfiability of Context-free String Constraints with Subword Ordering
Akgun, Ozgur	(CP) A framework for generating informative benchmark instances (CP) Understanding how people approach constraint modelling and solving
Akshay, S.	(IJCAR) On eventual non-negativity and positivity for the weighted sum of powers of matrices
Albert, Elvira	(CAV) Distilling Constraints in Zero-Knowledge Protocols (IJCAR) Using Automated Reasoning Techniques for Enhancing the Efficiency and Security of (Ethereum) Smart Contracts
Alberti, Marco	(ICLP) An Iterative Fixpoint Semantics for MKNF Hybrid Knowledge Bases with Function Symbols
Albini, Emanuele	(KR) Influence-Driven Explanations for Bayesian Network Classifiers
Alechina, Natasha	(KR) Automatic Synthesis of Dynamic Norms for Multi-Agent Systems (VardiFest) Synthesis of plans for teams of manufacturing robots
Alexander, Christopher	(GDE) Unmanned Aerial Vehicle compliance checking using Goal-Directed Answer Set Programming
Algehed, Maximilian	(CSF) Applying consensus and replication securely with FLAQR
Alkmim, Bernardo	(DL) A Labelled Natural Deduction System for an Intuitionistic Description Logic with Nominals
Allouche, David	(CP) Parallel Hybrid Best-First Search
Alos, Josep	(SAT) OptiLog v2: Model, Solve, Tune And Run
Alrabbaa, Christian	(DL) Finding Good Proofs for Answers to Conjunctive Queries Mediated by Lightweight Ontologies (DL) On the Eve of True Explainability for OWL Ontologies: Description Logic Proofs with Evee and Evonne (XLoKR) Finding Good Proofs for Answers to Conjunctive Queries Mediated by Lightweight Ontologies (Extended Abstract) (XLoKR) Explaining Description Logic Entailments in Practice with Evee and Evonne (IJCAR) Evonne: Interactive Proof Visualization for Description Logics (System Description)
Alt, Leonardo	(CAV) SolCMC: Solidity Compiler’s Model Checker (SMT) On Satisfiability of Polynomial Equations over Large Prime Fields
Alur, Rajeev	(SYNT) Complexity of Relational Query Synthesis (SYNT) A Framework for Transforming Specifications in Reinforcement Learning (Mentoring Workshop) Formal methods for Machine Learning (CAV) Specification-Guided Learning of Nash Equilibria with High Social Welfare (VardiFest) The Joy of Automata
Alvarez-Picallo, Mario	(FSCD) Rewriting for monoidal closed categories
Alves, Sandra	(IFIP-WG1.6) Quantitative Weak Linearisation
Amendola, Arturo	(SMT) NORMA: a tool for the analysis of Relay-based Railway Interlocking Systems
Amendola, Giovanni	(ICLP) Solving Problems in PH with ASP(Q)
Amir, Guy	(FoMLAS) Verification-Aided Deep Ensemble Selection
Amir, Guy	(CAV) Neural Network Robustness as a Verification Property: A Principled Case Study
Anastacio, Marie	(MC) Stochastic Constraint Optimisation with Applications in Network Analysis
Anders, Markus	(SAT) SAT Preprocessors and Symmetry
Annenkov, Danil	(FMBC) Finding smart contract vulnerabilities with ConCert's property-based testing framework
Ansótegui, Carlos	(SAT) OptiLog v2: Model, Solve, Tune And Run
Antonelli, Melissa	(LICS) Curry and Howard Meet Borel
Aoto, Takahito	(IWC) A Critical Pair Criterion for Level-Commutation of Conditional Term Rewriting Systems
Aparicio, Damian	(GuttmanFest) Protocol Analysis with Time and Space
Appel, Andrew	(NSV) Verified Numerical Methods for Ordinary Differential Equations (CAV) Verified Erasure Correction in Coq with MathComp and VST
Arbelaez, Alejandro	(CP) Large Neighborhood Search for Robust Solutions for Constraint Satisfaction Problems with Ordered Domains (CP) Large Neighborhood Search for Robust Solutions for Constraint Satisfaction Problems with Ordered Domains
Arden, Owen	(CSF) Applying consensus and replication securely with FLAQR
Arias, Joaquin	(ICLP) Building Information Modeling using Constraint Logic Programming (ICLP) Towards Dynamic Consistency Checking in Goal-directed Predicate Answer Set Programming (ICLP) Modeling and Reasoning in Event Calculus using Goal-Directed Constraint Answer Set Programming (Extended Abstract) (GDE) Modeling Administrative Discretion Using Goal-Directed Answer Set Programming (GDE) An s(CASP) In-Browser Playground based on Ciao Prolog (GDE) LTL Model Checking using Coinductive Answer Set programming (GDE) Symbolic Reinforcement Learning Framework with Incremental Learning of Rule-based Policy (GDE) GDE of ASP: applications, potential and future directions
Arieli, Ofer	(NMR) Abductive Reasoning with Sequent-Based Argumentation (Extended Abstract)
Arnaboldi, Luca	(FoMLAS) Vehicle: A High-Level Language for Embedding Logical Specifications in Neural Networks (FoMLAS) Why Robust Natural Language Understanding is a Challenge
Arrighi, Emmanuel	(PCCR) Kemeny Rank Aggregation: Width Measure and Diversity Notion
Artikis, Alexander	(PLP) Online Reasoning under Uncertainty with the Event Calculus (ICLP) Stream Reasoning with Deadlines (KR) Stream Reasoning with Cycles
Arvind,	(CAV) Hemiola: A DSL and Verification Tools to Guide Design and Proof of Hierarchical Cache-Coherence Protocols
Asada, Kazuyuki	(LICS) Linear-Algebraic Models of Linear Logic as Categories of Modules over Sigma-Semirings
Asilis, Julian	(LICS) Computable PAC Learning of Continuous Features
Asimi, Kristina	(CP) Fixed-Template Promise Model Checking Problems (WiL) Fixed-Template Promise Model Checking Problems
Aspis, Yaniv	(KR) Embed2Sym - Scalable Neuro-Symbolic Reasoning via Clustered Embeddings
Asplund, Mikael	(CSF) Exploiting Partial Order of Keys to Verify Security of a Vehicular Group Protocol
Atkey, Robert	(FoMLAS) Vehicle: A High-Level Language for Embedding Logical Specifications in Neural Networks
Attiya, Hagit	(FRIDA) Preserving Hyperproperties when Using Concurrent Objects
Aubert, Clément	(FSCD) mwp-Analysis Improvement and Implementation: Realizing Implicit Computational Complexity
Audemard, Gilles	(SAT) A New Exact Solver for (Weighted) Max#SAT
Avanzini, Martin	(LICS) Quantum Expectation Transformers for Cost Analysis
Avron, Arnon	(LogTeach) What Should Students of a Course in Logic Know at Its End?
Ayala-Rincón, Mauricio	(FSCD) A Certified Algorithm for AC-Unification
Azimov, Rustam	(ICLP) Jumping Evaluation of Nested Regular Path Queries
Azzolini, Damiano	(PLP) Statistical Statements in Probabilistic Logic Programming (PLP) Semantics for Hybrid Probabilistic Logic Programs with Function Symbols: Technical Summary (ICLP) Abduction in Probabilistic Logic Programs
B
Baader, Franz	(KR) Pushing Optimal ABox Repair from EL Towards More Expressive Horn-DLs (UNIF) Restricted Unification in the Description Logic FLbot (DL) Optimal ABox Repair w.r.t. Static EL TBoxes: from Quantified ABoxes back to ABoxes (Extended Abstract) (DL) Efficient TBox Reasoning with Value Restrictions using the FL0wer Reasoner (Extended Abstract) (IJCAR) Evonne: Interactive Proof Visualization for Description Logics (System Description)
Baanen, Anne	(ITP) Use and abuse of instance parameters in the Lean mathematical library
Baaz, Matthias	(LogTeach) Teaching Logic
Babaki, Behrouz	(MC) Stochastic Constraint Optimisation with Applications in Network Analysis
Baccelli, Emmanuel	(CAV) End-to-end Mechanised Proof of an eBPF Virtual Machine for Microcontrollers
Bach, Jakob	(SAT) A Comprehensive Study of k-Portfolios of Recent SAT Solvers
Badings, Thom	(CAV) Sampling-Based Verification of CTMCs with Uncertain Rates (VeriProp) Safe Sampling-Based Planning for Stochastic Systems with Uncertain Dynamics
Bae, Kyungmin	(CAV) STLmc: Robust STL Model Checking of Hybrid Systems using SMT
Baelde, David	(CSF) Cracking the Stateful Nut -- Computational Proofs of Stateful Security Protocols using the Squirrel Proof Assistant (LICS) Bouncing threads for circular and non-wellfounded proofs
Baeta, Nuno	(ThEdu) Rule Based Geometry Automated Theorem Provers
Bak, Stanley	(CAV) Reachability of Koopman Linearized Systems Using Random Fourier Feature Observables and Polynomial Zonotope Refinement
Baker, Clayton	(NMR) Asking human reasoners to judge postulates of belief change for plausibility (KR) Do Humans Find Postulates of Belief Change Plausible?
Balaji, Nikhil	(LICS) Identity testing for radical expressions
Balbiani, Philippe	(UNIF) Unification types in modal logics (DL) Advanced languages of terms for ontologies
Balcan, Maria-Florina	(CP) Improved Sample Complexity Bounds for Branch-and-Cut (CP) Improved Sample Complexity Bounds for Branch-and-Cut
Baldazzi, Teodoro	(KR) On the Relationship between Shy and Warded Datalog+/-
Balintová, Iveta	(DL) Hybrid MHS-MXP ABox Abduction Solver: First Emprical Results
Balintová, Iveta	(NMR) Hybrid MHS-MXP ABox Abduction Solver: First Emprical Results
Ballesteros, Ignacio	(FMBC) Automatic generation of attacker contracts in Solidity
Balliu, Musard	(GuttmanFest) Securing Node-RED Applications
Balogh, Andrea	(CP) Symmetry breaking and Knowledge Compilation
Baltag, Alexandru	(KR) The Topology of Surprise
Baluch, Miroslav	(FOMEO) First-Order Logic Workbook
Balyo, Tomas	(POS) Dinosat: A SAT Solver with Native DNF Support
Balzer, Stephanie	(TLLA-LINEARITY) Recursive Session Logical Relations
Ban Kirigin, Tajana	(GuttmanFest) On the Complexity of Verification of Time-Sensitive Distributed Systems
Bandyopadhyay, Soumyadip	(PERR) Implementing a Path Based Equivalence Checker for Petri net based Models of Programs
Bang, Seongwon	(CAV) SMT-based Translation Validation for Machine Learning Compiler
Banković, Milan	(SMT) Trail saving in SMT
Bannach, Max	(SAT) On the Parallel Parameterized Complexity of MaxSAT Variants (PCCR) MaxSAT: Parameterized, Parallel, Absolute (PDAR) Structural Parameter Based Parallel Algorithms for Partially Weighted MaxSAT (MC) Extending Partially Directed Graphs and Determine the Size of their Markov Equivalence Class
Banno, Ryotaro	(CAV) Oblivious Online Monitoring for Safety LTL Specification via Fully Homomorphic Encryption
Bansal, Suguman	(SYNT) A Framework for Transforming Specifications in Reinforcement Learning (CAV) Specification-Guided Learning of Nash Equilibria with High Social Welfare (VardiFest) Automata-Based Quantitative Reasoning (WOLVERINE) Safe Reinforcement Learning
Bao, Jialu	(CAV) Data-Driven Invariant Learning for Probabilistic Programs
Bapanapally, Jagadish	(ITP) A Complete, Mechanically-Verified Proof of the Banach-Tarski Theorem in ACL2(r)
Barbarossa, Davide	(TLLA-LINEARITY) Denotational semantics driven simplicial homology? (LICS) Resource approximation for the lambda-mu-calculus
Barbone, Mark	(SYNT) Regex+: Synthesizing Regular Expressions from Positive Examples
Barbosa, Haniel	(CAV) Even Faster Conflicts and Lazier Reductions for String Solvers (IJCAR) Flexible Proof Production in an Industrial-Strength SMT Solver (SMT) cvc5: A Versatile and Industrial-Strength SMT Solver (SMT) SMT-COMP Report and Tool Presentations (SMT) SMT Proof Standardization Update
Barloy, Corentin	(LICS) The Regular Languages of First-Order Logic with One Alternation
Baroni, Pietro	(KR) Influence-Driven Explanations for Bayesian Network Classifiers (KR) Explaining Causal Models with Argumentation: the Case of Bi-variate Reinforcement
Barrett, Clark	(CAV) Even Faster Conflicts and Lazier Reductions for String Solvers (CAV) Murxla: A Modular and Highly Extensible API Fuzzer for SMT Solvers (IJCAR) Cooperating Techniques for Solving nonlinear arithmetic in the cvc5 SMT solver (System Description) (IJCAR) Reasoning About Vectors using an SMT Theory of Sequences (IJCAR) Flexible Proof Production in an Industrial-Strength SMT Solver (SMT) Murxla: A Modular and Highly Extensible API Fuzzer for SMT Solvers (SMT) cvc5: A Versatile and Industrial-Strength SMT Solver (SMT) Bit-Precise Reasoning via Int-Blasting (FoMLAS) Neural Network Verification with Proof Production (FoMLAS) An Abstraction-Refinement Approach to Verifying Convolutional Neural Networks (FoMLAS) Scalable Verification of GNN-based Job Schedulers
Barrett, Clark	(SMT) Panel discussion "SMT: Past, Present and Future" (SMT) SMT-Lib Update Report
Bartel, Thomas	(POS) Dinosat: A SAT Solver with Native DNF Support
Barthe, Gilles	(LICS) Quantum Weakest Preconditions for Reasoning about Expected Runtimes of Quantum Programs
Barto, Libor	(CP) Fixed-Template Promise Model Checking Problems (CP) Weisfeiler-Leman Invariant Promise Valued CSPs (WiL) Fixed-Template Promise Model Checking Problems
Bartoletti, Massimo	(FMBC) MEV-freedom, in DeFi and beyond
Barwell, Adam	(WPTE) Towards a Refactoring Tool for Dependently-Typed Programs (work in progress)
Basin, David	(CSF) DPL: A Language for GDPR Enforcement (CSF) IFCIL: An Information Flow Configuration Language for SELinux (CSF) N-Tube: Formally Verified Secure Bandwidth Reservation in Path-Aware Internet Architectures
Basrur, Chaithanya	(CP) Trajectory Optimization for Safe Navigation in Maritime Traffic Using Historical Data
Bastani, Osbert	(SYNT) A Framework for Transforming Specifications in Reinforcement Learning (CAV) Specification-Guided Learning of Nash Equilibria with High Social Welfare (TERMGRAPH) Ideograph: A Language for Expressing and Manipulating Structured Data
Basu, Kinjal	(GDE) Summary on "Hybrid Neuro-Symbolic Approach for Text-Based Games using Inductive Logic Programming" (GDE) Symbolic Reinforcement Learning Framework with Incremental Learning of Rule-based Policy
Baudon, Thaïs	(IWC) On Confluence of Parallel-Innermost Term Rewriting
Baumeister, Joachim	(ASPOCP) Conflict Handling in Product Configuration using Answer Set Programming
Baunsgaard Kristensen, Magnus	(LICS) Greatest HITs: Higher inductive types in coinductive definitions via induction under clocks
Beame, Paul	(POS) Adding Dual Variables to Algebraic Reasoning for Gate-Level Multiplier Verification
Becchi, Anna	(CAV) Abstraction Modulo Stability for Reverse Engineering (SMT) NORMA: a tool for the analysis of Relay-based Railway Interlocking Systems
Becker, Heiko	(ITP) Dandelion: Certified Approximations of Elementary Functions
Beckman, Arnold	(PC) Towards higher order proof complexity
Bednarczyk, Bartosz	(DECFOML) Forward Guarded Fragment: A tamed higher-arity extension of ALC (DL) Comonadic Semantics for Description Logics Games
Beierle, Christoph	(KR) Iterated Belief Change, Computationally (KR) Inference with System W Satisfies Syntax Splitting
Beldiceanu, Nicolas	(CP) Acquiring Maps of Interrelated Conjectures on Sharp Bounds (CP) A Boolean Formula Seeker in the Context of Acquiring Maps of Interrelated Conjectures on Sharp Bounds (CP) Extended Abstract: Acquiring Maps of Interrelated Conjectures on Sharp Bounds
Beldjilali, Abdelkader	(CP) Parallel Hybrid Best-First Search
Belle, Vaishak	(PLP) Explainability, causality and computational and-or graphs (XLoKR) Using Abstraction for Interpretable Robot Programs in Stochastic Domains (MC) Recursive Solutions to First-Order Model Counting
Bellodi, Elena	(PLP) Statistical Statements in Probabilistic Logic Programming (ICLP) Abduction in Probabilistic Logic Programs
Bellomarini, Luigi	(KR) On the Relationship between Shy and Warded Datalog+/-
Bellés-Muñoz, Marta	(CAV) Distilling Constraints in Zero-Knowledge Protocols
Benac, Clara	(FMBC) Automatic generation of attacker contracts in Solidity
Bendik, Jaroslav	(DSV) Formal Verification of Ethereum Smart Contracts: SMT-Based Approaches and Challenges
Bensalem, Saddek	(FoMLAS) Formal Specification for Learning-Enabled Autonomous Systems (Extended Abstract)
Benz, Chloe	(NMR) There and Back Again: Combining Nonmonotonic Logical Reasoning and Deep Learning on an Assistive Robot
Benzmüller, Christoph	(ARQNL) Solving QMLTP Problems by Translation to Higher-order Logic (ARQNL) Automated verification of deontic correspondences in Isabelle/HOL - First results (PAAR) Automated Reasoning in Non-classical Logics in the TPTP World
Beohar, Harsh	(LICS) Graded Monads and Behavioural Equivalence Games
Beraldo-de-Araujo, Anderson	(TLLA-LINEARITY) Cloning and Deleting Quantum Information from a Linear Logical Point of View
Berden, Senne	(CP) Learning MAX-SAT Models from Examples using Genetic Algorithms and Knowledge Compilation
Bereczky, Péter	(WPTE) A Machine-Checked Formalisation of Erlang Modules
Berent, Lucas	(SAT) Towards a SAT Encoding for Quantum Circuits
Berg, Jeremias	(SAT) Incremental Maximum Satisfiability (SAT) Improvements to the Implicit Hitting Set Approach to Pseudo-Boolean Optimization (SAT) MaxSAT-Based Bi-Objective Boolean Optimization (SAT) 25 years of SAT: Maximum Satisfiability for Real-World Optimization (IJCAR) Clause Redundancy and Preprocessing in Maximum Satisfiability
Bergsträßer, Pascal	(LICS) Ramsey Quantifiers over Automatic Structures: Complexity and Applications to Verification
Beringer, Lennart	(ASL) Proving Logical Atomicity using Lock Invariants
Bernreiter, Michael	(NMR) The Effect of Preferences in Abstract Argumentation Under a Claim-Centric View (IJCAR) Sequent Calculi for Choice Logics
Berthold, Matti	(KR) On Syntactic Forgetting with Strong Persistence
Bessa, Iury	(FoMLAS) Counter-Example Guided Neural Network Compression Refinement (CEG4N)
Bessai, Jan	(FSCD) Restricting tree grammars with term rewriting
Bessiere, Christian	(CP) Complexity of Minimum-Size Arc-Inconsistency Explanations
Besson, Frédéric	(CAV) End-to-end Mechanised Proof of an eBPF Virtual Machine for Microcontrollers
Beutner, Raven	(CAV) Software Verification of Hyperproperties Beyond k-Safety (CSF) Prophecy Variables for Hyperproperty Verification (LICS) Deciding Hyperproperties Combined with Functional Specifications
Beyer, Dirk	(iPRA) Interpolation and SAT-Based Model Checking Revisited: Adoption to Software Verification
Beyersdorff, Olaf	(SAT) Should decisions in QCDCL follow prefix order? (SAT) Classes of Hard Formulas for QBF Resolution (SAT) 25 years of SAT: Proof complexity and SAT solving (PC) QCDCL with Cube Learning or Pure Literal Elimination – What is best?
Bezhanishvili, Nick	(KR) The Topology of Surprise
Bhandary, Prajna	(GuttmanFest) Searching for Selfie in TLS 1.3 with the Cryptographic Protocol Shapes Analyzer
Bhargavan, Karthikeyan	(GuttmanFest) A Tutorial-Style Introduction to DY*
Bhatia, Amit	(VardiFest) Logic-driven approaches for smart, safe and energy-efficient aviation
Bian, Song	(CAV) Oblivious Online Monitoring for Safety LTL Specification via Fully Homomorphic Encryption
Bichhawat, Abhishek	(GuttmanFest) A Tutorial-Style Introduction to DY*
Bidoit, Nicole	(IJCAR) Hyper-graph based Inference Rules for Computing EL+-Ontology Justifications
Bienvenu, Meghyn	(KR) LACE: A Logical Approach to Collective Entity Resolution (KR) Counting queries over ELHI⊥ ontologies (KR) Querying Inconsistent Prioritized Data with ORBITS: Algorithms, Implementation, and Experiments (DL) Querying Inconsistent Prioritized Data with ORBITS: Algorithms, Implementation, and Experiments (Extended Abstract) (DL) Complexity Landscape for Counting Queries (Extended abstract)
Biere, Armin	(POS) Adding Dual Variables to Algebraic Reasoning for Gate-Level Multiplier Verification (POS) Scalable Proof Producing Multi-Threaded SAT Solving with Gimsatul through Sharing instead of Copying Clauses (SAT) Migrating Solver State (PAAR) QuAPI: Adding Assumptions to Non-Assuming SAT & QBF Solvers
Biere, Armin	(SAT) 25 years of SAT: Trusting SAT Solvers
Biernacka, Małgorzata	(ITP) The Zoo of Lambda-Calculus Reduction Strategies, and Coq
Biewer, Sebastian	(FCS) A Preview to HoRStify: Sound Security Analysis of Smart Contracts
Bilkova, Marta	(IJCAR) Paraconsistent Gödel modal logic
Billi, Marco	(GDE) Integration of Logical English and s(CASP)
Birkedal, Lars	(FSCD) A stratified approach to Lob induction (CSF) Proving full-system security properties under multiple attacker models on capability machines
Biswas, Sayan	(GuttmanFest) Establishing the Price of Privacy in Federated Data Trading
Bjørner, Nikolaj	(Mentoring Workshop) Advancing Science with Platforms and Driving Scenarios: a perspective from a researcher at Microsoft Research (SAT) Analysis of Core-Guided MaxSAT Using Cores and Correction Sets (SMT) User-Propagators for Custom Theories in SMT Solving
Blaisdell, Eben	(LFMTP) Associativity or Non-Associativity, Local or Global! (IJCAR) Non-associative, non-commutative multi-modal linear logic
Blanchette, Jasmin	(ITP) Seventeen Provers under the Hammer
Blanco, Roberto	(CSF) SecurePtrs: Proving Secure Compilation Using Data-Flow Back-Translation and Turn-Taking Simulation
Blanqui, Frédéric	(FSCD) Encoding type universes without using matching modulo associativity and commutativity
Blanqui, Frédéric	(IFIP-WG1.6) The International School on Rewriting
Bleukx, Ignace	(XLoKR) Stepwise Explanations of Unsatisfiable Constraint Programs (Extended abstract)
Blicha, Martin	(CAV) SolCMC: Solidity Compiler’s Model Checker
Blondin, Michael	(CAV) Verifying generalised and structural soundness of workflow nets via relaxations (LICS) The complexity of soundness in workflow nets
Blot, Valentin	(LFMTP) An Implementation of Set Theory with Pointed Graphs in Dedukti (LICS) A direct computational interpretation of second-order arithmetic via update recursion
Blümel, Lydia	(KR) Defining Defense and Defeat in Abstract Argumentation From Scratch -- A Generalizing Approach (KR) Impact of Logic Paradigms on Abstract Argumentation
Boborová, Janka	(DL) Hybrid MHS-MXP ABox Abduction Solver: First Emprical Results
Boborová, Janka	(NMR) Hybrid MHS-MXP ABox Abduction Solver: First Emprical Results
Bochman, Alexander	(ABR) Tutorial: Assumption-Based Nonmonotonic Reasoning (Part 1) (ABR) Tutorial: Assumption-Based Nonmonotonic Reasoning (Part 2)
Bode, Vincent	(PAAR) The Isabelle Community Benchmark
Boeira, Felipe	(CSF) Exploiting Partial Order of Keys to Verify Security of a Vehicular Group Protocol
Boey, Bernard	(Coq) HenBlocks: Structured Editing for Coq
Bogaerts, Bart	(POS) Certified Symmetry and Dominance Breaking for Combinatorial Optimisation (ICLP) Nested Justification Systems (ICLP) Tree-Like Justification Systems are Consistent (XLoKR) Stepwise Explanations of Unsatisfiable Constraint Programs (Extended abstract) (ModRef) Efficiently Explaining CSPs with Unsatisfiable Subset Optimization (extended abstract)
Bogaerts, Bart	(CP) Solving with Provably Correct Results: Beyond Satisfiability, and Towards Constraint Programming
Bogomolov, Sergiy	(CAV) Reachability of Koopman Linearized Systems Using Random Fourier Feature Observables and Polynomial Zonotope Refinement
Boigelot, Bernard	(SC^2) Decidability of difference logics with unary predicates
Bolignano, Pauline	(WiL) Automated Logic-Based Reasoning for Analyzing Prime Video Code
Bonacina, Ilario	(PC) On vanishing sums of roots of unity in polynomial calculus and sum-of-squares (PC) On combinatorial principles coming from semi-algebraic proof systems (LICS) On the strength of Sherali-Adams and Nullstellensatz as propositional proof systems
Bonacina, Maria Paola	(PAAR) On SGGS and Horn Clauses (SMT) CDSAT for nondisjoint theories with shared predicates: arrays with abstract length (SMT) Panel discussion "SMT: Past, Present and Future"
Bonakdarpour, Borzoo	(CSF) Mapping Synthesis for Hyperproperties
Bonatti, Piero	(KR) Sticky Policies in OWL2: Extending PL with fixpoints and Transitive Closure
Bonet, Blai	(KR) Learning generalized policies without supervision using GNNs
Bonet, Maria Luisa	(LICS) On the strength of Sherali-Adams and Nullstellensatz as propositional proof systems
Bonnet, Édouard	(LICS) Model Checking on Interpretations of Classes of Bounded Local Cliquewidth
Booth, Richard	(NMR) Truth-Tracking with Non-Expert Information Sources (KR) Who’s the Expert? On Multi-source Belief Change
Borca-Tasciuc, Giorgian	(ICLP) Knowledge Authoring with Factual English
Bordais, Benjamin	(VardiFest) Strategy synthesis for Global Window PCTL
Bordini, Rafael H.	(KR) Towards an Enthymeme-Based Communication Framework in Multi-Agent Systems
Borg, Annemarie	(NMR) Abductive Reasoning with Sequent-Based Argumentation (Extended Abstract)
Borgida, Alex	(DL) Accessing Document Data Sources using Referring Expression Types
Borgwardt, Stefan	(DL) Expressivity of Planning with Horn Description Logic Ontologies (Extended Abstract) (DL) Finding Good Proofs for Answers to Conjunctive Queries Mediated by Lightweight Ontologies (DL) On the Eve of True Explainability for OWL Ontologies: Description Logic Proofs with Evee and Evonne (XLoKR) Finding Good Proofs for Answers to Conjunctive Queries Mediated by Lightweight Ontologies (Extended Abstract) (XLoKR) Explaining Description Logic Entailments in Practice with Evee and Evonne (IJCAR) Evonne: Interactive Proof Visualization for Description Logics (System Description)
Borgyos, Szabolcs	(GDE) Unmanned Aerial Vehicle compliance checking using Goal-Directed Answer Set Programming
Bouajjani, Ahmed	(CAV) Data-driven Numerical Invariant Synthesis with Automatic Generation of Attributes
Boudreault, Raphaël	(CP) A Constraint Programming Approach to Ship Refit Project Scheduling
Boukhobza, Taha	(ASPOCP) Automatic Synthesis of Boolean Networks from Biological Knowledge and Data
Bouraoui, Zied	(KR) Region-Based Merging of Open-Domain Terminological Knowledge
Bourgaux, Camille	(KR) Revisiting Semiring Provenance for Datalog (KR) Querying Inconsistent Prioritized Data with ORBITS: Algorithms, Implementation, and Experiments (DL) Querying Inconsistent Prioritized Data with ORBITS: Algorithms, Implementation, and Experiments (Extended Abstract)
Bourhis, Pierre	(KR) Revisiting Semiring Provenance for Datalog
Boutglay, Wael-Amine	(CAV) Data-driven Numerical Invariant Synthesis with Automatic Generation of Attributes
Boutsis, Ioannis	(WiL) Automated Logic-Based Reasoning for Analyzing Prime Video Code
Bouziane, Hinde	(IJCAR) Goéland : A Concurrent Tableau-Based Theorem Prover (System Description)
Bozga, Marius	(IJCAR) Decision Problems in a Logic for Reasoning about Reconfigurable Distributed Systems
Bozzato, Loris	(NMR) Reasoning on Multi-Relational Contextual Hierarchies via Answer Set Programming with Algebraic Measures (DL) Reasoning on Multi-Relational Contextual Hierarchies via Answer Set Programming with Algebraic Measures
Brady, Edwin	(WPTE) Towards a Refactoring Tool for Dependently-Typed Programs (work in progress)
Brain, Martin	(SMT) cvc5: A Versatile and Industrial-Strength SMT Solver
Braje, Timothy	(CSF) Adversary Safety by Construction in a Language of Cryptographic Protocols
Brieulle, Ludovic	(DL) Category-based Semantics for the Description Logic ALC and Reasoning
Bright, Curtis	(KR) Solving Lam's Problem via SAT and Isomorph-Free Exhaustive Generation (SC^2) Enumerating Projective Planes of Order Nine with Proof Verification (SC^2) An SC-Square Approach to the Minimum Kochen–Specker Problem
Brix, Christopher	(FoMLAS) VNN-COMP 2022
Brockschmidt, Marc	(PAAR) Exploring Representation of Horn clauses using GNNs
Broda, Krysia	(ASPOCP) A Semantics For Probabilistic Answer Set Programs With Incomplete Stochastic Knowledge (KR) Embed2Sym - Scalable Neuro-Symbolic Reasoning via Clustered Embeddings
Bromberger, Martin	(PAAR) A Two-Watched Literal Scheme for First-Order Logic (PAAR) Exploring Partial Models with SCL (IJCAR) An Efficient Subsumption Test Pipeline for BS(LRA) Clauses
Brown, Chad	(UNIF) Higher-Order Unification with Definition by Cases
Brown, Chad	(FMBC) Proofgold: Blockchain for Formal Methods (IJCAR) Lash 1.0 (System Description)
Brown, Chad	(SMT) Challenges and Solutions for Higher-Order SMT Proofs
Brown, Christopher	(WPTE) Towards a Refactoring Tool for Dependently-Typed Programs (work in progress)
Brozius, Wouter	(WPTE) Extending a Lemma Generation Approach for Rewriting Induction on Logically Constrained Term Rewriting Systems (PERR) Extending a Lemma Generation Approach for Rewriting Induction on Logically Constrained Term Rewriting Systems
Brugger, Lea Salome	(FMBC) Automating Security Analysis of Off-Chain Protocols
Bruni, Alessandro	(GuttmanFest) Security Protocols as Choreographies
Bruynooghe, Maurice	(ICLP) Analyzing Semantics of Aggregate Answer Set Programming Using Approximation Fixpoint Theory
Bryant, Randal	(POS) TBUDDY: A Proof-Generating BDD Package (POS) Combining CDCL, Gauss-Jordan Elimination, and Proof Generation (SAT) (BDD event) (QBF) Moving Definition Variables in Quantified Boolean Formulas (Extended Abstract) (IJCAR) Preprocessing of Propagation Redundant Clauses
Buchholtz, Ulrik	(HoTT/UF) Towards Normalization of Simplicial Type Theory via Synthetic Tait Computability
Bueri, Lucas	(IJCAR) Decision Problems in a Logic for Reasoning about Reconfigurable Distributed Systems
Bueso, Luis Eduardo	(FMBC) Automatic generation of attacker contracts in Solidity
Bun, Mark	(CSF) The Complexity of Verifying Boolean Programs as Differentially Private
Bunina, Elena	(LogTeach) How to teach logic for CS-undergraduate? Step-by-step!
Burel, Guillaume	(PAAR) EuroProofNet presentation on proofs in Dedukti
Burgholzer, Lukas	(SAT) Towards a SAT Encoding for Quantum Circuits
Burlats, Auguste	(CP) Exploiting Model Entropy to Make Branching Decisions in Constraint Programming
Bursuc, Sergiu	(CSF) Contingent payments from two-party signing and verification for abelian groups (FCS) Towards Unlinkable Smartcard-based Payments: an extended abstract
Busatto-Gaston, Damien	(VardiFest) Strategy synthesis for Global Window PCTL
Busi, Matteo	(FCS) pi_RA: A pi-calculus for verifying protocols that use remote attestation
Buss, Sam	(PC) Towards higher order proof complexity
Butti, Silvia	(CP) Fixed-Template Promise Model Checking Problems (CP) Weisfeiler-Leman Invariant Promise Valued CSPs (WiL) Fixed-Template Promise Model Checking Problems
Böhm, Benjamin	(SAT) Should decisions in QCDCL follow prefix order? (PC) QCDCL with Cube Learning or Pure Literal Elimination – What is best?
Böhm, Klemens	(SAT) A Comprehensive Study of k-Portfolios of Recent SAT Solvers
C
Cabral, Miguel	(SAT) SAT-based Leximax Optimisation Algorithms
Cadilhac, Michaël	(LICS) The Regular Languages of First-Order Logic with One Alternation
Cai, Shaowei	(CAV) Local Search For SMT on Linear Integer Arithmetic
Cailler, Julie	(PDAR) Goéland : A Concurrent Tableau-Based Theorem Prover (IJCAR) Goéland : A Concurrent Tableau-Based Theorem Prover (System Description)
Calegari, Roberta	(KR) Symbolic Knowledge Extraction from Opaque Machine Learning Predictors: GridREx & PEDRO (XLoKR) Clustering-Based Approaches for Symbolic Knowledge Extraction
Calimeri, Francesco	(ICLP) Applications of Answer Set Programming to Smart Devices and Large Scale Reasoning
Calvanese, Diego	(DL) Ontology-based Data Federation (Extended Abstract) (DL) Extraction of Object-Centric Event Logs through Virtual Knowledge Graphs (VardiFest) Rewriting, Answering, and Losslessness: A Clarification by the “Four Italians”
Capon, Chloé	(ASPOCP) Computing H-Partitions in ASP and Datalog
Cappart, Quentin	(CP) Scheduling the Equipment Maintenance of an Electric Power Transmission Network using Constraint Programming (CP) Peel-and-Bound: Generating Stronger Relaxed Bounds with Multivalued Decision Diagrams (CP) Extended Abstract for : Scheduling the Equipment Maintenance of an Electric Power Transmission Network using Constraint Programming (CP) Peel-and-Bound: Generating Stronger Relaxed Bounds with Multivalued Decision Diagrams
Cappart, Quentin	(CP) Building a Constraint Programming Solver Guided by Machine Learning: Opportunities and Challenges
Carbone, Marco	(GuttmanFest) Security Protocols as Choreographies
Carbonnel, Clément	(CP) Complexity of Minimum-Size Arc-Inconsistency Explanations (CP) On Redundancy in Constraint Satisfaction Problems
Carral, David	(KR) Normalisations of Existential Rules: Not so Innocuous! (LICS) Deciding Hyperproperties Combined with Functional Specifications
Carro, Manuel	(ICLP) Building Information Modeling using Constraint Logic Programming (ICLP) Modeling and Reasoning in Event Calculus using Goal-Directed Constraint Answer Set Programming (Extended Abstract) (GDE) An s(CASP) In-Browser Playground based on Ciao Prolog
Carro, Manuel	(ICLP) Towards Dynamic Consistency Checking in Goal-directed Predicate Answer Set Programming
Casadio, Marco	(CAV) Neural Network Robustness as a Verification Property: A Principled Case Study (FoMLAS) Why Robust Natural Language Understanding is a Challenge
Casini, Giovanni	(NMR) Situated Conditionals - A Brief Introduction (NMR) Defeasible reasoning in RDFS (KR) A General Framework for Modelling Conditional Reasoning - Preliminary Report (KR) A Minimal Deductive System for RDFS with Negative Statements (DL) Defeasible reasoning in RDFS
Castañeda Lozano, Roberto	(CP) Optimized Code Generation against Power Side Channels
Castro, Pablo	(CAV) Playing Against Fair Adversaries in Stochastic Games with Total Rewards
Cattabriga, Paola	(WiL) A note on Türing 1936
Cauli, Claudia	(IJCAR) Actions over Core-closed Knowledge Bases
Cavada, Roberto	(SMT) NORMA: a tool for the analysis of Relay-based Railway Interlocking Systems
Cavallo, Evan	(HoTT/UF) A type-theoretic model structure over cubes with one connection presenting spaces
Ceragioli, Lorenzo	(CSF) IFCIL: An Information Flow Configuration Language for SELinux (FCS) Automatic Fair Exchanges
Ceresa, Martin	(FMBC) Multi: a Formal Playground for Smart Multi-contract interaction
Cerna, David	(UNIF) Higher-Order Unification with Definition by Cases
Chakraborty, Sourav	(CP) On Quantitative Testing of Samplers (MC) Designing Samplers is Easy: The Boon of Testers
Chakraborty, Supratik	(IJCAR) On eventual non-negativity and positivity for the weighted sum of powers of matrices (VardiFest) To Count or Not to Count: A Personal Perspective
Chakravarty, Manuel	(FMBC) Designing EUTxO smart contracts as communicating state machines: the case of simulating accounts
Chandar, Sarath	(CP) Combining Reinforcement Learning and Constraint Programming for Sequence-Generation Tasks with Hard Constraints (CP) Combining Reinforcement Learning and Constraint Programming for Sequence-Generation Tasks with Hard Constraints - Extended Abstract
Chang, Bor-Yuh Evan	(WiL) Automated Logic-Based Reasoning for Analyzing Prime Video Code
Chapman, James	(FMBC) Designing EUTxO smart contracts as communicating state machines: the case of simulating accounts (FMBC) Determinism of ledger updates (FMBC) Human and machine-readable models of state machines for the Cardano ledger
Charalambidis, Angelos	(ICLP) Strong Equivalence of Logic Programs with Ordered Disjunction: a Logical Perspective
Charatonik, Witold	(ITP) The Zoo of Lambda-Calculus Reduction Strategies, and Coq
Charguéraud, Arthur	(ASL) Polishing a Rough Diamond: An Enhanced Separation Logic for Heap Space under Garbage Collection
Chatterjee, Krishnendu	(CAV) Sound and Complete Certificates for Quantitative Termination Analysis of Probabilistic Programs
Chatterjee, Prantik	(CAV) Proof-guided Underapproximation Widening for Bounded Model Checking
Chaudhri, Vinay	(LogTeach) The Herbrand Manifesto: Thinking Inside the Box
Cheang, Kevin	(CAV) UCLID5: Multi-Modal Formal Modeling, Verification, and Synthesis
Chen, Carol	(ITP) Formalizing Algorithmic Bounds in the Query Model in EasyCrypt
Chen, Dingding	(CP) Completeness Matters: Towards Efficient Caching in Tree-based Synchronous Backtracking Search for DCOPs
Chen, Haibo	(CAV) Affine Loop Invariant Generation via Matrix Algebra
Chen, Mingshuai	(CAV) Does a Program Yield the Right Distribution? Verifying Probabilistic Programs via Generating Functions
Chen, Taolue	(CAV) PoS4MPC: Automated Security Policy Synthesis for Secure Multi-Party Computation
Chen, Zhuo	(ICLP) Modeling and Reasoning in Event Calculus using Goal-Directed Constraint Answer Set Programming (Extended Abstract)
Chen, Ziyu	(CP) Completeness Matters: Towards Efficient Caching in Tree-based Synchronous Backtracking Search for DCOPs
Cheng, Chih-Hong	(FoMLAS) Formal Specification for Learning-Enabled Autonomous Systems (Extended Abstract)
Cherif, Mohamed Sami	(CP) From Crossing-Free Resolution to Max-SAT Resolution
Cherradi, El Mehdi	(HoTT/UF) Models of homotopy type theory from the Yoneda embedding
Cherubini, Felix	(HoTT/UF) Towards computing cohomology of dependent abelian groups
Cheukam-Ngouonou, Jovial	(CP) Acquiring Maps of Interrelated Conjectures on Sharp Bounds (CP) A Boolean Formula Seeker in the Context of Acquiring Maps of Interrelated Conjectures on Sharp Bounds (CP) Extended Abstract: Acquiring Maps of Interrelated Conjectures on Sharp Bounds
Cheung, Kevin K. H.	(KR) Solving Lam's Problem via SAT and Isomorph-Free Exhaustive Generation
Cheval, Vincent	(CSF) Symbolic protocol verification with dice: process equivalences in the presence of probabilities
Chew, Leroy	(SAT) Relating existing powerful proof systems for QBF (QBF) Strategy Extraction and Proof (PC) Strategy Extraction and Proof
Chiariello, Francesco	(ICLP) ASP-Based Declarative Process Mining
Chida, Nariyoshi	(FSCD) On Lookaheads in Regular Expressions with Backreferences
Chingoma, Julian	(KR) Simulating Multiwinner Voting Rules in Judgment Aggregation
Chistikov, Dmitry	(LICS) Geometric decision procedures and the VC dimension of linear arithmetic theories
Chlebowski, Szymon	(IJCAR) Synthetic tableaux: minimal tableau search heuristics
Chlipala, Adam	(ITP) Accelerating Verified-Compiler Development with a Verified Rewriting Engine (ITP) Automatic Test-Case Reduction in Proof Assistants: A Case Study in Coq (CAV) Hemiola: A DSL and Verification Tools to Guide Design and Proof of Hierarchical Cache-Coherence Protocols (CSF) Adversary Safety by Construction in a Language of Cryptographic Protocols
Chockler, Hana	(WOLVERINE) Explainable Artificial Intelligence
Choi, Joonwon	(CAV) Hemiola: A DSL and Verification Tools to Guide Design and Proof of Hierarchical Cache-Coherence Protocols
Choi, Yejin	(KR) Neuro-Symbolic Adventures on Commonsense Knowledge and Reasoning
Chowdhury, Md Solimul	(SAT) Migrating Solver State
Chrpa, Lukáš	(ICLP) Determining Action Reversibility in STRIPS Using Answer Set Programming with Quantifiers
Chun, Inwhan	(CAV) SMT-based Translation Validation for Machine Learning Compiler
Ciampi, Michele	(CSF) Collusion-Preserving Computation without a Mediator
Cifra, Milan	(FOMEO) First-Order Logic Workbook
Cima, Gianluca	(KR) LACE: A Logical Approach to Collective Entity Resolution
Cimatti, Alessandro	(CAV) Abstraction Modulo Stability for Reverse Engineering (SMT) The VMT-LIB Language and Tools (SMT) NORMA: a tool for the analysis of Relay-based Railway Interlocking Systems (VardiFest) The Safety Fragment of LTL
Classen, Jens	(KR) Projection of Belief in the Presence of Nondeterministic Actions and Fallible Sensing
Climent, Laura	(CP) Large Neighborhood Search for Robust Solutions for Constraint Satisfaction Problems with Ordered Domains (CP) Large Neighborhood Search for Robust Solutions for Constraint Satisfaction Problems with Ordered Domains
Cloerkes, Daniel	(WST) AProVE 2022
Coenen, Norine	(CAV) Explaining Hyperproperty Violations
Cohen, Irun	(VardiFest) Natural Autoencoding
Cohen, Joshua M.	(CAV) Verified Erasure Correction in Coq with MathComp and VST
Cohen, Liron	(Mentoring Workshop) Managing a life that also includes research (FSCD) Constructing Unprejudiced Extensional Type Theories with Choices via Modalities
Colange, Maximilien	(CAV) From Spot 2.0 to Spot 2.10: What's New?
Collenette, Joe	(XLoKR) Dialogue-Based Explanations of Reasoning in Rule-based Systems
Competitions, Awards And	(SAT) Awards / Competition Results - I (with Live Broadcast) (PERR) Regression verification of unbalanced recursive functions with multiple calls
Confalonieri, Roberto	(DL) Evaluating the Interpretability of Threshold Operators
Contente, Michele	(HoTT/UF) The Compatibility of MF with HoTT
Contissa, Giuseppe	(GDE) Integration of Logical English and s(CASP)
Cooper, Martin	(CP) Complexity of Minimum-Size Arc-Inconsistency Explanations (CP) Isomorphisms between STRIPS problems and sub-problems
Coppé, Vianney	(CP) Solving the Constrained Single-Row Facility Layout Problem with Decision Diagrams (CP) Solving the Constrained Single-Row Facility Layout Problem with Decision Diagrams (Extended Abstract)
Cordeiro, Lucas C.	(FoMLAS) Counter-Example Guided Neural Network Compression Refinement (CEG4N)
Cortier, Veronique	(CSF) A small bound on the number of sessions for security protocols (GuttmanFest) How to Explain Security Protocols to Your Children
Costantini, Stefania	(ASPOCP) Epistemic Logic Programs: a Novel Perspective and some Extensions (NMR) Modelling Agents Roles in the Epistemic Logic L-DINF (VardiFest) An Epistemic Logic for modelling Cooperative Agents
Coulombe, Christopher	(CP) Constraint Acquisition Based on Solution Counting (CP) Extended Abstract: Constraint Acquisition Based on Solution Counting
Cousineau, Denis	(Coq) Trakt: a generic pre-processing tactic for theory-based proof automation
Cozman, Fabio	(NMR) Bipolar Argumentation Frameworks with Explicit Conclusions: Connecting Argumentation and Logic Programming (KR) A Credal Least Undefined Stable Semantics for Probabilistic Logic Programs and Probabilistic Argumentation (XLoKR) Invited Talk: Explaining and Arguing with Facts and Rules
Crance, Enzo	(Coq) Trakt: a generic pre-processing tactic for theory-based proof automation
Crubillé, Raphaëlle	(CSF) Symbolic protocol verification with dice: process equivalences in the presence of probabilities
Cseh, Ágnes	(CP) Computing relaxations for the three-dimensional stable matching problem with cyclic preferences
Cuellar, Jorge	(GuttmanFest) Three Branches of Accountability
Cuenca, Alba	(WiL) A goal-oriented proof system for epistemic modal logic
Cuenca Grau, Bernardo	(KR) Faithful Approaches to Rule Learning
Cunningham, Robert	(CSF) Adversary Safety by Construction in a Language of Cryptographic Protocols
Curry, Timothy	(CP) DUELMIPs: Jointly Optimizing Software Defined Network Functionality and Security
Curzi, Gianluca	(LICS) Cyclic Implicit Complexity
Cuteri, Bernardo	(ICLP) Solving Problems in PH with ASP(Q)
Czajka, Lukasz	(FSCD) Restricting tree grammars with term rewriting
Czerwiński, Wojciech	(LICS) Lower Bounds for the Reachability Problem in Fixed Dimensional VASSes (LICS) The boundedness and zero isolation problems for weighted automata over nonnegative rationals
Câmara, Igor de Camargo E Souza	(DL) Rational defeasible subsumption in DLs with nested quantifiers: the case of ELI_⊥
Côté, Alain	(CP) Scheduling the Equipment Maintenance of an Electric Power Transmission Network using Constraint Programming (CP) Extended Abstract for : Scheduling the Equipment Maintenance of an Electric Power Transmission Network using Constraint Programming
D
D'Argenio, Pedro R.	(CAV) Playing Against Fair Adversaries in Stochastic Games with Total Rewards
Dachselt, Raimund	(CAV) Explaining Hyperproperty Violations (IJCAR) Evonne: Interactive Proof Visualization for Description Logics (System Description)
Daggitt, Matthew	(FoMLAS) Vehicle: A High-Level Language for Embedding Logical Specifications in Neural Networks
Daggitt, Matthew L.	(CAV) Neural Network Robustness as a Verification Property: A Principled Case Study (FoMLAS) Differentiable Logics for Neural Network Verification (FoMLAS) Why Robust Natural Language Understanding is a Challenge
Dagnino, Francesco	(FSCD) A Fibrational Tale of Operational Logical Relations (LICS) Logical Foundations of Quantitative Equality
Dahlqvist, Fredrik	(VeriProp) Deterministic stream-sampling for probabilistic programming: semantics and verification
Dal Lago, Ugo	(FSCD) On Quantitative Algebraic Higher-Order Theories (LICS) Reasonable Space for the Lambda-Calculus, Logarithmically (LICS) Curry and Howard Meet Borel
Dalla, Marco	(CP) Automated SAT Problem Feature Extraction using 1 Convolutional Autoencoders
Dallaire, Daniel	(SC^2) Enumerating Projective Planes of Order Nine with Proof Verification
Dallon, Antoine	(CSF) A small bound on the number of sessions for security protocols
Dalmonte, Tiziano	(ARQNL) Reasoning in Non-normal Modal Description Logics
Dana-Picard, Noah	(ThEdu) Invited Talk: Computer-assisted proofs and automated methods in Mathematics Education
Dang, Nguyen	(CP) A framework for generating informative benchmark instances (ModRef) A portfolio-based analysis method for competition results (ModRef) A Constraint-Based Tool for Generating Benchmark Instances
Dardinier, Thibault	(CAV) Sound Automation of Magic Wands
Dartois, Luc	(LICS) Efficient Construction of Reversible Transducers from Regular Transducer Expressions
Darulova, Eva	(ITP) Dandelion: Certified Approximations of Elementary Functions
Das, Anupam	(PC) Towards higher order proof complexity (FSCD) Decision problems for linear logic with least and greatest fixed points (LICS) Cyclic Implicit Complexity (IJCAR) Cyclic Proofs, Hypersequents, and Transitive Closure Logic
Davenport, James H.	(SC^2) NP: SMT-Solving Combinatorial Inequalities
David, Bogdan	(SC^2) Automatic Deployment of Component-based Applications in the Cloud
Davila, Jacinto	(GDE) Integration of Logical English and s(CASP)
Davis, Ernest	(LogTeach) My Experience Teaching Logic in Undergraduate AI at NYU}
Dawar, Anuj	(LICS) Separating LREC from LFP
De, Abhishek	(FSCD) Decision problems for linear logic with least and greatest fixed points
de Almeida Borges, Ana	(DECFOML) The Quantified Reflection Calculus as a Modal Logic (ARQNL) Towards a Coq formalization of a quantified modal logic (Coq) Coq Community Survey 2022: Summary of Results
De Angelis, Emanuele	(ICLP) Verifying Catamorphism-Based Contracts using Constrained Horn Clauses
De Bortoli, Filippo	(KR) Filippo De Bortoli - Reasoning Efficiently with Description Logics that Count
de Camargo E Souza Câmara, Igor	(NMR) Rational defeasible subsumption in DLs with nested quantifiers: the case of ELI_⊥
de Felice, Giovanni	(LICS) Monoidal Streams for Dataflow Programming
de Frutos-Fernández, María Inés	(ITP) Formalizing the ring of adèles of a global field
De Giacomo, Giuseppe	(KR) Act for Your Duties but Maintain Your Rights (KR) Automatic Synthesis of Dynamic Norms for Multi-Agent Systems (VardiFest) Comments from Giuseppe, Kuldeep, and Kristin
de Givry, Simon	(CP) Structured Set Variable Domains in Bayesian Network Structure Learning (CP) Parallel Hybrid Best-First Search
de Givry, Simon	(CP) Interdisciplinary Research -- Cost Function Network for Life Sciences
de Haan, Ronald	(KR) Simulating Multiwinner Voting Rules in Judgment Aggregation
De Oliveira Oliveira, Mateus	(CAV) Synthesis and Analysis of Petri Nets from Causal Specifications
De Raedt, Luc	(ICLP) Inference and Learning with Model Uncertainty in Probabilistic Logic Programs (ICLP) DeepStochLog: Neural Stochastic Logic Programming
de Sousa Ribeiro, Manuel	(KR) Looking Inside the Black-Box: Logic-based Explanations for Neural Networks
de Vries, Ben	(FOMEO) LogInd, a tool for supporting students in mastering structural induction
Degano, Pierpaolo	(CSF) IFCIL: An Information Flow Configuration Language for SELinux (FCS) Automatic Fair Exchanges (GuttmanFest) Verifying a Blockchain-Based Remote Debugging Protocol for Bug Bounty
Delahaye, David	(IJCAR) Goéland : A Concurrent Tableau-Based Theorem Prover (System Description)
Delannoy, Remi	(LICS) On Almost-Uniform Generation of SAT Solutions: The power of 3-wise independent hashing
Delaune, Stephanie	(CSF) A small bound on the number of sessions for security protocols (CSF) Cracking the Stateful Nut -- Computational Proofs of Stateful Security Protocols using the Squirrel Proof Assistant (CSF) So near and yet so far: formal verification of distance bounding protocols
Delecluse, Augustin	(CP) Sequence Variables for Routing Problems (CP) Extended Abstract: Sequence Variables for Routing Problems
Delgrande, James	(KR) Projection of Belief in the Presence of Nondeterministic Actions and Fallible Sensing
Demasi, Ramiro	(CAV) Playing Against Fair Adversaries in Stochastic Games with Total Rewards
Denecker, Marc	(ICLP) Analyzing Semantics of Aggregate Answer Set Programming Using Approximation Fixpoint Theory (ICLP) Nested Justification Systems
Dennis, Louise	(XLoKR) Dialogue-Based Explanations of Reasoning in Rule-based Systems
DePace, Gabe	(CP) DUELMIPs: Jointly Optimizing Software Defined Network Functionality and Security
Derek, Ante	(CSF) Conditional Observational Equivalence and Off-line Guessing Attacks in Multiset Rewriting
Derkinderen, Vincent	(ICLP) Inference and Learning with Model Uncertainty in Probabilistic Logic Programs
Desharnais, Martin	(ITP) Seventeen Provers under the Hammer
Desmartin, Remi	(FoMLAS) Neural Networks in Imandra: Matrix Representation as a Verification Choice
Dev Gupta, Sharmi	(CP) Finding Counterfactual Explanations through Constraint Relaxations
Devriese, Dominique	(CSF) Proving full-system security properties under multiple attacker models on capability machines (FCS) pi_RA: A pi-calculus for verifying protocols that use remote attestation
Dhami, Devendra Singh	(KR) Sum-Product Loop Programming: From Probabilistic Circuits to Loop Programming (KR) Neural-Probabilistic Answer Set Programming
Di, Jieqi	(LICS) Computable PAC Learning of Continuous Features
Di Guardia, Rémi	(TLLA-LINEARITY) Bottom-Up Sequentialization of Unit-Free MALL Proof Nets
Di Lavore, Elena	(LICS) Monoidal Streams for Dataflow Programming (WiL) Monoidal Width -- Extended Abstract
Di Pierro, Alessandra	(GuttmanFest) Quantum Machine Learning and Fraud Detection
Di Stasio, Antonio	(VardiFest) LTLf Synthesis Under Environment Specifications
Di Stefano, Federica	(NMR) Pointwise Circumscription in Description Logics
Di Stefano, Federica	(DL) Pointwise Circumscription in Description Logics
Dilkas, Paulius	(MC) Recursive Solutions to First-Order Model Counting (MC) Generating Random Weighted Model Counting Instances: An Empirical Analysis with Varying Primal Treewidth
Dill, David	(IJCAR) Reasoning About Vectors using an SMT Theory of Sequences
Dillies, Yaël	(ITP) Formalizing Szemerédi's Regularity Lemma in Lean
Dimitrov, Dimitar I.	(CAV) Shared Certificates for Neural Network Verification
Ding, Ming	(CSF) Universal Optimality and Robust Utility Bounds for Metric Differential Privacy
Dixon, Clare	(IJCAR) Local Reductions for the Modal Cube
Dixon, Clare	(XLoKR) Dialogue-Based Explanations of Reasoning in Rule-based Systems
Diéguez, Martín	(KR) A Gödel calculus for Linear Temporal Logic (DL) Advanced languages of terms for ontologies
Do, Quoc Huy	(GuttmanFest) A Tutorial-Style Introduction to DY*
Dollase, Stefan	(WST) AProVE 2022
Doré, Maximilian	(HoTT/UF) Elementary Simplicial Collapses in Cubical Agda
Douence, Rémi	(CP) Acquiring Maps of Interrelated Conjectures on Sharp Bounds (CP) Extended Abstract: Acquiring Maps of Interrelated Conjectures on Sharp Bounds
Dougherty, Daniel	(GuttmanFest) Model Finding for Exploration
Doumane, Amina	(LICS) Bouncing threads for circular and non-wellfounded proofs
Doveri, Kyveli	(CAV) FORQ-based Language Inclusion Formal Testing
Dowek, Gilles	(FSCD) Linear lambda-calculus is linear (LFMTP) An Implementation of Set Theory with Pointed Graphs in Dedukti (IJCAR) From the Universality of Mathematical Truth to the Interoperability of Proof Systems (Invited Talk)
Doyen, Laurent	(LICS) Stochastic Games with Synchronizing Objectives
Drab, Tomasz	(ITP) The Zoo of Lambda-Calculus Reduction Strategies, and Coq
Drachsler Cohen, Dana	(SYNT) Future Work and Open Challenges Panel – Authors+Chairs (FCS) VeNuS: Neural Network Robustness Specifications via Verifier-guided Optimization (WOLVERINE) Robustness of Neural Networks
Dragoi, Cezara	(FMBC) A Domain Specific Language for Testing Consensus Implementations
Draheim, Dirk	(GDE) First order logic and commonsense reasoning: a path less travelled (IJCAR) GK: Implementing Full First Order Default Logic for Commonsense Reasoning (System Description)
Dreier, Jan	(CP) CSP Beyond Tractable Constraint Languages (LICS) Model Checking on Interpretations of Classes of Bounded Local Cliquewidth (LICS) Treelike decompositions for transductions of sparse graphs
Drăgan, Constantin Cătălin	(CSF) Machine-Checked Proofs of Privacy Against Malicious Boards for Selene & Co
Du, Hanxiang	(ICLP) A Preliminary Data-driven Analysis of Common Errors Encountered by Novice Answer Set Programmers
Duarte, André	(IJCAR) Ground joinability and connectedness in the superposition calculus
Dubois, Jérôme	(CAV) From Spot 2.0 to Spot 2.10: What's New?
Dudenhefner, Andrej	(ITP) Undecidability of Dyadic First-Order Logic in Coq (FSCD) Certified Decision Procedures for Two-Counter Machines
Dudenhefner, Andrej	(Coq) A Coq Library for Mechanised First-Order Logic
Dundua, Besik	(IFIP-WG1.6) The International School on Rewriting
Dung, Ho Tuan	(ICLP) On Model Reconciliation: How to Reconcile When Robot Does not Know Human’s Model?
Dupressoir, François	(CSF) Bringing State-Separating Proofs to EasyCrypt - A Security Proof for Cryptobox (CSF) Machine-Checked Proofs of Privacy Against Malicious Boards for Selene & Co
Dupuis, Frédéric	(ITP) Formalized functional analysis with semilinear maps
Duret-Lutz, Alexandre	(CAV) From Spot 2.0 to Spot 2.10: What's New?
Durán, Francisco	(IJCAR) Equational Unification and Matching, and Symbolic Reachability Analysis in Maude 3.2 (System Description)
Dutertre, Bruno	(SMT) Panel discussion "SMT: Past, Present and Future"
Dvořák, Wolfgang	(NMR) The Effect of Preferences in Abstract Argumentation Under a Claim-Centric View (PCCR) Tractable Abstract Argumentation via Backdoor-Treewidth (KR) Rediscovering Argumentation Principles Utilizing Collective Attacks
Dwyer Satterfield, Saraid	(UNIF) Graph-Embedded Term Rewrite Systems and Applications (A Preliminary Report)
Dyer, Tristan	(GuttmanFest) Prototyping Formal Methods Tools: a Protocol Analysis Case Study
Déharbe, David	(SMT) Business Meeting
Díaz-Caro, Alejandro	(FSCD) Linear lambda-calculus is linear
E
Eades Iii, Harley	(WiL) A Mixed Linear and Graded Logic-Extended Abstract
Echenim, Mnacho	(ASL) Two Results on Separation Logic With Theory Reasoning
Eckel, Rory	(ICLP) A Preliminary Data-driven Analysis of Common Errors Encountered by Novice Answer Set Programmers
Edmonds, Chelsea	(ITP) Formalising Fisher’s Inequality: Formal Linear Algebraic Techniques in Combinatorics
Ehrhard, Thomas	(TLLA-LINEARITY) A coherent differential PCF
Eifler, Rebecca	(XLoKR) Explaining Soft-Goal Conflicts through Constraint Relaxations
Eisenhofer, Clemens	(SMT) User-Propagators for Custom Theories in SMT Solving
Eiter, Thomas	(ICLP) A Neuro-Symbolic ASP Pipeline for Visual Question Answering (ICLP) Large-Neighbourhood Search for ASP Optimisation (KR) ALASPO: An Adaptive Large-Neighbourhood ASP Optimiser (KR) Chasing streams with existential rules (DL) Reasoning on Multi-Relational Contextual Hierarchies via Answer Set Programming with Algebraic Measures (DL) Hybrid Answer Set Programming: Opportunities and Challenges
Eiter, Thomas	(NMR) Hybrid Anwer Set Programming: Opportunities and Challenges
Eiter, Thomas	(NMR) Reasoning on Multi-Relational Contextual Hierarchies via Answer Set Programming with Algebraic Measures
Ek, Alexander	(CP) Explaining Propagation for Gini and Spread with Variable Mean (CP) Explaining Propagation for Gini and Spread with Variable Mean (Extended Abstract)
Eker, Steven	(IJCAR) Equational Unification and Matching, and Symbolic Reachability Analysis in Maude 3.2 (System Description)
El-Kholany, Mohammed	(ICLP) Problem Decomposition and Multi-shot ASP Solving for Job-shop Scheduling (ICLP) Solving a Multi-resource Partial-ordering Flexible Variant of the Job-shop Scheduling Problem with Hybrid ASP
El-Korashy, Akram	(CSF) SecurePtrs: Proving Secure Compilation Using Data-Flow Back-Translation and Turn-Taking Simulation
Eldefrawy, Karim	(FCS) Computer-aided Verification and Automated Synthesis of Cryptographic Protocols
Elmassad, Mohamed	(CSF) Locked Circuit Indistinguishability: A Notion of Security for Logic Locking
Endriss, Ulle	(KR) Simulating Multiwinner Voting Rules in Judgment Aggregation
Endrullis, Jörg	(IFIP-WG1.6) RLooP (the Rewriting List of open Problems) (TERMGRAPH) A PBPO+ Graph Rewriting Tutorial (TERMGRAPH) PBPO+ Graph Rewriting in Context
Enea, Constantin	(FMBC) A Domain Specific Language for Testing Consensus Implementations (FRIDA) Quorum Tree Abstractions of Consensus Protocols
England, Matthew	(SC^2) NP: SMT-Solving Combinatorial Inequalities
Erașcu, Mădălina	(SC^2) Automatic Deployment of Component-based Applications in the Cloud
Erbatur, Serdar	(FSCD) Combined Hierarchical Matching: The Regular Case (UNIF) Graph-Embedded Term Rewrite Systems and Applications (A Preliminary Report)
Erbsen, Andres	(ITP) Accelerating Verified-Compiler Development with a Verified Rewriting Engine (Coq) 10 Years of Superlinear Slowness in Coq
Erdem, Esra	(ASPOCP) Hard Variants of Stable Marriage Problems: An Empirical Comparison of ASP with Other Computing Paradigms (KR) Hybrid Conditional Planning for Robotic Applications (Extended Abstract) (KR) A General Framework for Stable Roommates Problems using Answer Set Programming (KR) Reasoning about Cardinal Directions between 3-Dimensional Extended Objects using Answer Set Programming (XLoKR) Invited Talk: Explanation Generation in Applications of Answer Set Programming
Escamocher, Guillaume	(CP) Computing relaxations for the three-dimensional stable matching problem with cyclic preferences
Eschen, Agnes Moesgård	(Isabelle) On Axiomatic Systems for Classical Propositional Logic
Escobar, Santiago	(IJCAR) Equational Unification and Matching, and Symbolic Reachability Analysis in Maude 3.2 (System Description)
Escobar, Santiago	(GuttmanFest) Protocol Analysis with Time and Space
Esen, Zafer	(SMT) An SMT-LIB Theory of Heaps (DSV) Eldarica and TriCera: towards an open verification framework
Espasa, Joan	(CP) A framework for generating informative benchmark instances (CP) Plotting: A Planning Problem With Complex Transitions
Estaji, Ehsan	(CSF) Machine-Checked Proofs of Privacy Against Malicious Boards for Selene & Co
Evdokimova, Anastasiia	(ASL) Proving Logical Atomicity using Lock Invariants
Everardo, Flavio	(ICLP) ApproxASP – A Scalable Approximate Answer Set Counter
F
Faber, Wolfgang	(ICLP) Determining Action Reversibility in STRIPS Using Answer Set Programming with Quantifiers
Faella, Marco	(CAV) Reasoning about Data Trees using CHCs
Faggian, Claudia	(FSCD) Strategies for Asymptotic Normalization
Fagin, Ronald	(VardiFest) Descriptive complexity and inexpressibly proofs (VardiFest) A Comment to Moshe by Ron Fagin
Fainekos, Georgios	(NSV) Adversarial Testing and Repair for Neural Network based Control Systems using Optimization
Falakh, Faiq Miftakhul	(NMR) AGM Revision in Description Logics Under Fixed-Domain Semantics (DL) AGM Revision in Description Logics Under Fixed-Domain Semantics
Falleri, Jean-Rémy	(Coq) Coq Community Survey 2022: Summary of Results
Falque, Thibault	(CP) Aggressive Bound Descent for Constraint Optimization (CP) On PB Encodings for Constraint Problems
Fan, Yuxin	(CAV) PoS4MPC: Automated Security Policy Synthesis for Secure Multi-Party Computation
Fang, Bin	(CAV) Affine Loop Invariant Generation via Matrix Algebra
Fang, Wang	(CAV) Verifying Fairness in Quantum Machine Learning
Fargier, Helene	(CP) Nucleus-Satellites Systems of OMDDs for Reducing the Size of Compiled Forms
Favorito, Marco	(KR) On the Relationship between Shy and Warded Datalog+/-
Fehrle, Jim	(Coq) Coq Community Survey 2022: Summary of Results
Felicissimo, Thiago	(FSCD) Adequate and computational encodings in the logical framework Dedukti
Felli, Paolo	(IJCAR) CTL* model checking for data-aware dynamic systems with arithmetic
Felty, Amy	(ITP) (Invited) Modelling and Verifying Properties of Biological Neural Networks (LFMTP) Metatheory of Proto-Quipper in Hybrid: Context Relations Revisited
Feng, Weizhi	(CAV) Divide-and-Conquer Determinization of Büchi Automata based on SCC Decomposition
Ferariu, Tudor	(FMBC) Designing EUTxO smart contracts as communicating state machines: the case of simulating accounts
Ferilli, Stefano	(ICLP) Abduction in Probabilistic Logic Programs
Fernandes, Natasha	(CSF) Universal Optimality and Robust Utility Bounds for Metric Differential Privacy
Fernandez, Maribel	(FSCD) A Certified Algorithm for AC-Unification
Fernandez Gil, Oliver	(UNIF) Restricted Unification in the Description Logic FLbot
Fernández-Duque, David	(KR) The Topology of Surprise (KR) A Gödel calculus for Linear Temporal Logic
Ferrando, Andrea	(SMT) NORMA: a tool for the analysis of Relay-based Railway Interlocking Systems
Ferrara, Andrea	(VardiFest) Capturing abscondings
Ferrari, Mauro	(IJCAR) SAT-based Proof Search in Intermediate Propositional Logics
Ferreira, João	(KR) Looking Inside the Black-Box: Logic-based Explanations for Neural Networks
Ferreira Santos, Felipe	(LICS) Separating LREC from LFP
Ferreira Silva, Gabriel	(FSCD) A Certified Algorithm for AC-Unification
Ferro, Quentin	(NSV) Neural Network Precision Tuning Using Stochastic Arithmetic
Fichte, Johannes K.	(SAT) Proofs for Propositional Model Counting (ICLP) Rushing and Strolling among Answer Sets – Navigation Made Easy (ICLP) ApproxASP – A Scalable Approximate Answer Set Counter (PCCR) Parameterized Algorithmics and Counting: Treewidth in Practice (KR) Rushing and Strolling among Answer Sets -- Navigation Made Easy (Extended Abstract)
Fidan, Müge	(KR) A General Framework for Stable Roommates Problems using Answer Set Programming
Figueira, Diego	(LICS) Reasoning on Data Words over Numeric Domains
Fijalkow, Nathanaël	(KR) Private and public affairs in strategic reasoning
Findelair, Arthur	(NMR) There and Back Again: Combining Nonmonotonic Logical Reasoning and Deep Learning on an Assistive Robot
Finkbeiner, Bernd	(SYNT) LTL Synthesis with Transformer Neural Networks (CAV) Information Flow Guided Synthesis (CAV) Explaining Hyperproperty Violations (CAV) Software Verification of Hyperproperties Beyond k-Safety (CSF) Prophecy Variables for Hyperproperty Verification (LICS) Deciding Hyperproperties Combined with Functional Specifications
Finster, Eric	(LICS) A Type Theory for Strictly Unital Infinity-Categories
Finster, Eric	(HoTT/UF) TBA
Fioravanti, Fabio	(ICLP) Verifying Catamorphism-Based Contracts using Constrained Horn Clauses
Fiore, Marcelo	(FSCD) A combinatorial approach to higher-order structure for polynomial functors
Fiorentini, Camillo	(IJCAR) SAT-based Proof Search in Intermediate Propositional Logics
Fischer, Marc	(CAV) Shared Certificates for Neural Network Verification
Fisman, Dana	(WiL) A normalized edit distance on finite and infinite words
Flaminio, Tommaso	(KR) Compound conditionals as random quantities and Boolean algebras
Flaten, Jarl G. Taxerås	(HoTT/UF) The internal AB axioms
Fleury, Mathias	(POS) Scalable Proof Producing Multi-Threaded SAT Solving with Gimsatul through Sharing instead of Copying Clauses
Focardi, Riccardo	(GuttmanFest) Secure Key Management Policies in Strand Spaces
Fodor, Paul	(ICLP) Knowledge Authoring with Factual English
Fokkinga, Daniël	(MC) Stochastic Constraint Optimisation with Applications in Network Analysis
Fontaine, Pascal	(SC^2) Decidability of difference logics with unary predicates
Ford, Chase	(LICS) Graded Monads and Behavioural Equivalence Games
Formisano, Andrea	(ASPOCP) Epistemic Logic Programs: a Novel Perspective and some Extensions (NMR) Modelling Agents Roles in the Epistemic Logic L-DINF (VardiFest) An Epistemic Logic for modelling Cooperative Agents
Forster, Yannick	(ITP) Synthetic Kolmogorov Complexity in Coq (Coq) A Coq Library for Mechanised First-Order Logic
Fortin, Marie	(Mentoring Workshop) Welcome (KR) Unique Characterisability and Learnability of Temporal Instance Queries (KR) Interpolants and Explicit Definitions in Extensions of the Description Logic EL (DL) Reverse Engineering of Temporal Queries with and without LTL Ontologies: First Steps
Fox, Anthony	(ITP) Taming an Authoritative Armv8 ISA Specification: L3 Validation and CakeML Compiler Verification
Fraccaroli, Michele	(ICLP) Exploiting Parameters Learning for Hyper-parameters Optimization in Deep Neural Networks
Fraer, Ranan	(VardiFest) Moshe Vardi and Intel Corporation: Long and Fruitful Collaboration
Francescutto, Giulia	(ICLP) Solving a Multi-resource Partial-ordering Flexible Variant of the Job-shop Scheduling Problem with Hybrid ASP
Franconi, Enrico	(DL) Accessing Document Data Sources using Referring Expression Types
Frank, Jeremy	(XLoKR) Explaining Soft-Goal Conflicts through Constraint Relaxations
Fredlund, Lars-Åke	(FMBC) Automatic generation of attacker contracts in Solidity
Fredrikson, Matt	(FoMLAS) Self-Correcting Neural Networks For Safe Classification
Freer, Cameron	(LICS) Computable PAC Learning of Continuous Features
Freiberger, Felix	(FOMEO) Teaching Concurrency with pseuCo Book
Fremont, Daniel	(CAV) Randomized Synthesis for Diversity and Cost Constraints with Control Improvisation (MC) Randomized Synthesis for Diversity and Cost Constraints with Control Improvisation
Frenkel, Hadar	(CAV) Explaining Hyperproperty Violations
Friese, Tom	(DL) On the Eve of True Explainability for OWL Ontologies: Description Logic Proofs with Evee and Evonne (XLoKR) Explaining Description Logic Entailments in Practice with Evee and Evonne
Frittella, Sabine	(IJCAR) Paraconsistent Gödel modal logic
Frohn, Florian	(WST) Deciding Termination of Uniform Loops with Polynomial Parameterized Complexity (WST) A Calculus for Modular Non-Termination Proofs by Loop Acceleration (WST) AProVE 2022 (WST) LoAT: The Loop Acceleration Tool (IJCAR) Proving Non-Termination and Lower Runtime Bounds with LoAT (System Description)
From, Asta Halkjær	(Isabelle) On Termination for Hybrid Tableaux (ITP) Verifying a Sequent Calculus Prover for First-Order Logic with Functions in Isabelle/HOL (FOMEO) Formal Methods Online: Sequent Calculus Verifier (SeCaV)
Fromherz, Aymeric	(FoMLAS) Self-Correcting Neural Networks For Safe Classification
Fu, Hongfei	(CAV) Affine Loop Invariant Generation via Matrix Algebra
Fuenmayor, David	(PAAR) Automated Reasoning in Non-classical Logics in the TPTP World
Fuhs, Carsten	(WST) A Calculus for Modular Non-Termination Proofs by Loop Acceleration (WST) Runtime complexity of parallel-innermost term rewriting at TermComp 2022 (WST) AProVE 2022 (IWC) On Confluence of Parallel-Innermost Term Rewriting
Fujita, Tomohiro	(IJCAR) Formula Simplification via Invariance Detection by Algebraically Indexed Types (ONLINE)
Fukiage, Tsubasa	(POS) DPS: A Framework for Deterministic Parallel SAT Solvers
Fuller, Benjamin	(CP) DUELMIPs: Jointly Optimizing Software Defined Network Functionality and Security
Funk, Maurice	(DL) Actively Learning ELIQs in the Presence of DL-Lite-Horn Ontologies
Fussner, Wesley	(iPRA) Interpolation via Finitely Subdirectly Irreducible Algebras
G
Gabbay, Dov	(KR) Dynamic Deontic Logic for Permitted Announcements
Gaboardi, Marco	(ITP) Formalizing Algorithmic Bounds in the Query Model in EasyCrypt (CSF) The Complexity of Verifying Boolean Programs as Differentially Private
Gaddamadugu, Pranav	(CAV) UCLID5: Multi-Modal Formal Modeling, Verification, and Synthesis
Gaevoy, Nikita	(PC) Simulations between proof systems
Gaggl, Sarah Alice	(ICLP) Rushing and Strolling among Answer Sets – Navigation Made Easy (KR) Rushing and Strolling among Answer Sets -- Navigation Made Easy (Extended Abstract)
Gaha, Mohamed	(CP) Scheduling the Equipment Maintenance of an Electric Power Transmission Network using Constraint Programming (CP) Extended Abstract for : Scheduling the Equipment Maintenance of an Electric Power Transmission Network using Constraint Programming
Gajarský, Jakup	(PCCR) Decompositions and algorithms for interpretations of sparse graphs (LICS) Model Checking on Interpretations of Classes of Bounded Local Cliquewidth (LICS) Stable graphs of bounded twin-width (LICS) Treelike decompositions for transductions of sparse graphs
Galal, Zeinab	(FSCD) A combinatorial approach to higher-order structure for polynomial functors
Galesi, Nicola	(PC) On vanishing sums of roots of unity in polynomial calculus and sum-of-squares
Gallego Arias, Emilio Jesús	(Coq) jsCoq: Literate Proof Documents Dressed for the Web (Coq) Discussion with Coq Core Development Team (Coq) Coq Community Survey 2022: Summary of Results
Galletta, Letterio	(CSF) IFCIL: An Information Flow Configuration Language for SELinux (FCS) Automatic Fair Exchanges
Galletta, Letterio	(GuttmanFest) Verifying a Blockchain-Based Remote Debugging Protocol for Bug Bounty
Gallicchio, James	(IJCAR) Implicit Definitions with Differential Equations for KeYmaera X (System Description)
Galmiche, Didier	(ASL) Labelled Tableaux for Linear Time Bunched Implication Logic
Gamba, Emilio	(XLoKR) Stepwise Explanations of Unsatisfiable Constraint Programs (Extended abstract) (ModRef) Efficiently Explaining CSPs with Unsatisfiable Subset Optimization (extended abstract)
Gamboa, Ruben	(ITP) A Complete, Mechanically-Verified Proof of the Banach-Tarski Theorem in ACL2(r)
Ganardi, Moses	(LICS) Ramsey Quantifiers over Automatic Structures: Complexity and Applications to Verification (LICS) The complexity of bidirected reachability in valence systems
Ganesh, Vijay	(KR) Solving Lam's Problem via SAT and Isomorph-Free Exhaustive Generation (SC^2) An SC-Square Approach to the Minimum Kochen–Specker Problem (SMT) Goose: A Meta Solver for Deep Neural Network Verification
Ganian, Robert	(SAT) Weighted Model Counting with Twin-Width
Ganty, Pierre	(CAV) FORQ-based Language Inclusion Formal Testing
Gao, Junsong	(CP) Completeness Matters: Towards Efficient Caching in Tree-based Synchronous Backtracking Search for DCOPs
García Pradales, Guillermo	(GDE) An s(CASP) In-Browser Playground based on Ciao Prolog
Gardner, Philippa	(ASL) Exact Separation Logic
Garg, Deepak	(CSF) SecurePtrs: Proving Secure Compilation Using Data-Flow Back-Translation and Turn-Taking Simulation (FCS) Compositional Higher-order Declassification Using Logical Relations
Garg, Siddharth	(CSF) Locked Circuit Indistinguishability: A Notion of Security for Logic Locking
Garzón, Iván	(SAT) On the performance of deep generative models of realistic SAT instances
Gastin, Paul	(LICS) Efficient Construction of Reversible Transducers from Regular Transducer Expressions
Gauthier, Thibault	(FMBC) Proofgold: Blockchain for Formal Methods
Gavazzo, Francesco	(FSCD) A Fibrational Tale of Operational Logical Relations
Gaysin, Azza	(PC) Proof complexity of CSP
Gbaguidi Aisse, Alexandre	(CAV) From Spot 2.0 to Spot 2.10: What's New?
Geatti, Luca	(VardiFest) The Safety Fragment of LTL
Gebser, Martin	(ICLP) Efficient lifting of symmetry breaking constraints for complex combinatorial problems (Best Student Paper Award) (ICLP) Problem Decomposition and Multi-shot ASP Solving for Job-shop Scheduling (KR) Lifting Symmetry Breaking Constraints with Inductive Logic Programming
Geffner, Hector	(KR) Learning generalized policies without supervision using GNNs (VardiFest) Logic and Languages for Representation Learning
Gehl, Tobias	(PAAR) A Two-Watched Literal Scheme for First-Order Logic
Geibinger, Tobias	(ICLP) Large-Neighbourhood Search for ASP Optimisation (KR) ALASPO: An Adaptive Large-Neighbourhood ASP Optimiser
Geleßus, David	(ICLP) Making ProB compatible with SICStus and SWI-Prolog (Best Application Paper Award)
Genc, Begum	(CP) Finding Counterfactual Explanations through Constraint Relaxations
Gencer, Cigdem	(DL) Advanced languages of terms for ontologies
Genesereth, Michael	(LogTeach) The Herbrand Manifesto: Thinking Inside the Box
Gengelbach, Arve	(ITP) A Verified Cyclicity Checker
Gentzel, Rebecca	(CP) Heuristics for MDD Propagation in Haddock
Geoffroy, Guillaume	(LICS) A first-order completeness result about characteristic Boolean algebras in classical realizability
Georges, Aïna Linn	(CSF) Proving full-system security properties under multiple attacker models on capability machines
Gerali, Selene	(GuttmanFest) Verifying a Blockchain-Based Remote Debugging Protocol for Bug Bounty
Gerevini, Alfonso Emilio	(KR) Online Grounding of Symbolic Planning Domains in Unknown Environments
Geser, Alfons	(WST) Approximating Relative Match-Bounds
Ghica, Dan	(FSCD) Rewriting for monoidal closed categories
Ghosh, Arka	(LICS) Solvability of orbit-finite systems of linear equations
Giannakopoulou, Dimitra	(CAV) Capture, Analyze, Diagnose: Realizability Checking of Requirements in FRET
Gianola, Alessandro	(iPRA) Uniform Interpolants and Model Completions in Formal Verification of Infinite-State Systems
Giba, Stefan	(WiL) Automated Logic-Based Reasoning for Analyzing Prime Video Code
Giesl, Jürgen	(WST) Improved Automatic Complexity Analysis of Integer Programs (WST) Deciding Termination of Uniform Loops with Polynomial Parameterized Complexity (WST) AProVE 2022 (WST) Automatic Complexity Analysis of (Probabilistic) Integer Programs via KoAT (WST) LoAT: The Loop Acceleration Tool (IJCAR) Proving Non-Termination and Lower Runtime Bounds with LoAT (System Description) (IJCAR) Automatic Complexity Analysis of Integer Programs via Triangular Weakly Non-Linear Loops (VeriProp) Inferring Expected Runtimes and Sizes
Gigante, Nicola	(KR) On the Expressive Power of Intermediate and Conditional Effects in Temporal Planning (VardiFest) The Safety Fragment of LTL
Gil-Pons, Reynaldo	(CSF) Is Eve nearby? Analysing protocols under the distant-attacker assumption
Gilio, Angelo	(KR) Compound conditionals as random quantities and Boolean algebras
Gillard, Clément	(CAV) From Spot 2.0 to Spot 2.10: What's New?
Gillard, Xavier	(CP) Solving the Constrained Single-Row Facility Layout Problem with Decision Diagrams (CP) Solving the Constrained Single-Row Facility Layout Problem with Decision Diagrams (Extended Abstract)
Gindullin, Ramiz	(CP) Acquiring Maps of Interrelated Conjectures on Sharp Bounds (CP) A Boolean Formula Seeker in the Context of Acquiring Maps of Interrelated Conjectures on Sharp Bounds (CP) Extended Abstract: Acquiring Maps of Interrelated Conjectures on Sharp Bounds
Giordano, Laura	(ICLP) An ASP approach for reasoning on neural networks under a finitely many-valued semantics for weighted conditional knowledge bases (NMR) From Weighted Conditionals to a Gradual Argumentation Semantics and back (KR) A conditional, a fuzzy and a probabilistic interpretation of self-organising maps (Abstract) (DL) Reasoning about actions with EL ontologies in a temporal action theory (Extended Abstract)
Girlando, Marianna	(IJCAR) Cyclic Proofs, Hypersequents, and Transitive Closure Logic
Giráldez-Cru, Jesús	(SAT) On the performance of deep generative models of realistic SAT instances
Gittis, Andreas	(CAV) Randomized Synthesis for Diversity and Cost Constraints with Control Improvisation (MC) Randomized Synthesis for Diversity and Cost Constraints with Control Improvisation
Giustolisi, Rosario	(GuttmanFest) Security Protocols as Choreographies
Gjøsteen, Kristian	(CSF) Machine-Checked Proofs of Privacy Against Malicious Boards for Selene & Co
Glauer, Martin	(KR) Structure-based ontology extensions
Gleißner, Tobias	(ARQNL) Solving QMLTP Problems by Translation to Higher-order Logic (PAAR) Automated Reasoning in Non-classical Logics in the TPTP World
Glimm, Birte	(DL) SAT-Based Axiom Pinpointing Revisited (DL) Computing Concept Referring Expressions with Standard OWL Reasoners (DL) Concept Abduction for Description Logics
Glinskih, Ludmila	(CSF) The Complexity of Verifying Boolean Programs as Differentially Private
Gliozzi, Valentina	(KR) A conditional, a fuzzy and a probabilistic interpretation of self-organising maps (Abstract)
Gloaguen, Kevin	(NMR) There and Back Again: Combining Nonmonotonic Logical Reasoning and Deep Learning on an Assistive Robot
Gocht, Stephan	(CP) An Auditable Constraint Programming Solver (POS) Certified Symmetry and Dominance Breaking for Combinatorial Optimisation (SAT) Certified CNF Translations for Pseudo-Boolean Solving
Godbole, Adwait	(CAV) UCLID5: Multi-Modal Formal Modeling, Verification, and Synthesis
Godo, Lluis	(KR) Compound conditionals as random quantities and Boolean algebras
Goel, Nikhil	(ICLP) Knowledge Authoring with Factual English
Goertzel, Zarathustra	(ITP) The Isabelle ENIGMA
Goharshady, Amir Kafshdar	(CAV) Sound and Complete Certificates for Quantitative Termination Analysis of Probabilistic Programs
Golia, Priyanka	(CP) On Quantitative Testing of Samplers (CP) Boolean Functional Synthesis and its Applications (QBF) A Data-Driven Approach for Boolean Functional Synthesis (CAV) A Scalable Shannon Entropy Estimator (MC) Designing Samplers is Easy: The Boon of Testers
Golumbic, Martin Charles	(VardiFest) On the Effectiveness of Logic in Algorithmic Graph Theory
Gombárová, Samantha	(FOMEO) First-Order Logic Workbook
Gomez, Rocio	(ICLP) What do you really want to do? Towards a Theory of Intentions for Human-Robot Collaboration
Gommerstadt, Hannah	(LFMTP) Logics for Robotics
Goncharov, Sergey	(FSCD) Stateful Structural Operational Semantics
Gonczarowski, Yannai A.	(LogTeach) Position Paper: Mathematical Logic through Python
Gondron, Sébastien	(CSF) Privacy as Reachability
Gonnord, Laure	(IWC) On Confluence of Parallel-Innermost Term Rewriting
Gonçalves, Ricardo	(ICLP) On Syntactic Forgetting under Uniform Equivalence (ICLP) Tractable Reasoning using Logic Programs with Intensional Concepts (KR) Looking Inside the Black-Box: Logic-based Explanations for Neural Networks (XLoKR) Modular Provenance in Multi-Context Systems
Gopinath, Divya	(FoMLAS) VPN: Verification of Poisoning in Neural Networks
Gordillo, Pablo	(IJCAR) Using Automated Reasoning Techniques for Enhancing the Efficiency and Security of (Ethereum) Smart Contracts
Gottlob, Georg	(ICLP) MV-Datalog+/-: Effective Rule-based Reasoning with Uncertain Observations (Best Paper Award) (KR) Rule Learning over Knowledge Graphs with Genetic Logic Programming (VardiFest) Data Complexity and Expressive Power of Ontological Reasoning Formalisms
Goubault, Eric	(CAV) RINO: Robust INner and Outer Approximated Reachability of Neural Networks Controlled Systems
Grabmayer, Clemens	(LICS) Milner's Proof System for Regular Expressions Modulo Bisimilarity is Complete
Graham-Lengrand, Stéphane	(SMT) CDSAT for nondisjoint theories with shared predicates: arrays with abstract length
Graillat, Stef	(NSV) Neural Network Precision Tuning Using Stochastic Arithmetic
Gratzer, Daniel	(FSCD) A stratified approach to Lob induction (LICS) Normalization for Multimodal Type Theory
Greenman, Ben	(VardiFest) Little Tricky Logic: Misconceptions in the Understanding of LTL
Grieskamp, Wolfgang	(IJCAR) Reasoning About Vectors using an SMT Theory of Sequences
Griggio, Alberto	(SMT) The VMT-LIB Language and Tools
Gros, Timo P.	(CAV) MoGym: Using Formal Models for Training and Verifying Decision-making Agents
Grosof, Isaac	(POS) Towards the shortest DRAT proof of the Pigeonhole Principle
Gross, Jason	(ITP) Accelerating Verified-Compiler Development with a Verified Rewriting Engine (ITP) Automatic Test-Case Reduction in Proof Assistants: A Case Study in Coq (Coq) Discussion with Coq Core Development Team (Coq) 10 Years of Superlinear Slowness in Coq
Grädel, Erich	(LICS) Zero-One Laws and Almost Sure Valuations of First-Order Logic in Semiring Semantics
Gu, Zhenzhen	(DL) Ontology-based Data Federation (Extended Abstract)
Gu, Zhenzhen	(DL) Extraction of Object-Centric Event Logs through Virtual Knowledge Graphs
Guan, Ji	(CAV) Verifying Fairness in Quantum Machine Learning
Guerrieri, Giulio	(TLLA-LINEARITY) The Call-by-Value Lambda-Calculus from a Linear Logic Perspective (FSCD) Strategies for Asymptotic Normalization
Guha, Shibashis	(CAV) PAC Statistical Model Checking of Mean Payoff in Discrete- and Continuous-Time MDP (VardiFest) Strategy synthesis for Global Window PCTL
Gunawan, Alvaro	(KR) A Graph Neural Network Reasoner for Game Description Language (KR) Investigating Novel Representations and Deep Reinforcement Learning for General Game Playing
Guns, Tias	(CP) Learning Constraint Programming Models from Data using Generate-and-Aggregate (CP) Learning MAX-SAT Models from Examples using Genetic Algorithms and Knowledge Compilation (XLoKR) Stepwise Explanations of Unsatisfiable Constraint Programs (Extended abstract) (ModRef) Efficiently Explaining CSPs with Unsatisfiable Subset Optimization (extended abstract)
Guo, Liye	(WST) A transitive HORPO for curried systems
Gupta, Aarti	(FLoC) SMT-based Verification of Distributed Network Control Planes
Gupta, Gopal	(ICLP) Building Information Modeling using Constraint Logic Programming (ICLP) FOLD-RM: A Scalable and Efficient Inductive Learning Algorithm for Multi-Category Classification of Mixed Data (ICLP) Towards Dynamic Consistency Checking in Goal-directed Predicate Answer Set Programming (ICLP) Graph-based Interpretation of Normal Logic Programs (ICLP) Modeling and Reasoning in Event Calculus using Goal-Directed Constraint Answer Set Programming (Extended Abstract) (GDE) LTL Model Checking using Coinductive Answer Set programming (GDE) Symbolic Reinforcement Learning Framework with Incremental Learning of Rule-based Policy (GDE) Tutorial: Automating Commonsense Reasoning
Gutierrez-Basulto, Victor	(KR) LACE: A Logical Approach to Collective Entity Resolution (KR) Finite Entailment of UCRPQs over ALC Ontologies
Gutin, Gregory	(PCCR) Parameterized algorithmics in access control: linking theory and practice
Gutiérrez, Raúl	(IWC) Proving Confluence with CONFident
Gutowski, Albert	(KR) Finite Entailment of UCRPQs over ALC Ontologies (KR) Decidability Limits of Finite Ontology-Mediated Query Entailment
Gutsfeld, Jens Oliver	(LICS) Temporal Team Semantics Revisited
Guéneau, Armaël	(CSF) Proving full-system security properties under multiple attacker models on capability machines
Gómez Álvarez, Lucia	(NMR) Modelling Multiple Perspectives by Standpoint-Enhanced Description Logics (KR) Automating Reasoning with Standpoint Logic via Nested Sequents (DL) Modelling Multiple Perspectives by Standpoint-Enhanced DLs
Gómez-Londoño, Alejandro	(ITP) Kalas: A Verified, End-to-End Compiler for a Choreographic Language
H
H. Pham, Long	(CAV) Verifying Neural Networks Against Backdoor Attacks
Haas, Thomas	(VeriProp) Widest Paths and Global Propagation in Bounded Value Iteration for Stochastic Games
Haase, Christoph	(Mentoring Workshop) Navigating through the academic jungle (LICS) Geometric decision procedures and the VC dimension of linear arithmetic theories
Habermehl, Peter	(CAV) Data-driven Numerical Invariant Synthesis with Automatic Generation of Attributes
Habet, Djamal	(CP) From Crossing-Free Resolution to Max-SAT Resolution
Hader, Thomas	(SMT) An SMT Approach for Solving Polynomials over Finite Fields
Haeusler, Edward	(DL) A Labelled Natural Deduction System for an Intuitionistic Description Logic with Nominals
Haga, Ryota	(IWC) A Critical Pair Criterion for Level-Commutation of Conditional Term Rewriting Systems
Hagens, Kasper	(WPTE) Extending a Lemma Generation Approach for Rewriting Induction on Logically Constrained Term Rewriting Systems (PERR) Extending a Lemma Generation Approach for Rewriting Induction on Logically Constrained Term Rewriting Systems
Hahn, Christopher	(SYNT) LTL Synthesis with Transformer Neural Networks (CAV) Explaining Hyperproperty Violations
Hahn, Susana	(ASPOCP) plingo: A system for probabilistic reasoning in clingo based on lpmln
Hahn, Ulrike	(KR) Probabilities, Reasoning, and Argumentation
Haifani, Fajar	(DL) Connection-minimal Abduction in EL via translation to FOL (Extended Abstract) (IJCAR) Connection-minimal Abduction in EL via translation to FOL (IJCAR) Semantic Relevance
Haifani, Fajar	(NMR) Connection-Minimal Abduction in EL via Translation to FOL
Haines, Thomas	(CSF) Machine-Checked Proofs of Privacy Against Malicious Boards for Selene & Co
Hajdu, Marton	(PAAR) The Vampire Approach to Induction
Haldimann, Jonas	(KR) Inference with System W Satisfies Syntax Splitting (KR) Relevance in Reasoning with and Revision of Conditional Beliefs
Hall, Brendan	(GDE) Unmanned Aerial Vehicle compliance checking using Goal-Directed Answer Set Programming
Halpern, Joe	(VardiFest) That's All I know: On the Effectiveness of Logic in Game Theory
Hamana, Makoto	(WST) The System SOL version 2022 (Tool Description) (IWC) Checking Confluence of Rewrite Rules in Haskell
Hamilton, Dennis	(LogTeach) Logic for CS Undergraduates: A Sketch
Hanna, Ziyad	(FLoC) Harnessing the Power of Formal Verification for the $Trillion Chip Design Industry
Hansen, Rene Rydhof	(GuttmanFest) Benign Interaction of Security Domains
Hansen, Zach	(ICLP) A Preliminary Data-driven Analysis of Common Errors Encountered by Novice Answer Set Programmers
Hanus, Michael	(ICLP) From Logic to Functional Logic Programs
Hao, Jifeng	(ITP) Compositional Verification of Interacting Systems using Event Monads
Harel, David	(VardiFest) Computability and Complexity over Finite Unordered Structures; e.g., Graphs (1979-1982)
Haret, Adrian	(KR) An Axiomatic Approach to Revising Preferences (Extended Abstract)
Hariharan, Gokul	(NSV) MLTL Multi-Type: A Logic for Reasoning about Traces of Different Types
Hark, Marcel	(WST) Improved Automatic Complexity Analysis of Integer Programs (WST) Deciding Termination of Uniform Loops with Polynomial Parameterized Complexity (WST) Automatic Complexity Analysis of (Probabilistic) Integer Programs via KoAT (VeriProp) Inferring Expected Runtimes and Sizes
Harper, Robert	(FSCD) Sheaf semantics of termination-insensitive noninterference (LFMTP) A (Logical) Framework for Collaboration
Hartisch, Michael	(QBF) Advances in Quantified Integer Programming
Hasuo, Ichiro	(CAV) The Lattice-Theoretic Essence of Property Directed Reachability Analysis (VeriProp) Widest Paths and Global Propagation in Bounded Value Iteration for Stochastic Games (VardiFest) Bisimulation Games Played in Fibered Categories (FoMLAS) Goal-Aware RSS for Complex Scenarios via Program Logic
Havlena, Vojtěch	(CAV) Complementing Büchi Automata with Ranker
Hayashi, Hisashi	(NMR) Towards Legally and Ethically Correct Online HTN Planning for Data Transfer
Hebrard, Emmanuel	(CP) Complexity of Minimum-Size Arc-Inconsistency Explanations
Hecher, Markus	(SAT) Proofs for Propositional Model Counting (ICLP) ApproxASP – A Scalable Approximate Answer Set Counter (ICLP) Treewidth-aware Reductions of Normal ASP to SAT– Is Normal ASP Harder than SAT after All? (QBF) Lower Bounds for QBFs of Bounded Treewidth (PCCR) Tractable Abstract Argumentation via Backdoor-Treewidth
Hedin, Daniel	(GuttmanFest) Securing Node-RED Applications
Heeren, Bastiaan	(FOMEO) LogInd, a tool for supporting students in mastering structural induction
Hegyi, Péter	(WPTE) Refactoring Steps for P4 (work in progress)
Heidemann, Lukas	(LICS) Zigzag normalisation for associative n-categories
Heijltjes, Willem	(FSCD) Normalization without syntax (IWC) Confluence by Higher-Order Multi--One Critical pairs with an application to the Functional Machine Calculus
Heisinger, Max	(PDAR) Dealing With Uncertainty Between Peers and Having the Best of Times With Distributed Systems (PAAR) QuAPI: Adding Assumptions to Non-Assuming SAT & QBF Solvers
Helal, Hayyan	(LICS) Zero-One Laws and Almost Sure Valuations of First-Order Logic in Semiring Semantics
Hensel, Jera	(WST) AProVE 2022
Henzinger, Thomas	(VardiFest) Between Determinism and Nondeterminism
Herbreteau, Frédéric	(LICS) Abstractions for the local-time semantics of timed automata: a foundation for partial-order methods
Hermann, Miki	(LMML) MCP: Capturing Big Data by Satisfiability
Hermanns, Holger	(CAV) MoGym: Using Formal Models for Training and Verifying Decision-making Agents
Hermenegildo, Manuel V.	(GDE) An s(CASP) In-Browser Playground based on Ciao Prolog
Hermes, Marc	(FSCD) An Analysis of Tennenbaum's Theorem in Constructive Type Theory (Coq) A Coq Library for Mechanised First-Order Logic
Hernández-Cerezo, Alejandro	(IJCAR) Using Automated Reasoning Techniques for Enhancing the Efficiency and Security of (Ethereum) Smart Contracts
Herranz, Ángel	(FMBC) Automatic generation of attacker contracts in Solidity
Herud, Konstantin	(ASPOCP) Conflict Handling in Product Configuration using Answer Set Programming
Herwig, Maurice	(FOMEO) Towards Graphical Feedback in the DiMo Learning Tool
Heskes, Tom	(IJCAR) Guiding an Automated Theorem Prover with Neural Rewriting
Hesse, Matthis	(NMR) Abductive Reasoning with Sequent-Based Argumentation (Extended Abstract)
Heuer, Tobias	(POS) SATViz: Real-Time Visualization of Clausal Proofs
Heule, Marijn	(CP) From Cliques to Colorings and Back Again (POS) Towards the shortest DRAT proof of the Pigeonhole Principle (SAT) The packing chromatic number of the infinite square grid is at least 14 (SAT) Migrating Solver State (SAT) Relating existing powerful proof systems for QBF (SAT) 25 years of SAT: Modern SAT Techniques / Remembering Hans van Maaren (QBF) Moving Definition Variables in Quantified Boolean Formulas (Extended Abstract) (PC) Exponential separations using guarded extension variables (IJCAR) Preprocessing of Propagation Redundant Clauses (VardiFest) Understandable Proofs of Unsatisfiability
Heyninck, Jesse	(ICLP) Nested Justification Systems (ICLP) Tractable Reasoning using Logic Programs with Intensional Concepts (NMR) Conditional Syntax Splitting, Lexicographic Entailment and the Drowning Effect
Hicks, Michael	(CSF) A Formal Model of Checked C
Hidouri, Amel	(CP) On the Enumeration of Frequent High Utility Itemsets: A symbolic AI Approach
Hietala, Kesha	(Coq) QuantumLib: A Library for Quantum Computing in Coq
Higuera, Nelson	(ICLP) A Neuro-Symbolic ASP Pipeline for Visual Question Answering (KR) ALASPO: An Adaptive Large-Neighbourhood ASP Optimiser
Higuera Ruiz, Nelson	(ICLP) Large-Neighbourhood Search for ASP Optimisation
Hilaire, Thibault	(NSV) Neural Network Precision Tuning Using Stochastic Arithmetic
Hirokawa, Nao	(FSCD) Compositional Confluence Criteria (WST) Hydra Battles and AC Termination (IWC) Seven Confluence Criteria for Solving COPS #20
Hirsch, Andrew K.	(FCS) Compositional Higher-order Declassification Using Logical Relations
Hirsch, Edward	(PC) Strong proof systems based on algebraic circuits (LogTeach) Whom to teach logic?
Hlávková, Zuzana	(DL) An API for DL Abduction Solvers (XLoKR) An API for DL Abduction Solvers
Hoenicke, Jochen	(SMT) A simple proof format for SMT
Hofbauer, Dieter	(WST) Approximating Relative Match-Bounds (WST) MultumNonMulta at termCOMP 2022
Hoffmann, Joerg	(CAV) MoGym: Using Formal Models for Training and Verifying Decision-making Agents (DL) Expressivity of Planning with Horn Description Logic Ontologies (Extended Abstract) (XLoKR) Explaining Soft-Goal Conflicts through Constraint Relaxations
Hoffmann, Ruth	(CP) Understanding how people approach constraint modelling and solving (ModRef) Constraint modelling and solving: Learning from observing people
Hofman, Piotr	(LICS) Solvability of orbit-finite systems of linear equations
Hofmann, Jana	(LICS) Deciding Hyperproperties Combined with Functional Specifications
Hofmann, Till	(XLoKR) Using Abstraction for Interpretable Robot Programs in Stochastic Domains
Holden, Sean	(IJCAR) Bayesian Ranking for Strategy Scheduling in Automated Theorem Provers
Hollenberg, Tommy	(CSF) A Complete Characterization of Security for Linicrypt Block Cipher Modes
Holler, Sebastian	(FCS) A Preview to HoRStify: Sound Security Analysis of Smart Contracts
Holub, Stepan	(Isabelle) Auxiliary tools for Combinatorics on Words (Isabelle) Transfer and reversal of lists (IJCAR) Binary codes that do not preserve primitivity
Holzenkamp, Tim	(POS) SATViz: Real-Time Visualization of Clausal Proofs
Homola, Martin	(NMR) Hybrid MHS-MXP ABox Abduction Solver: First Emprical Results (FOMEO) SIVA: Simulation and visualization of the DL tableau algorithm (DL) Hybrid MHS-MXP ABox Abduction Solver: First Emprical Results (DL) An API for DL Abduction Solvers (DL) DL Opening Remarks (DL) Business Meeting (XLoKR) An API for DL Abduction Solvers
Hong, Ye	(ITP) Compositional Verification of Interacting Systems using Event Monads
Honsell, Furio	(FSCD) On Quantitative Algebraic Higher-Order Theories
Hoos, Holger	(MC) Stochastic Constraint Optimisation with Applications in Network Analysis
Horak, Tom	(CAV) Explaining Hyperproperty Violations
Horne, Ross	(FSCD) A Graphical Proof Theory of Logical Time (CSF) Is Eve nearby? Analysing protocols under the distant-attacker assumption (CSF) Unlinkability of an Improved Key Agreement Protocol for EMV 2nd Gen Payments (FCS) Towards Unlinkable Smartcard-based Payments: an extended abstract
Horpácsi, Dániel	(WPTE) A Machine-Checked Formalisation of Erlang Modules
Hosseyni, Pedram	(GuttmanFest) A Tutorial-Style Introduction to DY*
Hostert, Johannes	(ITP) Undecidability of Dyadic First-Order Logic in Coq (Coq) A Coq Library for Mechanised First-Order Logic
Houmansadr, Amir	(FCS) Robust Indistinguishability
Hozzová, Petra	(SYNT) Towards Synthesis in Superposition (PAAR) Reuse of Introduced Symbols in Automatic Theorem Provers
Hritcu, Catalin	(CSF) SecurePtrs: Proving Secure Compilation Using Data-Flow Back-Translation and Turn-Taking Simulation
Hsu, Justin	(CAV) Data-Driven Invariant Learning for Probabilistic Programs
Hsu, Tzu-Han	(CSF) Mapping Synthesis for Hyperproperties
Huang, Xiaowei	(KR) A Graph Neural Network Reasoner for Game Description Language (FoMLAS) Formal Specification for Learning-Enabled Autonomous Systems (Extended Abstract)
Huch, Fabian	(Isabelle) A Linter for Isabelle: Implementation and Evaluation (PAAR) The Isabelle Community Benchmark
Hughes, Dominic	(FSCD) Normalization without syntax
Hundeshagen, Norbert	(FOMEO) Towards Graphical Feedback in the DiMo Learning Tool
Hunter, Aaron	(NMR) Trust Graphs for Belief Revision: Framework and Implementation
Hunter, Anthony	(KR) From Non-monotonic Reasoning to Argumentation and Commonsense (Great Moments in KR Talk)
Hustadt, Ullrich	(IJCAR) Local Reductions for the Modal Cube
Hym, Samuel	(CAV) End-to-end Mechanised Proof of an eBPF Virtual Machine for Microcontrollers
Hyvärinen, Antti	(CAV) SolCMC: Solidity Compiler’s Model Checker (SMT) Business Meeting
I
Iatrou, Evan	(ASPOCP) A normative model of explanation for binary classification legal AI and its implementation on causal explanations of Answer Set Programming
Ibanez-Garcia, Yazmin	(KR) Finite Entailment of UCRPQs over ALC Ontologies
Idziak, Paweł	(LICS) Complexity of Modular Circuits
Ignatiev, Alexey	(CP) Formal Explainable AI
Ihalainen, Hannes	(IJCAR) Clause Redundancy and Preprocessing in Maximum Satisfiability
Illich, Moritz	(DL) Computing Concept Referring Expressions with Standard OWL Reasoners
Imai, Keigo	(WST) The System SOL version 2022 (Tool Description)
Incudini, Massimiliano	(GuttmanFest) Quantum Machine Learning and Fraud Detection
Indrzejczak, Andrzej	(IJCAR) Le\'sniewski's Ontology -- Proof-Theoretic Characterization (iPRA) When iota Meets lambda
Inoue, Katsumi	(POS) DPS: A Framework for Deterministic Parallel SAT Solvers
Iosif, Radu	(IJCAR) Decision Problems in a Logic for Reasoning about Reconfigurable Distributed Systems (ASL) On the Expressiveness of a Logic of Separated Relations
Irfan, Ahmed	(SMT) Bit-Precise Reasoning via Int-Blasting
Irwin, Benjamin	(KR) Forecasting Argumentation Frameworks
Isabel, Miguel	(CAV) Distilling Constraints in Zero-Knowledge Protocols
Isac, Omri	(FoMLAS) Neural Network Verification with Proof Production
Iser, Markus	(POS) Calculating Sufficient Reasons for Random Forest Classifiers (POS) SATViz: Real-Time Visualization of Clausal Proofs (POS) Dinosat: A SAT Solver with Native DNF Support (SAT) A Comprehensive Study of k-Portfolios of Recent SAT Solvers (PDAR) Beyond Portfolios of Stable Solvers
Itsykson, Dmitry	(SAT) Tight Bounds for Tseitin Formulas (PC) Proof complexity of natural formulas via communication arguments
Itzhaky, Shachar	(Coq) jsCoq: Literate Proof Documents Dressed for the Web
Izmirlioglu, Yusuf	(KR) Reasoning about Cardinal Directions between 3-Dimensional Extended Objects using Answer Set Programming
J
Jabbour, Said	(CP) On the Enumeration of Frequent High Utility Itemsets: A symbolic AI Approach
Jabs, Christoph	(SAT) MaxSAT-Based Bi-Objective Boolean Optimization
Jacobs, Bart	(LICS) Partitions and Ewens Distributions in element-free Probability Theory
Jacobsen, Frederik Krogsdal	(Isabelle) Lessons of Teaching Formal Methods with Isabelle (ITP) Verifying a Sequent Calculus Prover for First-Order Logic with Functions in Isabelle/HOL (LogTeach) Teaching Logic for Computer Science Students: Proof Assistants and Related Tools (FOMEO) Formal Methods Online: Sequent Calculus Verifier (SeCaV) (ThEdu) On Exams with the Isabelle Proof Assistant
Jakobsson, Arvid	(FMBC) FAT CAT: Formal Acceptance Testing of Contracts for Administering Tokens
Jakubův, Jan	(ITP) The Isabelle ENIGMA
Jamroga, Wojtek	(GuttmanFest) A Declaration of Software Independence
Jana, Suman	(FoMLAS) Efficient Neural Network Verification using Branch and Bound
Janhunen, Tomi	(ASPOCP) plingo: A system for probabilistic reasoning in clingo based on lpmln (ICLP) On Syntactic Forgetting under Uniform Equivalence (ICLP) Implementing Stable-Unstable Semantics with ASPTOOLS and Clingo
Janota, Mikolas	(SAT) Towards Learning Quantifier Instantiation in SMT (SAT) SAT-based Leximax Optimisation Algorithms (IJCAR) Guiding an Automated Theorem Prover with Neural Rewriting (SMT) Challenges and Solutions for Higher-Order SMT Proofs
Jansen, Nils	(CAV) Sampling-Based Verification of CTMCs with Uncertain Rates (VeriProp) Safe Sampling-Based Planning for Stochastic Systems with Uncertain Dynamics
Jeandel, Emmanuel	(FSCD) Addition and differentiation of ZX-diagrams
Jeannin, Jean-Baptiste	(ITP) Dandelion: Certified Approximations of Elementary Functions
Jeuring, Johan	(FOMEO) LogInd, a tool for supporting students in mastering structural induction
Jhoo, Ho Young	(CAV) SMT-based Translation Validation for Machine Learning Compiler
Ji, Yucheng	(CAV) Affine Loop Invariant Generation via Matrix Algebra
Jiang, Jie-Hong Roland	(SAT) Quantifier Elimination in Stochastic Boolean Satisfiability
Jiang, Junqi	(XLoKR) Should counterfactual explanations always be data instances?
Jin, Peng	(CAV) Trainify: A CEGAR-Driven Training and Verification Framework for Verifiable Deep Reinforcement Learning
Johnsen, Einar Broch	(CSF) DPL: A Language for GDPR Enforcement
Johnson, Dale	(GuttmanFest) Formal Methods and Mathematical Intuition
Joinet, Jean-Baptiste	(TLLA-LINEARITY) Dissymetrical Linear Logic
Jones, Michael Peyton	(FMBC) Designing EUTxO smart contracts as communicating state machines: the case of simulating accounts
Jones, Phillip H.	(NSV) MLTL Multi-Type: A Logic for Reasoning about Traces of Different Types
Joosten, Joost J.	(DECFOML) The Quantified Reflection Calculus as a Modal Logic
Jothimurugan, Kishor	(SYNT) A Framework for Transforming Specifications in Reinforcement Learning (CAV) Specification-Guided Learning of Nash Equilibria with High Social Welfare
Juba, Brendan	(CAV) A Scalable Shannon Entropy Estimator
Jukiewicz, Marcin	(IJCAR) Synthetic tableaux: minimal tableau search heuristics
Juma, Nahid	(CSF) Locked Circuit Indistinguishability: A Notion of Security for Logic Locking
Jung, Jean Christoph	(SAT) QBF Programming with the Modeling Language Bule (KR) Conservative Extensions for Existential Rules (DL) Actively Learning ELIQs in the Presence of DL-Lite-Horn Ontologies (DL) More on Interpolants and Explicit Definitions for Description Logics with Nominals and/or Role Inclusions
Jung, Jean Christoph	(DL) DL Opening Remarks
Jung, Jean Christoph	(DL) Business Meeting
Jung, Kangsoo	(GuttmanFest) Establishing the Price of Privacy in Federated Data Trading
Jung, Ralf	(ASL) Functional correctness specifications for concurrent data structures: Logical Atomicity in Iris
Junges, Sebastian	(CAV) Abstraction-Refinement for Hierarchical Probabilistic Models (CAV) Sampling-Based Verification of CTMCs with Uncertain Rates
Junosza-Szaniawski, Konstanty	(POS) Towards an Efficient CNF Encoding of Block Ciphers
Jurík, Norbert	(FOMEO) First-Order Logic Workbook
Järv, Priit	(GDE) First order logic and commonsense reasoning: a path less travelled (IJCAR) GK: Implementing Full First Order Default Logic for Commonsense Reasoning (System Description)
Järvisalo, Matti	(SAT) Incremental Maximum Satisfiability (SAT) Improvements to the Implicit Hitting Set Approach to Pseudo-Boolean Optimization (SAT) MaxSAT-Based Bi-Objective Boolean Optimization (SAT) Awards and Competition - II (with Live Broadcast) (KR) Computing Stable Argumentative Conclusions under the Weakest-Link Principle in the ASPIC+ Framework (IJCAR) Clause Redundancy and Preprocessing in Maximum Satisfiability
Jézéquel, Fabienne	(NSV) Neural Network Precision Tuning Using Stochastic Arithmetic
K
Kabaha, Anan	(FCS) VeNuS: Neural Network Robustness Specifications via Verifier-guided Optimization
Kabir, Mohimenul	(ICLP) ApproxASP – A Scalable Approximate Answer Set Counter
Kagaya, Yuki	(IWC) A Critical Pair Criterion for Level-Commutation of Conditional Term Rewriting Systems
Kahle, Reinhard	(LogTeach) Logic for Students of Modern Artificial Intelligence
Kaiser, Benjamin	(CSF) Adversary Safety by Construction in a Language of Cryptographic Protocols
Kalayci, Tahir Emre	(DL) Extraction of Object-Centric Event Logs through Virtual Knowledge Graphs
Kaliszyk, Cezary	(ITP) The Isabelle ENIGMA (ITP) Formalizing the set of primes as an alternative to the DPRM theorem (short paper) (FMBC) Proofgold: Blockchain for Formal Methods (PAAR) Lazy Paramodulation in Practice (IJCAR) Lash 1.0 (System Description) (SMT) Challenges and Solutions for Higher-Order SMT Proofs
Kalita, Pankaj Kumar	(SYNT) Interactive Debugging of Concurrent Programs under Relaxed Memory Models
Kalke, Martine	(CSF) Adversary Safety by Construction in a Language of Cryptographic Protocols
Kamhi, Gila	(VardiFest) Moshe Vardi and Intel Corporation: Long and Fruitful Collaboration
Kaminski, Roland	(ASPOCP) plingo: A system for probabilistic reasoning in clingo based on lpmln
Kanabar, Hrutvik	(ITP) Taming an Authoritative Armv8 ISA Specification: L3 Validation and CakeML Compiler Verification
Kanckos, Annika	(ARQNL) Intuitionistic derivability in Anderson's variant of the ontological argument
Kang, Eunsuk	(CSF) Mapping Synthesis for Hyperproperties
Kanovich, Max	(LFMTP) Associativity or Non-Associativity, Local or Global! (IJCAR) Non-associative, non-commutative multi-modal linear logic (GuttmanFest) On the Complexity of Verification of Time-Sensitive Distributed Systems
Kappé, Tobias	(VeriProp) Probabilistic Guarded Kleene Algebra with Tests
Karahalios, Anthony	(CP) From Cliques to Colorings and Back Again
Karami, Farzane	(CSF) DPL: A Language for GDPR Enforcement
Karayel, Emin	(ITP) Formalization of Randomized Approximation Algorithms for Frequency Moments
Karge, Jonas	(KR) The More the Worst-Case-Merrier: A Generalized Condorcet Jury Theorem for Belief Fusion (KR) Doctoral Consortium Application (DL) Uniform and Modular Sequent Systems for Description Logics
Katis, Andreas	(CAV) Capture, Analyze, Diagnose: Realizability Checking of Requirements in FRET
Kato, Takumi	(WPTE) On Transforming Imperative Programs into Logically Constrained Term Rewrite Systems via Injective Functions from Configurations to Terms
Katoen, Joost-Pieter	(SYNT) Inductive and Parameter Synthesis to Find POMDP Controllers (CAV) Does a Program Yield the Right Distribution? Verifying Probabilistic Programs via Generating Functions
Katsaros, Panagiotis	(FoMLAS) Formal Specification for Learning-Enabled Autonomous Systems (Extended Abstract)
Katsirelos, George	(CP) Structured Set Variable Domains in Bayesian Network Structure Learning (CP) Parallel Hybrid Best-First Search
Katsumata, Shin-ya	(CAV) The Lattice-Theoretic Essence of Property Directed Reachability Analysis
Katz, Guy	(CAV) Neural Network Robustness as a Verification Property: A Principled Case Study (FoMLAS) Neural Network Verification with Proof Production (FoMLAS) Minimal Multi-Layer Modifications of Deep Neural Networks (FoMLAS) An Abstraction-Refinement Approach to Verifying Convolutional Neural Networks (FoMLAS) Verification-Aided Deep Ensemble Selection (FoMLAS) RoMA: a Method for Neural Network Robustness Measurement and Assessment
Kaufmann, Daniela	(POS) Adding Dual Variables to Algebraic Reasoning for Gate-Level Multiplier Verification
Kavraki, Lydia	(VardiFest) On the Effectiveness of Logic in Robotics
Kavvos, Alex	(ITP) Deeper Shallow Embeddings (LICS) Syllepsis in Homotopy Type Theory
Kawałek, Piotr	(LICS) Complexity of Modular Circuits
Kazakov, Yevgeny	(DL) SAT-Based Axiom Pinpointing Revisited (DL) Concept Abduction for Description Logics
Keisler, H. Jerome	(iPRA) Application of Interpolation in Networks
Keisler, Jeffrey M.	(iPRA) Application of Interpolation in Networks
Keller, David	(WST) AProVE 2022
Kellison, Ariel	(NSV) Verified Numerical Methods for Ordinary Differential Equations
Kelmendi, Edon	(LICS) Computing the Density of the Positivity Set for Linear Recurrence Sequences
Kempa, Brian	(NSV) MLTL Multi-Type: A Logic for Reasoning about Traces of Different Types
Kerjean, Marie	(TLLA-LINEARITY) Copromotion and Taylor Approximation (Work in Progress)
Kern-Isberner, Gabriele	(NMR) Conditional Syntax Splitting, Lexicographic Entailment and the Drowning Effect (KR) KR 2022 Closing
Kersting, Kristian	(KR) Sum-Product Loop Programming: From Probabilistic Circuits to Loop Programming (KR) Neural-Probabilistic Answer Set Programming
Kesner, Delia	(FSCD) Solvability for Generalized Applications (TERMGRAPH) A Computational Interpretation of Girard’s Intuitionistic Proof-Nets (WiL) Embedding Quantitative Properties of Call-by-Name and Call-by-Value into Call-by-Push-Value
Khalil, Elias	(SMT) Goose: A Meta Solver for Deep Neural Network Verification
Khoja, Alan	(VardiFest) Checking Legal Contracts - On a Not So Usual Application of Mechanized Logic
Kiefer, Sandra	(LICS) Treelike decompositions for transductions of sparse graphs
Kienitz, Daniel	(FoMLAS) Why Robust Natural Language Understanding is a Challenge
Kiesel, Rafael	(ICLP) Efficient Knowledge Compilation Beyond Weighted Model Counting (Best Student Paper Award) (DL) Reasoning on Multi-Relational Contextual Hierarchies via Answer Set Programming with Algebraic Measures
Kiesel, Rafael	(NMR) Reasoning on Multi-Relational Contextual Hierarchies via Answer Set Programming with Algebraic Measures
Kiesl, Benjamin	(SAT) Migrating Solver State
Kifer, Michael	(ICLP) Knowledge Authoring with Factual English
Killen, Spencer	(ICLP) A Fixpoint Characterization of Three-Valued Disjunctive Hybrid MKNF Knowledge Bases
Kimmig, Angelika	(ICLP) Efficient Knowledge Compilation Beyond Weighted Model Counting (Best Student Paper Award)
Kirchweger, Markus	(SAT) A SAT Attack on Rota's Basis Conjecture
Kirst, Dominik	(ITP) Computational Back-and-Forth Arguments in Constructive Type Theory (ITP) Undecidability of Dyadic First-Order Logic in Coq (FSCD) An Analysis of Tennenbaum's Theorem in Constructive Type Theory (Coq) A Coq Library for Mechanised First-Order Logic
Klauck, Michaela	(CAV) MoGym: Using Formal Models for Training and Verifying Decision-making Agents
Klinkenberg, Lutz	(CAV) Does a Program Yield the Right Distribution? Verifying Probabilistic Programs via Generating Functions (VeriProp) Verifying Probabilistic Programs using Generating Functions
Knispel, Andre	(FMBC) Human and machine-readable models of state machines for the Cardano ledger
Knispel, Andre	(FMBC) Determinism of ledger updates
Knorr, Matthias	(ICLP) On Syntactic Forgetting under Uniform Equivalence (ICLP) Tractable Reasoning using Logic Programs with Intensional Concepts (XLoKR) Modular Provenance in Multi-Context Systems
Knuth, Donald	(CP) All Questions Answered
Koch, Mark	(Coq) A Coq Library for Mechanised First-Order Logic
Kochdumper, Niklas	(CAV) Reachability of Koopman Linearized Systems Using Random Fourier Feature Observables and Polynomial Zonotope Refinement
Kohbrok, Konrad	(CSF) Bringing State-Separating Proofs to EasyCrypt - A Security Proof for Cryptobox
Kohl, Christina	(WST) CeTA – A certifier for termCOMP 2022 (IWC) Development Closed Critical Pairs: Towards a Formalized Proof
Kojima, Misaki	(WPTE) On Transforming Imperative Programs into Logically Constrained Term Rewrite Systems via Injective Functions from Configurations to Terms (WPTE) On Reducing Non-Occurrence of Specified Runtime Errors to All-Path Reachability Problems of Constrained Rewriting
Kokke, Wen	(CAV) Neural Network Robustness as a Verification Property: A Principled Case Study (FoMLAS) Vehicle: A High-Level Language for Embedding Logical Specifications in Neural Networks (FoMLAS) Why Robust Natural Language Understanding is a Challenge
Kolaitis, Phokion	(VardiFest) Moshe Y. Vardi's First Love
Kolb, Samuel	(CP) Learning Constraint Programming Models from Data using Generate-and-Aggregate (CP) Learning MAX-SAT Models from Examples using Genetic Algorithms and Knowledge Compilation
Komendantskaya, Ekaterina	(CAV) Neural Network Robustness as a Verification Property: A Principled Case Study (FoMLAS) Neural Networks in Imandra: Matrix Representation as a Verification Choice (FoMLAS) Vehicle: A High-Level Language for Embedding Logical Specifications in Neural Networks (FoMLAS) Differentiable Logics for Neural Network Verification (FoMLAS) Why Robust Natural Language Understanding is a Challenge
Komlóssy, Matej	(FOMEO) First-Order Logic Workbook
Konev, Boris	(KR) Unique Characterisability and Learnability of Temporal Instance Queries (KR) Interpolants and Explicit Definitions in Extensions of the Description Logic EL (DL) Reverse Engineering of Temporal Queries with and without LTL Ontologies: First Steps
Konieczny, Sebastien	(ICLP) On Paraconsistent Belief Revision: the Case of Priest’s Logic of Paradox (KR) On Paraconsistent Belief Revision in LP (Extended Abstract) (KR) Region-Based Merging of Open-Domain Terminological Knowledge (KR) On the Representation of Darwiche and Pearl’s Epistemic States for Iterated Belief Revision
Koopmann, Patrick	(DL) Optimal ABox Repair w.r.t. Static EL TBoxes: from Quantified ABoxes back to ABoxes (Extended Abstract) (DL) Connection-minimal Abduction in EL via translation to FOL (Extended Abstract) (DL) Efficient TBox Reasoning with Value Restrictions using the FL0wer Reasoner (Extended Abstract) (DL) Finding Good Proofs for Answers to Conjunctive Queries Mediated by Lightweight Ontologies (DL) On the Eve of True Explainability for OWL Ontologies: Description Logic Proofs with Evee and Evonne (DL) An API for DL Abduction Solvers (XLoKR) Finding Good Proofs for Answers to Conjunctive Queries Mediated by Lightweight Ontologies (Extended Abstract) (XLoKR) An API for DL Abduction Solvers (XLoKR) Explaining Description Logic Entailments in Practice with Evee and Evonne (IJCAR) Evonne: Interactive Proof Visualization for Description Logics (System Description) (IJCAR) Connection-minimal Abduction in EL via translation to FOL
Koopmann, Patrick	(NMR) Connection-Minimal Abduction in EL via Translation to FOL
Kop, Cynthia	(FSCD) Cutting a Proof into Bite-Sized Chunks: Incrementally Proving Termination in Higher-Order Term Rewriting (WPTE) Extending a Lemma Generation Approach for Rewriting Induction on Logically Constrained Term Rewriting Systems (WST) Tuple Interpretations and Applications to Higher-Order Runtime Complexity (WST) A transitive HORPO for curried systems (WST) Things WANDA cannot do (PERR) Extending a Lemma Generation Approach for Rewriting Induction on Logically Constrained Term Rewriting Systems
Kori, Mayuko	(CAV) The Lattice-Theoretic Essence of Property Directed Reachability Analysis
Korkut, Joomy	(ThEdu) A Proof Tree Builder for Sequent Calculus and Hoare Logic
Korovin, Konstantin	(IJCAR) Ground joinability and connectedness in the superposition calculus
Kotsireas, Ilias	(KR) Solving Lam's Problem via SAT and Isomorph-Free Exhaustive Generation
Koutavas, Vasileios	(PERR) From Bounded Checking to Verification of Equivalence via Symbolic Up-to Techniques (Extended Abstract)
Koutsos, Adrien	(CSF) Cracking the Stateful Nut -- Computational Proofs of Stateful Security Protocols using the Squirrel Proof Assistant
Kovtunova, Alisa	(DL) Expressivity of Planning with Horn Description Logic Ontologies (Extended Abstract) (DL) Finding Good Proofs for Answers to Conjunctive Queries Mediated by Lightweight Ontologies (XLoKR) Finding Good Proofs for Answers to Conjunctive Queries Mediated by Lightweight Ontologies (Extended Abstract)
Kovács, Laura	(SYNT) Towards Synthesis in Superposition (FMBC) Automating Security Analysis of Off-Chain Protocols (PAAR) The Vampire Approach to Induction (SMT) User-Propagators for Custom Theories in SMT Solving (SMT) An SMT Approach for Solving Polynomials over Finite Fields
Kowalski, Robert	(GDE) Integration of Logical English and s(CASP)
Kozhemiachenko, Daniil	(IJCAR) Paraconsistent Gödel modal logic
Kragl, Bernhard	(FRIDA) Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3
Kremer, Gereon	(SC^2) Cylindrical Algebraic Coverings for Quantifiers (IJCAR) Cooperating Techniques for Solving nonlinear arithmetic in the cvc5 SMT solver (System Description) (IJCAR) Flexible Proof Production in an Industrial-Strength SMT Solver (SMT) cvc5: A Versatile and Industrial-Strength SMT Solver
Kremer, Steve	(CSF) Symbolic protocol verification with dice: process equivalences in the presence of probabilities
Kreutzer, Stephan	(LICS) Model Checking on Interpretations of Classes of Bounded Local Cliquewidth
Kriegel, Francesco	(KR) Pushing Optimal ABox Repair from EL Towards More Expressive Horn-DLs (DL) Optimal ABox Repair w.r.t. Static EL TBoxes: from Quantified ABoxes back to ABoxes (Extended Abstract)
Krijnen, Jacco	(FMBC) Designing EUTxO smart contracts as communicating state machines: the case of simulating accounts
Krishnamurthi, Shriram	(VardiFest) Little Tricky Logic: Misconceptions in the Understanding of LTL
Krishnamurthi, Shriram	(GuttmanFest) Prototyping Formal Methods Tools: a Protocol Analysis Case Study
Krzaczkowski, Jacek	(LICS) Complexity of Modular Circuits
Kräuter, Tim	(TERMGRAPH) Formalization and analysis of BPMN using graph transformation systems
Krötzsch, Markus	(KR) Chasing streams with existential rules (LICS) Deciding Hyperproperties Combined with Functional Specifications (DL) Expressivity of Planning with Horn Description Logic Ontologies (Extended Abstract)
Kudasov, Nikolai	(UNIF) Higher-order unification from E-unification with second-order equations and parametrised metavariables
Kudryashov, Yury	(ITP) Formalizing the divergence theorem and the Cauchy integral formula in Lean
Kulíková, Nikola	(FOMEO) First-Order Logic Workbook
Kumar, Akshat	(CP) Trajectory Optimization for Safe Navigation in Maritime Traffic Using Historical Data
Kumar, Mohit	(CP) Learning Constraint Programming Models from Data using Generate-and-Aggregate
Kumar, Mohit	(CP) Learning MAX-SAT Models from Examples using Genetic Algorithms and Knowledge Compilation
Kumar, Ramana	(ITP) Candle: A Verified Implementation of HOL Light
Kumar, T. K. Satish	(CP) Trajectory Optimization for Safe Navigation in Maritime Traffic Using Historical Data
Kunze, Fabian	(ITP) Synthetic Kolmogorov Complexity in Coq
Kuperberg, Denis	(LICS) Bouncing threads for circular and non-wellfounded proofs
Kupferman, Orna	(FLoC) Complexity Measures for Reactive Systems (VardiFest) On how the past illuminates the future
Kupke, Clemens	(LICS) Size measures and alphabetic equivalence in the mu-calculus
Kuryshev, Kevin	(POS) SATViz: Real-Time Visualization of Clausal Proofs
Kutsia, Temur	(IJCAR) A framework for approximate generalization in quantitative theories (ONLINE)
Kuznetsov, Stepan	(LFMTP) Associativity or Non-Associativity, Local or Global! (IJCAR) Non-associative, non-commutative multi-modal linear logic
Köhl, Maximilian Alexander	(CAV) MoGym: Using Formal Models for Training and Verifying Decision-making Agents
Kölbl, Martin	(VardiFest) Checking Legal Contracts - On a Not So Usual Application of Mechanized Logic
König, Barbara	(LICS) Graded Monads and Behavioural Equivalence Games
König, Harald	(TERMGRAPH) Formalization and analysis of BPMN using graph transformation systems
König, Matthias	(PCCR) Tractable Abstract Argumentation via Backdoor-Treewidth (KR) Rediscovering Argumentation Principles Utilizing Collective Attacks (KR) Matthias König's Thesis: Graph Parameters for Abstract Argumentation
Küsters, Ralf	(GuttmanFest) A Tutorial-Style Introduction to DY*
Kľuka, Ján	(FOMEO) First-Order Logic Workbook
Křetínský, Jan	(CAV) PAC Statistical Model Checking of Mean Payoff in Discrete- and Continuous-Time MDP
L
Laarmann, Felix	(FSCD) Restricting tree grammars with term rewriting
Lachnitt, Hanna	(IJCAR) Flexible Proof Production in an Industrial-Strength SMT Solver (SMT) cvc5: A Versatile and Industrial-Strength SMT Solver
Laeufer, Kevin	(CAV) UCLID5: Multi-Modal Formal Modeling, Verification, and Synthesis
Lafleur, Daphné	(CP) Combining Reinforcement Learning and Constraint Programming for Sequence-Generation Tasks with Hard Constraints (CP) Combining Reinforcement Learning and Constraint Programming for Sequence-Generation Tasks with Hard Constraints - Extended Abstract
Lafond, Daniel	(CP) A Constraint Programming Approach to Ship Refit Project Scheduling
Lagniez, Jean Marie	(SAT) A New Exact Solver for (Weighted) Max#SAT
Lahav, Ori	(IJCAR) Effective Semantics for the Modal Logics K and KT via Non-deterministic Matrices (FRIDA) What's Decidable about Causally Consistent Shared Memory?
Lai, Yong	(MC) Scalable Uniform Sampling via Efficient Knowledge Compilation
Lal, Akash	(CAV) Proof-guided Underapproximation Widening for Bounded Model Checking
Lamanna, Leonardo	(KR) Online Grounding of Symbolic Planning Domains in Unknown Environments
Lamb, Luis	(VardiFest) From Logic to Neurosymbolic AI
Lamma, Evelina	(PLP) Semantics for Hybrid Probabilistic Logic Programs with Function Symbols: Technical Summary (ICLP) An Iterative Fixpoint Semantics for MKNF Hybrid Knowledge Bases with Function Symbols (ICLP) Exploiting Parameters Learning for Hyper-parameters Optimization in Deep Neural Networks
Lammich, Peter	(ITP) Refinement of Parallel Algorithms down to LLVM (PDAR) Isabelle LLVM Parallel
Lamo, Yngve	(TERMGRAPH) Formalization and analysis of BPMN using graph transformation systems
Lampropoulos, Leonidas	(ITP) Deeper Shallow Embeddings (CSF) A Formal Model of Checked C
Lan, Jianglin	(FoMLAS) Tight Neural Network Verification via Semidefinite Relaxations and Linear Reformulations
Lanckriet, Emiel	(FCS) pi_RA: A pi-calculus for verifying protocols that use remote attestation
Landver, Avner	(VardiFest) Moshe Vardi and Intel Corporation: Long and Fruitful Collaboration
Lange, Martin	(FOMEO) Towards Graphical Feedback in the DiMo Learning Tool
Lanti, Davide	(DL) Ontology-based Data Federation (Extended Abstract)
Lanzinger, Matthias	(ICLP) MV-Datalog+/-: Effective Rule-based Reasoning with Uncertain Observations (Best Paper Award)
Larchey-Wendling, Dominique	(Coq) A Coq Library for Mechanised First-Order Logic
Larroque, Lucas	(KR) Normalisations of Existential Rules: Not so Innocuous!
Larry, Paulson	(IJCAR) Bayesian Ranking for Strategy Scheduling in Automated Theorem Provers
Lasota, Sławomir	(LICS) Solvability of orbit-finite systems of linear equations
Latour, Anna	(MC) Stochastic Constraint Optimisation with Applications in Network Analysis
Laud, Peeter	(CSF) Interpreting Epsilon of Differential Privacy in Terms of Advantage in Guessing or Approximating Sensitive Attributes
Lauermann, Nils	(ITP) Synthetic Kolmogorov Complexity in Coq
Lauko, Henrich	(CAV) From Spot 2.0 to Spot 2.10: What's New?
Laurent, Olivier	(TLLA-LINEARITY) Bottom-Up Sequentialization of Unit-Free MALL Proof Nets
Lauria, Massimo	(PC) On vanishing sums of roots of unity in polynomial calculus and sum-of-squares
Law, Mark	(ICLP) Efficient lifting of symmetry breaking constraints for complex combinatorial problems (Best Student Paper Award)
Lazić, Marijana	(Mentoring Workshop) Welcome
Le Duc, Chan	(DL) Category-based Semantics for the Description Logic ALC and Reasoning
Lecomte, Nicolas	(ASPOCP) Computing H-Partitions in ASP and Datalog
Lecoutre, Christophe	(CP) Aggressive Bound Descent for Constraint Optimization
Lee, Alice	(CSF) Adversary Safety by Construction in a Language of Cryptographic Protocols
Lee, Jia	(CAV) STLmc: Robust STL Model Checking of Hybrid Systems using SMT
Lee, Jimmy H. M.	(CP) Exploiting Functional Constraints in Generating Dominance Breaking Nogoods for Constraint Optimization (CP) Exploiting Functional Constraints in Automatic Dominance Breaking for Constraint Optimization (Extended Abstract) (ModRef) Automatic Generation of Dominance Breaking Nogoods for Constraint Optimization
Lee, Juneyoung	(CAV) SMT-based Translation Validation for Machine Learning Compiler
Lee, Nian-Ze	(iPRA) Interpolation and SAT-Based Model Checking Revisited: Adoption to Software Verification
Lefaucheux, Engel	(LICS) The boundedness and zero isolation problems for weighted automata over nonnegative rationals
Lehtonen, Tuomo	(KR) Computing Stable Argumentative Conclusions under the Weakest-Link Principle in the ASPIC+ Framework (KR) Computational Aspects of Structured Argumentation
Leidinger, Hendrik	(IJCAR) SCL(EQ): SCL for First-Order Logic with Equality
Leino, Klas	(FoMLAS) Self-Correcting Neural Networks For Safe Classification
Leite, João	(ICLP) On Syntactic Forgetting under Uniform Equivalence (ICLP) Tractable Reasoning using Logic Programs with Intensional Concepts (KR) Looking Inside the Black-Box: Logic-based Explanations for Neural Networks (XLoKR) Modular Provenance in Multi-Context Systems
Lemay, Jean-Simon	(TLLA-LINEARITY) Copromotion and Taylor Approximation (Work in Progress)
Lengal, Ondrej	(CAV) Complementing Büchi Automata with Ranker
Lenisa, Marina	(FSCD) On Quantitative Algebraic Higher-Order Theories
Lenzerini, Maurizio	(VardiFest) Rewriting of Regular Path Queries: The first paper of the four Italians
Leone, Nicola	(ICLP) Applications of Answer Set Programming to Smart Devices and Large Scale Reasoning
Lequen, Arnaud	(CP) Isomorphisms between STRIPS problems and sub-problems
Lester, Martin Mariusz	(ModRef) Solving XCSP3 constraint problems using tools from software verification
Leszczyńska-Jasion, Dorota	(IJCAR) Synthetic tableaux: minimal tableau search heuristics
Leue, Stefan	(VardiFest) Checking Legal Contracts - On a Not So Usual Application of Mechanized Logic
Leuschel, Michael	(ICLP) Making ProB compatible with SICStus and SWI-Prolog (Best Application Paper Award)
Leutgeb, Lorenz	(CAV) Automated Expected Amortised Cost Analysis of Probabilistic Data Structures (PAAR) A Two-Watched Literal Scheme for First-Order Logic (IJCAR) An Efficient Subsumption Test Pipeline for BS(LRA) Clauses
Levie, Ron	(LMML) A Rate-Distortion Framework for Explaining Model Decisions and Application to CartoonX
Levy, Natan	(FoMLAS) RoMA: a Method for Neural Network Robustness Measurement and Assessment
Lew, Ethan	(CAV) Reachability of Koopman Linearized Systems Using Random Fourier Feature Observables and Polynomial Zonotope Refinement
Lewandwoski, Basile	(NSV) Neural Network Precision Tuning Using Stochastic Arithmetic
Lewis, Robert	(ITP) Formalized functional analysis with semilinear maps (SC^2) Computer algebra and automation in Lean's mathematical library
Li, Bohan	(CAV) Local Search For SMT on Linear Integer Arithmetic
Li, Da-Wei	(KR) Open Relation Extraction With Non-existent and Multi-span Relationships
Li, Fang	(ICLP) Graph-based Interpretation of Normal Logic Programs
Li, Guanyan	(LICS) Probabilistic Verification Beyond Context-Freeness
Li, Hongbo	(CP) A Portfolio-Based Approach to Select Efficient Variable Ordering Heuristics for Constraint Satisfaction Problems
Li, Jianwen	(VardiFest) SAT-based Reasoning Techniques for LTL over Finite and Infinite Traces
Li, Liyi	(CSF) A Formal Model of Checked C
Li, Ninghui	(CSF) Membership Inference Attacks against Classifiers
Li, Peixuan	(CSF) Towards a General-Purpose Dynamic Information Flow Policy
Li, Xu	(KR) Dynamic Deontic Logic for Permitted Announcements (KR) Deontic Logic for Epistemic Actions
Li, Yannan	(CAV) Synthesizing Fair Decision Trees via Iterative Constraint Solving
Li, Yong	(CAV) Divide-and-Conquer Determinization of Büchi Automata based on SCC Decomposition (VardiFest) Divide-and-Conquer Determinization for B\"uchi Automata
Li, Zekun	(KR) Open Relation Extraction With Non-existent and Multi-span Relationships
Li, Zhanshan	(CP) A Portfolio-Based Approach to Select Efficient Variable Ordering Heuristics for Constraint Satisfaction Problems
Li, Zhengyu	(SC^2) An SC-Square Approach to the Minimum Kochen–Specker Problem
Liang, Chencheng	(PAAR) Exploring Representation of Horn clauses using GNNs
Libal, Tomer	(ARQNL) Do Lawyers Use Automated Reasoning?
Libkin, Leon	(KR) Graph Queries: Do We Study What Matters?
Libkin, Leonid	(VardiFest) Approximations of Certain Answers in First-Order Logic
Lichter, Moritz	(LICS) Choiceless Polynomial Time with Witnessed Symmetric Choice
Lifschitz, Vladimir	(ASPOCP) Translating Definitions into the Language of Logic Programming: A Case Study (ICLP) Strong Equivalence of Logic Programs with Counting (ICLP) Transforming Gringo Rules into Formulas in a Natural Way
Lim, How Khang	(GDE) Automating Defeasible Reasoning in Law with Answer Set Programming
Lin, Anthony Widjaja	(LICS) Reasoning on Data Words over Numeric Domains (LICS) Ramsey Quantifiers over Automatic Structures: Complexity and Applications to Verification (VardiFest) Data Path Queries over Embedded Graph Databases
Lin, Shaokai	(CAV) UCLID5: Multi-Modal Formal Modeling, Verification, and Synthesis
Lin, Yu-Yang	(PERR) From Bounded Checking to Verification of Equivalence via Symbolic Up-to Techniques (Extended Abstract)
Lipton, Richard	(LICS) On the Skolem Problem and the Skolem Conjecture
Liu, Junyi	(LICS) Quantum Weakest Preconditions for Reasoning about Expected Runtimes of Quantum Programs
Liu, Mo	(DECFOML) Are Bundles Good Deals for FOML?
Liu, Si	(CSF) N-Tube: Formally Verified Secure Bandwidth Reservation in Path-Aware Internet Architectures
Liu, Wanwei	(CAV) PoS4MPC: Automated Security Policy Synthesis for Secure Multi-Party Computation
Liu, Xiangshuang	(CP) Completeness Matters: Towards Efficient Caching in Tree-based Synchronous Backtracking Search for DCOPs
Liu, Yiyun	(CSF) A Formal Model of Checked C
Lobo, Jorge	(KR) Embed2Sym - Scalable Neuro-Symbolic Reasoning via Clustered Embeddings
Lochmann, Alexander	(IWC) Formalized Signature Extension Results for Equivalence
Lodder, Josje	(FOMEO) LogInd, a tool for supporting students in mastering structural induction
Logan, Brian	(KR) Automatic Synthesis of Dynamic Norms for Multi-Agent Systems
Lolic, Anela	(IJCAR) Sequent Calculi for Choice Logics
Lommen, Nils	(WST) Improved Automatic Complexity Analysis of Integer Programs (WST) AProVE 2022 (WST) Automatic Complexity Analysis of (Probabilistic) Integer Programs via KoAT (IJCAR) Automatic Complexity Analysis of Integer Programs via Triangular Weakly Non-Linear Loops
Lomuscio, Alessio	(FoMLAS) Tight Neural Network Verification via Semidefinite Relaxations and Linear Reformulations
Lopez, Aliaume	(LICS) When Locality Meets Preservation
Lopez, Jheisson	(CP) Large Neighborhood Search for Robust Solutions for Constraint Satisfaction Problems with Ordered Domains (CP) Large Neighborhood Search for Robust Solutions for Constraint Satisfaction Problems with Ordered Domains
Lorini, Emiliano	(KR) Epistemic Actions: Comparing Multi-agent Belief Bases with Action Models
Lu, Xiao-Nan	(POS) DPS: A Framework for Deterministic Parallel SAT Solvers
Lu, Yun	(CSF) Collusion-Preserving Computation without a Mediator
Luca, Florian	(LICS) On the Skolem Problem and the Skolem Conjecture
Lucas, Salvador	(IWC) Proving Confluence with CONFident (IWC) On local confluence of conditional rewrite systems
Luccio, Flaminia	(GuttmanFest) Secure Key Management Policies in Strand Spaces
Lugo, Justin	(ICLP) A Preliminary Data-driven Analysis of Common Errors Encountered by Novice Answer Set Programmers
Lukács, Dániel	(WPTE) Refactoring Steps for P4 (work in progress)
Lutz, Carsten	(KR) Ontology-Mediated Querying on Databases of Bounded Cliquewidth (KR) Conservative Extensions for Existential Rules
Lutz, Carsten	(DL) Actively Learning ELIQs in the Presence of DL-Lite-Horn Ontologies
Lv, Yi	(ITP) Compositional Verification of Interacting Systems using Event Monads
Lynch, Christopher	(UNIF) Unification Decision Procedures using Basic Narrowing modulo an Equational Theory
Lyon, Tim	(KR) Automating Reasoning with Standpoint Logic via Nested Sequents (DL) Uniform and Modular Sequent Systems for Description Logics
M
Ma, Thanh	(KR) Region-Based Merging of Open-Domain Terminological Knowledge (KR) On Merging of Open-Domain Ontologies
Ma, Yue	(IJCAR) Hyper-graph based Inference Rules for Computing EL+-Ontology Justifications
Macbeth, Heather	(ITP) Formalized functional analysis with semilinear maps
Magaud, Nicolas	(ITP) Proof Pearl: Formalizing Spreads and Packings of the Smallest Projective Space PG(3,2) using the Coq Proof Assistant
Maggi, Fabrizio Maria	(ICLP) ASP-Based Declarative Process Mining
Mahajan, Avishkar	(GDE) Automating Defeasible Reasoning in Law with Answer Set Programming
Mahajan, Meena	(SAT) QBF Merge Resolution is powerful but unnatural
Mahboubi, Assia	(Coq) Trakt: a generic pre-processing tactic for theory-based proof automation
Maietti, Maria Emilia	(HoTT/UF) The Compatibility of MF with HoTT
Majumdar, Rupak	(LICS) The complexity of bidirected reachability in valence systems
Makowsky, Johann	(LogTeach) Why and how to teach logic for CS undergraduates
Mal, Soumodev	(LICS) On the Satisfiability of Context-free String Constraints with Subword Ordering
Malhotra, Sagar	(PLP) On Projectivity in Markov Logic Networks
Malik, Sharad	(VardiFest) Bridging Practice and Theory in SAT: Moshe Vardi the Catalyst
Malladi, Sreekanth	(GuttmanFest) Adapting constraint solving to automatically analyze UPI Protocols
Maly, Jan	(IJCAR) Sequent Calculi for Choice Logics
Manerkar, Yatin	(DSV) UCLID5: Multi-Modal Formal Modeling, Verification, and Synthesis
Manerkar, Yatin A.	(CAV) UCLID5: Multi-Modal Formal Modeling, Verification, and Synthesis
Mangal, Ravi	(FoMLAS) Self-Correcting Neural Networks For Safe Classification (FoMLAS) A Cascade of Checkers for Run-time Certification of Local Robustness
Mangla, Chaitanya	(IJCAR) Bayesian Ranking for Strategy Scheduling in Automated Theorem Provers
Manhaeve, Robin	(ICLP) DeepStochLog: Neural Stochastic Logic Programming
Manighetti, Matteo	(TLLA-LINEARITY) Peano Arithmetic and muMALL: An extended abstract
Manino, Edoardo	(FoMLAS) Counter-Example Guided Neural Network Compression Refinement (CEG4N)
Manière, Quentin	(KR) Counting queries over ELHI⊥ ontologies (DL) Complexity Landscape for Counting Queries (Extended abstract)
Manlove, David	(KR) A General Framework for Stable Roommates Problems using Answer Set Programming
Mann, Makai	(SMT) cvc5: A Versatile and Industrial-Strength SMT Solver (SMT) Bit-Precise Reasoning via Int-Blasting
Manquinho, Vasco	(SAT) SAT-based Leximax Optimisation Algorithms
Mansky, William	(ASL) Proving Logical Atomicity using Lock Invariants
Mansutti, Alessio	(LICS) Geometric decision procedures and the VC dimension of linear arithmetic theories
Mantenoglou, Periklis	(ICLP) Stream Reasoning with Deadlines (KR) Stream Reasoning with Cycles (KR) Optimisation Methods for Complex Event Recognition
Mantenogloy, Periklis	(PLP) Online Reasoning under Uncertainty with the Event Calculus
Marcinkowski, Jerzy	(KR) Conservative Extensions for Existential Rules
Marcos, Joao	(IJCAR) Finite two-dimensional proof systems for non-finitely axiomatizable logics
Maris, Frédéric	(CP) Isomorphisms between STRIPS problems and sub-problems
Mariño, Julio	(FMBC) Automatic generation of attacker contracts in Solidity
Markovich, Réka	(KR) Dynamic Deontic Logic for Permitted Announcements
Marpally, Shashank Rao	(KR) Discovering User-Interpretable Capabilities of Black-Box Planning Agents
Marquis, Pierre	(NMR) Rectifying Classifiers (DL) Rectifying Classifiers
Marra, Giuseppe	(ICLP) DeepStochLog: Neural Stochastic Logic Programming
Marron, Assaf	(VardiFest) Natural Autoencoding
Marshall, Andrew M.	(FSCD) Combined Hierarchical Matching: The Regular Case (UNIF) Graph-Embedded Term Rewrite Systems and Applications (A Preliminary Report)
Marshall, Daniel	(WiL) A Mixed Linear and Graded Logic-Extended Abstract
Martelli, Alberto	(DL) Reasoning about actions with EL ontologies in a temporal action theory (Extended Abstract)
Martens, Chris	(LFMTP) Language Minimalism and Logical Frameworks
Marti, Johannes	(LICS) Size measures and alphabetic equivalence in the mu-calculus
Marti-Oliet, Narciso	(IJCAR) Equational Unification and Matching, and Symbolic Reachability Analysis in Maude 3.2 (System Description)
Marti-Oliet, Narciso	(IFIP-WG1.6) The International School on Rewriting
Martin, Antoine	(CAV) From Spot 2.0 to Spot 2.10: What's New?
Martin, Christian	(PERR) Generating Mutation Tests Using an Equivalence Prover
Martin-Dorel, Erik	(Coq) Coq Community Survey 2022: Summary of Results
Martinelli Tabajara, Lucas	(VardiFest) Boolean Synthesis via Decision Diagrams
Martins, Ruben	(SAT) Certified CNF Translations for Pseudo-Boolean Solving
Marynissen, Simon	(ICLP) Nested Justification Systems (ICLP) Tree-Like Justification Systems are Consistent
Matache, Cristina	(LICS) Concrete categories and higher-order recursion (with applications including probability, differentiability, and full abstraction)
Matos, Vinícius Bitencourt	(NMR) Repairing Ontologies via Kernel Pseudo-Contraction (DL) Repairing Ontologies via Kernel Pseudo-Contraction
Matsumoto, Naoki	(CAV) Oblivious Online Monitoring for Safety LTL Specification via Fully Homomorphic Encryption
Matsuoka, Kotaro	(CAV) Oblivious Online Monitoring for Safety LTL Specification via Fully Homomorphic Encryption
Matsuzaki, Takuya	(IJCAR) Formula Simplification via Invariance Detection by Algebraically Indexed Types (ONLINE)
Matthes, Ralph	(HoTT/UF) A Library of Monoidal Categories for Display and Univalence
Maubert, Bastien	(KR) Private and public affairs in strategic reasoning (VardiFest) Automated Synthesis of Mechanisms
Mauw, Sjouke	(FSCD) A Graphical Proof Theory of Logical Time (CSF) Is Eve nearby? Analysing protocols under the distant-attacker assumption (CSF) Contingent payments from two-party signing and verification for abelian groups (CSF) Unlinkability of an Improved Key Agreement Protocol for EMV 2nd Gen Payments (FCS) Towards Unlinkable Smartcard-based Payments: an extended abstract
Mavridou, Anastasia	(CAV) Capture, Analyze, Diagnose: Realizability Checking of Requirements in FRET
May, Alexander	(CSF) Legendre PRF (Multiple) Key Attacks and the Power of Preprocessing
Mayer-Eichberger, Valentin	(SAT) QBF Programming with the Modeling Language Bule
Mazowiecki, Filip	(CAV) Verifying generalised and structural soundness of workflow nets via relaxations (LICS) The complexity of soundness in workflow nets (LICS) The boundedness and zero isolation problems for weighted automata over nonnegative rationals
Mazure, Bertrand	(CP) Aggressive Bound Descent for Constraint Optimization
Mazzocchi, Nicolas	(CAV) FORQ-based Language Inclusion Formal Testing
Mazzullo, Andrea	(ARQNL) Reasoning in Non-normal Modal Description Logics (DL) More on Interpolants and Explicit Definitions for Description Logics with Nominals and/or Role Inclusions
McBurney, Peter	(KR) Towards an Enthymeme-Based Communication Framework in Multi-Agent Systems
McCreesh, Ciaran	(CP) An Auditable Constraint Programming Solver (CP) Solving with Provably Correct Results: Beyond Satisfiability, and Towards Constraint Programming (POS) Certified Symmetry and Dominance Breaking for Combinatorial Optimisation
McDermott, Dylan	(FSCD) Galois connecting call-by-value and call-by-name
McIver, Annabelle	(CSF) Universal Optimality and Robust Utility Bounds for Metric Differential Privacy
McLean, Brett	(KR) A Gödel calculus for Linear Temporal Logic
McMillan, Ken	(iPRA) Interpolants and Transformational Proof Systems
Meadows, Catherine	(GuttmanFest) Protocol Analysis with Time and Space
Meda, Jaydeepsinh	(CAV) Proof-guided Underapproximation Widening for Bounded Model Checking
Medioni, Thomas	(CAV) From Spot 2.0 to Spot 2.10: What's New?
Meel, Kuldeep S.	(CP) On Quantitative Testing of Samplers (CP) Early Career Award (CP) Boolean Functional Synthesis and its Applications (ICLP) ApproxASP – A Scalable Approximate Answer Set Counter (CAV) A Scalable Shannon Entropy Estimator (LICS) On Almost-Uniform Generation of SAT Solutions: The power of 3-wise independent hashing (VeriProp) Distribution Testing and Probabilistic Programming: A Match made in Heaven (MC) Scalable Uniform Sampling via Efficient Knowledge Compilation (MC) Designing Samplers is Easy: The Boon of Testers (VardiFest) Comments from Giuseppe, Kuldeep, and Kristin (DSV) Democratizing SAT Solving
Megdiche, Yecine	(Isabelle) A Linter for Isabelle: Implementation and Evaluation
Meggendorfer, Tobias	(CAV) Sound and Complete Certificates for Quantitative Termination Analysis of Probabilistic Programs (FOMEO) DOMtutor -- Competitive Programming as Teaching Tool
Mehta, Bhavik	(ITP) Formalizing Szemerédi's Regularity Lemma in Lean
Meier, Arne	(LICS) Temporal Team Semantics Revisited (MC) Counting Complexity for Projected Reasoning in Abstract Argumentation
Meiswinkel, Sebastian	(CP) Modeling and Solving Parallel Machine Scheduling with Contamination Constraints in the Agricultural Industry
Melkonian, Orestis	(FMBC) Designing EUTxO smart contracts as communicating state machines: the case of simulating accounts (FMBC) Determinism of ledger updates (FMBC) Human and machine-readable models of state machines for the Cardano ledger
Mell, Stephen	(TERMGRAPH) Ideograph: A Language for Expressing and Manipulating Structured Data
Melliès, Paul-André	(LICS) A functorial excursion between algebraic geometry and linear logic
Meng, Baoluo	(GDE) Unmanned Aerial Vehicle compliance checking using Goal-Directed Answer Set Programming
Mengel, Stefan	(SAT) Changing Partitions in Rectangle Decision Lists
Mengin, Jérôme	(CP) Nucleus-Satellites Systems of OMDDs for Reducing the Size of Compiled Forms
Menz, Jan	(FCS) Compositional Higher-order Declassification Using Logical Relations
Mery, Daniel	(ASL) Labelled Tableaux for Linear Time Bunched Implication Logic
Meseguer, Jose	(IJCAR) Equational Unification and Matching, and Symbolic Reachability Analysis in Maude 3.2 (System Description) (GuttmanFest) Protocol Analysis with Time and Space
Mesejo, Pablo	(SAT) On the performance of deep generative models of realistic SAT instances
Mestel, David	(CSF) How Efficient are Replay Attacks against Vote Privacy? A Formal Quantitative Analysis (CSF) Beware of Greeks bearing entanglement? Quantum covert channels, information flow and non-local games
Metcalfe, George	(iPRA) Interpolation via Finitely Subdirectly Irreducible Algebras
Metzger, Niklas	(CAV) Information Flow Guided Synthesis (CAV) Explaining Hyperproperty Violations
Meyer, Eleanore	(WST) Improved Automatic Complexity Analysis of Integer Programs (WST) AProVE 2022 (WST) Automatic Complexity Analysis of (Probabilistic) Integer Programs via KoAT (IJCAR) Automatic Complexity Analysis of Integer Programs via Triangular Weakly Non-Linear Loops
Meyer, Eleanore	(VeriProp) Inferring Expected Runtimes and Sizes
Meyer, Thomas	(NMR) Situated Conditionals - A Brief Introduction (NMR) Asking human reasoners to judge postulates of belief change for plausibility (NMR) Conditional Syntax Splitting, Lexicographic Entailment and the Drowning Effect (KR) KR 2022 Closing
Miceli, Marie	(SAT) A New Exact Solver for (Weighted) Max#SAT
Michel, Friedrich	(DL) Efficient TBox Reasoning with Value Restrictions using the FL0wer Reasoner (Extended Abstract)
Michel, Laurent	(CP) Heuristics for MDD Propagation in Haddock (CP) DUELMIPs: Jointly Optimizing Software Defined Network Functionality and Security (CP) MDD-Based Constraint Programming in Haddock
Micheli, Andrea	(KR) On the Expressive Power of Intermediate and Conditional Effects in Temporal Planning
Middeldorp, Aart	(FSCD) Polynomial Termination over N is Undecidable (WST) Hydra Battles and AC Termination (WST) DEPP (IWC) Formalized Signature Extension Results for Equivalence (IWC) Development Closed Critical Pairs: Towards a Formalized Proof (IWC) Confluence Competition
Middeldorp, Aart	(IFIP-WG1.6) The International School on Rewriting
Miguel, Ian	(CP) A framework for generating informative benchmark instances (CP) Plotting: A Planning Problem With Complex Transitions
Milanese, Gian Carlo	(UNIF) Fuzzy Order-Sorted Feature Term Unification
Milius, Stefan	(FSCD) Stateful Structural Operational Semantics (LICS) Graded Monads and Behavioural Equivalence Games
Millen, Jonathan	(GuttmanFest) Adapting constraint solving to automatically analyze UPI Protocols
Miller, Dale	(TLLA-LINEARITY) Peano Arithmetic and muMALL: An extended abstract (LFMTP) A positive perspective on term representation: work in progress
Milo, Mikkel	(FMBC) Finding smart contract vulnerabilities with ConCert's property-based testing framework
Mimram, Samuel	(FSCD) Division by two, in homotopy type theory
Mio, Matteo	(LICS) Beyond Nonexpansive Operations in Quantitative Algebraic Reasoning
Mitsch, Stefan	(IJCAR) Implicit Definitions with Differential Equations for KeYmaera X (System Description)
Mittelmann, Munyque	(KR) Logics for Representation and Design of Auctions (VardiFest) Automated Synthesis of Mechanisms
Mitterwallner, Fabian	(FSCD) Polynomial Termination over N is Undecidable (WST) DEPP (IWC) Formalized Signature Extension Results for Equivalence
Mocanu, Ionela	(KR) On the learnability of knowledge in language domains
Mogavero, Fabio	(VardiFest) Strategy Logic: Origin, Results, and Open Questions
Mohamed, Abdalrhman	(SMT) cvc5: A Versatile and Industrial-Strength SMT Solver
Mohamed, Mudathir Mahgoub Yahia	(SMT) cvc5: A Versatile and Industrial-Strength SMT Solver
Moine, Alexandre	(ASL) Polishing a Rough Diamond: An Enhanced Separation Logic for Heap Space under Garbage Collection
Mok, Matej	(FOMEO) First-Order Logic Workbook
Molin, Adam	(FoMLAS) Formal Specification for Learning-Enabled Autonomous Systems (Extended Abstract)
Moller, Faron	(LogTeach) Introducing Logic by Stealth to Computer Science Students
Mondal, Priyanka	(CSF) Applying consensus and replication securely with FLAQR
Moniot, Monica	(FCS) Robust Indistinguishability
Monroe, Hunter	(PC) Hard Inputs from Kolmogorov Randomness---Can Merlin Tame Open Problems?
Montacute, Yoàv	(LICS) The Pebble-Relation Comonad in Finite Model Theory
Montalbano, Pierre	(CP) Parallel Hybrid Best-First Search
Montali, Marco	(DL) Extraction of Object-Centric Event Logs through Virtual Knowledge Graphs (IJCAR) CTL* model checking for data-aware dynamic systems with arithmetic
Montanari, Angelo	(VardiFest) The Safety Fragment of LTL
Mora, Federico	(CAV) UCLID5: Multi-Modal Formal Modeling, Verification, and Synthesis
Morak, Michael	(ICLP) Determining Action Reversibility in STRIPS Using Answer Set Programming with Quantifiers
Morales, Jose F.	(GDE) An s(CASP) In-Browser Playground based on Ciao Prolog
Moreau, Solène	(CSF) Cracking the Stateful Nut -- Computational Proofs of Stateful Security Protocols using the Squirrel Proof Assistant
Moreno-Rebato, Mar	(GDE) Modeling Administrative Discretion Using Goal-Directed Answer Set Programming
Morris, Jason	(GDE) Blawx: Web-based user-friendly Rules as Code
Mosca, Alessandro	(DL) Ontology-based Data Federation (Extended Abstract)
Moser, Georg	(CAV) Automated Expected Amortised Cost Analysis of Probabilistic Data Structures (LICS) Quantum Expectation Transformers for Cost Analysis
Moses, Yoram	(CAV) Information Flow Guided Synthesis (FRIDA) On Direct and Indirect Information in Distributed Protocols (VardiFest) A Toast for Moshe at the FLoC VardiFest
Moss, Eliot	(ITP) Mechanizing Soundness of Off-Policy Evaluation
Moss, Sean	(LICS) Concrete categories and higher-order recursion (with applications including probability, differentiability, and full abstraction) (LICS) Probability monads with submonads of deterministic states
Mosse, Milan	(SAT) A generalization of the Satisfiability Coding Lemma and its applications
Motik, Boris	(KR) Faithful Approaches to Rule Learning
Mottet, Antoine	(LICS) Smooth approximations and CSPs over finitely bounded homogeneous structures
Mugnier, Marie-Laure	(KR) Normalisations of Existential Rules: Not so Innocuous!
Mugnier, Marie-Laure	(DL) DL Opening Remarks
Mugnier, Marie-Laure	(DL) Business Meeting
Murano, Aniello	(KR) Private and public affairs in strategic reasoning (VardiFest) Formal Aspects of Strategic Reasoning in MAS (VardiFest) Automated Synthesis of Mechanisms
Murawski, Andrzej	(LICS) Probabilistic Verification Beyond Context-Freeness (PERR) Compositional relational reasoning via operational game semantics
Murlak, Filip	(KR) Finite Entailment of UCRPQs over ALC Ontologies
Muruganandham, Pazhamalai	(CAV) PAC Statistical Model Checking of Mean Payoff in Discrete- and Continuous-Time MDP
Muscholl, Anca	(LICS) Active learning for sound negotiations
Musliu, Nysret	(CP) Modeling and Solving Parallel Machine Scheduling with Contamination Constraints in the Agricultural Industry (ICLP) Large-Neighbourhood Search for ASP Optimisation (KR) ALASPO: An Adaptive Large-Neighbourhood ASP Optimiser
Mycroft, Alan	(FSCD) Galois connecting call-by-value and call-by-name
Myers Jr, J Paul	(LogTeach) Possible Desiderata for Logic in the CS Curriculum
Myreen, Magnus O.	(ITP) Candle: A Verified Implementation of HOL Light (ITP) Taming an Authoritative Armv8 ISA Specification: L3 Validation and CakeML Compiler Verification
Mählmann, Nikolas	(LICS) Model Checking on Interpretations of Classes of Bounded Local Cliquewidth
Méndez, Julián	(DL) On the Eve of True Explainability for OWL Ontologies: Description Logic Proofs with Evee and Evonne (XLoKR) Explaining Description Logic Entailments in Practice with Evee and Evonne (IJCAR) Evonne: Interactive Proof Visualization for Description Logics (System Description)
Mödersheim, Sebastian	(CSF) Privacy as Reachability (GuttmanFest) Security Protocols as Choreographies (GuttmanFest) Three Branches of Accountability
Møgelberg, Rasmus Ejlers	(LICS) Greatest HITs: Higher inductive types in coinductive definitions via induction under clocks
Mück, Niklas	(Coq) A Coq Library for Mechanised First-Order Logic
Müller, Johannes	(CSF) How Efficient are Replay Attacks against Vote Privacy? A Formal Quantitative Analysis
Müller, Mark Niklas	(LMML) Verification of Realistic Neural Networks (FoMLAS) VNN-COMP 2022
Müller, Peter	(CAV) Sound Automation of Magic Wands
Mündler, Niels	(Isabelle) A Verified Implementation of B-trees in Isabelle/HOL
N
Naaf, Matthias	(LICS) Zero-One Laws and Almost Sure Valuations of First-Order Logic in Semiring Semantics
Nabeshima, Hidetomo	(POS) DPS: A Framework for Deterministic Parallel SAT Solvers
Nacenta, Miguel	(CP) Understanding how people approach constraint modelling and solving
Nadathur, Gopalan	(LFMTP) Reasoning about Specifications in LF
Nadel, Alexander	(SAT) Introducing Intel(R) SAT Solver (SAT) 25 years of SAT: Conflict-Driven SAT Solving
Nagendra, Srinidhi	(FMBC) A Domain Specific Language for Testing Consensus Implementations
Naik, Mayur	(SYNT) Complexity of Relational Query Synthesis
Nalbach, Jasper	(SC^2) Cylindrical Algebraic Coverings for Quantifiers
Nalon, Cláudia	(DL) A Labelled Natural Deduction System for an Intuitionistic Description Logic with Nominals (IJCAR) Local Reductions for the Modal Cube
Nam, Seunghyeon	(CAV) SMT-based Translation Validation for Machine Learning Compiler
Nantes-Sobrinho, Daniele	(FSCD) Nominal Anti-Unification with Atom-Variables (FSCD) A Certified Algorithm for AC-Unification (UNIF) Nominal Anti-Unification of Letrec-Expressions
Narodytska, Nina	(CP) Industrial Research Career Path as a Sequence of Constraint Satisfaction Problems (SAT) Analysis of Core-Guided MaxSAT Using Cores and Correction Sets (LMML) Verification of Binarized Neural Networks: Challenges and Opportunities (FoMLAS) Scalable Verification of GNN-based Job Schedulers
Nebel, Bernhard	(DL) Expressivity of Planning with Horn Description Logic Ontologies (Extended Abstract)
Nedunuri, Srinivas	(SYNT) Inferring Environment Assumptions in Model Refinement
Neele, Thomas	(ARQNL) (Re)moving Quantifiers to Simplify Parameterised Boolean Equation Systems
Nelson, Tim	(VardiFest) Little Tricky Logic: Misconceptions in the Understanding of LTL
Nelson, Tim	(GuttmanFest) Prototyping Formal Methods Tools: a Protocol Analysis Case Study
Neumann, Jacob	(HoTT/UF) Towards Directed Higher Observational Type Theory
Neuper, Walther	(Isabelle) Towards Accessible Formal Mathematics with ISAC and Isabelle/VSCode
Nguewouo, Franklin	(CP) Scheduling the Equipment Maintenance of an Electric Power Transmission Network using Constraint Programming (CP) Extended Abstract for : Scheduling the Equipment Maintenance of an Electric Power Transmission Network using Constraint Programming
Nguyen, Van	(ICLP) Model Reconciliation in Logic Programs
Nicholas, Charles	(GuttmanFest) Searching for Selfie in TLS 1.3 with the Cryptographic Protocol Shapes Analyzer
Nickovic, Dejan	(FoMLAS) Formal Specification for Learning-Enabled Autonomous Systems (Extended Abstract)
Nicolicin-Georgescu, Vlad	(WiL) Automated Logic-Based Reasoning for Analyzing Prime Video Code
Niehren, Joachim	(ICLP) Jumping Evaluation of Nested Regular Path Queries
Nielsen, Eske Hoy	(FMBC) Finding smart contract vulnerabilities with ConCert's property-based testing framework
Nielson, Flemming	(GuttmanFest) Benign Interaction of Security Domains
Nielson, Hanne Riis	(GuttmanFest) Benign Interaction of Security Domains
Niemetz, Aina	(CAV) Murxla: A Modular and Highly Extensible API Fuzzer for SMT Solvers (IJCAR) Flexible Proof Production in an Industrial-Strength SMT Solver (SMT) Murxla: A Modular and Highly Extensible API Fuzzer for SMT Solvers (SMT) cvc5: A Versatile and Industrial-Strength SMT Solver (SMT) Bit-Precise Reasoning via Int-Blasting (SMT) Local Search for Bit-Precise Reasoning and Beyond
Nieuwveld, Joris	(LICS) On the Skolem Problem and the Skolem Conjecture
Nigam, Vivek	(GuttmanFest) On the Complexity of Verification of Time-Sensitive Distributed Systems
Nightingale, Peter	(CP) A framework for generating informative benchmark instances (CP) Selecting SAT Encodings for Pseudo-Boolean and Linear Integer Constraints (CP) Selecting SAT Encodings for Pseudo-Boolean and Linear Integer Constraints
Nijssen, Siegfried	(MC) Stochastic Constraint Optimisation with Applications in Network Analysis
Nipkow, Tobias	(Isabelle) Gale-Shapley Verified (Isabelle) A Verified Implementation of B-trees in Isabelle/HOL (Isabelle) Welcome
Nisan, Noam	(LogTeach) Position Paper: Mathematical Logic through Python
Nishida, Naoki	(IFIP-WG1.6) Inversion and Determinization in Term Rewriting (WPTE) On Transforming Imperative Programs into Logically Constrained Term Rewrite Systems via Injective Functions from Configurations to Terms (WPTE) On Transforming Rewriting-Induction Proofs for Logical-Connective-Free Sequents into Cyclic Proofs (WPTE) On Reducing Non-Occurrence of Specified Runtime Errors to All-Path Reachability Problems of Constrained Rewriting
Niskanen, Andreas	(SAT) Incremental Maximum Satisfiability (SAT) MaxSAT-Based Bi-Objective Boolean Optimization
Noetzli, Andres	(CAV) Even Faster Conflicts and Lazier Reductions for String Solvers (PAAR) EuroProofNet presentation on SMT and proofs (IJCAR) Reasoning About Vectors using an SMT Theory of Sequences (IJCAR) Flexible Proof Production in an Industrial-Strength SMT Solver (SMT) cvc5: A Versatile and Industrial-Strength SMT Solver (SMT) Bit-Precise Reasoning via Int-Blasting
Nomikos, Christos	(ICLP) Strong Equivalence of Logic Programs with Ordered Disjunction: a Logical Perspective
Nordström, Jakob	(CP) An Auditable Constraint Programming Solver (POS) Adding Dual Variables to Algebraic Reasoning for Gate-Level Multiplier Verification (POS) Certified Symmetry and Dominance Breaking for Combinatorial Optimisation (SAT) Certified CNF Translations for Pseudo-Boolean Solving
Nordström, Jakob	(CP) Solving with Provably Correct Results: Beyond Satisfiability, and Towards Constraint Programming
Norrish, Michael	(ITP) Kalas: A Verified, End-to-End Compiler for a Choreographic Language (ITP) Mechanizing Soundness of Off-Policy Evaluation
North, Paige	(LICS) Semantics for two-dimensional type theory (HoTT/UF) Towards Normalization of Simplicial Type Theory via Synthetic Tait Computability (HoTT/UF) Semantics for two-dimensional type theory
Nosan, Klara	(LICS) Identity testing for radical expressions
Nouman, Ahmed	(KR) Hybrid Conditional Planning for Robotic Applications (Extended Abstract)
Nowak, David	(WPTE) Towards Corecursion Without Corecursion in Coq
Nowé, Ann	(WOLVERINE) Artificial Intelligence
Nuradiansyah, Adrian	(DL) Optimal ABox Repair w.r.t. Static EL TBoxes: from Quantified ABoxes back to ABoxes (Extended Abstract)
Nyitraiová, Alexandra	(FOMEO) First-Order Logic Workbook
O
O'Neill, Adam	(FCS) Robust Indistinguishability
O'Reilly, Liam	(LogTeach) Introducing Logic by Stealth to Computer Science Students
O'Sullivan, Barry	(CP) Symmetry breaking and Knowledge Compilation (CP) Finding Counterfactual Explanations through Constraint Relaxations (CP) Automated SAT Problem Feature Extraction using 1 Convolutional Autoencoders
Oakley, Lisa	(CSF) Adversarial Robustness Verification and Attack Synthesis in Stochastic Systems
Obitsu, Yuto	(POS) DPS: A Framework for Deterministic Parallel SAT Solvers
Ochs, Daniel	(KR) Neural-Probabilistic Answer Set Programming
Oechsner, Sabine	(CSF) Bringing State-Separating Proofs to EasyCrypt - A Security Proof for Cryptobox
Oertel, Andy	(SAT) Certified CNF Translations for Pseudo-Boolean Solving
Oetsch, Johannes	(ICLP) A Neuro-Symbolic ASP Pipeline for Visual Question Answering (ICLP) Large-Neighbourhood Search for ASP Optimisation (KR) ALASPO: An Adaptive Large-Neighbourhood ASP Optimiser
Oey, Alexander	(ASL) Proving Logical Atomicity using Lock Invariants
Offtermatt, Philip	(CAV) Verifying generalised and structural soundness of workflow nets via relaxations (LICS) The complexity of soundness in workflow nets
Ohlmann, Pierre	(LICS) Characterizing Positionality in Games of Infinite Duration over Infinite Graphs
Ohrem, Christoph	(LICS) Temporal Team Semantics Revisited
Oleon, Émile	(FSCD) Division by two, in homotopy type theory
Oliveira Da Costa, Ana	(WiL) Hypertrace Logic
Olsson, Lars Eric	(GuttmanFest) Securing Node-RED Applications
Oltmann, Thomas	(POS) SATViz: Real-Time Visualization of Clausal Proofs
Olšák, Miroslav	(ITP) The Isabelle ENIGMA
Ong, Luke	(LICS) Probabilistic Verification Beyond Context-Freeness
Onódy, Zoltán	(FOMEO) First-Order Logic Workbook
Oprea, Alina	(CSF) Adversarial Robustness Verification and Attack Synthesis in Stochastic Systems
Orchard, Dominic	(WiL) A Mixed Linear and Graded Logic-Extended Abstract
Ordyniak, Sebastian	(CP) CSP Beyond Tractable Constraint Languages (PCCR) Welcome and Introduction
Orlandelli, Eugenio	(DECFOML) Terminating sequent calculi for decidable fragments of FOML
Orlikowski, Łukasz	(LICS) Lower Bounds for the Reachability Problem in Fixed Dimensional VASSes
Ortiz, Magdalena	(DL) Pointwise Circumscription in Description Logics (IJCAR) Actions over Core-closed Knowledge Bases
Ortiz, Magdalena	(NMR) Pointwise Circumscription in Description Logics
Osipov, George	(PCCR) Resolving Inconsistency of Linear Equations
Ossowski, Sascha	(GDE) Modeling Administrative Discretion Using Goal-Directed Answer Set Programming
Ostrovsky, Matan	(FoMLAS) An Abstraction-Refinement Approach to Verifying Convolutional Neural Networks
Otten, Jens	(ARQNL) Advancing Automated Theorem Proving for the Modal Logics D and S5
Ouaknine, Joel	(LICS) On the Skolem Problem and the Skolem Conjecture (VardiFest) A Brief Glimpse of the Skolem Landscape
Overbeek, Roy	(TERMGRAPH) A PBPO+ Graph Rewriting Tutorial
Ozaki, Ana	(ARQNL) Reasoning in Non-normal Modal Description Logics
Ozdemir, Alex	(IJCAR) Flexible Proof Production in an Industrial-Strength SMT Solver (SMT) cvc5: A Versatile and Industrial-Strength SMT Solver
P
Padalkar, Parth	(GDE) Symbolic Reinforcement Learning Framework with Incremental Learning of Rule-based Policy
Padmanabha, Anantha	(DECFOML) Decidable Fragments of Term Modal Logic
Paesani, Giacomo	(PCCR) Learning Small Decision Trees
Pal, Debtanu	(IJCAR) On eventual non-negativity and positivity for the weighted sum of powers of matrices
Palamidessi, Catuscia	(CSF) Universal Optimality and Robust Utility Bounds for Metric Differential Privacy (FLoC) Information Structures for Privacy and Fairness
Palamidessi, Catuscia	(GuttmanFest) Establishing the Price of Privacy in Federated Data Trading
Palmskog, Karl	(Coq) Coq Community Survey 2022: Summary of Results
Pan, Guanting	(SMT) Goose: A Meta Solver for Deep Neural Network Verification
Pandey, Awanish	(SYNT) Interactive Debugging of Concurrent Programs under Relaxed Memory Models
Panisson, Alison R.	(KR) Towards an Enthymeme-Based Communication Framework in Multi-Agent Systems
Pankova, Alisa	(CSF) Interpreting Epsilon of Differential Privacy in Terms of Advantage in Guessing or Approximating Sensitive Attributes
Papacchini, Fabio	(IJCAR) Local Reductions for the Modal Cube
Papadimitratos, Panagiotis	(CP) Optimized Code Generation against Power Side Channels
Paperman, Charles	(LICS) The Regular Languages of First-Order Logic with One Alternation
Paquet, Hugo	(FSCD) A combinatorial approach to higher-order structure for polynomial functors
Paradžik, Petar	(CSF) Conditional Observational Equivalence and Off-line Guessing Attacks in Multiset Rewriting
Parent, Xavier	(ARQNL) Automated verification of deontic correspondences in Isabelle/HOL - First results (NMR) On some weakenings of transitivity in the logic of norms (extended abstract)
Park, Daniel	(CSF) Adversary Safety by Construction in a Language of Cryptographic Protocols
Park, Junkil	(IJCAR) Reasoning About Vectors using an SMT Theory of Sequences
Parker, Dave	(VeriProp) Safe Sampling-Based Planning for Stochastic Systems with Uncertain Dynamics
Parlato, Gennaro	(CAV) Reasoning about Data Trees using CHCs (DSV) C2C-trans as a design methodology for software verification tools
Parno, Bryan	(FoMLAS) Self-Correcting Neural Networks For Safe Classification
Parsia, Bijan	(DL) Next Steps for ReAD: Modules for Classification Optimisation
Parthasarathy, Gaurav	(CAV) Sound Automation of Magic Wands
Pasi, Gabriella	(UNIF) Fuzzy Order-Sorted Feature Term Unification
Pasquali, Fabio	(LICS) Logical Foundations of Quantitative Equality
Passmore, Grant	(FoMLAS) Neural Networks in Imandra: Matrix Representation as a Verification Choice
Pathak, Drashti	(CAV) Data-Driven Invariant Learning for Probabilistic Programs
Patoglu, Volkan	(KR) Hybrid Conditional Planning for Robotic Applications (Extended Abstract)
Patrizi, Fabio	(ICLP) ASP-Based Declarative Process Mining
Pau, Cleo	(IJCAR) A framework for approximate generalization in quantitative theories (ONLINE)
Paulino-Passos, Guilherme	(XLoKR) On interactive explanations as reasoning
Paulovics, Peter	(FOMEO) SIVA: Simulation and visualization of the DL tableau algorithm
Paulsen, Brandon	(CAV) Example Guided Synthesis of Linear Approximations for Neural Network Verification
Paulson, Lawrence C.	(ITP) Formalising Fisher’s Inequality: Formal Linear Algebraic Techniques in Combinatorics
Pavlovic, Dusko	(GuttmanFest) Probabilistic annotations for protocol models
Peitl, Tomáš	(SAT) Should decisions in QCDCL follow prefix order? (QBF) QCDCL with Cube Learning or Pure Literal Elimination - Part 2 (PC) Are Hitting Formulas Hard for Resolution? (PC) QCDCL with Cube Learning or Pure Literal Elimination – What is best? (PC) QCDCL with Cube Learning or Pure Literal Elimination – What is best? (II)
Peled, Doron	(FoMLAS) Formal Specification for Learning-Enabled Autonomous Systems (Extended Abstract)
Peleg, Hila	(DSV) Interaction Models vs. Formal Models: Synthesis Co-Design
Peltier, Nicolas	(ASL) Two Results on Separation Logic With Theory Reasoning
Peng, Xiao	(CP) Solving the Non-Crossing MAPF for non point-sized robots
Perdrix, Simon	(FSCD) Addition and differentiation of ZX-diagrams (LICS) Quantum Expectation Transformers for Cost Analysis
Pereira Matos Júnior, João Batista	(FoMLAS) Counter-Example Guided Neural Network Compression Refinement (CEG4N)
Perelli, Giuseppe	(KR) Automatic Synthesis of Dynamic Norms for Multi-Agent Systems (VardiFest) On the Extraordinary Effectiveness of Logic in Strategic Reasoning
Perez, Guillermo	(SYNT) SYNTCOMP Results
Perez, Mateo	(VardiFest) An Automata-Theoretic Approach to Model-Free Reinforcement Learning
Perháč, Ján	(FOMEO) Visualization of structural operational semantics over programs of simple imperative language.
Perri, Simona	(ICLP) Applications of Answer Set Programming to Smart Devices and Large Scale Reasoning
Perrig, Adrian	(CSF) N-Tube: Formally Verified Secure Bandwidth Reservation in Path-Aware Internet Architectures
Perrone, Paolo	(LICS) Probability monads with submonads of deterministic states
Perrotin, Elise	(KR) Epistemic Actions: Comparing Multi-agent Belief Bases with Action Models
Perrussel, Laurent	(VardiFest) Automated Synthesis of Mechanisms
Pertseva, Elizaveta	(SYNT) Regex+: Synthesizing Regular Expressions from Positive Examples
Pesant, Gilles	(CP) Combining Reinforcement Learning and Constraint Programming for Sequence-Generation Tasks with Hard Constraints (CP) Exploiting Model Entropy to Make Branching Decisions in Constraint Programming (CP) Combining Reinforcement Learning and Constraint Programming for Sequence-Generation Tasks with Hard Constraints - Extended Abstract
Pestun, Vasily	(ITP) Formalization of a Stochastic Approximation Theorem
Peterfreund, Liat	(KR) Revisiting Semiring Provenance for Datalog
Peterfreund, Liat	(Mentoring Workshop) How logic-based approaches can be used in data management
Peters, Benjamin	(Coq) A Coq Library for Mechanised First-Order Logic
Petković Komel, Anja	(FMBC) Automating Security Analysis of Off-Chain Protocols (WiL) The essence of type-theoretic elaboration
Pettorossi, Alberto	(ICLP) Verifying Catamorphism-Based Contracts using Constrained Horn Clauses
Peyrot, Loïc	(FSCD) Solvability for Generalized Applications
Pfanschilling, Viktor	(KR) Sum-Product Loop Programming: From Probabilistic Circuits to Loop Programming
Pfenning, Frank	(FSCD) Type-Based Termination for Futures
Phalakarn, Kittiphon	(VeriProp) Widest Paths and Global Propagation in Bounded Value Iteration for Stochastic Games
Phawade, Ramchandra	(WiL) Two Dimensional Bounded Model Checking for Unbounded Client-Server Systems
Philipoom, Jade	(ITP) Accelerating Verified-Compiler Development with a Verified Rewriting Engine
Pientka, Brigitte	(LFMTP) A modal analysis of dependently typed metaprogramming
Piepenbrock, Jelle	(ITP) The Isabelle ENIGMA (SAT) Towards Learning Quantifier Instantiation in SMT (IJCAR) Guiding an Automated Theorem Prover with Neural Rewriting
Piessens, Frank	(CSF) Proving full-system security properties under multiple attacker models on capability machines
Pilati, Lorenzo	(SMT) NORMA: a tool for the analysis of Relay-based Railway Interlocking Systems
Pilipczuk, Michał	(LICS) Stable graphs of bounded twin-width (LICS) Treelike decompositions for transductions of sparse graphs
Pimentel, Elaine	(LFMTP) Associativity or Non-Associativity, Local or Global! (IJCAR) Non-associative, non-commutative multi-modal linear logic
Pino Perez, Ramon	(KR) On the Representation of Darwiche and Pearl’s Epistemic States for Iterated Belief Revision
Pino Perez, Ramon	(ICLP) On Paraconsistent Belief Revision: the Case of Priest’s Logic of Paradox (KR) On Paraconsistent Belief Revision in LP (Extended Abstract)
Pinsker, Michael	(LICS) Smooth approximations and CSPs over finitely bounded homogeneous structures
Pinsky, Sylvan	(GuttmanFest) Joshua Guttman: Pioneering Strand Spaces
Piotrowski, Bartosz	(SAT) Towards Learning Quantifier Instantiation in SMT
Pisano, Giuseppe	(GDE) Integration of Logical English and s(CASP)
Pistone, Paolo	(FSCD) On Quantitative Algebraic Higher-Order Theories (LICS) Curry and Howard Meet Borel
Piterman, Nir	(IJCAR) Actions over Core-closed Knowledge Bases (VardiFest) Modelling with Reconfigurable Communication Interfaces
Pitoni, Valentina	(NMR) Modelling Agents Roles in the Epistemic Logic L-DINF
Pitoni, Valentina	(VardiFest) An Epistemic Logic for modelling Cooperative Agents
Pitsikalis, Manolis	(ICLP) Stream Reasoning with Deadlines (KR) Stream Reasoning with Cycles
Place, Thomas	(LICS) The amazing mixed polynomial closure and its applications to two-variable first-order logic
Platzer, André	(IJCAR) Implicit Definitions with Differential Equations for KeYmaera X (System Description)
Poddar-Agrawal, Miraya	(ITP) Accelerating Verified-Compiler Development with a Verified Rewriting Engine (ITP) Automatic Test-Case Reduction in Proof Assistants: A Case Study in Coq
Pokrývka, Filip	(SAT) Weighted Model Counting with Twin-Width
Polgreen, Elizabeth	(SYNT) Beyond Counterexamples: Satisfiability and Synthesis Modulo Oracles (CAV) UCLID5: Multi-Modal Formal Modeling, Verification, and Synthesis (DSV) UCLID5: Multi-Modal Formal Modeling, Verification, and Synthesis
Polikarpova, Nadia	(SYNT) Regex+: Synthesizing Regular Expressions from Positive Examples
Poonawala, Hasan	(VeriProp) Safe Sampling-Based Planning for Stochastic Systems with Uncertain Dynamics
Popescu, Andrei	(IJCAR) Rensets and Renaming-Based Recursion for Syntax and Bindings
Popovic, Louis	(CP) Scheduling the Equipment Maintenance of an Electric Power Transmission Network using Constraint Programming (CP) Extended Abstract for : Scheduling the Equipment Maintenance of an Electric Power Transmission Network using Constraint Programming
Popovič, Alexej	(DL) On the Eve of True Explainability for OWL Ontologies: Description Logic Proofs with Evee and Evonne (XLoKR) Explaining Description Logic Entailments in Practice with Evee and Evonne
Porello, Daniele	(DL) Evaluating the Interpretability of Threshold Operators
Postol, Deena	(CSF) A Formal Model of Checked C
Potomkin, Kostiantyn	(CAV) Reachability of Koopman Linearized Systems Using Random Fourier Feature Observables and Polynomial Zonotope Refinement
Pottier, François	(ASL) Polishing a Rough Diamond: An Enhanced Separation Logic for Heap Space under Garbage Collection
Potyka, Nico	(KR) Abstract Argumentation with Markov Networks (Extended Abstract) (KR) Interpreting Neural Networks as Quantitative Argumentation Frameworks (Extended Abstract)
Poulsen, Seth	(Coq) Autogenerating Natural Language Proofs
Prasad, Siddharth	(CP) Improved Sample Complexity Bounds for Branch-and-Cut (CP) Improved Sample Complexity Bounds for Branch-and-Cut
Pratt-Hartman, Ian	(DECFOML) From Modal Logic to Fluted logic
Preiner, Mathias	(CAV) Murxla: A Modular and Highly Extensible API Fuzzer for SMT Solvers (IJCAR) Flexible Proof Production in an Industrial-Strength SMT Solver (SMT) Murxla: A Modular and Highly Extensible API Fuzzer for SMT Solvers (SMT) cvc5: A Versatile and Industrial-Strength SMT Solver (SMT) Bit-Precise Reasoning via Int-Blasting
Pressburger, Thomas	(CAV) Capture, Analyze, Diagnose: Realizability Checking of Requirements in FRET
Prince, Tephilla	(WiL) Two Dimensional Bounded Model Checking for Unbounded Client-Server Systems
Prinz, Jacob	(ITP) Deeper Shallow Embeddings
Pritz, Michael	(ICLP) A Neuro-Symbolic ASP Pipeline for Visual Question Answering
Proietti, Maurizio	(ICLP) Verifying Catamorphism-Based Contracts using Constrained Horn Clauses
Prosser, Patrick	(KR) A General Framework for Stable Roommates Problems using Answer Set Programming
Prusak, Grzegorz	(PAAR) Lazy Paramodulation in Practice
Pshenitsyn, Tikhon	(TERMGRAPH) Transformation of DPO Grammars into Hypergraph Lambek Grammars With The Conjunctive Kleene Star
Pukancová, Júlia	(FOMEO) SIVA: Simulation and visualization of the DL tableau algorithm (DL) Hybrid MHS-MXP ABox Abduction Solver: First Emprical Results (DL) An API for DL Abduction Solvers (XLoKR) An API for DL Abduction Solvers
Pukancová, Júlia	(NMR) Hybrid MHS-MXP ABox Abduction Solver: First Emprical Results
Purser, David	(LICS) The boundedness and zero isolation problems for weighted automata over nonnegative rationals (LICS) On the Skolem Problem and the Skolem Conjecture
Putot, Sylvie	(CAV) RINO: Robust INner and Outer Approximated Reachability of Neural Networks Controlled Systems (VeriProp) Uncertainty propagation in discrete-time systems using probabilistic forms
Putruele, Luciano	(CAV) Playing Against Fair Adversaries in Stochastic Games with Total Rewards
Py, Matthieu	(CP) From Crossing-Free Resolution to Max-SAT Resolution
Péchoux, Romain	(LICS) Quantum Expectation Transformers for Cost Analysis
Pérution-Kihli, Guillaume	(KR) Data Quality in Ontology-Based Data Access
Păsăreanu, Corina	(FoMLAS) VPN: Verification of Poisoning in Neural Networks (FoMLAS) Self-Correcting Neural Networks For Safe Classification (FoMLAS) A Cascade of Checkers for Run-time Certification of Local Robustness
Pąk, Karol	(ITP) Formalizing the set of primes as an alternative to the DPRM theorem (short paper)
Q
Qadeer, Shaz	(IJCAR) Reasoning About Vectors using an SMT Theory of Sequences
Qu, Weihao	(ITP) Formalizing Algorithmic Bounds in the Query Model in EasyCrypt
Quaresma, Pedro	(ThEdu) Rule Based Geometry Automated Theorem Provers (ThEdu) A Rule-Based Theorem Prover: an Introduction to Proofs at 7th Year
Quesada, Luis	(CP) Computing relaxations for the three-dimensional stable matching problem with cyclic preferences
Quimper, Claude-Guy	(CP) Constraint Acquisition Based on Solution Counting (CP) Acquiring Maps of Interrelated Conjectures on Sharp Bounds (CP) A Constraint Programming Approach to Ship Refit Project Scheduling (CP) Extended Abstract: Acquiring Maps of Interrelated Conjectures on Sharp Bounds (CP) Extended Abstract: Constraint Acquisition Based on Solution Counting
R
R, Govind	(LICS) Efficient Construction of Reversible Transducers from Regular Transducer Expressions (LICS) Abstractions for the local-time semantics of timed automata: a foundation for partial-order methods
Rabe, Markus N.	(SYNT) LTL Synthesis with Transformer Neural Networks
Raddaoui, Badran	(CP) On the Enumeration of Frequent High Utility Itemsets: A symbolic AI Approach
Rago, Antonio	(KR) Influence-Driven Explanations for Bayesian Network Classifiers (KR) Forecasting Argumentation Frameworks (KR) Explaining Causal Models with Argumentation: the Case of Bi-variate Reinforcement (XLoKR) Should counterfactual explanations always be data instances?
Rahli, Vincent	(FSCD) Constructing Unprejudiced Extensional Type Theories with Choices via Modalities
Raimondi, Franco	(WiL) Automated Logic-Based Reasoning for Analyzing Prime Video Code
Rain, Sophie	(FMBC) Automating Security Analysis of Off-Chain Protocols
Rajasekaran, Senthil	(KR) Verification and Realizability in Finite-Horizon Multiagent Systems
Rakotonirina, Itsaka	(GuttmanFest) How to Explain Security Protocols to Your Children
Ramanujam, R.	(LogTeach) Logic for computer science: starting earlier, at school
Ramsdell, John	(GuttmanFest) Cryptographic Protocol Analysis and Compilation Using CPSA and Roletran
Rand, Robert	(Coq) QuantumLib: A Library for Quantum Computing in Coq
Rapberger, Anna	(NMR) Argumentation Frameworks induced by Assumption-based Argumentation: Relating Size and Complexity (NMR) The Effect of Preferences in Abstract Argumentation Under a Claim-Centric View (KR) On Dynamics in Structured Argumentation Formalisms
Raskin, Jean-Francois	(VardiFest) Strategy synthesis for Global Window PCTL
Ratschan, Stefan	(SC^2) Non-Linear Real Arithmetic with Transcendental Function Symbols: Undecidable but Easy?
Rawson, Michael	(PAAR) The Vampire Approach to Induction (PAAR) Reuse of Introduced Symbols in Automatic Theorem Provers
Rawson, Michael	(FMBC) Automating Security Analysis of Off-Chain Protocols
Raykova, Mariana	(CSF) Locked Circuit Indistinguishability: A Notion of Security for Logic Locking
Raška, Martin	(Isabelle) Auxiliary tools for Combinatorics on Words (Isabelle) Transfer and reversal of lists (IJCAR) Binary codes that do not preserve primitivity
Rbaia, Mohamed	(ICLP) A Multi-shot ASP Encoding for the Aircraft Routing and Maintenance Planning Problem
Reale, Kristian	(ICLP) Applications of Answer Set Programming to Smart Devices and Large Scale Reasoning
Rebola Pardo, Adrian	(iPRA) Interpolants and Interference
Reeves, Joseph	(QBF) Moving Definition Variables in Quantified Boolean Formulas (Extended Abstract) (IJCAR) Preprocessing of Propagation Redundant Clauses
Refaeli, Idan	(FoMLAS) Minimal Multi-Layer Modifications of Deep Neural Networks
Refaeli, Idan	(CAV) Neural Network Robustness as a Verification Property: A Principled Case Study
Reger, Giles	(PAAR) Reuse of Introduced Symbols in Automatic Theorem Provers
Rehof, Jakob	(FSCD) Restricting tree grammars with term rewriting
Reichl, Franz-Xaver	(SAT) Pedant: A Certifying DQBF Solver
Reisert, Pascal	(CSF) How Efficient are Replay Attacks against Vote Privacy? A Formal Quantitative Analysis
Renault, Etienne	(CAV) From Spot 2.0 to Spot 2.10: What's New?
Renkin, Florian	(CAV) From Spot 2.0 to Spot 2.10: What's New?
Reutter, David	(LICS) Zigzag normalisation for associative n-categories
Reutter, David	(LICS) A Type Theory for Strictly Unital Infinity-Categories
Reynolds, Andrew	(SYNT) SyGuS-IF + SemGuS Results (CAV) Even Faster Conflicts and Lazier Reductions for String Solvers (IJCAR) Cooperating Techniques for Solving nonlinear arithmetic in the cvc5 SMT solver (System Description) (IJCAR) Reasoning About Vectors using an SMT Theory of Sequences (IJCAR) Flexible Proof Production in an Industrial-Strength SMT Solver (SMT) cvc5: A Versatile and Industrial-Strength SMT Solver (SMT) Bit-Precise Reasoning via Int-Blasting
Riazanov, Artur	(SAT) Tight Bounds for Tseitin Formulas (PC) Proof complexity of natural formulas via communication arguments
Ribeiro, Jandson S.	(KR) Kernel Contraction and the Order of Relevance
Ricca, Francesco	(ICLP) Solving Problems in PH with ASP(Q) (ICLP) Applications of Answer Set Programming to Smart Devices and Large Scale Reasoning
Rice, Alex	(LICS) A Type Theory for Strictly Unital Infinity-Categories
Rieser, Verena	(FoMLAS) Why Robust Natural Language Understanding is a Challenge
Righetti, Guendalina	(DL) Evaluating the Interpretability of Threshold Operators
Riguzzi, Fabrizio	(PLP) Statistical Statements in Probabilistic Logic Programming (PLP) Semantics for Hybrid Probabilistic Logic Programs with Function Symbols: Technical Summary (ICLP) An Iterative Fixpoint Semantics for MKNF Hybrid Knowledge Bases with Function Symbols (ICLP) Abduction in Probabilistic Logic Programs (ICLP) Exploiting Parameters Learning for Hyper-parameters Optimization in Deep Neural Networks
Riley, Heather	(ICLP) What do you really want to do? Towards a Theory of Intentions for Human-Robot Collaboration
Ringeissen, Christophe	(FSCD) Combined Hierarchical Matching: The Regular Case (UNIF) Graph-Embedded Term Rewrite Systems and Applications (A Preliminary Report)
Ringer, Talia	(Coq) Autogenerating Natural Language Proofs
Robillard, Simon	(IJCAR) Goéland : A Concurrent Tableau-Based Theorem Prover (System Description)
Rocha, Camilo	(IFIP-WG1.6) The International School on Rewriting
Rocha, Victor Hugo	(NMR) Bipolar Argumentation Frameworks with Explicit Conclusions: Connecting Argumentation and Logic Programming (KR) A Credal Least Undefined Stable Semantics for Probabilistic Logic Programs and Probabilistic Argumentation
Rodrigues Greati, Vitor	(IJCAR) Finite two-dimensional proof systems for non-finitely axiomatizable logics
Rodriguez, Andoni	(SYNT) Reactive Synthesis of LTL specifications with Rich Theories
Rodríguez, Jose Antonio	(GDE) Modeling Administrative Discretion Using Goal-Directed Answer Set Programming
Rodríguez-Núñez, Clara	(CAV) Distilling Constraints in Zero-Knowledge Protocols (IJCAR) Using Automated Reasoning Techniques for Enhancing the Efficiency and Security of (Ethereum) Smart Contracts
Roland, Valentin	(SAT) Proofs for Propositional Model Counting
Romao, Licio	(VeriProp) Safe Sampling-Based Planning for Stochastic Systems with Uncertain Dynamics
Romero, Javier	(ASPOCP) On the generalization of learnt constraints in ASP solving for temporal domains (ASPOCP) plingo: A system for probabilistic reasoning in clingo based on lpmln
Román, Mario	(LICS) Monoidal Streams for Dataflow Programming
Rondogiannis, Panos	(ICLP) Strong Equivalence of Logic Programs with Ordered Disjunction: a Logical Perspective
Rosain, Johann	(IJCAR) Goéland : A Concurrent Tableau-Based Theorem Prover (System Description)
Rossi, Francesca	(FLoC) Thinking Fast and Slow in AI
Rosulek, Mike	(CSF) A Complete Characterization of Security for Linicrypt Block Cipher Modes
Rousseau, Louis-Martin	(CP) Peel-and-Bound: Generating Stronger Relaxed Bounds with Multivalued Decision Diagrams (CP) Building a Constraint Programming Solver Guided by Machine Learning: Opportunities and Challenges (CP) Peel-and-Bound: Generating Stronger Relaxed Bounds with Multivalued Decision Diagrams
Rowe, Paul	(GuttmanFest) On Orderings in Security Models
Roy, Lawrence	(CSF) A Complete Characterization of Security for Linicrypt Block Cipher Modes
Roy, Subhajit	(SYNT) Interactive Debugging of Concurrent Programs under Relaxed Memory Models (CP) Boolean Functional Synthesis and its Applications (CAV) Proof-guided Underapproximation Widening for Bounded Model Checking (CAV) Data-Driven Invariant Learning for Probabilistic Programs
Rozier, Kristin Yvonne	(Mentoring Workshop) On Time and Space (of Humans) (NSV) MLTL Multi-Type: A Logic for Reasoning about Traces of Different Types (VardiFest) Comments from Giuseppe, Kuldeep, and Kristin
Rozowski, Wojciech	(VeriProp) Probabilistic Guarded Kleene Algebra with Tests
Ruan, Ji	(KR) A Graph Neural Network Reasoner for Game Description Language
Rubiano, Thomas	(FSCD) mwp-Analysis Improvement and Implementation: Realizing Implicit Computational Complexity
Rubin, Sasha	(KR) Private and public affairs in strategic reasoning
Rubio, Albert	(CAV) Distilling Constraints in Zero-Knowledge Protocols (IJCAR) Using Automated Reasoning Techniques for Enhancing the Efficiency and Security of (Ethereum) Smart Contracts
Rubio, Ruben	(IJCAR) Equational Unification and Matching, and Symbolic Reachability Analysis in Maude 3.2 (System Description)
Rudek, Joey	(SYNT) Regex+: Synthesizing Regular Expressions from Positive Examples
Rudich, Isaac	(CP) Peel-and-Bound: Generating Stronger Relaxed Bounds with Multivalued Decision Diagrams (CP) Peel-and-Bound: Generating Stronger Relaxed Bounds with Multivalued Decision Diagrams
Rudolph, Sebastian	(KR) The More the Worst-Case-Merrier: A Generalized Condorcet Jury Theorem for Belief Fusion (DL) Modelling Multiple Perspectives by Standpoint-Enhanced DLs (DL) AGM Revision in Description Logics Under Fixed-Domain Semantics (DL) Charting the Borderland – Decidability in Description Logics and Beyond
Rudolph, Sebastian	(NMR) Modelling Multiple Perspectives by Standpoint-Enhanced Description Logics
Rudolph, Sebastian	(NMR) AGM Revision in Description Logics Under Fixed-Domain Semantics
Rueckschloss, Kilian	(PLP) Exploiting the Full Power of Pearl's Causality in Probabilistic Logic Programming
Rueckschloss, Kilian	(ASPOCP) Correct Causal Inference in Probabilistic Logic Programming
Ruehling, Nicolas	(ASPOCP) plingo: A system for probabilistic reasoning in clingo based on lpmln
Rusch, Neea	(FSCD) mwp-Analysis Improvement and Implementation: Realizing Implicit Computational Complexity
Rusovac, Dominik	(ICLP) Rushing and Strolling among Answer Sets – Navigation Made Easy (KR) Rushing and Strolling among Answer Sets -- Navigation Made Easy (Extended Abstract) (MC) Rushing and Strolling among Answer Sets - Navigation Made Easy
Russo, Alessandra	(ASPOCP) A Semantics For Probabilistic Answer Set Programs With Incomplete Stochastic Knowledge (KR) Embed2Sym - Scalable Neuro-Symbolic Reasoning via Clustered Embeddings
Rusu, Vlad	(WPTE) Towards Corecursion Without Corecursion in Coq
Rutle, Adrian	(TERMGRAPH) Formalization and analysis of BPMN using graph transformation systems
Ryan, Peter Y A	(GuttmanFest) A Declaration of Software Independence
Ryan, Peter Y. A.	(CSF) Machine-Checked Proofs of Privacy Against Malicious Boards for Selene & Co
Ryzhikov, Vladislav	(KR) Unique Characterisability and Learnability of Temporal Instance Queries (DL) Reverse Engineering of Temporal Queries with and without LTL Ontologies: First Steps
Rønne, Peter B.	(CSF) Machine-Checked Proofs of Privacy Against Malicious Boards for Selene & Co
Rümmer, Philipp	(PAAR) Exploring Representation of Horn clauses using GNNs (SMT) An SMT-LIB Theory of Heaps
S
S, Krishna	(LICS) Efficient Construction of Reversible Transducers from Regular Transducer Expressions
S, Sheerazuddin	(WiL) Two Dimensional Bounded Model Checking for Unbounded Client-Server Systems
Saarinen, Sam	(VardiFest) Little Tricky Logic: Misconceptions in the Understanding of LTL
Sabbatini, Federico	(KR) Symbolic Knowledge Extraction from Opaque Machine Learning Predictors: GridREx & PEDRO (XLoKR) Clustering-Based Approaches for Symbolic Knowledge Extraction
Sabel, David	(WPTE) Program Equivalence in a Typed Probabilistic Call-by-Need Functional Language
Sabelfeld, Andrei	(GuttmanFest) Securing Node-RED Applications
Sabellek, Leif	(KR) Ontology-Mediated Querying on Databases of Bounded Cliquewidth
Sabuncu, Orkunt	(ASPOCP) Conflict Handling in Product Configuration using Answer Set Programming
Saeedloei, Neda	(GDE) LTL Model Checking using Coinductive Answer Set programming
Saetti, Alessandro	(KR) Online Grounding of Symbolic Planning Domains in Unknown Environments
Saffidine, Abdallah	(SAT) QBF Programming with the Modeling Language Bule (QBF) From QBF to the Dynamic Logic of Propositional Assignments and back: a computational perspective
Saivasan, Prakash	(LICS) On the Satisfiability of Context-free String Constraints with Subword Ordering
Sakaguchi, Kazuhiko	(ITP) Reflexive tactics for algebra, revisited
Sakr, Mostafa	(DL) Fine-Grained Forgetting for the Description Logic ALC
Salazar, Elmer	(ICLP) Towards Dynamic Consistency Checking in Goal-directed Predicate Answer Set Programming (GDE) LTL Model Checking using Coinductive Answer Set programming (GDE) Symbolic Reinforcement Learning Framework with Incremental Learning of Rule-based Policy
Salazar, Elmer	(ICLP) Graph-based Interpretation of Normal Logic Programs
Sallinger, Emanuel	(KR) Rule Learning over Knowledge Graphs with Genetic Logic Programming (KR) On the Relationship between Shy and Warded Datalog+/-
Salvati, Sylvain	(ICLP) Jumping Evaluation of Nested Regular Path Queries
Salvia, Josep Maria	(SAT) OptiLog v2: Model, Solve, Tune And Run
Salzer, Gernot	(LMML) MCP: Capturing Big Data by Satisfiability
Sandholm, Tuomas	(CP) Improved Sample Complexity Bounds for Branch-and-Cut (CP) Improved Sample Complexity Bounds for Branch-and-Cut
Sanfilippo, Giuseppe	(KR) Compound conditionals as random quantities and Boolean algebras
Santomauro, Mia	(GuttmanFest) Prototyping Formal Methods Tools: a Protocol Analysis Case Study
Santos, Vanda	(ThEdu) A Rule-Based Theorem Prover: an Introduction to Proofs at 7th Year
Sapiña, Julia	(GuttmanFest) Protocol Analysis with Time and Space
Sardar, Muhammad Usama	(FOMEO) Experiences on Online Teaching of Formal Methods to Systems Engineering Students (FCS) Unveiling Security through Obscurity Approach of Intel TDX Remote Attestation
Sarkar, Susmit	(WPTE) Towards a Refactoring Tool for Dependently-Typed Programs (work in progress)
Sarkis, Ralph	(LICS) Beyond Nonexpansive Operations in Quantitative Algebraic Reasoning
Sartor, Galileo	(GDE) Integration of Logical English and s(CASP)
Satoh, Ken	(NMR) Towards Legally and Ethically Correct Online HTN Planning for Data Transfer (GDE) A Query Evaluation Method for ASP with Abduction
Sattler, Christian	(HoTT/UF) A type-theoretic model structure over cubes with one connection presenting spaces
Sattler, Uli	(DL) Next Steps for ReAD: Modules for Classification Optimisation
Saue, Aurélien	(FMBC) FAT CAT: Formal Acceptance Testing of Contracts for Administering Tokens
Sauerwald, Kai	(KR) Iterated Belief Change, Computationally
Saurabh, Saket	(PCCR) TBA
Saurin, Alexis	(FSCD) Decision problems for linear logic with least and greatest fixed points (LICS) Bouncing threads for circular and non-wellfounded proofs
Sauro, Luigi	(KR) Sticky Policies in OWL2: Extending PL with fixpoints and Transitive Closure
Savateev, Yury	(DL) Reverse Engineering of Temporal Queries with and without LTL Ontologies: First Steps
Savateev, Yury	(KR) Unique Characterisability and Learnability of Temporal Instance Queries
Sayedoff, Chaked R.J.	(PERR) Regression verification of unbalanced recursive functions with multiple calls
Scaglione, Giuseppe	(SMT) NORMA: a tool for the analysis of Relay-based Railway Interlocking Systems
Scala, Enrico	(KR) On the Expressive Power of Intermediate and Conditional Effects in Temporal Planning
Scedrov, Andre	(LFMTP) Associativity or Non-Associativity, Local or Global! (IJCAR) Non-associative, non-commutative multi-modal linear logic
Scedrov, Andre	(GuttmanFest) On the Complexity of Verification of Time-Sensitive Distributed Systems
Schapira, Michael	(FoMLAS) Verification-Aided Deep Ensemble Selection
Schaub, Torsten	(ASPOCP) Conflict Handling in Product Configuration using Answer Set Programming (ASPOCP) On the generalization of learnt constraints in ASP solving for temporal domains (ASPOCP) plingo: A system for probabilistic reasoning in clingo based on lpmln (ASPOCP) ASP in Industry, here and there
Schaus, Pierre	(CP) Sequence Variables for Routing Problems (CP) Solving the Constrained Single-Row Facility Layout Problem with Decision Diagrams (CP) Extended Abstract: Sequence Variables for Routing Problems (CP) Solving the Constrained Single-Row Facility Layout Problem with Decision Diagrams (Extended Abstract)
Schekotihin, Konstantin	(ICLP) Efficient lifting of symmetry breaking constraints for complex combinatorial problems (Best Student Paper Award) (ICLP) Problem Decomposition and Multi-shot ASP Solving for Job-shop Scheduling (ICLP) Solving a Multi-resource Partial-ordering Flexible Variant of the Job-shop Scheduling Problem with Hybrid ASP (KR) Lifting Symmetry Breaking Constraints with Inductive Logic Programming
Scherl, Richard	(NMR) A situation-calculus model of Knowledge and Belief based on Thinking about Justifications
Scheucher, Manfred	(SAT) A SAT Attack on Rota's Basis Conjecture
Schidler, André	(SAT) Weighted Model Counting with Twin-Width (PCCR) Tractable Abstract Argumentation via Backdoor-Treewidth (LMML) SAT-Based Induction of Explainable Decision Trees
Schindler, Tanja	(SMT) A simple proof format for SMT
Schlaipfer, Matthias	(DSV) Achieving Verified Cloud Authorization
Schlehuber-Caissier, Philipp	(CAV) From Spot 2.0 to Spot 2.10: What's New?
Schleitzer, Agnes	(SAT) Classes of Hard Formulas for QBF Resolution
Schmellenkamp, Marko	(FOMEO) Teaching Formal Languages with Iltis - A Preview
Schmid, Todd	(VeriProp) Probabilistic Guarded Kleene Algebra with Tests
Schmidt, Nicolas	(CP) Nucleus-Satellites Systems of OMDDs for Reducing the Size of Compiled Forms
Schmidt, Renate	(ARQNL) Advances and Challenges in the Development and Application of Forgetting Tools (DL) Fine-Grained Forgetting for the Description Logic ALC (DL) Knowledge Extraction Based on Forgetting and Subontology Generation
Schmidt-Schauss, Manfred	(FSCD) Nominal Anti-Unification with Atom-Variables (UNIF) Nominal Anti-Unification of Letrec-Expressions (WPTE) Program Equivalence in a Typed Probabilistic Call-by-Need Functional Language
Schmitt, Frederik	(SYNT) LTL Synthesis with Transformer Neural Networks
Schmitz, Guido	(GuttmanFest) A Tutorial-Style Introduction to DY*
Schneider, Steve	(GuttmanFest) A Declaration of Software Independence
Schneidewind, Clara	(FCS) A Preview to HoRStify: Sound Security Analysis of Smart Contracts
Schoepe, Daniel	(WiL) Automated Logic-Based Reasoning for Analyzing Prime Video Code
Scholl, Christoph	(SAT) Quantifier Elimination in Stochastic Boolean Satisfiability
Schröder, Lutz	(FSCD) Stateful Structural Operational Semantics (LICS) Graded Monads and Behavioural Equivalence Games
Schröer, Philipp	(VeriProp) A Quantitative Verification Infrastructure
Schulz, Stephan	(PAAR) Empirical Properties of Term Orderings for Superposition
Schulze, Lukas	(KR) Ontology-Mediated Querying on Databases of Bounded Cliquewidth
Schumann, Johann	(CAV) Capture, Analyze, Diagnose: Realizability Checking of Requirements in FRET
Schurr, Hans-Jörg	(PAAR) Optimal Strategy Schedules for Everyone
Schutt, Andreas	(CP) Explaining Propagation for Gini and Spread with Variable Mean (CP) Explaining Propagation for Gini and Spread with Variable Mean (Extended Abstract)
Schwarz, Simon	(PAAR) Exploring Partial Models with SCL
Schwarzentruber, Francois	(KR) Epistemic Actions: Comparing Multi-agent Belief Bases with Action Models (FOMEO) Prooffold: a prototype for displaying structured proofs (FOMEO) Tableaunoir: an online blackboard for teaching formal methods and making slides
Schweitzer, Pascal	(LICS) Choiceless Polynomial Time with Witnessed Symmetric Choice
Schwentick, Thomas	(LogTeach) Teaching logic to CS undergraduates
Schwind, Nicolas	(ICLP) On Paraconsistent Belief Revision: the Case of Priest’s Logic of Paradox (KR) On Paraconsistent Belief Revision in LP (Extended Abstract) (KR) Region-Based Merging of Open-Domain Terminological Knowledge (KR) On the Representation of Darwiche and Pearl’s Epistemic States for Iterated Belief Revision
Schürmann, Carsten	(GuttmanFest) Security Protocols as Choreographies
Schürmann, Carsten	(GuttmanFest) A Declaration of Software Independence
Scott, Joseph	(SMT) Goose: A Meta Solver for Deep Neural Network Verification
Sebastiani, Roberto	(SMT) Panel discussion "SMT: Past, Present and Future"
Seidl, Martina	(PAAR) QuAPI: Adding Assumptions to Non-Assuming SAT & QBF Solvers
Seiller, Thomas	(FSCD) mwp-Analysis Improvement and Implementation: Realizing Implicit Computational Complexity
Serafini, Luciano	(PLP) On Projectivity in Markov Logic Networks (KR) Online Grounding of Symbolic Planning Domains in Unknown Environments
Serebrenik, Alexander	(Coq) Coq Community Survey 2022: Summary of Results
Seshia, Sanjit A.	(CAV) UCLID5: Multi-Modal Formal Modeling, Verification, and Synthesis
Sewell, Thomas	(ITP) Candle: A Verified Implementation of HOL Light
Sezgin, Meliha	(KR) A Conditional Perspective for Reasoning, Revision and Relevance
Sferrazza, Stefano	(ICLP) MV-Datalog+/-: Effective Rule-based Reasoning with Uncertain Observations (Best Paper Award)
Sha, Harry	(SAT) A generalization of the Satisfiability Coding Lemma and its applications
Shachnai, Hadas	(PCCR) Parameterized Approximations and CSPs
Shah, Nihil	(LICS) The Pebble-Relation Comonad in Finite Model Theory
Shahen, Jonathan	(CSF) Locked Circuit Indistinguishability: A Notion of Security for Logic Locking
Shaker, James	(ITP) Kalas: A Verified, End-to-End Compiler for a Choreographic Language
Shankar, Natarajan	(Mentoring Workshop) How to be an Abstraction Engineer (IJCAR) The Pleasures of Proof (SMT) CDSAT for nondisjoint theories with shared predicates: arrays with abstract length
Sharif, Mahmood	(FoMLAS) Scalable Verification of GNN-based Job Schedulers
Sharma, Roshan	(ASL) Proving Logical Atomicity using Lock Invariants
Sharygina, Natasha	(CAV) SolCMC: Solidity Compiler’s Model Checker
Shen, Jun	(ASPOCP) Constrained Default Logic Programming
Shen, Yi-Dong	(KR) Learning Typed Rules over Knowledge Graphs
Sheng, Ying	(IJCAR) Reasoning About Vectors using an SMT Theory of Sequences (SMT) cvc5: A Versatile and Industrial-Strength SMT Solver
Sherkhonov, Evgeny	(KR) Rule Learning over Knowledge Graphs with Genetic Logic Programming
Shindo, Hikaru	(KR) Sum-Product Loop Programming: From Probabilistic Circuits to Loop Programming
Shinnar, Avraham	(ITP) Formalization of a Stochastic Approximation Theorem
Shintani, Kiraku	(FSCD) Compositional Confluence Criteria
Shirmohammadi, Mahsa	(LICS) Identity testing for radical expressions
Shukla, Ankit	(ICLP) ApproxASP – A Scalable Approximate Answer Set Counter
Shukla, Sandeep	(VardiFest) A Short Talk Proposal for the VardiFest "On the Not So Unusual Effectiveness of Logic"
Siber, Julian	(CAV) Explaining Hyperproperty Violations
Siegel, Abigail	(GuttmanFest) Prototyping Formal Methods Tools: a Protocol Analysis Case Study
Sighireanu, Mihaela	(ASL) Deciding Separation Logic with Heap Lists (ASL) Report on SL-COMP
Silva, Alexandra	(Mentoring Workshop) How to Give a Good (Research) Talk (VeriProp) Deterministic stream-sampling for probabilistic programming: semantics and verification (VeriProp) Probabilistic Guarded Kleene Algebra with Tests
Simard, Vanessa	(CP) A Constraint Programming Approach to Ship Refit Project Scheduling
Simkus, Mantas	(DL) Pointwise Circumscription in Description Logics
Simmons, Robert	(LFMTP) Language Minimalism and Logical Frameworks
Simon, Pierre	(LICS) Model Checking on Interpretations of Classes of Bounded Local Cliquewidth
Simonin, Olivier	(CP) Solving the Non-Crossing MAPF for non point-sized robots
Simonov, Kirill	(SAT) Weighted Model Counting with Twin-Width
Singerman, Eli	(VardiFest) Moshe Vardi and Intel Corporation: Long and Fruitful Collaboration
Singh, Arambam James	(CP) Trajectory Optimization for Safe Navigation in Maritime Traffic Using Historical Data
Singh, Gagandeep	(CAV) Shared Certificates for Neural Network Verification (FoMLAS) Scalable Verification of GNN-based Job Schedulers
Singh, Lavanya	(Isabelle) Automating Kantian Ethics in Isabelle: A Case Study
Singleton, Joseph	(NMR) Truth-Tracking with Non-Expert Information Sources (KR) Who’s the Expert? On Multi-source Belief Change
Sinha, Arunesh	(CP) Trajectory Optimization for Safe Navigation in Maritime Traffic Using Historical Data
Skambath, Malte	(SAT) On the Parallel Parameterized Complexity of MaxSAT Variants
Skryagin, Arseny	(KR) Neural-Probabilistic Answer Set Programming
Slivovsky, Friedrich	(SAT) Quantified CDCL with Universal Resolution (SAT) Pedant: A Certifying DQBF Solver (QBF) QBF Solvers and their Proof Systems (PC) QBF Solvers and their Proof Systems (PCCR) Towards Tractable QSAT for Structural Parameters Below Treewidth (MC) A Faster Algorithm for Propositional Model Counting Parameterized by Incidence Treewidth
Smail-Tabbone, Malika	(ASPOCP) Automatic Synthesis of Boolean Networks from Biological Knowledge and Data
Smirnov, Pavel	(SAT) Improvements to the Implicit Hitting Set Approach to Pseudo-Boolean Optimization
Smirnov, Petr	(SAT) Tight Bounds for Tseitin Formulas
Smith, Douglas	(SYNT) Inferring Environment Assumptions in Model Refinement
Smith, William	(VeriProp) Deterministic stream-sampling for probabilistic programming: semantics and verification
Smolka, Gert	(Coq) A Coq Library for Mechanised First-Order Logic
Sobocinski, Pawel	(WiL) Monoidal Width -- Extended Abstract
Sochański, Michał	(IJCAR) Synthetic tableaux: minimal tableau search heuristics
Sojakova, Kristina	(FMBC) FAT CAT: Formal Acceptance Testing of Contracts for Administering Tokens (LICS) Syllepsis in Homotopy Type Theory (HoTT/UF) TBA
Solberg, Morten Rotvold	(CSF) Machine-Checked Proofs of Privacy Against Malicious Boards for Selene & Co
Solnon, Christine	(CP) Solving the Non-Crossing MAPF for non point-sized robots
Somayyajula, Siva	(TLLA-LINEARITY) Parametric Chu Translation (FSCD) Type-Based Termination for Futures
Somenzi, Fabio	(VardiFest) An Automata-Theoretic Approach to Model-Free Reinforcement Learning
Son, Tran Cao	(ICLP) On Model Reconciliation: How to Reconcile When Robot Does not Know Human’s Model? (ICLP) Model Reconciliation in Logic Programs
Song, Fu	(CAV) PoS4MPC: Automated Security Policy Synthesis for Secure Multi-Party Computation
Song, Xidan	(FoMLAS) Counter-Example Guided Neural Network Compression Refinement (CEG4N)
Sood, Gaurav	(SAT) QBF Merge Resolution is powerful but unnatural
Soos, Mate	(CP) On Quantitative Testing of Samplers (POS) Combining CDCL, Gauss-Jordan Elimination, and Proof Generation (PDAR) Leveraging GPUs for Parallel SAT Solving (MC) Designing Samplers is Easy: The Boon of Testers
Soutchanski, Mikhail	(VardiFest) Towards Combination of Logic and Calculus for Near-Optimal Planning in Relational Hybrid Systems (CHANGE) Tutorial: Hybrid Temporal Situation Calculus for Planning with Continuous Processes: Semantics (CHANGE) Tutorial: Hybrid Temporal Situation Calculus for Planning with Continuous Processes: Semantics
Souza, Marlo	(KR) Hyperintensional Partial Meet Contractions
Spaan, Matthijs T. J.	(CAV) Abstraction-Refinement for Hierarchical Probabilistic Models
Speight, Sam	(HoTT/UF) Groupoidal Realizability: Formalizing the Topological BHK Interpretation
Spitters, Bas	(FMBC) Finding smart contract vulnerabilities with ConCert's property-based testing framework
Sprecher, Christian	(CAV) Shared Certificates for Neural Network Verification
Sprenger, Christoph	(CSF) N-Tube: Formally Verified Secure Bandwidth Reservation in Path-Aware Internet Architectures
Sprunger, David	(FSCD) Rewriting for monoidal closed categories
Sridharan, Mohan	(ICLP) What do you really want to do? Towards a Theory of Intentions for Human-Robot Collaboration (NMR) There and Back Again: Combining Nonmonotonic Logical Reasoning and Deep Learning on an Assistive Robot
Srivas, Mandayam	(FMBC) A Domain Specific Language for Testing Consensus Implementations
Srivastava, Siddharth	(KR) Discovering User-Interpretable Capabilities of Black-Box Planning Agents
Srivathsan, B	(LICS) Abstractions for the local-time semantics of timed automata: a foundation for partial-order methods
Stammer, Wolfgang	(KR) Neural-Probabilistic Answer Set Programming
Stark, Philip	(GuttmanFest) A Declaration of Software Independence
Starosta, Štěpán	(Isabelle) Auxiliary tools for Combinatorics on Words (IJCAR) Binary codes that do not preserve primitivity
Staton, Sam	(LICS) Concrete categories and higher-order recursion (with applications including probability, differentiability, and full abstraction)
Steen, Alexander	(ARQNL) Solving QMLTP Problems by Translation to Higher-order Logic (PAAR) Automated Reasoning in Non-classical Logics in the TPTP World (PAAR) An Extensible Logic Embedding Tool for Lightweight Non-Classical Reasoning (PAAR) short COST action EuroProofNet introduction
Steinmetz, Marcel	(DL) Expressivity of Planning with Horn Description Logic Ontologies (Extended Abstract)
Stepanova, Daria	(ICLP) Large-Neighbourhood Search for ASP Optimisation (KR) ALASPO: An Adaptive Large-Neighbourhood ASP Optimiser
Sterling, Jonathan	(FSCD) Sheaf semantics of termination-insensitive noninterference
Stevens, Brett	(KR) Solving Lam's Problem via SAT and Isomorph-Free Exhaustive Generation
Stevens, Lukas	(Isabelle) A Linter for Isabelle: Implementation and Evaluation
Stewart, Robert	(FoMLAS) Differentiable Logics for Neural Network Verification
Stoelinga, Marielle	(CAV) Sampling-Based Verification of CTMCs with Uncertain Rates (VeriProp) Safe Sampling-Based Planning for Stochastic Systems with Uncertain Dynamics
Stoilkovska, Ilina	(Mentoring Workshop) From PhD to industry: A recent graduate’s perspective (Mentoring Workshop) From PhD to industry: A recent graduate’s perspective (FRIDA) Eliminating Message Counters in Threshold Automata (WiL) Automated Logic-Based Reasoning for Analyzing Prime Video Code
Stoughton, Alley	(ITP) Formalizing Algorithmic Bounds in the Query Model in EasyCrypt
Straccia, Umberto	(NMR) Defeasible reasoning in RDFS (KR) A General Framework for Modelling Conditional Reasoning - Preliminary Report (KR) A Minimal Deductive System for RDFS with Negative Statements
Straccia, Umberto	(DL) Defeasible reasoning in RDFS
Strass, Hannes	(DL) Modelling Multiple Perspectives by Standpoint-Enhanced DLs
Strass, Hannes	(NMR) Modelling Multiple Perspectives by Standpoint-Enhanced Description Logics
Strasser, Christian	(NMR) Abductive Reasoning with Sequent-Based Argumentation (Extended Abstract)
Strauch, Klaus	(ASPOCP) On the generalization of learnt constraints in ASP solving for temporal domains
Straßburger, Lutz	(FSCD) Normalization without syntax (FSCD) A Graphical Proof Theory of Logical Time
Strecker, Martin	(GDE) Automating Defeasible Reasoning in Law with Answer Set Programming
Stuckey, Peter J.	(CP) Explaining Propagation for Gini and Spread with Variable Mean (CP) Explaining Propagation for Gini and Spread with Variable Mean (Extended Abstract) (LMML) Building Optimal Decision Trees
Ståhlberg, Simon	(KR) Learning generalized policies without supervision using GNNs
Stöger, Bernhard	(Isabelle) Towards Accessible Formal Mathematics with ISAC and Isabelle/VSCode
Subercaseaux, Bernardo	(SAT) The packing chromatic number of the infinite square grid is at least 14 (LMML) The Exciting Theory of Formal Explanations
Suda, Martin	(PAAR) Reuse of Introduced Symbols in Automatic Theorem Provers (IJCAR) Vampire Getting Noisy: Will Random Bits Help Conquer Chaos? (System Description)
Suenaga, Kohei	(CAV) The Lattice-Theoretic Essence of Property Directed Reachability Analysis (CAV) Oblivious Online Monitoring for Safety LTL Specification via Fully Homomorphic Encryption
Summers, Alexander J.	(CAV) Sound Automation of Magic Wands
Sun, Jun	(CAV) Verifying Neural Networks Against Backdoor Attacks
Sun, Wanyun	(ASL) Deciding Separation Logic with Heap Lists
Sun, Yan	(CP) DUELMIPs: Jointly Optimizing Software Defined Network Functionality and Security
Sun, Youcheng	(FoMLAS) VPN: Verification of Poisoning in Neural Networks
Sutcliffe, Geoff	(ARQNL) Solving QMLTP Problems by Translation to Higher-order Logic (PAAR) Automated Reasoning in Non-classical Logics in the TPTP World (PAAR) The Logic Languages of the TPTP World and Proofs and Models in the TPTP World
Syverson, Paul	(GuttmanFest) Principles of Remote Sattestation
Szeider, Stefan	(CP) CSP Beyond Tractable Constraint Languages (SAT) Weighted Model Counting with Twin-Width (SAT) A SAT Attack on Rota's Basis Conjecture (PC) Are Hitting Formulas Hard for Resolution? (PCCR) Tractable Abstract Argumentation via Backdoor-Treewidth (PCCR) The Parameterized Complexity of SAT (MC) A Faster Algorithm for Propositional Model Counting Parameterized by Incidence Treewidth
Sághi, György	(WPTE) A Machine-Checked Formalisation of Erlang Modules
Sánchez, César	(SYNT) Reactive Synthesis of LTL specifications with Rich Theories (FMBC) Multi: a Formal Playground for Smart Multi-contract interaction
T
Tacchella, Alberto	(SMT) NORMA: a tool for the analysis of Relay-based Railway Interlocking Systems
Tack, Guido	(CP) Explaining Propagation for Gini and Spread with Variable Mean (CP) Explaining Propagation for Gini and Spread with Variable Mean (Extended Abstract)
Tadey, Sam	(NMR) Trust Graphs for Belief Revision: Framework and Implementation
Takisaka, Toru	(VeriProp) Widest Paths and Global Propagation in Bounded Value Iteration for Stochastic Games
Talcott, Carolyn	(IJCAR) Equational Unification and Matching, and Symbolic Reachability Analysis in Maude 3.2 (System Description)
Talcott, Carolyn	(GuttmanFest) On the Complexity of Verification of Time-Sensitive Distributed Systems
Talpin, Jean-Pierre	(CAV) End-to-end Mechanised Proof of an eBPF Virtual Machine for Microcontrollers
Tamaki, Hisao	(MC) Heuristic computation of exact treewidth - some improvements and more experimental evaluations
Tammet, Tanel	(GDE) First order logic and commonsense reasoning: a path less travelled (IJCAR) GK: Implementing Full First Order Default Logic for Commonsense Reasoning (System Description)
Tan, Li-Yang	(SAT) A generalization of the Satisfiability Coding Lemma and its applications
Tan, Yong Kiam	(IJCAR) Implicit Definitions with Differential Equations for KeYmaera X (System Description)
Tantau, Till	(SAT) On the Parallel Parameterized Complexity of MaxSAT Variants
Tarau, Paul	(ICLP) Abductive Reasoning in Intuitionistic Propositional Logic via Theorem Synthesis (ICLP) A Gaze into the Internal Logic of Graph Neural Networks, with Logic
Tarzariol, Alice	(ICLP) Efficient lifting of symmetry breaking constraints for complex combinatorial problems (Best Student Paper Award) (KR) Lifting Symmetry Breaking Constraints with Inductive Logic Programming
Tassel, Pierre	(ICLP) A Multi-shot ASP Encoding for the Aircraft Routing and Maintenance Planning Problem
Tattersall, Daniel	(WiL) Automated Logic-Based Reasoning for Analyzing Prime Video Code
Teixeira, Pedro	(ThEdu) Rule Based Geometry Automated Theorem Provers
Tejfel, Máté	(WPTE) Refactoring Steps for P4 (work in progress)
Tekriwal, Mohit	(ITP) Dandelion: Certified Approximations of Elementary Functions
Teles, Joana	(ThEdu) A Rule-Based Theorem Prover: an Introduction to Proofs at 7th Year
Tena Cucala, David	(KR) Faithful Approaches to Rule Learning
Terauchi, Tachio	(FSCD) On Lookaheads in Regular Expressions with Backreferences
Ternovska, Eugenia	(VardiFest) Towards Algebraic Techniques for Descriptive Complexity
Teuber, Samuel	(MC) Quantifying Software Reliability via Model-Counting
Thakkar, Aalok	(SYNT) Complexity of Relational Query Synthesis
Theseider Dupré, Daniele	(ICLP) An ASP approach for reasoning on neural networks under a finitely many-valued semantics for weighted conditional knowledge bases (KR) A conditional, a fuzzy and a probabilistic interpretation of self-organising maps (Abstract) (DL) Reasoning about actions with EL ontologies in a temporal action theory (Extended Abstract)
Thibault, Jérémy	(CSF) SecurePtrs: Proving Secure Compilation Using Data-Flow Back-Translation and Turn-Taking Simulation
Thiemann, René	(Isabelle) From P != NP to monotone circuits of super-polynomial size (WST) CeTA — Efficient Certification of Termination Proofs (WST) CeTA – A certifier for termCOMP 2022
Thomas, Philip	(ITP) Mechanizing Soundness of Off-Policy Evaluation
Thomazo, Michaël	(KR) Normalisations of Existential Rules: Not so Innocuous! (KR) Counting queries over ELHI⊥ ontologies (KR) Revisiting Semiring Provenance for Datalog (DL) Complexity Landscape for Counting Queries (Extended abstract)
Thompson, Simon	(WPTE) Towards a Refactoring Tool for Dependently-Typed Programs (work in progress)
Tian, Jiaxu	(CAV) Trainify: A CEGAR-Driven Training and Verification Framework for Verifiable Deep Reinforcement Learning
Tiihonen, Mikko	(GDE) Embedding s(CASP) in Prolog
Timany, Amin	(CSF) Proving full-system security properties under multiple attacker models on capability machines
Tinelli, Cesare	(CAV) Even Faster Conflicts and Lazier Reductions for String Solvers (IJCAR) Cooperating Techniques for Solving nonlinear arithmetic in the cvc5 SMT solver (System Description) (IJCAR) Reasoning About Vectors using an SMT Theory of Sequences (IJCAR) Flexible Proof Production in an Industrial-Strength SMT Solver (SMT) cvc5: A Versatile and Industrial-Strength SMT Solver (SMT) Bit-Precise Reasoning via Int-Blasting (SMT) Panel discussion "SMT: Past, Present and Future" (SMT) SMT-Lib Update Report
Tirtarasa, Satyadharma	(DL) A new dimension to generalization: computing temporal EL concepts from positive examples (Extended Abstract)
Tiu, Alwen	(FSCD) A Methodology for Designing Proof Search Calculi for Non-Classical Logics (CSF) Is Eve nearby? Analysing protocols under the distant-attacker assumption
Toman, David	(REAI) Referring Expressions in Artificial Intelligence and Knowledge Representation Systems (Tutorial at KR-22 https://cs.uwaterloo.ca/~david/kr22/) (REAI) Referring Expressions in Artificial Intelligence and Knowledge Representation Systems (Tutorial at KR-22) (DL) Accessing Document Data Sources using Referring Expression Types
Tomczyk, Agata	(IJCAR) Synthetic tableaux: minimal tableau search heuristics
Tonetta, Stefano	(SMT) The VMT-LIB Language and Tools (VardiFest) The Safety Fragment of LTL
Toni, Francesca	(KR) Influence-Driven Explanations for Bayesian Network Classifiers (KR) Forecasting Argumentation Frameworks (KR) Explaining Causal Models with Argumentation: the Case of Bi-variate Reinforcement (XLoKR) On interactive explanations as reasoning (XLoKR) Should counterfactual explanations always be data instances?
Torres Montiel, Eduard	(SAT) OptiLog v2: Model, Solve, Tune And Run
Torstensson, Olle	(Isabelle) Oracle Integration of Floating-Point Solvers with Isabelle
Toruńczyk, Szymon	(LICS) Model Checking on Interpretations of Classes of Bounded Local Cliquewidth (LICS) Stable graphs of bounded twin-width (LICS) Treelike decompositions for transductions of sparse graphs
Totis, Pietro	(ICLP) Efficient Knowledge Compilation Beyond Weighted Model Counting (Best Student Paper Award)
Tourret, Sophie	(DL) Connection-minimal Abduction in EL via translation to FOL (Extended Abstract) (IJCAR) Connection-minimal Abduction in EL via translation to FOL
Tourret, Sophie	(NMR) Connection-Minimal Abduction in EL via Translation to FOL
Trager, Barry	(ITP) Formalization of a Stochastic Approximation Theorem
Traversié, Thomas	(LFMTP) An Implementation of Set Theory with Pointed Graphs in Dedukti
Traverso, Paolo	(KR) Online Grounding of Symbolic Planning Domains in Unknown Environments
Trieu, Alix	(CSF) Proving full-system security properties under multiple attacker models on capability machines
Tripakis, Stavros	(CSF) Mapping Synthesis for Hyperproperties
Tripakis, Stavros	(CSF) Adversarial Robustness Verification and Attack Synthesis in Stochastic Systems
Tripunitara, Mahesh	(CSF) Locked Circuit Indistinguishability: A Notion of Security for Logic Locking
Tristan, Jean-Baptiste	(LICS) Computable PAC Learning of Continuous Features
Trivedi, Ashutosh	(VardiFest) An Automata-Theoretic Approach to Model-Free Reinforcement Learning
Trivedi, Nitesh	(CAV) Data-Driven Invariant Learning for Probabilistic Programs
Troubitsyna, Elena	(CP) Optimized Code Generation against Power Side Channels
Trujillo-Rasua, Rolando	(CSF) Is Eve nearby? Analysing protocols under the distant-attacker assumption
Truszczynski, Mirek	(ICLP) Solving Problems in PH with ASP(Q)
Trösser, Fulya	(CP) Structured Set Variable Domains in Bayesian Network Structure Learning
Tsampas, Stelios	(FSCD) Stateful Structural Operational Semantics
Tsimbolynets, Vitalii	(FOMEO) Visualization of structural operational semantics over programs of simple imperative language.
Tsoupidi, Rodothea Myrsini	(CP) Optimized Code Generation against Power Side Channels
Tsukada, Takeshi	(LICS) Linear-Algebraic Models of Linear Logic as Categories of Modules over Sigma-Semirings
Tu, Kuan-Hua	(SAT) Quantifier Elimination in Stochastic Boolean Satisfiability
Tuckey, David	(ASPOCP) A Semantics For Probabilistic Answer Set Programs With Incomplete Stochastic Knowledge
Tumova, Jana	(NSV) Motion planning with temporal logic constraints and preferences
Turhan, Anni-Yasmin	(NMR) Rational defeasible subsumption in DLs with nested quantifiers: the case of ELI_⊥ (DL) Efficient TBox Reasoning with Value Restrictions using the FL0wer Reasoner (Extended Abstract) (DL) A new dimension to generalization: computing temporal EL concepts from positive examples (Extended Abstract)
Turhan, Anni-Yasmin	(DL) Rational defeasible subsumption in DLs with nested quantifiers: the case of ELI_⊥
Turrini, Andrea	(CAV) Divide-and-Conquer Determinization of Büchi Automata based on SCC Decomposition
Tzevelekos, Nikos	(PERR) From Bounded Checking to Verification of Equivalence via Symbolic Up-to Techniques (Extended Abstract)
Tóth, Richard	(FOMEO) First-Order Logic Workbook
Törmá, Seppo	(ICLP) Building Information Modeling using Constraint Logic Programming
U
Uemura, Taichi	(HoTT/UF) Internal languages of diagrams of ∞-toposes
Ulbricht, Markus	(NMR) Argumentation Frameworks induced by Assumption-based Argumentation: Relating Size and Complexity (KR) Defining Defense and Defeat in Abstract Argumentation From Scratch -- A Generalizing Approach (KR) On Dynamics in Structured Argumentation Formalisms (KR) Rediscovering Argumentation Principles Utilizing Collective Attacks
Ulrich-Oltean, Felix	(CP) Selecting SAT Encodings for Pseudo-Boolean and Linear Integer Constraints (CP) Selecting SAT Encodings for Pseudo-Boolean and Linear Integer Constraints
Uncu, Ali Kemal	(SC^2) NP: SMT-Solving Combinatorial Inequalities
Urabe, Natsuki	(CAV) The Lattice-Theoretic Essence of Property Directed Reachability Analysis
Urban, Caterina	(Mentoring Workshop) Welcome
Urban, Josef	(ITP) The Isabelle ENIGMA (FMBC) Proofgold: Blockchain for Formal Methods (PAAR) Training ENIGMAs, CoPs, and other thinking creatures (IJCAR) Guiding an Automated Theorem Prover with Neural Rewriting
Urbani, Jacopo	(KR) Chasing streams with existential rules
Urbat, Henning	(FSCD) Stateful Structural Operational Semantics
Urbańczyk, Mateusz	(DL) Comonadic Semantics for Description Logics Games
Uskuplu, Elif	(HoTT/UF) An Experiment with 2LTT Features in Agda
Usman, Muhammad	(FoMLAS) VPN: Verification of Poisoning in Neural Networks
V
V. Deshmukh, Jyotirmoy	(NSV) Combining learning-based methods and temporal logic specifications for designing controllers for unknown environments
Vaginay, Athénaïs	(ASPOCP) Automatic Synthesis of Boolean Networks from Biological Knowledge and Data
Vahdati, Sahar	(KR) Rule Learning over Knowledge Graphs with Genetic Logic Programming
Vaillant, Pascal	(DL) Category-based Semantics for the Description Logic ALC and Reasoning
Vajjha, Koundinya	(ITP) Formalization of a Stochastic Approximation Theorem
Vale, Deivid	(WST) Tuple Interpretations and Applications to Higher-Order Runtime Complexity
van der Weide, Niels	(LICS) Semantics for two-dimensional type theory (HoTT/UF) Semantics for two-dimensional type theory
Van Hentenryck, Pascal	(CP) Sequence Variables for Routing Problems (CP) Extended Abstract: Sequence Variables for Routing Problems
van Hoeve, Willem-Jan	(CP) From Cliques to Colorings and Back Again (CP) Heuristics for MDD Propagation in Haddock
Van Hoeve, Willem-Jan	(CP) MDD-Based Constraint Programming in Haddock
Van Horn, David	(CSF) A Formal Model of Checked C
Van Oostrom, Vincent	(TERMGRAPH) Greedily Decomposing Proof Terms for String Rewriting into Multistep Derivations by Topological Multisorting (IWC) Confluence by Higher-Order Multi--One Critical pairs with an application to the Functional Machine Calculus (IWC) Uniform Completeness
Van Strydonck, Thomas	(CSF) Proving full-system security properties under multiple attacker models on capability machines
Vanbesien, Linde	(ICLP) Analyzing Semantics of Aggregate Answer Set Programming Using Approximation Fixpoint Theory
Vanoni, Gabriele	(LICS) Reasonable Space for the Lambda-Calculus, Logarithmically
Varanasi, Sarat Chandra	(GDE) Unmanned Aerial Vehicle compliance checking using Goal-Directed Answer Set Programming (GDE) LTL Model Checking using Coinductive Answer Set programming
Vardi, Moshe	(KR) Private and public affairs in strategic reasoning (CAV) Divide-and-Conquer Determinization of Büchi Automata based on SCC Decomposition (LogTeach) How to be an ethical computer scientist (Joint with Vardi Fest)
Vardi, Moshe Y.	(KR) Verification and Realizability in Finite-Horizon Multiagent Systems (VardiFest) How to be an ethical computer scientist
Varzinczak, Ivan	(NMR) Situated Conditionals - A Brief Introduction (KR) Region-Based Merging of Open-Domain Terminological Knowledge
Vasileiou, Stylianos Loukas	(ICLP) Model Reconciliation in Logic Programs (KR) Towards a Logical Account for Human-Aware Explanation Generation in Model Reconciliation Problems
Vechev, Martin	(CAV) Shared Certificates for Neural Network Verification
Vehlken, Fabian	(FOMEO) Iltis: Teaching Logic in the Web
Vella, Lucas	(SMT) On Satisfiability of Polynomial Equations over Large Prime Fields
Venema, Yde	(LICS) Size measures and alphabetic equivalence in the mu-calculus
Vergain, Baptiste	(SC^2) Decidability of difference logics with unary predicates
Verhaeghe, Hélène	(CP) Doctoral Research Award (CP) Opening
Verma, Aakanksha	(SYNT) Interactive Debugging of Concurrent Programs under Relaxed Memory Models
Verma, Pulkit	(KR) Discovering User-Interpretable Capabilities of Black-Box Planning Agents (KR) Data Efficient Paradigms for Personalized Assessment of Taskable AI Systems
Verreet, Victor	(ICLP) Inference and Learning with Model Uncertainty in Probabilistic Logic Programs
Verrev, Martin	(GDE) First order logic and commonsense reasoning: a path less travelled
Veshchezerova, Margarita	(FSCD) Addition and differentiation of ZX-diagrams
Vezzosi, Andrea	(LICS) Greatest HITs: Higher inductive types in coinductive definitions via induction under clocks
Vianu, Victor	(VardiFest) Fixpoint Logics, Relational Machines, and Computational Complexity
Vicary, Jamie	(LICS) A Type Theory for Strictly Unital Infinity-Categories (LICS) Zigzag normalisation for associative n-categories
Viegas Damásio, Carlos	(XLoKR) Modular Provenance in Multi-Context Systems
Viganò, Luca	(CSF) Privacy as Reachability (FCS) Automatic Fair Exchanges
Vignudelli, Valeria	(LICS) Beyond Nonexpansive Operations in Quantitative Algebraic Reasoning
Villadsen, Jørgen	(Isabelle) Lessons of Teaching Formal Methods with Isabelle (Isabelle) On Axiomatic Systems for Classical Propositional Logic (LogTeach) Teaching Logic for Computer Science Students: Proof Assistants and Related Tools (FOMEO) Formal Methods Online: Sequent Calculus Verifier (SeCaV) (ThEdu) On Exams with the Isabelle Proof Assistant
Villaret, Mateu	(CP) Plotting: A Planning Problem With Complex Transitions
Villata, Serena	(NMR) Fallacious arguments: the place where Knowledge Representation and Argument Mining meet each other
Villemaire, Roger	(LogTeach) Undergraduate Logic Teaching in Computing: Why, What, How?
Vin, Eric	(CAV) Randomized Synthesis for Diversity and Cost Constraints with Control Improvisation (MC) Randomized Synthesis for Diversity and Cost Constraints with Control Improvisation
Vinogradova, Polina	(FMBC) Designing EUTxO smart contracts as communicating state machines: the case of simulating accounts (FMBC) Determinism of ledger updates (FMBC) Human and machine-readable models of state machines for the Cardano ledger
Virtema, Jonni	(LICS) Temporal Team Semantics Revisited
Visentin, Andrea	(CP) Automated SAT Problem Feature Extraction using 1 Convolutional Autoencoders
Viswanathan, Arjun	(IJCAR) Flexible Proof Production in an Industrial-Strength SMT Solver
Viswanathan, Mahesh	(VardiFest) Verifying Accuracy Claims of Differential Privacy Algorithms
Vitercik, Ellen	(CP) Improved Sample Complexity Bounds for Branch-and-Cut (CP) Improved Sample Complexity Bounds for Branch-and-Cut
Viteri, Scott	(IJCAR) Flexible Proof Production in an Industrial-Strength SMT Solver
Vizel, Yakir	(DSV) Solving Constrained Horn Clauses Lazily and Incrementally
Volk, Matthias	(CAV) Sampling-Based Verification of CTMCs with Uncertain Rates
Volkova, Anastasia	(ITP) Dandelion: Certified Approximations of Elementary Functions
Vollmer, Victoria	(WiL) A Mixed Linear and Graded Logic-Extended Abstract
Voronkov, Andrei	(SYNT) Towards Synthesis in Superposition (PAAR) The Vampire Approach to Induction
Vukmirović, Petar	(ITP) Seventeen Provers under the Hammer
Vítores, Miguel	(IWC) Proving Confluence with CONFident
W
Waga, Masaki	(CAV) Oblivious Online Monitoring for Safety LTL Specification via Fully Homomorphic Encryption
Wagner, Andrew	(CSF) Adversary Safety by Construction in a Language of Cryptographic Protocols
Waldmann, Johannes	(IFIP-WG1.6) The International School on Rewriting (WST) Approximating Relative Match-Bounds (WST) Certified Matchbox
Walker, James Alfred	(CP) Selecting SAT Encodings for Pseudo-Boolean and Linear Integer Constraints (CP) Selecting SAT Encodings for Pseudo-Boolean and Linear Integer Constraints
Walkiewicz, Daniel	(CP) Modeling and Solving Parallel Machine Scheduling with Contamination Constraints in the Agricultural Industry
Wallner, Johannes P.	(NMR) Argumentation Frameworks induced by Assumption-based Argumentation: Relating Size and Complexity (KR) An Axiomatic Approach to Revising Preferences (Extended Abstract) (KR) Computing Stable Argumentative Conclusions under the Weakest-Link Principle in the ASPIC+ Framework
Wallon, Romain	(CP) On PB Encodings for Constraint Problems
Walukiewicz, Igor	(LICS) Abstractions for the local-time semantics of timed automata: a foundation for partial-order methods (LICS) Active learning for sound negotiations
Wan, Hai	(ICLP) Efficient Datalog Rewriting for Query Answering in TGD Ontologies
Wang, Chao	(CAV) Example Guided Synthesis of Linear Approximations for Neural Network Verification (CAV) Synthesizing Fair Decision Trees via Iterative Constraint Solving
Wang, Hao-Ren	(SAT) Quantifier Elimination in Stochastic Boolean Satisfiability
Wang, Huaduo	(ICLP) FOLD-RM: A Scalable and Efficient Inductive Learning Algorithm for Multi-Category Classification of Mixed Data
Wang, Huaduo	(GDE) Symbolic Reinforcement Learning Framework with Incremental Learning of Rule-based Policy
Wang, Jie	(CP) Completeness Matters: Towards Efficient Caching in Tree-based Synchronous Backtracking Search for DCOPs
Wang, Jingbo	(CAV) Synthesizing Fair Decision Trees via Iterative Constraint Solving
Wang, Kewen	(ICLP) Efficient Datalog Rewriting for Query Answering in TGD Ontologies (KR) Learning Typed Rules over Knowledge Graphs
Wang, Qinshi	(CAV) Verified Erasure Correction in Coq with MathComp and VST
Wang, Ruiwei	(CP) CNF Encodings of Binary Constraint Trees (CP) CNF Encodings of Binary Constraint Trees (Extended Abstract)
Wang, Shengyi	(ASL) Proving Logical Atomicity using Lock Invariants
Wang, Shuling	(ITP) Compositional Verification of Interacting Systems using Event Monads
Wang, Yuheng	(ICLP) Knowledge Authoring with Factual English
Wang, Zhe	(ICLP) Efficient Datalog Rewriting for Query Answering in TGD Ontologies (KR) Learning Typed Rules over Knowledge Graphs
Ward, Francis Rhys	(ASPOCP) A Casual Perspective on AI Deception
Wasowski, Andrzej	(VeriProp) Quantifying Leakage in Privacy Risk Analysis using Probabilistic Programming
Wassermann, Renata	(BCORE) Tutorial: Belief Change, Ontology Repair and Evolution (Part 1) (BCORE) Tutorial: Belief Change, Ontology Repair and Evolution (Part 2) (NMR) Repairing Ontologies via Kernel Pseudo-Contraction (KR) Hyperintensional Partial Meet Contractions
Wassermann, Renata	(DL) Repairing Ontologies via Kernel Pseudo-Contraction
Waszkiewicz, Daniel	(POS) Towards an Efficient CNF Encoding of Block Ciphers
Watanabe, Kazuki	(PERR) Compositional Approaches to Games in Model Checking
Wattez, Hugues	(CP) Aggressive Bound Descent for Constraint Optimization
Wałęga, Przemysław	(DatalogMTL) DatalogMTL (DatalogMTL) DatalogMTL
Weber, Tjark	(Isabelle) Oracle Integration of Floating-Point Solvers with Isabelle
Weddell, Grant	(DL) Accessing Document Data Sources using Referring Expression Types
Weeks, Noé	(CAV) Sound Automation of Magic Wands
Weghorn, Thilo	(CSF) N-Tube: Formally Verified Secure Bandwidth Reservation in Path-Aware Internet Architectures
Wehr, Dominik	(Coq) A Coq Library for Mechanised First-Order Logic
Weidenbach, Christoph	(PAAR) A Two-Watched Literal Scheme for First-Order Logic (PAAR) Exploring Partial Models with SCL (DL) Connection-minimal Abduction in EL via translation to FOL (Extended Abstract) (IJCAR) Connection-minimal Abduction in EL via translation to FOL (IJCAR) Semantic Relevance (IJCAR) SCL(EQ): SCL for First-Order Logic with Equality (IJCAR) An Efficient Subsumption Test Pipeline for BS(LRA) Clauses
Weidenbach, Christoph	(NMR) Connection-Minimal Abduction in EL via Translation to FOL
Weigl, Alexander	(MC) Quantifying Software Reliability via Model-Counting
Weinberger, Jonathan	(HoTT/UF) Towards Normalization of Simplicial Type Theory via Synthetic Tait Computability
Weininger, Maximilian	(FOMEO) Automata Tutor
Weitkämper, Felix	(PLP) Exploiting the Full Power of Pearl's Causality in Probabilistic Logic Programming
Welt, Michael	(DL) Concept Abduction for Description Logics
Wen, Xuejun	(CAV) Trainify: A CEGAR-Driven Training and Verification Framework for Verifiable Deep Reinforcement Learning
Wendler, Philipp	(iPRA) Interpolation and SAT-Based Model Checking Revisited: Adoption to Software Verification
Wenzel, Makarius	(Isabelle) Isabelle/VSCode and Electron/Node.js as emerging Isabelle technologies (Isabelle) Towards Accessible Formal Mathematics with ISAC and Isabelle/VSCode (ITP) Seventeen Provers under the Hammer
Wernhard, Christoph	(PAAR) Generating Compressed Combinatory Proof Structures: An Approach to Automated First-Order Theorem Proving
West, Matthew	(Coq) Autogenerating Natural Language Proofs
Whalen, Michael	(SAT) Migrating Solver State
Whiteland, Markus	(LICS) The boundedness and zero isolation problems for weighted automata over nonnegative rationals
Wielemaker, Jan	(GDE) Embedding s(CASP) in Prolog
Wijs, Anton	(PDAR) A Linear Parallel Algorithm to Compute Strong and Branching Bisimilarity
Wijsen, Jef	(ASPOCP) Computing H-Partitions in ASP and Datalog
Wilhelmi, Rüdiger	(VardiFest) Checking Legal Contracts - On a Not So Usual Application of Mechanized Logic
Wilke, Richard	(LICS) Zero-One Laws and Almost Sure Valuations of First-Order Logic in Semiring Semantics
Wille, Robert	(SAT) Towards a SAT Encoding for Quantum Circuits
Winkler, Sarah	(PAAR) On SGGS and Horn Clauses (IJCAR) CTL* model checking for data-aware dynamic systems with arithmetic
Winkler, Tobias	(CAV) Does a Program Yield the Right Distribution? Verifying Probabilistic Programs via Generating Functions
Winter, Felix	(CP) Modeling and Solving Parallel Machine Scheduling with Contamination Constraints in the Agricultural Industry
Winters, Thomas	(ICLP) DeepStochLog: Neural Stochastic Logic Programming
Wolf, Verena	(CAV) MoGym: Using Formal Models for Training and Verifying Decision-making Agents
Wolper, Pierre	(VardiFest) On the unusual effectiveness of automata in logic
Wolter, Frank	(DECFOML) Decidability Questions beyond Satisfiability for First-order Modal Logics (KR) Unique Characterisability and Learnability of Temporal Instance Queries (KR) Interpolants and Explicit Definitions in Extensions of the Description Logic EL (DL) Reverse Engineering of Temporal Queries with and without LTL Ontologies: First Steps (DL) More on Interpolants and Explicit Definitions for Description Logics with Nominals and/or Role Inclusions
Woltran, Stefan	(NMR) The Effect of Preferences in Abstract Argumentation Under a Claim-Centric View (PCCR) Tractable Abstract Argumentation via Backdoor-Treewidth (KR) Rediscovering Argumentation Principles Utilizing Collective Attacks (IJCAR) Sequent Calculi for Choice Logics
Wong, Meng Weng	(GDE) Automating Defeasible Reasoning in Law with Answer Set Programming
Wongpiromsarn, Tichakorn	(NSV) MLTL Multi-Type: A Logic for Reasoning about Traces of Different Types
Worrell, James	(LICS) Identity testing for radical expressions (LICS) On the Skolem Problem and the Skolem Conjecture
Wu, Bin	(KR) Open Relation Extraction With Non-existent and Multi-span Relationships
Wu, Haoze	(FoMLAS) Scalable Verification of GNN-based Job Schedulers
Wu, Hong	(KR) Learning Typed Rules over Knowledge Graphs
Wu, Jui-Hsuan	(LFMTP) A positive perspective on term representation: work in progress
Wu, Lianlong	(KR) Rule Learning over Knowledge Graphs with Genetic Logic Programming
Wu, Yaling	(CP) A Portfolio-Based Approach to Select Efficient Variable Ordering Heuristics for Constraint Satisfaction Problems
Wu, Zhilin	(ASL) Deciding Separation Logic with Heap Lists
Wullaert, Kobe	(HoTT/UF) A Library of Monoidal Categories for Display and Univalence
Wäldele, Lucas	(POS) SATViz: Real-Time Visualization of Clausal Proofs
Würtele, Tim	(GuttmanFest) A Tutorial-Style Introduction to DY*
X
Xia, Bican	(ITP) Compositional Verification of Interacting Systems using Event Monads
Xiao, Guohui	(DL) Ontology-based Data Federation (Extended Abstract) (DL) Extraction of Object-Centric Event Logs through Virtual Knowledge Graphs
Xiao, Peng	(ICLP) Efficient Datalog Rewriting for Query Answering in TGD Ontologies
Xing, Wanli	(ICLP) A Preliminary Data-driven Analysis of Common Errors Encountered by Novice Answer Set Programmers
Xiong, Jing	(DL) Ontology-based Data Federation (Extended Abstract) (DL) Extraction of Object-Centric Event Logs through Virtual Knowledge Graphs
Xu, Yifan	(XLoKR) Dialogue-Based Explanations of Reasoning in Rule-based Systems
Y
Yamada, Akihisa	(WPTE) Transforming Text to (and from) XML (WST) The Termination Competition (IJCAR) Term Ordering for Non-Reachability of (Conditional) Rewriting
Yang, Donglin	(KR) Open Relation Extraction With Non-existent and Multi-span Relationships
Yang, Hui	(IJCAR) Hyper-graph based Inference Rules for Computing EL+-Ontology Justifications
Yang, Huifan	(KR) Open Relation Extraction With Non-existent and Multi-span Relationships
Yap, Roland	(CP) CNF Encodings of Binary Constraint Trees (CP) CNF Encodings of Binary Constraint Trees (Extended Abstract) (MC) Scalable Uniform Sampling via Efficient Knowledge Compilation
Yeager, Jared	(ITP) Mechanizing Soundness of Off-Policy Evaluation
Yeoh, William	(ICLP) Model Reconciliation in Logic Programs
Yin, Minghao	(CP) A Portfolio-Based Approach to Select Efficient Variable Ordering Heuristics for Constraint Satisfaction Problems
Ying, Mingsheng	(CAV) Verifying Fairness in Quantum Machine Learning (LICS) Quantum Weakest Preconditions for Reasoning about Expected Runtimes of Quantum Programs
Yolcu, Emre	(PC) Exponential separations using guarded extension variables
You, Jia-Huai	(ICLP) A Fixpoint Characterization of Three-Valued Disjunctive Hybrid MKNF Knowledge Bases
Yu, Geunyeol	(CAV) STLmc: Robust STL Model Checking of Hybrid Systems using SMT
Yuan, Shenghao	(CAV) End-to-end Mechanised Proof of an eBPF Virtual Machine for Microcontrollers
Yurkov, Semyon	(CSF) Unlinkability of an Improved Key Agreement Protocol for EMV 2nd Gen Payments (FCS) Towards Unlinkable Smartcard-based Payments: an extended abstract
Z
Zakharyaschev, Michael	(KR) Unique Characterisability and Learnability of Temporal Instance Queries (DL) Reverse Engineering of Temporal Queries with and without LTL Ontologies: First Steps
Zamboni, Marco	(SMT) NORMA: a tool for the analysis of Relay-based Railway Interlocking Systems
Zamdzhiev, Vladimir	(LICS) Quantum Expectation Transformers for Cost Analysis
Zanasi, Fabio	(FSCD) Rewriting for monoidal closed categories
Zandberg, Koen	(CAV) End-to-end Mechanised Proof of an eBPF Virtual Machine for Microcontrollers
Zantema, Hans	(IFIP-WG1.6) The International School on Rewriting
Zarriess, Benjamin	(DL) Efficient TBox Reasoning with Value Restrictions using the FL0wer Reasoner (Extended Abstract)
Zawidzki, Michal	(iPRA) When iota Meets lambda
Zdancewic, Steve	(TERMGRAPH) Ideograph: A Language for Expressing and Manipulating Structured Data
Zehavi, Meirav	(PCCR) The Tournament Fixing Problem
Zeilberger, Noam	(LFMTP) Type refinement as a unifying principle
Zelazny, Tom	(FoMLAS) Verification-Aided Deep Ensemble Selection
Zese, Riccardo	(ICLP) An Iterative Fixpoint Semantics for MKNF Hybrid Knowledge Bases with Function Symbols (ICLP) Abduction in Probabilistic Logic Programs
Zetzsche, Georg	(LICS) Ramsey Quantifiers over Automatic Structures: Complexity and Applications to Verification (LICS) The complexity of bidirected reachability in valence systems
Zeume, Thomas	(LogTeach) Teaching logic to CS undergraduates (LICS) The Regular Languages of First-Order Logic with One Alternation
Zhan, Bohua	(ITP) Compositional Verification of Interacting Systems using Event Monads (ITP) (Invited) User Interface Design in the HolPy Theorem Prover
Zhang, Danfeng	(CSF) Towards a General-Purpose Dynamic Information Flow Policy
Zhang, Liangfeng	(CAV) PoS4MPC: Automated Security Policy Synthesis for Secure Multi-Party Computation
Zhang, Lijun	(CAV) Divide-and-Conquer Determinization of Büchi Automata based on SCC Decomposition
Zhang, Min	(CAV) Trainify: A CEGAR-Driven Training and Verification Framework for Verifiable Deep Reinforcement Learning (FoMLAS) Neural Network Verification with Proof Production
Zhang, Naifeng	(POS) Towards the shortest DRAT proof of the Pigeonhole Principle
Zhang, Shujun	(WPTE) On Transforming Rewriting-Induction Proofs for Logical-Connective-Free Sequents into Cyclic Proofs
Zhang, Shutao	(ASPOCP) Constrained Default Logic Programming
Zhang, Xindi	(CAV) Local Search For SMT on Linear Integer Arithmetic
Zhang, Yuanlin	(ICLP) A Preliminary Data-driven Analysis of Common Errors Encountered by Novice Answer Set Programmers
Zhang, Zhizheng	(ASPOCP) Assumable Answer Set Programming (ASPOCP) Constrained Default Logic Programming
Zhao, Gehang	(ITP) Compositional Verification of Interacting Systems using Event Monads
Zhao, Haoruo	(DL) Next Steps for ReAD: Modules for Classification Optimisation
Zheng, Yang	(FoMLAS) Tight Neural Network Verification via Semidefinite Relaxations and Linear Reformulations
Zhi, Dapeng	(CAV) Trainify: A CEGAR-Driven Training and Verification Framework for Verifiable Deep Reinforcement Learning
Zhong, Allen Z.	(CP) Exploiting Functional Constraints in Generating Dominance Breaking Nogoods for Constraint Optimization (CP) Exploiting Functional Constraints in Automatic Dominance Breaking for Constraint Optimization (Extended Abstract) (ModRef) Automatic Generation of Dominance Breaking Nogoods for Constraint Optimization
Zhou, Li	(LICS) Quantum Weakest Preconditions for Reasoning about Expected Runtimes of Quantum Programs
Zhou, Neng-Fa	(ModRef) Constraint-based Part-of-Speech Tagging
Zhu, Shufang	(KR) Act for Your Duties but Maintain Your Rights (VardiFest) LTLf Synthesis as AND-OR Graph Search: Knowledge Compilation at Work
Zhu, Xu	(CP) Understanding how people approach constraint modelling and solving
Zhuang, Zhiqiang	(ICLP) Efficient Datalog Rewriting for Query Answering in TGD Ontologies
Zieglar, Edward	(GuttmanFest) Searching for Selfie in TLS 1.3 with the Cryptographic Protocol Shapes Analyzer
Zikas, Vassilis	(CSF) Collusion-Preserving Computation without a Mediator
Zimmermann, Théo	(ITP) Automatic Test-Case Reduction in Proof Assistants: A Case Study in Coq (Coq) Coq Community Survey 2022: Summary of Results
Zohar, Yoni	(IJCAR) Reasoning About Vectors using an SMT Theory of Sequences (IJCAR) Flexible Proof Production in an Industrial-Strength SMT Solver (IJCAR) Effective Semantics for the Modal Logics K and KT via Non-deterministic Matrices (SMT) cvc5: A Versatile and Industrial-Strength SMT Solver (SMT) Bit-Precise Reasoning via Int-Blasting (ThEdu) Invited Talk: Satisfiability Modulo Theories in an Undergraduate Class
Zuber, Johann	(POS) SATViz: Real-Time Visualization of Clausal Proofs
Zuidberg Dos Martires, Pedro	(ICLP) Inference and Learning with Model Uncertainty in Probabilistic Logic Programs
Zuleger, Florian	(CAV) Automated Expected Amortised Cost Analysis of Probabilistic Data Structures (ASL) On the Expressiveness of a Logic of Separated Relations
Zweifler, Jacob	(Coq) QuantumLib: A Library for Quantum Computing in Coq
Zweydinger, Floyd	(CSF) Legendre PRF (Multiple) Key Attacks and the Power of Preprocessing
Å
Åman Pohjola, Johannes	(ITP) A Verified Cyclicity Checker (ITP) Kalas: A Verified, End-to-End Compiler for a Choreographic Language
Ś
Ślusarz, Natalia	(FoMLAS) Differentiable Logics for Neural Network Verification
Š
Šimkus, Mantas	(NMR) Pointwise Circumscription in Description Logics
Šiška, Jozef	(FOMEO) First-Order Logic Workbook
Šmahlíková, Barbora	(CAV) Complementing Büchi Automata with Ranker
Šćepanović, David	(SMT) Trail saving in SMT
Ž
Žikelić, Đorđe	(CAV) Sound and Complete Certificates for Quantitative Termination Analysis of Probabilistic Programs