LPAR-22: Author Index

AuthorPapers
A
Agarwal, PalakParse Condition: Symbolic Encoding of LL(1) Parsing
Alevizos, EliasWayeb: a Tool for Complex Event Forecasting
Aparicio-Sánchez, DamiánFormal verification of the YubiKey and YubiHSM APIs in Maude-NPA
Apt, KrzysztofWhen Are Two Gossips the Same?
Areces, CarlosReasoning About Prescription and Description Using Prioritized Default Rules
Artikis, AlexanderWayeb: a Tool for Complex Event Forecasting
Asadi, SepidehFunction Summarization Modulo Theories
B
Baader, FranzMatching in the Description Logic FL0 with respect to General TBoxes
Baaz, MatthiasLyndon Interpolation holds for the Prenex ⊃ Prenex Fragment of Gödel Logic
Bardin, SébastienArrays Made Simpler: An Efficient, Scalable and Thorough Preprocessing
Bauer, SabineDecidable Inequalities over Infinite Trees
Bendík, JaroslavEvaluation of Domain Agnostic Approaches for Enumeration of Minimal Unsatisfiable Subsets
Bickford, MarkA Verified Theorem Prover Backend Supported by a Monotonic Library
Biewer, SebastianVerification, Testing, and Runtime Monitoring of Automotive Exhaust Emissions
Blicha, MartinFunction Summarization Modulo Theories
Boker, UdiWhy These Automata Types?
Bottesch, RalphA Verified Efficient Implementation of the LLL Basis Reduction Algorithm
Boudane, AbdelhamidEfficient SAT-Based Encodings of Conditional Cardinality Constraints
C
Cassano, ValentinReasoning About Prescription and Description Using Prioritized Default Rules
Castro, PabloReasoning About Prescription and Description Using Prioritized Default Rules
Cerna, IvanaEvaluation of Domain Agnostic Approaches for Enumeration of Minimal Unsatisfiable Subsets
Charatonik, WitoldTwo-variable First-Order Logic with Counting in Forests
Chatterjee, KrishnenduQuasipolynomial Set-Based Symbolic Algorithms for Parity Games
Chockler, HanaFunction Summarization Modulo Theories
Lookahead-Based SMT Solving
Ciaffaglione, AlbertoThe involutions-as-principal types/application-as-unification Analogy
Ciardo, GianfrancoImproving SAT-based Bounded Model Checking for Existential CTL through Path Reuse
Ciesielski, MaciejRewriting Environment for Arithmetic Circuit Verification
Cohen, LironA Verified Theorem Prover Backend Supported by a Monotonic Library
D
D'Argenio, Pedro R.Verification, Testing, and Runtime Monitoring of Automotive Exhaust Emissions
Das, AnupamLeft-Handed Completeness for Kleene algebra, via Cyclic Proofs
David, RobinArrays Made Simpler: An Efficient, Scalable and Thorough Preprocessing
Davy, GuillaumeExperiments in Verification of Linear Model Predictive Control: Automatic Generation and Formal Verification of an Interior Point Method Algorithm
Dershowitz, NachumGraph Path Orderings
Dietz, Emmanuelle-AnnaThe Weak Completion Semantics and Equality
Doumane, AminaLeft-Handed Completeness for Kleene algebra, via Cyclic Proofs
Dvořák, WolfgangQuasipolynomial Set-Based Symbolic Algorithms for Parity Games
E
Escobar, SantiagoFormal verification of the YubiKey and YubiHSM APIs in Maude-NPA
Even-Mendoza, KarineFunction Summarization Modulo Theories
F
Faran, RachelLTL with Arithmetic and its Applications in Reasoning about Hierarchical Systems
Farinier, BenjaminArrays Made Simpler: An Efficient, Scalable and Thorough Preprocessing
Fedyukovich, GrigoryFunction Summarization Modulo Theories
Fernandez Gil, OliverMatching in the Description Logic FL0 with respect to General TBoxes
Feron, EricExperiments in Verification of Linear Model Predictive Control: Automatic Generation and Formal Verification of an Interior Point Method Algorithm
G
Garoche, Pierre-LoicExperiments in Verification of Linear Model Predictive Control: Automatic Generation and Formal Verification of an Interior Point Method Algorithm
Gleiss, BernhardLoop Analysis by Quantification over Iterations
González-Burgueño, AntonioFormal verification of the YubiKey and YubiHSM APIs in Maude-NPA
Grossi, DavideWhen Are Two Gossips the Same?
Gupta, RahulKnowledge Compilation meets Uniform Sampling
Guskov, YegorTwo-variable First-Order Logic with Counting in Forests
H
Haslbeck, Max W.A Verified Efficient Implementation of the LLL Basis Reduction Algorithm
Henrion, DidierExperiments in Verification of Linear Model Predictive Control: Automatic Generation and Formal Verification of an Interior Point Method Algorithm
Henzinger, MonikaQuasipolynomial Set-Based Symbolic Algorithms for Parity Games
Hermanns, HolgerVerification, Testing, and Runtime Monitoring of Automotive Exhaust Emissions
Hoffmann, JanAutomatic Space Bound Analysis for Functional Programs with Garbage Collection
Hofmann, MartinDecidable Inequalities over Infinite Trees
Honsell, FurioThe involutions-as-principal types/application-as-unification Analogy
Hyvärinen, AnttiFunction Summarization Modulo Theories
Lookahead-Based SMT Solving
SMTS: Distributed, Visualized Constraint Solving
Hölldobler, SteffenThe Weak Completion Semantics and Equality
I
Iosif, RaduA Complete Cyclic Proof System for Inductive Entailments in First Order Logic
J
Jabbour, SaidEfficient SAT-Based Encodings of Conditional Cardinality Constraints
Janota, MikolasTowards Smarter MACE-style Model Finders
Jhunjhunwala, SaketParse Condition: Symbolic Encoding of LL(1) Parsing
Jiang, ChuanImproving SAT-based Bounded Model Checking for Existential CTL through Path Reuse
Jonáš, MartinIs Satisfiability of Quantified Bit-Vector Formulas Stable Under Bit-Width Changes? (Experimental Paper)
Jost, SteffenDecidable Inequalities over Infinite Trees
Jouannaud, Jean-PierreGraph Path Orderings
K
Kovács, LauraLoop Analysis by Quantification over Iterations
Kupferman, OrnaPlaying with the Maximum-Flow Problem
LTL with Arithmetic and its Applications in Reasoning about Hierarchical Systems
Alternating Reachability Games with Behavioral and Revenue Objectives
Köhl, Maximilian A.Verification, Testing, and Runtime Monitoring of Automotive Exhaust Emissions
L
Lemerre, MatthieuArrays Made Simpler: An Efficient, Scalable and Thorough Preprocessing
Lenisa, MarinaThe involutions-as-principal types/application-as-unification Analogy
Lolic, AnelaLyndon Interpolation holds for the Prenex ⊃ Prenex Fragment of Gödel Logic
López-Fraguas, Francisco J.Polymorphic success types for Erlang
M
Marantidis, PavlosMatching in the Description Logic FL0 with respect to General TBoxes
Marescotti, MatteoLookahead-Based SMT Solving
SMTS: Distributed, Visualized Constraint Solving
Meadows, CatherineFormal verification of the YubiKey and YubiHSM APIs in Maude-NPA
Meel, Kuldeep S.Knowledge Compilation meets Uniform Sampling
Meseguer, JoséFormal verification of the YubiKey and YubiHSM APIs in Maude-NPA
Mishchenko, AlanRewriting Environment for Arithmetic Circuit Verification
Montenegro, ManuelPolymorphic success types for Erlang
N
Niu, YueAutomatic Space Bound Analysis for Functional Programs with Garbage Collection
P
Paliouras, GeorgiosWayeb: a Tool for Complex Event Forecasting
Pous, DamienLeft-Handed Completeness for Kleene algebra, via Cyclic Proofs
Pratt-Hartmann, IanTwo-variable First-Order Logic with Counting in Forests
R
Raddaoui, BadranEfficient SAT-Based Encodings of Conditional Cardinality Constraints
Rahli, VincentA Verified Theorem Prover Backend Supported by a Monotonic Library
Rebola-Pardo, AdriánA Theory of Satisfiability-Preserving Proofs in SAT Solving
Robillard, SimonLoop Analysis by Quantification over Iterations
Roy, SubhajitKnowledge Compilation meets Uniform Sampling
Parse Condition: Symbolic Encoding of LL(1) Parsing
Rudolph, SebastianThe Triguarded Fragment of First-Order Logic
S
Sadigova, ParvinLookahead-Based SMT Solving
Sais, LakhdarEfficient SAT-Based Encodings of Conditional Cardinality Constraints
Scagnetto, IvanThe involutions-as-principal types/application-as-unification Analogy
Schwarz, SibylleThe Weak Completion Semantics and Equality
Serban, CristinaA Complete Cyclic Proof System for Inductive Entailments in First Order Logic
Sharma, ShubhamKnowledge Compilation meets Uniform Sampling
Sharygina, NatashaFunction Summarization Modulo Theories
Lookahead-Based SMT Solving
SMTS: Distributed, Visualized Constraint Solving
Simkus, MantasThe Triguarded Fragment of First-Order Logic
Singal, DhruvParse Condition: Symbolic Encoding of LL(1) Parsing
Stefanus, L. YohanesThe Weak Completion Semantics and Equality
Strejček, JanIs Satisfiability of Quantified Bit-Vector Formulas Stable Under Bit-Width Changes? (Experimental Paper)
Su, TiankaiRewriting Environment for Arithmetic Circuit Verification
Suda, MartinTowards Smarter MACE-style Model Finders
A Theory of Satisfiability-Preserving Proofs in SAT Solving
Suárez-García, GorkaPolymorphic success types for Erlang
Svozil, AlexanderQuasipolynomial Set-Based Symbolic Algorithms for Parity Games
T
Tamir, TamiAlternating Reachability Games with Behavioral and Revenue Objectives
Thiemann, RenéA Verified Efficient Implementation of the LLL Basis Reduction Algorithm
v
van der Hoek, WiebeWhen Are Two Gossips the Same?
W
Witkowski, PiotrTwo-variable First-Order Logic with Counting in Forests
Y
Yasin, AtifRewriting Environment for Arithmetic Circuit Verification
Yu, CunxiRewriting Environment for Arithmetic Circuit Verification