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 |