LPAR 2023: Author Index

AuthorPapers
A
Arielly de Lima, ThaynaraFormalization of Algebraic Theorems in PVS (Invited Talk)
Avelar, Andréia B.Formalization of Algebraic Theorems in PVS (Invited Talk)
Ayala-Rincon, MauricioFormalization of Algebraic Theorems in PVS (Invited Talk)
B
Barbosa, HanielAn Interactive SMT Tactic in Coq using Abductive Reasoning
Barrett, ClarkAn Interactive SMT Tactic in Coq using Abductive Reasoning
Tighter Abstract Queries in Neural Network Verification
Begdouri, AhlameSyntactic computation of Fagin-Halpern conditioning in possibility theory
Bendík, JaroslavOverapproximation of Non-Linear Integer Arithmetic for Smart Contract Verification
Benferhat, SalemSyntactic computation of Fagin-Halpern conditioning in possibility theory
Beutner, RavenModel Checking Omega-Regular Hyperproperties with AutoHyperQ
Bhayat, AhmedRefining Unification with Abstraction
Bromberger, MartinExploring Partial Models with SCL
Brown, ChadA Mathematical Benchmark for Inductive Theorem Provers
Brown, ChadExperiments on Infinite Model Finding in SMT Solving
Bubel, RichardTrace-based Deductive Verification
Bártek, FilipHow Much Should This Symbol Weigh? A GNN-Advised Clause Selection
C
Chvalovský, KarelGuiding an Instantiation Prover with Graph Neural Networks
Cohen, ElazarTighter Abstract Queries in Neural Network Verification
Cruz-Filipe, LuísKeep 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, CaroleSyntactic computation of Fagin-Halpern conditioning in possibility theory
E
Elboher, Yizhak YisraelTighter Abstract Queries in Neural Network Verification
Ettarguy, OmarSyntactic computation of Fagin-Halpern conditioning in possibility theory
F
Fedyukovich, GrigoryCollaborative Inference of Combined Invariants
Finkbeiner, BerndModel Checking Omega-Regular Hyperproperties with AutoHyperQ
Counterfactuals Modulo Temporal Logics
Fiuk, OskarAn excursion to the border of decidability: between two- and three-variable logic
Fontaine, PascalRepresentation, Verification, and Visualization of Tarskian Interpretations for Typed First-order Logic
G
Galdino, André LuizFormalization of Algebraic Theorems in PVS (Invited Talk)
Gauthier, ThibaultA Mathematical Benchmark for Inductive Theorem Provers
Gurov, DilianTrace-based Deductive Verification
H
Hader, ThomasSMT Solving over Finite Field Arithmetic
Hamza, JadOn the Complexity of Convex and Reverse Convex Prequadratic Constraints
Heule, MarijnToward Optimal Radio Colorings of Hypercubes via SAT-solving
Hozzová, PetraOverapproximation of Non-Linear Integer Arithmetic for Smart Contract Verification
Hähnle, ReinerTrace-based Deductive Verification
J
Janota, MikolasA Mathematical Benchmark for Inductive Theorem Provers
Experiments on Infinite Model Finding in SMT Solving
K
Kabir, MohimenulA Fast and Accurate ASP Counting Based Network Reliability Estimator
Kaliszyk, CezaryExperiments on Infinite Model Finding in SMT Solving
Katz, GuyTighter Abstract Queries in Neural Network Verification
Keller, ChantalAn Interactive SMT Tactic in Coq using Abductive Reasoning
Kieronski, EmanuelAn excursion to the border of decidability: between two- and three-variable logic
Komendantskaya, EkaterinaLogic of Differentiable Logics: Towards a Uniform Semantics of DL
Korovin, KonstantinRefining Unification with Abstraction
Guiding an Instantiation Prover with Graph Neural Networks
Kostyukov, YuriiCollaborative Inference of Combined Invariants
Kovács, LauraRefining Unification with Abstraction
SMT Solving over Finite Field Arithmetic
Kuncak, ViktorOn the Complexity of Convex and Reverse Convex Prequadratic Constraints
L
Liang, VictorScalable Probabilistic Routes
M
McKeown, JackRepresentation, 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, FabrizioKeep me out of the loop: a more flexible choreographic projection
Mordvinov, DmitryCollaborative Inference of Combined Invariants
N
Nutz, AlexanderOverapproximation of Non-Linear Integer Arithmetic for Smart Contract Verification
O
Obdrzalek, JanCartesian Reachability Logic: A Language-parametric Logic for Verifying k-Safety Properties
Oliveras, AlbertAnalyzing Multiple Conflicts in SAT: An Experimental Evaluation
P
Parsert, JulianExperiments on Infinite Model Finding in SMT Solving
Piepenbrock, JelleGuiding an Instantiation Prover with Graph Neural Networks
Pluska, AlexanderEmbedding Intuitionistic into Classical Logic
R
Rasmussen, Robert R.Keep me out of the loop: a more flexible choreographic projection
Raya, RodrigoOn the Complexity of Convex and Reverse Convex Prequadratic Constraints
Reynolds, AndrewAn Interactive SMT Tactic in Coq using Abductive Reasoning
Ritirc, DanielaSMT Solving over Finite Field Arithmetic
Rodeh, YoavOverapproximation of Non-Linear Integer Arithmetic for Smart Contract Verification
Rodríguez-Carbonell, EnricAnalyzing Multiple Conflicts in SAT: An Experimental Evaluation
S
Scaletta, MarcoTrace-based Deductive Verification
Schoisswohl, JohannesRefining Unification with Abstraction
Schwarz, SimonExploring Partial Models with SCL
Serbanuta, TraianCartesian Reachability Logic: A Language-parametric Logic for Verifying k-Safety Properties
Siber, JulianCounterfactuals Modulo Temporal Logics
Stark, KathrinLogic of Differentiable Logics: Towards a Uniform Semantics of DL
Steen, AlexanderRepresentation, Verification, and Visualization of Tarskian Interpretations for Typed First-order Logic
Stewart, RobertLogic of Differentiable Logics: Towards a Uniform Semantics of DL
Subercaseaux, BernardoToward Optimal Radio Colorings of Hypercubes via SAT-solving
Suda, MartinHow Much Should This Symbol Weigh? A GNN-Advised Clause Selection
Sutcliffe, GeoffRepresentation, Verification, and Visualization of Tarskian Interpretations for Typed First-order Logic
T
Tinelli, CesareAn Interactive SMT Tactic in Coq using Abductive Reasoning
Tušil, JanCartesian Reachability Logic: A Language-parametric Logic for Verifying k-Safety Properties
U
Urban, JosefGuiding an Instantiation Prover with Graph Neural Networks
A Mathematical Benchmark for Inductive Theorem Provers
V
Viswanathan, ArjunAn Interactive SMT Tactic in Coq using Abductive Reasoning
W
Weidenbach, ChristophExploring Partial Models with SCL
Y
Yang, SuweiScalable Probabilistic Routes
Z
Zhao, RuiAnalyzing Multiple Conflicts in SAT: An Experimental Evaluation
Zuleger, FlorianEmbedding Intuitionistic into Classical Logic
Ś
Ślusarz, NataliaLogic of Differentiable Logics: Towards a Uniform Semantics of DL