LPAR 2023: Keyword Index

KeywordPapers
a
abductionAn Interactive SMT Tactic in Coq using Abductive Reasoning
abstraction refinementTighter Abstract Queries in Neural Network Verification
algebraic data typesCollaborative Inference of Combined Invariants
Answer Set ProgrammingA Fast and Accurate ASP Counting Based Network Reliability Estimator
arithmeticRefining Unification with Abstraction
A Mathematical Benchmark for Inductive Theorem Provers
Automata-basedModel Checking Omega-Regular Hyperproperties with AutoHyperQ
automated reasoningEmbedding Intuitionistic into Classical Logic
On the Complexity of Convex and Reverse Convex Prequadratic Constraints
automated theorem proversA Mathematical Benchmark for Inductive Theorem Provers
automated theorem provingRefining Unification with Abstraction
How Much Should This Symbol Weigh? A GNN-Advised Clause Selection
b
benchmarkA Mathematical Benchmark for Inductive Theorem Provers
c
causalityCounterfactuals Modulo Temporal Logics
CEGARTighter Abstract Queries in Neural Network Verification
Collaborative Inference of Combined Invariants
Certified implementationKeep me out of the loop: a more flexible choreographic projection
Choreographic ProgrammingKeep me out of the loop: a more flexible choreographic projection
Clause EvaluationGuiding an Instantiation Prover with Graph Neural Networks
Clause selectionHow Much Should This Symbol Weigh? A GNN-Advised Clause Selection
Collaborative InferenceCollaborative Inference of Combined Invariants
computational complexityOn the Complexity of Convex and Reverse Convex Prequadratic Constraints
conditioningSyntactic computation of Fagin-Halpern conditioning in possibility theory
conflict analysisAnalyzing Multiple Conflicts in SAT: An Experimental Evaluation
Constrained Horn ClausesCollaborative Inference of Combined Invariants
constraintsScalable Probabilistic Routes
contract-based reasoningTrace-based Deductive Verification
CoqAn Interactive SMT Tactic in Coq using Abductive Reasoning
counterfactualsCounterfactuals Modulo Temporal Logics
cvc5An Interactive SMT Tactic in Coq using Abductive Reasoning
d
decidabilityCounterfactuals Modulo Temporal Logics
decision diagramsScalable Probabilistic Routes
declarative semanticsLogic of Differentiable Logics: Towards a Uniform Semantics of DL
deductive verificationTrace-based Deductive Verification
Differentiable LogicLogic of Differentiable Logics: Towards a Uniform Semantics of DL
distributed protocolsKeep me out of the loop: a more flexible choreographic projection
e
Euclidean AlgorithmsFormalization of Algebraic Theorems in PVS (Invited Talk)
Euclidean DomainsFormalization of Algebraic Theorems in PVS (Invited Talk)
experimental evaluationAnalyzing Multiple Conflicts in SAT: An Experimental Evaluation
f
finite fieldsSMT Solving over Finite Field Arithmetic
finite satisfiability problemAn excursion to the border of decidability: between two- and three-variable logic
first-order model buildingExploring Partial Models with SCL
first-order reasoningExploring Partial Models with SCL
formal verificationOverapproximation of Non-Linear Integer Arithmetic for Smart Contract Verification
Formalization of Algebraic StructuresFormalization of Algebraic Theorems in PVS (Invited Talk)
Fuzzy LogicLogic of Differentiable Logics: Towards a Uniform Semantics of DL
g
Graph Neural NetworkHow Much Should This Symbol Weigh? A GNN-Advised Clause Selection
Graph Neural NetworksGuiding an Instantiation Prover with Graph Neural Networks
h
hypercubesToward Optimal Radio Colorings of Hypercubes via SAT-solving
HyperpropertiesModel Checking Omega-Regular Hyperproperties with AutoHyperQ
Cartesian Reachability Logic: A Language-parametric Logic for Verifying k-Safety Properties
HyperQPTLModel Checking Omega-Regular Hyperproperties with AutoHyperQ
i
inductionA Mathematical Benchmark for Inductive Theorem Provers
inductive invariantsCollaborative Inference of Combined Invariants
inductive theorem proversA Mathematical Benchmark for Inductive Theorem Provers
infinite modelExperiments on Infinite Model Finding in SMT Solving
interpretationsRepresentation, Verification, and Visualization of Tarskian Interpretations for Typed First-order Logic
intuitionistic logicEmbedding Intuitionistic into Classical Logic
k
k-safetyCartesian Reachability Logic: A Language-parametric Logic for Verifying k-Safety Properties
knowledge compilationScalable Probabilistic Routes
l
Language-parametricCartesian Reachability Logic: A Language-parametric Logic for Verifying k-Safety Properties
Linear Integer ArithmeticOverapproximation of Non-Linear Integer Arithmetic for Smart Contract Verification
logicCartesian Reachability Logic: A Language-parametric Logic for Verifying k-Safety Properties
m
machine learningHow 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 logicCounterfactuals Modulo Temporal Logics
model checkingModel Checking Omega-Regular Hyperproperties with AutoHyperQ
model theoryEmbedding Intuitionistic into Classical Logic
mu-calculusTrace-based Deductive Verification
n
network reliabilityA Fast and Accurate ASP Counting Based Network Reliability Estimator
neural networksTighter Abstract Queries in Neural Network Verification
non-linear arithmeticOn the Complexity of Convex and Reverse Convex Prequadratic Constraints
non-linear integer arithmeticOverapproximation of Non-Linear Integer Arithmetic for Smart Contract Verification
non-linear real arithmeticOverapproximation of Non-Linear Integer Arithmetic for Smart Contract Verification
non-redundant learningExploring Partial Models with SCL
o
OEISA Mathematical Benchmark for Inductive Theorem Provers
p
polynomial arithmeticSMT Solving over Finite Field Arithmetic
possibility theorySyntactic computation of Fagin-Halpern conditioning in possibility theory
probabilistic logicLogic of Differentiable Logics: Towards a Uniform Semantics of DL
PromptnessModel Checking Omega-Regular Hyperproperties with AutoHyperQ
proof theoryEmbedding Intuitionistic into Classical Logic
PVSFormalization of Algebraic Theorems in PVS (Invited Talk)
q
QPTLModel Checking Omega-Regular Hyperproperties with AutoHyperQ
QuaternionsFormalization of Algebraic Theorems in PVS (Invited Talk)
r
radio coloringsToward Optimal Radio Colorings of Hypercubes via SAT-solving
RoutingScalable Probabilistic Routes
s
samplingScalable Probabilistic Routes
SATAnalyzing Multiple Conflicts in SAT: An Experimental Evaluation
Toward Optimal Radio Colorings of Hypercubes via SAT-solving
Satisfiability Modulo TheoriesOn the Complexity of Convex and Reverse Convex Prequadratic Constraints
satisfiability problemAn excursion to the border of decidability: between two- and three-variable logic
saturation-based theorem provingHow Much Should This Symbol Weigh? A GNN-Advised Clause Selection
SCLExploring Partial Models with SCL
smart contractsOverapproximation of Non-Linear Integer Arithmetic for Smart Contract Verification
SMTExperiments on Infinite Model Finding in SMT Solving
SMT solvingSMT Solving over Finite Field Arithmetic
Overapproximation of Non-Linear Integer Arithmetic for Smart Contract Verification
SMTCoqAn Interactive SMT Tactic in Coq using Abductive Reasoning
SyGuSExperiments on Infinite Model Finding in SMT Solving
symbolic executionTrace-based Deductive Verification
t
temporal logicCounterfactuals Modulo Temporal Logics
theorem provingGuiding an Instantiation Prover with Graph Neural Networks
Keep me out of the loop: a more flexible choreographic projection
three-variable logicAn excursion to the border of decidability: between two- and three-variable logic
TPTPRepresentation, Verification, and Visualization of Tarskian Interpretations for Typed First-order Logic
trace contractsTrace-based Deductive Verification
Triangular SetsSMT Solving over Finite Field Arithmetic
two-variable logicAn excursion to the border of decidability: between two- and three-variable logic
typesLogic of Differentiable Logics: Towards a Uniform Semantics of DL
u
unificationRefining Unification with Abstraction
Unification with AbstractionRefining Unification with Abstraction
uniform one-dimensional fragmentAn excursion to the border of decidability: between two- and three-variable logic
v
verificationModel 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 basesSyntactic computation of Fagin-Halpern conditioning in possibility theory
Weighted Model CountingA Fast and Accurate ASP Counting Based Network Reliability Estimator