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