FLOC 2022: FEDERATED LOGIC CONFERENCE 2022

A
Abramsky, Samson	(VardiFest) From Kochen-Specker to Feder-Vardi (, talk)
Agarwal, Chaitanya	(CAV) PAC Statistical Model Checking of Mean Payoff in Discrete- and Continuous-Time MDP (, talk)
Akshay, S.	(IJCAR) On Eventual Non-negativity and Positivity for the Weighted Sum of Powers of Matrices (, talk)
Albert, Elvira	(IJCAR) Using Automated Reasoning Techniques for Enhancing the Efficiency and Security of (Ethereum) Smart Contracts (, talk) (CAV) Distilling Constraints in Zero-Knowledge Protocols (, talk)
Alechina, Natasha	(VardiFest) Synthesis of plans for teams of manufacturing robots (, talk)
Alkmim, Bernardo	(DL) A Labelled Natural Deduction System for an Intuitionistic Description Logic with Nominals (, talk)
Alrabbaa, Christian	(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) (DL) Finding Good Proofs for Answers to Conjunctive Queries Mediated by Lightweight Ontologies (, talk)
Alt, Leonardo	(CAV) SolCMC: Solidity Compiler’s Model Checker (, talk)
Alur, Rajeev	(CAV) Specification-Guided Learning of Nash Equilibria with High Social Welfare (, talk)
Amir, Guy	(FoMLAS) Verification-Aided Deep Ensemble Selection (, talk)
Amir, Guy	(CAV) Neural Network Robustness as a Verification Property: A Principled Case Study (, talk)
Annenkov, Danil	(FMBC) Finding smart contract vulnerabilities with ConCert's property-based testing framework (, talk)
Appel, Andrew W.	(CAV) Verified Erasure Correction in Coq with MathComp and VST (, talk)
Arbelaez, Alejandro	(CP) Large Neighborhood Search for Robust Solutions for Constraint Satisfaction Problems with Ordered Domains (, talk)
Arnaboldi, Luca	(FoMLAS) Vehicle: A High-Level Language for Embedding Logical Specifications in Neural Networks (, talk) (FoMLAS) Why Robust Natural Language Understanding is a Challenge (, talk)
Arvind,	(CAV) Hemiola: A DSL and Verification Tools to Guide Design and Proof of Hierarchical Cache-Coherence Protocols (, talk)
Ashok, Dhananjay	(VardiFest) A Solver + Gradient Descent Training Algorithm for Deep Neural Network (, )
Atkey, Robert	(FoMLAS) Vehicle: A High-Level Language for Embedding Logical Specifications in Neural Networks (, talk)
B
Baader, Franz	(IJCAR) Evonne: Interactive Proof Visualization for Description Logics (System Description) (, talk) (DL) Efficient TBox Reasoning with Value Restrictions using the FL0wer Reasoner (Extended Abstract) (, talk) (DL) Optimal ABox Repair w.r.t. Static EL TBoxes: from Quantified ABoxes back to ABoxes (Extended Abstract) (, talk)
Baccelli, Emmanuel	(CAV) End-to-end Mechanised Proof of an eBPF Virtual Machine for Microcontrollers (, talk)
Badings, Thom	(CAV) Sampling-Based Verification of CTMCs with Uncertain Rates (, talk)
Bae, Kyungmin	(CAV) STLmc: Robust STL Model Checking of Hybrid Systems using SMT (, talk)
Bak, Stanley	(CAV) Reachability of Koopman Linearized Systems Using Random Fourier Feature Observables and Polynomial Zonotope Refinement (, talk)
Balbiani, Philippe	(DL) Advanced languages of terms for ontologies (, talk)
Balcan, Maria-Florina	(CP) Improved Sample Complexity Bounds for Branch-and-Cut (, talk)
Balintová, Iveta	(DL) Hybrid MHS-MXP ABox Abduction Solver: First Emprical Results (, talk)
Ballesteros, Ignacio	(FMBC) Automatic generation of attacker contracts in Solidity (, talk)
Balogh, Andrea	(CP) Symmetry breaking and Knowledge Compilation (, talk)
Balyo, Tomas	(POS) Dinosat: A SAT Solver with Native DNF Support (, talk)
Bang, Seongwon	(CAV) SMT-based Translation Validation for Machine Learning Compiler (, talk)
Banno, Ryotaro	(CAV) Oblivious Online Monitoring for Safety LTL Specification via Fully Homomorphic Encryption (, talk)
Bansal, Suguman	(VardiFest) Automata-Based Quantitative Reasoning (, talk) (CAV) Specification-Guided Learning of Nash Equilibria with High Social Welfare (, talk)
Bao, Jialu	(CAV) Data-Driven Invariant Learning for Probabilistic Programs (, talk)
Barbosa, Haniel	(IJCAR) Flexible Proof Production in an Industrial-Strength SMT Solver (, talk) (CAV) Even Faster Conflicts and Lazier Reductions for String Solvers (, talk)
Barrett, Clark	(IJCAR) Flexible Proof Production in an Industrial-Strength SMT Solver (, talk) (IJCAR) Cooperating Techniques for Solving Nonlinear Arithmetic in the cvc5 SMT Solver (System Description) (, talk) (IJCAR) Reasoning About Vectors using an SMT Theory of Sequences (, talk) (FoMLAS) Scalable Verification of GNN-based Job Schedulers (, talk) (FoMLAS) An Abstraction-Refinement Approach to Verifying Convolutional Neural Networks (, talk) (FoMLAS) Neural Network Verification with Proof Production (, talk) (CAV) Murxla: A Modular and Highly Extensible API Fuzzer for SMT Solvers (, talk) (CAV) Even Faster Conflicts and Lazier Reductions for String Solvers (, talk)
Bartel, Thomas	(POS) Dinosat: A SAT Solver with Native DNF Support (, talk)
Bastani, Osbert	(CAV) Specification-Guided Learning of Nash Equilibria with High Social Welfare (, talk)
Becchi, Anna	(CAV) Abstraction Modulo Stability for Reverse Engineering (, talk)
Bednarczyk, Bartosz	(DL) Comonadic Semantics for Description Logics Games (, talk)
Beldiceanu, Nicolas	(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)
Bellés-Muñoz, Marta	(CAV) Distilling Constraints in Zero-Knowledge Protocols (, talk)
Benac, Clara	(FMBC) Automatic generation of attacker contracts in Solidity (, talk)
Bensalem, Saddek	(FoMLAS) Formal Specification for Learning-Enabled Autonomous Systems (, talk)
Berg, Jeremias	(IJCAR) Clause Redundancy and Preprocessing in Maximum Satisfiability (, talk)
Bernreiter, Michael	(IJCAR) Sequent Calculi for Choice Logics (, talk)
Bessa, Iury	(FoMLAS) CEG4N: Counter-Example Guided Neural Network Quantization Refinement (, talk)
Besson, Frédéric	(CAV) End-to-end Mechanised Proof of an eBPF Virtual Machine for Microcontrollers (, talk)
Beutner, Raven	(CAV) Software Verification of Hyperproperties Beyond k-Safety (, talk)
Beyersdorff, Olaf	(PC) QCDCL with Cube Learning or Pure Literal Elimination – What is best? (, talk)
Bhatia, Amit	(VardiFest) Logic-driven approaches for smart, safe and energy-efficient aviation (, talk)
Bian, Song	(CAV) Oblivious Online Monitoring for Safety LTL Specification via Fully Homomorphic Encryption (, talk)
Bidoit, Nicole	(IJCAR) Hypergraph-Based Inference Rules for Computing EL+-Ontology Justifications (, talk)
Bienvenu, Meghyn	(DL) Complexity Landscape for Counting Queries (Extended abstract) (, talk) (DL) Querying Inconsistent Prioritized Data with ORBITS: Algorithms, Implementation, and Experiments (Extended Abstract) (, talk)
Biere, Armin	(POS) Scalable Proof Producing Multi-Threaded SAT Solving with Gimsatul through Sharing instead of Copying Clauses (, talk)
Bilkova, Marta	(IJCAR) Paraconsistent Gödel Modal Logic (, talk)
Blaisdell, Eben	(IJCAR) Non-associative, Non-commutative Multi-Modal Linear Logic (, talk)
Blicha, Martin	(CAV) SolCMC: Solidity Compiler’s Model Checker (, talk)
Blondin, Michael	(CAV) Verifying generalised and structural soundness of workflow nets via relaxations (, talk)
Boborová, Janka	(DL) Hybrid MHS-MXP ABox Abduction Solver: First Emprical Results (, talk)
Bogomolov, Sergiy	(CAV) Reachability of Koopman Linearized Systems Using Random Fourier Feature Observables and Polynomial Zonotope Refinement (, talk)
Bonacina, Ilario	(PC) On vanishing sums of roots of unity in polynomial calculus and sum-of-squares (an extended abstract) (, talk)
Bordais, Benjamin	(VardiFest) Strategy synthesis for Global Window PCTL (, talk)
Borgida, Alex	(DL) Accessing Document Data Sources using Referring Expression Types (, talk)
Borgwardt, Stefan	(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) (DL) Finding Good Proofs for Answers to Conjunctive Queries Mediated by Lightweight Ontologies (, talk) (DL) Expressivity of Planning with Horn Description Logic Ontologies (Extended Abstract) (, talk)
Bouajjani, Ahmed	(CAV) Data-driven Numerical Invariant Synthesis with Automatic Generation of Attributes (, talk)
Bourgaux, Camille	(DL) Querying Inconsistent Prioritized Data with ORBITS: Algorithms, Implementation, and Experiments (Extended Abstract) (, talk)
Boutglay, Wael-Amine	(CAV) Data-driven Numerical Invariant Synthesis with Automatic Generation of Attributes (, talk)
Bouziane, Hinde	(IJCAR) Goéland: A Concurrent Tableau-Based Theorem Prover (System Description) (, talk)
Bozga, Marius	(IJCAR) Decision Problems in a Logic for Reasoning about Reconfigurable Distributed Systems (, talk)
Bozzato, Loris	(DL) Reasoning on Multi-Relational Contextual Hierarchies via Answer Set Programming with Algebraic Measures (, talk)
Brieulle, Ludovic	(DL) Category-based Semantics for the Description Logic ALC and Reasoning (, talk)
Bromberger, Martin	(IJCAR) An Efficient Subsumption Test Pipeline for BS(LRA) Clauses (, talk)
Brown, Chad	(IJCAR) Lash 1.0 (System Description) (, talk) (FMBC) Proofgold: Blockchain for Formal Methods (, talk)
Brugger, Lea Salome	(FMBC) Automating Security Analysis of Off-Chain Protocols (, talk)
Bryant, Randal	(IJCAR) Preprocessing of Propagation Redundant Clauses (, talk) (POS) Combining CDCL, Gauss-Jordan Elimination, and Proof Generation (, talk)
Bueri, Lucas	(IJCAR) Decision Problems in a Logic for Reasoning about Reconfigurable Distributed Systems (, talk)
Bueso, Luis Eduardo	(FMBC) Automatic generation of attacker contracts in Solidity (, talk)
Burlats, Auguste	(CP) Exploiting Model Entropy to Make Branching Decisions in Constraint Programming (, talk)
Busatto-Gaston, Damien	(VardiFest) Strategy synthesis for Global Window PCTL (, talk)
Böhm, Benjamin	(PC) QCDCL with Cube Learning or Pure Literal Elimination – What is best? (, talk)
C
Cai, Shaowei	(CAV) Local Search For SMT on Linear Integer Arithmetic (, talk)
Cailler, Julie	(IJCAR) Goéland: A Concurrent Tableau-Based Theorem Prover (System Description) (, talk)
Calvanese, Diego	(VardiFest) Rewriting, Answering, and Losslessness: A Clarification by the “Four Italians” (, talk) (DL) Extraction of Object-Centric Event Logs through Virtual Knowledge Graphs (, talk) (DL) Ontology-based Data Federation (Extended Abstract) (, talk)
Cappart, Quentin	(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)
Casadio, Marco	(FoMLAS) Why Robust Natural Language Understanding is a Challenge (, talk) (CAV) Neural Network Robustness as a Verification Property: A Principled Case Study (, talk)
Castañeda Lozano, Roberto	(CP) Optimized Code Generation against Power Side Channels (, talk)
Castro, Pablo	(CAV) Playing Against Fair Adversaries in Stochastic Games with Total Rewards (, talk)
Cauli, Claudia	(IJCAR) Actions over Core-Closed Knowledge Bases (, talk)
Ceresa, Martin	(FMBC) Multi: a Formal Playground for Smart Multi-contract interaction (, talk)
Chakraborty, Supratik	(IJCAR) On Eventual Non-negativity and Positivity for the Weighted Sum of Powers of Matrices (, talk) (VardiFest) To Count or Not to Count: A Personal Perspective (, talk)
Chakravarty, Manuel	(FMBC) Designing EUTxO smart contracts as communicating state machines: the case of simulating accounts (, talk)
Chandar, Sarath	(CP) Combining Reinforcement Learning and Constraint Programming for Sequence-Generation Tasks with Hard Constraints - Extended Abstract (, talk)
Chapman, James	(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) (FMBC) Determinism of ledger updates (, talk)
Chatterjee, Krishnendu	(CAV) Sound and Complete Certificates for Quantitative Termination Analysis of Probabilistic Programs (, talk)
Chatterjee, Prantik	(CAV) Proof-guided Underapproximation Widening for Bounded Model Checking (, talk)
Cheang, Kevin	(CAV) UCLID5: Multi-Modal Formal Modeling, Verification, and Synthesis (, talk)
Chen, Haibo	(CAV) Affine Loop Invariant Generation via Matrix Algebra (, talk)
Chen, Mingshuai	(CAV) Does a Program Yield the Right Distribution? Verifying Probabilistic Programs via Generating Functions (, talk)
Chen, Taolue	(CAV) PoS4MPC: Automated Security Policy Synthesis for Secure Multi-Party Computation (, talk)
Cheng, Chih-Hong	(FoMLAS) Formal Specification for Learning-Enabled Autonomous Systems (, talk)
Cheukam Ngouonou, Jovial	(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)
Chlebowski, Szymon	(IJCAR) Synthetic Tableaux: Minimal Tableau Search Heuristics (, talk)
Chlipala, Adam	(CAV) Hemiola: A DSL and Verification Tools to Guide Design and Proof of Hierarchical Cache-Coherence Protocols (, talk)
Choi, Joonwon	(CAV) Hemiola: A DSL and Verification Tools to Guide Design and Proof of Hierarchical Cache-Coherence Protocols (, talk)
Chun, Inwhan	(CAV) SMT-based Translation Validation for Machine Learning Compiler (, talk)
Cimatti, Alessandro	(VardiFest) The Safety Fragment of LTL (, talk) (CAV) Abstraction Modulo Stability for Reverse Engineering (, talk)
Climent, Laura	(CP) Large Neighborhood Search for Robust Solutions for Constraint Satisfaction Problems with Ordered Domains (, talk)
Coenen, Norine	(CAV) Explaining Hyperproperty Violations (, talk)
Cohen, Irun	(VardiFest) Natural Autoencoding (, talk)
Cohen, Joshua M.	(CAV) Verified Erasure Correction in Coq with MathComp and VST (, talk)
Colange, Maximilien	(CAV) From Spot 2.0 to Spot 2.10: What's New? (, talk)
Confalonieri, Roberto	(DL) Evaluating the Interpretability of Threshold Operators (, talk)
Coppé, Vianney	(CP) Solving the Constrained Single-Row Facility Layout Problem with Decision Diagrams (Extended Abstract) (, talk)
Cordeiro, Lucas C.	(FoMLAS) CEG4N: Counter-Example Guided Neural Network Quantization Refinement (, talk)
Costantini, Stefania	(VardiFest) An Epistemic Logic for modelling Cooperative Agents (, talk)
Coulombe, Christopher	(CP) Extended Abstract: Constraint Acquisition Based on Solution Counting (, talk)
Côté, Alain	(CP) Extended Abstract for : Scheduling the Equipment Maintenance of an Electric Power Transmission Network using Constraint Programming (, talk)
D
D'Argenio, Pedro R.	(CAV) Playing Against Fair Adversaries in Stochastic Games with Total Rewards (, talk)
Dachselt, Raimund	(IJCAR) Evonne: Interactive Proof Visualization for Description Logics (System Description) (, talk) (CAV) Explaining Hyperproperty Violations (, talk)
Daggitt, Matthew	(FoMLAS) Why Robust Natural Language Understanding is a Challenge (, talk) (FoMLAS) Differentiable Logics for Neural Network Training and Verification (, talk) (CAV) Neural Network Robustness as a Verification Property: A Principled Case Study (, talk)
Daggitt, Matthew	(FoMLAS) Vehicle: A High-Level Language for Embedding Logical Specifications in Neural Networks (, talk)
Dalla, Marco	(CP) Automated SAT Problem Feature Extraction using 1 Convolutional Autoencoders (, talk)
Dardinier, Thibault	(CAV) Sound Automation of Magic Wands (, talk)
Das, Anupam	(IJCAR) Cyclic Proofs, Hypersequents, and Transitive Closure Logic (, talk)
De Giacomo, Giuseppe	(VardiFest) LTLf? It's Easy! Precisely! (, )
De Oliveira Oliveira, Mateus	(CAV) Synthesis and Analysis of Petri Nets from Causal Specifications (, talk)
Delahaye, David	(IJCAR) Goéland: A Concurrent Tableau-Based Theorem Prover (System Description) (, talk)
Delecluse, Augustin	(CP) Extended Abstract: Sequence Variables for Routing Problems (, talk)
Demasi, Ramiro	(CAV) Playing Against Fair Adversaries in Stochastic Games with Total Rewards (, talk)
Desmartin, Remi	(FoMLAS) Neural Networks in Imandra: Matrix Representation as a Verification Choice (, talk)
Dev Gupta, Sharmi	(CP) Finding Counterfactual Explanations through Constraint Relaxations (, talk)
Di Stasio, Antonio	(VardiFest) LTLf Synthesis Under Environment Specifications (, talk)
Di Stefano, Federica	(DL) Pointwise Circumscription in Description Logics (, talk)
Dill, David	(IJCAR) Reasoning About Vectors using an SMT Theory of Sequences (, talk)
Dimitrov, Dimitar I.	(CAV) Shared Certificates for Neural Network Verification (, talk)
Dixon, Clare	(IJCAR) Local Reductions for the Modal Cube (, talk)
Diéguez, Martin	(DL) Advanced languages of terms for ontologies (, talk)
Douence, Rémi	(CP) Extended Abstract: Acquiring Maps of Interrelated Conjectures on Sharp Bounds (, talk)
Doveri, Kyveli	(CAV) FORQ-based Language Inclusion Formal Testing (, talk)
Dowek, Gilles	(IJCAR) From the Universality of Mathematical Truth to the Interoperability of Proof Systems (, talk)
Dragoi, Cezara	(FMBC) A Domain Specific Language for Testing Consensus Implementations (, talk)
Draheim, Dirk	(IJCAR) GK: Implementing Full First Order Default Logic for Commonsense Reasoning (System Description) (, talk)
Duarte, André	(IJCAR) Ground Joinability and Connectedness in the Superposition Calculus (, talk)
Dubois, Jérôme	(CAV) From Spot 2.0 to Spot 2.10: What's New? (, talk)
Duret-Lutz, Alexandre	(CAV) From Spot 2.0 to Spot 2.10: What's New? (, talk)
Durán, Francisco	(IJCAR) Equational Unification and Matching, and Symbolic Reachability Analysis in Maude 3.2 (System Description) (, talk)
E
Eiter, Thomas	(DL) Reasoning on Multi-Relational Contextual Hierarchies via Answer Set Programming with Algebraic Measures (, talk)
Ek, Alexander	(CP) Explaining Propagation for Gini and Spread with Variable Mean (Extended Abstract) (, talk)
Eker, Steven	(IJCAR) Equational Unification and Matching, and Symbolic Reachability Analysis in Maude 3.2 (System Description) (, talk)
Enea, Constantin	(FMBC) A Domain Specific Language for Testing Consensus Implementations (, talk)
Escobar, Santiago	(IJCAR) Equational Unification and Matching, and Symbolic Reachability Analysis in Maude 3.2 (System Description) (, talk)
F
Faella, Marco	(CAV) Reasoning about Data Trees using CHCs (, talk)
Falakh, Faiq Miftakhul	(DL) AGM Revision in Description Logics Under Fixed-Domain Semantics (, talk)
Falque, Thibault	(CP) Aggressive Bound Descent for Constraint Optimization (, talk) (CP) On PB Encodings for Constraint Problems (, talk)
Fan, Yuxin	(CAV) PoS4MPC: Automated Security Policy Synthesis for Secure Multi-Party Computation (, talk)
Fang, Bin	(CAV) Affine Loop Invariant Generation via Matrix Algebra (, talk)
Fang, Wang	(CAV) Verifying Fairness in Quantum Machine Learning (, talk)
Felli, Paolo	(IJCAR) CTL* Model Checking for Data-Aware Dynamic Systems with Arithmetic (, talk)
Feng, Weizhi	(CAV) Divide-and-Conquer Determinization of Büchi Automata based on SCC Decomposition (, talk)
Ferariu, Tudor	(FMBC) Designing EUTxO smart contracts as communicating state machines: the case of simulating accounts (, talk)
Ferrara, Andrea	(VardiFest) Capturing abscondings (, talk)
Ferrari, Mauro	(IJCAR) SAT-based Proof Search in Intermediate Propositional Logics (, talk)
Finkbeiner, Bernd	(CAV) Software Verification of Hyperproperties Beyond k-Safety (, talk) (CAV) Explaining Hyperproperty Violations (, talk) (CAV) Information Flow Guided Synthesis (, talk)
Fiorentini, Camillo	(IJCAR) SAT-based Proof Search in Intermediate Propositional Logics (, talk)
Fischer, Marc	(CAV) Shared Certificates for Neural Network Verification (, talk)
Fleury, Mathias	(POS) Scalable Proof Producing Multi-Threaded SAT Solving with Gimsatul through Sharing instead of Copying Clauses (, talk)
Formisano, Andrea	(VardiFest) An Epistemic Logic for modelling Cooperative Agents (, talk)
Fortin, Marie	(DL) Reverse Engineering of Temporal Queries with and without LTL Ontologies: First Steps (, talk)
Fraer, Ranan	(VardiFest) Moshe Vardi and Intel Corporation: Long and Fruitful Collaboration (, talk)
Franconi, Enrico	(DL) Accessing Document Data Sources using Referring Expression Types (, talk)
Fredlund, Lars-Åke	(FMBC) Automatic generation of attacker contracts in Solidity (, talk)
Fredrikson, Matt	(FoMLAS) Self-Correcting Neural Networks For Safe Classification (, talk)
Fremont, Daniel	(CAV) Randomized Synthesis for Diversity and Cost Constraints with Control Improvisation (, talk)
Frenkel, Hadar	(CAV) Explaining Hyperproperty Violations (, talk)
Friese, Tom	(DL) On the Eve of True Explainability for OWL Ontologies: Description Logic Proofs with Evee and Evonne (, talk)
Frittella, Sabine	(IJCAR) Paraconsistent Gödel Modal Logic (, talk)
Frohn, Florian	(WST) A Calculus for Modular Non-Termination Proofs by Loop Acceleration (, talk) (WST) Deciding Termination of Uniform Loops with Polynomial Parameterized Complexity (, talk) (IJCAR) Proving Non-Termination and Lower Runtime Bounds with LoAT (System Description) (, talk)
Fromherz, Aymeric	(FoMLAS) Self-Correcting Neural Networks For Safe Classification (, talk)
Fu, Hongfei	(CAV) Affine Loop Invariant Generation via Matrix Algebra (, talk)
Fuhs, Carsten	(WST) A Calculus for Modular Non-Termination Proofs by Loop Acceleration (, talk)
Fujita, Tomohiro	(IJCAR) Formula Simplification via Invariance Detection by Algebraically Indexed Types (, talk)
Fukiage, Tsubasa	(POS) DPS: A Framework for Deterministic Parallel SAT Solvers (, talk)
Funk, Maurice	(DL) Actively Learning ELIQs in the Presence of DL-Lite-Horn Ontologies (, talk)
G
Gaddamadugu, Pranav	(CAV) UCLID5: Multi-Modal Formal Modeling, Verification, and Synthesis (, talk)
Gaevoy, Nikita	(PC) Simulations between proof systems (, talk)
Gaha, Mohamed	(CP) Extended Abstract for : Scheduling the Equipment Maintenance of an Electric Power Transmission Network using Constraint Programming (, talk)
Galesi, Nicola	(PC) On vanishing sums of roots of unity in polynomial calculus and sum-of-squares (an extended abstract) (, talk)
Gallicchio, James	(IJCAR) Implicit Definitions with Differential Equations for KeYmaera X (System Description) (, talk)
Ganesh, Vijay	(VardiFest) A Solver + Gradient Descent Training Algorithm for Deep Neural Network (, )
Ganty, Pierre	(CAV) FORQ-based Language Inclusion Formal Testing (, talk)
Gauthier, Thibault	(FMBC) Proofgold: Blockchain for Formal Methods (, talk)
Gaysin, Azza	(PC) Proof complexity of CSP (, talk)
Gbaguidi Aisse, Alexandre	(CAV) From Spot 2.0 to Spot 2.10: What's New? (, talk)
Geatti, Luca	(VardiFest) The Safety Fragment of LTL (, talk)
Geffner, Hector	(VardiFest) Logic and Languages for Representation Learning (, talk)
Genc, Begum	(CP) Finding Counterfactual Explanations through Constraint Relaxations (, talk)
Gencer, Cigdem	(DL) Advanced languages of terms for ontologies (, talk)
Geser, Alfons	(WST) Approximating Relative Match-Bounds (, talk)
Giannakopoulou, Dimitra	(CAV) Capture, Analyze, Diagnose: Realizability Checking of Requirements in FRET (, talk)
Giesl, Jürgen	(WST) Deciding Termination of Uniform Loops with Polynomial Parameterized Complexity (, talk) (WST) Improved Automatic Complexity Analysis of Integer Programs (, talk) (WST) Automatic Complexity Analysis of (Probabilistic) Integer Programs via KoAT (, 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)
Gigante, Nicola	(VardiFest) The Safety Fragment of LTL (, talk)
Gillard, Clément	(CAV) From Spot 2.0 to Spot 2.10: What's New? (, talk)
Gillard, Xavier	(CP) Solving the Constrained Single-Row Facility Layout Problem with Decision Diagrams (Extended Abstract) (, talk)
Gindullin, Ramiz	(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)
Giordano, Laura	(DL) Reasoning about actions with EL ontologies in a temporal action theory (Extended Abstract) (, talk)
Girlando, Marianna	(IJCAR) Cyclic Proofs, Hypersequents, and Transitive Closure Logic (, talk)
Gittis, Andreas	(CAV) Randomized Synthesis for Diversity and Cost Constraints with Control Improvisation (, talk)
Glimm, Birte	(DL) Concept Abduction for Description Logics (, talk) (DL) Computing Concept Referring Expressions with Standard OWL Reasoners (, talk) (DL) SAT-Based Axiom Pinpointing Revisited (, talk)
Godbole, Adwait	(CAV) UCLID5: Multi-Modal Formal Modeling, Verification, and Synthesis (, talk)
Goharshady, Amir Kafshdar	(CAV) Sound and Complete Certificates for Quantitative Termination Analysis of Probabilistic Programs (, talk)
Golia, Priyanka	(CP) Boolean Functional Synthesis and its Applications (, talk) (CAV) A Scalable Shannon Entropy Estimator (, talk)
Golumbic, Martin Charles	(VardiFest) On the Effectiveness of Logic in Algorithmic Graph Theory (, talk)
Gopinath, Divya	(FoMLAS) VPN: Verification of Poisoning in Neural Networks (, talk)
Gordillo, Pablo	(IJCAR) Using Automated Reasoning Techniques for Enhancing the Efficiency and Security of (Ethereum) Smart Contracts (, talk)
Gottlob, Georg	(VardiFest) Data Complexity and Expressive Power of Ontological Reasoning Formalisms (, talk)
Goubault, Eric	(CAV) RINO: Robust INner and Outer Approximated Reachability of Neural Networks Controlled Systems (, talk)
Greenman, Ben	(VardiFest) Little Tricky Logic: Misconceptions in the Understanding of LTL (, talk)
Grieskamp, Wolfgang	(IJCAR) Reasoning About Vectors using an SMT Theory of Sequences (, talk)
Gros, Timo P.	(CAV) MoGym: Using Formal Models for Training and Verifying Decision-making Agents (, talk)
Grosof, Isaac	(POS) Towards the shortest DRAT proof of the Pigeonhole Principle (, talk)
Gu, Zhenzhen	(DL) Ontology-based Data Federation (Extended Abstract) (, talk)
Gu, Zhenzhen	(DL) Extraction of Object-Centric Event Logs through Virtual Knowledge Graphs (, talk)
Guan, Ji	(CAV) Verifying Fairness in Quantum Machine Learning (, talk)
Guha, Shibashis	(VardiFest) Strategy synthesis for Global Window PCTL (, talk) (CAV) PAC Statistical Model Checking of Mean Payoff in Discrete- and Continuous-Time MDP (, talk)
Guo, Liye	(WST) A transitive HORPO for curried systems (, talk)
Gurfinkel, Arie	(CAV) Program Verification with Constrained Horn Clauses (Invited Paper) ()
Gómez Álvarez, Lucía	(DL) Modelling Multiple Perspectives by Standpoint-Enhanced DLs (, talk)
H
H. Pham, Long	(CAV) Verifying Neural Networks Against Backdoor Attacks (, talk)
Habermehl, Peter	(CAV) Data-driven Numerical Invariant Synthesis with Automatic Generation of Attributes (, talk)
Haeusler, Edward	(DL) A Labelled Natural Deduction System for an Intuitionistic Description Logic with Nominals (, talk)
Hahn, Christopher	(CAV) Explaining Hyperproperty Violations (, talk)
Haifani, Fajar	(IJCAR) Connection-Minimal Abduction in EL via Translation to FOL (, talk) (IJCAR) Semantic Relevance (, talk) (DL) Connection-minimal Abduction in EL via translation to FOL (Extended Abstract) (, talk)
Halpern, Joe	(VardiFest) That's All I know: On the Effectiveness of Logic in Game Theory (, talk)
Harel, David	(VardiFest) Computability and Complexity over Finite Unordered Structures; e.g., Graphs (1979-1982) (, talk)
Hark, Marcel	(WST) Deciding Termination of Uniform Loops with Polynomial Parameterized Complexity (, talk) (WST) Improved Automatic Complexity Analysis of Integer Programs (, talk) (WST) Automatic Complexity Analysis of (Probabilistic) Integer Programs via KoAT (, talk)
Hasuo, Ichiro	(FoMLAS) Goal-Aware RSS for Complex Scenarios via Program Logic (, talk) (VardiFest) Bisimulation Games Played in Fibered Categories (, talk) (CAV) The Lattice-Theoretic Essence of Property Directed Reachability Analysis (, talk)
Havlena, Vojtěch	(CAV) Complementing Büchi Automata with Ranker (, talk)
Hencey, Brandon	(CAV) Reachability of Koopman Linearized Systems Using Random Fourier Feature Observables and Polynomial Zonotope Refinement (, talk)
Henzinger, Thomas	(VardiFest) Between Determinism and Nondeterminism (, talk)
Hermanns, Holger	(CAV) MoGym: Using Formal Models for Training and Verifying Decision-making Agents (, talk)
Hernández-Cerezo, Alejandro	(IJCAR) Using Automated Reasoning Techniques for Enhancing the Efficiency and Security of (Ethereum) Smart Contracts (, talk)
Herranz, Ángel	(FMBC) Automatic generation of attacker contracts in Solidity (, talk)
Heskes, Tom	(IJCAR) Guiding an Automated Theorem Prover with Neural Rewriting (, talk)
Heuer, Tobias	(POS) SATViz: Real-Time Visualization of Clausal Proofs (, talk)
Heule, Marijn	(IJCAR) Preprocessing of Propagation Redundant Clauses (, talk) (PC) Exponential separations using guarded extension variables (, talk) (VardiFest) Understandable Proofs of Unsatisfiability (, talk) (POS) Towards the shortest DRAT proof of the Pigeonhole Principle (, talk)
Hirokawa, Nao	(WST) Hydra Battles and AC Termination (, talk)
Hlávková, Zuzana	(DL) An API for DL Abduction Solvers (, talk)
Hofbauer, Dieter	(WST) Approximating Relative Match-Bounds (, talk)
Hoffmann, Joerg	(CAV) MoGym: Using Formal Models for Training and Verifying Decision-making Agents (, talk) (DL) Expressivity of Planning with Horn Description Logic Ontologies (Extended Abstract) (, talk)
Holden, Sean	(IJCAR) Bayesian Ranking for Strategy Scheduling in Automated Theorem Provers (, talk)
Holub, Štěpán	(IJCAR) Binary Codes that do Not Preserve Primitivity (, talk)
Holzenkamp, Tim	(POS) SATViz: Real-Time Visualization of Clausal Proofs (, talk)
Homola, Martin	(DL) An API for DL Abduction Solvers (, talk) (DL) Hybrid MHS-MXP ABox Abduction Solver: First Emprical Results (, talk)
Horak, Tom	(CAV) Explaining Hyperproperty Violations (, talk)
Hsu, Justin	(CAV) Data-Driven Invariant Learning for Probabilistic Programs (, talk)
Huang, Xiaowei	(FoMLAS) Formal Specification for Learning-Enabled Autonomous Systems (, talk)
Hustadt, Ullrich	(IJCAR) Local Reductions for the Modal Cube (, talk)
Hym, Samuel	(CAV) End-to-end Mechanised Proof of an eBPF Virtual Machine for Microcontrollers (, talk)
Hyvärinen, Antti	(CAV) SolCMC: Solidity Compiler’s Model Checker (, talk)
I
Ihalainen, Hannes	(IJCAR) Clause Redundancy and Preprocessing in Maximum Satisfiability (, talk)
Illich, Moritz	(DL) Computing Concept Referring Expressions with Standard OWL Reasoners (, talk)
Indrzejczak, Andrzej	(IJCAR) Le\'sniewski's Ontology -- Proof-Theoretic Characterization (, talk)
Inoue, Katsumi	(POS) DPS: A Framework for Deterministic Parallel SAT Solvers (, talk)
Iosif, Radu	(IJCAR) Decision Problems in a Logic for Reasoning about Reconfigurable Distributed Systems (, talk)
Isabel, Miguel	(CAV) Distilling Constraints in Zero-Knowledge Protocols (, talk)
Isac, Omri	(FoMLAS) Neural Network Verification with Proof Production (, talk)
Iser, Markus	(POS) Dinosat: A SAT Solver with Native DNF Support (, talk) (POS) SATViz: Real-Time Visualization of Clausal Proofs (, talk)
Itsykson, Dmitry	(PC) Proof complexity of natural formulas via communication arguments (, talk)
J
Jakobsson, Arvid	(FMBC) FAT CAT: Formal Acceptance Testing of Contracts for Administering Tokens (, talk)
Janota, Mikolas	(IJCAR) Guiding an Automated Theorem Prover with Neural Rewriting (, talk)
Jansen, Nils	(CAV) Sampling-Based Verification of CTMCs with Uncertain Rates (, talk)
Jhoo, Ho Young	(CAV) SMT-based Translation Validation for Machine Learning Compiler (, talk)
Ji, Yucheng	(CAV) Affine Loop Invariant Generation via Matrix Algebra (, talk)
Jin, Peng	(CAV) Trainify: A CEGAR-Driven Training and Verification Framework for Safe Deep Reinforcement Learning (, talk)
Jones, Michael Peyton	(FMBC) Designing EUTxO smart contracts as communicating state machines: the case of simulating accounts (, talk)
Jothimurugan, Kishor	(CAV) Specification-Guided Learning of Nash Equilibria with High Social Welfare (, talk)
Juba, Brendan	(CAV) A Scalable Shannon Entropy Estimator (, talk)
Jukiewicz, Marcin	(IJCAR) Synthetic Tableaux: Minimal Tableau Search Heuristics (, talk)
Jung, Jean Christoph	(DL) More on Interpolants and Explicit Definitions for Description Logics with Nominals and/or Role Inclusions (, talk) (DL) Actively Learning ELIQs in the Presence of DL-Lite-Horn Ontologies (, talk)
Junges, Sebastian	(CAV) Abstraction-Refinement for Hierarchical Probabilistic Models (, talk) (CAV) Sampling-Based Verification of CTMCs with Uncertain Rates (, talk)
Junosza-Szaniawski, Konstanty	(POS) Towards an Efficient CNF Encoding of Block Ciphers (, talk)
Järv, Priit	(IJCAR) GK: Implementing Full First Order Default Logic for Commonsense Reasoning (System Description) (, talk)
Järvisalo, Matti	(IJCAR) Clause Redundancy and Preprocessing in Maximum Satisfiability (, talk)
K
Kalayci, Tahir Emre	(DL) Extraction of Object-Centric Event Logs through Virtual Knowledge Graphs (, talk)
Kaliszyk, Cezary	(IJCAR) Lash 1.0 (System Description) (, talk) (FMBC) Proofgold: Blockchain for Formal Methods (, talk)
Kamhi, Gila	(VardiFest) Moshe Vardi and Intel Corporation: Long and Fruitful Collaboration (, talk)
Kanovich, Max	(IJCAR) Non-associative, Non-commutative Multi-Modal Linear Logic (, talk)
Karge, Jonas	(DL) Uniform and Modular Sequent Systems for Description Logics (, talk)
Katis, Andreas	(CAV) Capture, Analyze, Diagnose: Realizability Checking of Requirements in FRET (, talk)
Katoen, Joost-Pieter	(CAV) Does a Program Yield the Right Distribution? Verifying Probabilistic Programs via Generating Functions (, talk)
Katsaros, Panagiotis	(FoMLAS) Formal Specification for Learning-Enabled Autonomous Systems (, talk)
Katsumata, Shin-ya	(CAV) The Lattice-Theoretic Essence of Property Directed Reachability Analysis (, talk)
Katz, Guy	(FoMLAS) RoMA: a Method for Neural Network Robustness Measurement and Assessment (, talk) (FoMLAS) Verification-Aided Deep Ensemble Selection (, talk) (FoMLAS) An Abstraction-Refinement Approach to Verifying Convolutional Neural Networks (, talk) (FoMLAS) Minimal Multi-Layer Modifications of Deep Neural Networks (, talk) (FoMLAS) Neural Network Verification with Proof Production (, talk) (CAV) Neural Network Robustness as a Verification Property: A Principled Case Study (, talk)
Kazakov, Yevgeny	(DL) Concept Abduction for Description Logics (, talk) (DL) SAT-Based Axiom Pinpointing Revisited (, talk)
Khoja, Alan	(VardiFest) Checking Legal Contracts - On a Not So Usual Application of Mechanized Logic (, talk)
Kienitz, Daniel	(FoMLAS) Why Robust Natural Language Understanding is a Challenge (, talk)
Kiesel, Rafael	(DL) Reasoning on Multi-Relational Contextual Hierarchies via Answer Set Programming with Algebraic Measures (, talk)
Klauck, Michaela	(CAV) MoGym: Using Formal Models for Training and Verifying Decision-making Agents (, talk)
Klinkenberg, Lutz	(CAV) Does a Program Yield the Right Distribution? Verifying Probabilistic Programs via Generating Functions (, talk)
Knispel, Andre	(FMBC) Human and machine-readable models of state machines for the Cardano ledger (, talk)
Knispel, Andre	(FMBC) Determinism of ledger updates (, talk)
Kochdumper, Niklas	(CAV) Reachability of Koopman Linearized Systems Using Random Fourier Feature Observables and Polynomial Zonotope Refinement (, talk)
Kohl, Christina	(WST) CeTA – A certifier for termCOMP 2022 (, talk)
Kokke, Wen	(FoMLAS) Vehicle: A High-Level Language for Embedding Logical Specifications in Neural Networks (, talk) (FoMLAS) Why Robust Natural Language Understanding is a Challenge (, talk) (CAV) Neural Network Robustness as a Verification Property: A Principled Case Study (, talk)
Komendantskaya, Ekaterina	(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) Neural Networks in Imandra: Matrix Representation as a Verification Choice (, talk) (CAV) Neural Network Robustness as a Verification Property: A Principled Case Study (, talk)
Konev, Boris	(DL) Reverse Engineering of Temporal Queries with and without LTL Ontologies: First Steps (, talk)
Koopmann, Patrick	(IJCAR) Connection-Minimal Abduction in EL via Translation to FOL (, talk) (IJCAR) Evonne: Interactive Proof Visualization for Description Logics (System Description) (, talk) (DL) An API for DL Abduction Solvers (, talk) (DL) On the Eve of True Explainability for OWL Ontologies: Description Logic Proofs with Evee and Evonne (, talk) (DL) Finding Good Proofs for Answers to Conjunctive Queries Mediated by Lightweight Ontologies (, talk) (DL) Efficient TBox Reasoning with Value Restrictions using the FL0wer Reasoner (Extended Abstract) (, 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)
Kop, Cynthia	(WST) Tuple Interpretations and Applications to Higher-Order Runtime Complexity (, talk) (WST) A transitive HORPO for curried systems (, talk)
Kori, Mayuko	(CAV) The Lattice-Theoretic Essence of Property Directed Reachability Analysis (, talk)
Korovin, Konstantin	(IJCAR) Ground Joinability and Connectedness in the Superposition Calculus (, talk)
Kovtunova, Alisa	(DL) Finding Good Proofs for Answers to Conjunctive Queries Mediated by Lightweight Ontologies (, talk) (DL) Expressivity of Planning with Horn Description Logic Ontologies (Extended Abstract) (, talk)
Kovács, Laura	(FMBC) Automating Security Analysis of Off-Chain Protocols (, talk)
Kozhemiachenko, Daniil	(IJCAR) Paraconsistent Gödel Modal Logic (, talk)
Kremer, Gereon	(IJCAR) Flexible Proof Production in an Industrial-Strength SMT Solver (, talk) (IJCAR) Cooperating Techniques for Solving Nonlinear Arithmetic in the cvc5 SMT Solver (System Description) (, talk)
Kriegel, Francesco	(DL) Optimal ABox Repair w.r.t. Static EL TBoxes: from Quantified ABoxes back to ABoxes (Extended Abstract) (, talk)
Krijnen, Jacco	(FMBC) Designing EUTxO smart contracts as communicating state machines: the case of simulating accounts (, talk)
Krishnamurthi, Shriram	(VardiFest) Little Tricky Logic: Misconceptions in the Understanding of LTL (, talk)
Krötzsch, Markus	(DL) Expressivity of Planning with Horn Description Logic Ontologies (Extended Abstract) (, talk)
Kuryshev, Kevin	(POS) SATViz: Real-Time Visualization of Clausal Proofs (, talk)
Kutsia, Temur	(IJCAR) A Framework for Approximate Generalization in Quantitative Theories (, talk)
Kuznetsov, Stepan	(IJCAR) Non-associative, Non-commutative Multi-Modal Linear Logic (, talk)
Köhl, Maximilian Alexander	(CAV) MoGym: Using Formal Models for Training and Verifying Decision-making Agents (, talk)
Kölbl, Martin	(VardiFest) Checking Legal Contracts - On a Not So Usual Application of Mechanized Logic (, talk)
Křetínský, Jan	(CAV) PAC Statistical Model Checking of Mean Payoff in Discrete- and Continuous-Time MDP (, talk)
L
Lachnitt, Hanna	(IJCAR) Flexible Proof Production in an Industrial-Strength SMT Solver (, talk)
Laeufer, Kevin	(CAV) UCLID5: Multi-Modal Formal Modeling, Verification, and Synthesis (, talk)
Lafleur, Daphné	(CP) Combining Reinforcement Learning and Constraint Programming for Sequence-Generation Tasks with Hard Constraints - Extended Abstract (, talk)
Lahav, Ori	(IJCAR) Effective Semantics for the Modal Logics K and KT via Non-deterministic Matrices (, talk)
Lal, Akash	(CAV) Proof-guided Underapproximation Widening for Bounded Model Checking (, talk)
Lamb, Luis	(VardiFest) From Logic to Neurosymbolic AI (, talk)
Lan, Jianglin	(FoMLAS) Tight Neural Network Verification via Semidefinite Relaxations and Linear Reformulations (, talk)
Landver, Avner	(VardiFest) Moshe Vardi and Intel Corporation: Long and Fruitful Collaboration (, talk)
Lanti, Davide	(DL) Ontology-based Data Federation (Extended Abstract) (, talk)
Larry, Paulson	(IJCAR) Bayesian Ranking for Strategy Scheduling in Automated Theorem Provers (, talk)
Lauko, Henrich	(CAV) From Spot 2.0 to Spot 2.10: What's New? (, talk)
Lauria, Massimo	(PC) On vanishing sums of roots of unity in polynomial calculus and sum-of-squares (an extended abstract) (, talk)
Le Duc, Chan	(DL) Category-based Semantics for the Description Logic ALC and Reasoning (, talk)
Lecoutre, Christophe	(CP) Aggressive Bound Descent for Constraint Optimization (, talk)
Lee, Jia	(CAV) STLmc: Robust STL Model Checking of Hybrid Systems using SMT (, talk)
Lee, Jimmy H. M.	(CP) Exploiting Functional Constraints in Automatic Dominance Breaking for Constraint Optimization (Extended Abstract) (, talk)
Lee, Juneyoung	(CAV) SMT-based Translation Validation for Machine Learning Compiler (, talk)
Leidinger, Hendrik	(IJCAR) SCL(EQ): SCL for First-Order Logic with Equality (, talk)
Leino, Klas	(FoMLAS) Self-Correcting Neural Networks For Safe Classification (, talk)
Lengal, Ondrej	(CAV) Complementing Büchi Automata with Ranker (, talk)
Lenzerini, Maurizio	(VardiFest) Rewriting of Regular Path Queries: The first paper of the four Italians (, talk)
Leszczyńska-Jasion, Dorota	(IJCAR) Synthetic Tableaux: Minimal Tableau Search Heuristics (, talk)
Leue, Stefan	(VardiFest) Checking Legal Contracts - On a Not So Usual Application of Mechanized Logic (, talk)
Leutgeb, Lorenz	(IJCAR) An Efficient Subsumption Test Pipeline for BS(LRA) Clauses (, talk) (CAV) Automated Expected Amortised Cost Analysis of Probabilistic Data Structures (, talk)
Levy, Natan	(FoMLAS) RoMA: a Method for Neural Network Robustness Measurement and Assessment (, talk)
Lew, Ethan	(CAV) Reachability of Koopman Linearized Systems Using Random Fourier Feature Observables and Polynomial Zonotope Refinement (, talk)
Li, Bohan	(CAV) Local Search For SMT on Linear Integer Arithmetic (, talk)
Li, Jianwen	(VardiFest) SAT-based Reasoning Techniques for LTL over Finite and Infinite Traces (, talk)
Li, Yannan	(CAV) Synthesizing Fair Decision Trees via Iterative Constraint Solving (, talk)
Li, Yong	(VardiFest) Divide-and-Conquer Determinization for B\"uchi Automata (, talk) (CAV) Divide-and-Conquer Determinization of Büchi Automata based on SCC Decomposition (, talk)
Libkin, Leonid	(VardiFest) Approximations of Certain Answers in First-Order Logic (, talk)
Lin, Anthony Widjaja	(VardiFest) Data Path Queries over Embedded Graph Databases (, talk)
Lin, Shaokai	(CAV) UCLID5: Multi-Modal Formal Modeling, Verification, and Synthesis (, talk)
Liu, Wanwei	(CAV) PoS4MPC: Automated Security Policy Synthesis for Secure Multi-Party Computation (, talk)
Lolic, Anela	(IJCAR) Sequent Calculi for Choice Logics (, talk)
Lommen, Nils	(WST) Improved Automatic Complexity Analysis of Integer Programs (, talk) (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)
Lomuscio, Alessio	(FoMLAS) Tight Neural Network Verification via Semidefinite Relaxations and Linear Reformulations (, talk)
Lu, Xiao-Nan	(POS) DPS: A Framework for Deterministic Parallel SAT Solvers (, talk)
Lutz, Carsten	(DL) Actively Learning ELIQs in the Presence of DL-Lite-Horn Ontologies (, talk)
Lyon, Tim	(DL) Uniform and Modular Sequent Systems for Description Logics (, talk)
López, Jheisson	(CP) Large Neighborhood Search for Robust Solutions for Constraint Satisfaction Problems with Ordered Domains (, talk)
M
Ma, Yue	(IJCAR) Hypergraph-Based Inference Rules for Computing EL+-Ontology Justifications (, talk)
Malik, Sharad	(VardiFest) Bridging Practice and Theory in SAT: Moshe Vardi the Catalyst (, talk)
Maly, Jan	(IJCAR) Sequent Calculi for Choice Logics (, talk)
Manerkar, Yatin A.	(CAV) UCLID5: Multi-Modal Formal Modeling, Verification, and Synthesis (, talk)
Mangal, Ravi	(FoMLAS) A Cascade of Checkers for Run-time Certification of Local Robustness (, talk) (FoMLAS) Self-Correcting Neural Networks For Safe Classification (, talk)
Mangla, Chaitanya	(IJCAR) Bayesian Ranking for Strategy Scheduling in Automated Theorem Provers (, talk)
Manino, Edoardo	(FoMLAS) CEG4N: Counter-Example Guided Neural Network Quantization Refinement (, talk)
Manière, Quentin	(DL) Complexity Landscape for Counting Queries (Extended abstract) (, talk)
Marcos, Joao	(IJCAR) Finite Two-Dimensional Proof Systems for Non-finitely Axiomatizable Logics (, talk)
Mariño, Julio	(FMBC) Automatic generation of attacker contracts in Solidity (, talk)
Marron, Assaf	(VardiFest) Natural Autoencoding (, talk)
Martelli, Alberto	(DL) Reasoning about actions with EL ontologies in a temporal action theory (Extended Abstract) (, talk)
Marti-Oliet, Narciso	(IJCAR) Equational Unification and Matching, and Symbolic Reachability Analysis in Maude 3.2 (System Description) (, talk)
Martin, Antoine	(CAV) From Spot 2.0 to Spot 2.10: What's New? (, talk)
Martinelli Tabajara, Lucas	(VardiFest) Boolean Synthesis via Decision Diagrams (, talk)
Matsumoto, Naoki	(CAV) Oblivious Online Monitoring for Safety LTL Specification via Fully Homomorphic Encryption (, talk)
Matsuoka, Kotaro	(CAV) Oblivious Online Monitoring for Safety LTL Specification via Fully Homomorphic Encryption (, talk)
Matsuzaki, Takuya	(IJCAR) Formula Simplification via Invariance Detection by Algebraically Indexed Types (, talk)
Maubert, Bastien	(VardiFest) Automated Synthesis of Mechanisms (, talk)
Mavridou, Anastasia	(CAV) Capture, Analyze, Diagnose: Realizability Checking of Requirements in FRET (, talk)
Mazowiecki, Filip	(CAV) Verifying generalised and structural soundness of workflow nets via relaxations (, talk)
Mazure, Bertrand	(CP) Aggressive Bound Descent for Constraint Optimization (, talk)
Mazzocchi, Nicolas	(CAV) FORQ-based Language Inclusion Formal Testing (, talk)
Mazzullo, Andrea	(DL) More on Interpolants and Explicit Definitions for Description Logics with Nominals and/or Role Inclusions (, talk)
Meda, Jaydeepsinh	(CAV) Proof-guided Underapproximation Widening for Bounded Model Checking (, talk)
Medioni, Thomas	(CAV) From Spot 2.0 to Spot 2.10: What's New? (, talk)
Meel, Kuldeep S.	(VardiFest) 12 Years and Counting: Samples from My Undergraduate Research Projec () (CP) Boolean Functional Synthesis and its Applications (, talk) (CAV) A Scalable Shannon Entropy Estimator (, talk)
Meggendorfer, Tobias	(CAV) Sound and Complete Certificates for Quantitative Termination Analysis of Probabilistic Programs (, talk)
Melkonian, Orestis	(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) (FMBC) Determinism of ledger updates (, talk)
Meseguer, Jose	(IJCAR) Equational Unification and Matching, and Symbolic Reachability Analysis in Maude 3.2 (System Description) (, talk)
Metzger, Niklas	(CAV) Explaining Hyperproperty Violations (, talk) (CAV) Information Flow Guided Synthesis (, talk)
Meyer, Fabian	(WST) Improved Automatic Complexity Analysis of Integer Programs (, talk) (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)
Michel, Friedrich	(DL) Efficient TBox Reasoning with Value Restrictions using the FL0wer Reasoner (Extended Abstract) (, talk)
Middeldorp, Aart	(WST) Hydra Battles and AC Termination (, talk)
Milo, Mikkel	(FMBC) Finding smart contract vulnerabilities with ConCert's property-based testing framework (, talk)
Mitsch, Stefan	(IJCAR) Implicit Definitions with Differential Equations for KeYmaera X (System Description) (, talk)
Mittelmann, Munyque	(VardiFest) Automated Synthesis of Mechanisms (, talk)
Mogavero, Fabio	(VardiFest) Strategy Logic: Origin, Results, and Open Questions (, talk)
Molin, Adam	(FoMLAS) Formal Specification for Learning-Enabled Autonomous Systems (, talk)
Monroe, Hunter	(PC) Average-Case Hardness of Proving Tautologies and Theorems (, talk)
Montali, Marco	(IJCAR) CTL* Model Checking for Data-Aware Dynamic Systems with Arithmetic (, talk) (DL) Extraction of Object-Centric Event Logs through Virtual Knowledge Graphs (, talk)
Montanari, Angelo	(VardiFest) The Safety Fragment of LTL (, talk)
Mora, Federico	(CAV) UCLID5: Multi-Modal Formal Modeling, Verification, and Synthesis (, talk)
Mosca, Alessandro	(DL) Ontology-based Data Federation (Extended Abstract) (, talk)
Moser, Georg	(CAV) Automated Expected Amortised Cost Analysis of Probabilistic Data Structures (, talk)
Moses, Yoram	(VardiFest) A Toast for Moshe at the FLoC VardiFest (, talk) (CAV) Information Flow Guided Synthesis (, talk)
Murano, Aniello	(VardiFest) Formal Aspects of Strategic Reasoning in MAS (, talk) (VardiFest) Automated Synthesis of Mechanisms (, talk)
Muruganandham, Pazhamalai	(CAV) PAC Statistical Model Checking of Mean Payoff in Discrete- and Continuous-Time MDP (, talk)
Méndez, Julián	(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)
Müller, Peter	(CAV) Sound Automation of Magic Wands (, talk)
N
Nabeshima, Hidetomo	(POS) DPS: A Framework for Deterministic Parallel SAT Solvers (, talk)
Nagendra, Srinidhi	(FMBC) A Domain Specific Language for Testing Consensus Implementations (, talk)
Nagisetty, Vineel	(VardiFest) A Solver + Gradient Descent Training Algorithm for Deep Neural Network (, )
Nalon, Cláudia	(IJCAR) Local Reductions for the Modal Cube (, talk) (DL) A Labelled Natural Deduction System for an Intuitionistic Description Logic with Nominals (, talk)
Nam, Seunghyeon	(CAV) SMT-based Translation Validation for Machine Learning Compiler (, talk)
Narodytska, Nina	(FoMLAS) Scalable Verification of GNN-based Job Schedulers (, talk)
Nebel, Bernhard	(DL) Expressivity of Planning with Horn Description Logic Ontologies (Extended Abstract) (, talk)
Nelson, Tim	(VardiFest) Little Tricky Logic: Misconceptions in the Understanding of LTL (, talk)
Nguewouo, Franklin	(CP) Extended Abstract for : Scheduling the Equipment Maintenance of an Electric Power Transmission Network using Constraint Programming (, talk)
Nickovic, Dejan	(FoMLAS) Formal Specification for Learning-Enabled Autonomous Systems (, talk)
Nielsen, Eske Hoy	(FMBC) Finding smart contract vulnerabilities with ConCert's property-based testing framework (, talk)
Niemetz, Aina	(IJCAR) Flexible Proof Production in an Industrial-Strength SMT Solver (, talk) (CAV) Murxla: A Modular and Highly Extensible API Fuzzer for SMT Solvers (, talk)
Nightingale, Peter	(CP) Selecting SAT Encodings for Pseudo-Boolean and Linear Integer Constraints (, talk)
Noetzli, Andres	(IJCAR) Flexible Proof Production in an Industrial-Strength SMT Solver (, talk) (IJCAR) Reasoning About Vectors using an SMT Theory of Sequences (, talk) (CAV) Even Faster Conflicts and Lazier Reductions for String Solvers (, talk)
Nuradiansyah, Adrian	(DL) Optimal ABox Repair w.r.t. Static EL TBoxes: from Quantified ABoxes back to ABoxes (Extended Abstract) (, talk)
O
O'Sullivan, Barry	(CP) Symmetry breaking and Knowledge Compilation (, talk) (CP) Automated SAT Problem Feature Extraction using 1 Convolutional Autoencoders (, talk) (CP) Finding Counterfactual Explanations through Constraint Relaxations (, talk)
Obitsu, Yuto	(POS) DPS: A Framework for Deterministic Parallel SAT Solvers (, talk)
Offtermatt, Philip	(CAV) Verifying generalised and structural soundness of workflow nets via relaxations (, talk)
Oltmann, Thomas	(POS) SATViz: Real-Time Visualization of Clausal Proofs (, talk)
Ortiz, Magdalena	(IJCAR) Actions over Core-Closed Knowledge Bases (, talk) (DL) Pointwise Circumscription in Description Logics (, talk)
Ostrovsky, Matan	(FoMLAS) An Abstraction-Refinement Approach to Verifying Convolutional Neural Networks (, talk)
Ouaknine, Joel	(VardiFest) Algorithms, Complexity, Verification: From Cook and Karp to Vardi; or, a Brief Glimpse of the Skolem Landscape (, talk)
Ozdemir, Alex	(IJCAR) Flexible Proof Production in an Industrial-Strength SMT Solver (, talk)
P
Pal, Debtanu	(IJCAR) On Eventual Non-negativity and Positivity for the Weighted Sum of Powers of Matrices (, talk)
Papacchini, Fabio	(IJCAR) Local Reductions for the Modal Cube (, talk)
Papadimitratos, Panagiotis	(CP) Optimized Code Generation against Power Side Channels (, talk)
Park, Junkil	(IJCAR) Reasoning About Vectors using an SMT Theory of Sequences (, talk)
Parlato, Gennaro	(CAV) Reasoning about Data Trees using CHCs (, talk)
Parno, Bryan	(FoMLAS) Self-Correcting Neural Networks For Safe Classification (, talk)
Parsia, Bijan	(DL) Next Steps for ReAD: Modules for Classification Optimisation (, talk)
Parthasarathy, Gaurav	(CAV) Sound Automation of Magic Wands (, talk)
Passmore, Grant	(FoMLAS) Neural Networks in Imandra: Matrix Representation as a Verification Choice (, talk)
Pathak, Drashti	(CAV) Data-Driven Invariant Learning for Probabilistic Programs (, talk)
Pau, Cleo	(IJCAR) A Framework for Approximate Generalization in Quantitative Theories (, talk)
Paulsen, Brandon	(CAV) Example Guided Synthesis of Linear Approximations for Neural Network Verification (, talk)
Peitl, Tomáš	(PC) QCDCL with Cube Learning or Pure Literal Elimination – What is best? (, talk) (PC) Are Hitting Formulas Hard for Resolution? (, talk)
Peled, Doron	(FoMLAS) Formal Specification for Learning-Enabled Autonomous Systems (, talk)
Peng, Xiao	(CP) Solving the Non-Crossing MAPF for non point-sized robots (, talk)
Pereira Matos Júnior, João Batista	(FoMLAS) CEG4N: Counter-Example Guided Neural Network Quantization Refinement (, talk)
Perelli, Giuseppe	(VardiFest) On the Extraordinary Effectiveness of Logic in Strategic Reasoning (, talk)
Perez, Mateo	(VardiFest) An Automata-Theoretic Approach to Model-Free Reinforcement Learning (, talk)
Perrussel, Laurent	(VardiFest) Automated Synthesis of Mechanisms (, talk)
Pesant, Gilles	(CP) Exploiting Model Entropy to Make Branching Decisions in Constraint Programming (, talk) (CP) Combining Reinforcement Learning and Constraint Programming for Sequence-Generation Tasks with Hard Constraints - Extended Abstract (, talk)
Petković Komel, Anja	(FMBC) Automating Security Analysis of Off-Chain Protocols (, talk)
Piepenbrock, Jelle	(IJCAR) Guiding an Automated Theorem Prover with Neural Rewriting (, talk)
Pimentel, Elaine	(IJCAR) Non-associative, Non-commutative Multi-Modal Linear Logic (, talk)
Piterman, Nir	(IJCAR) Actions over Core-Closed Knowledge Bases (, talk) (VardiFest) Modelling with Reconfigurable Communication Interfaces (, talk)
Pitoni, Valentina	(VardiFest) An Epistemic Logic for modelling Cooperative Agents (, talk)
Platzer, André	(IJCAR) Implicit Definitions with Differential Equations for KeYmaera X (System Description) (, talk)
Polgreen, Elizabeth	(CAV) UCLID5: Multi-Modal Formal Modeling, Verification, and Synthesis (, talk)
Popescu, Andrei	(IJCAR) Rensets and Renaming-Based Recursion for Syntax with Bindings (, talk)
Popovic, Louis	(CP) Extended Abstract for : Scheduling the Equipment Maintenance of an Electric Power Transmission Network using Constraint Programming (, talk)
Popovič, Alexej	(DL) On the Eve of True Explainability for OWL Ontologies: Description Logic Proofs with Evee and Evonne (, talk)
Porello, Daniele	(DL) Evaluating the Interpretability of Threshold Operators (, talk)
Potomkin, Kostiantyn	(CAV) Reachability of Koopman Linearized Systems Using Random Fourier Feature Observables and Polynomial Zonotope Refinement (, talk)
Prasad, Siddharth	(CP) Improved Sample Complexity Bounds for Branch-and-Cut (, talk)
Preiner, Mathias	(IJCAR) Flexible Proof Production in an Industrial-Strength SMT Solver (, talk) (CAV) Murxla: A Modular and Highly Extensible API Fuzzer for SMT Solvers (, talk)
Pressburger, Thomas	(CAV) Capture, Analyze, Diagnose: Realizability Checking of Requirements in FRET (, talk)
Pukancová, Júlia	(DL) An API for DL Abduction Solvers (, talk) (DL) Hybrid MHS-MXP ABox Abduction Solver: First Emprical Results (, talk)
Putot, Sylvie	(CAV) RINO: Robust INner and Outer Approximated Reachability of Neural Networks Controlled Systems (, talk)
Putruele, Luciano	(CAV) Playing Against Fair Adversaries in Stochastic Games with Total Rewards (, talk)
Păsăreanu, Corina	(FoMLAS) VPN: Verification of Poisoning in Neural Networks (, talk) (FoMLAS) A Cascade of Checkers for Run-time Certification of Local Robustness (, talk) (FoMLAS) Self-Correcting Neural Networks For Safe Classification (, talk)
Q
Qadeer, Shaz	(IJCAR) Reasoning About Vectors using an SMT Theory of Sequences (, talk)
Quimper, Claude-Guy	(CP) Extended Abstract: Acquiring Maps of Interrelated Conjectures on Sharp Bounds (, talk) (CP) Extended Abstract: Constraint Acquisition Based on Solution Counting (, talk)
R
Rain, Sophie	(FMBC) Automating Security Analysis of Off-Chain Protocols (, talk)
Raskin, Jean-Francois	(VardiFest) Strategy synthesis for Global Window PCTL (, talk)
Rawson, Michael	(FMBC) Automating Security Analysis of Off-Chain Protocols (, talk)
Raška, Martin	(IJCAR) Binary Codes that do Not Preserve Primitivity (, talk)
Reeves, Joseph	(IJCAR) Preprocessing of Propagation Redundant Clauses (, talk)
Refaeli, Idan	(FoMLAS) Minimal Multi-Layer Modifications of Deep Neural Networks (, talk)
Refaeli, Idan	(CAV) Neural Network Robustness as a Verification Property: A Principled Case Study (, talk)
Renault, Etienne	(CAV) From Spot 2.0 to Spot 2.10: What's New? (, talk)
Renkin, Florian	(CAV) From Spot 2.0 to Spot 2.10: What's New? (, talk)
Reynolds, Andrew	(IJCAR) Flexible Proof Production in an Industrial-Strength SMT Solver (, talk) (IJCAR) Cooperating Techniques for Solving Nonlinear Arithmetic in the cvc5 SMT Solver (System Description) (, talk) (IJCAR) Reasoning About Vectors using an SMT Theory of Sequences (, talk) (CAV) Even Faster Conflicts and Lazier Reductions for String Solvers (, talk)
Riazanov, Artur	(PC) Proof complexity of natural formulas via communication arguments (, talk)
Rieser, Verena	(FoMLAS) Why Robust Natural Language Understanding is a Challenge (, talk)
Righetti, Guendalina	(DL) Evaluating the Interpretability of Threshold Operators (, talk)
Robillard, Simon	(IJCAR) Goéland: A Concurrent Tableau-Based Theorem Prover (System Description) (, talk)
Rodrigues Greati, Vitor	(IJCAR) Finite Two-Dimensional Proof Systems for Non-finitely Axiomatizable Logics (, talk)
Rodríguez-Núñez, Clara	(IJCAR) Using Automated Reasoning Techniques for Enhancing the Efficiency and Security of (Ethereum) Smart Contracts (, talk) (CAV) Distilling Constraints in Zero-Knowledge Protocols (, talk)
Rosain, Johann	(IJCAR) Goéland: A Concurrent Tableau-Based Theorem Prover (System Description) (, talk)
Rousseau, Louis-Martin	(CP) Peel-and-Bound: Generating Stronger Relaxed Bounds with Multivalued Decision Diagrams (, talk)
Roy, Subhajit	(CP) Boolean Functional Synthesis and its Applications (, talk) (CAV) Data-Driven Invariant Learning for Probabilistic Programs (, talk) (CAV) Proof-guided Underapproximation Widening for Bounded Model Checking (, talk)
Rubin, Sasha	(VardiFest) Trace-view vs Strategy-view of the Environment in Reactive Synthesis (, )
Rubio, Albert	(IJCAR) Using Automated Reasoning Techniques for Enhancing the Efficiency and Security of (Ethereum) Smart Contracts (, talk) (CAV) Distilling Constraints in Zero-Knowledge Protocols (, talk)
Rubio, Ruben	(IJCAR) Equational Unification and Matching, and Symbolic Reachability Analysis in Maude 3.2 (System Description) (, talk)
Rudich, Isaac	(CP) Peel-and-Bound: Generating Stronger Relaxed Bounds with Multivalued Decision Diagrams (, talk)
Rudolph, Sebastian	(DL) AGM Revision in Description Logics Under Fixed-Domain Semantics (, talk) (DL) Modelling Multiple Perspectives by Standpoint-Enhanced DLs (, talk)
Rungta, Neha	(CAV) A Billion SMT Queries a Day ()
Ryzhikov, Vladislav	(DL) Reverse Engineering of Temporal Queries with and without LTL Ontologies: First Steps (, talk)
S
Saarinen, Sam	(VardiFest) Little Tricky Logic: Misconceptions in the Understanding of LTL (, talk)
Sakr, Mostafa	(DL) Fine-Grained Forgetting for the Description Logic ALC (, talk)
Sanchez, Cesar	(FMBC) Multi: a Formal Playground for Smart Multi-contract interaction (, talk)
Sandholm, Tuomas	(CP) Improved Sample Complexity Bounds for Branch-and-Cut (, talk)
Sattler, Uli	(DL) Next Steps for ReAD: Modules for Classification Optimisation (, talk)
Saue, Aurélien	(FMBC) FAT CAT: Formal Acceptance Testing of Contracts for Administering Tokens (, talk)
Savateev, Yury	(DL) Reverse Engineering of Temporal Queries with and without LTL Ontologies: First Steps (, talk)
Scedrov, Andre	(IJCAR) Non-associative, Non-commutative Multi-Modal Linear Logic (, talk)
Schapira, Michael	(FoMLAS) Verification-Aided Deep Ensemble Selection (, talk)
Schaus, Pierre	(CP) Solving the Constrained Single-Row Facility Layout Problem with Decision Diagrams (Extended Abstract) (, talk) (CP) Extended Abstract: Sequence Variables for Routing Problems (, talk)
Schlehuber-Caissier, Philipp	(CAV) From Spot 2.0 to Spot 2.10: What's New? (, talk)
Schmidt, Renate A.	(DL) Fine-Grained Forgetting for the Description Logic ALC (, talk)
Schumann, Johann	(CAV) Capture, Analyze, Diagnose: Realizability Checking of Requirements in FRET (, talk)
Schutt, Andreas	(CP) Explaining Propagation for Gini and Spread with Variable Mean (Extended Abstract) (, talk)
Seshia, Sanjit A.	(CAV) UCLID5: Multi-Modal Formal Modeling, Verification, and Synthesis (, talk)
Sharif, Mahmood	(FoMLAS) Scalable Verification of GNN-based Job Schedulers (, talk)
Sharygina, Natasha	(CAV) SolCMC: Solidity Compiler’s Model Checker (, talk)
Sheng, Ying	(IJCAR) Reasoning About Vectors using an SMT Theory of Sequences (, talk)
Shukla, Sandeep	(VardiFest) A Short Talk Proposal for the VardiFest "On the Not So Unusual Effectiveness of Logic" (, talk)
Siber, Julian	(CAV) Explaining Hyperproperty Violations (, talk)
Simkus, Mantas	(DL) Pointwise Circumscription in Description Logics (, talk)
Simonin, Olivier	(CP) Solving the Non-Crossing MAPF for non point-sized robots (, talk)
Singerman, Eli	(VardiFest) Moshe Vardi and Intel Corporation: Long and Fruitful Collaboration (, talk)
Singh, Gagandeep	(FoMLAS) Scalable Verification of GNN-based Job Schedulers (, talk) (CAV) Shared Certificates for Neural Network Verification (, talk)
Sochański, Michał	(IJCAR) Synthetic Tableaux: Minimal Tableau Search Heuristics (, talk)
Sojakova, Kristina	(FMBC) FAT CAT: Formal Acceptance Testing of Contracts for Administering Tokens (, talk)
Solnon, Christine	(CP) Solving the Non-Crossing MAPF for non point-sized robots (, talk)
Somenzi, Fabio	(VardiFest) An Automata-Theoretic Approach to Model-Free Reinforcement Learning (, talk)
Song, Fu	(CAV) PoS4MPC: Automated Security Policy Synthesis for Secure Multi-Party Computation (, talk)
Song, Xidan	(FoMLAS) CEG4N: Counter-Example Guided Neural Network Quantization Refinement (, talk)
Soos, Mate	(POS) Combining CDCL, Gauss-Jordan Elimination, and Proof Generation (, talk)
Soutchanski, Mikhail	(VardiFest) Towards Combination of Logic and Calculus for Near-Optimal Planning in Relational Hybrid Systems (, talk)
Spaan, Matthijs T. J.	(CAV) Abstraction-Refinement for Hierarchical Probabilistic Models (, talk)
Spitters, Bas	(FMBC) Finding smart contract vulnerabilities with ConCert's property-based testing framework (, talk)
Sprecher, Christian	(CAV) Shared Certificates for Neural Network Verification (, talk)
Srinivasa, Christopher	(VardiFest) A Solver + Gradient Descent Training Algorithm for Deep Neural Network (, )
Srivas, Mandayam	(FMBC) A Domain Specific Language for Testing Consensus Implementations (, talk)
Starosta, Štěpán	(IJCAR) Binary Codes that do Not Preserve Primitivity (, talk)
Steinmetz, Marcel	(DL) Expressivity of Planning with Horn Description Logic Ontologies (Extended Abstract) (, talk)
Stewart, Robert	(FoMLAS) Differentiable Logics for Neural Network Training and Verification (, talk)
Stoelinga, Marielle	(CAV) Sampling-Based Verification of CTMCs with Uncertain Rates (, talk)
Strass, Hannes	(DL) Modelling Multiple Perspectives by Standpoint-Enhanced DLs (, talk)
Stuckey, Peter J.	(CP) Explaining Propagation for Gini and Spread with Variable Mean (Extended Abstract) (, talk)
Suda, Martin	(IJCAR) Vampire Getting Noisy: Will Random Bits Help Conquer Chaos? (System Description) (, talk)
Suenaga, Kohei	(CAV) The Lattice-Theoretic Essence of Property Directed Reachability Analysis (, talk) (CAV) Oblivious Online Monitoring for Safety LTL Specification via Fully Homomorphic Encryption (, talk)
Summers, Alexander J.	(CAV) Sound Automation of Magic Wands (, talk)
Sun, Jun	(CAV) Verifying Neural Networks Against Backdoor Attacks (, talk)
Sun, Youcheng	(FoMLAS) VPN: Verification of Poisoning in Neural Networks (, talk)
Szeider, Stefan	(PC) Are Hitting Formulas Hard for Resolution? (, talk)
T
Tack, Guido	(CP) Explaining Propagation for Gini and Spread with Variable Mean (Extended Abstract) (, talk)
Talcott, Carolyn	(IJCAR) Equational Unification and Matching, and Symbolic Reachability Analysis in Maude 3.2 (System Description) (, talk)
Talpin, Jean-Pierre	(CAV) End-to-end Mechanised Proof of an eBPF Virtual Machine for Microcontrollers (, talk)
Tammet, Tanel	(IJCAR) GK: Implementing Full First Order Default Logic for Commonsense Reasoning (System Description) (, talk)
Tan, Yong Kiam	(IJCAR) Implicit Definitions with Differential Equations for KeYmaera X (System Description) (, talk)
Ternovska, Eugenia	(VardiFest) Towards Algebraic Techniques for Descriptive Complexity (, talk)
Theseider Dupre, Daniele	(DL) Reasoning about actions with EL ontologies in a temporal action theory (Extended Abstract) (, talk)
Thiemann, René	(WST) Efficient Formalization of Simplification Orders () (WST) CeTA – A certifier for termCOMP 2022 (, talk)
Thomazo, Michaël	(DL) Complexity Landscape for Counting Queries (Extended abstract) (, talk)
Tian, Jiaxu	(CAV) Trainify: A CEGAR-Driven Training and Verification Framework for Safe Deep Reinforcement Learning (, talk)
Tinelli, Cesare	(IJCAR) Flexible Proof Production in an Industrial-Strength SMT Solver (, talk) (IJCAR) Cooperating Techniques for Solving Nonlinear Arithmetic in the cvc5 SMT Solver (System Description) (, talk) (IJCAR) Reasoning About Vectors using an SMT Theory of Sequences (, talk) (CAV) Even Faster Conflicts and Lazier Reductions for String Solvers (, talk)
Tirtarasa, Satyadharma	(DL) A new dimension to generalization: computing temporal EL concepts from positive examples (Extended Abstract) (, talk)
Toman, David	(DL) Accessing Document Data Sources using Referring Expression Types (, talk)
Tomczyk, Agata	(IJCAR) Synthetic Tableaux: Minimal Tableau Search Heuristics (, talk)
Tonetta, Stefano	(VardiFest) The Safety Fragment of LTL (, talk)
Tourret, Sophie	(IJCAR) Connection-Minimal Abduction in EL via Translation to FOL (, talk) (DL) Connection-minimal Abduction in EL via translation to FOL (Extended Abstract) (, talk)
Trivedi, Ashutosh	(VardiFest) An Automata-Theoretic Approach to Model-Free Reinforcement Learning (, talk)
Trivedi, Nitesh	(CAV) Data-Driven Invariant Learning for Probabilistic Programs (, talk)
Troubitsyna, Elena	(CP) Optimized Code Generation against Power Side Channels (, talk)
Tsoupidi, Rodothea Myrsini	(CP) Optimized Code Generation against Power Side Channels (, talk)
Turhan, Anni-Yasmin	(DL) A new dimension to generalization: computing temporal EL concepts from positive examples (Extended Abstract) (, talk) (DL) Efficient TBox Reasoning with Value Restrictions using the FL0wer Reasoner (Extended Abstract) (, talk)
Turrini, Andrea	(CAV) Divide-and-Conquer Determinization of Büchi Automata based on SCC Decomposition (, talk)
U
Ulrich-Oltean, Felix	(CP) Selecting SAT Encodings for Pseudo-Boolean and Linear Integer Constraints (, talk)
Urabe, Natsuki	(CAV) The Lattice-Theoretic Essence of Property Directed Reachability Analysis (, talk)
Urban, Josef	(IJCAR) Guiding an Automated Theorem Prover with Neural Rewriting (, talk) (FMBC) Proofgold: Blockchain for Formal Methods (, talk)
Urbańczyk, Mateusz	(DL) Comonadic Semantics for Description Logics Games (, talk)
Usman, Muhammad	(FoMLAS) VPN: Verification of Poisoning in Neural Networks (, talk)
V
Vaillant, Pascal	(DL) Category-based Semantics for the Description Logic ALC and Reasoning (, talk)
Vale, Deivid	(WST) Tuple Interpretations and Applications to Higher-Order Runtime Complexity (, talk)
Van Hentenryck, Pascal	(CP) Extended Abstract: Sequence Variables for Routing Problems (, talk)
Vardi, Moshe	(CAV) Divide-and-Conquer Determinization of Büchi Automata based on SCC Decomposition (, talk)
Vechev, Martin	(CAV) Shared Certificates for Neural Network Verification (, talk)
Vianu, Victor	(VardiFest) Fixpoint Logics, Relational Machines, and Computational Complexity (, talk)
Vin, Eric	(CAV) Randomized Synthesis for Diversity and Cost Constraints with Control Improvisation (, talk)
Vinogradova, Polina	(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) (FMBC) Determinism of ledger updates (, talk)
Visentin, Andrea	(CP) Automated SAT Problem Feature Extraction using 1 Convolutional Autoencoders (, talk)
Viswanathan, Arjun	(IJCAR) Flexible Proof Production in an Industrial-Strength SMT Solver (, talk)
Viswanathan, Mahesh	(VardiFest) Verifying Accuracy Claims of Differential Privacy Algorithms (, talk)
Vitercik, Ellen	(CP) Improved Sample Complexity Bounds for Branch-and-Cut (, talk)
Viteri, Scott	(IJCAR) Flexible Proof Production in an Industrial-Strength SMT Solver (, talk)
Volk, Matthias	(CAV) Sampling-Based Verification of CTMCs with Uncertain Rates (, talk)
W
Waga, Masaki	(CAV) Oblivious Online Monitoring for Safety LTL Specification via Fully Homomorphic Encryption (, talk)
Waldmann, Johannes	(WST) Approximating Relative Match-Bounds (, talk) (WST) Certified Matchbox (, talk)
Walker, James	(CP) Selecting SAT Encodings for Pseudo-Boolean and Linear Integer Constraints (, talk)
Wallon, Romain	(CP) On PB Encodings for Constraint Problems (, talk)
Wang, Chao	(CAV) Example Guided Synthesis of Linear Approximations for Neural Network Verification (, talk) (CAV) Synthesizing Fair Decision Trees via Iterative Constraint Solving (, talk)
Wang, Jingbo	(CAV) Synthesizing Fair Decision Trees via Iterative Constraint Solving (, talk)
Wang, Qinshi	(CAV) Verified Erasure Correction in Coq with MathComp and VST (, talk)
Wang, Ruiwei	(CP) CNF Encodings of Binary Constraint Trees (Extended Abstract) (, talk)
Waszkiewicz, Daniel	(POS) Towards an Efficient CNF Encoding of Block Ciphers (, talk)
Wattez, Hugues	(CP) Aggressive Bound Descent for Constraint Optimization (, talk)
Weddell, Grant	(DL) Accessing Document Data Sources using Referring Expression Types (, talk)
Weeks, Noé	(CAV) Sound Automation of Magic Wands (, talk)
Weidenbach, Christoph	(IJCAR) An Efficient Subsumption Test Pipeline for BS(LRA) Clauses (, talk) (IJCAR) Connection-Minimal Abduction in EL via Translation to FOL (, talk) (IJCAR) Semantic Relevance (, talk) (IJCAR) SCL(EQ): SCL for First-Order Logic with Equality (, talk) (DL) Connection-minimal Abduction in EL via translation to FOL (Extended Abstract) (, talk)
Welt, Michael	(DL) Concept Abduction for Description Logics (, talk)
Wen, Xuejun	(CAV) Trainify: A CEGAR-Driven Training and Verification Framework for Safe Deep Reinforcement Learning (, talk)
Wilhelmi, Rüdiger	(VardiFest) Checking Legal Contracts - On a Not So Usual Application of Mechanized Logic (, talk)
Winkler, Sarah	(IJCAR) CTL* Model Checking for Data-Aware Dynamic Systems with Arithmetic (, talk)
Winkler, Tobias	(CAV) Does a Program Yield the Right Distribution? Verifying Probabilistic Programs via Generating Functions (, talk)
Wolf, Verena	(CAV) MoGym: Using Formal Models for Training and Verifying Decision-making Agents (, talk)
Wolter, Frank	(DL) More on Interpolants and Explicit Definitions for Description Logics with Nominals and/or Role Inclusions (, talk) (DL) Reverse Engineering of Temporal Queries with and without LTL Ontologies: First Steps (, talk)
Woltran, Stefan	(IJCAR) Sequent Calculi for Choice Logics (, talk)
Wu, Haoze	(FoMLAS) Scalable Verification of GNN-based Job Schedulers (, talk)
Wäldele, Lucas	(POS) SATViz: Real-Time Visualization of Clausal Proofs (, talk)
X
Xiao, Guohui	(DL) Extraction of Object-Centric Event Logs through Virtual Knowledge Graphs (, talk) (DL) Ontology-based Data Federation (Extended Abstract) (, talk)
Xiong, Jing	(DL) Extraction of Object-Centric Event Logs through Virtual Knowledge Graphs (, talk) (DL) Ontology-based Data Federation (Extended Abstract) (, talk)
Y
Yamada, Akihisa	(WST) Efficient Formalization of Simplification Orders () (IJCAR) Term Ordering for Non-Reachability of (Conditional) Rewriting (, talk)
Yang, Hui	(IJCAR) Hypergraph-Based Inference Rules for Computing EL+-Ontology Justifications (, talk)
Yap, Roland	(CP) CNF Encodings of Binary Constraint Trees (Extended Abstract) (, talk)
Ying, Mingsheng	(CAV) Verifying Fairness in Quantum Machine Learning (, talk)
Yolcu, Emre	(PC) Exponential separations using guarded extension variables (, talk)
Yu, Geunyeol	(CAV) STLmc: Robust STL Model Checking of Hybrid Systems using SMT (, talk)
Yuan, Shenghao	(CAV) End-to-end Mechanised Proof of an eBPF Virtual Machine for Microcontrollers (, talk)
Z
Zakharyaschev, Michael	(DL) Reverse Engineering of Temporal Queries with and without LTL Ontologies: First Steps (, talk)
Zandberg, Koen	(CAV) End-to-end Mechanised Proof of an eBPF Virtual Machine for Microcontrollers (, talk)
Zarriess, Benjamin	(DL) Efficient TBox Reasoning with Value Restrictions using the FL0wer Reasoner (Extended Abstract) (, talk)
Zelazny, Tom	(FoMLAS) Verification-Aided Deep Ensemble Selection (, talk)
Zhang, Liangfeng	(CAV) PoS4MPC: Automated Security Policy Synthesis for Secure Multi-Party Computation (, talk)
Zhang, Lijun	(CAV) Divide-and-Conquer Determinization of Büchi Automata based on SCC Decomposition (, talk)
Zhang, Min	(FoMLAS) Neural Network Verification with Proof Production (, talk) (CAV) Trainify: A CEGAR-Driven Training and Verification Framework for Safe Deep Reinforcement Learning (, talk)
Zhang, Naifeng	(POS) Towards the shortest DRAT proof of the Pigeonhole Principle (, talk)
Zhang, Xindi	(CAV) Local Search For SMT on Linear Integer Arithmetic (, talk)
Zhao, Haoruo	(DL) Next Steps for ReAD: Modules for Classification Optimisation (, talk)
Zheng, Yang	(FoMLAS) Tight Neural Network Verification via Semidefinite Relaxations and Linear Reformulations (, talk)
Zhi, Dapeng	(CAV) Trainify: A CEGAR-Driven Training and Verification Framework for Safe Deep Reinforcement Learning (, talk)
Zhong, Allen Z.	(CP) Exploiting Functional Constraints in Automatic Dominance Breaking for Constraint Optimization (Extended Abstract) (, talk)
Zhu, Shufang	(VardiFest) LTLf Synthesis as AND-OR Graph Search: Knowledge Compilation at Work (, talk)
Zohar, Yoni	(IJCAR) Flexible Proof Production in an Industrial-Strength SMT Solver (, talk) (IJCAR) Reasoning About Vectors using an SMT Theory of Sequences (, talk) (IJCAR) Effective Semantics for the Modal Logics K and KT via Non-deterministic Matrices (, talk)
Zuber, Johann	(POS) SATViz: Real-Time Visualization of Clausal Proofs (, talk)
Zuleger, Florian	(CAV) Automated Expected Amortised Cost Analysis of Probabilistic Data Structures (, talk)
Ś
Ślusarz, Natalia	(FoMLAS) Differentiable Logics for Neural Network Training and Verification (, talk)
Š
Šmahlíková, Barbora	(CAV) Complementing Büchi Automata with Ranker (, talk)
Ž
Žikelić, Đorđe	(CAV) Sound and Complete Certificates for Quantitative Termination Analysis of Probabilistic Programs (, talk)