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 veriﬁcation 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 veriﬁcation of the YubiKey and YubiHSM APIs in Maude-NPA |

Exclusive-OR | Formal veriﬁcation 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 veriﬁcation 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 veriﬁcation 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 veriﬁcation 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 veriﬁcation of the YubiKey and YubiHSM APIs in Maude-NPA |

YubiKey | Formal veriﬁcation of the YubiKey and YubiHSM APIs in Maude-NPA |