LPAR 2024: Keyword Index

KeywordPapers
a
abstract interpretationAutomatic Detection of Vulnerable Variables for CTL Properties of Programs
action modelSymbolic Realisation of Epistemic Processes
arithmeticVIRAS: Conflict-Driven Quantifier Elimination for Integer-Real Arithmetic
automated inductive reasoningSaturating Sorting without Sorts
automated reasoningSaturating Sorting without Sorts
Scaling CheckMate for Game-Theoretic Security
First Experiments with Neural cvc5
automated software verificationSaturating Sorting without Sorts
automated theorem provingAutomated Theorem Provers Help Improve Large Language Model Reasoning
Saturating Sorting without Sorts
Waste Reduction: Experiments in Sharing Clauses between Runs of a Portfolio of Strategies (Experimental Paper)
A Generic Deskolemization Strategy
Prover9 Unleashed: Automated Configuration for Enhanced Proof Discovery
b
bagsVerifying SQL queries using theories of tables and relations
belief changeA Tool for Reasoning about Trust and Belief
blockchain protocolsScaling CheckMate for Game-Theoretic Security
Blocked-clause AdditionSometimes Hoarding is Harder than Cleaning: NP-hardness of Maximum Blocked-Clause Addition
bounded tree-widthTree-Verifiable Graph Grammars
btor2mlirEfficient Simulation for Hardware Model Checking
bvDeep Inference in Proof Search: The Need for Shallow Inference
c
call-by-nameHybrid Intersection Types for PCF
call-by-valueHybrid Intersection Types for PCF
certificationTranslating HOL-Light proofs to Coq
Certifying Incremental SAT Solving
choiceExperiments with Choice in Dependently-Typed Higher-Order Logic
CNF formulasSometimes Hoarding is Harder than Cleaning: NP-hardness of Maximum Blocked-Clause Addition
concept alignmentTranslating HOL-Light proofs to Coq
confluenceConfluence for Proof-Nets via Parallel Cut Elimination
Constrained Horn ClausesAutomatic Bit- and Memory-Precise Verification of eBPF Code
constraint solvingMinimizing Sorting Networks at the Sub-Comparator Level
CTLAutomatic Detection of Vulnerable Variables for CTL Properties of Programs
cut eliminationConfluence for Proof-Nets via Parallel Cut Elimination
d
DatalogFuzzy Datalog∃ over Arbitrary t-Norms
decision listsAutomated Synthesis of Decision Lists for Polynomial Specifications over Integers
decision procedureVIRAS: Conflict-Driven Quantifier Elimination for Integer-Real Arithmetic
deep inferenceDeep Inference in Proof Search: The Need for Shallow Inference
dependent HOLExperiments with Choice in Dependently-Typed Higher-Order Logic
dependent type theoryTranslating HOL-Light proofs to Coq
e
eBPFAutomatic Bit- and Memory-Precise Verification of eBPF Code
epistemic logicSymbolic Realisation of Epistemic Processes
epistemic processSymbolic Realisation of Epistemic Processes
epsilon calculusOn Translations of Epsilon Proofs to LK
evaluation strategiesHybrid Intersection Types for PCF
f
first-order logicAutomated Theorem Provers Help Improve Large Language Model Reasoning
first-order theorem provingSaturating Sorting without Sorts
formal methodsSaturating Sorting without Sorts
Free-Variable TableauxA Generic Deskolemization Strategy
Fuzzy LogicFuzzy Datalog∃ over Arbitrary t-Norms
g
game semanticsA Simple Token Game and its Logic
Game-theoretic securityScaling CheckMate for Game-Theoretic Security
Games semanticsReasoning About Group Polarization: From Semantic Games to Sequent Systems
graph grammarsTree-Verifiable Graph Grammars
h
Herbrand sequentsHerbrand's Theorem in Inductive Proofs
higher-order logicTranslating HOL-Light proofs to Coq
Hilbert's epsilon formalismOn Translations of Epsilon Proofs to LK
hypergraphsConfluence for Proof-Nets via Parallel Cut Elimination
i
incentive compatibilityScaling CheckMate for Game-Theoretic Security
Incremental SATCertifying Incremental SAT Solving
inductionRewriting and Inductive Reasoning
Inductive proofsHerbrand's Theorem in Inductive Proofs
intersection typesHybrid Intersection Types for PCF
k
knowledge representationA Tool for Reasoning about Trust and Belief
l
lambda calculusHybrid Intersection Types for PCF
large language modelsAutomated Theorem Provers Help Improve Large Language Model Reasoning
linear logicA Simple Token Game and its Logic
Confluence for Proof-Nets via Parallel Cut Elimination
LIRAVIRAS: Conflict-Driven Quantifier Elimination for Integer-Real Arithmetic
logic programmingAutomated Theorem Provers Help Improve Large Language Model Reasoning
logical frameworksTranslating HOL-Light proofs to Coq
m
machine learningFirst Experiments with Neural cvc5
MLLDeep Inference in Proof Search: The Need for Shallow Inference
modal logicReasoning About Group Polarization: From Semantic Games to Sequent Systems
model checkingEfficient Simulation for Hardware Model Checking
monadic second-order logicTree-Verifiable Graph Grammars
n
natural languageAutomated Theorem Provers Help Improve Large Language Model Reasoning
non-linear integer arithmeticAutomated Synthesis of Decision Lists for Polynomial Specifications over Integers
nondeterminismDeep Inference in Proof Search: The Need for Shallow Inference
NP-hardnessSometimes Hoarding is Harder than Cleaning: NP-hardness of Maximum Blocked-Clause Addition
p
parallel reductionConfluence for Proof-Nets via Parallel Cut Elimination
Portfolio of StrategiesWaste Reduction: Experiments in Sharing Clauses between Runs of a Portfolio of Strategies (Experimental Paper)
PreprocessingSometimes Hoarding is Harder than Cleaning: NP-hardness of Maximum Blocked-Clause Addition
program optimizationMinimizing Sorting Networks at the Sub-Comparator Level
program verificationAutomatic Detection of Vulnerable Variables for CTL Properties of Programs
Automatic Bit- and Memory-Precise Verification of eBPF Code
proof certificateA Generic Deskolemization Strategy
proof checkingCertifying Incremental SAT Solving
Proof SchemaHerbrand's Theorem in Inductive Proofs
proof searchDeep Inference in Proof Search: The Need for Shallow Inference
proof theoryA Simple Token Game and its Logic
proof transformationTranslating HOL-Light proofs to Coq
proof translationTranslating HOL-Light proofs to Coq
Experiments with Choice in Dependently-Typed Higher-Order Logic
proof-netConfluence for Proof-Nets via Parallel Cut Elimination
Proof-Search ProceduresA Generic Deskolemization Strategy
proofsCertifying Incremental SAT Solving
propositional dynamic logicSymbolic Realisation of Epistemic Processes
protocol verificationScaling CheckMate for Game-Theoretic Security
q
quantifier eliminationVIRAS: Conflict-Driven Quantifier Elimination for Integer-Real Arithmetic
quantitative modelsHybrid Intersection Types for PCF
r
ReasoningAutomated Theorem Provers Help Improve Large Language Model Reasoning
recursive programsSaturating Sorting without Sorts
relationsVerifying SQL queries using theories of tables and relations
Resolution CalculusHerbrand's Theorem in Inductive Proofs
resource logicA Simple Token Game and its Logic
reuseWaste Reduction: Experiments in Sharing Clauses between Runs of a Portfolio of Strategies (Experimental Paper)
rewritingTranslating HOL-Light proofs to Coq
Rewriting and Inductive Reasoning
s
SAT solvingSometimes Hoarding is Harder than Cleaning: NP-hardness of Maximum Blocked-Clause Addition
satisfiabilityMinimizing Sorting Networks at the Sub-Comparator Level
Satisfiability Modulo TheoriesCombining Combination Properties: Minimal Models
saturationRewriting and Inductive Reasoning
Saturation-based provingWaste Reduction: Experiments in Sharing Clauses between Runs of a Portfolio of Strategies (Experimental Paper)
SecurityAutomatic Detection of Vulnerable Variables for CTL Properties of Programs
sequent calculusOn Translations of Epsilon Proofs to LK
sequent systemReasoning About Group Polarization: From Semantic Games to Sequent Systems
setsVerifying SQL queries using theories of tables and relations
simulationEfficient Simulation for Hardware Model Checking
SkolemizationA Generic Deskolemization Strategy
SMTVIRAS: Conflict-Driven Quantifier Elimination for Integer-Real Arithmetic
Verifying SQL queries using theories of tables and relations
sorting algorithmsSaturating Sorting without Sorts
sorting networksMinimizing Sorting Networks at the Sub-Comparator Level
SQLVerifying SQL queries using theories of tables and relations
static analysisAutomatic Detection of Vulnerable Variables for CTL Properties of Programs
Automated Synthesis of Decision Lists for Polynomial Specifications over Integers
Steamroller ProblemsAutomated Theorem Provers Help Improve Large Language Model Reasoning
strategy inventionProver9 Unleashed: Automated Configuration for Enhanced Proof Discovery
Strategy SchedulingProver9 Unleashed: Automated Configuration for Enhanced Proof Discovery
superpositionRewriting and Inductive Reasoning
superposition calculusSaturating Sorting without Sorts
symbolic abstractionSymbolic Realisation of Epistemic Processes
symbolic executionSymbolic Realisation of Epistemic Processes
synthesisAutomated Synthesis of Decision Lists for Polynomial Specifications over Integers
system descriptionA Tool for Reasoning about Trust and Belief
t
tablesVerifying SQL queries using theories of tables and relations
theorem provingFirst Experiments with Neural cvc5
theory combinationCombining Combination Properties: Minimal Models
Theory PolitenessCombining Combination Properties: Minimal Models
TrustA Tool for Reasoning about Trust and Belief
Tuple-generating dependenciesFuzzy Datalog∃ over Arbitrary t-Norms
v
verificationEfficient Simulation for Hardware Model Checking
virtual substitutionVIRAS: Conflict-Driven Quantifier Elimination for Integer-Real Arithmetic
w
weakest liberal preconditionSymbolic Realisation of Epistemic Processes