FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
GLOBAL KEYWORD INDEX
#
#SAT
#SMT(BV)
#SMT(LA)
$
$\omega$-categorical
(
(Constraint) Logic Programming
(homeomorphically) embedded E-unifiers
2
2-CNF
A
A-infinity-(co)algebras
aa
aaa
abductive reasoning
Abella
Absolute Correctness
Abstract Interpretation
abstract recursion theory
abstract state machine
Abstract State Machines
Abstract syntax
abstract winning condition
Abstraction
Abstraction Refinement
abstraction-refinement
accumulated weight constraints
Ackermann's Lemma
action language
Active Objects
Actor
actors
Actual Cause
ACUI
Ada programming
adaptive
additive monad
adequate numeral system
adjoint logic
adjoint model
Adjunctions
admissibility
admissible rules
affine term
Agda
agent programming
agents
Aggregates
aggregations in logic programming
AI Safety
air traffic surveillance systems
Algebra
algebra in type theory
algebraic confluence
Algebraic crossover operators
algebraic effects
Algebraic evolutionary computation
algebraic extensions
Algebraic Geometry
algebraic proof systems
algebraic structures
algorithm
Algorithm selection
algorithm substitution attacks
algorithmic complexity
algorithms
all maximal clique partitions in a graph
allegories
Alloy
Almost Full relations
Almost-sure winning
alpha-equivalence
Alternating Automata
Alternating time
Alternating-time Temporal Logic
AMBA AHB
anaphora
Android Applications
Android back stack
Android stack systems
Animation
annotation
answer set computation
Answer Set Programming
Anti-unification
Apache Spark
Application
applicative bisimulation distance
applicative first-order logic
applicative simulation distance
applied lambda-calculus
Apprenticeship Learning
approximate circuits
approximate counting
approximate equivalence checking
Approximate inference
approximate partial order reduction
Approximate synthesis
Approximation
Approximation Fixpoint Theory
approximation theorem
architecture
arithmetic circuits
Armstrong relation
Arrays
artificial intelligence
ASMETA
ASN.1
ASP
ASP systems
ASPIDE
Assertions
Associative operad
assumptions refinement
Asynchronous
Asynchronous Games
Atom tracing
atom variables
Atomic flows
Atomic Formula
ATP
Attack Trees
attacker knowledge
Attempto Controlled English
attribute-based access control
Authentication
auto-generated code
autocorrelation
automata
automata learning
Automata over infinite words
Automata Theory
Automata with counters
Automated Algebraic Reasonings
automated complexity analysis
Automated configuration
automated guided vehicle routing
automated reasoning
automated reasonning
automated theorem proving
automated trading systems
Automated verification
automatic algorithm configuration
Automatic Proof checking
Automatic Verification
automation
Automaton State
automotive
Automotive case study
Autonomous
Autonomous automotive
Autonomous Driving
Autonomous system
Autonomous vehicle
autonomous vehicles
avionics systems
Axiom Pinpointing
axiomatization
axioms
B
B combinator
backdoor
backdoors
backtracking
Backus FP
Backward exploration ·
backwards analysis
Bar inductive predicates
Barendregt's Variable Convention
Barrier Certificates
Basis Reduction
BayesianInference
bb
bbb
BDD
Behavioural equivalence
Behavioural metrics
Belenios
Belief Function Theory
belief merging
benchmark
Benchmarking
beta reduction
Beth models
Betweenness Centrality
Bi-directional Grammars
bi-intuitionistic logic
bicategories
Bidding games
Biform theories
Bimonad
binarized neural network
Binary Analysis
Binary Encoding
binary search tree
binder mobility
Binders
Binding operations
Bioinformatics
bisimulation
Bit-vectors
Bitvectors
black-box optimization
Blockchain
blocked clauses
boolean algebra
Boolean Functional synthesis
Boolean games
Boolean polynomials
Boolean satisfiability
Boolean-valued models
Boot code
bottom-up
Bounded
bounded arithmetic
Bounded expansion
bounded model checking
bounded model-checking
bounded synthesis
bounds on leakage
Braidings
branching programs
broadcast communication
Brzozowski derivatives
Buchberger algorithm
Buchi Automaton
Bug Finding
bug finding tool
Böhm trees
Büchi Automaton
C
C code
C Programming Language
cache coherence protocols
Cached Address Translation
calculational method
Calculational proof
calculus of structures
call by push value
call by value
call-by-name
call-by-need evaluation
call-by-push value
call-by-value
CAMUS
car assembly operations
Cardinality Constraint
cardinality encodings
Cartesian cubes
Cartesian Genetic Programming
Cartesian Monoids
case study
Catalan numbers
categorial grammar
Categorical Logic
Categorical model
Categorical models
Categorical Quantum Mechanics
Categorical semantics
categories with families
Categorification
category theory
Causal Dependency
causality preservation
Cautious Reasoning
cc
ccc
ccg
CCSL
CDCL
cdcl-cuttingplanes
Cedille
CEGIS
Cellular automata
cellular cohomology
Centrality
certificate checking
certificates
certification
certified code
Certified execution engine
certified software
channel composition
chat bot
chemical computation
Chemical reaction networks
Chinese monoids
Choice Logic
Choice sequences
choiceless polynomial time
Chronological Backtracking
Church's type theory
Church-Turing thesis
circuit
Circuit complexity
circuit lower bounds
circuit satisfiability
circular proofs
classical arithmetic
classical B
classical higher-order logic
classical linear logic
classical logic
classical realizability
Classical sequent calculus
Clause Learning
CLF
clocks
cluster algebra
CNF
CNF configuration
Co-Simulation
Coalgebra Modality
Coarse computability
Coarse-grained modeling
CoCoA and MathSAT
codatatypes
code generation
Code Generators
code review
code-generation
coends
Cognitive Modeling
cographs
coherence
coherence theorems
coherent presentations
coinduction
coinduction up-to
Coinductive Invariants
coinductive types
Combination
Combinatorial benchmarks
combinatorial proofs
combinatorial search algorithms
combinatoric
combinatorics
combinators
combinatory logic
common knowledge
Common Language for Geometric Problems
Commonsense Reasoning
Comonads
Comparator
comparator network
comparison systems
CompCert
Competition
compiler
Compilers
complementary approximate reachability
Complementation
complete abstract domains
complete lattices
Complete Segal Spaces
completeness
completion
Complexity
Complexity Analysis
complexity classes
complexity dichotomy
Complexity measures
Complexity Proving
complexity results
Complexity Theory
composition
compositional analysis of software systems
compositional model checking
compositional reasoning
Compositional verification
compositionality
Computability
computation and deduction
Computation Complexity
Computation Tree Logic
computational complexity
Computational Hardness
computational model
Computational modeling
computational monads
Computational Reductions
computational soundness
Computational thinking
computational type theory
computer aided security proofs
Computer Algebra
computer-aided cryptography
concurrency
concurrency and distributed computation
Concurrency Testing
Concurrent datatypes
Concurrent games
Concurrent objects
Concurrent operation specification
Concurrent Process Calculi
concurrent program algebra
Concurrent Separation Logic
Concurrent strategies
Condition Synchronization
Conditional Independence
conditional rewriting
conditional term rewriting
conditional value at risk
Confidentiality
Conflict-Driven Clause Learning
Conflict-driven search
confluence
Confluence Analysis
Confluence and Standardization
confluence competition
Confluence modulo
confluence tool
Confusion
Connection-based proof-search
cons-free computation
Conservative approximation
Conservativity
consistency
Consistency Analysis
Consistency Checking
Consistency proofs
constant-time security
Constrained Horn Clauses
Constrained Optimization
constrained rewriting
Constraint Handling Rules
Constraint Handling Rules (CHR)
Constraint Language
Constraint Logic Programming
Constraint Logic Programming on Finite Domains
Constraint Modelling
constraint problem
Constraint programming
constraint satisfaction
Constraint Satisfaction Problem
constraint satisfaction problems
Constraint satisfaction processing
Constraint Solving
Constraint Systems
Constraint-based synthesis
Constraint-based verification
constraints
constraints solver
Constructive Decidability
constructive mathematics
Constructive Type Theory
constructivism
contact logics
context-free
Context-free Grammars
contextual equivalence
contextual fibrancy
contextuality
Continuous computation
Continuous delivery
continuous systems
continuous validation
Continuous-time Markov chain
contract-based verification
contractibility
Contraction
control
control improvisation
Control parameters
Control Theory
Control-Flow Refinment
Controlled Natural Language
Controlled Natural Languages
controller synthesis
conversion algorithm
convex polyhedra
Cooperative Scheduling
Coq
Coq library
Coq proof assistant
Core SAT
Corecursion
correctness
Correctness by extraction
correctness criteria
Correctness Enhancement
Correctness proof
Correspondence theory
Cost Analysis
Cost bounded reachability
Cost relations
counter-example
Counterexample-guided Algorithms
Counterexample-Guided Inductive Synthesis
counterexamples
counting classes
Courcelle's Theorem
Covering Theory
CPS translation
CR-Prolog
CR-Prolog2
Crafted benchmarks
Craig Interpolation
critical complexity region
critical pair
critical software assurance
Critical Systems
CRN
CRN equivalence
cross-fertilization
cross-section property
crowds
cryptographic CNF instances
cryptographic constant-time
Cryptographic protocol
Cryptographic protocols
cryptographic schemes
Cryptographic software
Cryptography
CSP
CSP Solver
cubical sets
cubical type theory
Curry-Howard
Curry-Howard correspondence
Curry-Howard isomorphism
cut elimination
Cut-elimination
Cutting and Packing
Cutting planes
Cyber Security
Cyber-Physical system
cyber-physical systems
Cycle finding
Cyclic graphs
cyclic induction
cyclic lambda calculus
cyclic proof
Cyclic proofs
cyclic sharing
Cyclic term-graps
cylindrical algebraic decomposition
D
D-optimaldesigns
data compression
Data Driven modelling
Data Races
data words
Data-structures
database theory
Databases
Datalog
datatypes
Deadlock
Deadlock Analysis
Deadlock Detection
deadlock-freedom
Decentralized planning
Decidability
decision
Decision making
Decision Model and Notation (DMN)
Decision Modeling
Decision Modelling
decision procedure
Decision Procedures
decisiveness
Declarative Algorithms
declarative knowledge representation
declarative programming
Declarative Prover
declassification
decoupled approach
decreasing diagrams
deduction
Deductive interactive program verification
Deductive program verification
Deductive programs verification
deductive verification
Dedukti
Deduplication
deep embedding
deep inference
Deficiency
definability
definable while programs
delay differential equations
Delta-completeness
denotation
denotational model
denotational semantics
deontic logis
Dependant Types
dependence maps
Dependency
dependent choice
dependent product types
Dependent Refinement Types
dependent temporal effects
dependent type theory
dependent types
dependently typed programming
derivational complexity
Deriving Reliable Programs
Description Logic
description logics
descriptive complexity
design automation
Design by contract
Design Space Exploration
determinacy
Deterministic Automata
Deterministic Parity Automaton
DFA
Diagrammatic Reasoning
dialectica category
Dialectica interpretation
diamond lemma
differential dynamic logic
differential equation axiomatization
Differential Equations
differential game logic
differential ghosts
Differential Linear Logic
Digital libraries
Diller-Nahm variant
Diophantine equations
direct-manipulation interaction
Discounted-sum determinization
Discounted-sum inclusion
discrete polymorphism
Discrete-Event
discrete-time linear system
display map category
distance bounding protocols
Distance fraud
Distance-bounding protocols
distribute consensus protocols
distributed autonomous systems
distributed computing
distributed concurrent systems
Distributed Protocols
distributed systems
Distribution based objectives
DLVSYSTEM srl
DMN
DNA algorithmic self-assembly
Dolev-Yao Attacker
domain specific languages
domain-level strand displacement
domain-specific formal languages
Domain-specific languages
dominance
Double Description method
Double negation
Double-pushout graph transformation
Double-pushout rewriting
downward closures
DPRM Theorem
drat
DRAT proofs
Drawing trees
DSL
dual-rail encoding
duality
dualized proof system
Dynamic analysis
Dynamic applications
Dynamic data structures
Dynamic domains
dynamic epistemic logic
Dynamic language
Dynamic Languages
dynamic logic
Dynamic nets
Dynamic Partial Order Reduction
Dynamic Programming
Dynamic Verification
Dynamical Systems
E
e-voting
EasyCrypt
Eckmann-Hilton morphism
Economic Reasoning
Economics
effectful bisimilarity
Efficiency
efficient computation
Egraph
Eilenberg-Moore Category
elaboration
Eldarica
Electronic Voting
elementary linear logic
elementary semantics
ellipsoid method
Embedded systems
Empirical evaluation
EMVCo
energy games
energy-efficient computing
engineering mathematics
enriched category theory
entailment check
Entitity Resolution
epistemic logic
Epistemic Logic Programs
epistemic specification
Epistemic Specifications
equality by abstraction over an interval
equational constraints
equational logic
equational rewriting
equational theories
equational theory
Equilibrium Logic
Equivalence
equivalence relations
erasure
Erlang
essential unification
Ethereum
Evaluable Functions
Evaluation
Event Calculus
Event structures
evidential verification
Evolution systems
exchange
exchange rule
Executable Specifications
execution time
exhaustive and randomized data generation
existential rules
expander graphs
expansion proofs
expected shortfall
Expected Utility
experimental analysis
experiments
Expert Systems
explainable decision set
explanation
explanatory analysis
explicit induction reasoning
explicit substitution
Exposed Datapath Architectures
expressiveness
extended resolution
Extension
extensive category
extraction
F
factorization
fairness
Fairness objectives
Fault tolerance
feasibility of functionals
feature tree constraints
fermionic quantum computing
fibrancy of the function type
fibrant replacement
field theory
Filter
filter models
Finite Automaton
Finite model generator
finite model property
finite model theory
finite multisets
Finite Semantics
finite sum types
finitization
Firmware
first order logic
First order transduction
first-order combinatorial proofs
First-order list function
first-order logic
first-order logic with inductive definitions
first-order logic with inductive predicates
First-order multiplicative linear logic
First-Order Syntactic Unification
First-order Theory
first-order theory of rewriting
First-order types
Fix-points
fixed parameter complexity
fixed parameter tractable
Fixed Point Arithmetic
fixed point equations
fixed points
fixed-point logic
Fixpoint Algorithms
fixpoint alternation
fixpoint logic
flattener
Floating Point Arithmetic
floating-point analysis
floating-point optimization
floating-point round-off errors
flocking
Flow Analysis
flows and nowhere-zero flows
Fly-Automata
FMI
Focused Proof Systems
focused sequent calculus
focused sequent calculus for first-order modal logic
focusing
Focussing
FOIL algorithm
FOL
Forest Algebra
Forest Algebras
Formal Analysis
formal aspects of program analysis
Formal Definition
formal languages and automata theory
Formal Library
Formal Metatheory
Formal Methods
formal methods for security
formal methods in practice
Formal Model
formal proof
formal proofs
Formal Semantics
formal specification
formal topology
formal verification
formal verification at runtime
Formalisation
formalization
FormalVerification
Frama-C
Free choice sequences
free modules
free monad
Free Variable
Frege systems
Freyd categories
Frobenius algebra
FSM
full abstraction
Function algebras
Function classes
function package
function summaries
Functional Analysis
functional and relational specifications
functional dependency
functional interpretation
Functional Mock-up Interface
functional programming
functor
fuzz
fuzzer
fuzzy generalization
Fuzzy logic
G
g-leakage
Game semantics
Game Theory
Games
games and logic
games played on finite graphs
Gandy
Gappa
garbled circuit
generalised species
Generalization of syntactic parse trees
generalized reactivity
Generic Binding Structures
generic proof assistant
Genetic algorithms
Geometric Automated Theorem Provers
geometric logic
geometric realization
Geometry
geometry of interaction
Gillespie algorithm
Girard's translations
global states
gluing
GNATProve
goal-directed evaluation
gradual typing
Grammar testing
Grammatical Framework
graph
graph algorithms
Graph Analysis
Graph Drawing
graph encoding
Graph Generation
graph grammars
graph isomorphism
graph minor theorem
Graph Queries
Graph Recognition
Graph Representation
graph rewriting
graph rewriting systems
graph theory
Graph transformation
Graph Views
graph-based characterization
Graphical reasoning
Gray categories
Gray category
greatest fixed point
Greedy Heuristics
Groebner bases
Grothendieck fibrations
ground systems
ground theories
Grounding
Group decision
Groupoid
Gröbner Basis
Guard Condition
Guarded Recursion
Guillotine Constraint
H
Hadamard matrices
halting problem
hammers
Handlers
handwriting
Handwritten Digit Recognition
handwritten mathematics
hardness of approximation
Hardware model
hardware verification
hardware-in-the-loop
Hardware/software interfaces
hash functions
Hashing-based Algorithm
HCI
head variable
Herbrand's theorem
hereditarily definable sets
heuristic search
heuristics
Hierarchical information
Hierarchical state machines
Hierarchy Theorem
higher categories
Higher dimensional linear rewriting
higher groups
higher inductive type
higher inductive types
Higher order recursion schemes
Higher-order abstract syntax (HOAS)
higher-order computability
higher-order logic
higher-order logic programming
higher-order modal logic
higher-order operads
higher-order programs
higher-order reasoning
higher-order recursion schemes
Higher-Order Rewriting
higher-order term rewriting
higher-order unification
Higher-Ranked Polymorphism
Highly Assured Software
Hilbert's tenth problem
HKDF
HMAC
HOL
HOL Light
homogeneous
homogeneous linear diophantine equations
homogeneous types
Homological algebra
Homomorphism
Homotopical algebra
Homotopy
homotopy type theory
Hopf Monad
Horn clause
Horn Clause Transformation
Horn clauses
Horn propositional satisfiability algorithm
howe's method
Human-Robot Interactions
Human-Robotic Interaction
HW-SW interface
hybrid logic
Hybrid System
hybrid system simulators
hybrid systems
hydraulic oil pump
Hyper sequents
hypercube optimization
Hyperintensional Logic
Hyperproperties
Hyperproperty Verification
hypersequents
I
ic3
IDE
Idempontent
Idempotent quasigroups
Identity type
ILP
immunization
imperative
imperative calculi
Imperative languages
imperative programming
imperative programs
Imperfect information
Implementation and benchmarks for parity games
implicate generation
implicative algebras
implicit complexity
Implicit Hitting Set
Importance Splitting
impredicative encodings
impredicativity
inconsistency measures
inconsistency-tolerant reasoning
Inconsistent Requirements Explanation
increasing chains
Incremental
Incremental Analysis
Incremental Maintenance
Incremental SAT
Indexed types
Indistinguishability
induction
induction principle
induction reasoning
induction rules
inductive datatypes
Inductive Definitions
Inductive invariants
Inductive Logic Programming
Inductive predicates
inductive theorem prover
Inductive Theorem Proving
inductive types
inductive validity cores
inductive-inductive types
Industrial application
industrial case
inference
inference attacks
infinitary and cyclic systems
Infinitary Proofs
infinitary rewriting
Infinite computation
infinite descent
infinite duration
infinite-state systems
Infinity-Categories
Infinity-Presheaves
information flow
information flow analysis
Information flow control
inner-approximations
innermost conditional narrowing
instantiation
Integer Arithmetic
Integer Transition Systems
integer weights
Integrated Development Environment
integrated verification
integration
integrity
Intension
Intensional Logic
Intensional Sets
Intensional Type Theory
intentions
interaction graphs
Interaction nets
Interactive system
interactive theorem prover
interactive theorem proving
interactive tool
Interface design
Interlocking
Intermediate Language for Verification
internal and external calculi
internal language
internal parametricity
Internet of Things
Interoperability
Interpolation
interprocedural analysis
Intersection Type Systems
intersection types
intersections
interval arithmetics
interval propagation
Intrinsic noise
intruder deduction problem
intuitionistic combinatorial proofs
Intuitionistic linear logic
Intuitionistic logic
Intuitionistic logic of constant domains
Intuitionistic mathematics
Intuitionistic modal logic
Invariant Generation
Invariants
Inverse Reinforcement Learning
IRM-calc
irrelevance
Isabelle
Isabelle Proof Assistant
Isabelle/HOL
Isabelle/HOL Theorem Proving
Isabelle/jEdit
IsaSAT
Isomorphism type
isotopy
Iterated Boolean games
J
JASP
Java
JDLV
jEdit
Jordan Normal Form
Judgemental Interpretation
Jupyter
K
k-safety verification
Kachinuki order
Kakutani's fixed point theorem
KeY
key set
kleptography
Knapsack
knot theory
Knowledge Acquisition
knowledge base paradigm
Knowledge based Reasoning
knowledge compilation
Knowledge Representation
Knowledge Representation and Reasoning
knowledge-based noninterference
Knuth-Bendix criterion
Koat
L
labelled Markov chain
Labelled proof-systems
labelled sequent calculi
Labelled sequents
labelled systems
lambda calculi
lambda calculus
lambda calculus and combinatory logic
lambda prolog
lambda-calculus
lambda-encodings
lambda-free higher-order logic
lambda-prolog
lambda-tree syntax
Lambek calculus
lams
language based security
Language inclusion
large libraries
Large set
large theories
large-scale reasoning
lattice
Lattice Basis Reduction
lattice traversal
Layout algorithm
laziness
lazy
lazy evaluation
lazy grounding
lazy self-composition
Lean proof assistant
learning
Least general generalization
Leo-III
Leveled sequents
Likelihood weighting
Linear Arithmetic
Linear categories
Linear Category
linear clauses
linear cliquewidth
Linear Constraints
linear distributivity
linear logic
Linear polygraphs
Linear Programming
Linear Temporal Logic
linear term
linear time hierarchy
Linear Transformations
Linear Tree Constraints
linear/non-linear logic
Linearity
linearizability
Linearization
Lists
Literate programming
Liveness Analysis
LLVM
Local determinism
locale theory
Log analysis
logarithmic space computation
logic
logic for PTime
Logic for Teaching
Logic Meta-Programming
Logic of Here and There
Logic on Trees
logic programming
Logic Programming Applications
Logic Solvers
Logic Tools
Logic-based tools
Logical complexity
logical design
logical formalism
logical framework
Logical Frameworks
Logical models
logical paradoxes
logical predicates
Logical Regulatory Networks
Logical relations
logically constrained term rewriting systems
Logics for strategic reasoning
Logistics
LOGSPACE
LOIS
long-distance resolution
loop unrolling
Lower bound techniques
Lower Bounds
LPMLN
LPOD
LTLf
lucas interpretation
Lukasiewicz Logics
M
MAC
machine checked proofs
Machine Learning
Machine Learning Systems
machine words
magic states
Magic wand
Maple
MapReduce
MARCO
Markov Decision Process
Markov decision processes
Markov processes
Martin-L\"{o}f type theory
Martin-Löf type theory
Mason's Marks
Master Theorem
mathematical analysis
Mathematical language
mathematical proof
Mathematics
Matita
Matrix Growth
Matrix Interpretation
Matrix semigroups
Maude
Maximum Satisfiability
MaxSAT
MAXSAT application
MaxSAT resolution
MaxSAT solving
maxSMT
MC-SAT
MCMT
Mean-payoff games
meaningless terms
mechanical reasoning
mechanised theorem proving
mechanized mathematics
mechanized meta-theory
Mechanized proofs
mechanized reasoning
Memoization
Memory
Memory Errors
memory isolation
memory model
message passing concurrency
Message Passing Interface
meta programming
meta-data library
Meta-Interpretive Learning
meta-programming
Meta-theory
Metamorphic Testing
Metareasoning
metatheory
Minimal models
Minimal unsatisfiability
Minimally strongly connected digraph
Minimisation
MIPS TLB
Mixed Arithmetic
Mixed Distributive Law
Mixed Integer Linear Programming
ML
MMSNP
Mobile robotics
modal fixpoint logic
modal logic
Modal logics
modal mu
modal mu calculus
Modal Type Theory
modalities
Model Animation
model checking
Model Checking Games
model construction
Model Counting
Model Expansion
model finding
model generation
Model learning
Model quality
Model Revision
model sampling
Model Theory
Model transformations
model-based engineering
Model-Based risk Analysis
model-based testing
model-checking
Model-checking first-order logic
model-checking problems
Model-level uncertainty
Modeling
Modeling and Specification
Modelling Languages
modelling secure protocols
models
Models of computation
Modular Analysis
modular approach
Modular Arithmetic
Modular System
Modular Tensor Category
modules
Molecular computing
Molecular Filters
Molecular programming
Monad
Monadic Second Order Logic
Monads
monitoring
monoidal categories
Monoidal Coalgebra Modality
monotone
Monotone complexity
Monotone proofs
monotonicity
Montague semantics
Montgomery Multiplication
MPI
MSO
MSO on Infinite Words
MSO on omega-Words
MSO transduction
mu-calculus
Multi Factor
Multi-agent systems
Multi-agent workflows
Multi-clock timed automata
Multi-graphs
multi-modelling
multi-objective optimization
Multi-objective synthesis
Multi-party computation
Multi-Pass Dynamic Programming
Multi-player games
Multi-Robot planning
Multi-valued Logic
multicategories
multiplayer games
multiplicative linear logic
Multiplier Verification
multitope
muMALL
N
N player games
nanoCoP
Nanofabricated Devices
narrowing
Nash equilibria
Nash equilibrium
Natural deduction
Natural language
natural language processing
natural language understanding
Natural mathematical language
natural proofs
Natural-style Proofs
Negation as failure
Negation in Logic Programming
Negative translations
neighbourhood singleton arc consistency
Nelson-Oppen
nested sequents
nested systems
Network Based Biocomputation
Network Intrusion Detection
Network-free simulation
networks of synchronized automata
neural network
neural networks
Newman's lemma
next state relation
Noise Reduction
nominal rewriting
nominal terms
nominal unification
nominalizations
non-clausal theorem proving
non-cnf
non-commutative
non-denoting terms
Non-Deterministic Automata
non-idempotency
non-idempotent intersection types
Non-interference
Non-interleaving semantics
Non-lawlike computability
non-linear arithmetic
Non-linear Real Arithmetic
Non-monotonic Reasoning
non-rigid terms
Non-Termination Bugs
Non-termination Proving
non-wellfounded proofs
non-zero sum games
nondeterminism
nonlinear integer arithmetic
NonMonotonic Semantics
nonmonotonic term orders
nonnegativity certificate
Normal Form
normal form bisimulation
normal forms
normalisation
Normalization
norms
Notation
Notebooks
novel applications domains
Nowhere dense graphs
Numerical Program Analysis
Nuprl
Nuprl proof assistant
nuxmv
O
o-minimality
OBDD
Object Constraint Language (OCL)
object-oriented
Object-oriented programs
observational equivalence
OCaml library
Ocra
odd-even network
omega-languages
Omega-regular languages
omega-regular objectives
OMT
Online Decomposition
Online Social Networks
ontologies
Ontology
Ontology Languages
Ontology Reasoning
open games
Open-WBO
OpenFlow
OpenJDK
OpenTheory
Operad
Operating System Verification
operational semantics
Operational Termination
opetope
Optical Networks on Chip
optimal propagation
Optimal Scheduling
Optimal Upper Bound
Optimisation
optimization
Optimization heuristics
Optimization Modulo Bit-Vectors
optimization techniques
optimizations
OR causality
oracle Turing machines
order invariant definability
order theory
ordered completion
ordered objectives
ordered structures
ordering
ordinal diagram system
Ordinary differential equation
ordinary differential equations
Origin
over-approximation
Overture
P
Paracoherent Answer Sets
Parallel computation
parallel improvements
Parallel Processing
parallelism
parameter optimization
parameter-free axioms
parameterised Boolean equation systems
Parameterised verification problem
parameterized AC^0
Parameterized Algorithms
parameterized complexity
Parameterized Model Checking
parameterized systems
parameterized verification
Parametricity
parametrized systems
Parity Game
parity games
parsing
Partial algorithms in Coq
partial correctness
Partial Evaluation
Partial Functions
Partial models
partial order reduction
Partial-order reduction
path orderings
pattern matching
paycheck pronouns
PB constraints
PDL
PDR
PDR-Z3
Peano arithmetic
Perfect masking
perfect samplers
permission inference
permission model
Permissions
Permutation problems
permutations
Persistent places
Petri nets
Phylostatic
Phylotastic
pi calculus
pi-caclulus
pi-calculus
Picat
Planning
Planning under uncertainty
PMCFG
pointer arithmetic
pointfree topology
polarity
Policing function
policy language
Policy Synthesis
polycategories
polygraph
polygraphs
Polyhedra Domain Analysis
Polymers
polymorphism
Polynomial Calculus
Polynomial Factorization
polynomial functor
Polynomial functors
Polynomial hierarchy
polynomial simulation
polynomial upper bounds
polynomial-time tractability
polytyptic programming
population protocols
port graphs
Portfolio
Portfolio Solver
Positive complexity
Post Correspondence Problem
power-law
precision medicine
precondition inference
predecessor function
predicate
Predicate Abstraction
preference
Preference Logic
Preference Modeling
Preferential Logics
prefix-constrained term rewriting
premature convergence
preprocessing
presheaf models
presheaf semantics
Presheaves
presupposition
pretty printing
primary key
Prime Numbers
priorities
Privacy
Privacy-type properties
proactive security
probabilistic
Probabilistic Algorithm
probabilistic bisimilarity
probabilistic bisimilarity distance
Probabilistic Boolean Program
Probabilistic computation
probabilistic CTL
probabilistic finite automata
probabilistic games
Probabilistic graphical models
Probabilistic Inductive Logic Programming
probabilistic lambda-calculus
Probabilistic Logic
Probabilistic logic programming
Probabilistic model checking
Probabilistic planning
Probabilistic programs
probabilistic reasoning
Probabilistic rewriting
Probabilistic Satisfiability
Probabilistic State Space Exploration
probabilistic systems
Probabilistic Timed Automata
probabilistic verification
probability
problem database
problem encodings and reformulations
problem fingerprinting
procedural interpretation
process calculi
process calculus
product types
profunctor
Program Analysis
Program Derivation
Program extraction
Program invariant
Program Projection
program refinement
program specialisation
Program Synthesis
program transformation
program transformations
Program translation
Program Verification
programming language semantics
programming languages
programming logic
programming paradigm
Programming-by-Example
progress measure
Projected Model Counting
Projective plane
Prolog
Prompt LTL
Proof
proof assistant
proof assistants
proof automation
proof by reflection
proof checker
Proof checking
proof complexity
proof compression
proof engineering
proof guidance
proof identity
Proof Method Recommendation
Proof Mining
Proof nets
proof of univalence
proof schema
proof search
proof semantics
Proof System
proof systems
proof terms
Proof theory
proof theory of modal logic
proof-as-program
Proof-checker
proof-relevant
Proof-relevant logic
proof-search
proof-theoretic semantics
proof-theoretical linear semantics
proofs
Proofs by reflection
proofs-as-programs
property directed reachability
property falsification
Property Specification Patterns
property-based testing
Propositional Dynamic Logic
propositional implicational intuitionistic logic
propositional logic
propositional model counting
Propositional Resizing
PROPs
Protocol Verification
protokernel
prototyping
prover
Prover IDE
Prover Trident
proximity relation
Pseudo-Boolean
Pseudo-Boolean Optimisation
Pseudo-Boolean Solving
PSPACE
Pushdown systems with transductions
PVS
python
Q
Q-Resolution
QBF
QBF calculi
QDimacs
QRAT
Qualitative Reasoning
qualitative spatial reasoning
qualitattive spatial reasoning
quantale relator
quantification
Quantified Bit-Vectors
quantified boolean formula
Quantified Boolean Formulas
Quantified Circuit
quantified modal logic
quantified modal logics
quantified resolution asymmetric tautology
Quantifier
quantifier elimination
quantifier instantiation
quantifier rank
Quantifier-free Theory of Arrays
quantifiers
quantitative algebraic reasoning
Quantitative Analysis
quantitative information flow
Quantitative Model Checking
Quantitative Objective
Quantitative Semantics for Temporal Logic
quantum computation
Quantum Computing
Quantum functional languages
quantum program
Quantum Programming
Quasi-inverse
queries
query
Query Answering
Query Enumeration
Query Optimization
Question Answering
Quicksort
Quotation and evaluation
quotient inductive types
quotients
R
Railway
railway interlocking systems
RAISE
Ramsey theory
Random Algorithms
random generation
random parity equations
random sample voting
random SAT
random variables
randomised
Randomization
randomized algorithm
Randomized algorithms
RankFinder
ranking functions
Rare Event Simulation
Rating of Geometric Provers
Rational closure
Rational synthesis
rationality
RBAC
Re-composition
reach-avoid specification
reachability
reachability analysis
Reachability analysis of nonlinear systems
reachability logic
Reachability problem
Reachable set over-approximation
reactive programs
reactive synthesis
read-once branching programs
real algebraic geometry
Real Analysis
Real Arithetmic
Real Cohesive Homotopy Type Theory
Real Numbers
real roots
real-time
real-time logic TCTL
Real-world applications
realisability
Realizability
Reasoning about Actions and Change
Reasoning about syntax
recognizability
record types
Recursion
recursion-free constrained Horn clause
Recursion-theoretic characterisations
Recursive functions
Recursive types
recursively enumerable
Reduction
Reduction orderings
Reduction semantics
reduction to SAT
Reductive cut elimination
Redundancy-free Proof-Search
refactoring
refinement
refinement logic
Reflection
Reformulation
register machines
Regression Tree
Regular Datalog
regular expressions
regular languages
regular tree grammar
regularity preservation
reification
Reinforcement Learning
relational databases
relational model
relational reasoning
relational semantics
relational theory
Relational Verification
Relative Correctness
relative entropy programming
relative soundness results
Relevance Logic
Reliable
rely-guarantee
rely/guarantee concurrency
remote build
replaceability
Requirement Analysis
requirements analysis
requirements based testing
Requirements Engineering
Requirements specification
Resolution
Resolution Calculi
resource calculus
Resource Usage Analysis
Resource-aware
Restart
restricted chase
Reverse mathematics
Reversibility
Rewrite Rules
Rewrite system
Rewrite Systems
rewriting
ribbon categories
Rice's theorem
rich logic
Richard Montague
Richman games
Riesz modal logic
right lifting property
Ring Theory
Robotic
robotic planning
robust declassification
robustness
Robustness guided falsification
Role-Based Access Control
Role-Based Access Control (RBAC)
roundoff error
Rule-base modeling
rule-based language
Rule-based modelling
Rule-Based Programming
Rule-Based Systems
rules
rules of the road
Run-time Checks
Runtime complexity
runtime verification
S
S5
safe schemes
safety
safety critical
Safety properties
safety verification
SAT
SAT and BDD-based decision procedures
SAT encoding
SAT modulo theories
SAT problem
SAT Solver
SAT solvers
SAT solving
SAT-based Optimization
Sat4j
Satisfiability
Satisfiability Checking
Satisfiability Modulo Constraint Handling Rules
Satisfiability Modulo Theories
Satisfiability Modulo Theory
satisfiability threshold
Satisfiablity Modulo Theories
SATsolvers
Scaling
Scheduling
Scoped channels
Scrambling
search
Search space pruning
Second Order Logic
second order quantifiers
second-order quantification
secure channels
Secure compilation
Secure multiparty computation
securitisation
Security
security definitions
Security Management
Security Policy
security protocols
security verification
selection network
self-composition
Self-Driving vehicle
semantic forgetting
Semantic model
semantic parsing
semantics
semantics of programming languages
Semantics preservation
semidefinite programming
semisimplicial type
sensibility
sensitivity analysis
Sentence Planning
separability
separation
separation logic
Separations
sequent calculus
Sequential algorithms
sequential types
session types
Set Membership
Set Theory
sets with atoms
shapes for higher-dimensional structure
shared-variable concurrent programs
sharing
sharpness
shuffling calculus
side conditions
Side-channel attack
side-channels
Sign-off
simple proof assistant
simple types
Simplicial sets
Simplicial Type Theory
Simply typed lambda calculus
simply typed lambda terms
simulation
Simulation of Turing Machines
Simulink
Simulink-based development
singleton arc consistency
Singular DP-reduction
Size
Skeptical Approach
Skolem functions
skolemization
SLD-resolution
Smart Buildings
Smart Contract Verification
Smart contracts
smart grid
SMT
SMT Solver
SMT solvers
SMT Solving
SMT-based model checking
SMT-solving
SMTLIB
Soft constraints
Software as a Service
software design
software development
Software Engineering
software formal verification
Software model checking
software model-checking
Software Product Lines
Software Testing
Software Tools
software verification
Software-Defined Networking
software-defined networks
solving equations
sound up-to techniques
Soundness
Space
SPARK2014 and Critical Ada Software
Spatial Reasoning
Species of Structures
specification
Specification Language
Specification-based monitoring
Splitting
SQL
Ssreflect
Stability
stable model
stable model semantics
Stack-Based Access Control
star-autonomous categories
State Complexity
state injection
State machine
State monad
state space minimisation
State-space abstraction
stateful protocols
Static Analysis
static analyzers
static dependency pairs
static equivalence problem
Static Profiling
Static program analysis
static semantics
Statistical Model Checking
Statistical relational learning
stepwise development
stereotypical activities
Stochastic Chemical Reaction Networks
Stochastic dynamical systems and control
stochastic games
Stochastic hybrid system
stochastic lambda calculus
Stochastic modeling
stochastic models
Stochastic multi-scenario optimization
stochastic reachability
stochastic shortest path
Stochastic simulation
Stone space
Straight-Line Graphs
strategic graph rewriting
strategies
strategy languages
Strategy Logic
Strategy synthesis
Streaming string transducers
Streams
Streett objectives
strict inequalities
Strict partial orders
strictification
string data structure
string data structures
string diagram
string diagrams
string rewriting
strings
strong sums
strongest postcondition
strongly normalizable terms
Structural modeling
Structural Operational Semantics
structural proof theory
structural rules
structure theory
stubborn sets
subject reduction
substitutability
Substitution
substructural calculus
subterm convergent theories
Subtyping
succinct ordered tree coding
sums of nonnegative circuit polynomials
sums of squares
sums-of-squares
superposition
swarms
SyGuS
Sylleptic categories
Symbolic Algorithms
Symbolic Analysis
symbolic automata
symbolic behavioral semantics
symbolic computation
symbolic constraints
symbolic cryptography
Symbolic evaluation
Symbolic Execution
symbolic heap
Symbolic heaps
Symbolic model
symbolic models
symbolic sampling
symbolic security
Symmetric monoidal categories
Symmetries
Symmetry Breaking
Symmetry reduction
Symmetry Rule
Symmetry-Breaking Predicates
Synchronization
synchronizations
Synchronous Programming
syntactic models
syntax
Syntax guided synthesis
syntax of type theory
Syntax-Guided Synthesis
Synthesis
Synthetic Biology
Synthetic Data
Synthetic Geometry
Synthetic Topology
system architectures
System Composition
system description
system F
System Verification
System-based design
Systematic Testing
systematicity
Systems Biology
Systems decomposition
Systems of recursion equations
syzygies
T
Tableau calculus
tableaux
tabling
tactics
tail bound
taint analysis
Taylor expansion
Taylor expansion of lambda-terms
Taylor models
TCP server
teaching
Teaching computer science with proof assistants
Technology
templates
Temporal Answer Set Programming
Temporal Logic
temporal logic of repeating values
Temporal logics
Temporal Verification
Tensor logic
tensorflow
tensorial logic
Term graph transformation
term orderings
term rewriting
term rewriting systems
termination
termination analysis
termination proofs
Termination Proving
termination tools
test case generation
Testing
text documents
text-based interaction
textual inference
The Coq Proof Assistant
the MRDP theorem
The Santa Claus Problem
theorem proving
Theorem Proving by Induction
theories
Theory of Computation
threads
Time complexity Analysis
Time Models
Time Refinement
Time-varying graphs
Timed automata
timed systems
timed-arc Petri nets
timing
timing attacks
timing transformations
TLS
tool
Tool paper
toolkit
top tree
top-down
topologicai logics
Topological Quantum Computation
topos theory
total correctness
Total Store Ordering
Totalizer
tptp
Trace semantics
traceability
traced monoidal categories
Traffic Scenarios
Trajectory
transcendental syntax
transducers
transduction
transition system
Transitive Closure
Transitive closure logic
Translation
Translation Lookaside Buffer (TLB)
translations
treap
Tree
tree automata
tree automata completion
tree constraints
Tree Decompositions
tree-depth
Trees
treewidth
tripos
true concurrency
truncation levels
Trust Management
trusted code base
trusted computing base
Tseitin formulas
tuple-generating dependencies
Turing degrees
tutoring
Two player games
two-level type theory
two-player games
Two-player win/lose
two-variable logic
type classes
Type Inference
type inference and type inhabitation
type inhabitation
type refinement systems
type system
type systems
type theory
Type-based Development
type-logical grammar
typed assembly languages
typed lambda calculus
typing results
U
UD
Ultrametrics
UML
unambiguous
unary negation fragment
Uncertain planning
Uncertainty
Uncountability
Undecidability
under-approximations
unification
unification problem
uniform interpolation
uniform intersection types
uniform one-dimensional fragment
uniform proof
Uniform quasi-wideness
uniform substitution
Unifying Theories of Programming
Uninterpreted Function Symbols
unions
unions of relations
unique normal form property
unit equality
unit propagation
unit testing
Univalence
univalence axiom
univalent foundations
universal algebra
universal IDE
Universe
universes
Unmanned Aircraft Systems
unraveling
Unsatisfiability proof generation
untyped call by value lambda calculus
untyped lambda calculus
Unweighted Partial MaxSAT
Usability
user interface
Utility Theory
V
vacuity
Vacuity Checking
validation
Validation and verification
value iteration
vampire
variant analysis
VC-density
VC-dimension
VDM
VDM-RT
VDMJ
vector addition systems with states
vector Lyapunov functions
Vehicle-to-Vehicle
verifiable electronic voting
Verification
verified compilation
verified compiler
Verified Prover
Vienna Development Method (VDM)
view
View abstraction
Virtual Machine
virtual physiological human
Visualization
Volume Computation
Volume Estimation
Von Neumann-Morgenstern Utility Theorem
VSCode
W
watchlist guidance
WCET analysis
weak diamond property
Weak Memory
weak memory models
Weak omega category theory
weak subgame perfect equilibria
weak units
weakest precondition
weakness
Web Service Composition
Web services
Web services composition
Weighted MaxSAT
weighted model counting
Weighted timed automata
well-founded relations
Well-foundedness
while programs with atoms
wide-spectrum language
Wireless Networks
witness generation
Witnessing
witnessing theorems
wordnet
Workflows
World View Constraints
World View Rules
Wreath Products
WS1S
WSN
WV Facts
X
XORSAT
XSB
Y
Yoneda isomorphism
Z
Zariski topology
zw calculus
zx calculus
α
α-conversion