| 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 |
