FLOC 2022: FEDERATED LOGIC CONFERENCE 2022

(
(iterated) admissibility	(VardiFest) That's All I know: On the Effectiveness of Logic in Game Theory (, talk)
(Probabilistic) Integer Programs	(WST) Automatic Complexity Analysis of (Probabilistic) Integer Programs via KoAT (, talk)
A
abduction	(IJCAR) Connection-Minimal Abduction in EL via Translation to FOL (, talk) (DL) Concept Abduction for Description Logics (, talk) (DL) An API for DL Abduction Solvers (, talk) (DL) Connection-minimal Abduction in EL via translation to FOL (Extended Abstract) (, talk)
ABox abduction	(DL) Hybrid MHS-MXP ABox Abduction Solver: First Emprical Results (, talk)
ABox approximation	(DL) Optimal ABox Repair w.r.t. Static EL TBoxes: from Quantified ABoxes back to ABoxes (Extended Abstract) (, talk)
Abstract Interpretation	(FoMLAS) Scalable Verification of GNN-based Job Schedulers (, talk)
Abstraction	(FoMLAS) An Abstraction-Refinement Approach to Verifying Convolutional Neural Networks (, talk)
abstraction and refinement	(CAV) Trainify: A CEGAR-Driven Training and Verification Framework for Safe Deep Reinforcement Learning (, talk)
abstraction refinement	(IJCAR) Cooperating Techniques for Solving Nonlinear Arithmetic in the cvc5 SMT Solver (System Description) (, talk)
Abstraction-Refinement	(FoMLAS) An Abstraction-Refinement Approach to Verifying Convolutional Neural Networks (, talk) (CAV) Abstraction-Refinement for Hierarchical Probabilistic Models (, talk)
Accuracy	(VardiFest) Verifying Accuracy Claims of Differential Privacy Algorithms (, talk)
Actions	(IJCAR) Actions over Core-Closed Knowledge Bases (, talk)
Actual Causality	(CAV) Explaining Hyperproperty Violations (, talk)
Adversarial Attacks	(FoMLAS) Verification-Aided Deep Ensemble Selection (, talk)
adversarial robustness	(CAV) Shared Certificates for Neural Network Verification (, talk)
Adversarial Training	(CAV) Neural Network Robustness as a Verification Property: A Principled Case Study (, talk)
Aerospace	(VardiFest) Logic-driven approaches for smart, safe and energy-efficient aviation (, talk)
Agda	(FoMLAS) Vehicle: A High-Level Language for Embedding Logical Specifications in Neural Networks (, talk) (FMBC) Human and machine-readable models of state machines for the Cardano ledger (, talk)
Aggressive Bound Descent	(CP) Aggressive Bound Descent for Constraint Optimization (, talk)
AI Certification	(FoMLAS) RoMA: a Method for Neural Network Robustness Measurement and Assessment (, talk)
ALC	(DL) Fine-Grained Forgetting for the Description Logic ALC (, talk)
Algebraic Measures	(DL) Reasoning on Multi-Relational Contextual Hierarchies via Answer Set Programming with Algebraic Measures (, talk)
Algorithmic Game Theory	(VardiFest) Strategy Logic: Origin, Results, and Open Questions (, talk)
algorithmic graph theory	(VardiFest) On the Effectiveness of Logic in Algorithmic Graph Theory (, talk)
all I know	(VardiFest) That's All I know: On the Effectiveness of Logic in Game Theory (, talk)
amortised cost analysis	(CAV) Automated Expected Amortised Cost Analysis of Probabilistic Data Structures (, talk)
AND-OR graph	(VardiFest) LTLf Synthesis as AND-OR Graph Search: Knowledge Compilation at Work (, talk)
Anti-unification	(IJCAR) A Framework for Approximate Generalization in Quantitative Theories (, talk)
archery	(VardiFest) A Toast for Moshe at the FLoC VardiFest (, talk)
arithmetic constraints	(IJCAR) CTL* Model Checking for Data-Aware Dynamic Systems with Arithmetic (, talk)
Artificial intelligence	(VardiFest) LTLf? It's Easy! Precisely! (, ) (CP) Extended Abstract: Acquiring Maps of Interrelated Conjectures on Sharp Bounds (, talk) (CP) Finding Counterfactual Explanations through Constraint Relaxations (, talk) (CP) A Boolean Formula Seeker in the Context of Acquiring Maps of Interrelated Conjectures on Sharp Bounds (, talk)
ASP	(DL) Reasoning on Multi-Relational Contextual Hierarchies via Answer Set Programming with Algebraic Measures (, talk)
Associativity	(IJCAR) Non-associative, Non-commutative Multi-Modal Linear Logic (, talk)
Assume-Guarantee Synthesis	(CAV) Information Flow Guided Synthesis (, talk)
assumptions	(VardiFest) Trace-view vs Strategy-view of the Environment in Reactive Synthesis (, )
at least three keywords must be specified	(WST) Certified Matchbox (, talk)
Autoencoding	(VardiFest) Natural Autoencoding (, talk)
Automata	(VardiFest) Automata-Based Quantitative Reasoning (, talk) (VardiFest) LTLf? It's Easy! Precisely! (, ) (CAV) Reasoning about Data Trees using CHCs (, talk)
Automata Theory	(VardiFest) Between Determinism and Nondeterminism (, talk) (VardiFest) The Safety Fragment of LTL (, talk)
Automata-Theoretic Approach	(VardiFest) LTLf Synthesis Under Environment Specifications (, talk)
automated algorithm configuration	(CP) Improved Sample Complexity Bounds for Branch-and-Cut (, talk)
automated driving	(FoMLAS) Goal-Aware RSS for Complex Scenarios via Program Logic (, talk)
automated numerical planning and scheduling	(VardiFest) Towards Combination of Logic and Calculus for Near-Optimal Planning in Relational Hybrid Systems (, talk)
Automated reasoning	(IJCAR) GK: Implementing Full First Order Default Logic for Commonsense Reasoning (System Description) (, talk) (IJCAR) Lash 1.0 (System Description) (, talk) (IJCAR) Guiding an Automated Theorem Prover with Neural Rewriting (, talk) (FoMLAS) Neural Networks in Imandra: Matrix Representation as a Verification Choice (, talk) (VardiFest) On the Extraordinary Effectiveness of Logic in Strategic Reasoning (, talk) (POS) Scalable Proof Producing Multi-Threaded SAT Solving with Gimsatul through Sharing instead of Copying Clauses (, talk) (FMBC) Automating Security Analysis of Off-Chain Protocols (, talk)
Automated Testing	(CAV) Murxla: A Modular and Highly Extensible API Fuzzer for SMT Solvers (, talk)
Automated Theorem Proving	(IJCAR) Goéland: A Concurrent Tableau-Based Theorem Prover (System Description) (, talk) (IJCAR) Bayesian Ranking for Strategy Scheduling in Automated Theorem Provers (, talk) (IJCAR) Guiding an Automated Theorem Prover with Neural Rewriting (, talk)
Automatic Complexity Analysis	(WST) Improved Automatic Complexity Analysis of Integer Programs (, talk) (WST) Automatic Complexity Analysis of (Probabilistic) Integer Programs via KoAT (, talk)
automatic verification	(CAV) Sound Automation of Magic Wands (, talk)
automation	(CAV) Automated Expected Amortised Cost Analysis of Probabilistic Data Structures (, talk)
automatizability of proof systems	(PC) Simulations between proof systems (, talk)
Average-case complexity	(PC) Average-Case Hardness of Proving Tautologies and Theorems (, talk)
Aviation	(VardiFest) Logic-driven approaches for smart, safe and energy-efficient aviation (, talk)
B
B\"uchi automata	(VardiFest) Divide-and-Conquer Determinization for B\"uchi Automata (, talk)
backdoor attack	(CAV) Verifying Neural Networks Against Backdoor Attacks (, talk)
Backtracking Search	(CP) Aggressive Bound Descent for Constraint Optimization (, talk)
battle of Hercules and Hydra	(WST) Hydra Battles and AC Termination (, talk)
Bayesian Machine Learning	(IJCAR) Bayesian Ranking for Strategy Scheduling in Automated Theorem Provers (, talk)
BCT	(CP) CNF Encodings of Binary Constraint Trees (Extended Abstract) (, talk)
BDD	(VardiFest) A Short Talk Proposal for the VardiFest "On the Not So Unusual Effectiveness of Logic" (, talk) (VardiFest) Boolean Synthesis via Decision Diagrams (, talk)
Belief Propagation	(CP) Exploiting Model Entropy to Make Branching Decisions in Constraint Programming (, talk)
Belief revision	(DL) AGM Revision in Description Logics Under Fixed-Domain Semantics (, talk)
Bell Labs	(VardiFest) A Short Talk Proposal for the VardiFest "On the Not So Unusual Effectiveness of Logic" (, talk)
benchmarking	(IJCAR) Local Reductions for the Modal Cube (, talk)
benchmarks	(DL) Expressivity of Planning with Horn Description Logic Ontologies (Extended Abstract) (, talk)
Bernays–Schönfinkel Fragment	(IJCAR) An Efficient Subsumption Test Pipeline for BS(LRA) Clauses (, talk)
best-effort synthesis	(VardiFest) Trace-view vs Strategy-view of the Environment in Reactive Synthesis (, )
Beth Definability Property	(DL) More on Interpolants and Explicit Definitions for Description Logics with Nominals and/or Role Inclusions (, talk)
binary codes	(IJCAR) Binary Codes that do Not Preserve Primitivity (, talk)
Binary Decision Diagrams	(POS) Combining CDCL, Gauss-Jordan Elimination, and Proof Generation (, talk)
bisimulation	(VardiFest) Bisimulation Games Played in Fibered Categories (, talk) (DL) Comonadic Semantics for Description Logics Games (, talk)
bit pigeonhole principle	(PC) Proof complexity of natural formulas via communication arguments (, talk)
Block Ciphers	(POS) Towards an Efficient CNF Encoding of Block Ciphers (, talk)
blockchain	(FMBC) Multi: a Formal Playground for Smart Multi-contract interaction (, talk) (FMBC) Human and machine-readable models of state machines for the Cardano ledger (, talk) (FMBC) Proofgold: Blockchain for Formal Methods (, talk) (FMBC) FAT CAT: Formal Acceptance Testing of Contracts for Administering Tokens (, talk)
Blockchains	(FMBC) A Domain Specific Language for Testing Consensus Implementations (, talk)
blocked clauses	(PC) Exponential separations using guarded extension variables (, talk)
boolean satisfiability	(CP) Automated SAT Problem Feature Extraction using 1 Convolutional Autoencoders (, talk) (POS) Combining CDCL, Gauss-Jordan Elimination, and Proof Generation (, talk)
Boolean synthesis	(VardiFest) Boolean Synthesis via Decision Diagrams (, talk)
Bounded arithmetic	(PC) Proof complexity of CSP (, talk)
Bounded model checking	(CAV) Proof-guided Underapproximation Widening for Bounded Model Checking (, talk)
branch-and-bound	(CP) Improved Sample Complexity Bounds for Branch-and-Cut (, talk) (CP) Peel-and-Bound: Generating Stronger Relaxed Bounds with Multivalued Decision Diagrams (, talk)
branch-and-cut	(CP) Improved Sample Complexity Bounds for Branch-and-Cut (, talk)
Branching Time	(VardiFest) A Short Talk Proposal for the VardiFest "On the Not So Unusual Effectiveness of Logic" (, talk)
Büchi automata	(CAV) FORQ-based Language Inclusion Formal Testing (, talk) (CAV) Divide-and-Conquer Determinization of Büchi Automata based on SCC Decomposition (, talk) (CAV) Complementing Büchi Automata with Ranker (, talk)
C
cache coherence	(CAV) Hemiola: A DSL and Verification Tools to Guide Design and Proof of Hierarchical Cache-Coherence Protocols (, talk)
Calculus of Names	(IJCAR) Le\'sniewski's Ontology -- Proof-Theoretic Characterization (, talk)
Cardano	(FMBC) Human and machine-readable models of state machines for the Cardano ledger (, talk)
Categorial Robustness	(FoMLAS) RoMA: a Method for Neural Network Robustness Measurement and Assessment (, talk)
category theory	(VardiFest) Bisimulation Games Played in Fibered Categories (, talk) (CAV) The Lattice-Theoretic Essence of Property Directed Reachability Analysis (, talk) (DL) Category-based Semantics for the Description Logic ALC and Reasoning (, talk)
CAV	(VardiFest) A Short Talk Proposal for the VardiFest "On the Not So Unusual Effectiveness of Logic" (, talk)
CDCL	(PC) QCDCL with Cube Learning or Pure Literal Elimination – What is best? (, talk)
CDCL Algorithm	(POS) SATViz: Real-Time Visualization of Clausal Proofs (, talk)
Certification	(WST) CeTA – A certifier for termCOMP 2022 (, talk)
Choice logics	(IJCAR) Sequent Calculi for Choice Logics (, talk)
Circumscription	(DL) Pointwise Circumscription in Description Logics (, talk)
Classification	(DL) Next Steps for ReAD: Modules for Classification Optimisation (, talk)
Clausal Proofs	(POS) Combining CDCL, Gauss-Jordan Elimination, and Proof Generation (, talk)
Clause exchange	(POS) DPS: A Framework for Deterministic Parallel SAT Solvers (, talk)
clause learning from simple models	(IJCAR) SCL(EQ): SCL for First-Order Logic with Equality (, talk)
clause redundancy	(IJCAR) Clause Redundancy and Preprocessing in Maximum Satisfiability (, talk)
Closed Form	(WST) Deciding Termination of Uniform Loops with Polynomial Parameterized Complexity (, talk)
closure redundancy	(IJCAR) Ground Joinability and Connectedness in the Superposition Calculus (, talk)
Cloud Security	(IJCAR) Actions over Core-Closed Knowledge Bases (, talk)
CNF	(CP) CNF Encodings of Binary Constraint Trees (Extended Abstract) (, talk)
CNF Encoding	(CP) Automated SAT Problem Feature Extraction using 1 Convolutional Autoencoders (, talk) (POS) Towards an Efficient CNF Encoding of Block Ciphers (, talk)
Combinations of Logic and Machine Learning	(VardiFest) A Solver + Gradient Descent Training Algorithm for Deep Neural Network (, )
Combinations of Solvers and Gradient Descent	(VardiFest) A Solver + Gradient Descent Training Algorithm for Deep Neural Network (, )
Combinatorial optimization	(CP) Extended Abstract: Acquiring Maps of Interrelated Conjectures on Sharp Bounds (, talk) (CP) A Boolean Formula Seeker in the Context of Acquiring Maps of Interrelated Conjectures on Sharp Bounds (, talk)
combinatorial structures	(VardiFest) On the Effectiveness of Logic in Algorithmic Graph Theory (, talk)
Combinatorics	(CP) Extended Abstract: Acquiring Maps of Interrelated Conjectures on Sharp Bounds (, talk) (CP) A Boolean Formula Seeker in the Context of Acquiring Maps of Interrelated Conjectures on Sharp Bounds (, talk)
combining decision procedures	(CAV) Reasoning about Data Trees using CHCs (, talk)
Commonsense reasoning	(IJCAR) GK: Implementing Full First Order Default Logic for Commonsense Reasoning (System Description) (, talk)
Commutativity	(IJCAR) Non-associative, Non-commutative Multi-Modal Linear Logic (, talk)
comonads	(DL) Comonadic Semantics for Description Logics Games (, talk)
Comparators	(VardiFest) Automata-Based Quantitative Reasoning (, talk)
compilation scheme	(DL) Expressivity of Planning with Horn Description Logic Ontologies (Extended Abstract) (, talk)
compiler optimization	(CP) Optimized Code Generation against Power Side Channels (, talk)
Compiler verification	(CAV) SMT-based Translation Validation for Machine Learning Compiler (, talk)
complementation	(CAV) Complementing Büchi Automata with Ranker (, talk)
Completeness guarantees	(CAV) Sound and Complete Certificates for Quantitative Termination Analysis of Probabilistic Programs (, talk)
Complexity	(WST) Deciding Termination of Uniform Loops with Polynomial Parameterized Complexity (, talk) (WST) CeTA – A certifier for termCOMP 2022 (, talk) (IJCAR) Decision Problems in a Logic for Reasoning about Reconfigurable Distributed Systems (, talk) (DL) Category-based Semantics for the Description Logic ALC and Reasoning (, talk) (DL) Optimal ABox Repair w.r.t. Static EL TBoxes: from Quantified ABoxes back to ABoxes (Extended Abstract) (, talk)
complexity analysis	(WST) Tuple Interpretations and Applications to Higher-Order Runtime Complexity (, talk) (IJCAR) Proving Non-Termination and Lower Runtime Bounds with LoAT (System Description) (, talk) (IJCAR) Automatic Complexity Analysis of Integer Programs via Triangular Weakly Non-Linear Loops (, talk)
complexity over structures	(VardiFest) Computability and Complexity over Finite Unordered Structures; e.g., Graphs (1979-1982) (, talk)
Compositional Synthesis	(CAV) Information Flow Guided Synthesis (, talk)
comprehensibility	(DL) Finding Good Proofs for Answers to Conjunctive Queries Mediated by Lightweight Ontologies (, talk)
computability over structures	(VardiFest) Computability and Complexity over Finite Unordered Structures; e.g., Graphs (1979-1982) (, talk)
computable queries	(VardiFest) Computability and Complexity over Finite Unordered Structures; e.g., Graphs (1979-1982) (, talk)
computational complexity	(VardiFest) Data Path Queries over Embedded Graph Databases (, talk) (VardiFest) Fixpoint Logics, Relational Machines, and Computational Complexity (, talk) (DL) Reverse Engineering of Temporal Queries with and without LTL Ontologies: First Steps (, talk) (DL) Pointwise Circumscription in Description Logics (, talk)
Computing methodologies	(CP) Extended Abstract: Acquiring Maps of Interrelated Conjectures on Sharp Bounds (, talk) (CP) A Boolean Formula Seeker in the Context of Acquiring Maps of Interrelated Conjectures on Sharp Bounds (, talk)
Concept Referring Expressions	(DL) Computing Concept Referring Expressions with Standard OWL Reasoners (, talk)
Concurrency	(IJCAR) Goéland: A Concurrent Tableau-Based Theorem Prover (System Description) (, talk)
Confluence	(WST) CeTA – A certifier for termCOMP 2022 (, talk)
connectedness	(IJCAR) Ground Joinability and Connectedness in the Superposition Calculus (, talk)
Consensus Protocols	(FMBC) A Domain Specific Language for Testing Consensus Implementations (, talk)
consequence relations	(IJCAR) Finite Two-Dimensional Proof Systems for Non-finitely Axiomatizable Logics (, talk)
Consistency Analysis	(VardiFest) Checking Legal Contracts - On a Not So Usual Application of Mechanized Logic (, talk)
Constrained Horn Clauses	(CAV) SolCMC: Solidity Compiler’s Model Checker (, talk) (CAV) Reasoning about Data Trees using CHCs (, talk)
Constrained Single-Row Facility Layout Problem	(CP) Solving the Constrained Single-Row Facility Layout Problem with Decision Diagrams (Extended Abstract) (, talk)
Constraint acquisition	(CP) Extended Abstract: Constraint Acquisition Based on Solution Counting (, talk)
constraint logic programming	(VardiFest) Towards Combination of Logic and Calculus for Near-Optimal Planning in Relational Hybrid Systems (, talk)
Constraint Optimization	(CP) Aggressive Bound Descent for Constraint Optimization (, talk)
Constraint Optimization Problems	(CP) Exploiting Functional Constraints in Automatic Dominance Breaking for Constraint Optimization (Extended Abstract) (, talk)
constraint programming	(CP) Exploiting Model Entropy to Make Branching Decisions in Constraint Programming (, talk) (CP) Explaining Propagation for Gini and Spread with Variable Mean (Extended Abstract) (, talk) (CP) On PB Encodings for Constraint Problems (, talk) (CP) Combining Reinforcement Learning and Constraint Programming for Sequence-Generation Tasks with Hard Constraints - Extended Abstract (, talk) (CP) Large Neighborhood Search for Robust Solutions for Constraint Satisfaction Problems with Ordered Domains (, talk) (CP) Solving the Non-Crossing MAPF for non point-sized robots (, talk) (CP) Extended Abstract for : Scheduling the Equipment Maintenance of an Electric Power Transmission Network using Constraint Programming (, talk) (CP) Peel-and-Bound: Generating Stronger Relaxed Bounds with Multivalued Decision Diagrams (, talk) (CP) Optimized Code Generation against Power Side Channels (, talk)
constraint satisfaction	(VardiFest) From Kochen-Specker to Feder-Vardi (, talk)
constraint satisfaction problems	(PC) Proof complexity of CSP (, talk) (VardiFest) On the Effectiveness of Logic in Algorithmic Graph Theory (, talk) (CP) Finding Counterfactual Explanations through Constraint Relaxations (, talk)
Constraint simplification	(CAV) Distilling Constraints in Zero-Knowledge Protocols (, talk)
constraint solving	(CAV) Automated Expected Amortised Cost Analysis of Probabilistic Data Structures (, talk) (CAV) Synthesizing Fair Decision Trees via Iterative Constraint Solving (, talk)
Constraint tableaux	(IJCAR) Paraconsistent Gödel Modal Logic (, talk)
contextuality	(VardiFest) From Kochen-Specker to Feder-Vardi (, talk)
continuous reachability	(CAV) Verifying generalised and structural soundness of workflow nets via relaxations (, talk)
Control-Flow Refinement	(WST) Improved Automatic Complexity Analysis of Integer Programs (, talk) (WST) Automatic Complexity Analysis of (Probabilistic) Integer Programs via KoAT (, talk)
Controller Synthesis	(CAV) Playing Against Fair Adversaries in Stochastic Games with Total Rewards (, talk)
convolutional autoencoders	(CP) Automated SAT Problem Feature Extraction using 1 Convolutional Autoencoders (, talk)
Convolutional Neural Networks	(FoMLAS) An Abstraction-Refinement Approach to Verifying Convolutional Neural Networks (, talk)
Convolutional Neural Networks Verification	(FoMLAS) An Abstraction-Refinement Approach to Verifying Convolutional Neural Networks (, talk)
Cooperation in MAS	(VardiFest) An Epistemic Logic for modelling Cooperative Agents (, talk)
Coq	(CAV) Hemiola: A DSL and Verification Tools to Guide Design and Proof of Hierarchical Cache-Coherence Protocols (, talk) (FMBC) Finding smart contract vulnerabilities with ConCert's property-based testing framework (, talk) (FMBC) FAT CAT: Formal Acceptance Testing of Contracts for Administering Tokens (, talk)
correct-by-construction	(CAV) Trainify: A CEGAR-Driven Training and Verification Framework for Safe Deep Reinforcement Learning (, talk)
counter systems	(IJCAR) CTL* Model Checking for Data-Aware Dynamic Systems with Arithmetic (, talk)
Counterexamples	(CAV) Explaining Hyperproperty Violations (, talk)
counterfactual explanations	(CP) Finding Counterfactual Explanations through Constraint Relaxations (, talk)
Counterfactual Reasoning	(CAV) Explaining Hyperproperty Violations (, talk)
countermodel construction	(IJCAR) SAT-based Proof Search in Intermediate Propositional Logics (, talk)
Counting	(VardiFest) To Count or Not to Count: A Personal Perspective (, talk)
Counting queries	(DL) Complexity Landscape for Counting Queries (Extended abstract) (, talk)
Craig interpolants	(DL) More on Interpolants and Explicit Definitions for Description Logics with Nominals and/or Role Inclusions (, talk)
CSP	(CP) Extended Abstract: Constraint Acquisition Based on Solution Counting (, talk)
CTL*	(IJCAR) CTL* Model Checking for Data-Aware Dynamic Systems with Arithmetic (, talk)
Cut Elimination	(IJCAR) Le\'sniewski's Ontology -- Proof-Theoretic Characterization (, talk)
cut-elimination	(IJCAR) Non-associative, Non-commutative Multi-Modal Linear Logic (, talk)
cutting planes	(CP) Improved Sample Complexity Bounds for Branch-and-Cut (, talk)
Cyber-physical systems	(VardiFest) Synthesis of plans for teams of manufacturing robots (, talk)
Cyclic proofs	(IJCAR) Cyclic Proofs, Hypersequents, and Transitive Closure Logic (, talk)
cylindrical algebraic coverings	(IJCAR) Cooperating Techniques for Solving Nonlinear Arithmetic in the cvc5 SMT Solver (System Description) (, talk)
D
Data analysis	(IJCAR) Synthetic Tableaux: Minimal Tableau Search Heuristics (, talk)
Data Complexity	(VardiFest) Data Complexity and Expressive Power of Ontological Reasoning Formalisms (, talk) (VardiFest) Towards Algebraic Techniques for Descriptive Complexity (, talk)
data federation	(DL) Ontology-based Data Federation (Extended Abstract) (, talk)
data logics	(CAV) Reasoning about Data Trees using CHCs (, talk)
data-driven algorithm design	(CP) Improved Sample Complexity Bounds for Branch-and-Cut (, talk)
Data-driven invariant learning	(CAV) Data-Driven Invariant Learning for Probabilistic Programs (, talk)
Data-driven methods	(CAV) Data-driven Numerical Invariant Synthesis with Automatic Generation of Attributes (, talk)
Databases	(VardiFest) Data Complexity and Expressive Power of Ontological Reasoning Formalisms (, talk)
databases as logical theories	(VardiFest) Approximations of Certain Answers in First-Order Logic (, talk)
decidability	(IJCAR) Non-associative, Non-commutative Multi-Modal Linear Logic (, talk) (IJCAR) Decision Problems in a Logic for Reasoning about Reconfigurable Distributed Systems (, talk) (VardiFest) Verifying Accuracy Claims of Differential Privacy Algorithms (, talk)
decidable subclasses	(WST) Automatic Complexity Analysis of (Probabilistic) Integer Programs via KoAT (, talk) (IJCAR) Automatic Complexity Analysis of Integer Programs via Triangular Weakly Non-Linear Loops (, talk)
Decision Diagrams	(VardiFest) Boolean Synthesis via Decision Diagrams (, talk) (CP) Solving the Constrained Single-Row Facility Layout Problem with Decision Diagrams (Extended Abstract) (, talk) (CP) Peel-and-Bound: Generating Stronger Relaxed Bounds with Multivalued Decision Diagrams (, talk)
Decision Procedure	(WST) Deciding Termination of Uniform Loops with Polynomial Parameterized Complexity (, talk)
decision tree	(CAV) Synthesizing Fair Decision Trees via Iterative Constraint Solving (, talk)
deep learning	(FoMLAS) Verification-Aided Deep Ensemble Selection (, talk) (CP) Automated SAT Problem Feature Extraction using 1 Convolutional Autoencoders (, talk)
Deep Learning Compiler	(CAV) SMT-based Translation Validation for Machine Learning Compiler (, talk)
Deep Neural Network Verification	(FoMLAS) An Abstraction-Refinement Approach to Verifying Convolutional Neural Networks (, talk)
Deep Neural Networks	(FoMLAS) Verification-Aided Deep Ensemble Selection (, talk) (FoMLAS) An Abstraction-Refinement Approach to Verifying Convolutional Neural Networks (, talk)
Deep reinforcement learning	(CAV) Trainify: A CEGAR-Driven Training and Verification Framework for Safe Deep Reinforcement Learning (, talk)
Default logic	(IJCAR) GK: Implementing Full First Order Default Logic for Commonsense Reasoning (System Description) (, talk)
Defeasible Knowledge	(DL) Reasoning on Multi-Relational Contextual Hierarchies via Answer Set Programming with Algebraic Measures (, talk)
definitions	(IJCAR) Implicit Definitions with Differential Equations for KeYmaera X (System Description) (, talk)
Delegate Reasoner	(DL) Next Steps for ReAD: Modules for Classification Optimisation (, talk)
Denotational semantics	(CAV) Does a Program Yield the Right Distribution? Verifying Probabilistic Programs via Generating Functions (, talk)
Description Logic	(IJCAR) Evonne: Interactive Proof Visualization for Description Logics (System Description) (, talk) (IJCAR) Actions over Core-Closed Knowledge Bases (, talk) (DL) Advanced languages of terms for ontologies (, talk) (DL) More on Interpolants and Explicit Definitions for Description Logics with Nominals and/or Role Inclusions (, talk) (DL) A Labelled Natural Deduction System for an Intuitionistic Description Logic with Nominals (, talk) (DL) Fine-Grained Forgetting for the Description Logic ALC (, talk)
Description Logic EL	(IJCAR) Connection-Minimal Abduction in EL via Translation to FOL (, talk) (IJCAR) Hypergraph-Based Inference Rules for Computing EL+-Ontology Justifications (, talk) (DL) Connection-minimal Abduction in EL via translation to FOL (Extended Abstract) (, talk) (DL) Optimal ABox Repair w.r.t. Static EL TBoxes: from Quantified ABoxes back to ABoxes (Extended Abstract) (, talk)
Description Logics	(DL) AGM Revision in Description Logics Under Fixed-Domain Semantics (, talk) (DL) Uniform and Modular Sequent Systems for Description Logics (, talk) (DL) Concept Abduction for Description Logics (, talk) (DL) An API for DL Abduction Solvers (, talk) (DL) Hybrid MHS-MXP ABox Abduction Solver: First Emprical Results (, talk) (DL) Accessing Document Data Sources using Referring Expression Types (, talk) (DL) Reasoning on Multi-Relational Contextual Hierarchies via Answer Set Programming with Algebraic Measures (, talk) (DL) Computing Concept Referring Expressions with Standard OWL Reasoners (, talk) (DL) SAT-Based Axiom Pinpointing Revisited (, talk) (DL) Complexity Landscape for Counting Queries (Extended abstract) (, talk)
Descriptive Complexity	(VardiFest) Towards Algebraic Techniques for Descriptive Complexity (, talk)
determinism	(FMBC) Determinism of ledger updates (, talk)
Deterministic Emerson-Lei automata	(VardiFest) Divide-and-Conquer Determinization for B\"uchi Automata (, talk)
Determinization	(VardiFest) Divide-and-Conquer Determinization for B\"uchi Automata (, talk) (CAV) Divide-and-Conquer Determinization of Büchi Automata based on SCC Decomposition (, talk)
Diagonalizable matrices	(IJCAR) On Eventual Non-negativity and Positivity for the Weighted Sum of Powers of Matrices (, talk)
Dial-A-Ride	(CP) Extended Abstract: Sequence Variables for Routing Problems (, talk)
Differentiable Logic	(FoMLAS) Differentiable Logics for Neural Network Training and Verification (, talk)
differential dynamic logic	(IJCAR) Implicit Definitions with Differential Equations for KeYmaera X (System Description) (, talk) (FoMLAS) Goal-Aware RSS for Complex Scenarios via Program Logic (, talk)
Differential Privacy	(VardiFest) Verifying Accuracy Claims of Differential Privacy Algorithms (, talk)
Dimensionality reduction	(VardiFest) Natural Autoencoding (, talk)
Discrete mathematics	(CP) Extended Abstract: Acquiring Maps of Interrelated Conjectures on Sharp Bounds (, talk) (CP) A Boolean Formula Seeker in the Context of Acquiring Maps of Interrelated Conjectures on Sharp Bounds (, talk)
Discrete Optimization	(CP) Solving the Constrained Single-Row Facility Layout Problem with Decision Diagrams (Extended Abstract) (, talk) (CP) Peel-and-Bound: Generating Stronger Relaxed Bounds with Multivalued Decision Diagrams (, talk)
disjointness	(PC) Proof complexity of natural formulas via communication arguments (, talk)
distributed ledger	(FMBC) FAT CAT: Formal Acceptance Testing of Contracts for Administering Tokens (, talk)
Distributed Synthesis	(CAV) Information Flow Guided Synthesis (, talk)
Distributed Systems	(CAV) Information Flow Guided Synthesis (, talk) (FMBC) A Domain Specific Language for Testing Consensus Implementations (, talk)
Divide-and-Conquer	(VardiFest) Divide-and-Conquer Determinization for B\"uchi Automata (, talk) (CAV) Divide-and-Conquer Determinization of Büchi Automata based on SCC Decomposition (, talk)
DL-Lite	(DL) Finding Good Proofs for Answers to Conjunctive Queries Mediated by Lightweight Ontologies (, talk)
DL-Lite-Horn	(DL) Actively Learning ELIQs in the Presence of DL-Lite-Horn Ontologies (, talk)
DNF	(POS) Dinosat: A SAT Solver with Native DNF Support (, talk)
document stores	(DL) Accessing Document Data Sources using Referring Expression Types (, talk)
Domain Specific Languages	(FMBC) A Domain Specific Language for Testing Consensus Implementations (, talk)
domain-specific language	(CAV) Hemiola: A DSL and Verification Tools to Guide Design and Proof of Hierarchical Cache-Coherence Protocols (, talk)
Dominance Breaking	(CP) Exploiting Functional Constraints in Automatic Dominance Breaking for Constraint Optimization (Extended Abstract) (, talk)
Dominance Relations	(CP) Exploiting Functional Constraints in Automatic Dominance Breaking for Constraint Optimization (Extended Abstract) (, talk)
DQBF	(CP) Boolean Functional Synthesis and its Applications (, talk)
Dynamic Logic	(VardiFest) Towards Algebraic Techniques for Descriptive Complexity (, talk)
E
Effective algorithms	(IJCAR) On Eventual Non-negativity and Positivity for the Weighted Sum of Powers of Matrices (, talk)
Efficient reasoning	(DL) Efficient TBox Reasoning with Value Restrictions using the FL0wer Reasoner (Extended Abstract) (, talk)
EL ontologies	(DL) Reasoning about actions with EL ontologies in a temporal action theory (Extended Abstract) (, talk)
elaborator reflection	(FMBC) Human and machine-readable models of state machines for the Cardano ledger (, talk)
Electric power network	(CP) Extended Abstract for : Scheduling the Equipment Maintenance of an Electric Power Transmission Network using Constraint Programming (, talk)
Emerson-Lei acceptance	(CAV) From Spot 2.0 to Spot 2.10: What's New? (, talk)
Emerson-Lei automata	(CAV) Divide-and-Conquer Determinization of Büchi Automata based on SCC Decomposition (, talk)
encoding	(POS) Towards the shortest DRAT proof of the Pigeonhole Principle (, talk)
Energy Efficiency	(VardiFest) Logic-driven approaches for smart, safe and energy-efficient aviation (, talk)
Ensembles	(FoMLAS) Verification-Aided Deep Ensemble Selection (, talk)
entailment	(IJCAR) Decision Problems in a Logic for Reasoning about Reconfigurable Distributed Systems (, talk)
Entropy	(CP) Exploiting Model Entropy to Make Branching Decisions in Constraint Programming (, talk)
Entropy Estimation	(CAV) A Scalable Shannon Entropy Estimator (, talk)
enumeration	(PC) Are Hitting Formulas Hard for Resolution? (, talk)
Epistemic Logic	(VardiFest) An Epistemic Logic for modelling Cooperative Agents (, talk)
equational unification	(IJCAR) Equational Unification and Matching, and Symbolic Reachability Analysis in Maude 3.2 (System Description) (, talk)
Equivalence Verification	(FoMLAS) CEG4N: Counter-Example Guided Neural Network Quantization Refinement (, talk)
Ethereum	(CAV) SolCMC: Solidity Compiler’s Model Checker (, talk)
evaluation	(IJCAR) Vampire Getting Noisy: Will Random Bits Help Conquer Chaos? (System Description) (, talk)
Eventual non-negativity	(IJCAR) On Eventual Non-negativity and Positivity for the Weighted Sum of Powers of Matrices (, talk)
Evolution	(VardiFest) Natural Autoencoding (, talk)
Exact Learning	(DL) Actively Learning ELIQs in the Presence of DL-Lite-Horn Ontologies (, talk)
exclusion set	(CP) Finding Counterfactual Explanations through Constraint Relaxations (, talk)
experiments	(DL) Expressivity of Planning with Horn Description Logic Ontologies (Extended Abstract) (, talk) (DL) Efficient TBox Reasoning with Value Restrictions using the FL0wer Reasoner (Extended Abstract) (, talk)
Explainable AI	(DL) Evaluating the Interpretability of Threshold Operators (, talk)
Explanation	(IJCAR) Evonne: Interactive Proof Visualization for Description Logics (System Description) (, talk) (DL) Reverse Engineering of Temporal Queries with and without LTL Ontologies: First Steps (, talk) (DL) On the Eve of True Explainability for OWL Ontologies: Description Logic Proofs with Evee and Evonne (, talk) (DL) SAT-Based Axiom Pinpointing Revisited (, talk)
Explanations	(CAV) Explaining Hyperproperty Violations (, talk)
explicit definability	(DL) More on Interpolants and Explicit Definitions for Description Logics with Nominals and/or Role Inclusions (, talk)
expressive DLs	(DL) Expressivity of Planning with Horn Description Logic Ontologies (Extended Abstract) (, talk)
expressive power	(VardiFest) Data Complexity and Expressive Power of Ontological Reasoning Formalisms (, talk) (DL) Comonadic Semantics for Description Logics Games (, talk)
extended resolution	(PC) Exponential separations using guarded extension variables (, talk)
F
factor interpretation	(IJCAR) Binary Codes that do Not Preserve Primitivity (, talk)
Fair simulation	(VardiFest) Between Determinism and Nondeterminism (, talk)
fairness	(CAV) Synthesizing Fair Decision Trees via Iterative Constraint Solving (, talk)
Fairness Verification	(CAV) Verifying Fairness in Quantum Machine Learning (, talk)
Farkas' Lemma	(CAV) Affine Loop Invariant Generation via Matrix Algebra (, talk)
fault isolation	(CAV) End-to-end Mechanised Proof of an eBPF Virtual Machine for Microcontrollers (, talk)
feature extraction	(CP) Automated SAT Problem Feature Extraction using 1 Convolutional Autoencoders (, talk)
Filtering algorithm	(CP) Explaining Propagation for Gini and Spread with Variable Mean (Extended Abstract) (, talk)
finite axiomatizability	(IJCAR) Finite Two-Dimensional Proof Systems for Non-finitely Axiomatizable Logics (, talk)
Finite model theory	(VardiFest) Data Path Queries over Embedded Graph Databases (, talk) (VardiFest) Strategy Logic: Origin, Results, and Open Questions (, talk)
finite-variable logics	(VardiFest) From Kochen-Specker to Feder-Vardi (, talk)
firmware	(VardiFest) Moshe Vardi and Intel Corporation: Long and Fruitful Collaboration (, talk)
first-order logic	(IJCAR) Connection-Minimal Abduction in EL via Translation to FOL (, talk) (IJCAR) Semantic Relevance (, talk) (VardiFest) Approximations of Certain Answers in First-Order Logic (, talk) (DL) Connection-minimal Abduction in EL via translation to FOL (Extended Abstract) (, talk)
first-order logic with equality	(IJCAR) SCL(EQ): SCL for First-Order Logic with Equality (, talk)
First-order LTL	(FoMLAS) Formal Specification for Learning-Enabled Autonomous Systems (, talk)
first-order theorem proving	(IJCAR) Ground Joinability and Connectedness in the Superposition Calculus (, talk)
fixed point theory	(CAV) The Lattice-Theoretic Essence of Property Directed Reachability Analysis (, talk)
Fixed-domain semantics	(DL) AGM Revision in Description Logics Under Fixed-Domain Semantics (, talk)
fixpoint logic	(VardiFest) Fixpoint Logics, Relational Machines, and Computational Complexity (, talk)
FL0 and FLbot	(DL) Efficient TBox Reasoning with Value Restrictions using the FL0wer Reasoner (Extended Abstract) (, talk)
Forgetting	(DL) On the Eve of True Explainability for OWL Ontologies: Description Logic Proofs with Evee and Evonne (, talk) (DL) Fine-Grained Forgetting for the Description Logic ALC (, talk)
Formal	(VardiFest) Moshe Vardi and Intel Corporation: Long and Fruitful Collaboration (, talk)
formal logic	(FMBC) Proofgold: Blockchain for Formal Methods (, talk)
formal methods	(VardiFest) Capturing abscondings (, talk) (CAV) MoGym: Using Formal Models for Training and Verifying Decision-making Agents (, talk) (CAV) Capture, Analyze, Diagnose: Realizability Checking of Requirements in FRET (, talk) (FMBC) Multi: a Formal Playground for Smart Multi-contract interaction (, talk) (FMBC) Human and machine-readable models of state machines for the Cardano ledger (, talk)
Formal specification	(FoMLAS) Formal Specification for Learning-Enabled Autonomous Systems (, talk)
formal verification	(FoMLAS) VPN: Verification of Poisoning in Neural Networks (, talk) (FoMLAS) An Abstraction-Refinement Approach to Verifying Convolutional Neural Networks (, talk) (FoMLAS) Neural Network Verification with Proof Production (, talk) (FoMLAS) Neural Networks in Imandra: Matrix Representation as a Verification Choice (, talk) (FoMLAS) Goal-Aware RSS for Complex Scenarios via Program Logic (, talk) (VardiFest) The Safety Fragment of LTL (, talk) (CAV) Reachability of Koopman Linearized Systems Using Random Fourier Feature Observables and Polynomial Zonotope Refinement (, talk) (CAV) Hemiola: A DSL and Verification Tools to Guide Design and Proof of Hierarchical Cache-Coherence Protocols (, talk) (FMBC) Finding smart contract vulnerabilities with ConCert's property-based testing framework (, talk) (FMBC) Human and machine-readable models of state machines for the Cardano ledger (, talk) (FMBC) FAT CAT: Formal Acceptance Testing of Contracts for Administering Tokens (, talk)
formalization	(WST) Efficient Formalization of Simplification Orders ()
Formula Simplification	(IJCAR) Formula Simplification via Invariance Detection by Algebraically Indexed Types (, talk)
free-choice nets	(CAV) Verifying generalised and structural soundness of workflow nets via relaxations (, talk)
Functional correctness verification	(CAV) Verified Erasure Correction in Coq with MathComp and VST (, talk)
functional programming	(FoMLAS) Neural Networks in Imandra: Matrix Representation as a Verification Choice (, talk) (CAV) Automated Expected Amortised Cost Analysis of Probabilistic Data Structures (, talk)
Fuzz Testing	(CAV) Murxla: A Modular and Highly Extensible API Fuzzer for SMT Solvers (, talk) (CAV) Randomized Synthesis for Diversity and Cost Constraints with Control Improvisation (, talk)
Fuzzy proximity relations	(IJCAR) A Framework for Approximate Generalization in Quantitative Theories (, talk)
G
game	(VardiFest) Bisimulation Games Played in Fibered Categories (, talk)
game theory	(VardiFest) Capturing abscondings (, talk) (FMBC) Automating Security Analysis of Off-Chain Protocols (, talk)
games	(CAV) Reasoning about Data Trees using CHCs (, talk) (DL) Comonadic Semantics for Description Logics Games (, talk)
gang membership	(VardiFest) A Toast for Moshe at the FLoC VardiFest (, talk)
Gauss-Jordan Elimination	(POS) Combining CDCL, Gauss-Jordan Elimination, and Proof Generation (, talk)
generalization	(IJCAR) A Framework for Approximate Generalization in Quantitative Theories (, talk) (DL) A new dimension to generalization: computing temporal EL concepts from positive examples (Extended Abstract) (, talk)
generalization guarantees	(CP) Improved Sample Complexity Bounds for Branch-and-Cut (, talk)
generalized soundness	(CAV) Verifying generalised and structural soundness of workflow nets via relaxations (, talk)
Generating functions	(CAV) Does a Program Yield the Right Distribution? Verifying Probabilistic Programs via Generating Functions (, talk)
Geometry Problem Solving	(IJCAR) Formula Simplification via Invariance Detection by Algebraically Indexed Types (, talk)
Gini index	(CP) Explaining Propagation for Gini and Spread with Variable Mean (Extended Abstract) (, talk)
graph databases	(VardiFest) Rewriting of Regular Path Queries: The first paper of the four Italians (, talk) (VardiFest) Rewriting, Answering, and Losslessness: A Clarification by the “Four Italians” (, talk)
Graph games	(VardiFest) Between Determinism and Nondeterminism (, talk)
Graph Neural Networks	(FoMLAS) Scalable Verification of GNN-based Job Schedulers (, talk)
graph theory	(VardiFest) Capturing abscondings (, talk)
ground joinability	(IJCAR) Ground Joinability and Connectedness in the Superposition Calculus (, talk)
Gödel logic	(IJCAR) Paraconsistent Gödel Modal Logic (, talk)
H
hardware	(VardiFest) Moshe Vardi and Intel Corporation: Long and Fruitful Collaboration (, talk) (CAV) Hemiola: A DSL and Verification Tools to Guide Design and Proof of Hierarchical Cache-Coherence Protocols (, talk)
Hardware Verification	(VardiFest) Bridging Practice and Theory in SAT: Moshe Vardi the Catalyst (, talk)
Haskell	(IJCAR) Synthetic Tableaux: Minimal Tableau Search Heuristics (, talk)
Heuristic function construction	(CP) Extended Abstract: Acquiring Maps of Interrelated Conjectures on Sharp Bounds (, talk)
Hierarchical Models	(CAV) Abstraction-Refinement for Hierarchical Probabilistic Models (, talk)
Higher-order logic	(IJCAR) Lash 1.0 (System Description) (, talk)
higher-order term rewriting	(WST) Tuple Interpretations and Applications to Higher-Order Runtime Complexity (, talk) (WST) A transitive HORPO for curried systems (, talk)
Hilbert-style proof systems	(IJCAR) Finite Two-Dimensional Proof Systems for Non-finitely Axiomatizable Logics (, talk)
hitting formulas	(PC) Are Hitting Formulas Hard for Resolution? (, talk)
homomorphic encryption	(CAV) Oblivious Online Monitoring for Safety LTL Specification via Fully Homomorphic Encryption (, talk)
Horn-fragments	(DL) Efficient TBox Reasoning with Value Restrictions using the FL0wer Reasoner (Extended Abstract) (, talk)
hybrid systems	(VardiFest) Towards Combination of Logic and Calculus for Near-Optimal Planning in Relational Hybrid Systems (, talk)
Hyperliveness	(CAV) Software Verification of Hyperproperties Beyond k-Safety (, talk)
HyperLTL	(CAV) Software Verification of Hyperproperties Beyond k-Safety (, talk)
Hyperproperties	(CAV) Software Verification of Hyperproperties Beyond k-Safety (, talk) (CAV) Explaining Hyperproperty Violations (, talk)
Hypersequents	(IJCAR) Cyclic Proofs, Hypersequents, and Transitive Closure Logic (, talk)
I
iALC	(DL) A Labelled Natural Deduction System for an Intuitionistic Description Logic with Nominals (, talk)
Imandra	(FoMLAS) Neural Networks in Imandra: Matrix Representation as a Verification Choice (, talk)
incomplete information	(VardiFest) Approximations of Certain Answers in First-Order Logic (, talk)
inconsistency-tolerant semantics	(DL) Querying Inconsistent Prioritized Data with ORBITS: Algorithms, Implementation, and Experiments (Extended Abstract) (, talk)
infeasibility	(IJCAR) Term Ordering for Non-Reachability of (Conditional) Rewriting (, talk)
Information Flow	(CAV) Information Flow Guided Synthesis (, talk)
Information leakage	(CAV) A Scalable Shannon Entropy Estimator (, talk)
inherently weak automata	(CAV) Complementing Büchi Automata with Ranker (, talk)
Inner-approximation	(CAV) RINO: Robust INner and Outer Approximated Reachability of Neural Networks Controlled Systems (, talk)
Integer Difference Logic	(CAV) Local Search For SMT on Linear Integer Arithmetic (, talk)
integer programming	(CP) Improved Sample Complexity Bounds for Branch-and-Cut (, talk)
Integer Programs	(WST) Improved Automatic Complexity Analysis of Integer Programs (, talk) (IJCAR) Automatic Complexity Analysis of Integer Programs via Triangular Weakly Non-Linear Loops (, talk)
integer transition systems	(WST) A Calculus for Modular Non-Termination Proofs by Loop Acceleration (, talk) (IJCAR) Proving Non-Termination and Lower Runtime Bounds with LoAT (System Description) (, talk)
Interaction	(VardiFest) Natural Autoencoding (, talk)
Interactive theorem proving	(CAV) Verified Erasure Correction in Coq with MathComp and VST (, talk)
Internet of Things	(CAV) Oblivious Online Monitoring for Safety LTL Specification via Fully Homomorphic Encryption (, talk)
Interpretability	(DL) Evaluating the Interpretability of Threshold Operators (, talk)
Intuitionistic Logic	(DL) A Labelled Natural Deduction System for an Intuitionistic Description Logic with Nominals (, talk)
Invariance	(IJCAR) Formula Simplification via Invariance Detection by Algebraically Indexed Types (, talk)
Invariant synthesis	(CAV) Data-driven Numerical Invariant Synthesis with Automatic Generation of Attributes (, talk)
Isabelle/HOL	(WST) Efficient Formalization of Simplification Orders () (WST) CeTA – A certifier for termCOMP 2022 (, talk) (IJCAR) Binary Codes that do Not Preserve Primitivity (, talk) (IJCAR) Rensets and Renaming-Based Recursion for Syntax with Bindings (, talk)
J
JSON documents	(DL) Accessing Document Data Sources using Referring Expression Types (, talk)
Justifiable Exceptions	(DL) Reasoning on Multi-Relational Contextual Hierarchies via Answer Set Programming with Algebraic Measures (, talk)
justifications	(IJCAR) Hypergraph-Based Inference Rules for Computing EL+-Ontology Justifications (, talk)
K
k-consistency	(VardiFest) From Kochen-Specker to Feder-Vardi (, talk)
knapsack	(PC) On vanishing sums of roots of unity in polynomial calculus and sum-of-squares (an extended abstract) (, talk)
Knowledge Acquisition	(VardiFest) Logic-driven approaches for smart, safe and energy-efficient aviation (, talk)
Knowledge compilation	(VardiFest) LTLf Synthesis as AND-OR Graph Search: Knowledge Compilation at Work (, talk) (CP) Symmetry breaking and Knowledge Compilation (, talk)
Knowledge Diversity	(DL) Modelling Multiple Perspectives by Standpoint-Enhanced DLs (, talk)
Knowledge Integration	(DL) Modelling Multiple Perspectives by Standpoint-Enhanced DLs (, talk)
knowledge representation	(DL) Advanced languages of terms for ontologies (, talk)
Koopman operator	(CAV) Reachability of Koopman Linearized Systems Using Random Fourier Feature Observables and Polynomial Zonotope Refinement (, talk)
L
Lambek Calculus	(IJCAR) Non-associative, Non-commutative Multi-Modal Linear Logic (, talk)
Language inclusion	(CAV) FORQ-based Language Inclusion Formal Testing (, talk)
languages	(VardiFest) Logic and Languages for Representation Learning (, talk)
Large Neighbourhood Search	(CP) Large Neighborhood Search for Robust Solutions for Constraint Satisfaction Problems with Ordered Domains (, talk)
lattice theory	(CAV) The Lattice-Theoretic Essence of Property Directed Reachability Analysis (, talk)
law enforcement	(VardiFest) Capturing abscondings (, talk)
Lazy clause generation	(CP) Explaining Propagation for Gini and Spread with Variable Mean (Extended Abstract) (, talk)
Le\'sniewski	(IJCAR) Le\'sniewski's Ontology -- Proof-Theoretic Characterization (, talk)
learning from examples	(DL) A new dimension to generalization: computing temporal EL concepts from positive examples (Extended Abstract) (, talk)
Learning-enabled systems	(FoMLAS) Formal Specification for Learning-Enabled Autonomous Systems (, talk)
Least General Generalizations	(DL) Actively Learning ELIQs in the Presence of DL-Lite-Horn Ontologies (, talk)
ledger	(FMBC) Human and machine-readable models of state machines for the Cardano ledger (, talk)
ledger model	(FMBC) Determinism of ledger updates (, talk)
Legal Contracts	(VardiFest) Checking Legal Contracts - On a Not So Usual Application of Mechanized Logic (, talk)
Limit-Deterministic Buchi Automata	(VardiFest) An Automata-Theoretic Approach to Model-Free Reinforcement Learning (, talk)
Linear Approximation	(CAV) Example Guided Synthesis of Linear Approximations for Neural Network Verification (, talk)
Linear Arithmetic	(IJCAR) An Efficient Subsumption Test Pipeline for BS(LRA) Clauses (, talk)
Linear Bounding	(CAV) Example Guided Synthesis of Linear Approximations for Neural Network Verification (, talk)
linear constraints	(CP) Selecting SAT Encodings for Pseudo-Boolean and Linear Integer Constraints (, talk)
Linear dynamical systems	(IJCAR) On Eventual Non-negativity and Positivity for the Weighted Sum of Powers of Matrices (, talk)
Linear Integer Arithmetic	(CAV) Local Search For SMT on Linear Integer Arithmetic (, talk)
Linear Logic	(IJCAR) Non-associative, Non-commutative Multi-Modal Linear Logic (, talk)
Linear Loops	(WST) Deciding Termination of Uniform Loops with Polynomial Parameterized Complexity (, talk)
Linear recurrence sequences	(IJCAR) On Eventual Non-negativity and Positivity for the Weighted Sum of Powers of Matrices (, talk)
linear temporal logic	(DL) Reverse Engineering of Temporal Queries with and without LTL Ontologies: First Steps (, talk)
Linear Time	(VardiFest) A Short Talk Proposal for the VardiFest "On the Not So Unusual Effectiveness of Logic" (, talk)
Linear Time Logic on Finite Traces	(VardiFest) LTLf? It's Easy! Precisely! (, )
Linear-time Temporal Logic on Finite and Infinite Traces	(VardiFest) LTLf Synthesis Under Environment Specifications (, talk)
Local robustness	(FoMLAS) A Cascade of Checkers for Run-time Certification of Local Robustness (, talk)
Local Search	(CAV) Local Search For SMT on Linear Integer Arithmetic (, talk)
local verification	(CAV) Shared Certificates for Neural Network Verification (, talk)
logic	(VardiFest) Logic and Languages for Representation Learning (, talk) (VardiFest) From Logic to Neurosymbolic AI (, talk) (VardiFest) On the Effectiveness of Logic in Algorithmic Graph Theory (, talk) (VardiFest) Bisimulation Games Played in Fibered Categories (, talk) (VardiFest) Logic-driven approaches for smart, safe and energy-efficient aviation (, talk)
Logic and finite model theory	(VardiFest) To Count or Not to Count: A Personal Perspective (, talk)
Logic and Law	(VardiFest) Checking Legal Contracts - On a Not So Usual Application of Mechanized Logic (, talk)
logic programming	(DL) Advanced languages of terms for ontologies (, talk)
Logical theories	(VardiFest) Data Path Queries over Embedded Graph Databases (, talk)
Logics for Multi-Agent Systems	(VardiFest) Automated Synthesis of Mechanisms (, talk)
Logics for the strategic reasoning	(VardiFest) Formal Aspects of Strategic Reasoning in MAS (, talk)
loop acceleration	(WST) A Calculus for Modular Non-Termination Proofs by Loop Acceleration (, talk) (IJCAR) Proving Non-Termination and Lower Runtime Bounds with LoAT (System Description) (, talk)
Loop Invariant Generation	(CAV) Affine Loop Invariant Generation via Matrix Algebra (, talk)
Loop termination	(VardiFest) Algorithms, Complexity, Verification: From Cook and Karp to Vardi; or, a Brief Glimpse of the Skolem Landscape (, talk)
Loss Functions	(FoMLAS) Differentiable Logics for Neural Network Training and Verification (, talk)
losslessness	(VardiFest) Rewriting, Answering, and Losslessness: A Clarification by the “Four Italians” (, talk)
lower bounds	(PC) QCDCL with Cube Learning or Pure Literal Elimination – What is best? (, talk)
lower runtime bounds	(IJCAR) Proving Non-Termination and Lower Runtime Bounds with LoAT (System Description) (, talk)
LTL	(VardiFest) SAT-based Reasoning Techniques for LTL over Finite and Infinite Traces (, talk) (VardiFest) The Safety Fragment of LTL (, talk) (VardiFest) An Automata-Theoretic Approach to Model-Free Reinforcement Learning (, talk) (VardiFest) Little Tricky Logic: Misconceptions in the Understanding of LTL (, talk) (CAV) From Spot 2.0 to Spot 2.10: What's New? (, talk)
LTL model checking	(VardiFest) To Count or Not to Count: A Personal Perspective (, talk)
LTL over finite traces	(VardiFest) SAT-based Reasoning Techniques for LTL over Finite and Infinite Traces (, talk)
LTLf	(VardiFest) LTLf Synthesis as AND-OR Graph Search: Knowledge Compilation at Work (, talk)
M
machine learning	(IJCAR) Guiding an Automated Theorem Prover with Neural Rewriting (, talk) (FoMLAS) Self-Correcting Neural Networks For Safe Classification (, talk) (VardiFest) From Logic to Neurosymbolic AI (, talk) (CP) Selecting SAT Encodings for Pseudo-Boolean and Linear Integer Constraints (, talk)
Machine Learning Compiler	(CAV) SMT-based Translation Validation for Machine Learning Compiler (, talk)
machine learning theory	(CP) Improved Sample Complexity Bounds for Branch-and-Cut (, talk)
magic wand	(CAV) Sound Automation of Magic Wands (, talk)
Manufacturing	(VardiFest) Synthesis of plans for teams of manufacturing robots (, talk)
Marabou	(FoMLAS) Vehicle: A High-Level Language for Embedding Logical Specifications in Neural Networks (, talk)
Markov decision processes	(VardiFest) Strategy synthesis for Global Window PCTL (, talk) (CAV) Abstraction-Refinement for Hierarchical Probabilistic Models (, talk) (CAV) PAC Statistical Model Checking of Mean Payoff in Discrete- and Continuous-Time MDP (, talk)
Martingales	(CAV) Sound and Complete Certificates for Quantitative Termination Analysis of Probabilistic Programs (, talk)
masking	(CP) Optimized Code Generation against Power Side Channels (, talk)
Match-bounds	(WST) Approximating Relative Match-Bounds (, talk)
Mathematics of computing	(CP) Extended Abstract: Acquiring Maps of Interrelated Conjectures on Sharp Bounds (, talk) (CP) A Boolean Formula Seeker in the Context of Acquiring Maps of Interrelated Conjectures on Sharp Bounds (, talk)
Matrix Algebra	(CAV) Affine Loop Invariant Generation via Matrix Algebra (, talk)
maximum satisfiability	(IJCAR) Clause Redundancy and Preprocessing in Maximum Satisfiability (, talk)
MaxSAT	(IJCAR) Clause Redundancy and Preprocessing in Maximum Satisfiability (, talk)
Mazurkiewicz Traces	(CAV) Synthesis and Analysis of Petri Nets from Causal Specifications (, talk)
MDD	(CP) CNF Encodings of Binary Constraint Trees (Extended Abstract) (, talk)
Mean payoff	(CAV) PAC Statistical Model Checking of Mean Payoff in Discrete- and Continuous-Time MDP (, talk)
Mechanism Design	(VardiFest) Automated Synthesis of Mechanisms (, talk)
Mechanized Logic	(VardiFest) Checking Legal Contracts - On a Not So Usual Application of Mechanized Logic (, talk)
message passing	(VardiFest) Modelling with Reconfigurable Communication Interfaces (, talk) (FMBC) Designing EUTxO smart contracts as communicating state machines: the case of simulating accounts (, talk)
meta-programming	(FMBC) Human and machine-readable models of state machines for the Cardano ledger (, talk)
Minimal Independent Sets	(VardiFest) Bridging Practice and Theory in SAT: Moshe Vardi the Catalyst (, talk)
Minimal Modification	(FoMLAS) Minimal Multi-Layer Modifications of Deep Neural Networks (, talk)
Minimal tableau	(IJCAR) Synthetic Tableaux: Minimal Tableau Search Heuristics (, talk)
minimal unsastisfiable set	(IJCAR) Semantic Relevance (, talk)
minimality criterion	(IJCAR) Connection-Minimal Abduction in EL via Translation to FOL (, talk) (DL) Connection-minimal Abduction in EL via translation to FOL (Extended Abstract) (, talk)
misconceptions	(VardiFest) Little Tricky Logic: Misconceptions in the Understanding of LTL (, talk)
Mixed-Integer Programming	(CP) Solving the Constrained Single-Row Facility Layout Problem with Decision Diagrams (Extended Abstract) (, talk)
modal logic	(IJCAR) Effective Semantics for the Modal Logics K and KT via Non-deterministic Matrices (, talk) (IJCAR) Local Reductions for the Modal Cube (, talk)
Modal logics	(IJCAR) Paraconsistent Gödel Modal Logic (, talk)
model checking	(VardiFest) Formal Aspects of Strategic Reasoning in MAS (, talk) (VardiFest) Modelling with Reconfigurable Communication Interfaces (, talk) (VardiFest) A Short Talk Proposal for the VardiFest "On the Not So Unusual Effectiveness of Logic" (, talk) (CAV) Trainify: A CEGAR-Driven Training and Verification Framework for Safe Deep Reinforcement Learning (, talk) (CAV) The Lattice-Theoretic Essence of Property Directed Reachability Analysis (, talk) (CAV) Explaining Hyperproperty Violations (, talk) (CAV) STLmc: Robust STL Model Checking of Hybrid Systems using SMT (, talk)
Model counting	(CP) Extended Abstract: Constraint Acquisition Based on Solution Counting (, talk) (CAV) Randomized Synthesis for Diversity and Cost Constraints with Control Improvisation (, talk)
Model-Checking	(CAV) Software Verification of Hyperproperties Beyond k-Safety (, talk)
Model-Free Reinforcement Learning	(VardiFest) An Automata-Theoretic Approach to Model-Free Reinforcement Learning (, talk)
Modular Reasoning	(DL) Next Steps for ReAD: Modules for Classification Optimisation (, talk)
Module checking	(VardiFest) Formal Aspects of Strategic Reasoning in MAS (, talk)
monadic second-order logic	(CAV) Reasoning about Data Trees using CHCs (, talk)
Most specific concept	(DL) Optimal ABox Repair w.r.t. Static EL TBoxes: from Quantified ABoxes back to ABoxes (Extended Abstract) (, talk)
MSC Languages	(CAV) Synthesis and Analysis of Petri Nets from Causal Specifications (, talk)
Multi-Agent Path Finding	(CP) Solving the Non-Crossing MAPF for non point-sized robots (, talk)
Multi-agent systems	(VardiFest) Formal Aspects of Strategic Reasoning in MAS (, talk)
Multi-Agent Systems (MAS)	(VardiFest) An Epistemic Logic for modelling Cooperative Agents (, talk)
Multi-Layer Modification	(FoMLAS) Minimal Multi-Layer Modifications of Deep Neural Networks (, talk)
multi-modal verification	(CAV) UCLID5: Multi-Modal Formal Modeling, Verification, and Synthesis (, talk)
Multi-Threaded Solving	(POS) Scalable Proof Producing Multi-Threaded SAT Solving with Gimsatul through Sharing instead of Copying Clauses (, talk)
multiparty communication complexity	(PC) Proof complexity of natural formulas via communication arguments (, talk)
Music generation	(CP) Combining Reinforcement Learning and Constraint Programming for Sequence-Generation Tasks with Hard Constraints - Extended Abstract (, talk)
N
Natural Deduction	(DL) A Labelled Natural Deduction System for an Intuitionistic Description Logic with Nominals (, talk)
Natural Language Understanding	(FoMLAS) Why Robust Natural Language Understanding is a Challenge (, talk)
Neural network	(FoMLAS) Tight Neural Network Verification via Semidefinite Relaxations and Linear Reformulations (, talk) (CAV) Verifying Neural Networks Against Backdoor Attacks (, talk)
Neural Network Compression	(FoMLAS) CEG4N: Counter-Example Guided Neural Network Quantization Refinement (, talk)
Neural Network Equivalence	(FoMLAS) CEG4N: Counter-Example Guided Neural Network Quantization Refinement (, talk)
Neural Network Modification	(FoMLAS) Minimal Multi-Layer Modifications of Deep Neural Networks (, talk)
Neural Network Verification	(FoMLAS) Scalable Verification of GNN-based Job Schedulers (, talk) (FoMLAS) An Abstraction-Refinement Approach to Verifying Convolutional Neural Networks (, talk) (CAV) Shared Certificates for Neural Network Verification (, talk) (CAV) Example Guided Synthesis of Linear Approximations for Neural Network Verification (, talk)
Neural Networks	(FoMLAS) VPN: Verification of Poisoning in Neural Networks (, talk) (FoMLAS) A Cascade of Checkers for Run-time Certification of Local Robustness (, talk) (FoMLAS) Verification-Aided Deep Ensemble Selection (, talk) (FoMLAS) An Abstraction-Refinement Approach to Verifying Convolutional Neural Networks (, talk) (FoMLAS) Vehicle: A High-Level Language for Embedding Logical Specifications in Neural Networks (, talk) (FoMLAS) Neural Network Verification with Proof Production (, talk) (FoMLAS) Differentiable Logics for Neural Network Training and Verification (, talk) (FoMLAS) Neural Networks in Imandra: Matrix Representation as a Verification Choice (, talk) (FoMLAS) Self-Correcting Neural Networks For Safe Classification (, talk) (FoMLAS) Formal Specification for Learning-Enabled Autonomous Systems (, talk) (CAV) Example Guided Synthesis of Linear Approximations for Neural Network Verification (, talk) (CAV) Neural Network Robustness as a Verification Property: A Principled Case Study (, talk)
Neural networks verification	(CAV) RINO: Robust INner and Outer Approximated Reachability of Neural Networks Controlled Systems (, talk)
Neurosymbolic AI	(VardiFest) From Logic to Neurosymbolic AI (, talk)
NFA/MDD constraint	(CP) CNF Encodings of Binary Constraint Trees (Extended Abstract) (, talk)
NMatrices	(IJCAR) Effective Semantics for the Modal Logics K and KT via Non-deterministic Matrices (, talk)
nominal logic	(IJCAR) Rensets and Renaming-Based Recursion for Syntax with Bindings (, talk)
Non-deterministic Semantics	(IJCAR) Effective Semantics for the Modal Logics K and KT via Non-deterministic Matrices (, talk) (IJCAR) Finite Two-Dimensional Proof Systems for Non-finitely Axiomatizable Logics (, talk)
Non-linear constraints	(CAV) Distilling Constraints in Zero-Knowledge Protocols (, talk)
Non-monotonic reasoning	(IJCAR) Sequent Calculi for Choice Logics (, talk)
Non-monotonic reasoning in DLs	(DL) Pointwise Circumscription in Description Logics (, talk)
Non-optimality of proof systems	(PC) Average-Case Hardness of Proving Tautologies and Theorems (, talk)
non-termination	(WST) A Calculus for Modular Non-Termination Proofs by Loop Acceleration (, talk) (IJCAR) Proving Non-Termination and Lower Runtime Bounds with LoAT (System Description) (, talk)
nonlinear real arithmetic	(IJCAR) Cooperating Techniques for Solving Nonlinear Arithmetic in the cvc5 SMT Solver (System Description) (, talk)
O
OBDA	(DL) Ontology-based Data Federation (Extended Abstract) (, talk)
Object-Centric Event Logs	(DL) Extraction of Object-Centric Event Logs through Virtual Knowledge Graphs (, talk)
off-chain channels	(FMBC) Automating Security Analysis of Off-Chain Protocols (, talk)
Omega Automata	(VardiFest) A Short Talk Proposal for the VardiFest "On the Not So Unusual Effectiveness of Logic" (, talk)
OMQA	(DL) Finding Good Proofs for Answers to Conjunctive Queries Mediated by Lightweight Ontologies (, talk)
online LTL monitoring	(CAV) Oblivious Online Monitoring for Safety LTL Specification via Fully Homomorphic Encryption (, talk)
ontologies	(DL) Concept Abduction for Description Logics (, talk) (DL) An API for DL Abduction Solvers (, talk) (DL) Hybrid MHS-MXP ABox Abduction Solver: First Emprical Results (, talk) (DL) Computing Concept Referring Expressions with Standard OWL Reasoners (, talk) (DL) Fine-Grained Forgetting for the Description Logic ALC (, talk)
ontology	(IJCAR) Hypergraph-Based Inference Rules for Computing EL+-Ontology Justifications (, talk) (IJCAR) Le\'sniewski's Ontology -- Proof-Theoretic Characterization (, talk)
Ontology Alignment	(DL) Modelling Multiple Perspectives by Standpoint-Enhanced DLs (, talk)
Ontology repair	(DL) Optimal ABox Repair w.r.t. Static EL TBoxes: from Quantified ABoxes back to ABoxes (Extended Abstract) (, talk)
Ontology-based data access	(DL) Extraction of Object-Centric Event Logs through Virtual Knowledge Graphs (, talk) (DL) Ontology-based Data Federation (Extended Abstract) (, talk)
ontology-mediated query	(DL) Reverse Engineering of Temporal Queries with and without LTL Ontologies: First Steps (, talk)
Ontology-mediated query answering	(DL) Complexity Landscape for Counting Queries (Extended abstract) (, talk)
Open Problems	(VardiFest) Strategy Logic: Origin, Results, and Open Questions (, talk)
optimal proof systems	(PC) Simulations between proof systems (, talk)
ordinary differential equations	(VardiFest) Towards Combination of Logic and Calculus for Near-Optimal Planning in Relational Hybrid Systems (, talk)
P
paraconsistency	(IJCAR) Finite Two-Dimensional Proof Systems for Non-finitely Axiomatizable Logics (, talk)
Parallel Reasoning	(POS) Scalable Proof Producing Multi-Threaded SAT Solving with Gimsatul through Sharing instead of Copying Clauses (, talk)
Parametric continuous-time Markov chains	(CAV) Sampling-Based Verification of CTMCs with Uncertain Rates (, talk)
parametric solution	(IJCAR) Binary Codes that do Not Preserve Primitivity (, talk)
Parity automata	(CAV) Divide-and-Conquer Determinization of Büchi Automata based on SCC Decomposition (, talk)
path orders	(IJCAR) Term Ordering for Non-Reachability of (Conditional) Rewriting (, talk)
Patient Transportation	(CP) Extended Abstract: Sequence Variables for Routing Problems (, talk)
PB solving	(CP) On PB Encodings for Constraint Problems (, talk)
PCTL	(VardiFest) Strategy synthesis for Global Window PCTL (, talk)
perfect matching	(PC) Proof complexity of natural formulas via communication arguments (, talk)
Perspectives	(DL) Modelling Multiple Perspectives by Standpoint-Enhanced DLs (, talk)
petri nets	(CAV) Synthesis and Analysis of Petri Nets from Causal Specifications (, talk) (CAV) Verifying generalised and structural soundness of workflow nets via relaxations (, talk)
pigeonhole principle	(IJCAR) Synthetic Tableaux: Minimal Tableau Search Heuristics (, talk) (POS) Towards the shortest DRAT proof of the Pigeonhole Principle (, talk)
Planning	(IJCAR) Actions over Core-Closed Knowledge Bases (, talk) (VardiFest) Logic-driven approaches for smart, safe and energy-efficient aviation (, talk) (DL) Expressivity of Planning with Horn Description Logic Ontologies (Extended Abstract) (, talk)
Poisoning attacks	(FoMLAS) VPN: Verification of Poisoning in Neural Networks (, talk)
polynomial calculus	(PC) On vanishing sums of roots of unity in polynomial calculus and sum-of-squares (an extended abstract) (, talk)
polynomial zonotopes	(CAV) Reachability of Koopman Linearized Systems Using Random Fourier Feature Observables and Polynomial Zonotope Refinement (, talk)
Portfolio parallel SAT solver	(POS) DPS: A Framework for Deterministic Parallel SAT Solvers (, talk)
power side channels	(CP) Optimized Code Generation against Power Side Channels (, talk)
Predicate Abstraction	(CAV) Software Verification of Hyperproperties Beyond k-Safety (, talk)
Preferences	(IJCAR) Sequent Calculi for Choice Logics (, talk)
preprocessing	(IJCAR) Clause Redundancy and Preprocessing in Maximum Satisfiability (, talk) (IJCAR) Preprocessing of Propagation Redundant Clauses (, talk)
preserving primitivity	(IJCAR) Binary Codes that do Not Preserve Primitivity (, talk)
prime implicates	(IJCAR) Connection-Minimal Abduction in EL via Translation to FOL (, talk) (DL) Connection-minimal Abduction in EL via translation to FOL (Extended Abstract) (, talk)
prioritized knowledge bases	(DL) Querying Inconsistent Prioritized Data with ORBITS: Algorithms, Implementation, and Experiments (Extended Abstract) (, talk)
Probabilistic model checking	(CAV) Abstraction-Refinement for Hierarchical Probabilistic Models (, talk) (CAV) Sampling-Based Verification of CTMCs with Uncertain Rates (, talk)
probabilistic programming	(CAV) Automated Expected Amortised Cost Analysis of Probabilistic Data Structures (, talk)
Probabilistic programs	(CAV) Data-Driven Invariant Learning for Probabilistic Programs (, talk) (CAV) Sound and Complete Certificates for Quantitative Termination Analysis of Probabilistic Programs (, talk) (CAV) Does a Program Yield the Right Distribution? Verifying Probabilistic Programs via Generating Functions (, talk) (CAV) Abstraction-Refinement for Hierarchical Probabilistic Models (, talk)
Procedure	(IJCAR) Reasoning About Vectors using an SMT Theory of Sequences (, talk)
Process Mining	(DL) Extraction of Object-Centric Event Logs through Virtual Knowledge Graphs (, talk)
Product Configuration	(POS) Dinosat: A SAT Solver with Native DNF Support (, talk)
Program equivalence	(CAV) Does a Program Yield the Right Distribution? Verifying Probabilistic Programs via Generating Functions (, talk)
program synthesis	(CP) Boolean Functional Synthesis and its Applications (, talk)
Program verification	(WST) A Calculus for Modular Non-Termination Proofs by Loop Acceleration (, talk) (VardiFest) Algorithms, Complexity, Verification: From Cook and Karp to Vardi; or, a Brief Glimpse of the Skolem Landscape (, talk) (CAV) Data-driven Numerical Invariant Synthesis with Automatic Generation of Attributes (, talk)
proof assistants	(CAV) Hemiola: A DSL and Verification Tools to Guide Design and Proof of Hierarchical Cache-Coherence Protocols (, talk)
proof checking	(VardiFest) Understandable Proofs of Unsatisfiability (, talk)
proof complexity	(PC) Proof complexity of CSP (, talk) (PC) Exponential separations using guarded extension variables (, talk) (PC) Average-Case Hardness of Proving Tautologies and Theorems (, talk) (PC) Proof complexity of natural formulas via communication arguments (, talk) (PC) Simulations between proof systems (, talk) (PC) QCDCL with Cube Learning or Pure Literal Elimination – What is best? (, talk)
proof methodology	(CAV) End-to-end Mechanised Proof of an eBPF Virtual Machine for Microcontrollers (, talk)
proof of unsatisfiability	(VardiFest) Understandable Proofs of Unsatisfiability (, talk) (POS) Towards the shortest DRAT proof of the Pigeonhole Principle (, talk)
proof presentation	(DL) Finding Good Proofs for Answers to Conjunctive Queries Mediated by Lightweight Ontologies (, talk)
Proof Production	(FoMLAS) Neural Network Verification with Proof Production (, talk)
Proof Theory	(DL) Uniform and Modular Sequent Systems for Description Logics (, talk)
proof-search	(IJCAR) SAT-based Proof Search in Intermediate Propositional Logics (, talk)
Proof-search heuristics	(IJCAR) Synthetic Tableaux: Minimal Tableau Search Heuristics (, talk)
proofgold	(FMBC) Proofgold: Blockchain for Formal Methods (, talk)
Proofs	(IJCAR) Flexible Proof Production in an Industrial-Strength SMT Solver (, talk) (IJCAR) Evonne: Interactive Proof Visualization for Description Logics (System Description) (, talk) (DL) On the Eve of True Explainability for OWL Ontologies: Description Logic Proofs with Evee and Evonne (, talk)
propagation redundancy	(IJCAR) Clause Redundancy and Preprocessing in Maximum Satisfiability (, talk)
propagation redundant proof	(IJCAR) Preprocessing of Propagation Redundant Clauses (, talk)
propagation strength	(CP) CNF Encodings of Binary Constraint Trees (Extended Abstract) (, talk)
Property Based Testing	(FMBC) Automatic generation of attacker contracts in Solidity (, talk)
property directed reachability analysis	(CAV) The Lattice-Theoretic Essence of Property Directed Reachability Analysis (, talk)
property language design	(VardiFest) Little Tricky Logic: Misconceptions in the Understanding of LTL (, talk)
Property-Based Testing	(FMBC) Finding smart contract vulnerabilities with ConCert's property-based testing framework (, talk)
Propositional Dynamic Logic	(IJCAR) Cyclic Proofs, Hypersequents, and Transitive Closure Logic (, talk)
propositional intermediate logics	(IJCAR) SAT-based Proof Search in Intermediate Propositional Logics (, talk)
propositional logic	(IJCAR) Semantic Relevance (, talk)
propositional proof systems	(PC) Simulations between proof systems (, talk)
Propositional satisfiability	(DL) SAT-Based Axiom Pinpointing Revisited (, talk)
Protégé Plugin	(DL) On the Eve of True Explainability for OWL Ontologies: Description Logic Proofs with Evee and Evonne (, talk)
pseudo-Boolean constraints	(CP) Selecting SAT Encodings for Pseudo-Boolean and Linear Integer Constraints (, talk)
Q
QBF	(PC) QCDCL with Cube Learning or Pure Literal Elimination – What is best? (, talk) (CP) Boolean Functional Synthesis and its Applications (, talk)
QPTIME	(VardiFest) Computability and Complexity over Finite Unordered Structures; e.g., Graphs (1979-1982) (, talk)
Quantified Information Flow	(CAV) A Scalable Shannon Entropy Estimator (, talk)
Quantitative reasoning	(VardiFest) Automata-Based Quantitative Reasoning (, talk)
Quantitative Synthesis	(CAV) Randomized Synthesis for Diversity and Cost Constraints with Control Improvisation (, talk)
Quantitative theories	(IJCAR) A Framework for Approximate Generalization in Quantitative Theories (, talk)
Quantitative verification	(CAV) Does a Program Yield the Right Distribution? Verifying Probabilistic Programs via Generating Functions (, talk)
Quantum Decision Model	(CAV) Verifying Fairness in Quantum Machine Learning (, talk)
Quantum Machine Learning	(CAV) Verifying Fairness in Quantum Machine Learning (, talk)
quantum mechanics	(VardiFest) From Kochen-Specker to Feder-Vardi (, talk)
Quantum Noise	(CAV) Verifying Fairness in Quantum Machine Learning (, talk)
Queries	(DL) Computing Concept Referring Expressions with Standard OWL Reasoners (, talk)
Query Evaluation	(VardiFest) Towards Algebraic Techniques for Descriptive Complexity (, talk)
query optimization	(DL) Ontology-based Data Federation (Extended Abstract) (, talk)
query rewriting	(VardiFest) Rewriting, Answering, and Losslessness: A Clarification by the “Four Italians” (, talk)
query-by-example	(DL) Reverse Engineering of Temporal Queries with and without LTL Ontologies: First Steps (, talk)
R
R1CS	(CAV) Distilling Constraints in Zero-Knowledge Protocols (, talk)
Rabin automata	(CAV) Divide-and-Conquer Determinization of Büchi Automata based on SCC Decomposition (, talk)
random Fourier features	(CAV) Reachability of Koopman Linearized Systems Using Random Fourier Feature Observables and Polynomial Zonotope Refinement (, talk)
randomization	(IJCAR) Vampire Getting Noisy: Will Random Bits Help Conquer Chaos? (System Description) (, talk)
randomized communication complexity	(PC) Proof complexity of natural formulas via communication arguments (, talk)
Randomized Planning	(CAV) Randomized Synthesis for Diversity and Cost Constraints with Control Improvisation (, talk)
Ranking Functions	(WST) Improved Automatic Complexity Analysis of Integer Programs (, talk) (WST) Automatic Complexity Analysis of (Probabilistic) Integer Programs via KoAT (, talk)
Rational Synthesis	(VardiFest) On the Extraordinary Effectiveness of Logic in Strategic Reasoning (, talk)
rationality	(VardiFest) That's All I know: On the Effectiveness of Logic in Game Theory (, talk)
reachability	(IJCAR) Term Ordering for Non-Reachability of (Conditional) Rewriting (, talk)
Reachability analysis	(CAV) Reachability of Koopman Linearized Systems Using Random Fourier Feature Observables and Polynomial Zonotope Refinement (, talk) (CAV) RINO: Robust INner and Outer Approximated Reachability of Neural Networks Controlled Systems (, talk)
reactive synthesis	(VardiFest) LTLf Synthesis as AND-OR Graph Search: Knowledge Compilation at Work (, talk) (VardiFest) Trace-view vs Strategy-view of the Environment in Reactive Synthesis (, )
Reactive systems	(VardiFest) Formal Aspects of Strategic Reasoning in MAS (, talk)
Realizability Checking	(CAV) Capture, Analyze, Diagnose: Realizability Checking of Requirements in FRET (, talk)
Reasoning	(VardiFest) Logic-driven approaches for smart, safe and energy-efficient aviation (, talk) (DL) Category-based Semantics for the Description Logic ALC and Reasoning (, talk) (DL) Concept Abduction for Description Logics (, talk)
reasoning about actions	(DL) Reasoning about actions with EL ontologies in a temporal action theory (Extended Abstract) (, talk)
Recollections	(VardiFest) To Count or Not to Count: A Personal Perspective (, talk)
reconfigurable interaction	(VardiFest) Modelling with Reconfigurable Communication Interfaces (, talk)
Recursive path ordering	(WST) A transitive HORPO for curried systems (, talk)
Reductions	(CAV) Even Faster Conflicts and Lazier Reductions for String Solvers (, talk)
Redundancy Elimination	(IJCAR) An Efficient Subsumption Test Pipeline for BS(LRA) Clauses (, talk)
Reed-Solomon coding	(CAV) Verified Erasure Correction in Coq with MathComp and VST (, talk)
Reentrancy Attack	(FMBC) Automatic generation of attacker contracts in Solidity (, talk)
referring expressions	(DL) Accessing Document Data Sources using Referring Expression Types (, talk)
Refutation calculus	(IJCAR) Sequent Calculi for Choice Logics (, talk)
Register automata	(VardiFest) Data Path Queries over Embedded Graph Databases (, talk)
Regular expressions	(VardiFest) Rewriting of Regular Path Queries: The first paper of the four Italians (, talk)
Regular path queries	(VardiFest) Data Path Queries over Embedded Graph Databases (, talk) (VardiFest) Rewriting of Regular Path Queries: The first paper of the four Italians (, talk) (VardiFest) Rewriting, Answering, and Losslessness: A Clarification by the “Four Italians” (, talk)
Reinforcement Learning	(CP) Combining Reinforcement Learning and Constraint Programming for Sequence-Generation Tasks with Hard Constraints - Extended Abstract (, talk) (CAV) PAC Statistical Model Checking of Mean Payoff in Discrete- and Continuous-Time MDP (, talk) (CAV) Specification-Guided Learning of Nash Equilibria with High Social Welfare (, talk) (CAV) MoGym: Using Formal Models for Training and Verifying Decision-making Agents (, talk)
relational complexity	(VardiFest) Fixpoint Logics, Relational Machines, and Computational Complexity (, talk)
relational databases	(VardiFest) Approximations of Certain Answers in First-Order Logic (, talk)
relational machines	(VardiFest) Fixpoint Logics, Relational Machines, and Computational Complexity (, talk)
relevance	(IJCAR) Semantic Relevance (, talk)
Repair of Neural Networks	(FoMLAS) Minimal Multi-Layer Modifications of Deep Neural Networks (, talk)
representation learning	(VardiFest) Logic and Languages for Representation Learning (, talk)
Reproducible parallel SAT solving	(POS) DPS: A Framework for Deterministic Parallel SAT Solvers (, talk)
Requirements Analysis	(CAV) Capture, Analyze, Diagnose: Realizability Checking of Requirements in FRET (, talk)
resolution	(PC) Exponential separations using guarded extension variables (, talk)
resolution complexity	(PC) Are Hitting Formulas Hard for Resolution? (, talk)
Resolution over linear equations	(PC) Proof complexity of natural formulas via communication arguments (, talk)
reverse engineering	(CAV) Abstraction Modulo Stability for Reverse Engineering (, talk)
Reverse engineering of queries	(DL) Reverse Engineering of Temporal Queries with and without LTL Ontologies: First Steps (, talk)
rewriting logic	(IJCAR) Equational Unification and Matching, and Symbolic Reachability Analysis in Maude 3.2 (System Description) (, talk)
Right barren	(WST) Approximating Relative Match-Bounds (, talk)
RNN	(CP) Combining Reinforcement Learning and Constraint Programming for Sequence-Generation Tasks with Hard Constraints - Extended Abstract (, talk)
Robust Compression	(FoMLAS) CEG4N: Counter-Example Guided Neural Network Quantization Refinement (, talk)
Robust Solutions	(CP) Large Neighborhood Search for Robust Solutions for Constraint Satisfaction Problems with Ordered Domains (, talk)
Robustness	(FoMLAS) RoMA: a Method for Neural Network Robustness Measurement and Assessment (, talk) (FoMLAS) Verification-Aided Deep Ensemble Selection (, talk) (CAV) Neural Network Robustness as a Verification Property: A Principled Case Study (, talk) (CAV) RINO: Robust INner and Outer Approximated Reachability of Neural Networks Controlled Systems (, talk)
Robustness degree	(CAV) STLmc: Robust STL Model Checking of Hybrid Systems using SMT (, talk)
Robustness Verification	(CAV) Example Guided Synthesis of Linear Approximations for Neural Network Verification (, talk)
roots of unity	(PC) On vanishing sums of roots of unity in polynomial calculus and sum-of-squares (an extended abstract) (, talk)
RSS	(FoMLAS) Goal-Aware RSS for Complex Scenarios via Program Logic (, talk)
Rule based temporal action logic	(DL) Reasoning about actions with EL ontologies in a temporal action theory (Extended Abstract) (, talk)
rule-based reasoning	(DL) Advanced languages of terms for ontologies (, talk)
Run-time checks	(FoMLAS) A Cascade of Checkers for Run-time Certification of Local Robustness (, talk)
Run-time enforcement	(FoMLAS) Self-Correcting Neural Networks For Safe Classification (, talk)
S
Safety	(FoMLAS) Self-Correcting Neural Networks For Safe Classification (, talk) (FoMLAS) Goal-Aware RSS for Complex Scenarios via Program Logic (, talk) (VardiFest) The Safety Fragment of LTL (, talk)
sample complexity	(CP) Improved Sample Complexity Bounds for Branch-and-Cut (, talk)
SAT encodings	(PC) Are Hitting Formulas Hard for Resolution? (, talk) (CP) On PB Encodings for Constraint Problems (, talk) (CP) Selecting SAT Encodings for Pseudo-Boolean and Linear Integer Constraints (, talk)
Sat Solver	(POS) Dinosat: A SAT Solver with Native DNF Support (, talk)
SAT Solving	(IJCAR) Preprocessing of Propagation Redundant Clauses (, talk) (POS) Scalable Proof Producing Multi-Threaded SAT Solving with Gimsatul through Sharing instead of Copying Clauses (, talk) (POS) SATViz: Real-Time Visualization of Clausal Proofs (, talk)
SAT-based algorithms	(DL) Querying Inconsistent Prioritized Data with ORBITS: Algorithms, Implementation, and Experiments (Extended Abstract) (, talk)
SAT-based reasoning	(VardiFest) SAT-based Reasoning Techniques for LTL over Finite and Infinite Traces (, talk)
satisfiability	(IJCAR) Decision Problems in a Logic for Reasoning about Reconfigurable Distributed Systems (, talk) (VardiFest) Understandable Proofs of Unsatisfiability (, talk)
satisfiability checking	(VardiFest) SAT-based Reasoning Techniques for LTL over Finite and Infinite Traces (, talk)
Satisfiability Modulo Theories	(IJCAR) Cooperating Techniques for Solving Nonlinear Arithmetic in the cvc5 SMT Solver (System Description) (, talk) (CAV) SolCMC: Solidity Compiler’s Model Checker (, talk) (CAV) Even Faster Conflicts and Lazier Reductions for String Solvers (, talk)
Satisfiability Modulo Theory	(CAV) SMT-based Translation Validation for Machine Learning Compiler (, talk)
Satisfiability Solvers	(VardiFest) Bridging Practice and Theory in SAT: Moshe Vardi the Catalyst (, talk)
saturation-based theorem proving	(IJCAR) Vampire Getting Noisy: Will Random Bits Help Conquer Chaos? (System Description) (, talk)
Scenario optimization	(CAV) Sampling-Based Verification of CTMCs with Uncertain Rates (, talk)
Schedulers	(FoMLAS) Scalable Verification of GNN-based Job Schedulers (, talk)
SDD	(VardiFest) LTLf Synthesis as AND-OR Graph Search: Knowledge Compilation at Work (, talk)
Search methodologies	(CP) Extended Abstract: Acquiring Maps of Interrelated Conjectures on Sharp Bounds (, talk) (CP) A Boolean Formula Seeker in the Context of Acquiring Maps of Interrelated Conjectures on Sharp Bounds (, talk)
secure blockchain	(FMBC) Automating Security Analysis of Off-Chain Protocols (, talk)
Secure Multi-Party Computation	(CAV) PoS4MPC: Automated Security Policy Synthesis for Secure Multi-Party Computation (, talk)
security	(CP) Optimized Code Generation against Power Side Channels (, talk)
Security Policy	(CAV) PoS4MPC: Automated Security Policy Synthesis for Secure Multi-Party Computation (, talk)
Security Verification	(CAV) PoS4MPC: Automated Security Policy Synthesis for Secure Multi-Party Computation (, talk)
self-adjusting data structures	(CAV) Automated Expected Amortised Cost Analysis of Probabilistic Data Structures (, talk)
Semantics	(DL) Category-based Semantics for the Description Logic ALC and Reasoning (, talk)
semi-deterministic automata	(CAV) Complementing Büchi Automata with Ranker (, talk)
Semidefinite programming	(FoMLAS) Tight Neural Network Verification via Semidefinite Relaxations and Linear Reformulations (, talk)
Sentence Embeddings	(FoMLAS) Why Robust Natural Language Understanding is a Challenge (, talk)
Sentential Decision Diagram	(CP) Symmetry breaking and Knowledge Compilation (, talk)
separation logic	(IJCAR) Decision Problems in a Logic for Reasoning about Reconfigurable Distributed Systems (, talk) (CAV) Sound Automation of Magic Wands (, talk)
separations	(PC) Exponential separations using guarded extension variables (, talk)
Sequence Variables	(CP) Extended Abstract: Sequence Variables for Routing Problems (, talk)
sequencing	(CP) Peel-and-Bound: Generating Stronger Relaxed Bounds with Multivalued Decision Diagrams (, talk)
Sequent Calculi	(IJCAR) Effective Semantics for the Modal Logics K and KT via Non-deterministic Matrices (, talk)
Sequent Calculus	(IJCAR) Sequent Calculi for Choice Logics (, talk) (IJCAR) Le\'sniewski's Ontology -- Proof-Theoretic Characterization (, talk) (DL) Uniform and Modular Sequent Systems for Description Logics (, talk)
Shannon Entropy	(CAV) A Scalable Shannon Entropy Estimator (, talk)
sheaves and cohomology	(VardiFest) From Kochen-Specker to Feder-Vardi (, talk)
Signal temporal logic	(CAV) STLmc: Robust STL Model Checking of Hybrid Systems using SMT (, talk)
simplification order	(WST) Efficient Formalization of Simplification Orders ()
simulations	(CAV) Abstraction Modulo Stability for Reverse Engineering (, talk)
situation calculus	(VardiFest) Towards Combination of Logic and Calculus for Near-Optimal Planning in Relational Hybrid Systems (, talk)
Skolem Problem	(VardiFest) Algorithms, Complexity, Verification: From Cook and Karp to Vardi; or, a Brief Glimpse of the Skolem Landscape (, talk)
Smart Contracts	(FMBC) Finding smart contract vulnerabilities with ConCert's property-based testing framework (, talk) (FMBC) Automatic generation of attacker contracts in Solidity (, talk) (FMBC) FAT CAT: Formal Acceptance Testing of Contracts for Administering Tokens (, talk)
smart-contracts	(FMBC) Multi: a Formal Playground for Smart Multi-contract interaction (, talk)
SMT	(IJCAR) Flexible Proof Production in an Industrial-Strength SMT Solver (, talk) (IJCAR) CTL* Model Checking for Data-Aware Dynamic Systems with Arithmetic (, talk) (IJCAR) Reasoning About Vectors using an SMT Theory of Sequences (, talk) (CAV) STLmc: Robust STL Model Checking of Hybrid Systems using SMT (, talk) (CAV) Local Search For SMT on Linear Integer Arithmetic (, talk)
SMT solvers	(CAV) Reasoning about Data Trees using CHCs (, talk)
SMT Solving	(VardiFest) Checking Legal Contracts - On a Not So Usual Application of Mechanized Logic (, talk) (CAV) Murxla: A Modular and Highly Extensible API Fuzzer for SMT Solvers (, talk)
software engineering	(DL) An API for DL Abduction Solvers (, talk)
Software Verification	(CAV) Proof-guided Underapproximation Widening for Bounded Model Checking (, talk) (CAV) Software Verification of Hyperproperties Beyond k-Safety (, talk) (CAV) Playing Against Fair Adversaries in Stochastic Games with Total Rewards (, talk)
Solidity	(CAV) SolCMC: Solidity Compiler’s Model Checker (, talk)
Solution counting	(CP) Extended Abstract: Constraint Acquisition Based on Solution Counting (, talk)
sound and complete calculus	(IJCAR) SCL(EQ): SCL for First-Order Logic with Equality (, talk)
soundness	(CAV) Verifying generalised and structural soundness of workflow nets via relaxations (, talk)
Species Interaction Code	(VardiFest) Natural Autoencoding (, talk)
specification	(VardiFest) Moshe Vardi and Intel Corporation: Long and Fruitful Collaboration (, talk)
Spread constraint	(CP) Explaining Propagation for Gini and Spread with Variable Mean (Extended Abstract) (, talk)
stability	(CAV) Abstraction Modulo Stability for Reverse Engineering (, talk)
Standpoint	(DL) Modelling Multiple Perspectives by Standpoint-Enhanced DLs (, talk)
state machines	(FMBC) Designing EUTxO smart contracts as communicating state machines: the case of simulating accounts (, talk)
Statistical Model Checking	(CAV) PAC Statistical Model Checking of Mean Payoff in Discrete- and Continuous-Time MDP (, talk) (CAV) MoGym: Using Formal Models for Training and Verifying Decision-making Agents (, talk)
Statistical Verification	(CAV) Specification-Guided Learning of Nash Equilibria with High Social Welfare (, talk)
Stochastic Games	(CAV) Playing Against Fair Adversaries in Stochastic Games with Total Rewards (, talk)
Stochastic invariants	(CAV) Sound and Complete Certificates for Quantitative Termination Analysis of Probabilistic Programs (, talk)
Straight-line programs	(POS) Towards an Efficient CNF Encoding of Block Ciphers (, talk)
Strategic Reasoning	(VardiFest) Formal Aspects of Strategic Reasoning in MAS (, talk) (VardiFest) Automated Synthesis of Mechanisms (, talk)
Strategy Logic	(VardiFest) Formal Aspects of Strategic Reasoning in MAS (, talk) (VardiFest) On the Extraordinary Effectiveness of Logic in Strategic Reasoning (, talk) (VardiFest) Strategy Logic: Origin, Results, and Open Questions (, talk)
Strategy Scheduling	(IJCAR) Bayesian Ranking for Strategy Scheduling in Automated Theorem Provers (, talk)
String rewriting	(WST) Approximating Relative Match-Bounds (, talk) (WST) Certified Matchbox (, talk)
Strings	(CAV) Even Faster Conflicts and Lazier Reductions for String Solvers (, talk)
Strongly Connected Components	(CAV) Divide-and-Conquer Determinization of Büchi Automata based on SCC Decomposition (, talk)
Strongly Connected Components (SCCs)	(VardiFest) Divide-and-Conquer Determinization for B\"uchi Automata (, talk)
structural soundness	(CAV) Verifying generalised and structural soundness of workflow nets via relaxations (, talk)
Subexponentials	(IJCAR) Non-associative, Non-commutative Multi-Modal Linear Logic (, talk)
substitution	(IJCAR) Rensets and Renaming-Based Recursion for Syntax with Bindings (, talk)
Subsumption	(IJCAR) An Efficient Subsumption Test Pipeline for BS(LRA) Clauses (, talk)
sum-of-squares	(PC) On vanishing sums of roots of unity in polynomial calculus and sum-of-squares (an extended abstract) (, talk)
superposition	(IJCAR) Ground Joinability and Connectedness in the Superposition Calculus (, talk)
Survival of the Fitted	(VardiFest) Natural Autoencoding (, talk)
Symbolic Model Checking	(CAV) SolCMC: Solidity Compiler’s Model Checker (, talk)
symbolic reachability	(IJCAR) Equational Unification and Matching, and Symbolic Reachability Analysis in Maude 3.2 (System Description) (, talk)
symmetries	(PC) Are Hitting Formulas Hard for Resolution? (, talk)
Symmetry breaking	(CP) Symmetry breaking and Knowledge Compilation (, talk)
syntax with bindings	(IJCAR) Rensets and Renaming-Based Recursion for Syntax with Bindings (, talk)
Synthesis	(VardiFest) SAT-based Reasoning Techniques for LTL over Finite and Infinite Traces (, talk) (VardiFest) On the Extraordinary Effectiveness of Logic in Strategic Reasoning (, talk) (VardiFest) Synthesis of plans for teams of manufacturing robots (, talk) (VardiFest) Strategy synthesis for Global Window PCTL (, talk) (VardiFest) LTLf? It's Easy! Precisely! (, ) (CAV) PoS4MPC: Automated Security Policy Synthesis for Secure Multi-Party Computation (, talk) (CAV) UCLID5: Multi-Modal Formal Modeling, Verification, and Synthesis (, talk) (CAV) Specification-Guided Learning of Nash Equilibria with High Social Welfare (, talk) (CAV) Synthesizing Fair Decision Trees via Iterative Constraint Solving (, talk)
Synthesis under Environment Specifications	(VardiFest) LTLf Synthesis Under Environment Specifications (, talk)
Synthetic tableau	(IJCAR) Synthetic Tableaux: Minimal Tableau Search Heuristics (, talk)
T
Tableaux	(IJCAR) Goéland: A Concurrent Tableau-Based Theorem Prover (System Description) (, talk)
Temporal Logic	(VardiFest) On the Extraordinary Effectiveness of Logic in Strategic Reasoning (, talk)
Temporal logics	(VardiFest) Formal Aspects of Strategic Reasoning in MAS (, talk)
temporal reasoning	(VardiFest) On the Effectiveness of Logic in Algorithmic Graph Theory (, talk) (DL) A new dimension to generalization: computing temporal EL concepts from positive examples (Extended Abstract) (, talk)
term rewriting	(WST) Hydra Battles and AC Termination (, talk) (IJCAR) Term Ordering for Non-Reachability of (Conditional) Rewriting (, talk)
Termination	(WST) A transitive HORPO for curried systems (, talk) (WST) Approximating Relative Match-Bounds (, talk) (WST) Hydra Battles and AC Termination (, talk) (WST) Deciding Termination of Uniform Loops with Polynomial Parameterized Complexity (, talk) (WST) CeTA – A certifier for termCOMP 2022 (, talk) (WST) Certified Matchbox (, talk) (IJCAR) Term Ordering for Non-Reachability of (Conditional) Rewriting (, talk) (CAV) Sound and Complete Certificates for Quantitative Termination Analysis of Probabilistic Programs (, talk)
termination analysis	(WST) Efficient Formalization of Simplification Orders ()
Testing	(FMBC) A Domain Specific Language for Testing Consensus Implementations (, talk)
theorem prover	(FMBC) Multi: a Formal Playground for Smart Multi-contract interaction (, talk)
theorem proving	(IJCAR) Local Reductions for the Modal Cube (, talk) (IJCAR) Implicit Definitions with Differential Equations for KeYmaera X (System Description) (, talk) (FoMLAS) Goal-Aware RSS for Complex Scenarios via Program Logic (, talk)
theory of changes	(FMBC) Determinism of ledger updates (, talk)
Theory of Sequences	(IJCAR) Reasoning About Vectors using an SMT Theory of Sequences (, talk)
Threshold operators	(DL) Evaluating the Interpretability of Threshold Operators (, talk)
toasts	(VardiFest) A Toast for Moshe at the FLoC VardiFest (, talk)
tool	(CAV) From Spot 2.0 to Spot 2.10: What's New? (, talk)
TPTP	(IJCAR) Lash 1.0 (System Description) (, talk)
Training Deep Neural Networks	(VardiFest) A Solver + Gradient Descent Training Algorithm for Deep Neural Network (, )
transformation	(CAV) From Spot 2.0 to Spot 2.10: What's New? (, talk)
transition systems	(VardiFest) Modelling with Reconfigurable Communication Interfaces (, talk)
Transitive Closure Logic	(IJCAR) Cyclic Proofs, Hypersequents, and Transitive Closure Logic (, talk)
translation	(VardiFest) A Toast for Moshe at the FLoC VardiFest (, talk)
Translation validation	(CAV) SMT-based Translation Validation for Machine Learning Compiler (, talk)
Transmission maintenance scheduling	(CP) Extended Abstract for : Scheduling the Equipment Maintenance of an Electric Power Transmission Network using Constraint Programming (, talk)
tree search	(CP) Improved Sample Complexity Bounds for Branch-and-Cut (, talk)
tree-like proofs	(PC) Proof complexity of natural formulas via communication arguments (, talk)
trustworthy AI	(CP) Finding Counterfactual Explanations through Constraint Relaxations (, talk)
TSPTW	(CP) Extended Abstract: Sequence Variables for Routing Problems (, talk)
tuple interpretations	(WST) Tuple Interpretations and Applications to Higher-Order Runtime Complexity (, talk)
Two-dimensional logics	(IJCAR) Paraconsistent Gödel Modal Logic (, talk)
Type Theory	(IJCAR) Formula Simplification via Invariance Detection by Algebraically Indexed Types (, talk)
U
Uncertainty	(CAV) Sampling-Based Verification of CTMCs with Uncertain Rates (, talk)
Underapproximation widening	(CAV) Proof-guided Underapproximation Widening for Bounded Model Checking (, talk)
Undergraduate research project	(VardiFest) 12 Years and Counting: Samples from My Undergraduate Research Projec ()
Uniform Random Sampling	(CAV) Randomized Synthesis for Diversity and Cost Constraints with Control Improvisation (, talk)
Uniform sampling	(VardiFest) 12 Years and Counting: Samples from My Undergraduate Research Projec ()
upper runtime bounds	(IJCAR) Automatic Complexity Analysis of Integer Programs via Triangular Weakly Non-Linear Loops (, talk)
user studies	(VardiFest) Little Tricky Logic: Misconceptions in the Understanding of LTL (, talk)
User study	(DL) Evaluating the Interpretability of Threshold Operators (, talk)
UTXO	(FMBC) Human and machine-readable models of state machines for the Cardano ledger (, talk) (FMBC) Designing EUTxO smart contracts as communicating state machines: the case of simulating accounts (, talk)
V
Vardi	(VardiFest) Data Complexity and Expressive Power of Ontological Reasoning Formalisms (, talk)
Vardifest	(VardiFest) 12 Years and Counting: Samples from My Undergraduate Research Projec ()
Variable Neighborhood Search	(CP) Solving the Non-Crossing MAPF for non point-sized robots (, talk)
Variable Ordering heuristic	(CP) Exploiting Model Entropy to Make Branching Decisions in Constraint Programming (, talk)
Vehicle Routing	(CP) Extended Abstract: Sequence Variables for Routing Problems (, talk)
Verification	(IJCAR) Flexible Proof Production in an Industrial-Strength SMT Solver (, talk) (IJCAR) CTL* Model Checking for Data-Aware Dynamic Systems with Arithmetic (, talk) (IJCAR) Preprocessing of Propagation Redundant Clauses (, talk) (FoMLAS) Tight Neural Network Verification via Semidefinite Relaxations and Linear Reformulations (, talk) (FoMLAS) Vehicle: A High-Level Language for Embedding Logical Specifications in Neural Networks (, talk) (FoMLAS) Why Robust Natural Language Understanding is a Challenge (, talk) (FoMLAS) Differentiable Logics for Neural Network Training and Verification (, talk) (FoMLAS) Self-Correcting Neural Networks For Safe Classification (, talk) (VardiFest) Moshe Vardi and Intel Corporation: Long and Fruitful Collaboration (, talk) (VardiFest) Verifying Accuracy Claims of Differential Privacy Algorithms (, talk) (CAV) Verifying Neural Networks Against Backdoor Attacks (, talk) (CAV) Neural Network Robustness as a Verification Property: A Principled Case Study (, talk) (CAV) Software Verification of Hyperproperties Beyond k-Safety (, talk) (CAV) UCLID5: Multi-Modal Formal Modeling, Verification, and Synthesis (, talk)
verification of hybrid systems	(IJCAR) Implicit Definitions with Differential Equations for KeYmaera X (System Description) (, talk)
view-based query answering	(VardiFest) Rewriting, Answering, and Losslessness: A Clarification by the “Four Italians” (, talk)
view-based query processing	(VardiFest) Rewriting, Answering, and Losslessness: A Clarification by the “Four Italians” (, talk)
Virtual Knowledge Graph	(DL) Extraction of Object-Centric Event Logs through Virtual Knowledge Graphs (, talk)
virtual machines	(CAV) End-to-end Mechanised Proof of an eBPF Virtual Machine for Microcontrollers (, talk)
Visualization	(IJCAR) Evonne: Interactive Proof Visualization for Description Logics (System Description) (, talk) (POS) SATViz: Real-Time Visualization of Clausal Proofs (, talk)
W
Weakest pre-expectations	(CAV) Data-Driven Invariant Learning for Probabilistic Programs (, talk)
Weisfeiler-Leman	(VardiFest) From Kochen-Specker to Feder-Vardi (, talk)
Well-quasiorders	(CAV) FORQ-based Language Inclusion Formal Testing (, talk)
workflow nets	(CAV) Verifying generalised and structural soundness of workflow nets via relaxations (, talk)
X
XOR-CNF	(POS) Towards an Efficient CNF Encoding of Block Ciphers (, talk)
Z
ZDD	(VardiFest) Boolean Synthesis via Decision Diagrams (, talk)
ZK protocols	(CAV) Distilling Constraints in Zero-Knowledge Protocols (, talk)
ω
ω-automata	(CAV) From Spot 2.0 to Spot 2.10: What's New? (, talk)