A |

abduction | An Interactive SMT Tactic in Coq using Abductive Reasoning |

abstraction refinement | Tighter Abstract Queries in Neural Network Verification |

algebraic data types | Collaborative Inference of Combined Invariants |

Answer Set Programming | A Fast and Accurate ASP Counting Based Network Reliability Estimator |

arithmetic | Refining Unification with Abstraction A Mathematical Benchmark for Inductive Theorem Provers |

Automata-based | Model Checking Omega-Regular Hyperproperties with AutoHyperQ |

automated reasoning | Embedding Intuitionistic into Classical Logic On the Complexity of Convex and Reverse Convex Prequadratic Constraints |

automated theorem provers | A Mathematical Benchmark for Inductive Theorem Provers |

automated theorem proving | Refining Unification with Abstraction How Much Should This Symbol Weigh? A GNN-Advised Clause Selection |

B |

benchmark | A Mathematical Benchmark for Inductive Theorem Provers |

C |

causality | Counterfactuals Modulo Temporal Logics |

CEGAR | Tighter Abstract Queries in Neural Network Verification Collaborative Inference of Combined Invariants |

Certified implementation | Keep me out of the loop: a more flexible choreographic projection |

Choreographic Programming | Keep me out of the loop: a more flexible choreographic projection |

Clause Evaluation | Guiding an Instantiation Prover with Graph Neural Networks |

Clause selection | How Much Should This Symbol Weigh? A GNN-Advised Clause Selection |

Collaborative Inference | Collaborative Inference of Combined Invariants |

computational complexity | On the Complexity of Convex and Reverse Convex Prequadratic Constraints |

conditioning | Syntactic computation of Fagin-Halpern conditioning in possibility theory |

conflict analysis | Analyzing Multiple Conflicts in SAT: An Experimental Evaluation |

Constrained Horn Clauses | Collaborative Inference of Combined Invariants |

constraints | Scalable Probabilistic Routes |

contract-based reasoning | Trace-based Deductive Verification |

Coq | An Interactive SMT Tactic in Coq using Abductive Reasoning |

counterfactuals | Counterfactuals Modulo Temporal Logics |

cvc5 | An Interactive SMT Tactic in Coq using Abductive Reasoning |

D |

decidability | Counterfactuals Modulo Temporal Logics |

decision diagrams | Scalable Probabilistic Routes |

declarative semantics | Logic of Differentiable Logics: Towards a Uniform Semantics of DL |

deductive verification | Trace-based Deductive Verification |

Differentiable Logic | Logic of Differentiable Logics: Towards a Uniform Semantics of DL |

distributed protocols | Keep me out of the loop: a more flexible choreographic projection |

E |

Euclidean Algorithms | Formalization of Algebraic Theorems in PVS (Invited Talk) |

Euclidean Domains | Formalization of Algebraic Theorems in PVS (Invited Talk) |

experimental evaluation | Analyzing Multiple Conflicts in SAT: An Experimental Evaluation |

F |

finite fields | SMT Solving over Finite Field Arithmetic |

finite satisfiability problem | An excursion to the border of decidability: between two- and three-variable logic |

first-order model building | Exploring Partial Models with SCL |

first-order reasoning | Exploring Partial Models with SCL |

formal verification | Overapproximation of Non-Linear Integer Arithmetic for Smart Contract Verification |

Formalization of Algebraic Structures | Formalization of Algebraic Theorems in PVS (Invited Talk) |

Fuzzy Logic | Logic of Differentiable Logics: Towards a Uniform Semantics of DL |

G |

Graph Neural Network | How Much Should This Symbol Weigh? A GNN-Advised Clause Selection |

Graph Neural Networks | Guiding an Instantiation Prover with Graph Neural Networks |

H |

hypercubes | Toward Optimal Radio Colorings of Hypercubes via SAT-solving |

Hyperproperties | Model Checking Omega-Regular Hyperproperties with AutoHyperQ Cartesian Reachability Logic: A Language-parametric Logic for Verifying k-Safety Properties |

HyperQPTL | Model Checking Omega-Regular Hyperproperties with AutoHyperQ |

I |

induction | A Mathematical Benchmark for Inductive Theorem Provers |

inductive invariants | Collaborative Inference of Combined Invariants |

inductive theorem provers | A Mathematical Benchmark for Inductive Theorem Provers |

infinite model | Experiments on Infinite Model Finding in SMT Solving |

interpretations | Representation, Verification, and Visualization of Tarskian Interpretations for Typed First-order Logic |

intuitionistic logic | Embedding Intuitionistic into Classical Logic |

K |

k-safety | Cartesian Reachability Logic: A Language-parametric Logic for Verifying k-Safety Properties |

knowledge compilation | Scalable Probabilistic Routes |

L |

Language-parametric | Cartesian Reachability Logic: A Language-parametric Logic for Verifying k-Safety Properties |

Linear Integer Arithmetic | Overapproximation of Non-Linear Integer Arithmetic for Smart Contract Verification |

logic | Cartesian Reachability Logic: A Language-parametric Logic for Verifying k-Safety Properties |

M |

machine learning | How Much Should This Symbol Weigh? A GNN-Advised Clause Selection Guiding an Instantiation Prover with Graph Neural Networks Logic of Differentiable Logics: Towards a Uniform Semantics of DL |

modal logic | Counterfactuals Modulo Temporal Logics |

model checking | Model Checking Omega-Regular Hyperproperties with AutoHyperQ |

model theory | Embedding Intuitionistic into Classical Logic |

mu-calculus | Trace-based Deductive Verification |

N |

network reliability | A Fast and Accurate ASP Counting Based Network Reliability Estimator |

neural networks | Tighter Abstract Queries in Neural Network Verification |

non-linear arithmetic | On the Complexity of Convex and Reverse Convex Prequadratic Constraints |

non-linear integer arithmetic | Overapproximation of Non-Linear Integer Arithmetic for Smart Contract Verification |

non-linear real arithmetic | Overapproximation of Non-Linear Integer Arithmetic for Smart Contract Verification |

non-redundant learning | Exploring Partial Models with SCL |

O |

OEIS | A Mathematical Benchmark for Inductive Theorem Provers |

P |

polynomial arithmetic | SMT Solving over Finite Field Arithmetic |

possibility theory | Syntactic computation of Fagin-Halpern conditioning in possibility theory |

probabilistic logic | Logic of Differentiable Logics: Towards a Uniform Semantics of DL |

Promptness | Model Checking Omega-Regular Hyperproperties with AutoHyperQ |

proof theory | Embedding Intuitionistic into Classical Logic |

PVS | Formalization of Algebraic Theorems in PVS (Invited Talk) |

Q |

QPTL | Model Checking Omega-Regular Hyperproperties with AutoHyperQ |

Quaternions | Formalization of Algebraic Theorems in PVS (Invited Talk) |

R |

radio colorings | Toward Optimal Radio Colorings of Hypercubes via SAT-solving |

Routing | Scalable Probabilistic Routes |

S |

sampling | Scalable Probabilistic Routes |

SAT | Analyzing Multiple Conflicts in SAT: An Experimental Evaluation Toward Optimal Radio Colorings of Hypercubes via SAT-solving |

Satisfiability Modulo Theories | On the Complexity of Convex and Reverse Convex Prequadratic Constraints |

satisfiability problem | An excursion to the border of decidability: between two- and three-variable logic |

saturation-based theorem proving | How Much Should This Symbol Weigh? A GNN-Advised Clause Selection |

SCL | Exploring Partial Models with SCL |

smart contracts | Overapproximation of Non-Linear Integer Arithmetic for Smart Contract Verification |

SMT | Experiments on Infinite Model Finding in SMT Solving |

SMT solving | SMT Solving over Finite Field Arithmetic Overapproximation of Non-Linear Integer Arithmetic for Smart Contract Verification |

SMTCoq | An Interactive SMT Tactic in Coq using Abductive Reasoning |

SyGuS | Experiments on Infinite Model Finding in SMT Solving |

symbolic execution | Trace-based Deductive Verification |

T |

temporal logic | Counterfactuals Modulo Temporal Logics |

theorem proving | Guiding an Instantiation Prover with Graph Neural Networks Keep me out of the loop: a more flexible choreographic projection |

three-variable logic | An excursion to the border of decidability: between two- and three-variable logic |

TPTP | Representation, Verification, and Visualization of Tarskian Interpretations for Typed First-order Logic |

trace contracts | Trace-based Deductive Verification |

Triangular Sets | SMT Solving over Finite Field Arithmetic |

two-variable logic | An excursion to the border of decidability: between two- and three-variable logic |

types | Logic of Differentiable Logics: Towards a Uniform Semantics of DL |

U |

unification | Refining Unification with Abstraction |

Unification with Abstraction | Refining Unification with Abstraction |

uniform one-dimensional fragment | An excursion to the border of decidability: between two- and three-variable logic |

V |

verification | Model Checking Omega-Regular Hyperproperties with AutoHyperQ Tighter Abstract Queries in Neural Network Verification Representation, Verification, and Visualization of Tarskian Interpretations for Typed First-order Logic |

W |

weighted knowledge bases | Syntactic computation of Fagin-Halpern conditioning in possibility theory |

Weighted Model Counting | A Fast and Accurate ASP Counting Based Network Reliability Estimator |