LPAR-22: Author Index| Author | Papers |
|---|
| A | | Agarwal, Palak | Parse Condition: Symbolic Encoding of LL(1) Parsing | | Alevizos, Elias | Wayeb: a Tool for Complex Event Forecasting | | Aparicio-Sánchez, Damián | Formal verification of the YubiKey and YubiHSM APIs in Maude-NPA | | Apt, Krzysztof | When Are Two Gossips the Same? | | Areces, Carlos | Reasoning About Prescription and Description Using Prioritized Default Rules | | Artikis, Alexander | Wayeb: a Tool for Complex Event Forecasting | | 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 | | Bauer, Sabine | Decidable Inequalities over Infinite Trees | | Bendík, Jaroslav | Evaluation of Domain Agnostic Approaches for Enumeration of Minimal Unsatisfiable Subsets | | Bickford, Mark | A Verified Theorem Prover Backend Supported by a Monotonic Library | | Biewer, Sebastian | Verification, Testing, and Runtime Monitoring of Automotive Exhaust Emissions | | Blicha, Martin | Function Summarization Modulo Theories | | Boker, Udi | Why These Automata Types? | | Bottesch, Ralph | A Verified Efficient Implementation of the LLL Basis Reduction Algorithm | | Boudane, Abdelhamid | Efficient SAT-Based Encodings of Conditional Cardinality Constraints | | C | | Cassano, Valentin | Reasoning About Prescription and Description Using Prioritized Default Rules | | Castro, Pablo | Reasoning About Prescription and Description Using Prioritized Default Rules | | 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 | | D'Argenio, Pedro R. | Verification, Testing, and Runtime Monitoring of Automotive Exhaust Emissions | | Das, Anupam | Left-Handed Completeness for 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 | Graph Path Orderings | | Dietz, Emmanuelle-Anna | The Weak Completion Semantics and Equality | | Doumane, Amina | Left-Handed Completeness for 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 | | 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 | Decidable Inequalities over Infinite Trees | | Honsell, Furio | The involutions-as-principal types/application-as-unification Analogy | | Hyvärinen, Antti | Function Summarization Modulo Theories
Lookahead-Based SMT Solving
SMTS: Distributed, Visualized Constraint Solving | | Hölldobler, Steffen | The Weak Completion Semantics and Equality | | I | | Iosif, Radu | A Complete Cyclic Proof System for Inductive Entailments in First Order Logic | | J | | Jabbour, Said | Efficient SAT-Based Encodings of Conditional Cardinality Constraints | | Janota, Mikoláš | Towards Smarter MACE-style Model Finders | | Jhunjhunwala, Saket | Parse Condition: Symbolic Encoding of 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? (Experimental Paper) | | Jost, Steffen | Decidable Inequalities over Infinite Trees | | Jouannaud, Jean-Pierre | Graph Path Orderings | | K | | Kovács, Laura | Loop Analysis by Quantification over Iterations | | Kupferman, Orna | Playing with the Maximum-Flow Problem
LTL with Arithmetic and its Applications in Reasoning about Hierarchical Systems
Alternating Reachability Games with Behavioral and Revenue Objectives | | Köhl, Maximilian A. | Verification, Testing, and Runtime Monitoring of Automotive Exhaust Emissions | | 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 | Lookahead-Based SMT Solving
SMTS: Distributed, Visualized Constraint 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 | | Paliouras, Georgios | Wayeb: a Tool for Complex Event Forecasting | | Pous, Damien | Left-Handed Completeness for Kleene algebra, via Cyclic Proofs | | Pratt-Hartmann, Ian | Two-variable First-Order Logic with Counting in Forests | | R | | Raddaoui, Badran | Efficient SAT-Based Encodings of Conditional Cardinality Constraints | | Rahli, Vincent | A Verified Theorem Prover Backend Supported by a Monotonic Library | | Rebola-Pardo, Adrián | 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: Symbolic Encoding of LL(1) Parsing | | Rudolph, Sebastian | The Triguarded Fragment of First-Order Logic | | S | | Sadigova, Parvin | Lookahead-Based SMT Solving | | Sais, Lakhdar | Efficient SAT-Based Encodings of Conditional Cardinality Constraints | | Scagnetto, Ivan | The involutions-as-principal types/application-as-unification Analogy | | Schwarz, Sibylle | The Weak Completion Semantics and Equality | | Serban, Cristina | A Complete Cyclic Proof System for Inductive Entailments in First Order Logic | | Sharma, Shubham | Knowledge Compilation meets Uniform Sampling | | Sharygina, Natasha | Function Summarization Modulo Theories
Lookahead-Based SMT Solving
SMTS: Distributed, Visualized Constraint Solving | | Simkus, Mantas | The Triguarded Fragment of First-Order Logic | | Singal, Dhruv | Parse Condition: Symbolic Encoding of LL(1) Parsing | | Stefanus, L. Yohanes | The Weak Completion Semantics and Equality | | Strejček, Jan | Is Satisfiability of Quantified Bit-Vector Formulas Stable Under Bit-Width Changes? (Experimental Paper) | | Su, Tiankai | Rewriting Environment for Arithmetic Circuit Verification | | Suda, Martin | Towards Smarter MACE-style Model Finders
A Theory of Satisfiability-Preserving Proofs in SAT Solving | | 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? | | W | | 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 |
|
|
