LPAR 2024: 25TH CONFERENCE ON LOGIC FOR PROGRAMMING, ARTIFICIAL INTELLIGENCE AND REASONING

A
Abraham, Erika	On the Idea of Exploration-guided Satisfiability Checking
Adam, Quentin	TBA
Ait El Hara, Hichem Rami	On SMT Theory Design: The Case of Sequences
Akshay, S.	Automated Synthesis of Decision Lists for Polynomial Specifications over Integers
Aleksandrova, Kristina	Prover9 Unleashed: Automated Configuration for Enhanced Proof Discovery
Alt, Leonardo	Automated Test Case Generation for Solidity Using Constrained Horn Clauses
B
Baaz, Matthias	On Translations of Epsilon Proofs to LK
Barenbaum, Pablo	Hybrid Intersection Types for PCF
Barrett, Clark	Verifying SQL queries using theories of tables and relations - virtual talk over Zoom
Baumgartner, Peter	Automated Theorem Provers Help Improve Large Language Model Reasoning
Biere, Armin	30 Years of Faster and Faster SAT Solving Certifying Incremental SAT Solving
Blanqui, Frédéric	Translating HOL-Light proofs to Coq
Blicha, Martin	Golem: A Flexibile and Efficient Solver for Constrained Horn Clauses
Bobot, François	On SMT Theory Design: The Case of Sequences
Bonichon, Richard	A Generic Deskolemization Strategy
Britikov, Konstantin	Golem: A Flexibile and Efficient Solver for Constrained Horn Clauses Automated Test Case Generation for Solidity Using Constrained Horn Clauses
Bromberger, Martin	Automatic Bit- and Memory-Precise Verification of eBPF Code
Brown, Chad	Experiments with Choice in Dependently-Typed Higher-Order Logic
Brugger, Lea Salome	Scaling CheckMate for Game-Theoretic Security
Bury, Guillaume	On SMT Theory Design: The Case of Sequences
C
Cailler, Julie	A Generic Deskolemization Strategy
Chakraborty, Supratik	Automated Synthesis of Decision Lists for Polynomial Specifications over Integers
Chimes, Mark	Tree-Verifiable Graph Grammars
Cruz-Filipe, Luís	Minimizing Sorting Networks at the Sub-Comparator Level
D
de Briey, Lancelot	TBA
Dershowitz, Nachum	Alternate Semantics of the Guarded Conditional
Dramnesc, Isabela	Certification of Tail Recursive Bubble--Sort in Theorema and Coq
F
Fazekas, Katalin	Certifying Incremental SAT Solving
Fedyukovich, Grigory	Automated Test Case Generation for Solidity Using Constrained Horn Clauses
Fermüller, Christian	A Simple Token Game and its Logic Reasoning About Group Polarization: From Semantic Games to Sequent Systems
Fish, Andrew	Automated Reasoning with Tangles: towards Quantum Verification Applications
Fleury, Mathias	Certifying Incremental SAT Solving
Freiman, Robert	A Simple Token Game and its Logic Reasoning About Group Polarization: From Semantic Games to Sequent Systems
G
Georgiou, Pamina	Sorting without Sorts
Gheorghiu, Alexander Victor	A System for Evaluating the Admissibility of Rules for Intuitionistic Propositional Logic
Gottlob, Georg	Fuzzy Datalog$^\exists$ over Arbitrary t-norms
Govind, R.	Automated Synthesis of Decision Lists for Polynomial Specifications over Integers
Guerrieri, Giulio	Confluence for Proof-Nets via Parallel Cut Elimination
Gurfinkel, Arie	Efficient Simulation for Hardware Model Checking
H
Hajdu, Marton	Rewriting and Inductive Reasoning Sorting without Sorts
Heenaye-Mamode Khan, Maleika	TBA
Hennicker, Rolf	Symbolic Realisation of Epistemic Processes
Hermant, Olivier	Numeric Base Conversion with Rewriting A Generic Deskolemization Strategy
Hitzler, Pascal	A Case for Extensional Non-Wellfounded Metamodeling
Hunter, Aaron	A Tool for Reasoning about Trust and Belief
I
Iglesias, Alberto	A Tool for Reasoning about Trust and Belief
Iosif, Radu	Tree-Verifiable Graph Grammars
Israel, Marc	TBA
J
Jakubův, Jan	First Experiments with Neural CVC5 Prover9 Unleashed: Automated Configuration for Enhanced Proof Discovery
Janota, Mikolas	First Experiments with Neural CVC5
Jebelean, Tudor	A Natural Style Prover in Theorema Using Sequent Calculus with Unit Propagation Certification of Tail Recursive Bubble--Sort in Theorema and Coq
K
Kafshdar Goharshady, Amir	Automated Synthesis of Decision Lists for Polynomial Specifications over Integers
Kahramanogullari, Ozan	Deep Inference in Proof Search: The Need for Shallow Inference
Kaliszyk, Cezary	Experiments with Choice in Dependently-Typed Higher-Order Logic Prover9 Unleashed: Automated Configuration for Enhanced Proof Discovery
Katoen, Joost-Pieter	Probabilistic Programs. Verified. Push-Button.
Kesner, Delia	Hybrid Intersection Types for PCF
Knapp, Alexander	Symbolic Realisation of Epistemic Processes
Koon, David	Internships in Mauritius
Korovin, Konstantin	VIRAS: Conflict-Driven Quantifier Elimination for Integer-Real Arithmetic
Kovács, Laura	VIRAS: Conflict-Driven Quantifier Elimination for Integer-Real Arithmetic Rewriting and Inductive Reasoning Scaling CheckMate for Game-Theoretic Security Sorting without Sorts
L
Lang, Timo	A Simple Token Game and its Logic
Lanzinger, Matthias	Fuzzy Datalog$^\exists$ over Arbitrary t-norms
Leitsch, Alexander	Herbrand's Theorem in Inductive Proofs On Proof Schemata and Primitive Recursive Arithmetic
Lisitsa, Alexei	Automated Reasoning with Tangles: towards Quantum Verification Applications Towards computer-assisted proofs of parametric Andrews-Curtis simplifications, II
Loboda, Wojciech	Numeric Base Conversion with Rewriting
Lolic, Anela	On Translations of Epsilon Proofs to LK Herbrand's Theorem in Inductive Proofs On Proof Schemata and Primitive Recursive Arithmetic
M
Mahler, Stella	On Proof Schemata and Primitive Recursive Arithmetic
Manara, Giulia	Confluence for Proof-Nets via Parallel Cut Elimination
Marianne, Thierry	Automated Theorem Proving for Prolog Verification
McGinness, Lachlan	Automated Theorem Provers Help Improve Large Language Model Reasoning
Meel, Kuldeep	Automated Synthesis: An Ideal Meeting Ground for Symbolic Reasoning and Machine Learning
Mesnard, Fred	Automated Theorem Proving for Prolog Verification
Milicich, Mariana	Hybrid Intersection Types for PCF
Miné, Antoine	Automatic Detection of Vulnerable Variables for CTL Properties of Programs
Mohamed, Mudathir Mahgoub Yahia	Verifying SQL queries using theories of tables and relations - virtual talk over Zoom
Motwani, Harshit Jitendra	Automated Synthesis of Decision Lists for Polynomial Specifications over Integers
Moussaoui Remil, Naïm	Automatic Detection of Vulnerable Variables for CTL Properties of Programs
O
Olarte, Carlos	Reasoning About Group Polarization: From Semantic Games to Sequent Systems
P
Payet, Etienne	Automated Theorem Proving for Prolog Verification
Petković Komel, Anja	Scaling CheckMate for Game-Theoretic Security
Piepenbrock, Jelle	First Experiments with Neural CVC5
Pimentel, Elaine	Reasoning About Group Polarization: From Semantic Games to Sequent Systems
Pollitt, Florian	Certifying Incremental SAT Solving
R
Rain, Sophie	Scaling CheckMate for Game-Theoretic Security
Ranalter, Daniel	Experiments with Choice in Dependently-Typed Higher-Order Logic
Rawson, Michael	Rewriting and Inductive Reasoning Scaling CheckMate for Game-Theoretic Security
Reynolds, Andrew	Verifying SQL queries using theories of tables and relations - virtual talk over Zoom
Rosain, Johann	A Generic Deskolemization Strategy
S
Schneider-Kamp, Peter	Minimizing Sorting Networks at the Sub-Comparator Level
Schoisswohl, Johannes	VIRAS: Conflict-Driven Quantifier Elimination for Integer-Real Arithmetic
Schwarz, Simon	Automatic Bit- and Memory-Precise Verification of eBPF Code
Sferrazza, Stefano	Fuzzy Datalog$^\exists$ over Arbitrary t-norms
Sharygina, Natasha	Golem: A Flexibile and Efficient Solver for Constrained Horn Clauses Automated Test Case Generation for Solidity Using Constrained Horn Clauses
Stratulat, Sorin	Certification of Tail Recursive Bubble--Sort in Theorema and Coq
Subercaseaux, Bernardo	Sometimes Hoarding is Harder than Cleaning: NP-hardness of Maximum Blocked-Clause Addition
T
Tafese, Joseph	Efficient Simulation for Hardware Model Checking
Tammet, Tanel	Waste Reduction: Experiments in Sharing Clauses between Runs of a Portfolio of Strategies (Experimental Paper)
Tinelli, Cesare	Verifying SQL queries using theories of tables and relations - virtual talk over Zoom
Toledo, Guilherme	Combining Combination Properties: Minimal Models
Tortora de Falco, Lorenzo	Confluence for Proof-Nets via Parallel Cut Elimination
U
Urban, Caterina	Automatic Detection of Vulnerable Variables for CTL Properties of Programs
Urban, Josef	First Experiments with Neural CVC5
V
Varanasi, Sai Teja	Automated Synthesis of Decision Lists for Polynomial Specifications over Integers
Vaux Auclair, Lionel	Confluence for Proof-Nets via Parallel Cut Elimination
Veanes, Margus	On Symbolic Derivatives and Transition Regexes
W
Wałęga, Przemysław Andrzej	Fuzzy Datalog$^\exists$ over Arbitrary t-norms
Weidenbach, Christoph	Automatic Bit- and Memory-Precise Verification of eBPF Code
Wirsing, Martin	Symbolic Realisation of Epistemic Processes
Z
Zalewski, Joseph	A Case for Extensional Non-Wellfounded Metamodeling
Zlatkin, Ilia	Automated Test Case Generation for Solidity Using Constrained Horn Clauses
Zohar, Yoni	Combining Combination Properties: Minimal Models
Zuleger, Florian	Tree-Verifiable Graph Grammars

Disclaimer | Powered by EasyChair Smart Program