| A |
| ACTL | Improving SAT-based Bounded Model Checking for Existential CTL through Path Reuse |
| Algorithm Portfolios | SMTS: Distributed, Visualized Constraint Solving |
| amortized analysis | Automatic Space Bound Analysis for Functional Programs with Garbage Collection |
| antichain-based tree automata language inclusion | A Complete Cyclic Proof System for Inductive Entailments in First Order Logic |
| API | Formal verification of the YubiKey and YubiHSM APIs in Maude-NPA |
| Arithmetic Circuits | Rewriting Environment for Arithmetic Circuit Verification |
| automata | Why These Automata Types?
Left-Handed Completeness for Kleene algebra, via Cyclic Proofs |
| automated reasoning | Loop Analysis by Quantification over Iterations |
| axiomatisation | Left-Handed Completeness for Kleene algebra, via Cyclic Proofs |
| B |
| bit-width | Is Satisfiability of Quantified Bit-Vector Formulas Stable Under Bit-Width Changes? (Experimental Paper) |
| Boolean operations | Why These Automata Types? |
| Bounded Model Checking | Function Summarization Modulo Theories
Improving SAT-based Bounded Model Checking for Existential CTL through Path Reuse |
| C |
| cardinality constraints | Efficient SAT-Based Encodings of Conditional Cardinality Constraints |
| CEGAR | Towards Smarter MACE-style Model Finders |
| clause learning | Lookahead-Based SMT Solving |
| cognitive reasoning | The Weak Completion Semantics and Equality |
| complexity | Matching in the Description Logic FL0 with respect to General TBoxes
A Verified Efficient Implementation of the LLL Basis Reduction Algorithm
The Triguarded Fragment of First-Order Logic |
| computer algebra | Rewriting Environment for Arithmetic Circuit Verification |
| Constrained Uniform Sampling | Knowledge Compilation meets Uniform Sampling |
| constraint satisfaction | Decidable Inequalities over Infinite Trees |
| constraint solving | Parse Condition: Symbolic Encoding of LL(1) Parsing |
| convex optimization | Experiments in Verification of Linear Model Predictive Control: Automatic Generation and Formal Verification of an Interior Point Method Algorithm |
| Coq | A Verified Theorem Prover Backend Supported by a Monotonic Library |
| cost semantics | Automatic Space Bound Analysis for Functional Programs with Garbage Collection |
| counterexample | Improving SAT-based Bounded Model Checking for Existential CTL through Path Reuse |
| counterfactual reasoning | The Weak Completion Semantics and Equality |
| Craig interpolation | Function Summarization Modulo Theories |
| Cyclic Graphs | Graph Path Orderings |
| cyclic proofs | Left-Handed Completeness for Kleene algebra, via Cyclic Proofs
A Complete Cyclic Proof System for Inductive Entailments in First Order Logic |
| D |
| d-DNNF | Knowledge Compilation meets Uniform Sampling |
| data streaming | Wayeb: a Tool for Complex Event Forecasting |
| deadlock | Improving SAT-based Bounded Model Checking for Existential CTL through Path Reuse |
| decidability | The Triguarded Fragment of First-Order Logic |
| decision procedures | Two-variable First-Order Logic with Counting in Forests |
| default logic | Reasoning About Prescription and Description Using Prioritized Default Rules |
| deontic logic | Reasoning About Prescription and Description Using Prioritized Default Rules |
| Description Logic | Matching in the Description Logic FL0 with respect to General TBoxes |
| Description Logics | The Triguarded Fragment of First-Order Logic |
| Digital Library | A Verified Theorem Prover Backend Supported by a Monotonic Library |
| Distributed IC3 | SMTS: Distributed, Visualized Constraint Solving |
| Distributed SMT | SMTS: Distributed, Visualized Constraint Solving |
| Divide and Conquer | SMTS: Distributed, Visualized Constraint Solving |
| Domain-agnostic | Evaluation of Domain Agnostic Approaches for Enumeration of Minimal Unsatisfiable Subsets |
| E |
| ECTL | Improving SAT-based Bounded Model Checking for Existential CTL through Path Reuse |
| epistemic logic | When Are Two Gossips the Same? |
| EPR | Towards Smarter MACE-style Model Finders |
| equational reasoning | The Weak Completion Semantics and Equality |
| Erlang | Polymorphic success types for Erlang |
| ethical decision-making | The Weak Completion Semantics and Equality |
| event lists | Formal verification of the YubiKey and YubiHSM APIs in Maude-NPA |
| Exclusive-OR | Formal verification of the YubiKey and YubiHSM APIs in Maude-NPA |
| experimental evaluation | Is Satisfiability of Quantified Bit-Vector Formulas Stable Under Bit-Width Changes? (Experimental Paper) |
| F |
| finite model finder | Towards Smarter MACE-style Model Finders |
| finite satisfiability | Two-variable First-Order Logic with Counting in Forests |
| first-order logic | Loop Analysis by Quantification over Iterations |
| Fluent Calculus | The Weak Completion Semantics and Equality |
| formal languages and automata theory | Wayeb: a Tool for Complex Event Forecasting |
| formal verification | Rewriting Environment for Arithmetic Circuit Verification |
| fragments of first-order logic | The Triguarded Fragment of First-Order Logic |
| Function Summaries | Function Summarization Modulo Theories |
| G |
| game theory | Alternating Reachability Games with Behavioral and Revenue Objectives |
| games | The involutions-as-principal types/application-as-unification Analogy |
| garbage collection | Automatic Space Bound Analysis for Functional Programs with Garbage Collection |
| general satisfiability | Two-variable First-Order Logic with Counting in Forests |
| Geometry of Interaction | The involutions-as-principal types/application-as-unification Analogy |
| gossip protocols | When Are Two Gossips the Same? |
| Graph games | Quasipolynomial Set-Based Symbolic Algorithms for Parity Games |
| graph rewriting | Graph Path Orderings |
| Gödel logics | Lyndon Interpolation holds for the Prenex ⊃ Prenex Fragment of Gödel Logic |
| H |
| Herbrand expansions | Lyndon Interpolation holds for the Prenex ⊃ Prenex Fragment of Gödel Logic |
| hierarchical systems | LTL with Arithmetic and its Applications in Reasoning about Hierarchical Systems |
| I |
| incremental verification | Function Summarization Modulo Theories |
| induction | Left-Handed Completeness for Kleene algebra, via Cyclic Proofs |
| inductive definitions | A Complete Cyclic Proof System for Inductive Entailments in First Order Logic |
| Infeasibility analysis | Evaluation of Domain Agnostic Approaches for Enumeration of Minimal Unsatisfiable Subsets |
| Infinite alphabets | LTL with Arithmetic and its Applications in Reasoning about Hierarchical Systems |
| infinite descent | A Complete Cyclic Proof System for Inductive Entailments in First Order Logic |
| infinite trees | Decidable Inequalities over Infinite Trees |
| inprocessing techniques | A Theory of Satisfiability-Preserving Proofs in SAT Solving |
| Integer Linear Programming | LTL with Arithmetic and its Applications in Reasoning about Hierarchical Systems |
| Interference | A Theory of Satisfiability-Preserving Proofs in SAT Solving |
| interior point method | Experiments in Verification of Linear Model Predictive Control: Automatic Generation and Formal Verification of an Interior Point Method Algorithm |
| interpolation | Lyndon Interpolation holds for the Prenex ⊃ Prenex Fragment of Gödel Logic |
| invariant generation | Loop Analysis by Quantification over Iterations |
| Isabelle/HOL | A Verified Efficient Implementation of the LLL Basis Reduction Algorithm |
| K |
| Kleene algebra | Left-Handed Completeness for Kleene algebra, via Cyclic Proofs |
| knowledge compilation | Knowledge Compilation meets Uniform Sampling |
| knowledge-based protocols | When Are Two Gossips the Same? |
| Kripke semantics | A Verified Theorem Prover Backend Supported by a Monotonic Library |
| L |
| lambda calculus | The involutions-as-principal types/application-as-unification Analogy |
| Lamport clocks | Formal verification of the YubiKey and YubiHSM APIs in Maude-NPA |
| lattice basis reduction | A Verified Efficient Implementation of the LLL Basis Reduction Algorithm |
| linear inequalities | Decidable Inequalities over Infinite Trees |
| LL(1) parsing | Parse Condition: Symbolic Encoding of LL(1) Parsing |
| logic and computational complexity | Two-variable First-Order Logic with Counting in Forests |
| logic programming | The Weak Completion Semantics and Equality |
| Lookahead Heuristic | Lookahead-Based SMT Solving |
| loop | Loop Analysis by Quantification over Iterations |
| LP Solving | Automatic Space Bound Analysis for Functional Programs with Garbage Collection |
| LTL with arithmetic | LTL with Arithmetic and its Applications in Reasoning about Hierarchical Systems |
| Lyndon interpolation | Lyndon Interpolation holds for the Prenex ⊃ Prenex Fragment of Gödel Logic |
| M |
| matching | Matching in the Description Logic FL0 with respect to General TBoxes |
| minimal unsatisfiable subsets | Evaluation of Domain Agnostic Approaches for Enumeration of Minimal Unsatisfiable Subsets |
| modal logic | The Triguarded Fragment of First-Order Logic |
| model checking | Quasipolynomial Set-Based Symbolic Algorithms for Parity Games
LTL with Arithmetic and its Applications in Reasoning about Hierarchical Systems |
| Model Predictive Control | Experiments in Verification of Linear Model Predictive Control: Automatic Generation and Formal Verification of an Interior Point Method Algorithm |
| modelling | Efficient SAT-Based Encodings of Conditional Cardinality Constraints |
| monotonicity | A Verified Theorem Prover Backend Supported by a Monotonic Library |
| Multigraphs | Graph Path Orderings |
| MUS enumeration | Evaluation of Domain Agnostic Approaches for Enumeration of Minimal Unsatisfiable Subsets |
| mutable memory | Formal verification of the YubiKey and YubiHSM APIs in Maude-NPA |
| N |
| Nash equilibrium | Alternating Reachability Games with Behavioral and Revenue Objectives |
| Nonmonotonic Proof Calculus | Reasoning About Prescription and Description Using Prioritized Default Rules |
| Numerical Software Verification | Experiments in Verification of Linear Model Predictive Control: Automatic Generation and Formal Verification of an Interior Point Method Algorithm |
| Nuprl | A Verified Theorem Prover Backend Supported by a Monotonic Library |
| O |
| omega-regular languages | Why These Automata Types? |
| operational semantics | Automatic Space Bound Analysis for Functional Programs with Garbage Collection |
| P |
| parity games | Quasipolynomial Set-Based Symbolic Algorithms for Parity Games |
| path orderings | Graph Path Orderings |
| pattern matching | Wayeb: a Tool for Complex Event Forecasting |
| polymorphism | Polymorphic success types for Erlang |
| program analysis | Experiments in Verification of Linear Model Predictive Control: Automatic Generation and Formal Verification of an Interior Point Method Algorithm |
| program verification | Loop Analysis by Quantification over Iterations |
| progress measure | Quasipolynomial Set-Based Symbolic Algorithms for Parity Games |
| proof checker | A Verified Theorem Prover Backend Supported by a Monotonic Library |
| propositional satisfiability | Efficient SAT-Based Encodings of Conditional Cardinality Constraints |
| protocol verification | Formal verification of the YubiKey and YubiHSM APIs in Maude-NPA |
| pushdown automata | Decidable Inequalities over Infinite Trees |
| Q |
| quantified bit-vectors | Is Satisfiability of Quantified Bit-Vector Formulas Stable Under Bit-Width Changes? (Experimental Paper) |
| R |
| Random walks and Markov chains | Wayeb: a Tool for Complex Event Forecasting |
| Rational synthesis | Alternating Reachability Games with Behavioral and Revenue Objectives |
| reachability games | Alternating Reachability Games with Behavioral and Revenue Objectives |
| read-over-write simplification | Arrays Made Simpler: An Efficient, Scalable and Thorough Preprocessing |
| regular languages | Decidable Inequalities over Infinite Trees
Left-Handed Completeness for Kleene algebra, via Cyclic Proofs |
| Resource Analysis | Decidable Inequalities over Infinite Trees |
| Resource Bound Analysis | Automatic Space Bound Analysis for Functional Programs with Garbage Collection |
| reversible computations | The involutions-as-principal types/application-as-unification Analogy |
| rewrite orderings | Graph Path Orderings |
| S |
| SAT | Towards Smarter MACE-style Model Finders
Improving SAT-based Bounded Model Checking for Existential CTL through Path Reuse |
| SAT solving | A Theory of Satisfiability-Preserving Proofs in SAT Solving
Knowledge Compilation meets Uniform Sampling |
| Satisfiability Modulo Theories | Function Summarization Modulo Theories
Is Satisfiability of Quantified Bit-Vector Formulas Stable Under Bit-Width Changes? (Experimental Paper) |
| Satisfiability Modulo Theory | Experiments in Verification of Linear Model Predictive Control: Automatic Generation and Formal Verification of an Interior Point Method Algorithm
Arrays Made Simpler: An Efficient, Scalable and Thorough Preprocessing |
| Skolemization | Lyndon Interpolation holds for the Prenex ⊃ Prenex Fragment of Gödel Logic |
| SMT encoding | Parse Condition: Symbolic Encoding of LL(1) Parsing |
| SMT solving | Lookahead-Based SMT Solving |
| software verification | Function Summarization Modulo Theories |
| static analysis | Automatic Space Bound Analysis for Functional Programs with Garbage Collection |
| success types | Polymorphic success types for Erlang |
| succinctness | Why These Automata Types? |
| symbolic computation | Quasipolynomial Set-Based Symbolic Algorithms for Parity Games |
| T |
| tableaux system | Reasoning About Prescription and Description Using Prioritized Default Rules |
| termination | Graph Path Orderings
Loop Analysis by Quantification over Iterations |
| The guarded fragment | The Triguarded Fragment of First-Order Logic |
| The two-variable fragment | The Triguarded Fragment of First-Order Logic |
| Theory of Arrays | Arrays Made Simpler: An Efficient, Scalable and Thorough Preprocessing |
| Three-Valued Lukasiewicz Logic | The Weak Completion Semantics and Equality |
| tree automata | Matching in the Description Logic FL0 with respect to General TBoxes |
| two-variable logic with counting quantifiers | Two-variable First-Order Logic with Counting in Forests |
| type inference | Automatic Space Bound Analysis for Functional Programs with Garbage Collection |
| type systems | Automatic Space Bound Analysis for Functional Programs with Garbage Collection |
| types | Polymorphic success types for Erlang |
| U |
| unranked trees/forests | Two-variable First-Order Logic with Counting in Forests |
| Unsatisfiability analysis | Evaluation of Domain Agnostic Approaches for Enumeration of Minimal Unsatisfiable Subsets |
| V |
| Verified theorem prover backend | A Verified Theorem Prover Backend Supported by a Monotonic Library |
| W |
| Weak Completion | The Weak Completion Semantics and Equality |
| web-based GUI | SMTS: Distributed, Visualized Constraint Solving |
| Witness | Improving SAT-based Bounded Model Checking for Existential CTL through Path Reuse |
| word combinatorics | Decidable Inequalities over Infinite Trees |
| Y |
| YubiHSM | Formal verification of the YubiKey and YubiHSM APIs in Maude-NPA |
| YubiKey | Formal verification of the YubiKey and YubiHSM APIs in Maude-NPA |
