LPAR-21: Author Index| Author | Papers |
|---|
| B | | Baaz, Matthias | Gödel logics and the fully boxed fragment of LTL | | Barthe, Gilles | Proving uniformity and independence by self-composition and coupling | | Bauer, Sabine | Decidable linear list constraints | | Benzmüller, Christoph | Theorem Provers For Every Normal Modal Logic | | Biere, Armin | Blocked Clauses in First-Order Logic | | Bistarelli, Stefano | A Quantitative Partial Model-Checking Function and Its Optimisation | | Blahoudek, František | Seminator: A Tool for Semi-Determinization of Omega-Automata | | Bogaerts, Bart | Propagators and Solvers for the Algebra of Modular Systems | | Boumarafi, Yazid | From SAT to Maximum Independent Set: A New Approach to Characterize Tractable Classes | | Bourbouh, Hamza | Automated analysis of Stateflow models | | C | | Ciabattoni, Agata | Bunched Hypersequent Calculi for Distributive Substructural Logics | | Cruz-Filipe, Luís | Formally Proving the Boolean Pythagorean Triples Conjecture | | D | | Duret-Lutz, Alexandre | Seminator: A Tool for Semi-Determinization of Omega-Automata | | E | | Echahed, Rachid | Parallel Graph Rewriting with Overlapping Rules | | Espitau, Thomas | Proving uniformity and independence by self-composition and coupling | | F | | Fedyukovich, Grigory | Synchronizing Constrained Horn Clauses | | Fischer, Jeffrey | Programming by Composing Filters | | Freitas, Fred | RACCOON: A Connection Reasoner for the Description Logic ALC | | Frohn, Florian | Analyzing Runtime Complexity via Innermost Runtime Complexity | | G | | Garion, Christophe | Automated analysis of Stateflow models | | Garoche, Pierre-Loic | Automated analysis of Stateflow models | | Gauthier, Thibault | TacticToe: Learning to Reason with HOL4 Tactics | | Giesl, Jürgen | Analyzing Runtime Complexity via Innermost Runtime Complexity | | Gigante, Nicola | A One-Pass Tree-Shaped Tableau for LTL+Past | | Gleißner, Tobias | Theorem Provers For Every Normal Modal Logic | | Grégoire, Benjamin | Proving uniformity and independence by self-composition and coupling | | Gurfinkel, Arie | Automated analysis of Stateflow models | | H | | Hainry, Emmanuel | Higher order interpretation for higher order complexity | | Hannula, Miika | On the Interaction of Inclusion Dependencies with Independence Atoms | | Hofmann, Martin | Decidable linear list constraints | | Hollingum, Nicholas | Cauliflower: a Solver Generator for Context-Free Language Reachability | | Hsu, Justin | Proving uniformity and independence by self-composition and coupling | | I | | Irving, Geoffrey | Deep Network Guided Proof Search | | J | | Jouannaud, Jean-Pierre | Coq without Type Casts: A Complete Proof of Coq Modulo Theory | | K | | Kahramanogullari, Ozan | Deep Proof Search in MELL | | Kahsai, Temesghen | Automated analysis of Stateflow models
Quantified Heap Invariants for Object-Oriented Programs | | Kaliszyk, Cezary | Deep Network Guided Proof Search
TacticToe: Learning to Reason with HOL4 Tactics | | Kersten, Rody | Quantified Heap Invariants for Object-Oriented Programs | | Kiesl, Benjamin | Blocked Clauses in First-Order Logic | | Klein, Gerwin | Reasoning about Translation Lookaside Buffers | | Klokočka, Mikuláš | Seminator: A Tool for Semi-Determinization of Omega-Automata | | Kontinen, Juha | On the Interaction of Inclusion Dependencies with Independence Atoms | | Kovács, Laura | First-Order Interpolation and Interpolating Proof Systems | | Křetínský, Mojmír | Seminator: A Tool for Semi-Determinization of Omega-Automata | | L | | Lellmann, Bjoern | A uniform framework for substructural logics with modalities | | Lindsberger, Josef | Quantified Boolean Formulas: Call the Plumber! | | Link, Sebastian | On the Interaction of Inclusion Dependencies with Independence Atoms | | Loos, Sarah | Deep Network Guided Proof Search | | M | | Maignan, Aude | Parallel Graph Rewriting with Overlapping Rules | | Majumdar, Rupak | Programming by Composing Filters | | Maringele, Alexander | Quantified Boolean Formulas: Call the Plumber! | | Martinelli, Fabio | A Quantitative Partial Model-Checking Function and Its Optimisation | | Matteucci, Ilaria | A Quantitative Partial Model-Checking Function and Its Optimisation | | Melo Filho, Dimas | RACCOON: A Connection Reasoner for the Description Logic ALC | | Mitchell, David | Propagators and Solvers for the Algebra of Modular Systems | | Montanari, Angelo | A One-Pass Tree-Shaped Tableau for LTL+Past | | Mordvinov, Dmitry | Synchronizing Constrained Horn Clauses | | Moser, Georg | Quantified Boolean Formulas: Call the Plumber! | | O | | Olarte, Carlos | A uniform framework for substructural logics with modalities | | Otten, Jens | RACCOON: A Connection Reasoner for the Description Logic ALC | | P | | Philipp, Tobias | Towards a Semantics of Unsatisfiability Proofs with Inprocessing | | Pimentel, Elaine | A uniform framework for substructural logics with modalities | | Preining, Norbert | Gödel logics and the fully boxed fragment of LTL | | Péchoux, Romain | Higher order interpretation for higher order complexity | | R | | Ramanayake, Revantha | Bunched Hypersequent Calculi for Distributive Substructural Logics | | Rebola-Pardo, Adrián | Towards a Semantics of Unsatisfiability Proofs with Inprocessing | | Reynolds, Mark | A One-Pass Tree-Shaped Tableau for LTL+Past | | Rümmer, Philipp | Quantified Heap Invariants for Object-Oriented Programs | | S | | Sais, Lakhdar | From SAT to Maximum Independent Set: A New Approach to Characterize Tractable Classes | | Salhi, Yakoub | From SAT to Maximum Independent Set: A New Approach to Characterize Tractable Classes | | Santini, Francesco | A Quantitative Partial Model-Checking Function and Its Optimisation | | Schneider-Kamp, Peter | Formally Proving the Boolean Pythagorean Triples Conjecture | | Scholz, Bernhard | Cauliflower: a Solver Generator for Context-Free Language Reachability | | Schäf, Martin | Quantified Heap Invariants for Object-Oriented Programs | | Seidl, Martina | Blocked Clauses in First-Order Logic | | Steen, Alexander | Theorem Provers For Every Normal Modal Logic | | Strejček, Jan | Seminator: A Tool for Semi-Determinization of Omega-Automata | | Strub, Pierre-Yves | Proving uniformity and independence by self-composition and coupling
Coq without Type Casts: A Complete Proof of Coq Modulo Theory | | Suda, Martin | Blocked Clauses in First-Order Logic | | Syeda, Hira | Reasoning about Translation Lookaside Buffers | | Szegedy, Christian | Deep Network Guided Proof Search | | T | | Ternovska, Eugenia | Propagators and Solvers for the Algebra of Modular Systems | | Thirioux, Xavier | Automated analysis of Stateflow models | | Tompits, Hans | Blocked Clauses in First-Order Logic | | U | | Urban, Josef | TacticToe: Learning to Reason with HOL4 Tactics | | V | | Voronkov, Andrei | First-Order Interpolation and Interpolating Proof Systems |
|
|
