LPAR-26: Author Index| Author | Papers |
|---|
| A | | Artikis, Alexander | Stream Reasoning with Sequencing | | B | | Baaz, Matthias | First-Order Tableaux with Unification for Henkin Quantifiers | | Bartocci, Ezio | STLSat — An Improved Tableau for Satisfiability Checking of Signal Temporal Logic Formulas | | Blanqui, Frédéric | Aligning HOL-Light and Rocq Libraries Formally
Formal Verification of Proofs from Automated Theorem Provers for Higher-Order Logic | | Bombardelli, Alberto | Induction and K-Induction for Hyperproperties | | Briefs, Yasmine | Extending SMT Solving with Non-Ground Clause Learning | | C | | Cailler, Julie | Challenging Benchmarks for Diagrammatic Equivalence of Circuits in TPTP and SMT-LIB | | Chew, Leroy | Reintroducing the Second Player in EPR | | Chiari, Michele | STLSat — An Improved Tableau for Satisfiability Checking of Signal Temporal Logic Formulas | | Chvalovský, Karel | Teaching Vampire New Tricks: An Experimental Study of Neural Clause Selection | | Cipollina, Matteo | Formalized Hopfield Networks and Boltzmann Machines | | Codish, Michael | Compact Partial Symmetry Breaking for Graph Search Problems | | Corbineau, Pierre | A Minimalist Approach to Trustworthy Programming with Precise Types using Small Inversions | | D | | Delorme, Noé | Challenging Benchmarks for Diagrammatic Equivalence of Circuits in TPTP and SMT-LIB | | Dershowitz, Nachum | de Vrijer's Strong Normalization in Haskell | | Dokoupil, David | Simple Complementation of Generalized Büchi Automata | | F | | Fiuk, Oskar | Maslov's class K with Equivalence | | G | | Gamsakhurdia, Mariami | First-Order Tableaux with Unification for Henkin Quantifiers | | Gontard, Antoine | Aligning HOL-Light and Rocq Libraries Formally | | Gros, Basile | A Minimalist Approach to Trustworthy Programming with Precise Types using Small Inversions | | H | | Henne, Michał | Subsumption in FL_⊥reg with TBox Is in ExpTime. | | Henzinger, Thomas A. | Reasoning About Hyperproperties with Automated Theorem Provers | | Heule, Marijn | Coloring Queens with Thousands of Encodings | | Hithnawi, Anwar | Scaling Zero Knowledge UNSAT Verification via Normalized Chaining | | J | | Janota, Mikoláš | Reintroducing the Second Player in EPR
Compact Partial Symmetry Breaking for Graph Search Problems | | K | | Karatarakis, Michail | Formalized Hopfield Networks and Boltzmann Machines | | Karthikeyan, Ashwin | Scaling Zero Knowledge UNSAT Verification via Normalized Chaining | | Kharitonov, Ethan | Scaling Zero Knowledge UNSAT Verification via Normalized Chaining | | Korovin, Konstantin | Enhancing Superposition Reasoning in Linear Real Arithmetic through Selection and Simplification | | Kovács, Laura | Enhancing Superposition Reasoning in Linear Real Arithmetic through Selection and Simplification
Reasoning About Hyperproperties with Automated Theorem Provers
Thousands of Problems to Lean
Polynomial Invariants for Probabilistic Transition Systems with Unbounded Support | | Kupferman, Orna | Blinking Synthesis | | L | | Lammel, Florian | STLSat — An Improved Tableau for Satisfiability Checking of Signal Temporal Logic Formulas | | Leferink, Wouter | Tight Complexity for Modal Extensions of Lec with K, 4, T | | Leuștean, Ioana | Formalizing a Many-Sorted Hybrid Polyadic Modal Logic in Lean | | Li, Ao | Formally Solving Answer-Construction Problems in Lean | | Lolic, Anela | First-Order Tableaux with Unification for Henkin Quantifiers | | M | | Macovei, Bogdan | Formalizing a Many-Sorted Hybrid Polyadic Modal Logic in Lean | | Maddison, Chris | Formally Solving Answer-Construction Problems in Lean | | Mahler, Stella | First-Order Tableaux with Unification for Henkin Quantifiers | | Meel, Kuldeep S. | Formally Solving Answer-Construction Problems in Lean
Scaling Zero Knowledge UNSAT Verification via Normalized Chaining | | Monin, Jean-Francois | A Minimalist Approach to Trustworthy Programming with Precise Types using Small Inversions | | Morawska, Barbara | Subsumption in FL_⊥reg with TBox Is in ExpTime. | | N | | Nießen, Tobias | Reasoning About Hyperproperties with Automated Theorem Provers | | O | | Oliveira da Costa, Ana | Reasoning About Hyperproperties with Automated Theorem Provers | | Oltean, Alexandru | Formalizing a Many-Sorted Hybrid Polyadic Modal Logic in Lean | | Olšák, Miroslav | Reintroducing the Second Player in EPR | | Ong, Luke | Polynomial Invariants for Probabilistic Transition Systems with Unbounded Support | | P | | Palmeri, Jordin | LLM-Assisted Formal Verification of Bit-vector Invertibility Conditions in Rocq | | Panja, Promit | Comparison Invariants for Verifying Control Invariance | | Parys, Paweł | Subsumption in FL_⊥reg with TBox Is in ExpTime. | | Pitsikalis, Manolis | Stream Reasoning with Sequencing | | Platzer, André | Comparison Invariants for Verifying Control Invariance | | Polaczek, Axel | Thousands of Problems to Lean | | Przybocki, Benjamin | Coloring Queens with Thousands of Encodings
A SAT Attack on Tarski's High School Algebra Problem | | R | | Ramanayake, Revantha | Tight Complexity for Modal Extensions of Lec with K, 4, T | | S | | Sanchez, Cesar | Induction and K-Induction for Hyperproperties | | Schoisswohl, Johannes | Enhancing Superposition Reasoning in Linear Real Arithmetic through Selection and Simplification
Reasoning About Hyperproperties with Automated Theorem Provers | | Schreuder, Anne | Polynomial Invariants for Probabilistic Transition Systems with Unbounded Support | | Schuckman, Jacob | LLM-Assisted Formal Verification of Bit-vector Invertibility Conditions in Rocq | | Secrist, Liam | LLM-Assisted Formal Verification of Bit-vector Invertibility Conditions in Rocq | | Shamash Halevy, Naama | Blinking Synthesis | | Steen, Alexander | Formal Verification of Proofs from Automated Theorem Provers for Higher-Order Logic
Experiments on Automating Boolos' Curious Inference | | Strejček, Jan | Simple Complementation of Generalized Büchi Automata | | Stuckey, Peter J. | Compact Partial Symmetry Breaking for Graph Search Problems | | Subercaseaux, Bernardo | Coloring Queens with Thousands of Encodings
A SAT Attack on Tarski's High School Algebra Problem | | Suda, Martin | Teaching Vampire New Tricks: An Experimental Study of Neural Clause Selection
Reintroducing the Second Player in EPR | | Sun, Jialiang | Formally Solving Answer-Construction Problems in Lean | | T | | Tammet, Tanel | Representation Abstraction and Proof Search for English-to-Logic Question Answering | | Tang, Yuzhi | Formally Solving Answer-Construction Problems in Lean | | Taprogge, Melanie | Formal Verification of Proofs from Automated Theorem Provers for Higher-Order Logic
Experiments on Automating Boolos' Curious Inference | | Tonetta, Stefano | Induction and K-Induction for Hyperproperties | | Tourret, Sophie | Challenging Benchmarks for Diagrammatic Equivalence of Circuits in TPTP and SMT-LIB | | Truong, Ha | LLM-Assisted Formal Verification of Bit-vector Invertibility Conditions in Rocq | | U | | Urban, Josef | Teaching Vampire New Tricks: An Experimental Study of Neural Clause Selection | | V | | Viswanathan, Arjun | LLM-Assisted Formal Verification of Bit-vector Invertibility Conditions in Rocq | | Voronkov, Andrei | Enhancing Superposition Reasoning in Linear Real Arithmetic through Selection and Simplification | | W | | Weidenbach, Christoph | Extending SMT Solving with Non-Ground Clause Learning | | Wiedijk, Freek | Formalized Hopfield Networks and Boltzmann Machines | | Winkler, Lorenz | Polynomial Invariants for Probabilistic Transition Systems with Unbounded Support | | Z | | Zamponi, Marco | STLSat — An Improved Tableau for Satisfiability Checking of Signal Temporal Logic Formulas | | Zohar, Yoni | LLM-Assisted Formal Verification of Bit-vector Invertibility Conditions in Rocq |
|
|
