LPAR-22: 22ND INTERNATIONAL CONFERENCE ON LOGIC FOR PROGRAMMING, ARTIFICIAL INTELLIGENCE AND REASONING

A
Agarwal, Palak	Parse Condition: A Symbolic Encoding for LL(1) Parsing
Aparicio-Sánchez, Damián	Formal verification of the YubiKey and YubiHSM APIs in Maude-NPA
Apt, Krzysztof	When Are Two Gossips the Same?
Asadi, Sepideh	Function Summarization Modulo Theories
B
Baader, Franz	Matching in the Description Logic FL0 with respect to General TBoxes
Baaz, Matthias	Lyndon Interpolation holds for the Prenex ⊃ Prenex Fragment of Gödel Logic
Bardin, Sébastien	Arrays Made Simpler: An Efficient, Scalable and Thorough Preprocessing
Bash, Tamar	Towards Efficient Metaquery Generator
Bauer, Sabine	Linear Tree Constraints
Ben-Eliyahu-Zohary, Rachel	Towards Efficient Metaquery Generator
Bendík, Jaroslav	Evaluation of Domain Agnostic Approaches for Enumeration of Minimal Unsatisfiable Subsets
Benhamou, Belaid	Symmetry breaking in a new stable model search method
Bickford, Mark	A Verified Theorem Prover Backend Supported by a Monotonic Library
Blicha, Martin	Function Summarization Modulo Theories
Boker, Udi	Why These Automata Types?
Bottesch, Ralph	A Verified Efficient Implementation of the LLL Basis Reduction Algorithm
C
Cerna, Ivana	Evaluation of Domain Agnostic Approaches for Enumeration of Minimal Unsatisfiable Subsets
Charatonik, Witold	Two-variable First-Order Logic with Counting in Forests
Chatterjee, Krishnendu	Quasipolynomial Set-Based Symbolic Algorithms for Parity Games
Chockler, Hana	Function Summarization Modulo Theories Lookahead-Based SMT Solving
Ciaffaglione, Alberto	The Involutions-as-Principal Types/Application-as-Unification Analogy
Ciardo, Gianfranco	Improving SAT-based Bounded Model Checking for Existential CTL through Path Reuse
Ciesielski, Maciej	Rewriting Environment for Arithmetic Circuit Verification
Cohen, Liron	A Verified Theorem Prover Backend Supported by a Monotonic Library
D
Das, Anupam	Completeness of Left Handed Kleene algebra via Cyclic Proofs
David, Robin	Arrays Made Simpler: An Efficient, Scalable and Thorough Preprocessing
Davy, Guillaume	Experiments in Verification of Linear Model Predictive Control: Automatic Generation and Formal Verification of an Interior Point Method Algorithm
Dershowitz, Nachum	Graphs Path Orderings
Dietz Saldanha, Emmanuelle-Anna	The Weak Completion Semantics and Equality
Doumane, Amina	Completeness of Left Handed Kleene algebra via Cyclic Proofs
Dvořák, Wolfgang	Quasipolynomial Set-Based Symbolic Algorithms for Parity Games
E
Escobar, Santiago	Formal verification of the YubiKey and YubiHSM APIs in Maude-NPA
Even-Mendoza, Karine	Function Summarization Modulo Theories
F
Faran, Rachel	LTL with Arithmetic and its Applications in Reasoning about Hierarchical Systems
Farinier, Benjamin	Arrays Made Simpler: An Efficient, Scalable and Thorough Preprocessing
Fedyukovich, Grigory	Function Summarization Modulo Theories
Fernandez Gil, Oliver	Matching in the Description Logic FL0 with respect to General TBoxes
Feron, Eric	Experiments in Verification of Linear Model Predictive Control: Automatic Generation and Formal Verification of an Interior Point Method Algorithm
G
Garoche, Pierre-Loic	Experiments in Verification of Linear Model Predictive Control: Automatic Generation and Formal Verification of an Interior Point Method Algorithm
Gleiss, Bernhard	Loop Analysis by Quantification over Iterations
Goertzel, Ben	Commonsense Reasoning for Robotics and Bioscience via Probabilistic Logic and Meta-learning
González-Burgueño, Antonio	Formal verification of the YubiKey and YubiHSM APIs in Maude-NPA
Grossi, Davide	When Are Two Gossips the Same?
Gupta, Rahul	Knowledge Compilation meets Uniform Sampling
Guskov, Yegor	Two-variable First-Order Logic with Counting in Forests
H
Haslbeck, Max W.	A Verified Efficient Implementation of the LLL Basis Reduction Algorithm
Henrion, Didier	Experiments in Verification of Linear Model Predictive Control: Automatic Generation and Formal Verification of an Interior Point Method Algorithm
Henzinger, Monika	Quasipolynomial Set-Based Symbolic Algorithms for Parity Games
Hermanns, Holger	Verification, Testing, and Runtime Monitoring of Automotive Exhaust Emissions
Hoffmann, Jan	Automatic Space Bound Analysis for Functional Programs with Garbage Collection
Hofmann, Martin	Linear Tree Constraints
Honsell, Furio	The Involutions-as-Principal Types/Application-as-Unification Analogy
Hyvärinen, Antti	SMTS: Distributed, Visualized Constraint Solving Function Summarization Modulo Theories Lookahead-Based SMT Solving
Hölldobler, Steffen	The Weak Completion Semantics and Equality
J
Janota, Mikolas	Towards Smarter MACE-style Model Finders
Jhunjhunwala, Saket	Parse Condition: A Symbolic Encoding for LL(1) Parsing
Jiang, Chuan	Improving SAT-based Bounded Model Checking for Existential CTL through Path Reuse
Jonáš, Martin	Is Satisfiability of Quantified Bit-Vector Formulas Stable Under Bit-Width Changes?
Jost, Steffen	Linear Tree Constraints In Memory of Martin Hofmann
Jouannaud, Jean-Pierre	Graphs Path Orderings
K
Khaled, Tarek	Symmetry breaking in a new stable model search method
Kovacs, Laura	Loop Analysis by Quantification over Iterations
Kupferman, Orna	Variations on the Classical Maximum-Flow Problem Alternating Reachability Games with Behavioral and Revenue Objectives LTL with Arithmetic and its Applications in Reasoning about Hierarchical Systems
L
Lemerre, Matthieu	Arrays Made Simpler: An Efficient, Scalable and Thorough Preprocessing
Lenisa, Marina	The Involutions-as-Principal Types/Application-as-Unification Analogy
Lolic, Anela	Lyndon Interpolation holds for the Prenex ⊃ Prenex Fragment of Gödel Logic
López-Fraguas, Francisco J.	Polymorphic success types for Erlang
M
Marantidis, Pavlos	Matching in the Description Logic FL0 with respect to General TBoxes
Marescotti, Matteo	SMTS: Distributed, Visualized Constraint Solving Lookahead-Based SMT Solving
Meadows, Catherine	Formal 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, Alan	Rewriting Environment for Arithmetic Circuit Verification
Montenegro, Manuel	Polymorphic success types for Erlang
N
Niu, Yue	Automatic Space Bound Analysis for Functional Programs with Garbage Collection
P
Pous, Damien	Completeness of Left Handed Kleene algebra via Cyclic Proofs
Pratt-Hartmann, Ian	Two-variable First-Order Logic with Counting in Forests
R
Rahli, Vincent	A Verified Theorem Prover Backend Supported by a Monotonic Library
Rebola Pardo, Adrian	A Theory of Satisfiability-Preserving Proofs in SAT Solving
Robillard, Simon	Loop Analysis by Quantification over Iterations
Roy, Subhajit	Knowledge Compilation meets Uniform Sampling Parse Condition: A Symbolic Encoding for LL(1) Parsing
Rudolph, Sebastian	The Triguarded Fragment of First-order Logic
S
Sadigova, Parvin	Lookahead-Based SMT Solving
Scagnetto, Ivan	The Involutions-as-Principal Types/Application-as-Unification Analogy
Schwarz, Sibylle	The Weak Completion Semantics and Equality
Sharma, Shubham	Knowledge Compilation meets Uniform Sampling
Sharygina, Natasha	SMTS: Distributed, Visualized Constraint Solving Function Summarization Modulo Theories Lookahead-Based SMT Solving
Simkus, Mantas	The Triguarded Fragment of First-order Logic
Singal, Dhruv	Parse Condition: A Symbolic Encoding for LL(1) Parsing
Stefanus, Lim Yohanes	The Weak Completion Semantics and Equality
Strejček, Jan	Is Satisfiability of Quantified Bit-Vector Formulas Stable Under Bit-Width Changes?
Su, Tiankai	Rewriting Environment for Arithmetic Circuit Verification
Suda, Martin	A Theory of Satisfiability-Preserving Proofs in SAT Solving Towards Smarter MACE-style Model Finders
Suárez-García, Gorka	Polymorphic success types for Erlang
Svozil, Alexander	Quasipolynomial Set-Based Symbolic Algorithms for Parity Games
T
Tamir, Tami	Alternating Reachability Games with Behavioral and Revenue Objectives
Thiemann, René	A Verified Efficient Implementation of the LLL Basis Reduction Algorithm
V
Van-Der-Hoek, Wiebe	When Are Two Gossips the Same?
Vivekanandan, Paventhan	HoTT-Crypt : A Study in Homotopy Type Theory based on Cryptography
W
Wałęga, Przemysław Andrzej	On Disallowing Punctual Intervals in Reflexive Semantics of Halpern-Shoham Logic
Witkowski, Piotr	Two-variable First-Order Logic with Counting in Forests
Y
Yasin, Atif	Rewriting Environment for Arithmetic Circuit Verification
Yu, Cunxi	Rewriting Environment for Arithmetic Circuit Verification

Disclaimer | Powered by EasyChair Smart Program