LPAR-22: Keyword Index

KeywordPapers
a
ACTLImproving SAT-based Bounded Model Checking for Existential CTL through Path Reuse
Algorithm PortfoliosSMTS: Distributed, Visualized Constraint Solving
amortized analysisAutomatic Space Bound Analysis for Functional Programs with Garbage Collection
antichain-based tree automata language inclusionA Complete Cyclic Proof System for Inductive Entailments in First Order Logic
APIFormal verification of the YubiKey and YubiHSM APIs in Maude-NPA
Arithmetic CircuitsRewriting Environment for Arithmetic Circuit Verification
automataWhy These Automata Types?
Left-Handed Completeness for Kleene algebra, via Cyclic Proofs
automated reasoningLoop Analysis by Quantification over Iterations
axiomatisationLeft-Handed Completeness for Kleene algebra, via Cyclic Proofs
b
bit-widthIs Satisfiability of Quantified Bit-Vector Formulas Stable Under Bit-Width Changes? (Experimental Paper)
Boolean operationsWhy These Automata Types?
Bounded Model CheckingFunction Summarization Modulo Theories
Improving SAT-based Bounded Model Checking for Existential CTL through Path Reuse
c
cardinality constraintsEfficient SAT-Based Encodings of Conditional Cardinality Constraints
CEGARTowards Smarter MACE-style Model Finders
clause learningLookahead-Based SMT Solving
cognitive reasoningThe Weak Completion Semantics and Equality
complexityMatching in the Description Logic FL0 with respect to General TBoxes
A Verified Efficient Implementation of the LLL Basis Reduction Algorithm
The Triguarded Fragment of First-Order Logic
computer algebraRewriting Environment for Arithmetic Circuit Verification
Constrained Uniform SamplingKnowledge Compilation meets Uniform Sampling
constraint satisfactionDecidable Inequalities over Infinite Trees
constraint solvingParse Condition: Symbolic Encoding of LL(1) Parsing
convex optimizationExperiments in Verification of Linear Model Predictive Control: Automatic Generation and Formal Verification of an Interior Point Method Algorithm
CoqA Verified Theorem Prover Backend Supported by a Monotonic Library
cost semanticsAutomatic Space Bound Analysis for Functional Programs with Garbage Collection
counterexampleImproving SAT-based Bounded Model Checking for Existential CTL through Path Reuse
counterfactual reasoningThe Weak Completion Semantics and Equality
Craig interpolationFunction Summarization Modulo Theories
Cyclic GraphsGraph Path Orderings
cyclic proofsLeft-Handed Completeness for Kleene algebra, via Cyclic Proofs
A Complete Cyclic Proof System for Inductive Entailments in First Order Logic
d
d-DNNFKnowledge Compilation meets Uniform Sampling
data streamingWayeb: a Tool for Complex Event Forecasting
deadlockImproving SAT-based Bounded Model Checking for Existential CTL through Path Reuse
decidabilityThe Triguarded Fragment of First-Order Logic
decision proceduresTwo-variable First-Order Logic with Counting in Forests
default logicReasoning About Prescription and Description Using Prioritized Default Rules
deontic logicReasoning About Prescription and Description Using Prioritized Default Rules
Description LogicMatching in the Description Logic FL0 with respect to General TBoxes
Description LogicsThe Triguarded Fragment of First-Order Logic
Digital LibraryA Verified Theorem Prover Backend Supported by a Monotonic Library
Distributed IC3SMTS: Distributed, Visualized Constraint Solving
Distributed SMTSMTS: Distributed, Visualized Constraint Solving
Divide and ConquerSMTS: Distributed, Visualized Constraint Solving
Domain-agnosticEvaluation of Domain Agnostic Approaches for Enumeration of Minimal Unsatisfiable Subsets
e
ECTLImproving SAT-based Bounded Model Checking for Existential CTL through Path Reuse
epistemic logicWhen Are Two Gossips the Same?
EPRTowards Smarter MACE-style Model Finders
equational reasoningThe Weak Completion Semantics and Equality
ErlangPolymorphic success types for Erlang
ethical decision-makingThe Weak Completion Semantics and Equality
event listsFormal verification of the YubiKey and YubiHSM APIs in Maude-NPA
Exclusive-ORFormal verification of the YubiKey and YubiHSM APIs in Maude-NPA
experimental evaluationIs Satisfiability of Quantified Bit-Vector Formulas Stable Under Bit-Width Changes? (Experimental Paper)
f
finite model finderTowards Smarter MACE-style Model Finders
finite satisfiabilityTwo-variable First-Order Logic with Counting in Forests
first-order logicLoop Analysis by Quantification over Iterations
Fluent CalculusThe Weak Completion Semantics and Equality
formal languages and automata theoryWayeb: a Tool for Complex Event Forecasting
formal verificationRewriting Environment for Arithmetic Circuit Verification
fragments of first-order logicThe Triguarded Fragment of First-Order Logic
Function SummariesFunction Summarization Modulo Theories
g
game theoryAlternating Reachability Games with Behavioral and Revenue Objectives
gamesThe involutions-as-principal types/application-as-unification Analogy
garbage collectionAutomatic Space Bound Analysis for Functional Programs with Garbage Collection
general satisfiabilityTwo-variable First-Order Logic with Counting in Forests
Geometry of InteractionThe involutions-as-principal types/application-as-unification Analogy
gossip protocolsWhen Are Two Gossips the Same?
Graph gamesQuasipolynomial Set-Based Symbolic Algorithms for Parity Games
graph rewritingGraph Path Orderings
Gödel logicsLyndon Interpolation holds for the Prenex ⊃ Prenex Fragment of Gödel Logic
h
Herbrand expansionsLyndon Interpolation holds for the Prenex ⊃ Prenex Fragment of Gödel Logic
hierarchical systemsLTL with Arithmetic and its Applications in Reasoning about Hierarchical Systems
i
incremental verificationFunction Summarization Modulo Theories
inductionLeft-Handed Completeness for Kleene algebra, via Cyclic Proofs
inductive definitionsA Complete Cyclic Proof System for Inductive Entailments in First Order Logic
Infeasibility analysisEvaluation of Domain Agnostic Approaches for Enumeration of Minimal Unsatisfiable Subsets
Infinite alphabetsLTL with Arithmetic and its Applications in Reasoning about Hierarchical Systems
infinite descentA Complete Cyclic Proof System for Inductive Entailments in First Order Logic
infinite treesDecidable Inequalities over Infinite Trees
inprocessing techniquesA Theory of Satisfiability-Preserving Proofs in SAT Solving
Integer Linear ProgrammingLTL with Arithmetic and its Applications in Reasoning about Hierarchical Systems
InterferenceA Theory of Satisfiability-Preserving Proofs in SAT Solving
interior point methodExperiments in Verification of Linear Model Predictive Control: Automatic Generation and Formal Verification of an Interior Point Method Algorithm
interpolationLyndon Interpolation holds for the Prenex ⊃ Prenex Fragment of Gödel Logic
invariant generationLoop Analysis by Quantification over Iterations
Isabelle/HOLA Verified Efficient Implementation of the LLL Basis Reduction Algorithm
k
Kleene algebraLeft-Handed Completeness for Kleene algebra, via Cyclic Proofs
knowledge compilationKnowledge Compilation meets Uniform Sampling
knowledge-based protocolsWhen Are Two Gossips the Same?
Kripke semanticsA Verified Theorem Prover Backend Supported by a Monotonic Library
l
lambda calculusThe involutions-as-principal types/application-as-unification Analogy
Lamport clocksFormal verification of the YubiKey and YubiHSM APIs in Maude-NPA
lattice basis reductionA Verified Efficient Implementation of the LLL Basis Reduction Algorithm
linear inequalitiesDecidable Inequalities over Infinite Trees
LL(1) parsingParse Condition: Symbolic Encoding of LL(1) Parsing
logic and computational complexityTwo-variable First-Order Logic with Counting in Forests
logic programmingThe Weak Completion Semantics and Equality
Lookahead HeuristicLookahead-Based SMT Solving
loopLoop Analysis by Quantification over Iterations
LP SolvingAutomatic Space Bound Analysis for Functional Programs with Garbage Collection
LTL with arithmeticLTL with Arithmetic and its Applications in Reasoning about Hierarchical Systems
Lyndon interpolationLyndon Interpolation holds for the Prenex ⊃ Prenex Fragment of Gödel Logic
m
matchingMatching in the Description Logic FL0 with respect to General TBoxes
minimal unsatisfiable subsetsEvaluation of Domain Agnostic Approaches for Enumeration of Minimal Unsatisfiable Subsets
modal logicThe Triguarded Fragment of First-Order Logic
model checkingQuasipolynomial Set-Based Symbolic Algorithms for Parity Games
LTL with Arithmetic and its Applications in Reasoning about Hierarchical Systems
Model Predictive ControlExperiments in Verification of Linear Model Predictive Control: Automatic Generation and Formal Verification of an Interior Point Method Algorithm
modellingEfficient SAT-Based Encodings of Conditional Cardinality Constraints
monotonicityA Verified Theorem Prover Backend Supported by a Monotonic Library
MultigraphsGraph Path Orderings
MUS enumerationEvaluation of Domain Agnostic Approaches for Enumeration of Minimal Unsatisfiable Subsets
mutable memoryFormal verification of the YubiKey and YubiHSM APIs in Maude-NPA
n
Nash equilibriumAlternating Reachability Games with Behavioral and Revenue Objectives
Nonmonotonic Proof CalculusReasoning About Prescription and Description Using Prioritized Default Rules
Numerical Software VerificationExperiments in Verification of Linear Model Predictive Control: Automatic Generation and Formal Verification of an Interior Point Method Algorithm
NuprlA Verified Theorem Prover Backend Supported by a Monotonic Library
o
omega-regular languagesWhy These Automata Types?
operational semanticsAutomatic Space Bound Analysis for Functional Programs with Garbage Collection
p
parity gamesQuasipolynomial Set-Based Symbolic Algorithms for Parity Games
path orderingsGraph Path Orderings
pattern matchingWayeb: a Tool for Complex Event Forecasting
polymorphismPolymorphic success types for Erlang
program analysisExperiments in Verification of Linear Model Predictive Control: Automatic Generation and Formal Verification of an Interior Point Method Algorithm
program verificationLoop Analysis by Quantification over Iterations
progress measureQuasipolynomial Set-Based Symbolic Algorithms for Parity Games
proof checkerA Verified Theorem Prover Backend Supported by a Monotonic Library
propositional satisfiabilityEfficient SAT-Based Encodings of Conditional Cardinality Constraints
protocol verificationFormal verification of the YubiKey and YubiHSM APIs in Maude-NPA
pushdown automataDecidable Inequalities over Infinite Trees
q
quantified bit-vectorsIs Satisfiability of Quantified Bit-Vector Formulas Stable Under Bit-Width Changes? (Experimental Paper)
r
Random walks and Markov chainsWayeb: a Tool for Complex Event Forecasting
Rational synthesisAlternating Reachability Games with Behavioral and Revenue Objectives
reachability gamesAlternating Reachability Games with Behavioral and Revenue Objectives
read-over-write simplificationArrays Made Simpler: An Efficient, Scalable and Thorough Preprocessing
regular languagesDecidable Inequalities over Infinite Trees
Left-Handed Completeness for Kleene algebra, via Cyclic Proofs
Resource AnalysisDecidable Inequalities over Infinite Trees
Resource Bound AnalysisAutomatic Space Bound Analysis for Functional Programs with Garbage Collection
reversible computationsThe involutions-as-principal types/application-as-unification Analogy
rewrite orderingsGraph Path Orderings
s
SATTowards Smarter MACE-style Model Finders
Improving SAT-based Bounded Model Checking for Existential CTL through Path Reuse
SAT solvingA Theory of Satisfiability-Preserving Proofs in SAT Solving
Knowledge Compilation meets Uniform Sampling
Satisfiability Modulo TheoriesFunction Summarization Modulo Theories
Is Satisfiability of Quantified Bit-Vector Formulas Stable Under Bit-Width Changes? (Experimental Paper)
Satisfiability Modulo TheoryExperiments in Verification of Linear Model Predictive Control: Automatic Generation and Formal Verification of an Interior Point Method Algorithm
Arrays Made Simpler: An Efficient, Scalable and Thorough Preprocessing
SkolemizationLyndon Interpolation holds for the Prenex ⊃ Prenex Fragment of Gödel Logic
SMT encodingParse Condition: Symbolic Encoding of LL(1) Parsing
SMT solvingLookahead-Based SMT Solving
software verificationFunction Summarization Modulo Theories
static analysisAutomatic Space Bound Analysis for Functional Programs with Garbage Collection
success typesPolymorphic success types for Erlang
succinctnessWhy These Automata Types?
symbolic computationQuasipolynomial Set-Based Symbolic Algorithms for Parity Games
t
tableaux systemReasoning About Prescription and Description Using Prioritized Default Rules
terminationGraph Path Orderings
Loop Analysis by Quantification over Iterations
The guarded fragmentThe Triguarded Fragment of First-Order Logic
The two-variable fragmentThe Triguarded Fragment of First-Order Logic
Theory of ArraysArrays Made Simpler: An Efficient, Scalable and Thorough Preprocessing
Three-Valued Lukasiewicz LogicThe Weak Completion Semantics and Equality
tree automataMatching in the Description Logic FL0 with respect to General TBoxes
two-variable logic with counting quantifiersTwo-variable First-Order Logic with Counting in Forests
type inferenceAutomatic Space Bound Analysis for Functional Programs with Garbage Collection
type systemsAutomatic Space Bound Analysis for Functional Programs with Garbage Collection
typesPolymorphic success types for Erlang
u
unranked trees/forestsTwo-variable First-Order Logic with Counting in Forests
Unsatisfiability analysisEvaluation of Domain Agnostic Approaches for Enumeration of Minimal Unsatisfiable Subsets
v
Verified theorem prover backendA Verified Theorem Prover Backend Supported by a Monotonic Library
w
Weak CompletionThe Weak Completion Semantics and Equality
web-based GUISMTS: Distributed, Visualized Constraint Solving
WitnessImproving SAT-based Bounded Model Checking for Existential CTL through Path Reuse
word combinatoricsDecidable Inequalities over Infinite Trees
y
YubiHSMFormal verification of the YubiKey and YubiHSM APIs in Maude-NPA
YubiKeyFormal verification of the YubiKey and YubiHSM APIs in Maude-NPA