LPAR 2023: Author Index

Author	Papers
A
Arielly de Lima, Thaynara	Formalization of Algebraic Theorems in PVS (Invited Talk)
Avelar, Andréia B.	Formalization of Algebraic Theorems in PVS (Invited Talk)
Ayala-Rincon, Mauricio	Formalization of Algebraic Theorems in PVS (Invited Talk)
B
Barbosa, Haniel	An Interactive SMT Tactic in Coq using Abductive Reasoning
Barrett, Clark	An Interactive SMT Tactic in Coq using Abductive Reasoning Tighter Abstract Queries in Neural Network Verification
Begdouri, Ahlame	Syntactic computation of Fagin-Halpern conditioning in possibility theory
Bendík, Jaroslav	Overapproximation of Non-Linear Integer Arithmetic for Smart Contract Verification
Benferhat, Salem	Syntactic computation of Fagin-Halpern conditioning in possibility theory
Beutner, Raven	Model Checking Omega-Regular Hyperproperties with AutoHyperQ
Bhayat, Ahmed	Refining Unification with Abstraction
Bromberger, Martin	Exploring Partial Models with SCL
Brown, Chad	A Mathematical Benchmark for Inductive Theorem Provers
Brown, Chad	Experiments on Infinite Model Finding in SMT Solving
Bubel, Richard	Trace-based Deductive Verification
Bártek, Filip	How Much Should This Symbol Weigh? A GNN-Advised Clause Selection
C
Chvalovský, Karel	Guiding an Instantiation Prover with Graph Neural Networks
Cohen, Elazar	Tighter Abstract Queries in Neural Network Verification
Cruz-Filipe, Luís	Keep me out of the loop: a more flexible choreographic projection
D
Daggitt, Matthew L.	Logic of Differentiable Logics: Towards a Uniform Semantics of DL
Delenne, Carole	Syntactic computation of Fagin-Halpern conditioning in possibility theory
E
Elboher, Yizhak Yisrael	Tighter Abstract Queries in Neural Network Verification
Ettarguy, Omar	Syntactic computation of Fagin-Halpern conditioning in possibility theory
F
Fedyukovich, Grigory	Collaborative Inference of Combined Invariants
Finkbeiner, Bernd	Model Checking Omega-Regular Hyperproperties with AutoHyperQ Counterfactuals Modulo Temporal Logics
Fiuk, Oskar	An excursion to the border of decidability: between two- and three-variable logic
Fontaine, Pascal	Representation, Verification, and Visualization of Tarskian Interpretations for Typed First-order Logic
G
Galdino, André Luiz	Formalization of Algebraic Theorems in PVS (Invited Talk)
Gauthier, Thibault	A Mathematical Benchmark for Inductive Theorem Provers
Gurov, Dilian	Trace-based Deductive Verification
H
Hader, Thomas	SMT Solving over Finite Field Arithmetic
Hamza, Jad	On the Complexity of Convex and Reverse Convex Prequadratic Constraints
Heule, Marijn	Toward Optimal Radio Colorings of Hypercubes via SAT-solving
Hozzová, Petra	Overapproximation of Non-Linear Integer Arithmetic for Smart Contract Verification
Hähnle, Reiner	Trace-based Deductive Verification
J
Janota, Mikolas	A Mathematical Benchmark for Inductive Theorem Provers Experiments on Infinite Model Finding in SMT Solving
K
Kabir, Mohimenul	A Fast and Accurate ASP Counting Based Network Reliability Estimator
Kaliszyk, Cezary	Experiments on Infinite Model Finding in SMT Solving
Katz, Guy	Tighter Abstract Queries in Neural Network Verification
Keller, Chantal	An Interactive SMT Tactic in Coq using Abductive Reasoning
Kieronski, Emanuel	An excursion to the border of decidability: between two- and three-variable logic
Komendantskaya, Ekaterina	Logic of Differentiable Logics: Towards a Uniform Semantics of DL
Korovin, Konstantin	Refining Unification with Abstraction Guiding an Instantiation Prover with Graph Neural Networks
Kostyukov, Yurii	Collaborative Inference of Combined Invariants
Kovács, Laura	Refining Unification with Abstraction SMT Solving over Finite Field Arithmetic
Kuncak, Viktor	On the Complexity of Convex and Reverse Convex Prequadratic Constraints
L
Liang, Victor	Scalable Probabilistic Routes
M
McKeown, Jack	Representation, Verification, and Visualization of Tarskian Interpretations for Typed First-order Logic
Meel, Kuldeep S.	A Fast and Accurate ASP Counting Based Network Reliability Estimator Scalable Probabilistic Routes
Montesi, Fabrizio	Keep me out of the loop: a more flexible choreographic projection
Mordvinov, Dmitry	Collaborative Inference of Combined Invariants
N
Nutz, Alexander	Overapproximation of Non-Linear Integer Arithmetic for Smart Contract Verification
O
Obdrzalek, Jan	Cartesian Reachability Logic: A Language-parametric Logic for Verifying k-Safety Properties
Oliveras, Albert	Analyzing Multiple Conflicts in SAT: An Experimental Evaluation
P
Parsert, Julian	Experiments on Infinite Model Finding in SMT Solving
Piepenbrock, Jelle	Guiding an Instantiation Prover with Graph Neural Networks
Pluska, Alexander	Embedding Intuitionistic into Classical Logic
R
Rasmussen, Robert R.	Keep me out of the loop: a more flexible choreographic projection
Raya, Rodrigo	On the Complexity of Convex and Reverse Convex Prequadratic Constraints
Reynolds, Andrew	An Interactive SMT Tactic in Coq using Abductive Reasoning
Ritirc, Daniela	SMT Solving over Finite Field Arithmetic
Rodeh, Yoav	Overapproximation of Non-Linear Integer Arithmetic for Smart Contract Verification
Rodríguez-Carbonell, Enric	Analyzing Multiple Conflicts in SAT: An Experimental Evaluation
S
Scaletta, Marco	Trace-based Deductive Verification
Schoisswohl, Johannes	Refining Unification with Abstraction
Schwarz, Simon	Exploring Partial Models with SCL
Serbanuta, Traian	Cartesian Reachability Logic: A Language-parametric Logic for Verifying k-Safety Properties
Siber, Julian	Counterfactuals Modulo Temporal Logics
Stark, Kathrin	Logic of Differentiable Logics: Towards a Uniform Semantics of DL
Steen, Alexander	Representation, Verification, and Visualization of Tarskian Interpretations for Typed First-order Logic
Stewart, Robert	Logic of Differentiable Logics: Towards a Uniform Semantics of DL
Subercaseaux, Bernardo	Toward Optimal Radio Colorings of Hypercubes via SAT-solving
Suda, Martin	How Much Should This Symbol Weigh? A GNN-Advised Clause Selection
Sutcliffe, Geoff	Representation, Verification, and Visualization of Tarskian Interpretations for Typed First-order Logic
T
Tinelli, Cesare	An Interactive SMT Tactic in Coq using Abductive Reasoning
Tušil, Jan	Cartesian Reachability Logic: A Language-parametric Logic for Verifying k-Safety Properties
U
Urban, Josef	Guiding an Instantiation Prover with Graph Neural Networks A Mathematical Benchmark for Inductive Theorem Provers
V
Viswanathan, Arjun	An Interactive SMT Tactic in Coq using Abductive Reasoning
W
Weidenbach, Christoph	Exploring Partial Models with SCL
Y
Yang, Suwei	Scalable Probabilistic Routes
Z
Zhao, Rui	Analyzing Multiple Conflicts in SAT: An Experimental Evaluation
Zuleger, Florian	Embedding Intuitionistic into Classical Logic
Ś
Ślusarz, Natalia	Logic of Differentiable Logics: Towards a Uniform Semantics of DL