FLOC 2018: FEDERATED LOGIC CONFERENCE 2018

This page contains an index consisting of author-provided keywords.

#
#SAT	(LaSh) Solving #SAT by Parameterized Algorithms: Exploiting Small Treewidth
#SMT(BV)	(IJCAR) A New Probabilistic Algorithm for Approximate Model Counting
#SMT(LA)	(PRUV) VolCE: An Efficient Tool for Solving #SMT(LA) Problems
2
2-CNF	(SAT) Minimal unsatisfiability and minimal strongly connected digraphs
A
A-infinity-(co)algebras	(HDRA) Minimal models for monomial algebras
abductive reasoning	(IJCAR) A Generic Framework for Implicate Generation Modulo Theories
Abella	(LFMTP) Functional programming with λ-tree syntax: a progress report (LFMTP) Computation-as-deduction in Abella: work in progress
ABNF	(VSTTE) A Formalization of the ABNF Notation and a Verified Parser of ABNF Grammars
Absolute Correctness	(REFINE) Programming Without Refinement
abstract interpretation	(FM) Software Safety and Security and AI (SMT) Selfless Interpolation for Infinite-State Model Checking (LICS) Sound up-to techniques and Complete abstract domains (IJCAR) Checking Array Bounds by Abstract Interpretation and Symbolic Expressions (CSF) Inductive Invariants for Noninterference in Multi-agent Workflows (VSTTE) The Map Equality Domain (ICLP) An iterative approach to precondition inference using constrained Horn clauses (ICLP) Towards Static Performance Guarantees for Programs with Run-time Checks (ICLP) Towards Incremental and Modular Context-sensitive Analysis
abstract recursion theory	(LCC) Computability over locally finite structures from algebra
abstract state machine	(DCM) Generic Graph Semantics
Abstract State Machines	(F-IDE) AsmetaF: a flattener for the ASMETA framework
Abstract syntax	(LFMTP) What Does This Notation Mean Anyway? BNF-style notation as it is actually used (LICS) Syntax and Semantics for Operations with Scopes
abstract winning condition	(SR) Concurrent games and semi-random determinacy
Abstraction	(CAV) Reasoning About TSO Programs Using Reduction and Abstraction (FM) Towards `Verifying' a Water Treatment System (ASPOCP) Towards Abstraction in ASP with an Application on Reasoning about Agent Policies (WST) Well-founded models in proofs of termination
abstraction learning	(LearnAut)
abstraction refinement	(CAV) Spacetime Interpolants (ICLP) An iterative approach to precondition inference using constrained Horn clauses
abstraction-refinement	(IJCAR) An abstraction-refinement framework for reasoning with large theories
accumulated weight constraints	(LICS) Stochastic Shortest Paths and Weight-Bounded Properties in Markov Decision Processes
Ackermann's Lemma	(IJCAR) FAME: An Automated Tool for Semantic Forgetting in Expressive Description Logics
ACL2	(VSTTE) A Formalization of the ABNF Notation and a Verified Parser of ABNF Grammars
action language	(ICLP-DC) Explaining Actual Causation via Reasoning about Actions and Change (ICLP-DC) Probabalistic Action Language pBC+ (ICLP) A Probabilistic Extension of Action Language BC+
Active Objects	(AVOCS) Detecting Deadlocks in Formal System Models with Condition Synchronization
Actor	(FM) Deadlock Detection for Actor-based Coroutines
actors	(FM) SDN-Actors: Modeling and Verification of SDN Programs
Actual Cause	(ICLP-DC) Explaining Actual Causation via Reasoning about Actions and Change
ACUI	(UNIF) ACUI Unification modulo Ground Theories
Ada programming	(WPTE) Verification of Ada Programs with AdaHorn
adaptive	(VaVAS) Work-in-Progress: Adaptive Neighborhood Resizing for Stochastic Reachability in Distributed Flocking
additive monad	(LICS) Dialectica models of type theory
adequate numeral system	(ITRS)
adjoint logic	(Linearity/TLLA) On the Lambek Calculus with an Exchange Modality
adjoint model	(Linearity/TLLA) On the Lambek Calculus with an Exchange Modality
adjunction	(MSFP) Relating Idioms, Arrows and Monads from Monoidal Adjunctions
Adjunctions	(HDRA) Termination in linear (2,2)-categories with braidings and duals
admissibility	(SR) Beyond admissibility: Dominance between chains of strategies
admissible rules	(CL&C) Admissible tools in the kitchen of intuitionistic logic
affine term	(Linearity/TLLA) How to count linear and affine closed lambda terms?
Agda	(MSFP) Formalizing Constructive Quantifier Elimination in Agda (ITP) Verified Timing Transformations in Synchronous Circuits with LambdaPi-Ware (ITP) An Agda Formalization of Üresin & Dubois' Asynchronous Fixed-Point Theory (LOLA) Experimenting with graded monads: certified grading-based program transformations (REFINE) Ordering strict partial orders to model behavioural refinement
agent policies	(ASPOCP) Towards Abstraction in ASP with an Application on Reasoning about Agent Policies
agent programming	(VaVAS) Formalisation of the Rules of the Road for embedding into an Autonomous Vehicle Agent
agents	(VaVAS) Social Consequence Engines (Abstract)
Aggregates	(ICLP) Functional ASP with Intensional Sets; Application to Gelfond-Zhang Agreggates (ICLP) Declarative Algorithms in Datalog with Aggregates: user-friendly formal semantics conducive to performance and scalability
aggregations in logic programming	(ICLP) Shared aggregate sets in answer set programming
AI Safety	(CAV) Safety-Aware Apprenticeship Learning
air traffic surveillance systems	(FM) A Formally Verified Floating-Point Implementation of the Compact Position Reporting Algorithm
Alarm ranking	(MLP) Difflog: Beyond Deductive Methods in Program Analysis
Algebra	(LaSh) Declarative Dynamic Programming with Inverse Coupled Rewrite Systems
algebra in type theory	(LICS) Degrees of Relatedness - A Unified Framework for Parametricity, Irrelevance, Ad Hoc Polymorphism, Intersections, Unions and Algebra in Dependent Type Theory
algebraic confluence	(IWC) Coherence of monoids by insertions
Algebraic crossover operators	(RCRA) Algebraic Crossover Operators for Permutations
algebraic effects	(FM) Modular Verification of Programs with Effects and Effect Handlers in Coq (LICS) Syntax and Semantics for Operations with Scopes (LICS) Quantitative Behavioural Reasoning for Higher-order Effectful Programs: Applicative Distances
Algebraic evolutionary computation	(RCRA) Algebraic Crossover Operators for Permutations
algebraic extensions	(SCSC) EA: New in CoCoA-5.2.4 and CoCoALib-0.99570 for SC-Square
Algebraic Geometry	(LICS) Polynomial Invariants for Affine Programs (Linearity/TLLA) Entropy and Complexity Lower Bounds
algebraic proof systems	(SCSC) RP: Refutation of Products of Linear Polynomials
algebraic structures	(LICS) Free Higher Groups in Homotopy Type Theory
algorithm	(CAV) Attracting Tangles to Solve Parity Games
Algorithm selection	(QBF) Portfolio-Based Algorithm Selection for Circuit QBFs
algorithm substitution attacks	(CSF) Self-Guarding Cryptographic Protocols against Algorithm Substitution Attacks
algorithmic complexity	(LICS) A modal mu perspective on solving parity games in quasipolynomial time.
algorithms	(SCSC) RP: Unknot Recognition Through Quantifier Elimination
all maximal clique partitions in a graph	(UNIF) Proximity-Based Generalization
allegories	(LICS) Allegories: decidability and graph homomorphisms
alloy	(FM) CompoSAT: Specification-Guided Coverage for Model Finding (F-IDE) Improving the Visualization of Alloy Instances
Almost Full relations	(IJCAR) Constructive Decision via Redundancy-free Proof-Search
Almost-sure winning	(CAV) Symbolic Algorithms for Graphs and Markov Decision Processes with Fairness Objectives
alpha-equivalence	(FSCD) Fixed-Point Constraints for Nominal Equational Unification
Alternating Automata	(LICS) The State Complexity of Alternating Automata
Alternating time	(IJCAR) Focussing, MALL and the polynomial hierarchy
Alternating-time Temporal Logic	(SR) Verification of Multi-agent Systems with Imperfect Information and Public Actions
AMBA AHB	(CAV) Strix: Explicit Reactive Synthesis Strikes Back!
anaphora	(NLCS) Paychecks, Presupposition, and Dependent Types
Android Applications	(AVOCS) Rule-Based Synthesis of Chains of Security Functions for Software-Defined Networks
Android back stack	(CAV) Android Stack Systems
Android stack systems	(CAV) Android Stack Systems
Animation	(Overture) ViennaVM: a Virtual Machine for VDM-SL development (ICLP) CHRvis: Syntax and Semantics
annotation	(VEMDP) Executable Biochemical Space for Specification and Analysis of Biochemical Systems
answer set	(ASPOCP) Syntactic Conditions for Antichain Property in Consistency Restoring Prolog
answer set computation	(ICLP) MASP-Reduce: a proposal for distributed computation of stable models
Answer Set Programming	(ICLP-DC) Scalable Robotic Intra-Logistics with Answer Set Programming (ICLP-DC) Translating P-log, LP^{MLN}, LPOD, and CR-Prolog2 into Standard Answer Set Programs (ICLP-DC) Explaining Actual Causation via Reasoning about Actions and Change (ICLP-DC) Model Revision of Logical Regulatory Networks using Logic-based Tools (ICLP-DC) Speeding Up Lazy-Grounding Answer Set Solving (LPOP) How to upgrade ASP for true dynamic modelling and solving? (LPOP) Role-Based Access Control via JASP (LPOP) Invited Talk: On the Development of Industrial Applications with ASP (ASPOCP) Towards Abstraction in ASP with an Application on Reasoning about Agent Policies (ASPOCP) selp: A Single-Shot Epistemic Logic Program Solver (ASPOCP) Invited Talk: Optimization Problems in Answer Set Programming (RCRA) Logic Programming approaches for routing fault-free and maximally-parallel Wavelength Routed Optical Networks on Chip (Application paper) (RCRA) Externally Supported Models for Efficient Computation of Paracoherent Answer Sets (ICLP) Functional ASP with Intensional Sets; Application to Gelfond-Zhang Agreggates (ICLP) First-order answer set programming as constructive proof search (ICLP) Routing Driverless Transport Vehicles in Car Assembly with Answer Set Programming (ICLP) Optimal Scheduling for Exposed Datapath Architectures with Buffered Processing Units by ASP (ICLP) A Trajectory Calculus for Qualitative Spatial Reasoning Using Answer Set Programming (ICLP) Exploiting Answer Set Programming with External Sources for Meta-Interpretive Learning (ICLP) Cautious Reasoning in ASP via Minimal models and Unsatisfiable Cores (ICLP) Shared aggregate sets in answer set programming (ICLP) Incremental and Iterative Learning of Answer Set Programs from Mutually Distinct Examples (ICLP) Experimenting with robotic intra-logistics domains (ICLP) Temporal Answer Set Programming on Finite Traces (ICLP) Specifying and Verbalising Answer Set Programs in Controlled Natural Language (ICLP) SMT-based Answer Set Solver CMODELS(DIFF) (System Description) (ICLP) MASP-Reduce: a proposal for distributed computation of stable models (ICLP) Introspecting Preferences In Answer Set Programming (ICLP) Learning Commonsense Knowledge through Interactive Dialogue (ICLP) Epistemic Logic Programs with World View Constraints
Answer Set Programming Extensions	(ASPOCP) A Survey of Advances in Epistemic Logic Program Solvers
Anti-unification	(FSCD) Term-Graph Anti-Unification (FSCD) Higher-Order Equational Pattern Anti-Unification (UNIF) Proximity-Based Generalization (UNIF) Towards Generalization Methods for Purely Idempotent Equational Theories (NLCS) Anti-Unification and Natural Language Processing
Apache Spark	(ICLP) MASP-Reduce: a proposal for distributed computation of stable models
Application	(ICLP) Application of Logic-Based Methods to Machine Component Design
applicative bisimulation distance	(LICS) Quantitative Behavioural Reasoning for Higher-order Effectful Programs: Applicative Distances
applicative first-order logic	(IJCAR) Superposition for Lambda-Free Higher-Order Logic
applicative functor	(MSFP) Relating Idioms, Arrows and Monads from Monoidal Adjunctions
applicative simulation distance	(LICS) Quantitative Behavioural Reasoning for Higher-order Effectful Programs: Applicative Distances
applied lambda-calculus	(LICS) Type-two polynomial-time and restricted lookahead.
Apprenticeship Learning	(CAV) Safety-Aware Apprenticeship Learning
Approximable Mappings	(Domains13) A logical view of complex analytic maps
approximate circuits	(CAV) ADAC: Automated Design of Approximate Circuits
approximate counting	(LCC) Feasibly constructive proofs of succinct weak circuit lower bounds
approximate equivalence checking	(CAV) ADAC: Automated Design of Approximate Circuits
Approximate inference	(ICLP) Constraint-Based Inference in Probabilistic Logic Programs
approximate partial order reduction	(FM) Approximate Partial Order Reduction
Approximate synthesis	(CAV) What’s hard about Boolean Functional Synthesis?
Approximation	(SMT) The next 10^4 UppSAT Approximations (IJCAR) Exploring Approximations for Floating-Point Arithmetic using UppSAT
Approximation Fixpoint Theory	(ICLP) Approximation Fixpoint Theory and the Well-Founded Semantics of Higher-Order Logic Programs
approximation theorem	(HOR) Refining Properties of Filter Models: Sensibility, Approximability and Reducibility
architecture	(FM) IPL: An Integration Property Language for Multi-Model Cyber-Physical Systems (VSTTE) Constructing Independently Verifiable Privacy-Compliant Type Systems for Message Passing between Black-Box Components
Arithmetic	(VSTTE) Extending VIAP to Handle Array Programs
arithmetic circuits	(LICS) Model-Theoretic Characterizations of Boolean and Arithmetic Circuit Classes of Small Depth
Armstrong relation	(IJCAR) Automated Reasoning about Key Sets
Array	(VSTTE) Extending VIAP to Handle Array Programs
Arrays	(IJCAR) Checking Array Bounds by Abstract Interpretation and Symbolic Expressions
arrow	(MSFP) Relating Idioms, Arrows and Monads from Monoidal Adjunctions
Artificial Intelligence	(POS) MLIC: A MaxSAT-Based framework for learning interpretable classification rules (SAT) QBF as an Alternative to Courcelle's Theorem
ASMETA	(F-IDE) AsmetaF: a flattener for the ASMETA framework
ASN.1	(CAV) Formal Verification of a Vehicle-to-Vehicle (V2V) Messaging System
ASP	(ICLP) Translating LPOD and CR-Prolog2 into Standard Answer Set Programs
ASP systems	(LPOP) Invited Talk: On the Development of Industrial Applications with ASP
ASPIDE	(LPOP) Invited Talk: On the Development of Industrial Applications with ASP
Assertions	(ICLP) Towards Static Performance Guarantees for Programs with Run-time Checks
Associative operad	(HDRA) Generalizations of the associative operad and convergent rewrite systems
assumptions refinement	(DS-FM) Heuristic-Based GR(1) Assumptions Refinement (FM) A Weakness Measure for GR(1) Formulae
Asynchronous	(CAV) Synthesis Of Asynchronous Reactive Programs From Temporal Specifications (ITP) An Agda Formalization of Üresin & Dubois' Asynchronous Fixed-Point Theory
Asynchronous Games	(LICS) An Asynchronous Soundness Theorem for Concurrent Separation Logic
Atom tracing	(VEMDP) Rule-Based Gillespie Simulation of Chemical Systems
atom variables	(UNIF) Rewriting with Generalized Nominal Unification
Atomic flows	(TYDI) Proof complexity of deep inference: a survey
Atomic Formula	(LaSh) Lazy Automata Techniques for WS1S
ATP	(Vampire) Testing ATP folklore: a statistical analysis of Vampire proofs. (Linearity/TLLA) Benchmarking Linear Logic Translations
Attack patterns	(GraMSec) A state machine system for insider threat detection
attack trees	(GraMSec) Deciding the Non-Emptiness of Attack trees (GraMSec) The Attacker Does not Always Hold the Initiative: Attack Trees with External Refinement (GraMSec) On Linear Logic, Functional Programming, and Attack Trees (CSF) Guided design of attack trees: a system-based approach
attacker knowledge	(CSF) Assuming you know: epistemic semantics of relational annotations for expressive flow policies
Attempto Controlled English	(ICLP) Natural Language Generation From Ontologies: Application Paper
attribute-based access control	(FCS) An Expressive, Flexible and Uniform Logical Formalism for Attribute-based Access Control
Authentication	(CSF) An extensive formal analysis of multi-factor authentication protocols
auto-generated code	(FM) Verifying Auto-Generated C Code from Simulink
autocorrelation	(SCSC) Hard Combinatorial Problems: A Challenge for Satisfiability
automata	(CAV) The Learnability of Symbolic Automata
automata learning	(CAV) The Learnability of Symbolic Automata (LearnAut)
Automata over infinite words	(LICS) One Theorem to Rule Them All: A Unified Translation of LTL into ω-Automata
automata theory	(GS) Automata Theory and Game Semantics (LICS) The State Complexity of Alternating Automata
Automata with counters	(SR) Quantifying Bounds in Strategy Logic
Automated Algebraic Reasonings	(Coq) ComplCoq: Rewrite Hint Construction with Completion Procedures
automated complexity analysis	(LICS) Efficient Algorithms for Asymptotic Bounds on Termination Time in VASS
Automated configuration	(RCRA) On the Configuration of SAT Formulae
Automated digital control	(SYNT) Safe, Automated and Formal Synthesis of Digital Controllers for Continuous Plants
automated guided vehicle routing	(ICLP) Routing Driverless Transport Vehicles in Car Assembly with Answer Set Programming
automated reasoning	(CAV) Understanding and Extending Incremental Determinization for 2QBF (CAV) Model Generation for Quantified Formulas: A Taint-Based Approach (WiL) On the Combination of Resolution and SAT Procedures for Modal Theorem-Proving (IJCAR) Automated Reasoning about Key Sets (IJCAR) ATPboost: Learning Premise Selection in Binary Setting with ATP Feedback (ITP) Understanding Parameters of Deductive Verification: an Empirical Investigation of KeY (CSF) Alethea: A Provably Secure Random Sample Voting Protocol
automated reasonning	(SMT) Centralizing Equality Reasoning in MCSAT
automated theorem proving	(ARQNL) System Demonstration: The Higher-Order Prover Leo-III (ThEdu) Towards intuitive reasoning in axiomatic geometry (Vampire) Towards Word Sense Disambiguation by Reasoning (Vampire) Experimenting with Theory Instantiation in Vampire (Vampire) Developments in Higher-order Theorem proving within Vampire (PAAR) TFX: The TPTP Extended Typed First-order Form (IJCAR) A FOOLish Encoding of the Next State Relations of Imperative Programs (IJCAR) Efficient encodings of first-order Horn formulas in equational logic (IJCAR) ATPboost: Learning Premise Selection in Binary Setting with ATP Feedback (IJCAR) The Higher-Order Prover Leo-III (F-IDE) Lightweight Interactive Proving inside an Automatic Program Verifier
automated trading systems	(Linearity/TLLA) Formalization of Automated Trading Systems in a Concurrent Linear Framework
Automated verification	(CAV) Formal Verification of a Vehicle-to-Vehicle (V2V) Messaging System (CAV) Constraint-Based Synthesis of Coupling Proofs (CSF) Automated Unbounded Verification of Stateful Cryptographic Protocols with Exclusive OR (CSF) An extensive formal analysis of multi-factor authentication protocols
automatic algorithm configuration	(POS) CryptoMiniSat Parameter-Optimization for Solving Cryptographic Instances
Automatic Program Verification	(VSTTE) Extending VIAP to Handle Array Programs
Automatic Proof checking	(SCSC) RP: A Practical Polynomial Calculus for Arithmetic Circuit Verification
automatic verification	(CAV) The DEEPSEC prover (FM) Compositional Reasoning for Shared-variable Concurrent Programs (WiL) Embedding Intuitionistic Modal Logics in Higher-Order Logic. An Easy Task?
automation	(FSCD) Completion for Logically Constrained Rewriting
Automaton State	(LaSh) Lazy Automata Techniques for WS1S
automotive	(FM) Verifying Auto-Generated C Code from Simulink
Automotive case study	(FM) Formal Verification of Automotive Simulink Controller Models: Empirical Technical Challenges, Evaluation and Recommendations
Autonomous	(VaVAS)
Autonomous automotive	(FM) Resource-aware Design for Reliable Autonomous Applications with Multiple Periods
Autonomous Driving	(SCSC) EA: Constraint Systems from Traffic Scenarios for the Validation of Autonomous Driving
Autonomous system	(VaVAS) Towards a verifiable decision making framework for self-driving vehicles
Autonomous vehicle	(VaVAS) Probabilistic Model Checking for Autonomous Agent Strategy Synthesis - Extended Abstract
autonomous vehicles	(VaVAS) Formalisation of the Rules of the Road for embedding into an Autonomous Vehicle Agent
avatar	(Vampire) Giving AVATAR Quantifiers to Play With
avionics systems	(FM) Model-Based Testing for Avionics Systems
Axiom Pinpointing	(IJCAR) Enumerating Justifications using Resolution
axiomatic domain theory	(Domains13) Diffeological Spaces and Semantics for Differential Programming (Domains13) Invited Talk: A domain theory for quasi-Borel spaces and statistical probabilistic programming
Axiomatic Method	(HoTT/UF) Univalent Foundations and the Constructive View of Theories
axiomatization	(LICS) Allegories: decidability and graph homomorphisms (LICS) Riesz Modal Logic with Threshold Operators (IJCAR) Automated Reasoning about Key Sets
axioms	(IJCAR) Uniform Substitution for Differential Game Logic
B
B combinator	(FSCD) On repetitive right application of B-terms
B+ trees	(ADSL) Automating the Flow Framework
back-and-forth equivalences	(Domains13) Invited Talk: Approximating partial by total: fixpoint characterizations of back-and-forth equivalences
backdoor	(SAT) ALIAS: A Modular Tool for Finding Backdoors for SAT
backdoors	(CSF) Backdoored Hash Functions: Immunizing HMAC and HKDF
Backtracking	(ARQNL) Pseudo-Propositional Logic (SAT) Chronological Backtracking
Backus FP	(HDRA) Minimal Bacus FP is Turing Complete
Backward exploration ·	(AVOCS) Backward reachability analysis for timed automata with data variables
backwards analysis	(ICLP) An iterative approach to precondition inference using constrained Horn clauses
Bar inductive predicates	(ITP) Proof Pearl: Constructive Extraction of Cycle Finding Algorithms
barcan formulas	(EICNCL) Proof theory for quantified monotone modal logics
Barendregt's Variable Convention	(LFMTP) Formalisation of Barendregt's Variable Convention for Generic Structures with Binders
Barrier Certificates	(CAV) Reachable Set Over-approximation for Nonlinear Systems Using Piecewise Barrier Tubes (FM) Vector Barrier Certificates and Comparison Systems
Basis Reduction	(ITP) A Formalization of the LLL Basis Reduction Algorithm
Bayesian inference	(MLP) Difflog: Beyond Deductive Methods in Program Analysis
Bayesian learning	(LearnAut) Learning Tree Distributions by Hidden Markov Models
Bayesian network	(GraMSec) Combining Bayesian Networks and Fishbone Diagrams to Distinguish between Intentional Attacks and Accidental Technical Failures
BayesianInference	(VEMDP) Bayesian Verification of Chemical Reaction Networks
BDD	(RCRA) Encoding PB Constraints into SAT via Binary Adders and BDDs -- Revisited
Behavioural equivalence	(CAV) The DEEPSEC prover
Behavioural metrics	(LICS) A van Benthem Theorem for Fuzzy Modal Logic
Belenios	(CSF) Machine-checked proofs for electronic voting: privacy and verifiability for Belenios
Belief Function Theory	(PRUV) Evidential Group Decision Making Model with Belief-Based Preferences
belief merging	(PRUV) Measuring Disagreement among Knowledge Bases
Belief networks	(MLP) Difflog: Beyond Deductive Methods in Program Analysis
benchmark	(Linearity/TLLA) Benchmarking Linear Logic Translations
Benchmarking	(LICS) A Simple and Optimal Complementation Algorithm for Büchi Automata (ICLP) Experimenting with robotic intra-logistics domains
beta reduction	(NLCS) Do different syntactic trees yield different logical readings? Some remarks on head variables in typed lambda calculus.
Beth models	(LICS) Computability Beyond Church-Turing via Choice Sequences
Betweenness Centrality	(SAT) Centrality-Based Improvements to CDCL Heuristics
Bi-directional Grammars	(ICLP) Specifying and Verbalising Answer Set Programs in Controlled Natural Language
bi-intuitionistic logic	(CL&C) Towards a Dualized Sequent Calculus with Canonicity
bicategories	(HDRA) Merge-bicategories: towards semi-strictification of higher categories
Bidding games	(SR) Infinite-Duration Richman Bidding Games
Biform theories	(ITP) HOL Light QE
BiLSTM	(MLP) Splitting source code identifiers using Bidirectional LSTM Recurrent Neural Network
Bimonad	(FSCD) Lifting Coalgebra Modalities and IMELL Model Structure to Eilenberg-Moore Categories
binarized neural network	(SAT) Constrained Image Generation Using Binarized Neural Networks with Decision Procedures
binarized neural networks	(VSTTE) Verification of Binarized Neural Networks via Inter-Neuron Factoring
Binary Analysis	(SAT) Effective use of SMT solvers for Program Equivalence Checking through Invariant Sketching and Query Decomposition
Binary Encoding	(PC) Resolution and the binary encoding of combinatorial principles
binary search tree	(ITP) Verified Analysis of Random Binary Tree Structures
binder mobility	(LFMTP) Functional programming with λ-tree syntax: a progress report
Binders	(LFMTP) Abstract Representation of Binders in OCaml using the Bindlib Library
Binding operations	(UNIF) Efficiency of a good but not linear nominal unification algorithm
Bioinformatics	(ICLP) Phylotastic: An Experiment in Creating, Manipulating, and Evolving Phylogenetic Biology Workflows Using Logic Programming
bisimulation	(VEMDP) Using Transitivity and Modularity in Chemical Reaction Network Bisimulation (LICS) Quasi-Open Bisimilarity with Mismatch is Intuitionistic
bit-blasting	(SMT) Building Better Bit-Blasting for Floating-Point Problems
Bit-vectors	(CAV) BTOR2, BtorMC and Boolector 3.0
Bitcoin	(GraMSec) Tendrils of Crime: Visualizing the Diffusion of Stolen Bitcoins
Bitvectors	(WST) Complexity Analysis for Bitvector Programs
black-box optimization	(SAT) ALIAS: A Modular Tool for Finding Backdoors for SAT
BLESS	(Vampire) Towards Word Sense Disambiguation by Reasoning
Blockchain	(SMT) SMT-based Compile-time Verification of Safety Properties for Smart Contracts
blocked clauses	(IJCAR) Extended Resolution Simulates DRAT
bobs-only	(POS) Stedman and Erin Triples encoded as a SAT Problem
boolean algebra	(LICS) Classical realizability as a classifier for nondeterminism
Boolean Functional synthesis	(CAV) What’s hard about Boolean Functional Synthesis?
Boolean games	(SR) Local Equilibria in Logic-Based Multi-Player Games
Boolean polynomials	(SCSC) RP: Refutation of Products of Linear Polynomials
Boolean Satisfiability	(ICLP-DC) Model Revision of Logical Regulatory Networks using Logic-based Tools (IJCAR) A SAT-Based Approach to Learn Explainable Decision Sets (POS) Stedman and Erin Triples encoded as a SAT Problem
Boolean-valued models	(LICS) Boolean-Valued Semantics for Stochastic Lambda-Calculus
Boot code	(CAV) Model Checking Boot Code from AWS Data Centers
bottom-up	(ICLP) Top-down and Bottom-up Evaluation Procedurally Integrated
Bounded	(UNIF) Bounded ACh Unification
bounded arithmetic	(PC) Towards theories for positive polynomial time and monotone proofs with extension (PC) (PC) Complexity of expander-based reasoning and the power of monotone proofs (TYDI) Proof complexity of deep inference: a survey (LCC) Feasibly constructive proofs of succinct weak circuit lower bounds
Bounded expansion	(LICS) Parameterized circuit complexity of model-checking on sparse structures
Bounded Model Checking	(CAV) JBMC: A Bounded Model Checking Tool for Verifying Java Bytecode (CAV) Lazy Self-Composition for Security Verification
bounded model-checking	(VSTTE) Lattice-Based Refinement in Bounded Model Checking
bounded synthesis	(CAV) Synthesizing Reactive Systems from Hyperproperties (SYNT) Maximum Realizability for Linear Temporal Logic Specifications
bounds on leakage	(CSF) Symbolic Side-Channel Analysis for Probabilistic Programs
Braidings	(HDRA) Termination in linear (2,2)-categories with braidings and duals
branching programs	(PC) Branching Program Complexity of Canonical Search Problems and Proof Complexity of Formulas
broadcast communication	(CSF) A Cryptographic Look at Multi-Party Channels
Brzozowski derivatives	(LaSh) A Derivative-Based Decision Procedure for WS1S
Buchberger algorithm	(HDRA) Generalizations of the associative operad and convergent rewrite systems
Buchi Automaton	(MoRe) Logically-Constrained Reinforcement Learning
Bug Finding	(CAV) Partial Order Aware Concurrency Sampling
bug finding tool	(CAV) SimpleCAR: An Efficient Bug-Finding Tool Based On Approximate Reachability
Bunched Implications Logic	(EICNCL) Proof Translations in BI logic
Business Process Model	(GraMSec) Disclosure Analysis of SQL Workflows
Böhm trees	(FSCD) Strict Ideal Completions of the Lambda Calculus (LICS) Probabilistic Böhm Trees and Probabilistic Separation
Büchi Automaton	(LICS) A Simple and Optimal Complementation Algorithm for Büchi Automata
C
C code	(FM) Verifying Auto-Generated C Code from Simulink
C Programming Language	(WST) Complexity Analysis for Bitvector Programs
cache coherence protocols	(CAV) Eager Abstraction for Symbolic Model Checking
Cached Address Translation	(ITP) Program Verification in the Presence of Cached Address Translation
CakeML	(VSTTE) Verified Certificate Checking for Counting Votes
calculational method	(ITP) Towards Verified Handwritten Calculational Proofs (Short Paper)
Calculational proof	(ITP) CalcCheck: a Proof Checker for Teaching the “Logical Approach to Discrete Math”
calculus of structures	(TYDI) Truely Concurrent Processes in the Calculus of Structures
call by push value	(ITP) A Formal Equational Theory for Call-by-Push-Value
call by value	(LICS) Eager Functions as Processes
call-by-name	(Linearity/TLLA) The Bang Calculus and the Two Girard's Translations
call-by-need evaluation	(WPTE) Optimizing Space of Parallel Processes
call-by-push value	(Linearity/TLLA) The Bang Calculus and the Two Girard's Translations
call-by-push-value	(Domains13) Algebra semantics of recursive computation types (LOLA) A resource modality for RAII
call-by-value	(ITRS) Towards a Semantic Measure of the Execution Time in Call-by-Value lambda-Calculus (Linearity/TLLA) The Bang Calculus and the Two Girard's Translations
CAMUS	(SAT) Finding all Minimal Safe Inductive Sets
car assembly operations	(ICLP) Routing Driverless Transport Vehicles in Car Assembly with Answer Set Programming
Cardinality Constraint	(SAT) Dynamic Polynomial Watchdog Encoding for Solving Weighted MaxSAT
cardinality encodings	(SAT) PySAT: A Python Toolkit for Prototyping with SAT Oracles
Cartesian cubes	(HoTT/UF) Cubical Computational Type Theory
Cartesian Genetic Programming	(CAV) ADAC: Automated Design of Approximate Circuits
Cartesian Monoids	(HDRA) Minimal Bacus FP is Turing Complete
cartesian-closed	(Domains13) Invited Talk: Topology and Domain Theory Interfaces
Case study	(FM) Verifying Auto-Generated C Code from Simulink (RCRA) Optimal Fault-Tolerant Placement of Relay Nodes in a Mission Critical Wireless Network
Catalan numbers	(HOR) Combinatorics of explicit substitutions (extended abstract)
categorial grammar	(NLCS) Do different syntactic trees yield different logical readings? Some remarks on head variables in typed lambda calculus.
Categorical Logic	(TYDI) Some incoherent musings on deep inference and combinatorial proofs (PARIS) LMSO: A Curry-Howard Approach to Church’s Synthesis via Linear Logic (speaker: Pierre PRADIC) (LICS) LMSO: A Curry-Howard Approach to Church's Synthesis via Linear Logic (LICS) The Syntax and Semantics of Quantitative Type Theory
Categorical model	(LICS) Syntax and Semantics for Operations with Scopes
Categorical models	(LICS) Extensional and Intensional Semantic Universes: A Denotational Model of Dependent Types (HoTT/UF) Dependent Right Adjoint Types (Linearity/TLLA) On the Lambek Calculus with an Exchange Modality
Categorical Quantum Mechanics	(FSCD) A diagrammatic axiomatisation of fermionic quantum circuits (LICS) Diagrammatic Reasoning beyond Clifford+T Quantum Mechanics (LICS) A Complete Axiomatisation of the ZX-Calculus for Clifford+T Quantum Mechanics (LICS) Two complete axiomatisations of pure-state qubit quantum computing
Categorical semantics	(LICS) Enriching a Linear/Non-linear Lambda Calculus: A Programming Language for String Diagrams (LICS) A Logical Account for Linear Partial Differential Equations (LICS) A General Framework for Relational Parametricity (HoTT/UF) Algebraic models of dependent type theory (Linearity/TLLA) Towards a Functional Language for Species of Structures
Categories of relations	(Domains13) Extending Stone Duality to Relations
categories with families	(HoTT/UF) Towards the syntax and semantics of higher dimensional type theory
Categorification	(HDRA) Termination in linear (2,2)-categories with braidings and duals
category	(LOLA) Heaps denote finitely partitioned trees
category theory	(FSCD) Call-by-name Gradual Type Theory (LICS) Dialectica models of type theory (LICS) A Generalized Modality for Recursion (LICS) What's in a game? A theory of game models (MSFP) Some No-Go Theorems for Distributive Laws (extended abstract) (SR) Compositional Game Theory
Causal Dependency	(LICS) Causal Computational Complexity of Distributed Processes
causality preservation	(CSF) A Cryptographic Look at Multi-Party Channels
Cautious Reasoning	(ICLP) Cautious Reasoning in ASP via Minimal models and Unsatisfiable Cores
ccg	(NLCS) Automated Reasoning from Polarized Parse Trees
CCSL	(REFINE) Ordering strict partial orders to model behavioural refinement
CDCL	(Isabelle) A Verified SAT Solver with Watched Literals Using Imperative HOL (Extended Abstract) (POS) Seeking Practical CDCL Insights from Theoretical SAT Benchmarks (POS) Divide and Conquer: Towards Faster Pseudo-Boolean Solving (SAT) Machine Learning-based Restart Policy for CDCL SAT Solvers (SAT) Chronological Backtracking (SAT) Centrality-Based Improvements to CDCL Heuristics
cdcl-cuttingplanes	(SAT) Using Combinatorial Benchmarks to Probe the Reasoning Power of Pseudo-Boolean Solvers
Cedille	(ITP) Efficient Mendler-Style Lambda-Encodings in Cedille
CEGIS	(CAV) Synthesis Modulo Theories
Cellular automata	(DCM) A Category Theoretic Interpretation of Gandy’s Principles for Mechanisms
cellular cohomology	(LICS) Cellular Cohomology in Homotopy Type Theory
Centrality	(SAT) Centrality-Based Improvements to CDCL Heuristics
Certificate checking	(ITP) Tactics and Certificates in Meta Dedukti (VSTTE) Verified Certificate Checking for Counting Votes
certificates	(SAT) Polynomial-Time Validation of QCDCL Certificates
certification	(IWC) Certified Ordered Completion
certified code	(ITP) A Formally Verified Solver for Homogeneous Linear Diophantine Equations
Certified execution engine	(ITP) A Coq Formalisation of SQL’S Execution Engines
certified software	(ITP) Towards Certified Meta-Programming with Typed Template-Coq
Certifying Compilation	(VSTTE) TWAM: A Certifying Abstract Machine for Logic Programs
channel composition	(FM) An Algebraic Approach for Reasoning About Information Flow
Character-level Language Model	(MLP) Splitting source code identifiers using Bidirectional LSTM Recurrent Neural Network
chat bot	(UITP) Automated Theorem Proving in a Chat Environment
chemical computation	(VEMDP) Computing properties of stable configurations of thermodynamic binding networks
Chemical Reaction Networks	(VEMDP) Using Transitivity and Modularity in Chemical Reaction Network Bisimulation (VEMDP) Noise control for molecular computing
Chinese monoids	(HDRA) String data structures for Chinese monoids
Choice Logic	(PRUV) A new logic for jointly representing hard and soft constraints
choice sequence	(Domains13) A Brouwerian proof of the Fan Theorem
Choice sequences	(LICS) Computability Beyond Church-Turing via Choice Sequences
choiceless polynomial time	(LICS) On computability and tractability for infinite sets
Chronological Backtracking	(SAT) Chronological Backtracking
Church's type theory	(ITP) HOL Light QE
Church-Turing thesis	(WST) Objective and Subjective Specifications
circuit	(SAT) Circuit-based Search Space Pruning in QBF
Circuit complexity	(LICS) Parameterized circuit complexity of model-checking on sparse structures
circuit lower bounds	(LCC) Feasibly constructive proofs of succinct weak circuit lower bounds
circuit satisfiability	(LICS) Satisfiability in multi-valued circuits
circular proofs	(PARIS) Local Validity for Circular Proofs in Linear Logic with Fixed Points
classical arithmetic	(LICS) A sequent calculus with dependent types for classical arithmetic
classical B	(AVOCS) Writing a Model Checker in 80 Days: Reusable Libraries and Custom Implementation
classical higher-order logic	(ARQNL) System Demonstration: The Higher-Order Prover Leo-III
classical linear logic	(WiL) A New Linear Logic for Deadlock-Free Session-Typed Processes (Talk Abstract)
classical logic	(TYDI) An introduction to deep inference (TYDI) Some incoherent musings on deep inference and combinatorial proofs (CL&C) Some ideas on cut-elimination for cyclic arithmetic proofs
classical realizability	(LICS) A sequent calculus with dependent types for classical arithmetic (LICS) Classical realizability as a classifier for nondeterminism (ITP) Formalizing Implicative Algebras in Coq
Classical sequent calculus	(CL&C) Herbrand's Theorem as Higher-Order Recursion
Clause Learning	(ITP) A Coq Tactic for Equality Learning in Linear Arithmetic
CLF	(Linearity/TLLA) Formalization of Automated Trading Systems in a Concurrent Linear Framework
clocks	(LICS) Guarded Computational Type Theory
closed set	(Domains13) T^\omega-representations of compact sets through dyadic subbases
cluster algebra	(IWC) Complete Axiom System of Cluster Algebra
clustering	(LearnAut) Learning Several Languages from Labeled Strings: State Merging and Evolutionary Approaches
CNF	(POS) The Effect of Scrambling CNFs
CNF configuration	(RCRA) On the Configuration of SAT Formulae
Co-Simulation	(Overture) Multi-modelling of Cooperative Swarms (Overture) Overture FMU: Export VDM-RT Models as Tool-Wrapper FMUs
Coalgebra Modality	(FSCD) Lifting Coalgebra Modalities and IMELL Model Structure to Eilenberg-Moore Categories
Coarse computability	(LICS) An answer to the Gamma question
Coarse-grained modeling	(VEMDP) Computational Approaches for the Programmed Assembly of Nanocellulose Meshes
CoCoA and MathSAT	(SCSC) EA: New in CoCoA-5.2.4 and CoCoALib-0.99570 for SC-Square
codatatypes	(IJCAR) Superposition with Datatypes and Codatatypes
code generation	(Isabelle) Lazy Algebraic Types in Isabelle/HOL (F-IDE) A Notebook Format for the Holistic Design of Embedded Systems (ITP) Fast Machine Words in Isabelle/HOL (ITP) A Formally Verified Solver for Homogeneous Linear Diophantine Equations (ITP) Software Verification with ITPs Should Use Binary Code Extraction to Reduce the TCB (Short Paper) (ICLP) Optimal Scheduling for Exposed Datapath Architectures with Buffered Processing Units by ASP
Code Generators	(Overture) ViennaVM: a Virtual Machine for VDM-SL development
code review	(FM) Evidential and Continuous Integration of Software Verification Tools
code-generation	(Overture) Enhancing Testing of VDM-SL models
coends	(Linearity/TLLA) Proof nets, coends and the Yoneda isomorphism
Cognitive Modeling	(LPOP) Confluence Analysis of Cognitive Models with Constraint Handling Rules
cographs	(Linearity/TLLA) Coherent interaction graphs: a nondeterministic geometry of interaction for MLL
coherence	(IWC) Coherence of monoids by insertions (IWC) Coherence modulo relations (FSCD) Coherence of Gray categories via rewriting (HoTT/UF) Towards the syntax and semantics of higher dimensional type theory (HDRA) Merge-bicategories: towards semi-strictification of higher categories
coherence theorems	(LICS) Ribbon tensorial logic
coherent presentations	(HDRA) String data structures for Chinese monoids
coinduction	(FSCD) Term rewriting characterisation of LOGSPACE for finite and infinite data (PARIS) Local Validity for Circular Proofs in Linear Logic with Fixed Points (PARIS) Coinductive Uniform Proofs: An Extended Abstract (speaker: Yue LI) (LICS) Every λ-Term is Meaningful for the Infinitary Relational Model (IJCAR) A Coinductive Approach to Proving Reachability in Logically Constrained Term Rewriting Systems (HCVS) Towards Coinductive Theory Exploration in Horn Clause Logic: Extended Abstract
coinduction up-to	(LICS) Sound up-to techniques and Complete abstract domains
Coinductive Invariants	(HCVS) Towards Coinductive Theory Exploration in Horn Clause Logic: Extended Abstract
coinductive types	(ITP) The Coinductive Formulation of Common Knowledge
Combination	(IJCAR) Complexity of Combinations of Qualitative Constraint Satisfaction Problems
Combinatorial benchmarks	(SAT) Using Combinatorial Benchmarks to Probe the Reasoning Power of Pseudo-Boolean Solvers
combinatorial proofs	(TYDI) Some incoherent musings on deep inference and combinatorial proofs (IJCAR) From Syntactic Proofs to Combinatorial Proofs
combinatorial search algorithms	(RCRA) Shaving with Occam's Razor: Deriving Minimalist Theorem Provers for Minimal Logic
combinatoric	(Linearity/TLLA) How to count linear and affine closed lambda terms?
Combinatorics	(FSCD) Counting Environments and Closures (HDRA) Generalizations of the associative operad and convergent rewrite systems (Linearity/TLLA) Towards a Functional Language for Species of Structures (HOR) Combinatorics of explicit substitutions (extended abstract)
combinators	(LICS) Regular Transducer Expressions for Regular Transformations over infinite words
combinatory logic	(FSCD) On repetitive right application of B-terms (Domains13) Domain Theory for Intensional Computation
common knowledge	(ITP) The Coinductive Formulation of Common Knowledge
Common Language for Geometric Problems	(ThEdu) Rating of Geometric Automated Theorem Provers
Commonsense Reasoning	(ICLP) Learning Commonsense Knowledge through Interactive Dialogue
commutative monads	(Domains13) Invited Talk: A domain theory for quasi-Borel spaces and statistical probabilistic programming
comonads	(Domains13) Invited Talk: Approximating partial by total: fixpoint characterizations of back-and-forth equivalences (NLCS) Propositional Attitude Operators in Homotopy Type Theory
Comparator	(CAV) Automata vs Linear-Programming Discounted-Sum Inclusion
comparator network	(POS) Competitive Sorter-based Encoding of PB-Constraints into SAT
comparison systems	(FM) Vector Barrier Certificates and Comparison Systems
CompCert	(FCS) A Study on the Preservation on Cryptographic Constant-Time Security in the CompCert Compiler
Competition	(POS) The Effect of Scrambling CNFs
compiler	(VEMDP) Equivalence of chemical reaction networks in a CRN-to-DNA compiler framework.
compiler verification	(LOLA) A more precise, more correct stack and register model for CompCert
Compilers	(SAT) Effective use of SMT solvers for Program Equivalence Checking through Invariant Sketching and Query Decomposition
complementary approximate reachability	(CAV) SimpleCAR: An Efficient Bug-Finding Tool Based On Approximate Reachability
Complementation	(LICS) A Simple and Optimal Complementation Algorithm for Büchi Automata
complete abstract domains	(LICS) Sound up-to techniques and Complete abstract domains
complete lattices	(ITP) Formalizing Implicative Algebras in Coq
Complete Segal Spaces	(HoTT/UF) (Truncated) Simplicial Models of Type Theory
completeness	(FSCD) Completeness of Tree Automata Completion (IJCAR) Formalizing Bachmair and Ganzinger's Ordered Resolution Prover (ADSL) A Complete Proof System for Basic Symbolic Heaps with Permissions
completion	(FSCD) Completion for Logically Constrained Rewriting (IJCAR) MaedMax: A Maximal Ordered Completion Tool (Coq) ComplCoq: Rewrite Hint Construction with Completion Procedures
complex analysis	(Domains13) Robust computability notions for types arising in classical analysis
Complexity	(FSCD) Counting Environments and Closures (FM) Timed Vacuity (Isabelle) Formal Verification of Bounds for the LLL Basis Reduction Algorithm (IJCAR) Complexity of Combinations of Qualitative Constraint Satisfaction Problems (ADSL) On the Complexity of Pointer Arithmetic in Separation Logic (ADSL) The Complexity of Prenex Separation Logic with One Selector
Complexity Analysis	(LCC) A General Equational Framework for Static Profiling of Parametric Resource Usage (WST) Complexity Analysis for Bitvector Programs
complexity classes	(FSCD) Unique perfect matchings and proof nets
complexity dichotomy	(LICS) A universal-algebraic proof of the complexity dichotomy for Monotone Monadic SNP
Complexity measures	(SAT) Cops-Robber games and the resolution of Tseitin formulas
Complexity Proving	(WST) A Perron-Frobenius Theorem for Jordan Blocks for Complexity Proving
complexity results	(MoRe) Constraint Problem for Weak Subgame Perfect Equilibria with omega-regular Boolean Objectives
Complexity Theory	(GraMSec) Deciding the Non-Emptiness of Attack trees (Linearity/TLLA) Entropy and Complexity Lower Bounds
composition	(FM) Modular Verification of Programs with Effects and Effect Handlers in Coq (CSF) Composition Theorems for CryptoVerif and Application to TLS 1.3
compositional analysis of software systems	(AVOCS) Using SMT engine to generate Symbolic Automata
compositional model checking	(FM) To Compose, Or Not to Compose, That is the Question: An Analysis of Compositional State Space Generation
compositional reasoning	(FM) Compositional Reasoning for Shared-variable Concurrent Programs
Compositional verification	(AVOCS) A Framework for the Formal Verification of Networks of Railway Interlockings - Application to the Belgian Railways
compositionality	(LICS) Compositional game theory (SR) Compositional Game Theory
Computability	(CAV) Program Analysis is Harder than Verification: A Computability Perspective (WiL) On Expanding Standard Notions of Constructivity (WST) Improving Static Dependency Pairs for Higher-Order Rewriting (LICS) An answer to the Gamma question (Domains13) Robust computability notions for types arising in classical analysis
computable metric space	(Domains13) T^\omega-representations of compact sets through dyadic subbases
computation and deduction	(LFMTP) Computation-as-deduction in Abella: work in progress
Computation Complexity	(LICS) Causal Computational Complexity of Distributed Processes
Computation Tree Logic	(LICS) Automaton-Based Criteria for Membership in CTL
computational complexity	(VEMDP) Using Transitivity and Modularity in Chemical Reaction Network Bisimulation (LCC) Computability over locally finite structures from algebra (LCC) Completeness in the Second Level of the Polynomial Time Hierarchy through Syntactic Properties (LICS) A pseudo-quasi-polynomial algorithm for solving mean-payoff parity games
computational effects	(Domains13) Algebra semantics of recursive computation types
Computational Hardness	(CAV) What’s hard about Boolean Functional Synthesis?
computational model	(CSF) Composition Theorems for CryptoVerif and Application to TLS 1.3
Computational modeling	(VEMDP) Computational Approaches for the Programmed Assembly of Nanocellulose Meshes
computational monads	(LICS) An algebraic theory of Markov processes
Computational Reductions	(ITP) Verification of PCP-Related Computational Reductions in Coq
computational soundness	(CSF) Symbolic security of garbled circuits
Computational thinking	(LICS) Sequential Relational Decomposition
computational type theory	(HoTT/UF) Cubical Computational Type Theory
computer aided security proofs	(CSF) Computer-aided proofs for multiparty computation with active security
Computer Algebra	(SCSC) RP: A Practical Polynomial Calculus for Arithmetic Circuit Verification
computer-aided cryptography	(CSF) Machine-checked proofs for electronic voting: privacy and verifiability for Belenios
concurrency	(FM) Operational Semantics of a Weak Memory Model with Channel Synchronization (GS) Resource-Tracking Concurrent Games (LICS) ReLoC: A Mechanised Relational Logic for Fine-Grained Concurrency (VSTTE) Store Buffer Reduction in The Presence of Mixed-Size Accesses and Misalignment (LOLA) Denotational Event structure for relaxed memory (REFINE) Challenges of specifying concurrent program components
concurrency and distributed computation	(LICS) Work Analysis with Resource-Aware Session Types
Concurrency Testing	(CAV) Partial Order Aware Concurrency Sampling
Concurrent datatypes	(FM) View abstraction for systems with component identities
concurrent dictionaries	(ADSL) Automating the Flow Framework
Concurrent games	(GS) A definable game semantics for the linear quantum lambda-calculus (GS) Continuous probability distributions in concurrent games (LICS) The concurrent game semantics of Probabilistic PCF
Concurrent objects	(REFINE) Refining Santa: An Excercise in Efficient Synchronization (REFINE) Correctness of Concurrent Objects under Weak Memory Models
Concurrent operation specification	(REFINE) Challenges of specifying concurrent program components
Concurrent Process Calculi	(LICS) Causal Computational Complexity of Distributed Processes
concurrent program algebra	(FM) Encoding fairness in a synchronous concurrent program algebra
concurrent programs	(Domains13) Invited Talk: A Brief History of Denotational Semantics
Concurrent Separation Logic	(LICS) An Asynchronous Soundness Theorem for Concurrent Separation Logic (ADSL) Automating the Flow Framework
Concurrent strategies	(LICS) What's in a game? A theory of game models
Condition Synchronization	(AVOCS) Detecting Deadlocks in Formal System Models with Condition Synchronization
Conditional Independence	(CAV) Constrained Dynamic Partial Order Reduction
Conditional logic	(EICNCL) Hypersequent calculus for the logic of conditional belief: preliminary results
conditional rewriting	(IWC) Convergence of Simultaneously and Sequentially Unraveled TRSs for Normal Conditional TRSs
conditional term rewriting	(FSCD) Narrowing Trees for Syntactically Deterministic Conditional Term Rewriting Systems
conditional value at risk	(LICS) Conditional Value-at-Risk for Reachability and Mean Payoff in Markov Decision Processes
Confidentiality	(CSF) A Cryptographic Look at Multi-Party Channels (CSF) The Complexity of Monitoring Hyperproperties
conflict-driven clause learning	(CAV) The Proof Complexity of SMT Solvers (POS) Seeking Practical CDCL Insights from Theoretical SAT Benchmarks
conflict-driven search	(POS) Divide and Conquer: Towards Faster Pseudo-Boolean Solving (SAT) In Between Resolution and Cutting Planes: A Study of Proof Systems for Pseudo-Boolean SAT Solving
confluence	(IWC) Towards a Verified Decision Procedure for Confluence of Ground Term Rewrite Systems in Isabelle/HOL (IWC) Convergence of Simultaneously and Sequentially Unraveled TRSs for Normal Conditional TRSs (FSCD) Decreasing diagrams with two labels are complete for confluence of countable systems (FSCD) Strict Ideal Completions of the Lambda Calculus (FSCD) Confluence of Prefix-Constrained Rewrite Systems
Confluence Analysis	(LPOP) Confluence Analysis of Cognitive Models with Constraint Handling Rules
Confluence and Standardization	(HDRA) Minimal Bacus FP is Turing Complete
confluence competition	(IJCAR) Cops and CoCoWeb: Infrastructure for Confluence Tools
Confluence modulo	(IWC) Coherence modulo relations
confluence tool	(IJCAR) Cops and CoCoWeb: Infrastructure for Confluence Tools
Confusion	(LICS) Concurrency and Probability: Removing Confusion, Compositionally
Congruence	(LearnAut) Decision problems for Clark-congruential languages
Connection-based proof-search	(ARQNL) Labelled Connection-based Proof Search for Multiplicative Intuitionistic Linear Logic
cons-free computation	(LCC) Computability over locally finite structures from algebra
Conservative approximation	(VEMDP) Conservative approximations of polymers
Conservativity	(LICS) Around Classical and Intuitionistic Linear Logics
consistency	(CAV) Monitoring Weak Consistency
Consistency Analysis	(AVOCS) Analyzing Consistency of Formal Requirements
Consistency Checking	(DS-FM) Consistency Checking of Functional Requirements
Consistency proofs	(CL&C) Some ideas on cut-elimination for cyclic arithmetic proofs
constant-time security	(FCS) A Study on the Preservation on Cryptographic Constant-Time Security in the CompCert Compiler
Constrained Horn Clauses	(SMT) Discovering Universally Quantified Solutions for Constrained Horn Clauses (WPTE) Verification of Ada Programs with AdaHorn (ICLP) Solving Horn Clauses on Inductive Data Types Without Induction
Constrained Optimization	(RCRA) Logic Programming approaches for routing fault-free and maximally-parallel Wavelength Routed Optical Networks on Chip (Application paper)
constrained rewriting	(FSCD) Completion for Logically Constrained Rewriting (VSTTE) Loop Detection by Logically Constrained Term Rewriting (WPTE) On Transforming Functions Accessing Global Variables into Logically Constrained Term Rewriting Systems
Constraint Handling Rules	(LPOP) Confluence Analysis of Cognitive Models with Constraint Handling Rules (ICLP) Shape Neutral Analysis of Graph-based Data-structures (ICLP) CHRvis: Syntax and Semantics (ICLP) A New Proof-theoretical Linear Semantics for CHR
Constraint Handling Rules (CHR)	(LPOP) Security Policies in Constraint Handling Rules
Constraint Language	(LaSh) Automated Constraint Modelling with Conjure (LaSh) ESSENCE, A Language for Specifying Combinatorial Problems: What, Why and So What?
Constraint Logic Programming	(HCVS) Metaprogramming and symbolic execution for detecting runtime errors in Erlang programs
Constraint Logic Programming on Finite Domains	(RCRA) Logic Programming approaches for routing fault-free and maximally-parallel Wavelength Routed Optical Networks on Chip (Application paper)
Constraint Modelling	(LaSh) Automated Constraint Modelling with Conjure (LaSh) ESSENCE, A Language for Specifying Combinatorial Problems: What, Why and So What?
constraint problem	(MoRe) Constraint Problem for Weak Subgame Perfect Equilibria with omega-regular Boolean Objectives
Constraint programming	(RCRA) Encoding PB Constraints into SAT via Binary Adders and BDDs -- Revisited
constraint satisfaction	(RCRA) Replaceability for constraint satisfaction problems: Algorithms, Inferences, and Complexity Patterns (RCRA) Partial (Neighbourhood) Singleton Arc Consistency for Constraint Satisfaction Problems
Constraint Satisfaction Problem	(LICS) Satisfiability in multi-valued circuits (IJCAR) Complexity of Combinations of Qualitative Constraint Satisfaction Problems
constraint satisfaction problems	(LICS) A universal-algebraic proof of the complexity dichotomy for Monotone Monadic SNP
Constraint satisfaction processing	(ICLP) SMT-based Answer Set Solver CMODELS(DIFF) (System Description)
Constraint Solving	(SCSC) EA: Constraint Systems from Traffic Scenarios for the Validation of Autonomous Driving (LaSh) Automated Constraint Modelling with Conjure (IJCAR) A Reduction from Unbounded Linear Mixed Arithmetic Problems into Bounded Problems (HCVS) Solving Constrained Horn Clauses Using Dependence-Disjoint Expansions (ICLP) Application of Logic-Based Methods to Machine Component Design
Constraint Systems	(SCSC) EA: Constraint Systems from Traffic Scenarios for the Validation of Autonomous Driving
Constraint-based synthesis	(CAV) Constraint-Based Synthesis of Coupling Proofs
Constraint-based verification	(CAV) Constraint-Based Synthesis of Coupling Proofs
constraints	(LPOP) Easier Rules and Constraints for Programming (WiL) Towards a Logical Framework for Latent Variable Modelling (PRUV) Evidential Group Decision Making Model with Belief-Based Preferences (ICLP) Constraint-Based Inference in Probabilistic Logic Programs (ICLP) Constraint Answer Set Programming without Grounding (ICLP) Epistemic Logic Programs with World View Constraints
constraints solver	(POS) Competitive Sorter-based Encoding of PB-Constraints into SAT
constructive	(MSFP) Formalizing Constructive Quantifier Elimination in Agda
Constructive Decidability	(IJCAR) Constructive Decision via Redundancy-free Proof-Search
constructive mathematics	(LICS) Computable decision making on the reals and other spaces via partiality and nondeterminism
Constructive Type Theory	(LFMTP) Formalization in Constructive Type Theory of the Standardization Theorem
Constructive View of Theories	(HoTT/UF) Univalent Foundations and the Constructive View of Theories
constructivism	(WiL) Towards a Logical Framework for Latent Variable Modelling
contact logics	(UNIF) About the unification type of topological logics over Euclidean spaces
context-free	(TERMGRAPH) A framework for rewriting families of string diagrams
Context-free Grammars	(ITP) Verification of PCP-Related Computational Reductions in Coq (LearnAut) Decision problems for Clark-congruential languages
contextual equivalence	(GS) Automata Theory and Game Semantics (ITP) A Formal Equational Theory for Call-by-Push-Value (WPTE) Automating the Diagram Method to Prove Correctness of Program Transformations
contextual fibrancy	(HoTT/UF) Robust Notions of Contextual Fibrancy
contextuality	(LICS) Logical paradoxes in quantum computation
Continuation Semantics	(Domains13) Abstractness of Continuation Semantics for Asynchronous Concurrency
Continuous computation	(CL&C) Some ideas on cut-elimination for cyclic arithmetic proofs
Continuous delivery	(Overture) Integrating VDM-SL into the continuous delivery pipelines of cloud-based software
continuous systems	(FM) Vector Barrier Certificates and Comparison Systems
continuous validation	(Overture) Enhancing Testing of VDM-SL models
continuous valuation	(Domains13)
Continuous-time Markov chain	(CAV) Monitoring CTMCs By Multi-Clock Timed Automata
contract-based verification	(AVOCS) Climbing the Software Assurance Ladder - Practical Formal Verification for Reliable Software
contractibility	(FSCD) Proof nets for bi-intuitionistic linear logic
Contraction	(TYDI) Proof complexity of deep inference: a survey
control	(VaVAS) Work-in-Progress: Adaptive Neighborhood Resizing for Stochastic Reachability in Distributed Flocking
control flow	(MLP) Deep Learning On Code with an Unbounded Vocabulary
control improvisation	(CAV) Reactive Control Improvisation
Control parameters	(ITP) Understanding Parameters of Deductive Verification: an Empirical Investigation of KeY
Control-Flow Refinment	(WST) Control-Flow Refinement via Partial Evaluation
Controlled Natural Language	(ICLP-DC) Knowledge Authoring and Question Answering via Controlled Natural Language (UITP) Text-Orientated Formal Mathematics (ICLP) Natural Language Generation From Ontologies: Application Paper
Controlled Natural Languages	(ICLP) Specifying and Verbalising Answer Set Programs in Controlled Natural Language
controller synthesis	(DS-FM) Heuristic-Based GR(1) Assumptions Refinement (CAV) Controller Synthesis Made Real: Reach-avoid Specifications and Linear Dynamics (FM) Optimal and Robust Controller Synthesis Using Energy Timed Automata with Uncertainty
controller system	(MoRe) Comfort and Energy Optimization for Floor Heating Systems
conversion algorithm	(CAV) A Direct Encoding for NNC Polyhedra
convex polyhedra	(CAV) A Direct Encoding for NNC Polyhedra
Cooperative Scheduling	(FM) Deadlock Detection for Actor-based Coroutines
Coq	(FSCD) Cumulative Inductive Types in Coq (LFMTP) Sharing a library between proof assistants: reaching out to the HOL family (FM) Modular Verification of Programs with Effects and Effect Handlers in Coq (AVOCS) Proof-Oriented Design of a Separation Kernel with Minimal Trusted Computing Base (Coq) Towards a formalization of the guard condition (Coq) Classical Analysis with Coq (Coq) Procrastination, A proof engineering technique (Coq) Teaching Your Rooster to Crow in C (ITP) A Formal Proof of the Minor-Exclusion Property for Treewidth-Two Graphs (ITP) Formalizing Implicative Algebras in Coq (ITP) Towards Certified Meta-Programming with Typed Template-Coq (ITP) A Coq Formalisation of SQL’S Execution Engines (ITP) Reification by Parametricity (VSTTE) A Java bytecode formalisation (LOLA) Towards a library of formalised undecidable problems in Coq: The undecidability of intuitionistic linear logic
Coq library	(Coq) Preliminary Report on the Yalla Library
Coq proof assistant	(FCS) A Study on the Preservation on Cryptographic Constant-Time Security in the CompCert Compiler
Core SAT	(SAT) Chronological Backtracking
Corecursion	(HCVS) Towards Coinductive Theory Exploration in Horn Clause Logic: Extended Abstract
correctness	(REFINE) Correctness of Concurrent Objects under Weak Memory Models (WPTE) Automating the Diagram Method to Prove Correctness of Program Transformations
Correctness by extraction	(ITP) Proof Pearl: Constructive Extraction of Cycle Finding Algorithms
correctness criteria	(FSCD) Unique perfect matchings and proof nets (Linearity/TLLA) Coherent interaction graphs: a nondeterministic geometry of interaction for MLL
Correctness Enhancement	(REFINE) Programming Without Refinement
Correctness proof	(HCVS) A simple functional presentation and an inductive correctness proof of the Horn algorithm
Correctness proofs	(VSTTE) Program Verification in the Presence of I/O: Semantics, verified library routines, and verified applications
Correspondence theory	(LICS) A van Benthem Theorem for Fuzzy Modal Logic
Cost Analysis	(WST) Inference of Linear Upper-Bounds on the Expected Cost by Solving Cost Relations (WST) Control-Flow Refinement via Partial Evaluation
Cost bounded reachability	(MoRe) Multiple Objectives and Cost Bounds in MDP
Cost relations	(WST) Inference of Linear Upper-Bounds on the Expected Cost by Solving Cost Relations
counter-example	(FM) Producing Explanations for Rich Logics
CounterExample Guided Inductive Synthesis	(SYNT) Safe, Automated and Formal Synthesis of Digital Controllers for Continuous Plants
Counterexample-guided Algorithms	(SAT) Effective use of SMT solvers for Program Equivalence Checking through Invariant Sketching and Query Decomposition
Counterexample-Guided Inductive Synthesis	(CAV) Safety-Aware Apprenticeship Learning
counterexamples	(ARQNL) Evidence Extraction from Parameterised Boolean Equation Systems (VSTTE) Executable Counterexamples in Software Model Checking
countermodel construction	(EICNCL) A Forward Calculus for Countermodel Construction in IPL
counting classes	(LICS) Model-Theoretic Characterizations of Boolean and Arithmetic Circuit Classes of Small Depth
Courcelle's Theorem	(LaSh) Courcelle’s Theorem – A Game-Theoretic Approach
Covering Theory	(HoTT/UF) Cohesive Covering Theory
CPS translation	(Linearity/TLLA) From Linear Logic to Cyclic Sharing
CR-Prolog	(ICLP-DC) Translating P-log, LP^{MLN}, LPOD, and CR-Prolog2 into Standard Answer Set Programs
CR-Prolog2	(ICLP) Translating LPOD and CR-Prolog2 into Standard Answer Set Programs
Crafted benchmarks	(POS) Seeking Practical CDCL Insights from Theoretical SAT Benchmarks (SAT) Using Combinatorial Benchmarks to Probe the Reasoning Power of Pseudo-Boolean Solvers
Craig Interpolation	(IJCAR) Efficient Interpolation for the Theory of Arrays
Crime tracing	(GraMSec) Tendrils of Crime: Visualizing the Diffusion of Stolen Bitcoins
critical complexity region	(RCRA) Replaceability for constraint satisfaction problems: Algorithms, Inferences, and Complexity Patterns
critical pair	(FSCD) Confluence of Prefix-Constrained Rewrite Systems
critical software assurance	(AVOCS) Climbing the Software Assurance Ladder - Practical Formal Verification for Reliable Software
Critical Systems	(AVOCS) Formal Verification of Synchronisation, Gossip and Environmental Effects for Wireless Sensor Networks
CRN	(VEMDP) Bayesian Verification of Chemical Reaction Networks
CRN equivalence	(VEMDP) Equivalence of chemical reaction networks in a CRN-to-DNA compiler framework.
cross-fertilization	(LICS) Sound up-to techniques and Complete abstract domains
cross-section property	(HDRA) String data structures for Chinese monoids
crowds	(FM) An Algebraic Approach for Reasoning About Information Flow
cryptographic CNF instances	(POS) CryptoMiniSat Parameter-Optimization for Solving Cryptographic Instances
cryptographic constant-time	(CSF) Secure compilation of side-channel countermeasures: the case of cryptographic “constant-time”
Cryptographic protocol	(CAV) The DEEPSEC prover
Cryptographic protocols	(FCS) Homomorphisms and Minimality for Enrich-by-Need Security Analysis
cryptographic schemes	(CSF) Self-Guarding Cryptographic Protocols against Algorithm Substitution Attacks
Cryptographic software	(CAV) SCInfer: Refinement-based Verification of Software Countermeasures against Side-Channel Attacks
Cryptography	(CAV) Continuous formal verification of Amazon s2n
CSP	(IJCAR) Complexity of Combinations of Qualitative Constraint Satisfaction Problems
CSP Solver	(LPOP) A Picat-based XCSP Solver - from Parsing, Modeling, to SAT Encoding
cubical sets	(FSCD) Internal Universes in Models of Homotopy Type Theory (HoTT/UF) The definitional symmetric cubical structure of types in type theory with equality defined by abstraction over an interval (HoTT/UF) Ordered Cubes
cubical type theory	(LICS) On Higher Inductive Types in Cubical Type Theory (LICS) Degrees of Relatedness - A Unified Framework for Parametricity, Irrelevance, Ad Hoc Polymorphism, Intersections, Unions and Algebra in Dependent Type Theory (HoTT/UF) The definitional symmetric cubical structure of types in type theory with equality defined by abstraction over an interval (HoTT/UF) Cubical Computational Type Theory (HoTT/UF) Cubical Assemblies and the Independence of the Propositional Resizing Axiom (HoTT/UF) Dependent Right Adjoint Types
Curry-Howard	(LICS) Classical realizability as a classifier for nondeterminism (CL&C) On Natural Deduction for Herbrand Constructive Logics III: The Strange Case of the Intuitionistic Logic of Constant Domains
Curry-Howard correspondence	(WiL) A New Linear Logic for Deadlock-Free Session-Typed Processes (Talk Abstract) (SAT) Local Soundness for QBF Calculi
Curry-Howard isomorphism	(RCRA) Shaving with Occam's Razor: Deriving Minimalist Theorem Provers for Minimal Logic
cut elimination	(ITRS) Intersection Subtyping with Constructors (LICS) Unification nets: canonical proof net quantifiers
cut-elimination	(CL&C) Some ideas on cut-elimination for cyclic arithmetic proofs (CL&C) Fast cut-elimination using proof terms: an empirical study
Cut-elimination theorem	(EICNCL) Sequent Calculi for Logic that Includes an Infinite Number of Modalities
Cutting and Packing	(RCRA) An Enhanced Genetic Algorithm with the BLF2G Guillotine Placement Heuristic for the Orthogonal Cutting-Stock Problem
cutting planes	(PC) Branching Program Complexity of Canonical Search Problems and Proof Complexity of Formulas (POS) Divide and Conquer: Towards Faster Pseudo-Boolean Solving (SAT) Using Combinatorial Benchmarks to Probe the Reasoning Power of Pseudo-Boolean Solvers (SAT) In Between Resolution and Cutting Planes: A Study of Proof Systems for Pseudo-Boolean SAT Solving
Cyber Security	(PRUV) Leveraging Probabilistic Existential Rules for Adversarial Deduplication
Cyber-Physical system	(FM) IPL: An Integration Property Language for Multi-Model Cyber-Physical Systems (FM) Towards `Verifying' a Water Treatment System
cyber-physical systems	(FM) Falsification of Cyber-Physical Systems Using Deep Reinforcement Learning (LICS) A Hybrid, Dynamic Logic for Hybrid-Dynamic Information Flow
Cybercrime	(GraMSec) Tendrils of Crime: Visualizing the Diffusion of Stolen Bitcoins
Cycle finding	(ITP) Proof Pearl: Constructive Extraction of Cycle Finding Algorithms
Cyclic graphs	(TERMGRAPH) Drags: an algebraic framework for graph rewriting
cyclic induction	(CL&C) Validating Back-links of FOL-ID Cyclic Pre-proofs
cyclic lambda calculus	(Linearity/TLLA) From Linear Logic to Cyclic Sharing
cyclic proof	(ADSL) Cyclic Theorem Prover for Separation Logic by Magic Wand
Cyclic proofs	(PARIS) Transitive Closure Logic: Infinitary and Cyclic Proof Systems (PARIS) On the Logical Complexity of Cyclic Arithmetic (AVOCS) An Entailment Checker for Separation Logic with Inductive Definitions (ADSL) Labelled Cyclic Proofs for Separation Logic (CL&C) Some ideas on cut-elimination for cyclic arithmetic proofs
cyclic sharing	(Linearity/TLLA) From Linear Logic to Cyclic Sharing
Cyclic term-graps	(FSCD) Term-Graph Anti-Unification
Cylindrical Algebraic Decomposition	(SCSC) RP: Towards Incremental Cylindrical Algebraic Decomposition in Maple (SCSC) RP: Evaluation of Equational Constraints for CAD in SMT Solving
D
D-optimaldesigns	(SCSC) Hard Combinatorial Problems: A Challenge for Satisfiability
Daniell-Kolmogorov theorem	(Domains13)
data compression	(IWC) Complete Axiom System of Cluster Algebra
Data Driven modelling	(VEMDP) Bayesian Verification of Chemical Reaction Networks
data flow	(VSTTE) A Tree-Based Approach to Data Flow Proofs
Data Races	(LICS) An Asynchronous Soundness Theorem for Concurrent Separation Logic
Data words	(LICS) Logics for Word Transductions with Synthesis (LICS) Playing with Repetitions in Data Words Using Energy Games
Data-structures	(ICLP) Shape Neutral Analysis of Graph-based Data-structures
database theory	(LICS) Can One Escape Red Chains? Regular Path Queries Determinacy is Undecidable.
Databases	(ITP) A Coq Formalisation of SQL’S Execution Engines
Datalog	(LPOP) Security Policies in Constraint Handling Rules (ASPOCP) Datalog for Static Analysis Involving Logical Formulae (IJCAR) Efficient Model Construction for Horn Logic with VLog: System Description (ICLP) Declarative Algorithms in Datalog with Aggregates: user-friendly formal semantics conducive to performance and scalability
datatypes	(IJCAR) Datatypes with Shared Selectors (IJCAR) Superposition with Datatypes and Codatatypes (ITP) Boosting the Reuse of Formal Specifications (ITP) Relational Parametricity and Quotient Preservation for Modular (Co)Datatypes
de Groot duality	(Domains13) Applications of entailments: de Groot duality
Deadlock	(FM) A lightweight deadlock analysis technique of object-oriented programs
Deadlock Analysis	(AVOCS) Detecting Deadlocks in Formal System Models with Condition Synchronization
Deadlock Detection	(FM) Deadlock Detection for Actor-based Coroutines (FM) Dynamic Symbolic Verification of MPI Programs
deadlock-freedom	(WiL) A New Linear Logic for Deadlock-Free Session-Typed Processes (Talk Abstract)
Decentralized planning	(FM) Multi-Robot LTL Planning Under Uncertainty
Decidability	(FM) The Compound Interest in Relaxing Punctuality (SYNT) On the Expressiveness of HyperLTL Synthesis (LICS) Allegories: decidability and graph homomorphisms (ADSL) The Complexity of Prenex Separation Logic with One Selector (MSFP) Formalizing Constructive Quantifier Elimination in Agda (LearnAut) Decision problems for Clark-congruential languages
decision	(IJCAR) FORT 2.0
Decision making	(VaVAS) Towards a verifiable decision making framework for self-driving vehicles
Decision Model and Notation (DMN)	(LPOP) Logic-based Methods for Software Engineers and Business People
Decision Modeling	(LPOP) Logic-based Methods for Software Engineers and Business People
Decision Modelling	(ICLP) Application of Logic-Based Methods to Machine Component Design
decision procedure	(CAV) Android Stack Systems (LaSh) Lazy Automata Techniques for WS1S (LaSh) A Derivative-Based Decision Procedure for WS1S (IJCAR) A Separation Logic with Data: Small Models and Automation (IJCAR) Deciding the First-Order Theory of an Algebra of Feature Trees with Updates (IJCAR) Probably Half True: Probabilistic Satisfiability over Lukasiewicz Infinitely-valued Logic (ADSL) Sloth: Separation Logic and Theories via Small Models
Decision Procedures	(SCSC) EA: Wrapping Computer Algebra is Surprisingly Successful for Non-Linear SMT (LaSh) Decidable Linear Tree Constraints (IJCAR) Datatypes with Shared Selectors (IJCAR) A Why3 framework for reflection proofs and its application to GMP's algorithms
decisiveness	(MoRe) Stochastic o-minimal hybrid systems
Declarative Algorithms	(RCRA) Shaving with Occam's Razor: Deriving Minimalist Theorem Provers for Minimal Logic (ICLP) Declarative Algorithms in Datalog with Aggregates: user-friendly formal semantics conducive to performance and scalability
declarative programming	(LPOP) A software system should be declarative except where it interacts with the real world (FM) Variant Analysis with QL (PRUV) A Model-Theoretic View on Preferences in Declarative Specifications of Search Problems
Declarative Prover	(ThEdu) Students' Proof Assistant (SPA)
declassification	(CSF) Assuming you know: epistemic semantics of relational annotations for expressive flow policies
decoupled approach	(CAV) Controller Synthesis Made Real: Reach-avoid Specifications and Linear Dynamics
decreasing diagrams	(FSCD) Decreasing diagrams with two labels are complete for confluence of countable systems
deduction	(WPTE) Automating the Diagram Method to Prove Correctness of Program Transformations
Deductive interactive program verification	(UITP) Adding Text-Based Interaction to a Direct-Manipulation Interface for Program Verification -- Lessons Learned
Deductive program verification	(IJCAR) A Why3 framework for reflection proofs and its application to GMP's algorithms
Deductive programs verification	(SMT) Alt-Ergo 2.2
deductive verification	(CAV) Eager Abstraction for Symbolic Model Checking (F-IDE) Experience Report on Formally Verifying Parts of OpenJDK's API with KeY (F-IDE) Lightweight Interactive Proving inside an Automatic Program Verifier (ITP) Understanding Parameters of Deductive Verification: an Empirical Investigation of KeY (VSTTE) Practical Methods for Reasoning about Java 8's Functional Programming Features
Dedukti	(LFMTP) Sharing a library between proof assistants: reaching out to the HOL family (ITP) Tactics and Certificates in Meta Dedukti
Deduplication	(PRUV) Leveraging Probabilistic Existential Rules for Adversarial Deduplication
deep embedding	(Coq) Preliminary Report on the Yalla Library
deep inference	(TYDI) Deep-Inference Intersection Types (TYDI) Proof complexity of deep inference: a survey (TYDI) Deep Inference, Herbrand's Theorem and Expansion Proofs (TYDI) Truely Concurrent Processes in the Calculus of Structures (TYDI) An introduction to deep inference (TYDI) Some incoherent musings on deep inference and combinatorial proofs
Deep Learning	(MLP) Deep Learning On Code with an Unbounded Vocabulary (MLP) Splitting source code identifiers using Bidirectional LSTM Recurrent Neural Network
Deficiency	(SAT) Minimal unsatisfiability and minimal strongly connected digraphs
definability	(LICS) Definable decompositions for graphs of bounded linear cliquewidth
Definable	(GS) A definable game semantics for the linear quantum lambda-calculus
definable while programs	(LICS) On computability and tractability for infinite sets
delay differential equations	(CAV) Inner and Outer Approximating Flowpipes for Delay Differential Equations
Delta-completeness	(CAV) Delta-Decision Procedures for Exists-Forall Problems over the Reals
denotation	(LICS) Every λ-Term is Meaningful for the Infinitary Relational Model
denotational model	(Linearity/TLLA) A semantic conjecture on second-order MLL and its complexity consequences (work in progress)
denotational semantics	(FSCD) Call-by-name Gradual Type Theory (FSCD) The clocks they are adjunctions. Denotational semantics for Clocked Type Theory (PARIS) What makes guarded types tick? (Isabelle) Using Isabelle/UTP for the Verification of Sorting Algorithms: A Case Study (LICS) Extensional and Intensional Semantic Universes: A Denotational Model of Dependent Types (LICS) Probabilistic stable functions on discrete cones are power series. (LICS) Boolean-Valued Semantics for Stochastic Lambda-Calculus (Domains13) Algebra semantics of recursive computation types (Domains13) Invited Talk: A Brief History of Denotational Semantics (Linearity/TLLA) The Bang Calculus and the Two Girard's Translations (CL&C) A Denotational Model of the Typed Lambda-Mu Calculus (HOR) The next 700 (type-theoretical) denotational models ? (HOR) Refining Properties of Filter Models: Sensibility, Approximability and Reducibility (LOLA) Heaps denote finitely partitioned trees (LOLA) Denotational Event structure for relaxed memory
deontic logis	(ARQNL) System Demonstration: The Higher-Order Prover Leo-III
Dependant Types	(WST) Termination of Lambda-Pi modulo rewriting using the size-change principle
dependence maps	(SR) Dependences in Strategy Logic
Dependency	(AVOCS) Detecting Deadlocks in Formal System Models with Condition Synchronization
dependency graph	(ASPOCP) Syntactic Conditions for Antichain Property in Consistency Restoring Prolog
dependent choice	(LICS) A sequent calculus with dependent types for classical arithmetic
dependent product types	(LICS) Dialectica models of type theory
Dependent Refinement Types	(CAV) Propositional Dynamic Logic for Higher-Order Functional Programs (LICS) A Fixpoint Logic and Dependent Effects for Temporal Property Verification
dependent temporal effects	(LICS) A Fixpoint Logic and Dependent Effects for Temporal Property Verification
dependent type theory	(FSCD) Internal Universes in Models of Homotopy Type Theory (LICS) Dialectica models of type theory (NLCS) Paychecks, Presupposition, and Dependent Types (HoTT/UF) Algebraic models of dependent type theory
dependent types	(ICLP-DC) Proof-relevant resolution for elaboration of programming languages (LICS) Extensional and Intensional Semantic Universes: A Denotational Model of Dependent Types (LICS) A sequent calculus with dependent types for classical arithmetic (LICS) Guarded Computational Type Theory (ITP) Tactics and Certificates in Meta Dedukti (ITP) Verified Timing Transformations in Synchronous Circuits with LambdaPi-Ware (Linearity/TLLA) Substructural Calculi with Dependent Types (ICLP) Proof-relevant Horn Clauses for Dependent Type Inference and Term Synthesis
dependently typed programming	(MSFP) Everybody's Got To Be Somewhere (ITP) Verified Timing Transformations in Synchronous Circuits with LambdaPi-Ware
derivational complexity	(WST) Embracing Infinity - Termination of String Rewriting by Almost Linear Weight Functions
derivationism	(WiL) Can every real proof be represented by a formal proof? The Hilbert-Gentzen thesis
Deriving Reliable Programs	(REFINE) Programming Without Refinement
Description logic	(LICS) A van Benthem Theorem for Fuzzy Modal Logic (IJCAR) Enumerating Justifications using Resolution
description logics	(IJCAR) FAME: An Automated Tool for Semantic Forgetting in Expressive Description Logics (PRUV) Reasoning about exceptions in ontologies: from the lexicographic closure to the skeptical closure (FCS) An Expressive, Flexible and Uniform Logical Formalism for Attribute-based Access Control
descriptive complexity	(LCC) Completeness in the Second Level of the Polynomial Time Hierarchy through Syntactic Properties (LICS) Model-Theoretic Characterizations of Boolean and Arithmetic Circuit Classes of Small Depth (LICS) A modal mu perspective on solving parity games in quasipolynomial time.
design automation	(CAV) ADAC: Automated Design of Approximate Circuits
design by contract	(F-IDE) Experience Report on Formally Verifying Parts of OpenJDK's API with KeY (ITP) Understanding Parameters of Deductive Verification: an Empirical Investigation of KeY
Design Space Exploration	(Overture) Design Space Exploration for Secure Building Control
destructors	(LOLA) A resource modality for RAII
determinacy	(LICS) Can One Escape Red Chains? Regular Path Queries Determinacy is Undecidable.
Deterministic Automata	(CAV) Rabinizer 4: From LTL to Your Favourite Deterministic Automaton (LICS) One Theorem to Rule Them All: A Unified Translation of LTL into ω-Automata
Deterministic Parity Automaton	(CAV) Strix: Explicit Reactive Synthesis Strikes Back!
DFA	(WiL) First-Order vs. Second-Order Encodings for LTLf-to-Automata Translation
Diagrammatic Reasoning	(LICS) Diagrammatic Reasoning beyond Clifford+T Quantum Mechanics (LICS) A Complete Axiomatisation of the ZX-Calculus for Clifford+T Quantum Mechanics
dialectica category	(Linearity/TLLA) On the Lambek Calculus with an Exchange Modality
Dialectica interpretation	(LICS) Dialectica models of type theory
diamond lemma	(IWC) The diamond lemma for free modules
diffeological spaces	(Domains13) Diffeological Spaces and Semantics for Differential Programming
differential dynamic logic	(LICS) Differential Equation Axiomatization: The Impressive Power of Differential Ghosts
differential equation axiomatization	(LICS) Differential Equation Axiomatization: The Impressive Power of Differential Ghosts
Differential Equations	(VEMDP) Conservative approximations of polymers (LICS) A Logical Account for Linear Partial Differential Equations
differential game logic	(IJCAR) Uniform Substitution for Differential Game Logic
differential ghosts	(LICS) Differential Equation Axiomatization: The Impressive Power of Differential Ghosts
Differential Linear Logic	(LICS) A Logical Account for Linear Partial Differential Equations (Linearity/TLLA) Models of Linear Logic based on the Schwartz epsilon product (Linearity/TLLA) Towards a Functional Language for Species of Structures
differential programming	(Domains13) Diffeological Spaces and Semantics for Differential Programming
Digital libraries	(LICS) Computability Beyond Church-Turing via Choice Sequences
Diller-Nahm variant	(LICS) Dialectica models of type theory
Diophantine equations	(Isabelle) Hilbert Meets Isabelle: Formalisation of the DPRM Theorem in Isabelle
direct-manipulation interaction	(UITP) Adding Text-Based Interaction to a Direct-Manipulation Interface for Program Verification -- Lessons Learned
directed complete	(Domains13) Invited Talk: Topology and Domain Theory Interfaces
Discounted-sum determinization	(CAV) Automata vs Linear-Programming Discounted-Sum Inclusion
Discounted-sum inclusion	(CAV) Automata vs Linear-Programming Discounted-Sum Inclusion
discrete polymorphism	(ITRS) Gradual Intersection Types
Discrete-Event	(Overture) Overture FMU: Export VDM-RT Models as Tool-Wrapper FMUs
discrete-time linear system	(CAV) Controller Synthesis Made Real: Reach-avoid Specifications and Linear Dynamics
Display calculi	(EICNCL) Effective Translations between Display and Labelled Proofs for Tense Logics
display map category	(LICS) Dialectica models of type theory
distance bounding protocols	(FCS) Proving physical proximity using symbolic models
Distance fraud	(FCS) Statistical Model Checking of Guessing and Timing Attacks on Distance-bounding Protocols
Distance-bounding protocols	(FCS) Statistical Model Checking of Guessing and Timing Attacks on Distance-bounding Protocols
distribute consensus protocols	(CAV) Eager Abstraction for Symbolic Model Checking
distributed autonomous systems	(VaVAS) Towards a Hierarchical-Control Architecture for Distributed Autonomous Systems (Extended Abstract - Paper)
distributed computing	(CAV) Peregrine: A Tool for the Analysis of Population Protocols
distributed concurrent systems	(FM) SDN-Actors: Modeling and Verification of SDN Programs
Distributed Protocols	(HCVS) Declarative Parameterized Verification of Topology-sensitive Distributed Protocols
distributed systems	(FM) Stepwise Development and Model Checking of a Distributed Interlocking System - using RAISE (ICLP) MASP-Reduce: a proposal for distributed computation of stable models
Distribution based objectives	(LICS) Distribution-based objectives for Markov Decision Processes
distributive laws	(MSFP) Some No-Go Theorems for Distributive Laws (extended abstract)
division	(POS) Divide and Conquer: Towards Faster Pseudo-Boolean Solving
DLVSYSTEM srl	(LPOP) Invited Talk: On the Development of Industrial Applications with ASP
DMN	(ICLP) Application of Logic-Based Methods to Machine Component Design
DNA algorithmic self-assembly	(VEMDP) Computational Approaches for the Programmed Assembly of Nanocellulose Meshes
DNF	(LearnAut) Toward Learning Boolean Functions from Positive Examples
Dolev-Yao Attacker	(CAV) Model checking indistinguishability of randomized security protocols
domain	(Domains13)
domain equation	(Domains13) Algebra semantics of recursive computation types
domain specific languages	(ITP) Verified Timing Transformations in Synchronous Circuits with LambdaPi-Ware
domain theory	(Domains13) Domain Theory for Intensional Computation (Domains13) Invited Talk: A Brief History of Denotational Semantics (Domains13) Invited Talk: Topology and Domain Theory Interfaces
domain-level strand displacement	(VEMDP) Equivalence of chemical reaction networks in a CRN-to-DNA compiler framework.
domain-specific formal languages	(F-IDE) Isabelle/jEdit as IDE for domain-specific formal languages and informal text documents
Domain-specific languages	(CSF) Enforcing ideal-world leakage bounds in real-world secret sharing MPC frameworks
dominance	(SR) Beyond admissibility: Dominance between chains of strategies
Double Description method	(CAV) A Direct Encoding for NNC Polyhedra
Double negation	(LICS) Around Classical and Intuitionistic Linear Logics
Double-pushout graph transformation	(TERMGRAPH) Semantics-Preserving DPO-Based Term Graph Rewriting
Double-pushout rewriting	(LICS) Rewriting with Frobenius
downward closures	(LICS) Separability by piecewise testable languages and downward closures beyond subwords
DPRM Theorem	(Isabelle) Hilbert Meets Isabelle: Formalisation of the DPRM Theorem in Isabelle
drat	(IJCAR) Extended Resolution Simulates DRAT
DRAT proofs	(POS) Two flavors of DRAT
DSL	(Coq) Teaching Your Rooster to Crow in C
dual-rail encoding	(PC) On Dual-Rail Based MaxSAT Solving
duality	(LICS) Riesz Modal Logic with Threshold Operators
dualized proof system	(CL&C) Towards a Dualized Sequent Calculus with Canonicity
Dynamic analysis	(CAV) Quasi-Optimal Partial Order Reduction
Dynamic applications	(ICLP) Experimenting with robotic intra-logistics domains
Dynamic data structures	(CAV) Let this Graph be your Witness! An Attestor for Verifying Java Pointer Programs
Dynamic domains	(LPOP) How to upgrade ASP for true dynamic modelling and solving?
dynamic epistemic logic	(ITP) Software Tool Support for Modular Reasoning in Modal Logics of Actions
Dynamic language	(CAV) Nagini: A Static Verifier for Python
Dynamic Languages	(CAV) MaxSMT-Based Type Inference for Python 3
Dynamic Logic	(FM) The Compound Interest in Relaxing Punctuality (LICS) A Hybrid, Dynamic Logic for Hybrid-Dynamic Information Flow
Dynamic nets	(LICS) Concurrency and Probability: Removing Confusion, Compositionally
Dynamic Partial Order Reduction	(CAV) Constrained Dynamic Partial Order Reduction
Dynamic Programming	(LaSh) Solving #SAT by Parameterized Algorithms: Exploiting Small Treewidth (LaSh) Declarative Dynamic Programming with Inverse Coupled Rewrite Systems (MLP) Splitting source code identifiers using Bidirectional LSTM Recurrent Neural Network (ITP) Verified Memoization and Dynamic Programming
Dynamic Verification	(FM) Dynamic Symbolic Verification of MPI Programs
Dynamical Systems	(Linearity/TLLA) Entropy and Complexity Lower Bounds
E
e-voting	(CSF) Alethea: A Provably Secure Random Sample Voting Protocol
EasyCrypt	(CSF) Machine-checked proofs for electronic voting: privacy and verifiability for Belenios (CSF) Computer-aided proofs for multiparty computation with active security (CSF) Formal Security Proof of CMAC and its Variants
Eckmann-Hilton morphism	(HDRA) Towards a fully formalized definition of syllepsis in weak higher categories
Economic Reasoning	(SCSC) RP: Non-linear Real Arithmetic Benchmarks derived from Automated Reasoning in Economics
Economics	(ITP) Towards Formal Foundations for Game Theory (Short Paper)
effectful bisimilarity	(LICS) Quantitative Behavioural Reasoning for Higher-order Effectful Programs: Applicative Distances
Effective translations	(EICNCL) Effective Translations between Display and Labelled Proofs for Tense Logics
Efficiency	(UNIF) Efficiency of a good but not linear nominal unification algorithm
Efficient Attractor	(PLR) An Efficient Zielonka's Algorithm for Parallel Parity Games
efficient computation	(ICLP) Shared aggregate sets in answer set programming
Egraph	(SMT) Centralizing Equality Reasoning in MCSAT
Eilenberg-Moore Category	(FSCD) Lifting Coalgebra Modalities and IMELL Model Structure to Eilenberg-Moore Categories
elaboration	(ICLP-DC) Proof-relevant resolution for elaboration of programming languages
Eldarica	(WPTE) Verification of Ada Programs with AdaHorn
Electronic Voting	(CAV) Model checking indistinguishability of randomized security protocols
elementary linear logic	(Linearity/TLLA) A semantic conjecture on second-order MLL and its complexity consequences (work in progress)
elementary semantics	(SR) Dependences in Strategy Logic
ellipsoid method	(LICS) Definable Ellipsoid Method, Sums-of-Squares Proofs, and the Isomorphism Problem
embedded domain specific language	(GraMSec) On Linear Logic, Functional Programming, and Attack Trees
Embedded systems	(FM) Resource-aware Design for Reliable Autonomous Applications with Multiple Periods
Empirical evaluation	(CAV) Automata vs Linear-Programming Discounted-Sum Inclusion
EMVCo	(Overture) VDM at large: analysing the EMV Next Generation Kernel
energy games	(LICS) Playing with Repetitions in Data Words Using Energy Games
energy-efficient computing	(CAV) ADAC: Automated Design of Approximate Circuits
engineering mathematics	(ThEdu) Lucas Interpretation from Programmers’ Perspective
enriched categories	(Domains13) Higher-dimensional categories: recursion on extensivity
enriched category theory	(LICS) Enriching a Linear/Non-linear Lambda Calculus: A Programming Language for String Diagrams
entailment check	(ADSL) Cyclic Theorem Prover for Separation Logic by Magic Wand
entailment relation	(Domains13) Applications of entailments: de Groot duality
Entitity Resolution	(PRUV) Leveraging Probabilistic Existential Rules for Adversarial Deduplication
epistemic logic	(FM) Timed Epistemic Knowledge Bases for Social Networks (ITP) The Coinductive Formulation of Common Knowledge (EICNCL) Hypersequent calculus for the logic of conditional belief: preliminary results
Epistemic Logic Program Solvers	(ASPOCP) A Survey of Advances in Epistemic Logic Program Solvers
Epistemic Logic Programs	(ASPOCP) selp: A Single-Shot Epistemic Logic Program Solver (ASPOCP) A Survey of Advances in Epistemic Logic Program Solvers (ICLP) Epistemic Logic Programs with World View Constraints
Epistemic Negations	(ASPOCP) A Survey of Advances in Epistemic Logic Program Solvers
epistemic specification	(ICLP) Introspecting Preferences In Answer Set Programming
Epistemic Specifications	(ASPOCP) A Survey of Advances in Epistemic Logic Program Solvers (ICLP) Epistemic Logic Programs with World View Constraints
equality by abstraction over an interval	(HoTT/UF) The definitional symmetric cubical structure of types in type theory with equality defined by abstraction over an interval
equational constraints	(SCSC) RP: Evaluation of Equational Constraints for CAD in SMT Solving
equational logic	(LICS) An algebraic theory of Markov processes (IJCAR) Efficient encodings of first-order Horn formulas in equational logic
equational rewriting	(UNIF) Knowledge Problems in Equational Extensions of Subterm Convergent Theories
Equational theories	(PC) Towards theories for positive polynomial time and monotone proofs with extension (FSCD) Fixed-Point Constraints for Nominal Equational Unification (FSCD) Higher-Order Equational Pattern Anti-Unification (UNIF) Towards Generalization Methods for Purely Idempotent Equational Theories
equational theory	(UNIF) Unification based on generalized embedding (ITP) A Formal Equational Theory for Call-by-Push-Value (LOLA) A graph-rewriting perspective of the beta-law
Equilibrium Logic	(ICLP) Functional ASP with Intensional Sets; Application to Gelfond-Zhang Agreggates
Equivalence	(LearnAut) Decision problems for Clark-congruential languages (FCS) A Homotopical Approach to Cryptography
equivalence relations	(LICS) Unary negation fragment with equivalence relations has the finite model property
erasure	(LICS) Degrees of Relatedness - A Unified Framework for Parametricity, Irrelevance, Ad Hoc Polymorphism, Intersections, Unions and Algebra in Dependent Type Theory
Erin	(POS) Stedman and Erin Triples encoded as a SAT Problem
Erin Triples	(POS) Stedman and Erin Triples encoded as a SAT Problem
Erlang	(HCVS) Metaprogramming and symbolic execution for detecting runtime errors in Erlang programs
essential unification	(UNIF) Unification based on generalized embedding
essentially algebraic theories	(Domains13) Invited Talk: A domain theory for quasi-Borel spaces and statistical probabilistic programming
Ethereum	(SMT) SMT-based Compile-time Verification of Safety Properties for Smart Contracts (CSF) KEVM: A Complete Formal Semantics of the Ethereum Virtual Machine (VSTTE) Towards verification of Ethereum smart contracts: a formalization of core of Solidity
Evaluable Functions	(ICLP) Functional ASP with Intensional Sets; Application to Gelfond-Zhang Agreggates
Evaluation	(POS) Seeking Practical CDCL Insights from Theoretical SAT Benchmarks (POS) The Effect of Scrambling CNFs
Event Calculus	(ICLP) Learning Commonsense Knowledge through Interactive Dialogue
Event structures	(GS) Continuous probability distributions in concurrent games (LICS) Extensional and Intensional Semantic Universes: A Denotational Model of Dependent Types (LICS) The concurrent game semantics of Probabilistic PCF (LOLA) Denotational Event structure for relaxed memory
evidential verification	(FM) Evidential and Continuous Integration of Software Verification Tools
Evolution systems	(VEMDP) Conservative approximations of polymers
exceptions	(LOLA) A resource modality for RAII
exchange	(Linearity/TLLA) On the Lambek Calculus with an Exchange Modality
exchange rule	(Coq) Preliminary Report on the Yalla Library
Executable Harnesses	(VSTTE) Executable Counterexamples in Software Model Checking
Executable Specifications	(ICLP) Specifying and Verbalising Answer Set Programs in Controlled Natural Language
execution time	(ITRS) Towards a Semantic Measure of the Execution Time in Call-by-Value lambda-Calculus
exhaustive and randomized data generation	(LFMTP) Property-Based Testing of Abstract Machines: an Experience Report
Existential Rules	(IJCAR) Efficient Model Construction for Horn Logic with VLog: System Description (PRUV) Leveraging Probabilistic Existential Rules for Adversarial Deduplication
expander graphs	(PC) Complexity of expander-based reasoning and the power of monotone proofs
expansion proofs	(TYDI) Deep Inference, Herbrand's Theorem and Expansion Proofs (CL&C) Fast cut-elimination using proof terms: an empirical study
expected shortfall	(LICS) Conditional Value-at-Risk for Reachability and Mean Payoff in Markov Decision Processes
Expected Utility	(ITP) Towards Formal Foundations for Game Theory (Short Paper)
experimental analysis	(SAT) Experimenting on Solving Nonlinear Integer Arithmetic with Incremental Linearization
Experiments	(POS) A Problem Meta-Data Library for Research in SAT (ICLP) Improving Candidate Quality of Probabilistic Logic Models
Expert Systems	(ICLP) Application of Logic-Based Methods to Machine Component Design
explainable decision set	(IJCAR) A SAT-Based Approach to Learn Explainable Decision Sets
explanation	(ICLP-DC) Explaining Actual Causation via Reasoning about Actions and Change (FM) Producing Explanations for Rich Logics
explanatory analysis	(FM) To Compose, Or Not to Compose, That is the Question: An Analysis of Compositional State Space Generation
explicit induction reasoning	(PARIS) Useless Explicit Induction Reasoning
explicit substitution	(HOR) Combinatorics of explicit substitutions (extended abstract)
Exposed Datapath Architectures	(ICLP) Optimal Scheduling for Exposed Datapath Architectures with Buffered Processing Units by ASP
expressiveness	(LICS) A Theory of Register Monitors
extended resolution	(IJCAR) Extended Resolution Simulates DRAT
Extension	(NLCS) Propositional Attitude Operators in Homotopy Type Theory
extensive categories	(Domains13) Higher-dimensional categories: recursion on extensivity
extensive category	(LICS) Dialectica models of type theory
extensive-form games	(GraMSec) The Attacker Does not Always Hold the Initiative: Attack Trees with External Refinement
External calculi	(EICNCL) Effective Translations between Display and Labelled Proofs for Tense Logics
extraction	(Coq) What is the Foreign Function Interface of the Coq Programming Language? (ITP) Software Verification with ITPs Should Use Binary Code Extraction to Reduce the TCB (Short Paper)
F
factorization	(SCSC) EA: New in CoCoA-5.2.4 and CoCoALib-0.99570 for SC-Square
fairness	(FM) Encoding fairness in a synchronous concurrent program algebra
Fairness objectives	(CAV) Symbolic Algorithms for Graphs and Markov Decision Processes with Fairness Objectives
false negative rate	(LearnAut) Toward Learning Boolean Functions from Positive Examples
false positive rate	(LearnAut) Toward Learning Boolean Functions from Positive Examples
Fan Theorem	(Domains13) A Brouwerian proof of the Fan Theorem
Fault tolerance	(FM) Resource-aware Design for Reliable Autonomous Applications with Multiple Periods
feasibility of functionals	(LICS) Type-two polynomial-time and restricted lookahead.
feature tree constraints	(IJCAR) Deciding the First-Order Theory of an Algebra of Feature Trees with Updates
fermionic quantum computing	(FSCD) A diagrammatic axiomatisation of fermionic quantum circuits
fibrancy of the function type	(HoTT/UF) Robust Notions of Contextual Fibrancy
fibrant replacement	(HoTT/UF) Robust Notions of Contextual Fibrancy
fibred category theory	(CL&C) The “duality of computation” from a fibrational perspective
field theory	(LCC) Computability over locally finite structures from algebra
Filter	(SAT) XORSAT Set Membership Filters
filter models	(HOR) Refining Properties of Filter Models: Sensibility, Approximability and Reducibility
Finite Automaton	(LaSh) Lazy Automata Techniques for WS1S
Finite model generator	(IJCAR) Investigating the Existence of Large Sets of Idempotent Quasigroups via Satisfiability Testing
finite model property	(LICS) Unary negation fragment with equivalence relations has the finite model property
finite model theory	(LICS) Model-Theoretic Characterizations of Boolean and Arithmetic Circuit Classes of Small Depth (LICS) A universal-algebraic proof of the complexity dichotomy for Monotone Monadic SNP
finite multisets	(Coq) Preliminary Report on the Yalla Library
Finite Semantics	(ICLP) Certified Graph View Maintenance with Regular Datalog
finite sum types	(LICS) Dialectica models of type theory
finitely partitioned trees	(LOLA) Heaps denote finitely partitioned trees
finitization	(PARIS) Local Validity for Circular Proofs in Linear Logic with Fixed Points
Firmware	(CAV) Model Checking Boot Code from AWS Data Centers
first order theories	(Vampire) Experimenting with Theory Instantiation in Vampire
First order transduction	(LICS) Regular and First Order List Functions
first-order combinatorial proofs	(TYDI) Some incoherent musings on deep inference and combinatorial proofs
First-order list function	(LICS) Regular and First Order List Functions
first-order logic	(CAV) Model Generation for Quantified Formulas: A Taint-Based Approach (TYDI) Deep Inference, Herbrand's Theorem and Expansion Proofs (FM) Formal Specification and Verification of Dynamic Parametrized Architectures (Isabelle) Substitutionless First-Order Logic: A Formal Soundness Proof (SMT) What is the Point of an SMT-LIB Problem? (Vampire) Foundations of SPECTRE (PAAR) A Verified Simple Prover for First-Order Logic (PAAR) TFX: The TPTP Extended Typed First-order Form (PAAR) Set of Support for Higher-Order Reasoning (PAAR) Dynamic Strategy Priority: Empower the strong and abandon the weak (LCC) Traversal-invariant definability and Logarithmic-space computation (LICS) Separability by piecewise testable languages and downward closures beyond subwords (IJCAR) Efficient encodings of first-order Horn formulas in equational logic (IJCAR) Superposition with Datatypes and Codatatypes (IJCAR) Formalizing Bachmair and Ganzinger's Ordered Resolution Prover (IJCAR) A Tableaux Calculus for Reducing Proof Size (HoTT/UF) First-order homotopical logic and Grothendieck fibrations (UITP) Partial Regularization of First-Order Resolution Proofs (VSTTE) Extending VIAP to Handle Array Programs (FCS) An Expressive, Flexible and Uniform Logical Formalism for Attribute-based Access Control
first-order logic with inductive definitions	(CL&C) Validating Back-links of FOL-ID Cyclic Pre-proofs
first-order logic with inductive predicates	(PARIS) Useless Explicit Induction Reasoning
First-order multiplicative linear logic	(LICS) Unification nets: canonical proof net quantifiers
First-Order Syntactic Unification	(UNIF) Formalization of First-Order Syntactic Unification
First-order Theory	(IJCAR) Complexity of Combinations of Qualitative Constraint Satisfaction Problems
first-order theory of rewriting	(IJCAR) FORT 2.0
First-order types	(LICS) On the number of types in sparse graphs
Fishbone diagram	(GraMSec) Combining Bayesian Networks and Fishbone Diagrams to Distinguish between Intentional Attacks and Accidental Technical Failures
Fix-points	(HCVS) A simple functional presentation and an inductive correctness proof of the Horn algorithm
fixed parameter complexity	(MoRe) Parameterized complexity of games with monotonically ordered omega-regular objectives
fixed parameter tractable	(QBF) Tractability results for structured quantified CNF-formulas via knowledge compilation
Fixed Point Arithmetic	(SMT) The next 10^4 UppSAT Approximations
fixed point equations	(FSCD) Fixed-Point Constraints for Nominal Equational Unification
fixed points	(PARIS) Local Validity for Circular Proofs in Linear Logic with Fixed Points
fixed-point algorithms for synthesis	(SYNT) Warm-Starting Fixed-Point Based Control Synthesis
fixed-point logic	(LICS) Definable Ellipsoid Method, Sums-of-Squares Proofs, and the Isomorphism Problem
Fixpoint Algorithms	(ICLP) Towards Incremental and Modular Context-sensitive Analysis
fixpoint alternation	(PARIS) Collapses of Fixpoint Alternation Hierarchies in Low Type-Levels of Higher-Order Fixpoint Logic
fixpoint logic	(ARQNL) Evidence Extraction from Parameterised Boolean Equation Systems (LICS) A Fixpoint Logic and Dependent Effects for Temporal Property Verification
fixpoints	(Domains13) Invited Talk: Approximating partial by total: fixpoint characterizations of back-and-forth equivalences
flattener	(F-IDE) AsmetaF: a flattener for the ASMETA framework
Floating Point Arithmetic	(SMT) The next 10^4 UppSAT Approximations (IJCAR) Exploring Approximations for Floating-Point Arithmetic using UppSAT
floating-point	(SMT) Building Better Bit-Blasting for Floating-Point Problems
floating-point analysis	(FM) Combining Tools for Optimization and Analysis of Floating-Point Computations
floating-point optimization	(FM) Combining Tools for Optimization and Analysis of Floating-Point Computations
floating-point round-off errors	(FM) A Formally Verified Floating-Point Implementation of the Compact Position Reporting Algorithm
flocking	(VaVAS) Work-in-Progress: Adaptive Neighborhood Resizing for Stochastic Reachability in Distributed Flocking
Flow Analysis	(LICS) Causal Computational Complexity of Distributed Processes
flows and nowhere-zero flows	(LICS) A theory of linear typings as flows on 3-valent graphs
Fly-Automata	(LaSh) Monadic Second-Order Model Checking with Fly-Automata
FMI	(Overture) Multi-modelling of Cooperative Swarms
Focused Proof Systems	(IJCAR) A Logical Framework with Commutative and Non-Commutative Subexponentials
focused sequent calculus	(ARQNL) An Outline for Simple Semi-automated Proof Assistants for First-order Modal Logics (UITP) Interfacing with a Prover using Focusing and Logic Programming
focused sequent calculus for first-order modal logic	(ARQNL) An Outline for Simple Semi-automated Proof Assistants for First-order Modal Logics
Focusing	(LICS) Strong Sums in Focused Logic (LICS) Around Classical and Intuitionistic Linear Logics
Focussing	(IJCAR) Focussing, MALL and the polynomial hierarchy
FOIL algorithm	(ICLP) Cumulative Scoring-based Induction of Default Theories
FOL	(WiL) First-Order vs. Second-Order Encodings for LTLf-to-Automata Translation
Forest Algebra	(LICS) MSO Queries on Trees: Enumerating Answers under Updates Using Forest Algebras
Forest Algebras	(LICS) Wreath Products of Distributive Forest Algebras
Formal Analysis	(CSF) An extensive formal analysis of multi-factor authentication protocols
formal aspects of program analysis	(LICS) Work Analysis with Resource-Aware Session Types
Formal Definition	(LFMTP) What Does This Notation Mean Anyway? BNF-style notation as it is actually used
formal languages and automata theory	(CAV) Reactive Control Improvisation
Formal Library	(Coq) Classical Analysis with Coq
Formal Metatheory	(LFMTP) Formalisation of Barendregt's Variable Convention for Generic Structures with Binders (LFMTP) Formalization in Constructive Type Theory of the Standardization Theorem
Formal Methods	(DS-FM) A Formal Study of MANET Routing Protocols (CAV) JBMC: A Bounded Model Checking Tool for Verifying Java Bytecode (CAV) The DEEPSEC prover (FM) Disruptive Innovations for the Development and the Deployment of Fault-Free Software (FM) Z3 and SMT in Industrial R&D (FM) From Formal Requirements to Highly Assured Software for Unmanned Aircraft Systems (FM) CompoSAT: Specification-Guided Coverage for Model Finding (FM) The Compound Interest in Relaxing Punctuality (AVOCS) Climbing the Software Assurance Ladder - Practical Formal Verification for Reliable Software (AVOCS) Analyzing Consistency of Formal Requirements (F-IDE) Integrating user design and formal models within PVSio-Web (F-IDE) The CLEAR Way To Transparent Formal Methods (F-IDE) Improving the Visualization of Alloy Instances (F-IDE) Experience Report on Formally Verifying Parts of OpenJDK's API with KeY (ITP) Understanding Parameters of Deductive Verification: an Empirical Investigation of KeY (CSF) Automated Unbounded Verification of Stateful Cryptographic Protocols with Exclusive OR (VaVAS) Policing Functions for Machine Learning Systems (VSTTE) Constructing Independently Verifiable Privacy-Compliant Type Systems for Message Passing between Black-Box Components (FCS) Homomorphisms and Minimality for Enrich-by-Need Security Analysis (SR) Verification of Multi-agent Systems with Imperfect Information and Public Actions
formal methods for security	(CSF) Symbolic security of garbled circuits
formal methods in practice	(FM) A Formally Verified Floating-Point Implementation of the Compact Position Reporting Algorithm
Formal Model	(FCS) LISA: Predicting the Impact of DoS Attacks on Real-World Low Power IoT Systems
Formal proof	(AVOCS) Proof-Oriented Design of a Separation Kernel with Minimal Trusted Computing Base (CSF) Formal Security Proof of CMAC and its Variants
formal proofs	(Coq) Procrastination, A proof engineering technique (ITP) A Formal Proof of the Minor-Exclusion Property for Treewidth-Two Graphs (ITP) Formalizing Ring Theory in PVS (Short Paper) (CSF) Secure compilation of side-channel countermeasures: the case of cryptographic “constant-time”
formal reasoning	(ReMOTE) Elements of a Model of Trust in Technology
Formal Semantics	(NLCS) Propositional Forms of Judgemental Interpretations
formal specification	(FM) Formal Specification and Verification of Dynamic Parametrized Architectures (VEMDP) Executable Biochemical Space for Specification and Analysis of Biochemical Systems
formal topology	(LICS) Computable decision making on the reals and other spaces via partiality and nondeterminism
formal verification	(DS-FM) Formal verification of neural networks (FM) Interlocking Design Automation using Prover Trident (FM) Formal Specification and Verification of Dynamic Parametrized Architectures (FM) Formal Verification of Automotive Simulink Controller Models: Empirical Technical Challenges, Evaluation and Recommendations (FM) Verifying Auto-Generated C Code from Simulink (SMT) SMT-based Compile-time Verification of Safety Properties for Smart Contracts (AVOCS) Formal Verification of Synchronisation, Gossip and Environmental Effects for Wireless Sensor Networks (VEMDP) Using Transitivity and Modularity in Chemical Reaction Network Bisimulation (VEMDP) Formal Verification of Network-Based Biocomputation Circuits (LICS) A Hybrid, Dynamic Logic for Hybrid-Dynamic Information Flow (ITP) Verifying the LTL to Büchi Automata Translation via Very Weak Alternating Automata (ITP) Verified Tail Bounds for Randomized Programs (CSF) Alethea: A Provably Secure Random Sample Voting Protocol (CSF) Computer-aided proofs for multiparty computation with active security (CSF) Composition Theorems for CryptoVerif and Application to TLS 1.3 (VaVAS) Formalisation of the Rules of the Road for embedding into an Autonomous Vehicle Agent (FCS) A Study on the Preservation on Cryptographic Constant-Time Security in the CompCert Compiler (FCS) Proving physical proximity using symbolic models
formal verification at runtime	(VaVAS) Towards a Hierarchical-Control Architecture for Distributed Autonomous Systems (Extended Abstract - Paper)
Formalisation	(ITP) An Agda Formalization of Üresin & Dubois' Asynchronous Fixed-Point Theory (VSTTE) Verified Certificate Checking for Counting Votes
formalization	(IWC) Certified Ordered Completion (IWC) Towards a Verified Decision Procedure for Confluence of Ground Term Rewrite Systems in Isabelle/HOL (UNIF) Formalization of First-Order Syntactic Unification (Isabelle) Substitutionless First-Order Logic: A Formal Soundness Proof (WiL) Can every real proof be represented by a formal proof? The Hilbert-Gentzen thesis (HDRA) Towards a fully formalized definition of syllepsis in weak higher categories
FormalVerification	(VEMDP) Bayesian Verification of Chemical Reaction Networks
forward proof-search	(EICNCL) A Forward Calculus for Countermodel Construction in IPL
four-valued logic	(GraMSec) On Linear Logic, Functional Programming, and Attack Trees
Frama-C	(FM) A Formally Verified Floating-Point Implementation of the Compact Position Reporting Algorithm
Frames	(Domains13) Frames and frame relations
Free choice sequences	(WiL) On Expanding Standard Notions of Constructivity
free modules	(IWC) The diamond lemma for free modules
free monad	(FM) Modular Verification of Programs with Effects and Effect Handlers in Coq
Free Variable	(LaSh) Lazy Automata Techniques for WS1S
Frege systems	(PC) Complexity of expander-based reasoning and the power of monotone proofs
Freyd categories	(Linearity/TLLA) From Linear Logic to Cyclic Sharing
Frobenius algebra	(LICS) Rewriting with Frobenius
FSM	(FM) FSM Inference from Long Traces
Full abstraction	(GS) A definable game semantics for the linear quantum lambda-calculus (LICS) Eager Functions as Processes
Function algebras	(LCC) A recursion-theoretic characterisation of the positive polynomial-time functions
Function classes	(LCC) A recursion-theoretic characterisation of the positive polynomial-time functions
function package	(ThEdu) Lucas Interpretation from Programmers’ Perspective
function summaries	(VSTTE) Lattice-Based Refinement in Bounded Model Checking
Functional Analysis	(LICS) A Logical Account for Linear Partial Differential Equations (Linearity/TLLA) Models of Linear Logic based on the Schwartz epsilon product
functional and relational specifications	(LFMTP) Computation-as-deduction in Abella: work in progress
functional dependency	(TERMGRAPH) Finding the Transitive Closure of Functional Dependencies using Strategic Port Graph Rewriting
Functional interpretation	(LICS) Dialectica models of type theory (LICS) A functional interpretation with state
Functional Mock-up Interface	(Overture) Overture FMU: Export VDM-RT Models as Tool-Wrapper FMUs
functional programming	(FSCD) Nominal Unification with Atom and Context Variables (FSCD) Counting Environments and Closures (LPOP) A software system should be declarative except where it interacts with the real world (LFMTP) Functional programming with λ-tree syntax: a progress report (GraMSec) On Linear Logic, Functional Programming, and Attack Trees (LICS) A Generalized Modality for Recursion (ITP) Verified Timing Transformations in Synchronous Circuits with LambdaPi-Ware (ITP) Formalization of a Polymorphic Subtyping Algorithm (VSTTE) Practical Methods for Reasoning about Java 8's Functional Programming Features (WPTE) Optimizing Space of Parallel Processes
functor	(ITP) Relational Parametricity and Quotient Preservation for Modular (Co)Datatypes (FCS) A Homotopical Approach to Cryptography
functor algebra	(Domains13) Algebra semantics of recursive computation types
functorial spans	(LOLA) Asynchronous games fifteen years later
fuzz	(LICS) Quantitative Behavioural Reasoning for Higher-order Effectful Programs: Applicative Distances
fuzzer	(CAV) StringFuzz: A Fuzzer for String Solvers
fuzzy generalization	(UNIF) Proximity-Based Generalization
Fuzzy logic	(LICS) A van Benthem Theorem for Fuzzy Modal Logic
G
g-leakage	(FM) An Algebraic Approach for Reasoning About Information Flow
Game semantics	(PARIS) LMSO: A Curry-Howard Approach to Church’s Synthesis via Linear Logic (speaker: Pierre PRADIC) (GS) Automata Theory and Game Semantics (GS) Resource-Tracking Concurrent Games (GraMSec) The Attacker Does not Always Hold the Initiative: Attack Trees with External Refinement (LICS) Extensional and Intensional Semantic Universes: A Denotational Model of Dependent Types (LICS) LMSO: A Curry-Howard Approach to Church's Synthesis via Linear Logic (LICS) The concurrent game semantics of Probabilistic PCF (LICS) What's in a game? A theory of game models (LOLA) Asynchronous games fifteen years later
game theory	(LICS) Compositional game theory (MSFP) Backward induction for repeated games (ITP) Towards Formal Foundations for Game Theory (Short Paper)
Games	(SAT) Cops-Robber games and the resolution of Tseitin formulas
games and logic	(LICS) Distribution-based objectives for Markov Decision Processes
games played on finite graphs	(SR) Beyond admissibility: Dominance between chains of strategies
Gandy	(DCM) A Category Theoretic Interpretation of Gandy’s Principles for Mechanisms
Gappa	(FM) A Formally Verified Floating-Point Implementation of the Compact Position Reporting Algorithm
garbled circuit	(CSF) Symbolic security of garbled circuits
generalised operads	(Domains13) Higher-dimensional categories: recursion on extensivity
generalised species	(LICS) Species, Profunctors and Taylor Expansion Weighted by SMCC--A Unified Framework for Modelling Nondeterministic, Probabilistic and Quantum Programs--
Generalization of syntactic parse trees	(NLCS) Anti-Unification and Natural Language Processing
Generalized Reactivity	(DS-FM) Heuristic-Based GR(1) Assumptions Refinement (FM) A Weakness Measure for GR(1) Formulae
Generic Binding Structures	(LFMTP) Formalisation of Barendregt's Variable Convention for Generic Structures with Binders
generic proof assistant	(UITP) Interfacing with a Prover using Focusing and Logic Programming
Genetic algorithms	(RCRA) An Enhanced Genetic Algorithm with the BLF2G Guillotine Placement Heuristic for the Orthogonal Cutting-Stock Problem
Geometric Automated Theorem Provers	(ThEdu) Rating of Geometric Automated Theorem Provers
geometric realization	(HoTT/UF) Geometric realization of truncated semi-simplicial sets meta-constructed within HoTT
Geometry	(WiL) On Expanding Standard Notions of Constructivity
geometry of interaction	(DCM) Models of Computation that Conserve Data (LICS) The Geometry of Computation-Graph Abstraction (Linearity/TLLA) Coherent interaction graphs: a nondeterministic geometry of interaction for MLL
Gillespie algorithm	(VEMDP) Rule-Based Gillespie Simulation of Chemical Systems
Girard's translations	(Linearity/TLLA) The Bang Calculus and the Two Girard's Translations
global states	(CSF) A little more conversation, a little less action, a lot more satisfaction: Global states in ProVerif.
gluing	(LICS) Dialectica models of type theory
GNATProve	(WPTE) Verification of Ada Programs with AdaHorn
goal-directed evaluation	(ICLP) Constraint Answer Set Programming without Grounding
graded monads	(LOLA) Experimenting with graded monads: certified grading-based program transformations
Gradient Boosting on Decision Trees	(MLP) Splitting source code identifiers using Bidirectional LSTM Recurrent Neural Network
Gradient descent	(MLP) Difflog: Beyond Deductive Methods in Program Analysis
Gradual Typing	(FSCD) Call-by-name Gradual Type Theory (ITRS) Gradual Intersection Types
grammar	(VSTTE) A Formalization of the ABNF Notation and a Verified Parser of ABNF Grammars
Grammar testing	(NLCS) Automatic test suite generation for PMCFG grammars
Grammatical Framework	(ICLP-DC) Natural Language Generation From Ontologies (NLCS) Automatic test suite generation for PMCFG grammars (ICLP) Natural Language Generation From Ontologies: Application Paper
grammatical inference	(LearnAut) Learning Several Languages from Labeled Strings: State Merging and Evolutionary Approaches
graph	(SR) Concurrent games and semi-random determinacy
graph algorithms	(FSCD) Unique perfect matchings and proof nets
Graph Analysis	(LPOP) A Rule-Based Tool for Analysis and Generation of Graphs Applied to Mason's Marks
Graph Drawing	(LPOP) A Rule-Based Tool for Analysis and Generation of Graphs Applied to Mason's Marks
graph encoding	(TERMGRAPH) SLD-Resolution Reduction of Second-Order Horn Fragments - Extended Abstract
Graph Generation	(LPOP) A Rule-Based Tool for Analysis and Generation of Graphs Applied to Mason's Marks
graph grammars	(CAV) Let this Graph be your Witness! An Attestor for Verifying Java Pointer Programs (TERMGRAPH) A framework for rewriting families of string diagrams
graph isomorphism	(LICS) Definable Ellipsoid Method, Sums-of-Squares Proofs, and the Isomorphism Problem
graph minor theorem	(ITP) A Formal Proof of the Minor-Exclusion Property for Treewidth-Two Graphs
graph neural networks	(MLP) Deep Learning On Code with an Unbounded Vocabulary
Graph Queries	(ICLP) Certified Graph View Maintenance with Regular Datalog
Graph Recognition	(LPOP) A Rule-Based Tool for Analysis and Generation of Graphs Applied to Mason's Marks
Graph Representation	(LPOP) A Rule-Based Tool for Analysis and Generation of Graphs Applied to Mason's Marks
graph rewriting	(TERMGRAPH) Drags: an algebraic framework for graph rewriting (WST) GPO: A Path Ordering for Graphs (LOLA) A graph-rewriting perspective of the beta-law
graph rewriting systems	(TERMGRAPH) A Port-graph Model for Finance
graph theory	(LCC) Completeness in the Second Level of the Polynomial Time Hierarchy through Syntactic Properties (LICS) Allegories: decidability and graph homomorphisms (LICS) A theory of linear typings as flows on 3-valent graphs (ITP) A Formal Proof of the Minor-Exclusion Property for Treewidth-Two Graphs
Graph transformation	(VEMDP) Rule-Based Gillespie Simulation of Chemical Systems
Graph Views	(ICLP) Certified Graph View Maintenance with Regular Datalog
Graph Weighted Models	(LearnAut) Learning Graph Weighted Models on Pictures
graph-based characterization	(ICLP) MASP-Reduce: a proposal for distributed computation of stable models
Graphical reasoning	(LICS) Rewriting with Frobenius
Gray categories	(IWC) Critical pairs for Gray categories
Gray category	(FSCD) Coherence of Gray categories via rewriting
greatest fixed point	(CSF) Symbolic security of garbled circuits
Greedy Heuristics	(RCRA) Greedy Randomized Search for Scalable Compilation of Quantum Circuits
Groebner bases	(SCSC) EA: New in CoCoA-5.2.4 and CoCoALib-0.99570 for SC-Square
Grothendieck fibrations	(HoTT/UF) First-order homotopical logic and Grothendieck fibrations
Grothendieck quasi-topos	(Domains13) Invited Talk: A domain theory for quasi-Borel spaces and statistical probabilistic programming
ground systems	(IWC) Towards a Verified Decision Procedure for Confluence of Ground Term Rewrite Systems in Isabelle/HOL
ground theories	(UNIF) ACUI Unification modulo Ground Theories
Grounding	(QBF) A Grounder From Second-Order Logic To QBF
Group decision	(PRUV) Evidential Group Decision Making Model with Belief-Based Preferences
Groupoid	(FCS) A Homotopical Approach to Cryptography
Gröbner Basis	(SCSC) RP: A Practical Polynomial Calculus for Arithmetic Circuit Verification
Guard Condition	(Coq) Towards a formalization of the guard condition
Guarded Recursion	(FSCD) The clocks they are adjunctions. Denotational semantics for Clocked Type Theory (PARIS) What makes guarded types tick? (LICS) Guarded Computational Type Theory (LICS) A Generalized Modality for Recursion
Guillotine Constraint	(RCRA) An Enhanced Genetic Algorithm with the BLF2G Guillotine Placement Heuristic for the Orthogonal Cutting-Stock Problem
H
Hadamard matrices	(SCSC) Hard Combinatorial Problems: A Challenge for Satisfiability
halting problem	(WST) Objective and Subjective Specifications (LICS) A parameterized halting problem, the linear time hierarchy, and the MRDP theorem
Hamiltonian cycle	(POS) Stedman and Erin Triples encoded as a SAT Problem
hammers	(ITP) ProofWatch: Watchlist Guidance for Large Theories in E
Handlers	(LICS) Syntax and Semantics for Operations with Scopes
handwriting	(ITP) Towards Verified Handwritten Calculational Proofs (Short Paper)
Handwritten Digit Recognition	(ICLP) Incremental and Iterative Learning of Answer Set Programs from Mutually Distinct Examples
handwritten mathematics	(ITP) Towards Verified Handwritten Calculational Proofs (Short Paper)
hardness of approximation	(VEMDP) Computing properties of stable configurations of thermodynamic binding networks (VSTTE) Verification of Binarized Neural Networks via Inter-Neuron Factoring
Hardware model	(ITP) Physical Addressing on Real Hardware in Isabelle/HOL
hardware verification	(FM) Modular Verification of Programs with Effects and Effect Handlers in Coq (ITP) Verified Timing Transformations in Synchronous Circuits with LambdaPi-Ware
hardware-in-the-loop	(FM) Model-Based Testing for Avionics Systems
Hardware/software interfaces	(CAV) Model Checking Boot Code from AWS Data Centers
hash functions	(CSF) Backdoored Hash Functions: Immunizing HMAC and HKDF
Hashing-based Algorithm	(PRUV) A New Probabilistic Algorithm for Approximate Model Counting
Haskell	(GraMSec) On Linear Logic, Functional Programming, and Attack Trees
HCI	(F-IDE) Improving the Visualization of Alloy Instances
head variable	(NLCS) Do different syntactic trees yield different logical readings? Some remarks on head variables in typed lambda calculus.
heaps	(LOLA) Heaps denote finitely partitioned trees
herbrand theorem	(SMT) Revisiting Enumerative Instantiation
Herbrand's theorem	(TYDI) Deep Inference, Herbrand's Theorem and Expansion Proofs (CL&C) Herbrand's Theorem as Higher-Order Recursion (CL&C) Fast cut-elimination using proof terms: an empirical study
hereditarily definable sets	(LICS) On computability and tractability for infinite sets
hereditary substitution	(MSFP) Everybody's Got To Be Somewhere
heuristic search	(DS-FM) Heuristic-Based GR(1) Assumptions Refinement
Heuristics	(ICLP-DC) Speeding Up Lazy-Grounding Answer Set Solving (RCRA) An Enhanced Genetic Algorithm with the BLF2G Guillotine Placement Heuristic for the Orthogonal Cutting-Stock Problem
hidden tree Markov model	(LearnAut) Learning Tree Distributions by Hidden Markov Models
Hierarchical information	(SR) Strategy Logic with Imperfect Information
Hierarchical state machines	(F-IDE) A Notebook Format for the Holistic Design of Embedded Systems
Hierarchy Theorem	(LICS) The State Complexity of Alternating Automata
higher categories	(IWC) Critical pairs for Gray categories (HoTT/UF) Towards the syntax and semantics of higher dimensional type theory
higher dimensional categories	(Domains13) Higher-dimensional categories: recursion on extensivity
Higher dimensional linear rewriting	(HDRA) Termination in linear (2,2)-categories with braidings and duals
higher groups	(LICS) Higher Groups in Homotopy Type Theory
higher inductive type	(HoTT/UF) Geometric realization of truncated semi-simplicial sets meta-constructed within HoTT (FCS) A Homotopical Approach to Cryptography
higher inductive types	(FSCD) A Syntax for Higher Inductive-Inductive Types (LICS) On Higher Inductive Types in Cubical Type Theory (LICS) Impredicative Encodings of (Higher) Inductive Types
Higher order recursion schemes	(CL&C) Herbrand's Theorem as Higher-Order Recursion
higher-order	(Domains13) Robust computability notions for types arising in classical analysis
Higher-order abstract syntax (HOAS)	(LFMTP) Abstract Representation of Binders in OCaml using the Bindlib Library
higher-order computability	(LICS) Type-two polynomial-time and restricted lookahead.
higher-order logic	(WiL) Embedding Intuitionistic Modal Logics in Higher-Order Logic. An Easy Task? (SMT) Higher-Order SMT Solving (Vampire) Developments in Higher-order Theorem proving within Vampire (PAAR) Set of Support for Higher-Order Reasoning (IJCAR) Superposition for Lambda-Free Higher-Order Logic (IJCAR) The Higher-Order Prover Leo-III
higher-order logic programming	(ARQNL) An Outline for Simple Semi-automated Proof Assistants for First-order Modal Logics (UITP) Interfacing with a Prover using Focusing and Logic Programming (ICLP) Approximation Fixpoint Theory and the Well-Founded Semantics of Higher-Order Logic Programs
higher-order modal logic	(IJCAR) The Higher-Order Prover Leo-III
higher-order operads	(HOR) The next 700 (type-theoretical) denotational models ?
higher-order programs	(CAV) Propositional Dynamic Logic for Higher-Order Functional Programs (LICS) A Fixpoint Logic and Dependent Effects for Temporal Property Verification
higher-order reasoning	(IJCAR) The Higher-Order Prover Leo-III
higher-order recursion schemes	(FSCD) Homogeneity without Loss of Generality
higher-order rewriting	(WST) Termination of Lambda-Pi modulo rewriting using the size-change principle (HOR) Orthogonality and sequentiality in substructural Linear HRSs
higher-order term rewriting	(WST) Improving Static Dependency Pairs for Higher-Order Rewriting
higher-order unification	(FSCD) Nominal Unification with Atom and Context Variables
Higher-Ranked Polymorphism	(ITP) Formalization of a Polymorphic Subtyping Algorithm
Highly Assured Software	(FM) From Formal Requirements to Highly Assured Software for Unmanned Aircraft Systems
Hilbert's tenth problem	(Isabelle) Hilbert Meets Isabelle: Formalisation of the DPRM Theorem in Isabelle
Hilbert-Gentzen thesis	(WiL) Can every real proof be represented by a formal proof? The Hilbert-Gentzen thesis
HKDF	(CSF) Backdoored Hash Functions: Immunizing HMAC and HKDF
HMAC	(CSF) Backdoored Hash Functions: Immunizing HMAC and HKDF
HOL	(LFMTP) Sharing a library between proof assistants: reaching out to the HOL family (Isabelle) Using Isabelle/UTP for the Verification of Sorting Algorithms: A Case Study (IJCAR) The Higher-Order Prover Leo-III (ITP) Verifying the LTL to Büchi Automata Translation via Very Weak Alternating Automata (VSTTE) Verified Certificate Checking for Counting Votes
HOL Light	(ITP) HOL Light QE
homogeneous	(IJCAR) Complexity of Combinations of Qualitative Constraint Satisfaction Problems
homogeneous linear diophantine equations	(ITP) A Formally Verified Solver for Homogeneous Linear Diophantine Equations
homogeneous types	(FSCD) Homogeneity without Loss of Generality
Homological algebra	(HDRA) Minimal models for monomial algebras
Homomorphism	(UNIF) Bounded ACh Unification
Homotopical algebra	(HDRA) Minimal models for monomial algebras
Homotopy	(FCS) A Homotopical Approach to Cryptography
homotopy type theory	(FSCD) A Syntax for Higher Inductive-Inductive Types (FSCD) Internal Universes in Models of Homotopy Type Theory (LICS) On Higher Inductive Types in Cubical Type Theory (LICS) Cellular Cohomology in Homotopy Type Theory (LICS) Free Higher Groups in Homotopy Type Theory (LICS) Higher Groups in Homotopy Type Theory (LICS) Impredicative Encodings of (Higher) Inductive Types (NLCS) Propositional Attitude Operators in Homotopy Type Theory (HoTT/UF) Cubical Computational Type Theory (HoTT/UF) Dependent Right Adjoint Types
Hopf Monad	(FSCD) Lifting Coalgebra Modalities and IMELL Model Structure to Eilenberg-Moore Categories
Horn clause	(PARIS) Coinductive Uniform Proofs: An Extended Abstract (speaker: Yue LI)
Horn Clause Transformation	(ICLP) Solving Horn Clauses on Inductive Data Types Without Induction
Horn clauses	(CAV) Constraint-Based Synthesis of Coupling Proofs (TERMGRAPH) SLD-Resolution Reduction of Second-Order Horn Fragments - Extended Abstract (HCVS) Towards Coinductive Theory Exploration in Horn Clause Logic: Extended Abstract (ICLP) Proof-relevant Horn Clauses for Dependent Type Inference and Term Synthesis
Horn propositional satisfiability algorithm	(HCVS) A simple functional presentation and an inductive correctness proof of the Horn algorithm
howe's method	(LICS) Quantitative Behavioural Reasoning for Higher-order Effectful Programs: Applicative Distances
HW-SW interface	(ITP) Physical Addressing on Real Hardware in Isabelle/HOL
hybrid logic	(LICS) A Hybrid, Dynamic Logic for Hybrid-Dynamic Information Flow
Hybrid System	(CAV) Spacetime Interpolants
hybrid system simulators	(RCRA) Computing Personalised Treatments through In Silico Clinical Trials. A Case Study on Downregulation in Assisted Reproduction.
hybrid systems	(SYNT) Safe, Automated and Formal Synthesis of Digital Controllers for Continuous Plants (LICS) A Hybrid, Dynamic Logic for Hybrid-Dynamic Information Flow
hydraulic oil pump	(FM) Optimal and Robust Controller Synthesis Using Energy Timed Automata with Uncertainty
Hyper sequents	(PARIS) Towards the Automatic Construction of Schematic Proofs
hypercube optimization	(PC) Optimization over the Boolean Hypercube via Sums of Nonnegative Circuit Polynomials
Hyperintensional Logic	(NLCS) Propositional Attitude Operators in Homotopy Type Theory
hyperltl	(SYNT) On the Expressiveness of HyperLTL Synthesis
hyperproperties	(CAV) Synthesizing Reactive Systems from Hyperproperties (CAV) Model Checking Quantitative Hyperproperties (SYNT) On the Expressiveness of HyperLTL Synthesis
Hyperproperty Verification	(CAV) Exploiting Synchrony and Symmetry in Relational Verification
Hypersequent calculus	(EICNCL) Hypersequent calculus for the logic of conditional belief: preliminary results
hypersequents	(Linearity/TLLA) Taking Linear Logic Apart
I
ic3	(SMT) Discovering Universally Quantified Solutions for Constrained Horn Clauses (AVOCS) A Framework for the Formal Verification of Networks of Railway Interlockings - Application to the Belgian Railways (SAT) Finding all Minimal Safe Inductive Sets
IDE	(ITP) Towards Verified Handwritten Calculational Proofs (Short Paper)
Idempontent	(UNIF) Towards Generalization Methods for Purely Idempotent Equational Theories
Idempotent quasigroups	(IJCAR) Investigating the Existence of Large Sets of Idempotent Quasigroups via Satisfiability Testing
identifier	(MLP) Splitting source code identifiers using Bidirectional LSTM Recurrent Neural Network
Identity type	(FCS) A Homotopical Approach to Cryptography
IEEE-754	(SMT) Building Better Bit-Blasting for Floating-Point Problems
ILP	(TERMGRAPH) SLD-Resolution Reduction of Second-Order Horn Fragments - Extended Abstract
immunization	(CSF) Backdoored Hash Functions: Immunizing HMAC and HKDF
imperative	(REFINE) a Theory of Lazy Imperative Timing
imperative calculi	(DCM) A syntactic model of mutation and aliasing
Imperative languages	(TERMGRAPH) Programming by Term Rewriting
imperative programming	(LPOP) A software system should be declarative except where it interacts with the real world
imperative programs	(WPTE) On Transforming Functions Accessing Global Variables into Logically Constrained Term Rewriting Systems
Imperfect information	(SR) Strategy Logic with Imperfect Information
Implementation and benchmarks for parity games	(SR) Solving Parity Games: Explicit vs Symbolic
implicate generation	(IJCAR) A Generic Framework for Implicate Generation Modulo Theories
implicative algebras	(ITP) Formalizing Implicative Algebras in Coq
implicit complexity	(FSCD) Term rewriting characterisation of LOGSPACE for finite and infinite data (LCC) A recursion-theoretic characterisation of the positive polynomial-time functions (Linearity/TLLA) A semantic conjecture on second-order MLL and its complexity consequences (work in progress)
Implicit Hitting Set	(IJCAR) Implicit Hitting Set Algorithms for Maximum Satisfiability Modulo Theories
Importance Splitting	(FM) Statistical Model Checking of LLVM Code
impredicative encodings	(LICS) Impredicative Encodings of (Higher) Inductive Types
impredicativity	(LICS) Impredicative Encodings of (Higher) Inductive Types
inconsistency measures	(PRUV) Measuring Disagreement among Knowledge Bases
inconsistency-tolerant reasoning	(PRUV) Measuring Disagreement among Knowledge Bases
Inconsistent Requirements Explanation	(DS-FM) Consistency Checking of Functional Requirements
increasing chains	(SR) Beyond admissibility: Dominance between chains of strategies
Incremental	(SCSC) RP: Towards Incremental Cylindrical Algebraic Decomposition in Maple
Incremental Analysis	(ICLP) Towards Incremental and Modular Context-sensitive Analysis
Incremental Maintenance	(ICLP) Certified Graph View Maintenance with Regular Datalog
Incremental SAT	(IJCAR) An Assumption-Based Approach for Solving The Minimal S5-Satisfiability Problem
Indexed types	(FSCD) Index-Stratified Types
Indistinguishability	(CAV) Model checking indistinguishability of randomized security protocols
induction	(PARIS) Local Validity for Circular Proofs in Linear Logic with Fixed Points (PARIS) Transitive Closure Logic: Infinitary and Cyclic Proof Systems (WiL) Non-well-founded proof system for Transitive Closure Logic
induction principle	(ITP) Efficient Mendler-Style Lambda-Encodings in Cedille
induction reasoning	(PARIS) Useless Explicit Induction Reasoning (CL&C) Validating Back-links of FOL-ID Cyclic Pre-proofs
induction rules	(PC)
inductive datatypes	(ITP) Efficient Mendler-Style Lambda-Encodings in Cedille
Inductive Definitions	(AVOCS) An Entailment Checker for Separation Logic with Inductive Definitions (HCVS) A simple functional presentation and an inductive correctness proof of the Horn algorithm
Inductive invariants	(CAV) Syntax-Guided Termination Analysis (SMT) Discovering Universally Quantified Solutions for Constrained Horn Clauses (CSF) Inductive Invariants for Noninterference in Multi-agent Workflows
Inductive Logic Programming	(ICLP-DC) The Learning-Knowledge-Reasoning Paradigm For Natural Language Understanding and Question Answering (ICLP) Exploiting Answer Set Programming with External Sources for Meta-Interpretive Learning (ICLP) Incremental and Iterative Learning of Answer Set Programs from Mutually Distinct Examples (ICLP) Learning Commonsense Knowledge through Interactive Dialogue (ICLP) Cumulative Scoring-based Induction of Default Theories
Inductive predicates	(ADSL) Labelled Cyclic Proofs for Separation Logic
inductive theorem prover	(PARIS) Towards the Automatic Construction of Schematic Proofs
Inductive Theorem Proving	(ICLP) Solving Horn Clauses on Inductive Data Types Without Induction
inductive types	(FSCD) Cumulative Inductive Types in Coq (LICS) Impredicative Encodings of (Higher) Inductive Types
inductive validity cores	(CAV) The JKind Model Checker
inductive-inductive types	(FSCD) A Syntax for Higher Inductive-Inductive Types
Industrial application	(Overture) Transforming an industrial case study from VDM++ to VDM-SL
industrial case	(FM) Optimal and Robust Controller Synthesis Using Energy Timed Automata with Uncertainty
industrial impact	(FM) 20 Years of "Real" Real-Time Model Checking
inference	(FM) FSM Inference from Long Traces (NLCS) Automated Reasoning from Polarized Parse Trees
inference attacks	(CSF) Privacy Risk in Machine Learning: Analyzing the Connection to Overfitting
infinitary and cyclic systems	(WiL) Non-well-founded proof system for Transitive Closure Logic
Infinitary Proofs	(PARIS) Transitive Closure Logic: Infinitary and Cyclic Proof Systems
infinitary rewriting	(FSCD) Strict Ideal Completions of the Lambda Calculus (FSCD) Term rewriting characterisation of LOGSPACE for finite and infinite data
Infinite computation	(CL&C) Some ideas on cut-elimination for cyclic arithmetic proofs
infinite descent	(PARIS) Local Validity for Circular Proofs in Linear Logic with Fixed Points (AVOCS) An Entailment Checker for Separation Logic with Inductive Definitions
infinite duration	(SR) Concurrent games and semi-random determinacy
Infinite modalities	(EICNCL) Sequent Calculi for Logic that Includes an Infinite Number of Modalities
infinite-state systems	(CAV) Eager Abstraction for Symbolic Model Checking (LICS) Separability by piecewise testable languages and downward closures beyond subwords
Infinite-valued logic	(ARQNL) Formalization of a Paraconsistent Infinite-Valued Logic
Infinitely nested Boolean structure	(CL&C) A Denotational Model of the Typed Lambda-Mu Calculus
Infinity-Categories	(HoTT/UF) (Truncated) Simplicial Models of Type Theory
Infinity-Presheaves	(HoTT/UF) (Truncated) Simplicial Models of Type Theory
informal proofs	(WiL) Can every real proof be represented by a formal proof? The Hilbert-Gentzen thesis
Information Disclosure Analysis	(GraMSec) Disclosure Analysis of SQL Workflows
Information Extraction	(MLP) Answering Cloze-style Software Questions Using Stack Overflow
information flow	(FM) Formal Specification and Verification of Dynamic Parametrized Architectures (LaSh) A Logic of Information Flows (LICS) A Hybrid, Dynamic Logic for Hybrid-Dynamic Information Flow (CSF) Assuming you know: epistemic semantics of relational annotations for expressive flow policies (CSF) Knowledge-based Security of Dynamic Secrets for Reactive Programs (CSF) A Permission-Dependent Type System for Secure Information Flow Analysis (CSF) The Complexity of Monitoring Hyperproperties
information flow analysis	(CAV) Lazy Self-Composition for Security Verification
Information flow control	(CSF) Types for Information Flow Control: Labeling Granularity and Semantic Models
Injectivity	(Domains13) Frames and frame relations
inner-approximations	(CAV) Inner and Outer Approximating Flowpipes for Delay Differential Equations
innermost conditional narrowing	(FSCD) Narrowing Trees for Syntactically Deterministic Conditional Term Rewriting Systems
Insider threat	(GraMSec) A state machine system for insider threat detection
instantiation	(SMT) Revisiting Enumerative Instantiation (SMT) Higher-Order SMT Solving (Vampire) Giving AVATAR Quantifiers to Play With
Integer Arithmetic	(IJCAR) A Reduction from Unbounded Linear Mixed Arithmetic Problems into Bounded Problems
Integer Transition Systems	(WST) Complexity Analysis for Bitvector Programs
integer weights	(LICS) Stochastic Shortest Paths and Weight-Bounded Properties in Markov Decision Processes
Integrated Development Environment	(FM) QFLan: A Tool for the Quantitative Analysis of Highly Reconfigurable Systems (F-IDE) User Support for the Combinator Logic Synthesizer Framework
integrated verification	(FM) Evidential and Continuous Integration of Software Verification Tools
Integration	(CAV) Continuous formal verification of Amazon s2n (FM) IPL: An Integration Property Language for Multi-Model Cyber-Physical Systems
integrity	(CSF) A Cryptographic Look at Multi-Party Channels
Intension	(NLCS) Propositional Attitude Operators in Homotopy Type Theory
intensional computation	(Domains13) Domain Theory for Intensional Computation
Intensional Logic	(NLCS) Propositional Attitude Operators in Homotopy Type Theory
Intensional Sets	(ICLP) Functional ASP with Intensional Sets; Application to Gelfond-Zhang Agreggates
Intensional Type Theory	(NLCS) Propositional Attitude Operators in Homotopy Type Theory
Intentional attack	(GraMSec) Combining Bayesian Networks and Fishbone Diagrams to Distinguish between Intentional Attacks and Accidental Technical Failures
intentions	(ICLP) An ASP Methodology for Understanding Narratives about Stereotypical Activities
interaction graphs	(Linearity/TLLA) Coherent interaction graphs: a nondeterministic geometry of interaction for MLL
Interaction nets	(DCM) Models of Computation that Conserve Data
Interactive system	(F-IDE) Integrating user design and formal models within PVSio-Web
interactive theorem prover	(UITP) Automated Theorem Proving in a Chat Environment
interactive theorem proving	(ThEdu) Towards intuitive reasoning in axiomatic geometry (LaSh) A Derivative-Based Decision Procedure for WS1S (IJCAR) Proof-Producing Synthesis of CakeML with I/O and Local State from Monadic HOL Functions (F-IDE) Lightweight Interactive Proving inside an Automatic Program Verifier (ITP) Verified Memoization and Dynamic Programming (ITP) Software Tool Support for Modular Reasoning in Modal Logics of Actions (ITP) Towards Verified Handwritten Calculational Proofs (Short Paper)
interactive tool	(FSCD) ProTeM: A Proof Term Manipulator
Interface design	(F-IDE) Integrating user design and formal models within PVSio-Web
Interlocking	(FM) Interlocking Design Automation using Prover Trident (AVOCS) A Framework for the Formal Verification of Networks of Railway Interlockings - Application to the Belgian Railways
Intermediate Language for Verification	(F-IDE) Lightweight Interactive Proving inside an Automatic Program Verifier
intermediate representations	(LOLA) A more precise, more correct stack and register model for CompCert
internal and external calculi	(WiL) A semantical view of sequent based systems
Internal calculi	(EICNCL) Effective Translations between Display and Labelled Proofs for Tense Logics
internal language	(FSCD) Internal Universes in Models of Homotopy Type Theory
internal parametricity	(HoTT/UF) Internalizing Presheaf Semantics: Charting the Design Space
Internet of Things	(AVOCS) Formal Verification of Synchronisation, Gossip and Environmental Effects for Wireless Sensor Networks (FCS) LISA: Predicting the Impact of DoS Attacks on Real-World Low Power IoT Systems
Interoperability	(LFMTP) Sharing a library between proof assistants: reaching out to the HOL family
Interpolation	(CAV) Spacetime Interpolants (CAV) Learning Abstractions for Program Synthesis (SMT) Selfless Interpolation for Infinite-State Model Checking (HCVS) Solving Constrained Horn Clauses Using Dependence-Disjoint Expansions
Interpretable Machine Learning	(POS) MLIC: A MaxSAT-Based framework for learning interpretable classification rules
interprocedural analysis	(WST) Procedure-Modular Termination Analysis
Intersection Type Systems	(Linearity/TLLA) Generalized generalized species of structure and resource modalities
intersection types	(ITRS) Natural Deduction and Normalization Proofs for the Intersection Type Discipline (ITRS) Gradual Intersection Types (ITRS) Intersection Subtyping with Constructors (ITRS) (TYDI) Deep-Inference Intersection Types (LICS) Every λ-Term is Meaningful for the Infinitary Relational Model
intersections	(LICS) Degrees of Relatedness - A Unified Framework for Parametricity, Irrelevance, Ad Hoc Polymorphism, Intersections, Unions and Algebra in Dependent Type Theory
interval arithmetics	(SCSC) EA: New in CoCoA-5.2.4 and CoCoALib-0.99570 for SC-Square
interval propagation	(SCSC) EA: Wrapping Computer Algebra is Surprisingly Successful for Non-Linear SMT
Intrinsic noise	(VEMDP) Noise control for molecular computing
intruder deduction problem	(UNIF) Knowledge Problems in Equational Extensions of Subterm Convergent Theories
intuitionism	(Domains13) A Brouwerian proof of the Fan Theorem
intuitionistic combinatorial proofs	(TYDI) Some incoherent musings on deep inference and combinatorial proofs
intuitionistic linear logic	(FSCD) Proof nets for bi-intuitionistic linear logic (LICS) Around Classical and Intuitionistic Linear Logics (LOLA) Towards a library of formalised undecidable problems in Coq: The undecidability of intuitionistic linear logic
Intuitionistic logic	(PC) Towards theories for positive polynomial time and monotone proofs with extension (LICS) Quasi-Open Bisimilarity with Mismatch is Intuitionistic (CL&C) Admissible tools in the kitchen of intuitionistic logic (EICNCL) Intuitionistic multi-agent subatomic natural deduction for belief and knowledge (ICLP) First-order answer set programming as constructive proof search
Intuitionistic logic of constant domains	(CL&C) On Natural Deduction for Herbrand Constructive Logics III: The Strange Case of the Intuitionistic Logic of Constant Domains
Intuitionistic mathematics	(WiL) On Expanding Standard Notions of Constructivity
Intuitionistic Modal Logic	(WiL) Decomposing labelled proof theory for intuitionistic modal logic (WiL) Embedding Intuitionistic Modal Logics in Higher-Order Logic. An Easy Task? (EICNCL) Toward intuitionistic non-normal modal logic and its calculi
intuitionistic propositional logic	(EICNCL) A Forward Calculus for Countermodel Construction in IPL
Invariant Checking	(SYNT) On Inductive Verification and Synthesis
Invariant Generation	(CAV) Exploiting Synchrony and Symmetry in Relational Verification
Invariant Synthesis	(SYNT) On Inductive Verification and Synthesis
Invariants	(Vampire) Foundations of SPECTRE (F-IDE) A Notebook Format for the Holistic Design of Embedded Systems (SAT) Effective use of SMT solvers for Program Equivalence Checking through Invariant Sketching and Query Decomposition
Inverse Reinforcement Learning	(CAV) Safety-Aware Apprenticeship Learning
IRM-calc	(SAT) Local Soundness for QBF Calculi
irrelevance	(LICS) Degrees of Relatedness - A Unified Framework for Parametricity, Irrelevance, Ad Hoc Polymorphism, Intersections, Unions and Algebra in Dependent Type Theory
Isabelle	(ThEdu) Lucas Interpretation from Programmers’ Perspective (Isabelle) Hilbert Meets Isabelle: Formalisation of the DPRM Theorem in Isabelle (Isabelle) Using Isabelle/UTP for the Verification of Sorting Algorithms: A Case Study (Isabelle) Further Scaling of Isabelle Technology (Isabelle) The remote_build Tool (LaSh) A Derivative-Based Decision Procedure for WS1S (IJCAR) Verifying Asymptotic Time Complexity of Imperative Programs in Isabelle (UITP) Isabelle/PIDE after 10 years of development (ITP) Software Tool Support for Modular Reasoning in Modal Logics of Actions (ITP) Verified Analysis of Random Binary Tree Structures (ITP) Towards Formal Foundations for Game Theory (Short Paper)
Isabelle Proof Assistant	(UNIF) Formalization of First-Order Syntactic Unification (ThEdu) Proving in the Isabelle Proof Assistant that the Set of Real Numbers is not Countable (ThEdu) Students' Proof Assistant (SPA) (ThEdu) Natural Deduction Assistant (NaDeA)
Isabelle/HOL	(IWC) Certified Ordered Completion (ARQNL) Formalization of a Paraconsistent Infinite-Valued Logic (Isabelle) Formal Verification of Bounds for the LLL Basis Reduction Algorithm (Isabelle) PaMpeR: A Proof Method Recommendation System for Isabelle/HOL (PAAR) A Verified Simple Prover for First-Order Logic (IJCAR) Formalizing Bachmair and Ganzinger's Ordered Resolution Prover (ITP) Verified Memoization and Dynamic Programming (ITP) Physical Addressing on Real Hardware in Isabelle/HOL (ITP) Relational Parametricity and Quotient Preservation for Modular (Co)Datatypes (ITP) Fast Machine Words in Isabelle/HOL (ITP) A Formalization of the LLL Basis Reduction Algorithm (ITP) A Formally Verified Solver for Homogeneous Linear Diophantine Equations (ITP) MDP + TA = PTA: Probabilistic Timed Automata, Formalized (Short Paper)
Isabelle/HOL Theorem Proving	(ITP) Program Verification in the Presence of Cached Address Translation
Isabelle/jEdit	(F-IDE) Isabelle/jEdit as IDE for domain-specific formal languages and informal text documents
IsaSAT	(Isabelle) A Verified SAT Solver with Watched Literals Using Imperative HOL (Extended Abstract)
Isomorphism type	(SAT) Minimal unsatisfiability and minimal strongly connected digraphs
isotopy	(HDRA) Normal forms for planar connected string diagrams
Iterated Boolean games	(SR) Local Equilibria in Logic-Based Multi-Player Games
J
JASP	(LPOP) Role-Based Access Control via JASP
Java	(CAV) JBMC: A Bounded Model Checking Tool for Verifying Java Bytecode (VSTTE) Practical Methods for Reasoning about Java 8's Functional Programming Features
Java byte-code	(VSTTE) A Java bytecode formalisation
JDLV	(LPOP) Invited Talk: On the Development of Industrial Applications with ASP
jEdit	(UITP) Isabelle/PIDE after 10 years of development
JML	(VSTTE) Practical Methods for Reasoning about Java 8's Functional Programming Features
Jordan Normal Form	(WST) A Perron-Frobenius Theorem for Jordan Blocks for Complexity Proving
Judgemental Interpretation	(NLCS) Propositional Forms of Judgemental Interpretations
Jung-Tix problem	(Domains13) Invited Talk: A domain theory for quasi-Borel spaces and statistical probabilistic programming
Jupyter	(F-IDE) A Notebook Format for the Holistic Design of Embedded Systems
K
k-safety verification	(CAV) Lazy Self-Composition for Security Verification
Kachinuki order	(WST) Comparing on Strings: Semantic Kachinuki Order
Kakutani's fixed point theorem	(LICS) Distribution-based objectives for Markov Decision Processes
KeY	(F-IDE) Experience Report on Formally Verifying Parts of OpenJDK's API with KeY (ITP) Understanding Parameters of Deductive Verification: an Empirical Investigation of KeY
key set	(IJCAR) Automated Reasoning about Key Sets
kleptography	(CSF) Backdoored Hash Functions: Immunizing HMAC and HKDF (CSF) Self-Guarding Cryptographic Protocols against Algorithm Substitution Attacks
Knapsack	(SMT) Puli - A Problem-Specific OMT Solver
knot theory	(SCSC) RP: Unknot Recognition Through Quantifier Elimination
Knowledge Acquisition	(ICLP-DC) Knowledge Authoring and Question Answering via Controlled Natural Language
Knowledge and belief	(EICNCL) Intuitionistic multi-agent subatomic natural deduction for belief and knowledge
Knowledge based Reasoning	(FM) Timed Epistemic Knowledge Bases for Social Networks
knowledge compilation	(PC) Proof systems for #SAT based on restricted circuits (QBF) Tractability results for structured quantified CNF-formulas via knowledge compilation
Knowledge Representation	(LPOP) Logic-based Methods for Software Engineers and Business People (NLCS) Graph Knowledge Representations for SICK
Knowledge Representation and Reasoning	(ICLP-DC) The Learning-Knowledge-Reasoning Paradigm For Natural Language Understanding and Question Answering (ICLP-DC) Explaining Actual Causation via Reasoning about Actions and Change
knowledge-based noninterference	(CSF) Knowledge-based Security of Dynamic Secrets for Reactive Programs
Knuth-Bendix criterion	(UNIF) Rewriting with Generalized Nominal Unification
Koat	(WST) Control-Flow Refinement via Partial Evaluation
Kripke model	(EICNCL) Sequent Calculi for Logic that Includes an Infinite Number of Modalities
L
L-derivative	(Domains13) A logical view of complex analytic maps
Labelled calculi	(EICNCL) Proof theory for quantified monotone modal logics (EICNCL) Effective Translations between Display and Labelled Proofs for Tense Logics
labelled calculus	(EICNCL) Toward intuitionistic non-normal modal logic and its calculi
labelled Markov chain	(CAV) Deciding Probabilistic Bisimilarity Distance One for Labelled Markov Chains
Labelled proof-systems	(ARQNL) Labelled Connection-based Proof Search for Multiplicative Intuitionistic Linear Logic
labelled sequent calculi	(ARQNL) Labelled Calculi for QMLs with Non-Rigid and Non-Denoting Terms
Labelled sequents	(WiL) Decomposing labelled proof theory for intuitionistic modal logic
labelled systems	(WiL) A semantical view of sequent based systems
lambda calculi	(LICS) Enriching a Linear/Non-linear Lambda Calculus: A Programming Language for String Diagrams
lambda calculus	(FSCD) Strict Ideal Completions of the Lambda Calculus (FSCD) On repetitive right application of B-terms (FSCD) Nominal Unification with Atom and Context Variables (ITRS) Strong normalization of simple types through uniform intersection types. (ITRS) Gradual Intersection Types (LPOP) A software system should be declarative except where it interacts with the real world (DCM) Towards a Formal System for Topological Quantum Computation (PARIS) Collapses of Fixpoint Alternation Hierarchies in Low Type-Levels of Higher-Order Fixpoint Logic (LFMTP) Formalization in Constructive Type Theory of the Standardization Theorem (LICS) Probabilistic stable functions on discrete cones are power series. (LICS) Eager Functions as Processes (Linearity/TLLA) The Bang Calculus and the Two Girard's Translations (Linearity/TLLA) How to count linear and affine closed lambda terms? (HOR) Orthogonality and sequentiality in substructural Linear HRSs (ICLP) First-order answer set programming as constructive proof search
lambda calculus and combinatory logic	(LICS) A theory of linear typings as flows on 3-valent graphs
lambda prolog	(ARQNL) An Outline for Simple Semi-automated Proof Assistants for First-order Modal Logics
lambda-calculus	(FSCD) Counting Environments and Closures (FSCD) Homogeneity without Loss of Generality (ITRS) Towards a Semantic Measure of the Execution Time in Call-by-Value lambda-Calculus (TYDI) Deep-Inference Intersection Types (TYDI) An introduction to deep inference (GS) A definable game semantics for the linear quantum lambda-calculus (WST) Termination of Lambda-Pi modulo rewriting using the size-change principle (LICS) Every λ-Term is Meaningful for the Infinitary Relational Model (Linearity/TLLA) On the Taylor expansion of λ-terms and the groupoid structure of their rigid approximants (HOR) Normalization and Taylor expansion of lambda-terms
lambda-encodings	(ITP) Efficient Mendler-Style Lambda-Encodings in Cedille
lambda-free higher-order logic	(IJCAR) Superposition for Lambda-Free Higher-Order Logic
lambda-prolog	(UITP) Interfacing with a Prover using Focusing and Logic Programming
lambda-tree syntax	(LFMTP) Functional programming with λ-tree syntax: a progress report
lambek calculus	(Linearity/TLLA) Substructural Calculi with Dependent Types (Linearity/TLLA) On the Lambek Calculus with an Exchange Modality
lams	(FM) A lightweight deadlock analysis technique of object-oriented programs
language based security	(CSF) A Permission-Dependent Type System for Secure Information Flow Analysis
Language inclusion	(CAV) Automata vs Linear-Programming Discounted-Sum Inclusion
large libraries	(ITP) ProofWatch: Watchlist Guidance for Large Theories in E
Large set	(IJCAR) Investigating the Existence of Large Sets of Idempotent Quasigroups via Satisfiability Testing
large theories	(IJCAR) An abstraction-refinement framework for reasoning with large theories
large-scale reasoning	(IJCAR) Efficient Model Construction for Horn Logic with VLog: System Description
lattice	(VSTTE) Lattice-Based Refinement in Bounded Model Checking
Lattice Basis Reduction	(Isabelle) Formal Verification of Bounds for the LLL Basis Reduction Algorithm
lattice traversal	(VSTTE) Lattice-Based Refinement in Bounded Model Checking
lax homomorphism	(Domains13) Algebra semantics of recursive computation types
laziness	(LICS) A sequent calculus with dependent types for classical arithmetic
lazy	(REFINE) a Theory of Lazy Imperative Timing
lazy evaluation	(Isabelle) Lazy Algebraic Types in Isabelle/HOL
lazy grounding	(ICLP-DC) Speeding Up Lazy-Grounding Answer Set Solving
lazy self-composition	(CAV) Lazy Self-Composition for Security Verification
Lean proof assistant	(LICS) Higher Groups in Homotopy Type Theory
learning	(CAV) The Learnability of Symbolic Automata (SYNT) Minimal Synthesis of String To String Functions From Examples
Learning from positive examples	(LearnAut) Toward Learning Boolean Functions from Positive Examples
learning transductions	(LearnAut) Learning Tree Distributions by Hidden Markov Models
Learning Weighted Automata	(LearnAut) Learning Graph Weighted Models on Pictures
learning-based testing	(LearnAut)
Least general generalization	(FSCD) Term-Graph Anti-Unification (NLCS) Anti-Unification and Natural Language Processing
Lemma learning	(SMT) Proofs in conflict-driven theory combination
lens	(MSFP) Profunctor Optics and the Yoneda Lemma
Leo-III	(IJCAR) The Higher-Order Prover Leo-III
Leveled sequents	(PARIS) Towards the Automatic Construction of Schematic Proofs
LFSR	(POS) Stedman and Erin Triples encoded as a SAT Problem
Likelihood weighting	(ICLP) Constraint-Based Inference in Probabilistic Logic Programs
Lina	(GraMSec) On Linear Logic, Functional Programming, and Attack Trees
linear algorithm	(POS) Local-Style Search in the Linear MaxSAT Algorithm: A Computational Study of Solution-Based Phase Saving
Linear Arithmetic	(IJCAR) A Reduction from Unbounded Linear Mixed Arithmetic Problems into Bounded Problems
Linear categories	(HDRA) Termination in linear (2,2)-categories with braidings and duals
Linear Category	(FSCD) Lifting Coalgebra Modalities and IMELL Model Structure to Eilenberg-Moore Categories
linear clauses	(SCSC) RP: Refutation of Products of Linear Polynomials
linear cliquewidth	(LICS) Definable decompositions for graphs of bounded linear cliquewidth
Linear Constraints	(IJCAR) Checking Array Bounds by Abstract Interpretation and Symbolic Expressions
linear distributivity	(TYDI) Some incoherent musings on deep inference and combinatorial proofs
linear logic	(FSCD) Proof nets for bi-intuitionistic linear logic (FSCD) Unique perfect matchings and proof nets (ITRS) Towards a Semantic Measure of the Execution Time in Call-by-Value lambda-Calculus (TYDI) Some incoherent musings on deep inference and combinatorial proofs (PARIS) LMSO: A Curry-Howard Approach to Church’s Synthesis via Linear Logic (speaker: Pierre PRADIC) (PARIS) Local Validity for Circular Proofs in Linear Logic with Fixed Points (ARQNL) Labelled Connection-based Proof Search for Multiplicative Intuitionistic Linear Logic (GraMSec) The Attacker Does not Always Hold the Initiative: Attack Trees with External Refinement (GraMSec) On Linear Logic, Functional Programming, and Attack Trees (LICS) LMSO: A Curry-Howard Approach to Church's Synthesis via Linear Logic (LICS) The Syntax and Semantics of Quantitative Type Theory (LICS) Unification nets: canonical proof net quantifiers (LICS) Work Analysis with Resource-Aware Session Types (LICS) Around Classical and Intuitionistic Linear Logics (LICS) A theory of linear typings as flows on 3-valent graphs (IJCAR) Focussing, MALL and the polynomial hierarchy (Coq) Preliminary Report on the Yalla Library (Linearity/TLLA) Generalized generalized species of structure and resource modalities (Linearity/TLLA) The structure of non decomposable connectives of linear logic (Linearity/TLLA) Substructural Calculi with Dependent Types (Linearity/TLLA) Formalization of Automated Trading Systems in a Concurrent Linear Framework (Linearity/TLLA) Benchmarking Linear Logic Translations (Linearity/TLLA) The Bang Calculus and the Two Girard's Translations (Linearity/TLLA) On the Taylor expansion of λ-terms and the groupoid structure of their rigid approximants (Linearity/TLLA) From Linear Logic to Cyclic Sharing (Linearity/TLLA) Taking Linear Logic Apart (Linearity/TLLA) On the Lambek Calculus with an Exchange Modality (HOR) Orthogonality and sequentiality in substructural Linear HRSs (HOR) Normalization and Taylor expansion of lambda-terms (LOLA) A resource modality for RAII (ICLP) A New Proof-theoretical Linear Semantics for CHR
Linear polygraphs	(HDRA) Termination in linear (2,2)-categories with braidings and duals
Linear Programming	(ITP) A Coq Tactic for Equality Learning in Linear Arithmetic
Linear Temporal Logic	(DS-FM) Consistency Checking of Functional Requirements (CAV) Rabinizer 4: From LTL to Your Favourite Deterministic Automaton (CAV) Strix: Explicit Reactive Synthesis Strikes Back! (SYNT) Warm-Starting Fixed-Point Based Control Synthesis (SYNT) Reactive Synthesis from LTL Specification with Spot (LICS) One Theorem to Rule Them All: A Unified Translation of LTL into ω-Automata (LICS) Automaton-Based Criteria for Membership in CTL (SR) Local Equilibria in Logic-Based Multi-Player Games (ICLP) Temporal Answer Set Programming on Finite Traces
linear term	(Linearity/TLLA) How to count linear and affine closed lambda terms?
linear time hierarchy	(LICS) A parameterized halting problem, the linear time hierarchy, and the MRDP theorem
Linear Transformations	(IJCAR) A Reduction from Unbounded Linear Mixed Arithmetic Problems into Bounded Problems
Linear Tree Constraints	(LaSh) Decidable Linear Tree Constraints
linear-feedback shift register	(POS) Stedman and Erin Triples encoded as a SAT Problem
linear/non-linear logic	(Linearity/TLLA) On the Lambek Calculus with an Exchange Modality
Linearity	(DCM) Models of Computation that Conserve Data
linearizability	(CAV) Monitoring Weak Consistency
Linearization	(SMT) The next 10^4 UppSAT Approximations
Lipschitz maps	(Domains13) A logical view of complex analytic maps
Lists	(ADSL) The Complexity of Prenex Separation Logic with One Selector
Literate programming	(F-IDE) A Notebook Format for the Holistic Design of Embedded Systems
Liveness Analysis	(CAV) Symbolic Liveness Analysis of Real-World Software
LLVM	(CAV) Formal Verification of a Vehicle-to-Vehicle (V2V) Messaging System (FM) Statistical Model Checking of LLVM Code
Local determinism	(DCM) A Category Theoretic Interpretation of Gandy’s Principles for Mechanisms
Local Theory Extensions	(SYNT) On Inductive Verification and Synthesis
locale theory	(LICS) Computable decision making on the reals and other spaces via partiality and nondeterminism
Log analysis	(CSF) The Complexity of Monitoring Hyperproperties
logarithmic space computation	(LCC) Traversal-invariant definability and Logarithmic-space computation
logic	(TYDI) Nested sequents for modal logics and beyond (SCSC) RP: Unknot Recognition Through Quantifier Elimination (FM) IPL: An Integration Property Language for Multi-Model Cyber-Physical Systems (LaSh) A Logic of Information Flows (LCC) A recursion-theoretic characterisation of the positive polynomial-time functions (LICS) Logics for Word Transductions with Synthesis
logic for PTime	(LICS) On computability and tractability for infinite sets
Logic for Teaching	(ThEdu) Towards intuitive reasoning in axiomatic geometry
Logic Meta-Programming	(LPOP) LPOP2018 XSB Position Paper
Logic of Here and There	(ICLP) Temporal Answer Set Programming on Finite Traces
Logic on Trees	(LICS) Wreath Products of Distributive Forest Algebras
logic program	(ASPOCP) Partial Evaluation of Logic Programs in Vector Spaces
logic programming	(LPOP) LPOP2018 XSB Position Paper (FM) Variant Analysis with QL (ASPOCP) A Survey of Advances in Epistemic Logic Program Solvers (ASPOCP) Syntactic Conditions for Antichain Property in Consistency Restoring Prolog (ASPOCP) Datalog for Static Analysis Involving Logical Formulae (VEMDP) Rule-based design of computational DNA devices (IJCAR) Focussing, MALL and the polynomial hierarchy (RCRA) Shaving with Occam's Razor: Deriving Minimalist Theorem Provers for Minimal Logic (RCRA) Externally Supported Models for Efficient Computation of Paracoherent Answer Sets (ICLP) Top-down and Bottom-up Evaluation Procedurally Integrated (ICLP) Epistemic Logic Programs with World View Constraints
Logic Programming Applications	(RCRA) Logic Programming approaches for routing fault-free and maximally-parallel Wavelength Routed Optical Networks on Chip (Application paper)
Logic Solvers	(CAV) Understanding and Extending Incremental Determinization for 2QBF
Logic Tools	(ThEdu) Students' Proof Assistant (SPA) (ThEdu) Natural Deduction Assistant (NaDeA)
Logic-based tools	(ICLP-DC) Model Revision of Logical Regulatory Networks using Logic-based Tools
Logical complexity	(PARIS) On the Logical Complexity of Cyclic Arithmetic
logical design	(TERMGRAPH) Finding the Transitive Closure of Functional Dependencies using Strategic Port Graph Rewriting
logical formalism	(FCS) An Expressive, Flexible and Uniform Logical Formalism for Attribute-based Access Control
logical framework	(Linearity/TLLA) Formalization of Automated Trading Systems in a Concurrent Linear Framework
Logical Frameworks	(LFMTP) Sharing a library between proof assistants: reaching out to the HOL family (LICS) Strong Sums in Focused Logic (IJCAR) A Logical Framework with Commutative and Non-Commutative Subexponentials
Logical models	(WST) Well-founded models in proofs of termination
logical paradoxes	(LICS) Logical paradoxes in quantum computation
logical predicates	(LICS) Dialectica models of type theory
Logical Regulatory Networks	(ICLP-DC) Model Revision of Logical Regulatory Networks using Logic-based Tools
Logical relations	(FSCD) A Syntax for Higher Inductive-Inductive Types (FSCD) Index-Stratified Types
logically constrained term rewriting systems	(IJCAR) A Coinductive Approach to Proving Reachability in Logically Constrained Term Rewriting Systems
Logics for strategic reasoning	(SR) Verification of Multi-agent Systems with Imperfect Information and Public Actions
Logistics	(ICLP-DC) Scalable Robotic Intra-Logistics with Answer Set Programming
LOGSPACE	(FSCD) Term rewriting characterisation of LOGSPACE for finite and infinite data
LOIS	(LICS) On computability and tractability for infinite sets
long-distance resolution	(SAT) Local Soundness for QBF Calculi
loop unrolling	(ITP) Verified Timing Transformations in Synchronous Circuits with LambdaPi-Ware
loops	(VSTTE) Loop Detection by Logically Constrained Term Rewriting
low-level language	(VSTTE) A Java bytecode formalisation
Lower Bounds	(PC) Resolution with Counting: Different Moduli and Tree-Like Lower Bounds (PC) Resolution and the binary encoding of combinatorial principles (LICS) The State Complexity of Alternating Automata
LPMLN	(ICLP-DC) Probabalistic Action Language pBC+ (ICLP) A Probabilistic Extension of Action Language BC+
LPOD	(ICLP-DC) Translating P-log, LP^{MLN}, LPOD, and CR-Prolog2 into Standard Answer Set Programs (ICLP) Translating LPOD and CR-Prolog2 into Standard Answer Set Programs
LTI systems	(SYNT) Safe, Automated and Formal Synthesis of Digital Controllers for Continuous Plants
LTLf	(WiL) First-Order vs. Second-Order Encodings for LTLf-to-Automata Translation
lucas interpretation	(ThEdu) Lucas Interpretation from Programmers’ Perspective
Lukasiewicz Logics	(IJCAR) Probably Half True: Probabilistic Satisfiability over Lukasiewicz Infinitely-valued Logic
M
MAC	(CSF) Formal Security Proof of CMAC and its Variants
machine checked proofs	(IJCAR) Well-Founded Unions
Machine Ethics	(ReMOTE) Moral Permissibility of Actions in Smart Home Systems
Machine Learning	(CAV) Fast Numerical Program Analysis with Reinforcement Learning (Isabelle) PaMpeR: A Proof Method Recommendation System for Isabelle/HOL (IJCAR) A SAT-Based Approach to Learn Explainable Decision Sets (IJCAR) ATPboost: Learning Premise Selection in Binary Setting with ATP Feedback (Coq) Proof Construction by Tactic Learning (MLP) Answering Cloze-style Software Questions Using Stack Overflow (MLP) Deep Learning On Code with an Unbounded Vocabulary (MLP) Measuring software development productivity: a machine learning approach (SAT) Machine Learning-based Restart Policy for CDCL SAT Solvers (CSF) Privacy Risk in Machine Learning: Analyzing the Connection to Overfitting (ICLP) Cumulative Scoring-based Induction of Default Theories
Machine Learning Systems	(VaVAS) Policing Functions for Machine Learning Systems
machine words	(ITP) Fast Machine Words in Isabelle/HOL
magic states	(LICS) Logical paradoxes in quantum computation
Magic wand	(ADSL) The Complexity of Prenex Separation Logic with One Selector
MANET	(DS-FM) A Formal Study of MANET Routing Protocols
Maple	(SCSC) EA: SMT-like Queries in Maple
MapReduce	(ICLP) MASP-Reduce: a proposal for distributed computation of stable models
MapReduce framework	(VSTTE) Relational Equivalence Proofs Between Imperative and MapReduce Algorithms
MARCO	(SAT) Finding all Minimal Safe Inductive Sets
Markov Decision Process	(MoRe) Logically-Constrained Reinforcement Learning (MoRe) Safe and Optimal Scheduling of Hard and Soft Tasks
Markov decision processes	(MoRe) Multiple Objectives and Cost Bounds in MDP (MoRe) Multi-Scenario Uncertainty in Markov Decision Processes (CAV) Value Iteration for Simple Stochastic Games: Stopping Criterion and Learning Algorithm (CAV) Sound Value Iteration (CAV) Symbolic Algorithms for Graphs and Markov Decision Processes with Fairness Objectives (LICS) Distribution-based objectives for Markov Decision Processes (LICS) Stochastic Shortest Paths and Weight-Bounded Properties in Markov Decision Processes (LICS) Conditional Value-at-Risk for Reachability and Mean Payoff in Markov Decision Processes (ITP) MDP + TA = PTA: Probabilistic Timed Automata, Formalized (Short Paper) (VaVAS) Policy Generation with Probabilistic Guarantees for Long-term Autonomy of a Mobile Service Robot
Markov processes	(LICS) An algebraic theory of Markov processes
Martin-L\"{o}f type theory	(LICS) Impredicative Encodings of (Higher) Inductive Types
Martin-Löf type theory	(LICS) Dialectica models of type theory
Mason's Marks	(LPOP) A Rule-Based Tool for Analysis and Generation of Graphs Applied to Mason's Marks
Master Theorem	(ITP) Verified Tail Bounds for Randomized Programs
matching representation	(Domains13) T^\omega-representations of compact sets through dyadic subbases
mathematical analysis	(FSCD) Counting Environments and Closures
Mathematical Induction	(VSTTE) Extending VIAP to Handle Array Programs
Mathematical language	(UITP) Text-Orientated Formal Mathematics
mathematical proof	(ITP) Towards Verified Handwritten Calculational Proofs (Short Paper)
mathematical proofs	(WiL) Can every real proof be represented by a formal proof? The Hilbert-Gentzen thesis
Mathematics	(ITP) An Agda Formalization of Üresin & Dubois' Asynchronous Fixed-Point Theory
Matita	(LFMTP) Sharing a library between proof assistants: reaching out to the HOL family
Matrix Growth	(WST) A Perron-Frobenius Theorem for Jordan Blocks for Complexity Proving
Matrix Interpretation	(WST) A Perron-Frobenius Theorem for Jordan Blocks for Complexity Proving
Matrix semigroups	(LICS) Polynomial Invariants for Affine Programs
Maude	(FCS) Statistical Model Checking of Guessing and Timing Attacks on Distance-bounding Protocols
maximum realizability	(SYNT) Maximum Realizability for Linear Temporal Logic Specifications
Maximum Satisfiability	(IJCAR) Implicit Hitting Set Algorithms for Maximum Satisfiability Modulo Theories
MaxSAT	(SYNT) Maximum Realizability for Linear Temporal Logic Specifications (POS) Local-Style Search in the Linear MaxSAT Algorithm: A Computational Study of Solution-Based Phase Saving (POS) MLIC: A MaxSAT-Based framework for learning interpretable classification rules (SAT) Dynamic Polynomial Watchdog Encoding for Solving Weighted MaxSAT (SAT) Solving MaxSAT with Bit-Vector Optimization
MAXSAT application	(SAT) Approximately Propagation Complete and Conflict Propagating Constraint Encodings
MaxSAT resolution	(PC) On Dual-Rail Based MaxSAT Solving
MaxSAT solving	(PC) On Dual-Rail Based MaxSAT Solving
maxSMT	(IJCAR) MaedMax: A Maximal Ordered Completion Tool
MC-SAT	(SMT) Centralizing Equality Reasoning in MCSAT
MCMT	(IJCAR) Cubicle-W: Parameterized Model Checking on Weak Memory
mealy machine	(SYNT) Minimal Synthesis of String To String Functions From Examples
mean-payoff games	(LICS) A pseudo-quasi-polynomial algorithm for solving mean-payoff parity games (SR) Infinite-Duration Richman Bidding Games
meaningless terms	(FSCD) Strict Ideal Completions of the Lambda Calculus
Measure theory	(GS) Continuous probability distributions in concurrent games
mechanical reasoning	(CL&C) Validating Back-links of FOL-ID Cyclic Pre-proofs
mechanised theorem proving	(LICS) Quasi-Open Bisimilarity with Mismatch is Intuitionistic
mechanized mathematics	(ITP) A Formally Verified Solver for Homogeneous Linear Diophantine Equations
mechanized meta-theory	(LFMTP) Property-Based Testing of Abstract Machines: an Experience Report
Mechanized proofs	(WiL) Towards a Playground for Logicians
mechanized reasoning	(LICS) Cellular Cohomology in Homotopy Type Theory
Memoization	(ITP) Verified Memoization and Dynamic Programming
Memory	(ITP) Physical Addressing on Real Hardware in Isabelle/HOL
Memory consistency models	(PLR) RTLCheck: Automatically Verifying the Memory Consistency of Processor RTL (VSTTE) Store Buffer Reduction in The Presence of Mixed-Size Accesses and Misalignment
Memory Errors	(ICLP) Shape Neutral Analysis of Graph-based Data-structures
memory isolation	(AVOCS) Proof-Oriented Design of a Separation Kernel with Minimal Trusted Computing Base
memory model	(FM) Operational Semantics of a Weak Memory Model with Channel Synchronization
message passing concurrency	(CAV) On the Completeness of Verifying Message Passing Programs under Bounded Asynchrony
Message Passing Interface	(FM) Dynamic Symbolic Verification of MPI Programs
meta programming	(ITP) Tactics and Certificates in Meta Dedukti
meta-data library	(POS) A Problem Meta-Data Library for Research in SAT
Meta-Interpretive Learning	(ICLP) Exploiting Answer Set Programming with External Sources for Meta-Interpretive Learning
meta-programming	(ITP) Towards Certified Meta-Programming with Typed Template-Coq
Meta-theory	(WiL) Towards a Playground for Logicians
Metamorphic Testing	(VaVAS) Policing Functions for Machine Learning Systems
Metareasoning	(ITP) HOL Light QE
metatheory	(HoTT/UF) Geometric realization of truncated semi-simplicial sets meta-constructed within HoTT
Metric Semantics	(Domains13) Abstractness of Continuation Semantics for Asynchronous Concurrency
Minimal models	(HDRA) Minimal models for monomial algebras
Minimal unsatisfiability	(SAT) Minimal unsatisfiability and minimal strongly connected digraphs
Minimally Adequate Teacher	(LearnAut) Decision problems for Clark-congruential languages
Minimally strongly connected digraph	(SAT) Minimal unsatisfiability and minimal strongly connected digraphs
Minimisation	(IJCAR) An Assumption-Based Approach for Solving The Minimal S5-Satisfiability Problem
Minsky machines	(LOLA) Towards a library of formalised undecidable problems in Coq: The undecidability of intuitionistic linear logic
MIPS TLB	(ITP) Physical Addressing on Real Hardware in Isabelle/HOL
Mixed Arithmetic	(IJCAR) A Reduction from Unbounded Linear Mixed Arithmetic Problems into Bounded Problems
Mixed Distributive Law	(FSCD) Lifting Coalgebra Modalities and IMELL Model Structure to Eilenberg-Moore Categories
Mixed Integer Linear Programming	(RCRA) Optimal Fault-Tolerant Placement of Relay Nodes in a Mission Critical Wireless Network
ML	(IJCAR) Proof-Producing Synthesis of CakeML with I/O and Local State from Monadic HOL Functions (VSTTE) Program Verification in the Presence of I/O: Semantics, verified library routines, and verified applications
MMSNP	(LICS) A universal-algebraic proof of the complexity dichotomy for Monotone Monadic SNP
Mobile robotics	(VaVAS) Policy Generation with Probabilistic Guarantees for Long-term Autonomy of a Mobile Service Robot
modal fixpoint logic	(PARIS) Collapses of Fixpoint Alternation Hierarchies in Low Type-Levels of Higher-Order Fixpoint Logic
modal logic	(ARQNL) System Demonstration: The Higher-Order Prover Leo-III (LICS) A van Benthem Theorem for Fuzzy Modal Logic (LICS) Quasi-Open Bisimilarity with Mismatch is Intuitionistic (IJCAR) An Assumption-Based Approach for Solving The Minimal S5-Satisfiability Problem (IJCAR) The Higher-Order Prover Leo-III
Modal Logics	(WiL) On the Combination of Resolution and SAT Procedures for Modal Theorem-Proving (IJCAR) A Resolution-Based Calculus for Preferential Logics
modal mu	(LICS) A modal mu perspective on solving parity games in quasipolynomial time.
modal mu calculus	(ARQNL) Evidence Extraction from Parameterised Boolean Equation Systems
Modal type theory	(NLCS) Propositional Attitude Operators in Homotopy Type Theory (HoTT/UF) Dependent Right Adjoint Types
modalities	(FSCD) Internal Universes in Models of Homotopy Type Theory (LICS) Guarded Computational Type Theory (Linearity/TLLA) On the Lambek Calculus with an Exchange Modality
Model Animation	(FM) From Formal Requirements to Highly Assured Software for Unmanned Aircraft Systems
model checking	(CAV) Propositional Dynamic Logic for Higher-Order Functional Programs (CAV) Model Checking Quantitative Hyperproperties (CAV) BTOR2, BtorMC and Boolector 3.0 (CAV) The JKind Model Checker (CAV) Monitoring CTMCs By Multi-Clock Timed Automata (CAV) On the Completeness of Verifying Message Passing Programs under Bounded Asynchrony (CAV) Eager Abstraction for Symbolic Model Checking (CAV) Model Checking Boot Code from AWS Data Centers (CAV) Start Pruning When Time Gets Urgent: Partial Order Reduction for Timed Systems (CAV) SimpleCAR: An Efficient Bug-Finding Tool Based On Approximate Reachability (CAV) Constrained Dynamic Partial Order Reduction (CAV) Attracting Tangles to Solve Parity Games (FM) 20 Years of "Real" Real-Time Model Checking (FM) SDN-Actors: Modeling and Verification of SDN Programs (FM) IPL: An Integration Property Language for Multi-Model Cyber-Physical Systems (FM) Verifying Auto-Generated C Code from Simulink (FM) Stepwise Development and Model Checking of a Distributed Interlocking System - using RAISE (FM) View abstraction for systems with component identities (FM) Producing Explanations for Rich Logics (LaSh) Monadic Second-Order Model Checking with Fly-Automata (ASPOCP) Datalog for Static Analysis Involving Logical Formulae (SMT) Selfless Interpolation for Infinite-State Model Checking (AVOCS) Writing a Model Checker in 80 Days: Reusable Libraries and Custom Implementation (ReMOTE) Moral Permissibility of Actions in Smart Home Systems (LICS) Distribution-based objectives for Markov Decision Processes (ITP) Verifying the LTL to Büchi Automata Translation via Very Weak Alternating Automata (VaVAS) RoboTool: Modelling and Verification with RoboChart (SR) Verification of Multi-agent Systems with Imperfect Information and Public Actions (SR) Quantifying Bounds in Strategy Logic (SR) Strategy Logic with Imperfect Information (WPTE) Verification of Ada Programs with AdaHorn
Model Checking Games	(LaSh) Courcelle’s Theorem – A Game-Theoretic Approach
model construction	(IJCAR) Efficient Model Construction for Horn Logic with VLog: System Description
Model Counting	(CAV) Model Checking Quantitative Hyperproperties (IJCAR) A New Probabilistic Algorithm for Approximate Model Counting (SAT) Fast and Flexible Probabilistic Model Counting (PRUV) VolCE: An Efficient Tool for Solving #SMT(LA) Problems (PRUV) A New Probabilistic Algorithm for Approximate Model Counting
Model Expansion	(PRUV) A Model-Theoretic View on Preferences in Declarative Specifications of Search Problems
model finding	(FM) CompoSAT: Specification-Guided Coverage for Model Finding
model generation	(CAV) Model Generation for Quantified Formulas: A Taint-Based Approach
Model learning	(FM) Towards `Verifying' a Water Treatment System
Model quality	(ICLP) Improving Candidate Quality of Probabilistic Logic Models
Model Revision	(ICLP-DC) Model Revision of Logical Regulatory Networks using Logic-based Tools
model sampling	(SAT) Fast Sampling of Perfectly Uniform Satisfying Assignments
model theory	(LICS) A universal-algebraic proof of the complexity dichotomy for Monotone Monadic SNP (PRUV) A Model-Theoretic View on Preferences in Declarative Specifications of Search Problems
Model transformations	(Overture) Transforming an industrial case study from VDM++ to VDM-SL
model-based engineering	(FM) IPL: An Integration Property Language for Multi-Model Cyber-Physical Systems
model-based testing	(FM) Model-Based Testing for Avionics Systems (ITP) Fast Machine Words in Isabelle/HOL
model-checking	(FM) Timed Vacuity (VaVAS) Social Consequence Engines (Abstract)
Model-checking first-order logic	(LICS) Parameterized circuit complexity of model-checking on sparse structures
model-checking problems	(LICS) Tree depth, quantifier elimination, and quantifier rank
Model-level uncertainty	(MoRe) Multi-Scenario Uncertainty in Markov Decision Processes
Modeling	(VEMDP) Rule-based design of computational DNA devices
Modeling and Specification	(CSF) KEVM: A Complete Formal Semantics of the Ethereum Virtual Machine
Modelling Languages	(QBF) A Grounder From Second-Order Logic To QBF
modelling secure protocols	(CSF) Computer-aided proofs for multiparty computation with active security
models	(IJCAR) Theories as Types
Models of computation	(DCM) A Category Theoretic Interpretation of Gandy’s Principles for Mechanisms
Modular Analysis	(ICLP) Towards Incremental and Modular Context-sensitive Analysis
modular approach	(FM) Modular Verification of Programs with Effects and Effect Handlers in Coq
Modular Arithmetic	(CAV) Formally Verified Montgomery Multiplication
Modular System	(LaSh) A Logic of Information Flows
Modular Tensor Category	(DCM) Towards a Formal System for Topological Quantum Computation
modules	(LICS) Strong Sums in Focused Logic
Molecular computing	(VEMDP) Noise control for molecular computing
Molecular Filters	(VEMDP) Molecular Filters for Noise Reduction
Molecular programming	(VEMDP) Rule-based design of computational DNA devices
monad	(LICS) Syntax and Semantics for Operations with Scopes (MSFP) Relating Idioms, Arrows and Monads from Monoidal Adjunctions (Linearity/TLLA) On the Lambek Calculus with an Exchange Modality
Monadic Second Order Logic	(LaSh) Courcelle’s Theorem – A Game-Theoretic Approach (LaSh) Monadic Second-Order Model Checking with Fly-Automata
Monads	(NLCS) Propositional Attitude Operators in Homotopy Type Theory (Coq) What is the Foreign Function Interface of the Coq Programming Language? (MSFP) Some No-Go Theorems for Distributive Laws (extended abstract)
monitoring	(LICS) A Theory of Register Monitors
monoid	(MSFP) Relating Idioms, Arrows and Monads from Monoidal Adjunctions
monoid model	(Domains13) A Brouwerian proof of the Fan Theorem
monoidal categories	(FSCD) A diagrammatic axiomatisation of fermionic quantum circuits (LICS) Compositional game theory (LICS) Two complete axiomatisations of pure-state qubit quantum computing (HDRA) Normal forms for planar connected string diagrams (Linearity/TLLA) From Linear Logic to Cyclic Sharing
monoidal category	(MSFP) Relating Idioms, Arrows and Monads from Monoidal Adjunctions
Monoidal Coalgebra Modality	(FSCD) Lifting Coalgebra Modalities and IMELL Model Structure to Eilenberg-Moore Categories
monotone	(PC) Complexity of expander-based reasoning and the power of monotone proofs
Monotone complexity	(PC) Towards theories for positive polynomial time and monotone proofs with extension (LCC) A recursion-theoretic characterisation of the positive polynomial-time functions
Monotone proofs	(PC) Towards theories for positive polynomial time and monotone proofs with extension
monotonicity	(NLCS) Automated Reasoning from Polarized Parse Trees
Montague semantics	(NLCS) Do different syntactic trees yield different logical readings? Some remarks on head variables in typed lambda calculus.
Montgomery Multiplication	(CAV) Formally Verified Montgomery Multiplication
MPI	(DS-FM) Analysis and Verification of Message Passing based Parallel Programs
MSO	(WiL) First-Order vs. Second-Order Encodings for LTLf-to-Automata Translation (LaSh) A Derivative-Based Decision Procedure for WS1S (LaSh) Monadic Second-Order Model Checking with Fly-Automata (LICS) MSO Queries on Trees: Enumerating Answers under Updates Using Forest Algebras
MSO on Infinite Words	(PARIS) LMSO: A Curry-Howard Approach to Church’s Synthesis via Linear Logic (speaker: Pierre PRADIC)
MSO on omega-Words	(LICS) LMSO: A Curry-Howard Approach to Church's Synthesis via Linear Logic
MSO transduction	(LICS) Regular and First Order List Functions
mu-calculus	(FM) Producing Explanations for Rich Logics
mu-mutilde-calculus	(CL&C) The “duality of computation” from a fibrational perspective
Multi Factor	(CSF) An extensive formal analysis of multi-factor authentication protocols
Multi Modal logic	(EICNCL) Sequent Calculi for Logic that Includes an Infinite Number of Modalities
Multi-agent models	(EICNCL) Hypersequent calculus for the logic of conditional belief: preliminary results
Multi-agent Systems	(SR) Verification of Multi-agent Systems with Imperfect Information and Public Actions (SR) Local Equilibria in Logic-Based Multi-Player Games
Multi-agent workflows	(CSF) Inductive Invariants for Noninterference in Multi-agent Workflows
Multi-clock timed automata	(CAV) Monitoring CTMCs By Multi-Clock Timed Automata
Multi-dimensional	(VSTTE) Extending VIAP to Handle Array Programs
Multi-graphs	(TERMGRAPH) Drags: an algebraic framework for graph rewriting
multi-modelling	(Overture) Multi-modelling of Cooperative Swarms (Overture) Design Space Exploration for Secure Building Control
multi-objective optimization	(LICS) Conditional Value-at-Risk for Reachability and Mean Payoff in Markov Decision Processes
Multi-objective synthesis	(MoRe) Safe and Optimal Scheduling of Hard and Soft Tasks
Multi-party computation	(CSF) Enforcing ideal-world leakage bounds in real-world secret sharing MPC frameworks
Multi-Pass Dynamic Programming	(SAT) Exploiting Treewidth for Projected Model Counting and its Limits
Multi-player games	(SR) Local Equilibria in Logic-Based Multi-Player Games
Multi-Robot planning	(FM) Multi-Robot LTL Planning Under Uncertainty
Multi-valued Logic	(IJCAR) Probably Half True: Probabilistic Satisfiability over Lukasiewicz Infinitely-valued Logic
multicategories	(HDRA) Merge-bicategories: towards semi-strictification of higher categories
multiplayer games	(MoRe) Constraint Problem for Weak Subgame Perfect Equilibria with omega-regular Boolean Objectives
multiple languages	(LearnAut) Learning Several Languages from Labeled Strings: State Merging and Evolutionary Approaches
multiplicative linear logic	(Linearity/TLLA) Proof nets, coends and the Yoneda isomorphism
Multiplier Verification	(SCSC) RP: A Practical Polynomial Calculus for Arithmetic Circuit Verification
multitope	(HDRA) The equivalence between opetopic sets and many-to-one polygraphs
muMALL	(PARIS) Local Validity for Circular Proofs in Linear Logic with Fixed Points
N
N player games	(LICS) Rational Synthesis Under Imperfect Information
nanoCoP	(PAAR) Proof Search Optimizations for Non-clausal Connection Calculi
Nanofabricated Devices	(VEMDP) Formal Verification of Network-Based Biocomputation Circuits
narrowing	(WPTE) On Transforming Narrowing Trees into Regular Tree Grammars Generating Ranges of Substitutions
Nash equilibria	(SR) Compositional Game Theory
Nash equilibrium	(LICS) Rational Synthesis Under Imperfect Information (SR) Local Equilibria in Logic-Based Multi-Player Games
Natural deduction	(ITRS) Natural Deduction and Normalization Proofs for the Intersection Type Discipline (ThEdu) Natural Deduction Assistant (NaDeA) (PAAR) Efficient translation of sequent calculus proofs into natural deduction proofs (CL&C) On Natural Deduction for Herbrand Constructive Logics III: The Strange Case of the Intuitionistic Logic of Constant Domains
Natural language	(UITP) Text-Orientated Formal Mathematics
natural language processing	(NLCS) Anti-Unification and Natural Language Processing (NLCS) OpenWordNet-PT: Taking Stock (MLP) Answering Cloze-style Software Questions Using Stack Overflow (MLP) Deep Learning On Code with an Unbounded Vocabulary
natural language understanding	(ICLP-DC) The Learning-Knowledge-Reasoning Paradigm For Natural Language Understanding and Question Answering (NLCS) OpenWordNet-PT: Taking Stock (ICLP) An ASP Methodology for Understanding Narratives about Stereotypical Activities
Natural mathematical language	(ThEdu) Towards intuitive reasoning in axiomatic geometry
natural proofs	(LCC) Feasibly constructive proofs of succinct weak circuit lower bounds
Natural-style Proofs	(SCSC) EA: Techniques for Natural-style Proofs in Elementary Analysis
Negation as failure	(ICLP) Cumulative Scoring-based Induction of Default Theories
Negation in Logic Programming	(ICLP) Approximation Fixpoint Theory and the Well-Founded Semantics of Higher-Order Logic Programs
Negative translations	(LICS) Around Classical and Intuitionistic Linear Logics
neighbourhood semantics	(EICNCL) Toward intuitionistic non-normal modal logic and its calculi
neighbourhood singleton arc consistency	(RCRA) Partial (Neighbourhood) Singleton Arc Consistency for Constraint Satisfaction Problems
Nelson-Oppen	(IJCAR) Complexity of Combinations of Qualitative Constraint Satisfaction Problems
Nested	(VSTTE) Extending VIAP to Handle Array Programs
nested sequents	(TYDI) Nested sequents for modal logics and beyond
nested systems	(TYDI) Sequentialising nested systems (WiL) A semantical view of sequent based systems
Network Based Biocomputation	(VEMDP) Formal Verification of Network-Based Biocomputation Circuits
Network Intrusion Detection	(FCS) LISA: Predicting the Impact of DoS Attacks on Real-World Low Power IoT Systems
Network-free simulation	(VEMDP) Rule-Based Gillespie Simulation of Chemical Systems
networks of synchronized automata	(AVOCS) Using SMT engine to generate Symbolic Automata
neural network	(DS-FM) Formal verification of neural networks
neural networks	(PAAR) Dynamic Strategy Priority: Empower the strong and abandon the weak
Newman's lemma	(IWC) Critical pairs for Gray categories
next state relation	(IJCAR) A FOOLish Encoding of the Next State Relations of Imperative Programs
no-go theorem	(MSFP) Some No-Go Theorems for Distributive Laws (extended abstract)
Noise Reduction	(VEMDP) Molecular Filters for Noise Reduction
nominal rewriting	(UNIF) Rewriting with Generalized Nominal Unification
nominal terms	(FSCD) Fixed-Point Constraints for Nominal Equational Unification
nominal unification	(FSCD) Fixed-Point Constraints for Nominal Equational Unification (FSCD) Nominal Unification with Atom and Context Variables (UNIF) Rewriting with Generalized Nominal Unification
nominalizations	(NLCS) OpenWordNet-PT: Taking Stock
non-clausal theorem proving	(PAAR) Proof Search Optimizations for Non-clausal Connection Calculi
non-cnf	(SAT) Circuit-based Search Space Pruning in QBF
non-commutative	(Linearity/TLLA) On the Lambek Calculus with an Exchange Modality
non-denoting terms	(ARQNL) Labelled Calculi for QMLs with Non-Rigid and Non-Denoting Terms
Non-Deterministic Automata	(LICS) One Theorem to Rule Them All: A Unified Translation of LTL into ω-Automata
non-deterministic mealy machine	(SYNT) Minimal Synthesis of String To String Functions From Examples
non-idempotency	(LICS) Every λ-Term is Meaningful for the Infinitary Relational Model
non-idempotent intersection types	(ITRS) Towards a Semantic Measure of the Execution Time in Call-by-Value lambda-Calculus
Non-interference	(CSF) Inductive Invariants for Noninterference in Multi-agent Workflows
Non-interleaving semantics	(CAV) Quasi-Optimal Partial Order Reduction
Non-lawlike computability	(LICS) Computability Beyond Church-Turing via Choice Sequences
non-linear arithmetic	(SCSC) EA: Wrapping Computer Algebra is Surprisingly Successful for Non-Linear SMT
Non-linear Real Arithmetic	(SCSC) RP: Non-linear Real Arithmetic Benchmarks derived from Automated Reasoning in Economics
Non-monotonic Reasoning	(RCRA) Externally Supported Models for Efficient Computation of Paracoherent Answer Sets
non-normal modal logic	(EICNCL) Toward intuitionistic non-normal modal logic and its calculi
non-normal modal logics	(EICNCL) Proof theory for quantified monotone modal logics
non-rigid terms	(ARQNL) Labelled Calculi for QMLs with Non-Rigid and Non-Denoting Terms
Non-Termination Bugs	(CAV) Symbolic Liveness Analysis of Real-World Software
Non-termination Proving	(CAV) Syntax-Guided Termination Analysis
Non-wellfounded proofs	(PARIS) Local Validity for Circular Proofs in Linear Logic with Fixed Points (CL&C) Some ideas on cut-elimination for cyclic arithmetic proofs
non-zero sum games	(LICS) Rational Synthesis Under Imperfect Information
nondeterminism	(LPOP) A software system should be declarative except where it interacts with the real world (DCM) Generic Graph Semantics (LICS) Classical realizability as a classifier for nondeterminism
nonlinear integer arithmetic	(IJCAR) A Why3 framework for reflection proofs and its application to GMP's algorithms (SAT) Experimenting on Solving Nonlinear Integer Arithmetic with Incremental Linearization
NonMonotonic Semantics	(ICLP) Declarative Algorithms in Datalog with Aggregates: user-friendly formal semantics conducive to performance and scalability
nonmonotonic term orders	(IJCAR) Superposition for Lambda-Free Higher-Order Logic
nonnegativity certificate	(PC) Optimization over the Boolean Hypercube via Sums of Nonnegative Circuit Polynomials
nontermination	(VSTTE) Loop Detection by Logically Constrained Term Rewriting
Normal Form	(PAAR) Evaluating Pre-Processing Techniques for the Separated Normal Form for Temporal Logics
normal form bisimulation	(ITP) A Formal Equational Theory for Call-by-Push-Value
normal forms	(HDRA) Normal forms for planar connected string diagrams
normalisation	(FSCD) Strict Ideal Completions of the Lambda Calculus (TYDI) Two Unifying Structural Principles
Normalization	(ITRS) Natural Deduction and Normalization Proofs for the Intersection Type Discipline (HOR) Normalization and Taylor expansion of lambda-terms
norms	(VaVAS) Social Consequence Engines (Abstract)
Notation	(LFMTP) What Does This Notation Mean Anyway? BNF-style notation as it is actually used (Coq) Teaching Your Rooster to Crow in C
Notebooks	(F-IDE) A Notebook Format for the Holistic Design of Embedded Systems
novel applications domains	(SAT) Constrained Image Generation Using Binarized Neural Networks with Decision Procedures
Nowhere dense graphs	(LICS) On the number of types in sparse graphs
Numerical optimization	(MLP) Difflog: Beyond Deductive Methods in Program Analysis
Numerical Program Analysis	(CAV) Fast Numerical Program Analysis with Reinforcement Learning
Nuprl	(WiL) On Expanding Standard Notions of Constructivity
Nuprl proof assistant	(LICS) Computability Beyond Church-Turing via Choice Sequences
nuxmv	(AVOCS) A Framework for the Formal Verification of Networks of Railway Interlockings - Application to the Belgian Railways
O
o-minimality	(MoRe) Stochastic o-minimal hybrid systems
OBDD	(PC) Branching Program Complexity of Canonical Search Problems and Proof Complexity of Formulas
Object Constraint Language (OCL)	(LPOP) Security Policies in Constraint Handling Rules
object-oriented	(FM) Object-Oriented Security Proofs
Object-oriented programs	(FM) A lightweight deadlock analysis technique of object-oriented programs
observational equivalence	(LICS) Probabilistic Böhm Trees and Probabilistic Separation (ITP) A Formal Equational Theory for Call-by-Push-Value (WPTE) Automating the Diagram Method to Prove Correctness of Program Transformations
OCaml library	(LFMTP) Abstract Representation of Binders in OCaml using the Bindlib Library
Ocra	(AVOCS) A Framework for the Formal Verification of Networks of Railway Interlockings - Application to the Belgian Railways
odd-even network	(POS) Competitive Sorter-based Encoding of PB-Constraints into SAT
omega-automata	(SYNT) Reactive Synthesis from LTL Specification with Spot
omega-languages	(FM) A Weakness Measure for GR(1) Formulae (LICS) A Theory of Register Monitors
Omega-regular languages	(LICS) Automaton-Based Criteria for Membership in CTL
omega-regular objectives	(MoRe) Parameterized complexity of games with monotonically ordered omega-regular objectives (MoRe) Constraint Problem for Weak Subgame Perfect Equilibria with omega-regular Boolean Objectives
OMT	(SMT) Puli - A Problem-Specific OMT Solver
Online Decomposition	(CAV) Fast Numerical Program Analysis with Reinforcement Learning
Online Social Networks	(FM) Timed Epistemic Knowledge Bases for Social Networks
ontologies	(IJCAR) FAME: An Automated Tool for Semantic Forgetting in Expressive Description Logics
Ontology	(ICLP-DC) Natural Language Generation From Ontologies
Ontology Languages	(PRUV) Leveraging Probabilistic Existential Rules for Adversarial Deduplication
Ontology Reasoning	(ICLP) Natural Language Generation From Ontologies: Application Paper
open games	(LICS) Compositional game theory (SR) Compositional Game Theory
open set lattice	(Domains13) Invited Talk: Topology and Domain Theory Interfaces
Open-WBO	(SAT) Using Combinatorial Benchmarks to Probe the Reasoning Power of Pseudo-Boolean Solvers
OpenFlow	(FM) SDN-Actors: Modeling and Verification of SDN Programs
OpenJDK	(F-IDE) Experience Report on Formally Verifying Parts of OpenJDK's API with KeY
OpenJML	(VSTTE) Practical Methods for Reasoning about Java 8's Functional Programming Features
OpenTheory	(LFMTP) Sharing a library between proof assistants: reaching out to the HOL family
Operad	(HDRA) Generalizations of the associative operad and convergent rewrite systems (Linearity/TLLA) Generalized generalized species of structure and resource modalities
Operating System Verification	(ITP) Program Verification in the Presence of Cached Address Translation
operational semantics	(FM) Operational Semantics of a Weak Memory Model with Channel Synchronization (FM) A wide-spectrum language for verification of programs on weak memory models (CSF) KEVM: A Complete Formal Semantics of the Ethereum Virtual Machine (Linearity/TLLA) The Bang Calculus and the Two Girard's Translations (LOLA) A more precise, more correct stack and register model for CompCert (WPTE) Reducing Total Correctness to Partial Correctness by a Transformation of the Language Semantics
Operational Termination	(WST) Well-founded models in proofs of termination
opetope	(HDRA) The equivalence between opetopic sets and many-to-one polygraphs
Optical Networks on Chip	(RCRA) Logic Programming approaches for routing fault-free and maximally-parallel Wavelength Routed Optical Networks on Chip (Application paper)
optimal propagation	(SAT) Approximately Propagation Complete and Conflict Propagating Constraint Encodings
Optimal Scheduling	(ICLP) Optimal Scheduling for Exposed Datapath Architectures with Buffered Processing Units by ASP
Optimal Upper Bound	(LICS) A Simple and Optimal Complementation Algorithm for Büchi Automata
Optimisation	(Overture) Design Space Exploration for Secure Building Control (RCRA) Optimal Fault-Tolerant Placement of Relay Nodes in a Mission Critical Wireless Network (RCRA) Greedy Randomized Search for Scalable Compilation of Quantum Circuits
optimization	(DS-FM) Formal verification of neural networks (CAV) Delta-Decision Procedures for Exists-Forall Problems over the Reals
Optimization heuristics	(MoRe) Multi-Scenario Uncertainty in Markov Decision Processes
Optimization Modulo Bit-Vectors	(SAT) Solving MaxSAT with Bit-Vector Optimization
optimization techniques	(PAAR) Proof Search Optimizations for Non-clausal Connection Calculi
optimizations	(ITP) A Formal Equational Theory for Call-by-Push-Value
OR causality	(LICS) Concurrency and Probability: Removing Confusion, Compositionally
oracle Turing machines	(LICS) Type-two polynomial-time and restricted lookahead.
Order enriched categories	(Domains13) Extending Stone Duality to Relations
order invariant definability	(LCC) Traversal-invariant definability and Logarithmic-space computation
order theory	(SR) Beyond admissibility: Dominance between chains of strategies
order-preserving embeddings	(MSFP) Everybody's Got To Be Somewhere
ordered completion	(IWC) Certified Ordered Completion
ordered objectives	(MoRe) Parameterized complexity of games with monotonically ordered omega-regular objectives
ordered structures	(HoTT/UF) Ordered Cubes
ordering	(UNIF) Unification based on generalized embedding
ordinal diagram system	(TERMGRAPH) On quasi ordinal diagram systems
Ordinary differential equation	(CAV) Monitoring CTMCs By Multi-Clock Timed Automata
ordinary differential equations	(FM) Vector Barrier Certificates and Comparison Systems
Origin	(LICS) Logics for Word Transductions with Synthesis
over-approximation	(FSCD) Completeness of Tree Automata Completion
overt set	(Domains13) T^\omega-representations of compact sets through dyadic subbases
Overture	(Overture) Integrating VDM-SL into the continuous delivery pipelines of cloud-based software (Overture) VDM at large: analysing the EMV Next Generation Kernel (Overture) Overture FMU: Export VDM-RT Models as Tool-Wrapper FMUs
P
Paracoherent Answer Sets	(RCRA) Externally Supported Models for Efficient Computation of Paracoherent Answer Sets
Paraconsistent logic	(ARQNL) Formalization of a Paraconsistent Infinite-Valued Logic
Parallel computation	(DCM) A Category Theoretic Interpretation of Gandy’s Principles for Mechanisms
parallel improvements	(WPTE) Optimizing Space of Parallel Processes
Parallel Processing	(POS) Tuning Parallel SAT Solvers
Parallel Zielonka's Algorithm	(PLR) An Efficient Zielonka's Algorithm for Parallel Parity Games
parallelism	(ICLP) MASP-Reduce: a proposal for distributed computation of stable models
parameter optimization	(POS) CryptoMiniSat Parameter-Optimization for Solving Cryptographic Instances
parameter-free axioms	(PC)
parameterised Boolean equation systems	(ARQNL) Evidence Extraction from Parameterised Boolean Equation Systems
Parameterised verification problem	(FM) View abstraction for systems with component identities
parameterized AC^0	(LICS) Tree depth, quantifier elimination, and quantifier rank (LICS) A parameterized halting problem, the linear time hierarchy, and the MRDP theorem
Parameterized Algorithms	(SAT) Exploiting Treewidth for Projected Model Counting and its Limits
parameterized complexity	(SAT) QBF as an Alternative to Courcelle's Theorem
Parameterized Model Checking	(IJCAR) Cubicle-W: Parameterized Model Checking on Weak Memory
parameterized systems	(CAV) Eager Abstraction for Symbolic Model Checking
Parameterized verification	(CAV) Peregrine: A Tool for the Analysis of Population Protocols (HCVS) Declarative Parameterized Verification of Topology-sensitive Distributed Protocols
Parametricity	(LICS) A General Framework for Relational Parametricity (LICS) Degrees of Relatedness - A Unified Framework for Parametricity, Irrelevance, Ad Hoc Polymorphism, Intersections, Unions and Algebra in Dependent Type Theory (Coq) What is the Foreign Function Interface of the Coq Programming Language? (ITP) Relational Parametricity and Quotient Preservation for Modular (Co)Datatypes
parametrized systems	(FM) Formal Specification and Verification of Dynamic Parametrized Architectures
Parity Game	(CAV) Strix: Explicit Reactive Synthesis Strikes Back! (CAV) Attracting Tangles to Solve Parity Games
parity games	(PLR) An Efficient Zielonka's Algorithm for Parallel Parity Games (SYNT) Reactive Synthesis from LTL Specification with Spot (LICS) A pseudo-quasi-polynomial algorithm for solving mean-payoff parity games (LICS) A modal mu perspective on solving parity games in quasipolynomial time. (SR) Dependences in Strategy Logic (SR) Infinite-Duration Richman Bidding Games (SR) Solving Parity Games: Explicit vs Symbolic
parsing	(NLCS) OpenWordNet-PT: Taking Stock (VSTTE) A Formalization of the ABNF Notation and a Verified Parser of ABNF Grammars
Partial algorithms in Coq	(ITP) Proof Pearl: Constructive Extraction of Cycle Finding Algorithms
partial correctness	(WPTE) Reducing Total Correctness to Partial Correctness by a Transformation of the Language Semantics
Partial Evaluation	(ASPOCP) Partial Evaluation of Logic Programs in Vector Spaces (WST) Control-Flow Refinement via Partial Evaluation
Partial Functions	(ICLP) Functional ASP with Intensional Sets; Application to Gelfond-Zhang Agreggates
Partial models	(FM) Multi-Robot LTL Planning Under Uncertainty
partial order reduction	(CAV) Partial Order Aware Concurrency Sampling (CAV) Start Pruning When Time Gets Urgent: Partial Order Reduction for Timed Systems (FM) SDN-Actors: Modeling and Verification of SDN Programs
Partial-order reduction	(CAV) Quasi-Optimal Partial Order Reduction
path orderings	(WST) GPO: A Path Ordering for Graphs
pattern matching	(Isabelle) Lazy Algebraic Types in Isabelle/HOL
paycheck pronouns	(NLCS) Paychecks, Presupposition, and Dependent Types
PB constraints	(RCRA) Encoding PB Constraints into SAT via Binary Adders and BDDs -- Revisited
PDL	(LICS) Wreath Products of Distributive Forest Algebras
PDR	(SMT) Discovering Universally Quantified Solutions for Constrained Horn Clauses (SAT) Finding all Minimal Safe Inductive Sets
PDR-Z3	(WPTE) Verification of Ada Programs with AdaHorn
Peano arithmetic	(PARIS) On the Logical Complexity of Cyclic Arithmetic (CL&C) Some ideas on cut-elimination for cyclic arithmetic proofs
Perfect masking	(CAV) SCInfer: Refinement-based Verification of Software Countermeasures against Side-Channel Attacks
perfect samplers	(SAT) Fast Sampling of Perfectly Uniform Satisfying Assignments
permission inference	(CAV) Permission Inference for Array Programs
permission model	(CSF) A Permission-Dependent Type System for Secure Information Flow Analysis
Permissions	(ADSL) A Complete Proof System for Basic Symbolic Heaps with Permissions
Permutation problems	(RCRA) Algebraic Crossover Operators for Permutations
permutations	(Coq) Preliminary Report on the Yalla Library
Persistent places	(LICS) Concurrency and Probability: Removing Confusion, Compositionally
Petri nets	(LICS) Concurrency and Probability: Removing Confusion, Compositionally
PGA	(MLP) Splitting source code identifiers using Bidirectional LSTM Recurrent Neural Network
phase saving	(POS) Local-Style Search in the Linear MaxSAT Algorithm: A Computational Study of Solution-Based Phase Saving
Phylostatic	(ICLP) Natural Language Generation From Ontologies: Application Paper
Phylotastic	(ICLP-DC) Natural Language Generation From Ontologies
pi calculus	(LICS) Eager Functions as Processes
pi-caclulus	(WiL) A New Linear Logic for Deadlock-Free Session-Typed Processes (Talk Abstract)
Pi-calculus	(DCM) Pointing to Private Names (LICS) Quasi-Open Bisimilarity with Mismatch is Intuitionistic
Picat	(LPOP) A Picat-based XCSP Solver - from Parsing, Modeling, to SAT Encoding
Picture Series	(LearnAut) Learning Graph Weighted Models on Pictures
Planning	(ICLP-DC) Scalable Robotic Intra-Logistics with Answer Set Programming (VaVAS) Social Consequence Engines (Abstract) (RCRA) Greedy Randomized Search for Scalable Compilation of Quantum Circuits (ICLP) Phylotastic: An Experiment in Creating, Manipulating, and Evolving Phylogenetic Biology Workflows Using Logic Programming
Planning under uncertainty	(MoRe) Multiple Objectives and Cost Bounds in MDP
Plotkin's T	(Domains13) T^\omega-representations of compact sets through dyadic subbases
PMCFG	(NLCS) Automatic test suite generation for PMCFG grammars
pointer arithmetic	(ADSL) On the Complexity of Pointer Arithmetic in Separation Logic
pointfree topology	(LICS) Computable decision making on the reals and other spaces via partiality and nondeterminism
polarity	(NLCS) Automated Reasoning from Polarized Parse Trees
Policing function	(VaVAS) Policing Functions for Machine Learning Systems
policy language	(FCS) An Expressive, Flexible and Uniform Logical Formalism for Attribute-based Access Control
Policy Synthesis	(MoRe) Logically-Constrained Reinforcement Learning
polycategories	(HDRA) Merge-bicategories: towards semi-strictification of higher categories
polygraph	(FSCD) Coherence of Gray categories via rewriting (HDRA) The equivalence between opetopic sets and many-to-one polygraphs
polygraphs	(HDRA) Merge-bicategories: towards semi-strictification of higher categories
Polyhedra Domain Analysis	(CAV) Fast Numerical Program Analysis with Reinforcement Learning
Polymers	(VEMDP) Conservative approximations of polymers
polymorphism	(SMT) Alt-Ergo 2.2 (LICS) Impredicative Encodings of (Higher) Inductive Types
Polynomial Calculus	(SCSC) RP: A Practical Polynomial Calculus for Arithmetic Circuit Verification
Polynomial Factorization	(ITP) A Formalization of the LLL Basis Reduction Algorithm
polynomial functor	(LICS) Dialectica models of type theory
Polynomial functors	(LICS) What's in a game? A theory of game models (HoTT/UF) Algebraic models of dependent type theory
Polynomial hierarchy	(IJCAR) Focussing, MALL and the polynomial hierarchy
polynomial simulation	(PC) On Dual-Rail Based MaxSAT Solving
polynomial upper bounds	(PC) On Dual-Rail Based MaxSAT Solving
polynomial-time tractability	(LICS) A universal-algebraic proof of the complexity dichotomy for Monotone Monadic SNP
polytyptic programming	(ITP) Relational Parametricity and Quotient Preservation for Modular (Co)Datatypes
population protocols	(CAV) Peregrine: A Tool for the Analysis of Population Protocols
port graphs	(TERMGRAPH) Finding the Transitive Closure of Functional Dependencies using Strategic Port Graph Rewriting
Portfolio	(QBF) Portfolio-Based Algorithm Selection for Circuit QBFs
Portfolio Solver	(POS) Tuning Parallel SAT Solvers
Positive complexity	(LCC) A recursion-theoretic characterisation of the positive polynomial-time functions
Post Correspondence Problem	(ITP) Verification of PCP-Related Computational Reductions in Coq (LOLA) Towards a library of formalised undecidable problems in Coq: The undecidability of intuitionistic linear logic
power-law	(SAT) Sharpness of the Satisfiability Threshold for Non-Uniform Random k-SAT
powerlocale	(Domains13) Applications of entailments: de Groot duality
precision medicine	(RCRA) Computing Personalised Treatments through In Silico Clinical Trials. A Case Study on Downregulation in Assisted Reproduction.
precondition inference	(ICLP) An iterative approach to precondition inference using constrained Horn clauses
predecessor function	(ITP) Efficient Mendler-Style Lambda-Encodings in Cedille
predicate	(ICLP) Constraint Answer Set Programming without Grounding
Predicate Abstraction	(FM) Deadlock Detection for Actor-based Coroutines
preference	(ICLP-DC) Translating P-log, LP^{MLN}, LPOD, and CR-Prolog2 into Standard Answer Set Programs (PRUV) Evidential Group Decision Making Model with Belief-Based Preferences (ICLP) Introspecting Preferences In Answer Set Programming
Preference Logic	(PRUV) A new logic for jointly representing hard and soft constraints
Preference Modeling	(PRUV) A Model-Theoretic View on Preferences in Declarative Specifications of Search Problems
Preferential logics	(IJCAR) A Resolution-Based Calculus for Preferential Logics (PRUV) Reasoning about exceptions in ontologies: from the lexicographic closure to the skeptical closure
prefix-constrained term rewriting	(FSCD) Confluence of Prefix-Constrained Rewrite Systems
premature convergence	(RCRA) An Enhanced Genetic Algorithm with the BLF2G Guillotine Placement Heuristic for the Orthogonal Cutting-Stock Problem
preprocessing	(PAAR) Evaluating Pre-Processing Techniques for the Separated Normal Form for Temporal Logics (IJCAR) QRAT+: Generalizing QRAT by a More Powerful QBF Redundancy Property
presheaf models	(HoTT/UF) Internalizing Presheaf Semantics: Charting the Design Space
presheaf semantics	(LICS) Degrees of Relatedness - A Unified Framework for Parametricity, Irrelevance, Ad Hoc Polymorphism, Intersections, Unions and Algebra in Dependent Type Theory
Presheaves	(LICS) What's in a game? A theory of game models
presupposition	(NLCS) Paychecks, Presupposition, and Dependent Types
pretty printing	(Coq) Teaching Your Rooster to Crow in C
primary key	(IJCAR) Automated Reasoning about Key Sets
Prime Numbers	(LICS) The State Complexity of Alternating Automata
priorities	(WiL) A New Linear Logic for Deadlock-Free Session-Typed Processes (Talk Abstract)
prism	(MSFP) Profunctor Optics and the Yoneda Lemma
Privacy	(FM) Timed Epistemic Knowledge Bases for Social Networks (CSF) Privacy Risk in Machine Learning: Analyzing the Connection to Overfitting (CSF) Enforcing ideal-world leakage bounds in real-world secret sharing MPC frameworks
Privacy by design	(VSTTE) Constructing Independently Verifiable Privacy-Compliant Type Systems for Message Passing between Black-Box Components
Privacy-type properties	(CAV) The DEEPSEC prover
proactive security	(CSF) Self-Guarding Cryptographic Protocols against Algorithm Substitution Attacks
probabilistic	(ITP) Verified Analysis of Random Binary Tree Structures
Probabilistic Algorithm	(IJCAR) A New Probabilistic Algorithm for Approximate Model Counting (PRUV) A New Probabilistic Algorithm for Approximate Model Counting
probabilistic bisimilarity	(CAV) Deciding Probabilistic Bisimilarity Distance One for Labelled Markov Chains
probabilistic bisimilarity distance	(CAV) Deciding Probabilistic Bisimilarity Distance One for Labelled Markov Chains
Probabilistic Boolean Program	(CAV) SCInfer: Refinement-based Verification of Software Countermeasures against Side-Channel Attacks
Probabilistic computation	(LICS) Probabilistic stable functions on discrete cones are power series.
probabilistic CTL	(LICS) Riesz Modal Logic with Threshold Operators
probabilistic finite automata	(LICS) Distribution-based objectives for Markov Decision Processes
probabilistic games	(CAV) Reactive Control Improvisation
Probabilistic graphical models	(ICLP) Constraint-Based Inference in Probabilistic Logic Programs
Probabilistic Inductive Logic Programming	(ICLP) Improving Candidate Quality of Probabilistic Logic Models
probabilistic lambda-calculus	(LICS) Probabilistic Böhm Trees and Probabilistic Separation
Probabilistic Logic	(IJCAR) Probably Half True: Probabilistic Satisfiability over Lukasiewicz Infinitely-valued Logic
Probabilistic logic programming	(ICLP) Constraint-Based Inference in Probabilistic Logic Programs
Probabilistic model checking	(CAV) Sound Value Iteration (CAV) Safety-Aware Apprenticeship Learning (F-IDE) A Notebook Format for the Holistic Design of Embedded Systems (VaVAS) Probabilistic Model Checking for Autonomous Agent Strategy Synthesis - Extended Abstract (VaVAS) Towards a Hierarchical-Control Architecture for Distributed Autonomous Systems (Extended Abstract - Paper) (VaVAS) Policy Generation with Probabilistic Guarantees for Long-term Autonomy of a Mobile Service Robot
Probabilistic planning	(VaVAS) Policy Generation with Probabilistic Guarantees for Long-term Autonomy of a Mobile Service Robot
probabilistic powerdomains	(Domains13) Invited Talk: A domain theory for quasi-Borel spaces and statistical probabilistic programming
Probabilistic programs	(CAV) Constraint-Based Synthesis of Coupling Proofs (WST) Inference of Linear Upper-Bounds on the Expected Cost by Solving Cost Relations (LICS) The concurrent game semantics of Probabilistic PCF
probabilistic reasoning	(ICLP-DC) Probabalistic Action Language pBC+ (ICLP) A Probabilistic Extension of Action Language BC+
Probabilistic rewriting	(FCS) Statistical Model Checking of Guessing and Timing Attacks on Distance-bounding Protocols
Probabilistic Satisfiability	(IJCAR) Probably Half True: Probabilistic Satisfiability over Lukasiewicz Infinitely-valued Logic
Probabilistic State Space Exploration	(CAV) Partial Order Aware Concurrency Sampling
probabilistic systems	(LICS) Distribution-based objectives for Markov Decision Processes
Probabilistic Timed Automata	(ITP) MDP + TA = PTA: Probabilistic Timed Automata, Formalized (Short Paper)
probabilistic verification	(CAV) Value Iteration for Simple Stochastic Games: Stopping Criterion and Learning Algorithm (CAV) Constraint-Based Synthesis of Coupling Proofs (LICS) Conditional Value-at-Risk for Reachability and Mean Payoff in Markov Decision Processes
probability	(GS) Continuous probability distributions in concurrent games (ITP) Verified Tail Bounds for Randomized Programs
problem database	(IJCAR) Cops and CoCoWeb: Infrastructure for Confluence Tools
problem encodings and reformulations	(SAT) Constrained Image Generation Using Binarized Neural Networks with Decision Procedures
problem fingerprinting	(POS) A Problem Meta-Data Library for Research in SAT
procedural interpretation	(ICLP) Top-down and Bottom-up Evaluation Procedurally Integrated
process calculi	(TYDI) Truely Concurrent Processes in the Calculus of Structures
process calculus	(Linearity/TLLA) Taking Linear Logic Apart
product types	(ITRS) Intersection Subtyping with Constructors
profunctor	(LICS) Species, Profunctors and Taylor Expansion Weighted by SMCC--A Unified Framework for Modelling Nondeterministic, Probabilistic and Quantum Programs-- (MSFP) Profunctor Optics and the Yoneda Lemma
Program Analysis	(CAV) Quasi-Optimal Partial Order Reduction (FM) Variant Analysis with QL (LaSh) Decidable Linear Tree Constraints (LICS) Polynomial Invariants for Affine Programs (ICLP) Shape Neutral Analysis of Graph-based Data-structures (ICLP) Towards Incremental and Modular Context-sensitive Analysis
program completion	(ASPOCP) anthem: Transforming gringo Programs into First-Order Theories (Preliminary Report)
program correctness	(ASPOCP) anthem: Transforming gringo Programs into First-Order Theories (Preliminary Report)
Program Debugging	(VSTTE) Executable Counterexamples in Software Model Checking
Program Derivation	(REFINE) Programming Without Refinement
program extraction	(LICS) A functional interpretation with state (Domains13) Invited Talk: Scott Domains for Denotational Semantics and Program Extraction
Program invariant	(LICS) Polynomial Invariants for Affine Programs
Program Projection	(REFINE) Programming Without Refinement
program refinement	(LICS) ReLoC: A Mechanised Relational Logic for Fine-Grained Concurrency
program semantics	(Domains13) Invited Talk: Scott Domains for Denotational Semantics and Program Extraction
program specialisation	(ICLP) An iterative approach to precondition inference using constrained Horn clauses
Program Synthesis	(CAV) Synthesis Modulo Theories (CAV) Syntax-Guided Termination Analysis (CAV) Constraint-Based Synthesis of Coupling Proofs (CAV) Syntax Guided Synthesis with Quantitative Syntactic Objectives (CAV) Learning Abstractions for Program Synthesis (SYNT) Programming by example: efficient, but not “helpful” (IJCAR) Proof-Producing Synthesis of CakeML with I/O and Local State from Monadic HOL Functions
program transformation	(FSCD) Narrowing Trees for Syntactically Deterministic Conditional Term Rewriting Systems (VSTTE) Relational Equivalence Proofs Between Imperative and MapReduce Algorithms (WPTE) Reducing Total Correctness to Partial Correctness by a Transformation of the Language Semantics (WPTE) Automating the Diagram Method to Prove Correctness of Program Transformations (WPTE) On Transforming Functions Accessing Global Variables into Logically Constrained Term Rewriting Systems
program transformations	(FSCD) Nominal Unification with Atom and Context Variables (LOLA) Experimenting with graded monads: certified grading-based program transformations
Program translation	(TERMGRAPH) Programming by Term Rewriting
Program Verification	(DS-FM) Analysis and Verification of Message Passing based Parallel Programs (CAV) Syntax-Guided Termination Analysis (CAV) Nagini: A Static Verifier for Python (CAV) Program Analysis is Harder than Verification: A Computability Perspective (CAV) Formally Verified Montgomery Multiplication (Isabelle) Using Isabelle/UTP for the Verification of Sorting Algorithms: A Case Study (SMT) Discovering Universally Quantified Solutions for Constrained Horn Clauses (IJCAR) Verifying Asymptotic Time Complexity of Imperative Programs in Isabelle (IJCAR) A FOOLish Encoding of the Next State Relations of Imperative Programs (ITP) Program Verification in the Presence of Cached Address Translation (ITP) Software Verification with ITPs Should Use Binary Code Extraction to Reduce the TCB (Short Paper) (VSTTE) Program Verification in the Presence of I/O: Semantics, verified library routines, and verified applications (VSTTE) A Tree-Based Approach to Data Flow Proofs (VSTTE) Verified Certificate Checking for Counting Votes (WPTE) Verification of Ada Programs with AdaHorn (WPTE) Reducing Total Correctness to Partial Correctness by a Transformation of the Language Semantics (HCVS) Metaprogramming and symbolic execution for detecting runtime errors in Erlang programs (ICLP) Solving Horn Clauses on Inductive Data Types Without Induction
Programming by example	(SYNT) Programming by example: efficient, but not “helpful”
programming language semantics	(LICS) Computable decision making on the reals and other spaces via partiality and nondeterminism (LICS) Work Analysis with Resource-Aware Session Types
programming languages	(LICS) Enriching a Linear/Non-linear Lambda Calculus: A Programming Language for String Diagrams
programming logic	(IJCAR) A Separation Logic with Data: Small Models and Automation
programming methodology	(ASPOCP) anthem: Transforming gringo Programs into First-Order Theories (Preliminary Report)
programming paradigm	(LPOP) A software system should be declarative except where it interacts with the real world
Programming-by-Example	(CAV) Learning Abstractions for Program Synthesis
progress measure	(LICS) A pseudo-quasi-polynomial algorithm for solving mean-payoff parity games
Projected Model Counting	(SAT) Exploiting Treewidth for Projected Model Counting and its Limits
projective limit	(Domains13)
Projective plane	(WiL) On Expanding Standard Notions of Constructivity
Prolog	(VSTTE) TWAM: A Certifying Abstract Machine for Logic Programs (ICLP) Top-down and Bottom-up Evaluation Procedurally Integrated (ICLP) Towards Static Performance Guarantees for Programs with Run-time Checks
Prompt LTL	(SR) Quantifying Bounds in Strategy Logic
Proof	(CAV) Continuous formal verification of Amazon s2n (Vampire) Testing ATP folklore: a statistical analysis of Vampire proofs.
proof assistant	(ARQNL) An Outline for Simple Semi-automated Proof Assistants for First-order Modal Logics (ThEdu) Lucas Interpretation from Programmers’ Perspective (IJCAR) Formalizing Bachmair and Ganzinger's Ordered Resolution Prover (UITP) Interfacing with a Prover using Focusing and Logic Programming
proof assistants	(FSCD) Cumulative Inductive Types in Coq (ITP) HOL Light QE (ITP) The Coinductive Formulation of Common Knowledge (ITP) Reification by Parametricity
proof automation	(ITP) ProofWatch: Watchlist Guidance for Large Theories in E
proof by reflection	(ITP) Reification by Parametricity
proof checker	(WST) TTT2 with Termination Templates for Teaching
Proof checking	(POS) Two flavors of DRAT (UITP) Text-Orientated Formal Mathematics
proof complexity	(CAV) The Proof Complexity of SMT Solvers (PC) Resolution with Counting: Different Moduli and Tree-Like Lower Bounds (PC) Resolution and the binary encoding of combinatorial principles (PC) Proof systems for #SAT based on restricted circuits (PC) Branching Program Complexity of Canonical Search Problems and Proof Complexity of Formulas (TYDI) Proof complexity of deep inference: a survey (TYDI) Two Unifying Structural Principles (PARIS) On the Logical Complexity of Cyclic Arithmetic (LCC) Feasibly constructive proofs of succinct weak circuit lower bounds (IJCAR) Extended Resolution Simulates DRAT (POS) Seeking Practical CDCL Insights from Theoretical SAT Benchmarks (SAT) Using Combinatorial Benchmarks to Probe the Reasoning Power of Pseudo-Boolean Solvers (SAT) In Between Resolution and Cutting Planes: A Study of Proof Systems for Pseudo-Boolean SAT Solving
Proof compression	(IJCAR) A Tableaux Calculus for Reducing Proof Size (UITP) Partial Regularization of First-Order Resolution Proofs
proof engineering	(Coq) Procrastination, A proof engineering technique (ITP) Reification by Parametricity
Proof generation	(SMT) Proofs in conflict-driven theory combination
proof guidance	(ITP) ProofWatch: Watchlist Guidance for Large Theories in E
proof identity	(IJCAR) From Syntactic Proofs to Combinatorial Proofs
Proof Method Recommendation	(Isabelle) PaMpeR: A Proof Method Recommendation System for Isabelle/HOL
Proof Mining	(Isabelle) PaMpeR: A Proof Method Recommendation System for Isabelle/HOL
proof nets	(FSCD) Proof nets for bi-intuitionistic linear logic (LICS) Unification nets: canonical proof net quantifiers (Linearity/TLLA) The structure of non decomposable connectives of linear logic (Linearity/TLLA) Proof nets, coends and the Yoneda isomorphism
proof of literal	(ASPOCP) Syntactic Conditions for Antichain Property in Consistency Restoring Prolog
proof of univalence	(HoTT/UF) Internalizing Presheaf Semantics: Charting the Design Space
proof schema	(PARIS) Towards the Automatic Construction of Schematic Proofs
Proof search	(IJCAR) Focussing, MALL and the polynomial hierarchy (Coq) Proof Construction by Tactic Learning (ADSL) Cyclic Theorem Prover for Separation Logic by Magic Wand
proof semantics	(TYDI) Two Unifying Structural Principles
Proof System	(Isabelle) Substitutionless First-Order Logic: A Formal Soundness Proof
proof systems	(IJCAR) QRAT+: Generalizing QRAT by a More Powerful QBF Redundancy Property (EICNCL) Proof Translations in BI logic
proof terms	(FSCD) ProTeM: A Proof Term Manipulator (CL&C) Fast cut-elimination using proof terms: an empirical study
Proof theory	(TYDI) Nested sequents for modal logics and beyond (TYDI) Sequentialising nested systems (TYDI) An introduction to deep inference (TYDI) Two Unifying Structural Principles (PARIS) On the Logical Complexity of Cyclic Arithmetic (WiL) Decomposing labelled proof theory for intuitionistic modal logic (WiL) Non-well-founded proof system for Transitive Closure Logic (WiL) Towards a Playground for Logicians (WiL) A semantical view of sequent based systems (PAAR) Efficient translation of sequent calculus proofs into natural deduction proofs (IJCAR) Focussing, MALL and the polynomial hierarchy (IJCAR) A Logical Framework with Commutative and Non-Commutative Subexponentials (IJCAR) A Tableaux Calculus for Reducing Proof Size (CL&C) Some ideas on cut-elimination for cyclic arithmetic proofs (CL&C) Admissible tools in the kitchen of intuitionistic logic (EICNCL) Intuitionistic multi-agent subatomic natural deduction for belief and knowledge (ICLP) First-order answer set programming as constructive proof search
proof theory of modal logic	(ITP) Software Tool Support for Modular Reasoning in Modal Logics of Actions
Proof translations	(EICNCL) Proof Translations in BI logic
proof-as-program	(LICS) Classical realizability as a classifier for nondeterminism
Proof-checker	(ITP) CalcCheck: a Proof Checker for Teaching the “Logical Approach to Discrete Math”
Proof-Producing Compilation	(VSTTE) TWAM: A Certifying Abstract Machine for Logic Programs
proof-relevant	(ICLP-DC) Proof-relevant resolution for elaboration of programming languages
Proof-relevant logic	(ICLP) Proof-relevant Horn Clauses for Dependent Type Inference and Term Synthesis
proof-search	(PARIS) Local Validity for Circular Proofs in Linear Logic with Fixed Points
proof-theoretic semantics	(NLCS) Paychecks, Presupposition, and Dependent Types
proof-theoretical linear semantics	(ICLP) A New Proof-theoretical Linear Semantics for CHR
proofs	(FM) Object-Oriented Security Proofs
Proofs by reflection	(IJCAR) A Why3 framework for reflection proofs and its application to GMP's algorithms
proofs-as-programs	(LICS) A sequent calculus with dependent types for classical arithmetic
proofs-as-programs-as-morphisms	(CL&C) The “duality of computation” from a fibrational perspective
property directed reachability	(SMT) Discovering Universally Quantified Solutions for Constrained Horn Clauses
property falsification	(CAV) Inner and Outer Approximating Flowpipes for Delay Differential Equations
Property Specification Patterns	(DS-FM) Consistency Checking of Functional Requirements
property-based testing	(LFMTP) Property-Based Testing of Abstract Machines: an Experience Report
Propositional Dynamic Logic	(CAV) Propositional Dynamic Logic for Higher-Order Functional Programs (LICS) Wreath Products of Distributive Forest Algebras
propositional implicational intuitionistic logic	(RCRA) Shaving with Occam's Razor: Deriving Minimalist Theorem Provers for Minimal Logic
propositional logic	(ARQNL) Pseudo-Propositional Logic (IJCAR) Extended Resolution Simulates DRAT (SAT) Exploiting Treewidth for Projected Model Counting and its Limits (CSF) Guided design of attack trees: a system-based approach (CL&C) Admissible tools in the kitchen of intuitionistic logic (PRUV) A new logic for jointly representing hard and soft constraints
propositional model counting	(PC) Proof systems for #SAT based on restricted circuits
Propositional Resizing	(HoTT/UF) Cubical Assemblies and the Independence of the Propositional Resizing Axiom
PROPs	(LICS) Rewriting with Frobenius
Protocol Verification	(CAV) Model checking indistinguishability of randomized security protocols (CSF) An extensive formal analysis of multi-factor authentication protocols
protokernel	(AVOCS) Proof-Oriented Design of a Separation Kernel with Minimal Trusted Computing Base
prototyping	(SAT) PySAT: A Python Toolkit for Prototyping with SAT Oracles
prover	(IJCAR) Formalizing Bachmair and Ganzinger's Ordered Resolution Prover
Prover IDE	(UITP) Isabelle/PIDE after 10 years of development
Prover Trident	(FM) Interlocking Design Automation using Prover Trident
proximity relation	(UNIF) Proximity-Based Generalization
Pseudo-Boolean	(POS) Competitive Sorter-based Encoding of PB-Constraints into SAT
Pseudo-Boolean Optimisation	(RCRA) Optimal Fault-Tolerant Placement of Relay Nodes in a Mission Critical Wireless Network
Pseudo-Boolean Solving	(POS) Divide and Conquer: Towards Faster Pseudo-Boolean Solving (SAT) Using Combinatorial Benchmarks to Probe the Reasoning Power of Pseudo-Boolean Solvers (SAT) In Between Resolution and Cutting Planes: A Study of Proof Systems for Pseudo-Boolean SAT Solving
PSPACE	(FSCD) A Unifying Framework for Type Inhabitation
Public Git Archive	(MLP) Splitting source code identifiers using Bidirectional LSTM Recurrent Neural Network
Pushdown systems with transductions	(CAV) Android Stack Systems
PVS	(FM) A Formally Verified Floating-Point Implementation of the Compact Position Reporting Algorithm (ITP) Boosting the Reuse of Formal Specifications (ITP) Formalizing Ring Theory in PVS (Short Paper)
Python	(LPOP) Logic-based Methods for Software Engineers and Business People (SAT) PySAT: A Python Toolkit for Prototyping with SAT Oracles
Q
Q-resolution	(SAT) Polynomial-Time Validation of QCDCL Certificates
QBF	(CAV) Synthesis Of Asynchronous Reactive Programs From Temporal Specifications (IJCAR) QRAT+: Generalizing QRAT by a More Powerful QBF Redundancy Property (QBF) A Grounder From Second-Order Logic To QBF (QBF) Portfolio-Based Algorithm Selection for Circuit QBFs (QBF) Towards the Semantics of QBF Clauses (SAT) QBF as an Alternative to Courcelle's Theorem (SAT) Polynomial-Time Validation of QCDCL Certificates
QBF calculi	(SAT) Local Soundness for QBF Calculi
QDimacs	(QBF) A Grounder From Second-Order Logic To QBF
QRAT	(IJCAR) QRAT+: Generalizing QRAT by a More Powerful QBF Redundancy Property
Qualitative Reasoning	(ICLP) A Trajectory Calculus for Qualitative Spatial Reasoning Using Answer Set Programming
qualitative spatial reasoning	(WiL) About the unification type of topological logics over Euclidean spaces
qualitattive spatial reasoning	(UNIF) About the unification type of topological logics over Euclidean spaces
quantale relator	(LICS) Quantitative Behavioural Reasoning for Higher-order Effectful Programs: Applicative Distances
quantification	(QBF) Tractability results for structured quantified CNF-formulas via knowledge compilation
Quantified Bit-Vectors	(CAV) Solving Quantified Bit-Vectors using Invertibility Conditions
quantified boolean formula	(SAT) Circuit-based Search Space Pruning in QBF
Quantified Boolean Formulas	(CAV) Understanding and Extending Incremental Determinization for 2QBF (IJCAR) QRAT+: Generalizing QRAT by a More Powerful QBF Redundancy Property (SAT) Symmetries for QBF
Quantified Circuit	(QBF) Portfolio-Based Algorithm Selection for Circuit QBFs
quantified effects	(LOLA) Experimenting with graded monads: certified grading-based program transformations
quantified modal logic	(ARQNL) An Outline for Simple Semi-automated Proof Assistants for First-order Modal Logics
quantified modal logics	(ARQNL) Labelled Calculi for QMLs with Non-Rigid and Non-Denoting Terms (EICNCL) Proof theory for quantified monotone modal logics
quantified resolution asymmetric tautology	(IJCAR) QRAT+: Generalizing QRAT by a More Powerful QBF Redundancy Property
Quantifier	(CAV) Delta-Decision Procedures for Exists-Forall Problems over the Reals
quantifier elimination	(SCSC) RP: Non-linear Real Arithmetic Benchmarks derived from Automated Reasoning in Economics (SCSC) EA: Wrapping Computer Algebra is Surprisingly Successful for Non-Linear SMT (FM) Optimal and Robust Controller Synthesis Using Energy Timed Automata with Uncertainty (SYNT) On Inductive Verification and Synthesis (IJCAR) Deciding the First-Order Theory of an Algebra of Feature Trees with Updates
quantifier instantiation	(SMT) Discovering Universally Quantified Solutions for Constrained Horn Clauses
quantifier rank	(LICS) Tree depth, quantifier elimination, and quantifier rank
Quantifier-free Theory of Arrays	(IJCAR) Efficient Interpolation for the Theory of Arrays
quantifiers	(SMT) Discovering Universally Quantified Solutions for Constrained Horn Clauses (LICS) Unification nets: canonical proof net quantifiers
quantitative algebraic reasoning	(LICS) An algebraic theory of Markov processes
Quantitative Analysis	(CAV) Automata vs Linear-Programming Discounted-Sum Inclusion (FM) QFLan: A Tool for the Quantitative Analysis of Highly Reconfigurable Systems
quantitative information flow	(FM) An Algebraic Approach for Reasoning About Information Flow (CSF) Symbolic Side-Channel Analysis for Probabilistic Programs
Quantitative Model Checking	(MoRe) Logically-Constrained Reinforcement Learning
Quantitative Objective	(CAV) Syntax Guided Synthesis with Quantitative Syntactic Objectives
Quantitative Semantics for Temporal Logic	(CAV) A Counting Semantics for Monitoring LTL Specifications over Finite Traces
Quantum	(GS) A definable game semantics for the linear quantum lambda-calculus
quantum computation	(LICS) Two complete axiomatisations of pure-state qubit quantum computing (LICS) Logical paradoxes in quantum computation
quantum computing	(FSCD) A diagrammatic axiomatisation of fermionic quantum circuits (TERMGRAPH) A framework for rewriting families of string diagrams (LICS) Enriching a Linear/Non-linear Lambda Calculus: A Programming Language for String Diagrams (LICS) Diagrammatic Reasoning beyond Clifford+T Quantum Mechanics (LICS) A Complete Axiomatisation of the ZX-Calculus for Clifford+T Quantum Mechanics (RCRA) Greedy Randomized Search for Scalable Compilation of Quantum Circuits
Quantum functional languages	(Linearity/TLLA) Quantum programming made easy
quantum program	(LICS) Species, Profunctors and Taylor Expansion Weighted by SMCC--A Unified Framework for Modelling Nondeterministic, Probabilistic and Quantum Programs--
Quantum Programming	(Linearity/TLLA) Quantum programming made easy
quasi-Borel spaces	(Domains13) Invited Talk: A domain theory for quasi-Borel spaces and statistical probabilistic programming
Quasi-inverse	(FCS) A Homotopical Approach to Cryptography
quasi-metric	(Domains13) Invited Talk: Topology and Domain Theory Interfaces
queries	(LPOP) Easier Rules and Constraints for Programming
query	(LICS) Can One Escape Red Chains? Regular Path Queries Determinacy is Undecidable.
Query Answering	(ICLP) Cautious Reasoning in ASP via Minimal models and Unsatisfiable Cores
Query Enumeration	(LICS) MSO Queries on Trees: Enumerating Answers under Updates Using Forest Algebras
Query Optimization	(WST) Verification of Rewriting-based Query Optimizers
Question Answering	(ICLP-DC) The Learning-Knowledge-Reasoning Paradigm For Natural Language Understanding and Question Answering (ICLP-DC) Knowledge Authoring and Question Answering via Controlled Natural Language (MLP) Answering Cloze-style Software Questions Using Stack Overflow (ICLP) Incremental and Iterative Learning of Answer Set Programs from Mutually Distinct Examples
Quicksort	(ITP) Verified Analysis of Random Binary Tree Structures
Quotation and evaluation	(ITP) HOL Light QE
quotient inductive types	(FSCD) A Syntax for Higher Inductive-Inductive Types
quotients	(ITP) Boosting the Reuse of Formal Specifications (ITP) Relational Parametricity and Quotient Preservation for Modular (Co)Datatypes
R
RAII	(LOLA) A resource modality for RAII
Railway	(VaVAS)
railway interlocking systems	(FM) Stepwise Development and Model Checking of a Distributed Interlocking System - using RAISE
RAISE	(FM) Stepwise Development and Model Checking of a Distributed Interlocking System - using RAISE
Ramsey theory	(LICS) A universal-algebraic proof of the complexity dichotomy for Monotone Monadic SNP
Random Algorithms	(RCRA) Greedy Randomized Search for Scalable Compilation of Quantum Circuits
Random Forest	(MLP) Splitting source code identifiers using Bidirectional LSTM Recurrent Neural Network
random generation	(HOR) Combinatorics of explicit substitutions (extended abstract)
random parity equations	(SAT) Fast and Flexible Probabilistic Model Counting
random sample voting	(CSF) Alethea: A Provably Secure Random Sample Voting Protocol
random SAT	(SAT) Sharpness of the Satisfiability Threshold for Non-Uniform Random k-SAT
random variables	(LICS) Boolean-Valued Semantics for Stochastic Lambda-Calculus (Domains13) A Domain-theoretic Skorohod’s Theorem
randomised	(ITP) Verified Analysis of Random Binary Tree Structures
Randomization	(CAV) Model checking indistinguishability of randomized security protocols
randomized algorithm	(ITP) Verified Tail Bounds for Randomized Programs
Randomized algorithms	(CAV) Constraint-Based Synthesis of Coupling Proofs (SAT) Fast and Flexible Probabilistic Model Counting
RankFinder	(WST) Control-Flow Refinement via Partial Evaluation
ranking functions	(LICS) Efficient Algorithms for Asymptotic Bounds on Termination Time in VASS
Rare Event Simulation	(FM) Statistical Model Checking of LLVM Code
Rating of Geometric Provers	(ThEdu) Rating of Geometric Automated Theorem Provers
Rational closure	(PRUV) Reasoning about exceptions in ontologies: from the lexicographic closure to the skeptical closure
Rational synthesis	(LICS) Rational Synthesis Under Imperfect Information
rationality	(SR) Beyond admissibility: Dominance between chains of strategies
RBAC	(LPOP) Easier Rules and Constraints for Programming
Re-composition	(ICLP) Phylotastic: An Experiment in Creating, Manipulating, and Evolving Phylogenetic Biology Workflows Using Logic Programming
reach-avoid specification	(CAV) Controller Synthesis Made Real: Reach-avoid Specifications and Linear Dynamics
reachability	(CAV) Value Iteration for Simple Stochastic Games: Stopping Criterion and Learning Algorithm (IJCAR) A Coinductive Approach to Proving Reachability in Logically Constrained Term Rewriting Systems (WPTE) On Transforming Narrowing Trees into Regular Tree Grammars Generating Ranges of Substitutions
reachability analysis	(CAV) SimpleCAR: An Efficient Bug-Finding Tool Based On Approximate Reachability (CAV) Inner and Outer Approximating Flowpipes for Delay Differential Equations (FM) Approximate Partial Order Reduction (AVOCS) Backward reachability analysis for timed automata with data variables
Reachability analysis of nonlinear systems	(CAV) Reachable Set Over-approximation for Nonlinear Systems Using Piecewise Barrier Tubes
reachability logic	(WPTE) Reducing Total Correctness to Partial Correctness by a Transformation of the Language Semantics
Reachability problem	(CAV) Android Stack Systems
Reachable set over-approximation	(CAV) Reachable Set Over-approximation for Nonlinear Systems Using Piecewise Barrier Tubes
reactive programs	(CSF) Knowledge-based Security of Dynamic Secrets for Reactive Programs
reactive synthesis	(CAV) Strix: Explicit Reactive Synthesis Strikes Back! (CAV) Reactive Control Improvisation (SYNT) Maximum Realizability for Linear Temporal Logic Specifications (SYNT) Reactive Synthesis from LTL Specification with Spot
read-once branching programs	(PC) Branching Program Complexity of Canonical Search Problems and Proof Complexity of Formulas
real algebraic geometry	(SCSC) RP: Unknot Recognition Through Quantifier Elimination
Real Analysis	(Coq) Classical Analysis with Coq
Real Arithetmic	(SMT) The next 10^4 UppSAT Approximations
Real Cohesive Homotopy Type Theory	(HoTT/UF) Cohesive Covering Theory
Real Numbers	(ThEdu) Proving in the Isabelle Proof Assistant that the Set of Real Numbers is not Countable
real proofs	(WiL) Can every real proof be represented by a formal proof? The Hilbert-Gentzen thesis
real roots	(SCSC) EA: New in CoCoA-5.2.4 and CoCoALib-0.99570 for SC-Square
Real-Time	(LICS) A Theory of Register Monitors (Overture) Overture FMU: Export VDM-RT Models as Tool-Wrapper FMUs
real-time logic TCTL	(FM) Timed Vacuity
Real-world applications	(LPOP) How to upgrade ASP for true dynamic modelling and solving?
realisability	(HOR) Refining Properties of Filter Models: Sensibility, Approximability and Reducibility
Realizability	(CAV) Synthesizing Reactive Systems from Hyperproperties (PARIS) LMSO: A Curry-Howard Approach to Church’s Synthesis via Linear Logic (speaker: Pierre PRADIC) (LICS) Classical realizability as a classifier for nondeterminism (HoTT/UF) Cubical Assemblies and the Independence of the Propositional Resizing Axiom
Reasoning	(ASPOCP) Invited Talk: Optimization Problems in Answer Set Programming
Reasoning about Actions and Change	(ICLP-DC) Explaining Actual Causation via Reasoning about Actions and Change
Reasoning about syntax	(ITP) HOL Light QE
recognizability	(LICS) Definable decompositions for graphs of bounded linear cliquewidth
record types	(IJCAR) Theories as Types
Recurrences	(VSTTE) Extending VIAP to Handle Array Programs
recursion	(Domains13) Diffeological Spaces and Semantics for Differential Programming (Coq) Towards a formalization of the guard condition
recursion-free constrained Horn clause	(HCVS) Solving Constrained Horn Clauses Using Dependence-Disjoint Expansions
Recursion-theoretic characterisations	(LCC) A recursion-theoretic characterisation of the positive polynomial-time functions
Recursive functions	(HCVS) A simple functional presentation and an inductive correctness proof of the Horn algorithm
Recursive types	(FSCD) Index-Stratified Types
recursively enumerable	(Isabelle) Hilbert Meets Isabelle: Formalisation of the DPRM Theorem in Isabelle
Reduction	(CAV) Reasoning About TSO Programs Using Reduction and Abstraction (LOLA) Towards a library of formalised undecidable problems in Coq: The undecidability of intuitionistic linear logic
Reduction orderings	(TERMGRAPH) On quasi ordinal diagram systems
Reduction Semantics	(DCM) Pointing to Private Names (PARIS) What makes guarded types tick?
reduction to SAT	(VEMDP) Computing properties of stable configurations of thermodynamic binding networks
Reductive cut elimination	(CL&C) Herbrand's Theorem as Higher-Order Recursion
Redundancy-free Proof-Search	(IJCAR) Constructive Decision via Redundancy-free Proof-Search
refactoring	(F-IDE) AsmetaF: a flattener for the ASMETA framework
references	(LOLA) Heaps denote finitely partitioned trees
refinement	(FM) Compositional Reasoning for Shared-variable Concurrent Programs (Isabelle) A Verified SAT Solver with Watched Literals Using Imperative HOL (Extended Abstract) (ITP) Boosting the Reuse of Formal Specifications (REFINE) Refining Santa: An Excercise in Efficient Synchronization (REFINE) Correctness of Concurrent Objects under Weak Memory Models
Reflection	(ITP) HOL Light QE
Reformulation	(LaSh) Automated Constraint Modelling with Conjure
register machines	(LICS) A Theory of Register Monitors
Regression Tree	(Isabelle) PaMpeR: A Proof Method Recommendation System for Isabelle/HOL
Regular Datalog	(ICLP) Certified Graph View Maintenance with Regular Datalog
regular expressions	(FM) The Compound Interest in Relaxing Punctuality (LaSh) A Derivative-Based Decision Procedure for WS1S (LICS) Regular Transducer Expressions for Regular Transformations over infinite words
regular languages	(LICS) Separability by piecewise testable languages and downward closures beyond subwords (Linearity/TLLA) A semantic conjecture on second-order MLL and its complexity consequences (work in progress)
regular tree grammar	(FSCD) Narrowing Trees for Syntactically Deterministic Conditional Term Rewriting Systems (WPTE) On Transforming Narrowing Trees into Regular Tree Grammars Generating Ranges of Substitutions
regularity preservation	(FSCD) Completeness of Tree Automata Completion
reification	(ITP) Reification by Parametricity
Reinforcement Learning	(MoRe) Logically-Constrained Reinforcement Learning (CAV) Fast Numerical Program Analysis with Reinforcement Learning (CAV) Safety-Aware Apprenticeship Learning (FM) Falsification of Cyber-Physical Systems Using Deep Reinforcement Learning
relational databases	(TERMGRAPH) Finding the Transitive Closure of Functional Dependencies using Strategic Port Graph Rewriting
Relational Equivalence Verification	(VSTTE) Relational Equivalence Proofs Between Imperative and MapReduce Algorithms
relational model	(LICS) Every λ-Term is Meaningful for the Infinitary Relational Model
relational reasoning	(LICS) ReLoC: A Mechanised Relational Logic for Fine-Grained Concurrency
relational semantics	(ITRS) Towards a Semantic Measure of the Execution Time in Call-by-Value lambda-Calculus
relational theory	(TERMGRAPH) Finding the Transitive Closure of Functional Dependencies using Strategic Port Graph Rewriting
Relational Verification	(CAV) Exploiting Synchrony and Symmetry in Relational Verification
Relations	(Domains13) Frames and frame relations
Relative Correctness	(REFINE) Programming Without Refinement
relative entropy programming	(PC) Optimization over the Boolean Hypercube via Sums of Nonnegative Circuit Polynomials
relative soundness results	(CSF) A Typing Result for Stateful Protocols
relaxed memory	(Domains13) Invited Talk: A Brief History of Denotational Semantics
Relevance Logic	(IJCAR) Constructive Decision via Redundancy-free Proof-Search
Reliable	(FM) Resource-aware Design for Reliable Autonomous Applications with Multiple Periods
rely-guarantee	(FM) Compositional Reasoning for Shared-variable Concurrent Programs
Rely/guarantee concurrency	(FM) Encoding fairness in a synchronous concurrent program algebra (REFINE) Challenges of specifying concurrent program components
remote build	(Isabelle) The remote_build Tool
repeated games	(MSFP) Backward induction for repeated games
replaceability	(RCRA) Replaceability for constraint satisfaction problems: Algorithms, Inferences, and Complexity Patterns
represented space	(Domains13) T^\omega-representations of compact sets through dyadic subbases
Requirement Analysis	(FM) From Formal Requirements to Highly Assured Software for Unmanned Aircraft Systems
requirements analysis	(F-IDE) The CLEAR Way To Transparent Formal Methods
requirements based testing	(F-IDE) The CLEAR Way To Transparent Formal Methods
Requirements Engineering	(DS-FM) Consistency Checking of Functional Requirements (AVOCS) Analyzing Consistency of Formal Requirements
Requirements specification	(FM) Formal Verification of Automotive Simulink Controller Models: Empirical Technical Challenges, Evaluation and Recommendations
resolution	(CAV) The Proof Complexity of SMT Solvers (PC) Resolution with Counting: Different Moduli and Tree-Like Lower Bounds (PC) Branching Program Complexity of Canonical Search Problems and Proof Complexity of Formulas (ICLP-DC) Proof-relevant resolution for elaboration of programming languages (WiL) On the Combination of Resolution and SAT Procedures for Modal Theorem-Proving (IJCAR) Enumerating Justifications using Resolution (IJCAR) A Resolution-Based Calculus for Preferential Logics (IJCAR) Formalizing Bachmair and Ganzinger's Ordered Resolution Prover (POS) Seeking Practical CDCL Insights from Theoretical SAT Benchmarks (POS) Divide and Conquer: Towards Faster Pseudo-Boolean Solving (UITP) Partial Regularization of First-Order Resolution Proofs (SAT) Using Combinatorial Benchmarks to Probe the Reasoning Power of Pseudo-Boolean Solvers (SAT) In Between Resolution and Cutting Planes: A Study of Proof Systems for Pseudo-Boolean SAT Solving (SAT) Cops-Robber games and the resolution of Tseitin formulas
resolution calculi	(PAAR) Evaluating Pre-Processing Techniques for the Separated Normal Form for Temporal Logics (QBF) Towards the Semantics of QBF Clauses
resource calculus	(LICS) Species, Profunctors and Taylor Expansion Weighted by SMCC--A Unified Framework for Modelling Nondeterministic, Probabilistic and Quantum Programs--
resource management	(LOLA) A resource modality for RAII
resource modality	(LOLA) A resource modality for RAII
Resource Usage Analysis	(LCC) A General Equational Framework for Static Profiling of Parametric Resource Usage (ICLP) Towards Static Performance Guarantees for Programs with Run-time Checks
Resource-aware	(FM) Resource-aware Design for Reliable Autonomous Applications with Multiple Periods
Resources analysis	(GS) Resource-Tracking Concurrent Games
Restart	(SAT) Machine Learning-based Restart Policy for CDCL SAT Solvers
restricted chase	(IJCAR) Efficient Model Construction for Horn Logic with VLog: System Description
Reverse mathematics	(PARIS) On the Logical Complexity of Cyclic Arithmetic
Reversibility	(DCM) Models of Computation that Conserve Data
Rewrite Rules	(SMT) Rewrites for SMT Solvers using Syntax-Guided Enumeration
Rewrite system	(HDRA) Generalizations of the associative operad and convergent rewrite systems
Rewrite Systems	(LaSh) Declarative Dynamic Programming with Inverse Coupled Rewrite Systems
rewriting	(IWC) Critical pairs for Gray categories (FSCD) A Unifying Framework for Type Inhabitation (FSCD) Coherence of Gray categories via rewriting (SMT) SMT Solving Modulo Tableau and Rewriting Theories (WST) Verification of Rewriting-based Query Optimizers (IJCAR) Cops and CoCoWeb: Infrastructure for Confluence Tools (HDRA) Normal forms for planar connected string diagrams (ITP) Tactics and Certificates in Meta Dedukti
ribbon categories	(LICS) Ribbon tensorial logic
Rice's theorem	(CAV) Program Analysis is Harder than Verification: A Computability Perspective
rich logic	(FM) Producing Explanations for Rich Logics
Richard Montague	(NLCS) Propositional Attitude Operators in Homotopy Type Theory
Richman games	(SR) Infinite-Duration Richman Bidding Games
Riesz modal logic	(LICS) Riesz Modal Logic with Threshold Operators
right lifting property	(HoTT/UF) Robust Notions of Contextual Fibrancy
Ring Theory	(ITP) Formalizing Ring Theory in PVS (Short Paper)
Robotic	(VaVAS)
robotic planning	(CAV) Reactive Control Improvisation
robust declassification	(CSF) Knowledge-based Security of Dynamic Secrets for Reactive Programs
robustness	(CAV) Reasoning About TSO Programs Using Reduction and Abstraction (CAV) Inner and Outer Approximating Flowpipes for Delay Differential Equations
Robustness guided falsification	(FM) Falsification of Cyber-Physical Systems Using Deep Reinforcement Learning
Role-Based Access Control	(LPOP) Role-Based Access Control via JASP
Role-Based Access Control (RBAC)	(LPOP) Security Policies in Constraint Handling Rules
roundoff error	(FM) Combining Tools for Optimization and Analysis of Floating-Point Computations
Routing Protocol	(DS-FM) A Formal Study of MANET Routing Protocols
RTL verification	(PLR) RTLCheck: Automatically Verifying the Memory Consistency of Processor RTL
Rule Decomposition	(ASPOCP) selp: A Single-Shot Epistemic Logic Program Solver
Rule-base modeling	(VEMDP) Computational Approaches for the Programmed Assembly of Nanocellulose Meshes
rule-based language	(VEMDP) Executable Biochemical Space for Specification and Analysis of Biochemical Systems
Rule-based modelling	(VEMDP) Rule-Based Gillespie Simulation of Chemical Systems (VEMDP) Conservative approximations of polymers
Rule-Based Programming	(AVOCS) Rule-Based Synthesis of Chains of Security Functions for Software-Defined Networks
Rule-Based Systems	(ICLP) Application of Logic-Based Methods to Machine Component Design
rules	(LPOP) Easier Rules and Constraints for Programming
rules of the road	(VaVAS) Formalisation of the Rules of the Road for embedding into an Autonomous Vehicle Agent
Run-time Checks	(ICLP) Towards Static Performance Guarantees for Programs with Run-time Checks
Runtime complexity	(CAV) Automata vs Linear-Programming Discounted-Sum Inclusion
Runtime verification	(CAV) Monitoring Weak Consistency (CAV) A Counting Semantics for Monitoring LTL Specifications over Finite Traces (CSF) The Complexity of Monitoring Hyperproperties
S
s-finite distributions	(Domains13) Invited Talk: A domain theory for quasi-Borel spaces and statistical probabilistic programming
S5	(IJCAR) An Assumption-Based Approach for Solving The Minimal S5-Satisfiability Problem
safe schemes	(FSCD) Homogeneity without Loss of Generality
Safety	(FM) Software Safety and Security and AI (GraMSec) Combining Bayesian Networks and Fishbone Diagrams to Distinguish between Intentional Attacks and Accidental Technical Failures
safety critical	(FM) Disruptive Innovations for the Development and the Deployment of Fault-Free Software
safety properties	(FM) Compositional Reasoning for Shared-variable Concurrent Programs (SMT) SMT-based Compile-time Verification of Safety Properties for Smart Contracts
safety verification	(FM) Approximate Partial Order Reduction (FM) Vector Barrier Certificates and Comparison Systems
SAT	(CAV) Understanding and Extending Incremental Determinization for 2QBF (LPOP) A Picat-based XCSP Solver - from Parsing, Modeling, to SAT Encoding (WiL) On the Combination of Resolution and SAT Procedures for Modal Theorem-Proving (SMT) SMT Solving Modulo Tableau and Rewriting Theories (IJCAR) Extended Resolution Simulates DRAT (IJCAR) Investigating the Existence of Large Sets of Idempotent Quasigroups via Satisfiability Testing (IJCAR) Exploring Approximations for Floating-Point Arithmetic using UppSAT (POS) Local-Style Search in the Linear MaxSAT Algorithm: A Computational Study of Solution-Based Phase Saving (POS) Tuning Parallel SAT Solvers (POS) The Effect of Scrambling CNFs (POS) Competitive Sorter-based Encoding of PB-Constraints into SAT (SAT) ALIAS: A Modular Tool for Finding Backdoors for SAT (SAT) Machine Learning-based Restart Policy for CDCL SAT Solvers (SAT) Chronological Backtracking
SAT and BDD-based decision procedures	(CAV) ADAC: Automated Design of Approximate Circuits
SAT encoding	(SAT) Approximately Propagation Complete and Conflict Propagating Constraint Encodings (RCRA) Encoding PB Constraints into SAT via Binary Adders and BDDs -- Revisited
SAT modulo theories	(CAV) Eager Abstraction for Symbolic Model Checking
SAT problem	(ARQNL) Pseudo-Propositional Logic
SAT solver	(FM) FSM Inference from Long Traces (Isabelle) A Verified SAT Solver with Watched Literals Using Imperative HOL (Extended Abstract) (POS) CryptoMiniSat Parameter-Optimization for Solving Cryptographic Instances (SAT) Centrality-Based Improvements to CDCL Heuristics
SAT solvers	(SAT) PySAT: A Python Toolkit for Prototyping with SAT Oracles
SAT solving	(SCSC) RP: Refutation of Products of Linear Polynomials (POS) Seeking Practical CDCL Insights from Theoretical SAT Benchmarks (POS) Divide and Conquer: Towards Faster Pseudo-Boolean Solving (SAT) Using Combinatorial Benchmarks to Probe the Reasoning Power of Pseudo-Boolean Solvers (SAT) In Between Resolution and Cutting Planes: A Study of Proof Systems for Pseudo-Boolean SAT Solving
SAT-based Optimization	(SAT) Solving MaxSAT with Bit-Vector Optimization
Sat4j	(SAT) Using Combinatorial Benchmarks to Probe the Reasoning Power of Pseudo-Boolean Solvers
Satisfiability	(LICS) Unary negation fragment with equivalence relations has the finite model property (IJCAR) Implicit Hitting Set Algorithms for Maximum Satisfiability Modulo Theories (RCRA) On the Configuration of SAT Formulae
Satisfiability Checking	(SCSC) EA: Techniques for Natural-style Proofs in Elementary Analysis
Satisfiability modulo assignment	(SMT) Proofs in conflict-driven theory combination
Satisfiability Modulo Constraint Handling Rules	(ICLP) Shape Neutral Analysis of Graph-based Data-structures
Satisfiability Modulo Theories	(CAV) Solving Quantified Bit-Vectors using Invertibility Conditions (CAV) The Proof Complexity of SMT Solvers (SCSC) RP: Non-linear Real Arithmetic Benchmarks derived from Automated Reasoning in Economics (SMT) Building Better Bit-Blasting for Floating-Point Problems (SMT) Selfless Interpolation for Infinite-State Model Checking (IJCAR) A Coinductive Approach to Proving Reachability in Logically Constrained Term Rewriting Systems (IJCAR) Implicit Hitting Set Algorithms for Maximum Satisfiability Modulo Theories (FCS) Homomorphisms and Minimality for Enrich-by-Need Security Analysis (ICLP) Shape Neutral Analysis of Graph-based Data-structures (ICLP) SMT-based Answer Set Solver CMODELS(DIFF) (System Description)
Satisfiability Modulo Theory	(IJCAR) Efficient Interpolation for the Theory of Arrays
satisfiability threshold	(SAT) Sharpness of the Satisfiability Threshold for Non-Uniform Random k-SAT
Satisfiablity Modulo Theories	(SMT) Alt-Ergo 2.2
SATsolvers	(SCSC) Hard Combinatorial Problems: A Challenge for Satisfiability
saturation	(POS) Divide and Conquer: Towards Faster Pseudo-Boolean Solving
Scaling	(Isabelle) Further Scaling of Isabelle Technology
Scheduling	(MoRe) Safe and Optimal Scheduling of Hard and Soft Tasks (RCRA) Greedy Randomized Search for Scalable Compilation of Quantum Circuits
Scoped channels	(DCM) Pointing to Private Names
Scott continuous map	(Domains13)
Scott domains	(Domains13) Invited Talk: Scott Domains for Denotational Semantics and Program Extraction
Scott topology	(Domains13) (Domains13) Invited Talk: Topology and Domain Theory Interfaces
Scott-Lemmon axioms	(EICNCL) Effective Translations between Display and Labelled Proofs for Tense Logics
Scrambling	(POS) The Effect of Scrambling CNFs
search	(RCRA) Computing Personalised Treatments through In Silico Clinical Trials. A Case Study on Downregulation in Assisted Reproduction.
Search space pruning	(ICLP) Improving Candidate Quality of Probabilistic Logic Models
Second Order Logic	(QBF) A Grounder From Second-Order Logic To QBF
second order quantifiers	(Linearity/TLLA) Proof nets, coends and the Yoneda isomorphism
second-order quantification	(Linearity/TLLA) A semantic conjecture on second-order MLL and its complexity consequences (work in progress)
secure channels	(CSF) A Cryptographic Look at Multi-Party Channels
Secure compilation	(CSF) Enforcing ideal-world leakage bounds in real-world secret sharing MPC frameworks (CSF) Secure compilation of side-channel countermeasures: the case of cryptographic “constant-time”
Secure multiparty computation	(CSF) Computer-aided proofs for multiparty computation with active security
securitisation	(TERMGRAPH) A Port-graph Model for Finance
Security	(CAV) Formal Verification of a Vehicle-to-Vehicle (V2V) Messaging System (CAV) The DEEPSEC prover (FM) Object-Oriented Security Proofs (FM) Variant Analysis with QL (FM) Software Safety and Security and AI (FM) Modular Verification of Programs with Effects and Effect Handlers in Coq (GraMSec) Combining Bayesian Networks and Fishbone Diagrams to Distinguish between Intentional Attacks and Accidental Technical Failures (Overture) Design Space Exploration for Secure Building Control (Overture) VDM at large: analysing the EMV Next Generation Kernel (ITP) Program Verification in the Presence of Cached Address Translation (CSF) Enforcing ideal-world leakage bounds in real-world secret sharing MPC frameworks (CSF) Formal Security Proof of CMAC and its Variants (VSTTE) SideTrail: Verifying Time-Balancing of Cryptosystems
security definitions	(CSF) Computer-aided proofs for multiparty computation with active security
Security Management	(AVOCS) Rule-Based Synthesis of Chains of Security Functions for Software-Defined Networks
Security Policy	(LPOP) Security Policies in Constraint Handling Rules
security protocols	(CSF) Automated Unbounded Verification of Stateful Cryptographic Protocols with Exclusive OR (CSF) A little more conversation, a little less action, a lot more satisfaction: Global states in ProVerif. (CSF) Composition Theorems for CryptoVerif and Application to TLS 1.3 (FCS) Proving physical proximity using symbolic models
security verification	(CAV) Lazy Self-Composition for Security Verification
selection functions	(MSFP) Backward induction for repeated games
selection monad	(MSFP) Backward induction for repeated games
selection network	(POS) Competitive Sorter-based Encoding of PB-Constraints into SAT
self-composition	(CAV) Lazy Self-Composition for Security Verification
Self-Driving vehicle	(VaVAS) Towards a verifiable decision making framework for self-driving vehicles
semantic forgetting	(IJCAR) FAME: An Automated Tool for Semantic Forgetting in Expressive Description Logics
Semantic model	(CSF) Types for Information Flow Control: Labeling Granularity and Semantic Models
semantic parsing	(NLCS) Graph Knowledge Representations for SICK (ICLP) Incremental and Iterative Learning of Answer Set Programs from Mutually Distinct Examples
Semantic View of Theories	(HoTT/UF) Univalent Foundations and the Constructive View of Theories
semantics	(DCM) Generic Graph Semantics (GraMSec) On Linear Logic, Functional Programming, and Attack Trees (LICS) Every λ-Term is Meaningful for the Infinitary Relational Model (QBF) Towards the Semantics of QBF Clauses (MSFP) Formalizing Constructive Quantifier Elimination in Agda (SAT) Local Soundness for QBF Calculi (CSF) Enforcing ideal-world leakage bounds in real-world secret sharing MPC frameworks (Linearity/TLLA) Entropy and Complexity Lower Bounds (Linearity/TLLA) From Linear Logic to Cyclic Sharing (VSTTE) Towards verification of Ethereum smart contracts: a formalization of core of Solidity (VSTTE) Formalising Executable Specifications of Low-Level Systems (WPTE) Automating the Diagram Method to Prove Correctness of Program Transformations
semantics of programming languages	(LICS) The Geometry of Computation-Graph Abstraction
Semantics preservation	(TERMGRAPH) Semantics-Preserving DPO-Based Term Graph Rewriting
semidefinite programming	(LICS) Definable Ellipsoid Method, Sums-of-Squares Proofs, and the Isomorphism Problem
Semilattices	(Domains13) Frames and frame relations
semisimplicial type	(HoTT/UF) Geometric realization of truncated semi-simplicial sets meta-constructed within HoTT
sensibility	(HOR) Refining Properties of Filter Models: Sensibility, Approximability and Reducibility
sensitivity analysis	(FM) Approximate Partial Order Reduction
Sentence Planning	(ICLP) Specifying and Verbalising Answer Set Programs in Controlled Natural Language
separability	(LICS) Separability by piecewise testable languages and downward closures beyond subwords
separation	(LICS) Probabilistic Böhm Trees and Probabilistic Separation
separation logic	(CAV) Permission Inference for Array Programs (CAV) Nagini: A Static Verifier for Python (AVOCS) An Entailment Checker for Separation Logic with Inductive Definitions (LICS) ReLoC: A Mechanised Relational Logic for Fine-Grained Concurrency (IJCAR) Verifying Asymptotic Time Complexity of Imperative Programs in Isabelle (IJCAR) A Separation Logic with Data: Small Models and Automation (ADSL) On the Complexity of Pointer Arithmetic in Separation Logic (ADSL) Cyclic Theorem Prover for Separation Logic by Magic Wand (ADSL) Labelled Cyclic Proofs for Separation Logic (ADSL) The Complexity of Prenex Separation Logic with One Selector (ADSL) Sloth: Separation Logic and Theories via Small Models (ADSL) A Complete Proof System for Basic Symbolic Heaps with Permissions (ITP) Backwards and Forwards with Separation Logic
Separations	(SAT) In Between Resolution and Cutting Planes: A Study of Proof Systems for Pseudo-Boolean SAT Solving
sequent calculi	(EICNCL) A Forward Calculus for Countermodel Construction in IPL
sequent calculus	(TYDI) Sequentialising nested systems (PARIS) Local Validity for Circular Proofs in Linear Logic with Fixed Points (WiL) A semantical view of sequent based systems (PAAR) Efficient translation of sequent calculus proofs into natural deduction proofs (LICS) A sequent calculus with dependent types for classical arithmetic (IJCAR) From Syntactic Proofs to Combinatorial Proofs (Linearity/TLLA) The structure of non decomposable connectives of linear logic (CL&C) Towards a Dualized Sequent Calculus with Canonicity (EICNCL) Sequent Calculi for Logic that Includes an Infinite Number of Modalities (EICNCL) Toward intuitionistic non-normal modal logic and its calculi
Sequential algorithms	(LICS) Extensional and Intensional Semantic Universes: A Denotational Model of Dependent Types
sequential types	(LICS) Every λ-Term is Meaningful for the Infinitary Relational Model
session types	(WiL) A New Linear Logic for Deadlock-Free Session-Typed Processes (Talk Abstract)
Set Membership	(SAT) XORSAT Set Membership Filters
Set Theory	(LFMTP) What Does This Notation Mean Anyway? BNF-style notation as it is actually used
sets with atoms	(LICS) On computability and tractability for infinite sets
SF-calculus	(Domains13) Domain Theory for Intensional Computation
shapes for higher-dimensional structure	(HoTT/UF) Ordered Cubes
shared-variable concurrent programs	(FM) Compositional Reasoning for Shared-variable Concurrent Programs
sharing	(DCM) A syntactic model of mutation and aliasing
sharpness	(SAT) Sharpness of the Satisfiability Threshold for Non-Uniform Random k-SAT
sheaf model	(Domains13) A Brouwerian proof of the Fan Theorem
shuffling calculus	(ITRS) Towards a Semantic Measure of the Execution Time in Call-by-Value lambda-Calculus
side conditions	(Coq) Procrastination, A proof engineering technique
Side-channel attack	(CAV) SCInfer: Refinement-based Verification of Software Countermeasures against Side-Channel Attacks
side-channels	(CSF) Symbolic Side-Channel Analysis for Probabilistic Programs (VSTTE) SideTrail: Verifying Time-Balancing of Cryptosystems
Sign-off	(FM) Interlocking Design Automation using Prover Trident
simple proof assistant	(UITP) Interfacing with a Prover using Focusing and Logic Programming
simple types	(FSCD) A Unifying Framework for Type Inhabitation (ITRS) Strong normalization of simple types through uniform intersection types.
Simplicial sets	(HoTT/UF) First-order homotopical logic and Grothendieck fibrations
Simplicial Type Theory	(HoTT/UF) (Truncated) Simplicial Models of Type Theory
Simply typed lambda calculus	(FSCD) Higher-Order Equational Pattern Anti-Unification
simply typed lambda terms	(RCRA) Shaving with Occam's Razor: Deriving Minimalist Theorem Provers for Minimal Logic
simulation	(CAV) Peregrine: A Tool for the Analysis of Population Protocols (TERMGRAPH) A Port-graph Model for Finance (VaVAS) RoboTool: Modelling and Verification with RoboChart (LOLA) A graph-rewriting perspective of the beta-law
Simulation of Turing Machines	(HDRA) Minimal Bacus FP is Turing Complete
Simulink	(FM) Verifying Auto-Generated C Code from Simulink
Simulink-based development	(FM) Formal Verification of Automotive Simulink Controller Models: Empirical Technical Challenges, Evaluation and Recommendations
Single Transferable Vote scheme	(VSTTE) Verified Certificate Checking for Counting Votes
singleton arc consistency	(RCRA) Partial (Neighbourhood) Singleton Arc Consistency for Constraint Satisfaction Problems
Singular DP-reduction	(SAT) Minimal unsatisfiability and minimal strongly connected digraphs
Size	(SAT) In Between Resolution and Cutting Planes: A Study of Proof Systems for Pseudo-Boolean SAT Solving
Skeptical Approach	(ITP) A Coq Tactic for Equality Learning in Linear Arithmetic
Skolem functions	(CAV) What’s hard about Boolean Functional Synthesis?
skolemization	(SR) Dependences in Strategy Logic
Skorohod's Theorem	(Domains13) A Domain-theoretic Skorohod’s Theorem
SLD-resolution	(TERMGRAPH) SLD-Resolution Reduction of Second-Order Horn Fragments - Extended Abstract
Smart Buildings	(Overture) Design Space Exploration for Secure Building Control
Smart Contract Verification	(CSF) KEVM: A Complete Formal Semantics of the Ethereum Virtual Machine
Smart contracts	(SMT) SMT-based Compile-time Verification of Safety Properties for Smart Contracts (VSTTE) Towards verification of Ethereum smart contracts: a formalization of core of Solidity
smart grid	(LICS) A Hybrid, Dynamic Logic for Hybrid-Dynamic Information Flow
Smart-Home Application	(ReMOTE) Moral Permissibility of Actions in Smart Home Systems
SMT	(CAV) Delta-Decision Procedures for Exists-Forall Problems over the Reals (CAV) Constraint-Based Synthesis of Coupling Proofs (CAV) Constrained Dynamic Partial Order Reduction (CAV) StringFuzz: A Fuzzer for String Solvers (SCSC) RP: Towards Incremental Cylindrical Algebraic Decomposition in Maple (SCSC) EA: SMT-like Queries in Maple (SCSC) EA: Wrapping Computer Algebra is Surprisingly Successful for Non-Linear SMT (FM) Z3 and SMT in Industrial R&D (SMT) The next 10^4 UppSAT Approximations (SMT) Building Better Bit-Blasting for Floating-Point Problems (SMT) Revisiting Enumerative Instantiation (SMT) SMT Solving Modulo Tableau and Rewriting Theories (SMT) Higher-Order SMT Solving (SMT) Rewrites for SMT Solvers using Syntax-Guided Enumeration (SMT) SMT-based Compile-time Verification of Safety Properties for Smart Contracts (SMT) What is the Point of an SMT-LIB Problem? (SMT) Puli - A Problem-Specific OMT Solver (SYNT) On Inductive Verification and Synthesis (Vampire) Giving AVATAR Quantifiers to Play With (Vampire) Experimenting with Theory Instantiation in Vampire (IJCAR) Datatypes with Shared Selectors (IJCAR) A Separation Logic with Data: Small Models and Automation (IJCAR) A Reduction from Unbounded Linear Mixed Arithmetic Problems into Bounded Problems (IJCAR) A Generic Framework for Implicate Generation Modulo Theories (IJCAR) Exploring Approximations for Floating-Point Arithmetic using UppSAT (IJCAR) Cubicle-W: Parameterized Model Checking on Weak Memory (ADSL) Sloth: Separation Logic and Theories via Small Models (SAT) Effective use of SMT solvers for Program Equivalence Checking through Invariant Sketching and Query Decomposition (SAT) Experimenting on Solving Nonlinear Integer Arithmetic with Incremental Linearization (VSTTE) Extending VIAP to Handle Array Programs
SMT Solver	(CAV) Formal Verification of a Vehicle-to-Vehicle (V2V) Messaging System (AVOCS) Writing a Model Checker in 80 Days: Reusable Libraries and Custom Implementation
SMT solvers	(CAV) The Proof Complexity of SMT Solvers (CAV) Controller Synthesis Made Real: Reach-avoid Specifications and Linear Dynamics (VSTTE) Lattice-Based Refinement in Bounded Model Checking (HCVS) Declarative Parameterized Verification of Topology-sensitive Distributed Protocols (ICLP) Solving Horn Clauses on Inductive Data Types Without Induction
SMT Solving	(CAV) MaxSMT-Based Type Inference for Python 3 (CAV) BTOR2, BtorMC and Boolector 3.0 (CAV) Solving Quantified Bit-Vectors using Invertibility Conditions (SCSC) RP: Evaluation of Equational Constraints for CAD in SMT Solving (SCSC) RP: Unknot Recognition Through Quantifier Elimination
SMT-based model checking	(FM) Formal Specification and Verification of Dynamic Parametrized Architectures
SMT-solving	(SMT) Centralizing Equality Reasoning in MCSAT
SMTLIB	(SCSC) EA: SMT-like Queries in Maple
Soft constraints	(PRUV) Evidential Group Decision Making Model with Belief-Based Preferences
Software as a Service	(Overture) Integrating VDM-SL into the continuous delivery pipelines of cloud-based software
software design	(LPOP) A software system should be declarative except where it interacts with the real world
software development	(FM) Disruptive Innovations for the Development and the Deployment of Fault-Free Software
Software Engineering	(FM) Z3 and SMT in Industrial R&D
software formal verification	(AVOCS) Climbing the Software Assurance Ladder - Practical Formal Verification for Reliable Software
Software model checking	(CAV) Let this Graph be your Witness! An Attestor for Verifying Java Pointer Programs (VSTTE) Executable Counterexamples in Software Model Checking
software model-checking	(VSTTE) Lattice-Based Refinement in Bounded Model Checking
Software Product Lines	(FM) QFLan: A Tool for the Quantitative Analysis of Highly Reconfigurable Systems
software productivity	(MLP) Measuring software development productivity: a machine learning approach
Software Testing	(CAV) Symbolic Liveness Analysis of Real-World Software
Software Tools	(LPOP) A Rule-Based Tool for Analysis and Generation of Graphs Applied to Mason's Marks
software verification	(CAV) On the Completeness of Verifying Message Passing Programs under Bounded Asynchrony (CAV) JBMC: A Bounded Model Checking Tool for Verifying Java Bytecode (FM) A Formally Verified Floating-Point Implementation of the Compact Position Reporting Algorithm (FM) Modular Verification of Programs with Effects and Effect Handlers in Coq (Vampire) Foundations of SPECTRE (IJCAR) Checking Array Bounds by Abstract Interpretation and Symbolic Expressions (ITP) Software Verification with ITPs Should Use Binary Code Extraction to Reduce the TCB (Short Paper)
Software-Defined Networking	(AVOCS) Rule-Based Synthesis of Chains of Security Functions for Software-Defined Networks
software-defined networks	(FM) SDN-Actors: Modeling and Verification of SDN Programs
Solidity	(VSTTE) Towards verification of Ethereum smart contracts: a formalization of core of Solidity
solution-based phase saving	(POS) Local-Style Search in the Linear MaxSAT Algorithm: A Computational Study of Solution-Based Phase Saving
Solvers	(ASPOCP) A Survey of Advances in Epistemic Logic Program Solvers
Solving	(ASPOCP) Invited Talk: Optimization Problems in Answer Set Programming
solving equations	(LICS) Satisfiability in multi-valued circuits
sound up-to techniques	(LICS) Sound up-to techniques and Complete abstract domains
Soundness	(Isabelle) Substitutionless First-Order Logic: A Formal Soundness Proof
source code	(MLP) Deep Learning On Code with an Unbounded Vocabulary (MLP) Splitting source code identifiers using Bidirectional LSTM Recurrent Neural Network
Space	(SAT) In Between Resolution and Cutting Planes: A Study of Proof Systems for Pseudo-Boolean SAT Solving
SPARK2014 and Critical Ada Software	(F-IDE) Lightweight Interactive Proving inside an Automatic Program Verifier
sparse Boolean functions	(LearnAut) Toward Learning Boolean Functions from Positive Examples
Spatial Reasoning	(ICLP) A Trajectory Calculus for Qualitative Spatial Reasoning Using Answer Set Programming
Species of Structures	(Linearity/TLLA) Generalized generalized species of structure and resource modalities
specification	(FM) IPL: An Integration Property Language for Multi-Model Cyber-Physical Systems (WST) Objective and Subjective Specifications
Specification Language	(LaSh) ESSENCE, A Language for Specifying Combinatorial Problems: What, Why and So What?
Specification-based monitoring	(CAV) A Counting Semantics for Monitoring LTL Specifications over Finite Traces
Splitting	(UNIF) Bounded ACh Unification
SQL	(GraMSec) Disclosure Analysis of SQL Workflows (ITP) A Coq Formalisation of SQL’S Execution Engines
Ssreflect	(ITP) A Formal Proof of the Minor-Exclusion Property for Treewidth-Two Graphs
Stability	(LICS) On the number of types in sparse graphs
stable model	(ICLP) Constraint Answer Set Programming without Grounding
stable model semantics	(ICLP) First-order answer set programming as constructive proof search
stably compact	(Domains13) Invited Talk: Topology and Domain Theory Interfaces
stably compact locale	(Domains13) Applications of entailments: de Groot duality
Stably Locally Compact	(Domains13) A logical view of complex analytic maps
Stack-Based Access Control	(CAV) Propositional Dynamic Logic for Higher-Order Functional Programs
star-autonomous categories	(Linearity/TLLA) Models of Linear Logic based on the Schwartz epsilon product
State Complexity	(LICS) The State Complexity of Alternating Automata
state injection	(LICS) Logical paradoxes in quantum computation
State machine	(VaVAS) RoboTool: Modelling and Verification with RoboChart
State monad	(LICS) A functional interpretation with state
state space minimisation	(FM) To Compose, Or Not to Compose, That is the Question: An Analysis of Compositional State Space Generation
state-merging	(LearnAut) Learning Several Languages from Labeled Strings: State Merging and Evolutionary Approaches
State-space abstraction	(CAV) Let this Graph be your Witness! An Attestor for Verifying Java Pointer Programs
stateful protocols	(CSF) A Typing Result for Stateful Protocols
Static Analysis	(CAV) Fast Numerical Program Analysis with Reinforcement Learning (CAV) Permission Inference for Array Programs (CAV) Constrained Dynamic Partial Order Reduction (ASPOCP) Datalog for Static Analysis Involving Logical Formulae (LCC) A General Equational Framework for Static Profiling of Parametric Resource Usage (IJCAR) Checking Array Bounds by Abstract Interpretation and Symbolic Expressions (IJCAR) A FOOLish Encoding of the Next State Relations of Imperative Programs (MLP) Difflog: Beyond Deductive Methods in Program Analysis (VSTTE) The Map Equality Domain
static analyzers	(WPTE) Verification of Ada Programs with AdaHorn
static dependency pairs	(WST) Improving Static Dependency Pairs for Higher-Order Rewriting
static equivalence problem	(UNIF) Knowledge Problems in Equational Extensions of Subterm Convergent Theories
Static Profiling	(LCC) A General Equational Framework for Static Profiling of Parametric Resource Usage
Static program analysis	(CAV) Program Analysis is Harder than Verification: A Computability Perspective (FM) Software Safety and Security and AI
static semantics	(IJCAR) Uniform Substitution for Differential Game Logic
Statistical Model Checking	(FM) Statistical Model Checking of LLVM Code (FM) QFLan: A Tool for the Quantitative Analysis of Highly Reconfigurable Systems (FCS) Statistical Model Checking of Guessing and Timing Attacks on Distance-bounding Protocols
Statistical relational learning	(ICLP) Constraint-Based Inference in Probabilistic Logic Programs
statistics	(Vampire) Testing ATP folklore: a statistical analysis of Vampire proofs.
Stedman	(POS) Stedman and Erin Triples encoded as a SAT Problem
Stedman Triples	(POS) Stedman and Erin Triples encoded as a SAT Problem
stepwise development	(FM) Stepwise Development and Model Checking of a Distributed Interlocking System - using RAISE
stereotypical activities	(ICLP) An ASP Methodology for Understanding Narratives about Stereotypical Activities
Stochastic Chemical Reaction Networks	(VEMDP) Molecular Filters for Noise Reduction
Stochastic dynamical systems and control	(VEMDP) Noise control for molecular computing
stochastic games	(CAV) Value Iteration for Simple Stochastic Games: Stopping Criterion and Learning Algorithm
stochastic hybrid game	(MoRe) Comfort and Energy Optimization for Floor Heating Systems
Stochastic hybrid system	(MoRe) Stochastic o-minimal hybrid systems
stochastic lambda calculus	(LICS) Boolean-Valued Semantics for Stochastic Lambda-Calculus
Stochastic modeling	(VEMDP) Computational Approaches for the Programmed Assembly of Nanocellulose Meshes
stochastic models	(VaVAS) Towards a Hierarchical-Control Architecture for Distributed Autonomous Systems (Extended Abstract - Paper)
Stochastic multi-scenario optimization	(MoRe) Multi-Scenario Uncertainty in Markov Decision Processes
stochastic process theory	(Domains13) A Domain-theoretic Skorohod’s Theorem
stochastic reachability	(VaVAS) Work-in-Progress: Adaptive Neighborhood Resizing for Stochastic Reachability in Distributed Flocking
stochastic shortest path	(LICS) Stochastic Shortest Paths and Weight-Bounded Properties in Markov Decision Processes
Stochastic simulation	(VEMDP) Rule-Based Gillespie Simulation of Chemical Systems
Stone Duality	(Domains13) A logical view of complex analytic maps (Domains13) Extending Stone Duality to Relations
Stone space	(LICS) On the number of types in sparse graphs
store buffer reduction	(VSTTE) Store Buffer Reduction in The Presence of Mixed-Size Accesses and Misalignment
Straight-Line Graphs	(LPOP) A Rule-Based Tool for Analysis and Generation of Graphs Applied to Mason's Marks
strategic graph rewriting	(TERMGRAPH) Finding the Transitive Closure of Functional Dependencies using Strategic Port Graph Rewriting
strategies	(SAT) Local Soundness for QBF Calculi
strategy languages	(TERMGRAPH) A Port-graph Model for Finance
Strategy Logic	(SR) Dependences in Strategy Logic (SR) Quantifying Bounds in Strategy Logic (SR) Strategy Logic with Imperfect Information (SR) Local Equilibria in Logic-Based Multi-Player Games
strategy synthesis	(MoRe) Safe and Optimal Scheduling of Hard and Soft Tasks (VaVAS) Probabilistic Model Checking for Autonomous Agent Strategy Synthesis - Extended Abstract
Streaming string transducers	(LICS) Regular and First Order List Functions
Streams	(LICS) A Generalized Modality for Recursion
Streett objectives	(CAV) Symbolic Algorithms for Graphs and Markov Decision Processes with Fairness Objectives
strict inequalities	(CAV) A Direct Encoding for NNC Polyhedra
Strict partial orders	(REFINE) Ordering strict partial orders to model behavioural refinement
strictification	(HDRA) Merge-bicategories: towards semi-strictification of higher categories
string data structure	(IWC) Coherence of monoids by insertions
string data structures	(HDRA) String data structures for Chinese monoids
string diagram	(HDRA) Normal forms for planar connected string diagrams
string diagrams	(FSCD) A diagrammatic axiomatisation of fermionic quantum circuits (TERMGRAPH) A framework for rewriting families of string diagrams (LICS) Enriching a Linear/Non-linear Lambda Calculus: A Programming Language for String Diagrams (LICS) Rewriting with Frobenius (LICS) Two complete axiomatisations of pure-state qubit quantum computing
string rewriting	(IWC) Coherence modulo relations (WST) Embracing Infinity - Termination of String Rewriting by Almost Linear Weight Functions (WST) Comparing on Strings: Semantic Kachinuki Order (ITP) Verification of PCP-Related Computational Reductions in Coq
strings	(CAV) StringFuzz: A Fuzzer for String Solvers
strong sums	(LICS) Strong Sums in Focused Logic
strongest postcondition	(ITP) Backwards and Forwards with Separation Logic
strongly normalizable terms	(ITRS)
Structural modeling	(VEMDP) Computational Approaches for the Programmed Assembly of Nanocellulose Meshes
Structural Operational Semantics	(IJCAR) A Logical Framework with Commutative and Non-Commutative Subexponentials
structural proof theory	(TYDI) Deep Inference, Herbrand's Theorem and Expansion Proofs
structural rules	(ARQNL) Labelled Calculi for QMLs with Non-Rigid and Non-Denoting Terms (EICNCL) Proof theory for quantified monotone modal logics
structure theory	(LICS) Satisfiability in multi-valued circuits
Structured Data	(LearnAut) Learning Graph Weighted Models on Pictures
stubborn sets	(CAV) Start Pruning When Time Gets Urgent: Partial Order Reduction for Timed Systems
subject reduction	(ITRS) Intersection Subtyping with Constructors
substitutability	(RCRA) Replaceability for constraint satisfaction problems: Algorithms, Inferences, and Complexity Patterns
Substitution	(Isabelle) Substitutionless First-Order Logic: A Formal Soundness Proof
substructural calculus	(Linearity/TLLA) Substructural Calculi with Dependent Types
subterm convergent theories	(UNIF) Knowledge Problems in Equational Extensions of Subterm Convergent Theories
subtyping	(FSCD) Cumulative Inductive Types in Coq (ITRS) Intersection Subtyping with Constructors
successor	(MSFP) Formalizing Constructive Quantifier Elimination in Agda
succinct ordered tree coding	(LICS) A pseudo-quasi-polynomial algorithm for solving mean-payoff parity games
SUMO	(Vampire) Towards Word Sense Disambiguation by Reasoning
sums of nonnegative circuit polynomials	(PC) Optimization over the Boolean Hypercube via Sums of Nonnegative Circuit Polynomials
sums of squares	(PC) Optimization over the Boolean Hypercube via Sums of Nonnegative Circuit Polynomials
sums-of-squares	(LICS) Definable Ellipsoid Method, Sums-of-Squares Proofs, and the Isomorphism Problem
superposition	(SMT) SMT Solving Modulo Tableau and Rewriting Theories (IJCAR) Superposition with Datatypes and Codatatypes (IJCAR) Superposition for Lambda-Free Higher-Order Logic
swarms	(Overture) Multi-modelling of Cooperative Swarms
switched systems	(MoRe) Comfort and Energy Optimization for Floor Heating Systems
SyGuS	(CAV) Syntax Guided Synthesis with Quantitative Syntactic Objectives
Sylleptic categories	(HDRA) Towards a fully formalized definition of syllepsis in weak higher categories
Symbol Elimination	(SYNT) On Inductive Verification and Synthesis
Symbolic Algorithms	(CAV) Symbolic Algorithms for Graphs and Markov Decision Processes with Fairness Objectives (SR) Solving Parity Games: Explicit vs Symbolic
Symbolic Analysis	(DS-FM) Analysis and Verification of Message Passing based Parallel Programs
symbolic automata	(CAV) The Learnability of Symbolic Automata
symbolic behavioral semantics	(AVOCS) Using SMT engine to generate Symbolic Automata
Symbolic computation	(SCSC) RP: Unknot Recognition Through Quantifier Elimination (SCSC) EA: Techniques for Natural-style Proofs in Elementary Analysis (ITP) HOL Light QE
symbolic constraints	(CSF) A Typing Result for Stateful Protocols
symbolic cryptography	(CSF) Symbolic security of garbled circuits
Symbolic evaluation	(ICLP) Constraint-Based Inference in Probabilistic Logic Programs
Symbolic Execution	(CAV) Formal Verification of a Vehicle-to-Vehicle (V2V) Messaging System (CAV) Symbolic Liveness Analysis of Real-World Software (CAV) Model Checking Boot Code from AWS Data Centers (ASPOCP) Datalog for Static Analysis Involving Logical Formulae (SYNT) Scalable Synthesis with Symbolic Syntax Graphs (ADSL) Automating the Flow Framework
symbolic heap	(ADSL) Cyclic Theorem Prover for Separation Logic by Magic Wand
Symbolic heaps	(ADSL) A Complete Proof System for Basic Symbolic Heaps with Permissions
Symbolic model	(CAV) The DEEPSEC prover
symbolic models	(FCS) Proving physical proximity using symbolic models
symbolic sampling	(CSF) Symbolic Side-Channel Analysis for Probabilistic Programs
symbolic security	(CSF) Symbolic security of garbled circuits
Symmetric monoidal categories	(LICS) Rewriting with Frobenius
symmetric monoidal closed bicategories	(LOLA) Asynchronous games fifteen years later
Symmetries	(SAT) Symmetries for QBF
Symmetry breaking	(IJCAR) Investigating the Existence of Large Sets of Idempotent Quasigroups via Satisfiability Testing (SAT) Symmetries for QBF
Symmetry reduction	(FM) View abstraction for systems with component identities
Symmetry-Breaking Predicates	(CAV) Exploiting Synchrony and Symmetry in Relational Verification
Synchronization	(REFINE) Refining Santa: An Excercise in Efficient Synchronization
synchronizations	(FM) A lightweight deadlock analysis technique of object-oriented programs
Synchronous Programming	(LICS) A Generalized Modality for Recursion
syntactic models	(DCM) A syntactic model of mutation and aliasing
syntax	(PAAR) TFX: The TPTP Extended Typed First-order Form
Syntax guided synthesis	(CAV) Synthesis Modulo Theories
syntax of type theory	(HoTT/UF) Towards the syntax and semantics of higher dimensional type theory
syntax with binding	(MSFP) Everybody's Got To Be Somewhere
Syntax-guided Synthesis	(SMT) Rewrites for SMT Solvers using Syntax-Guided Enumeration (IJCAR) Datatypes with Shared Selectors
synthesis	(CAV) Rabinizer 4: From LTL to Your Favourite Deterministic Automaton (CAV) Synthesizing Reactive Systems from Hyperproperties (CAV) Understanding and Extending Incremental Determinization for 2QBF (CAV) Synthesis Of Asynchronous Reactive Programs From Temporal Specifications (CAV) Attracting Tangles to Solve Parity Games (SYNT) Safe, Automated and Formal Synthesis of Digital Controllers for Continuous Plants (SYNT) Minimal Synthesis of String To String Functions From Examples (SYNT) Scalable Synthesis with Symbolic Syntax Graphs (LICS) Logics for Word Transductions with Synthesis (IJCAR) FORT 2.0
Synthetic Biology	(VEMDP) Bayesian Verification of Chemical Reaction Networks
Synthetic Data	(FCS) LISA: Predicting the Impact of DoS Attacks on Real-World Low Power IoT Systems
Synthetic Geometry	(ThEdu) Towards intuitive reasoning in axiomatic geometry
synthetic measure theory	(Domains13) Invited Talk: A domain theory for quasi-Borel spaces and statistical probabilistic programming
Synthetic Topology	(HoTT/UF) Cohesive Covering Theory
system architectures	(FM) Formal Specification and Verification of Dynamic Parametrized Architectures
System Composition	(LICS) Sequential Relational Decomposition
system description	(IJCAR) The Higher-Order Prover Leo-III
system F	(LICS) Impredicative Encodings of (Higher) Inductive Types
System Verification	(VaVAS) Towards a verifiable decision making framework for self-driving vehicles
System-based design	(CSF) Guided design of attack trees: a system-based approach
Systematic Testing	(CAV) Partial Order Aware Concurrency Sampling
systematicity	(WiL) Towards a Logical Framework for Latent Variable Modelling
Systems Biology	(VEMDP) Bayesian Verification of Chemical Reaction Networks
Systems decomposition	(LICS) Sequential Relational Decomposition
Systems of recursion equations	(FSCD) Term-Graph Anti-Unification
SystemVerilog Assertions	(PLR) RTLCheck: Automatically Verifying the Memory Consistency of Processor RTL
syzygies	(IWC) The diamond lemma for free modules
T
Tableau calculus	(IJCAR) A Tableaux Calculus for Reducing Proof Size
Tableaux	(SMT) SMT Solving Modulo Tableau and Rewriting Theories (IJCAR) From Syntactic Proofs to Combinatorial Proofs
tabling	(ICLP) Top-down and Bottom-up Evaluation Procedurally Integrated
Tactics	(Coq) Proof Construction by Tactic Learning (ITP) Tactics and Certificates in Meta Dedukti
tail bound	(ITP) Verified Tail Bounds for Randomized Programs
taint analysis	(CAV) Lazy Self-Composition for Security Verification
Taylor expansion	(LICS) Species, Profunctors and Taylor Expansion Weighted by SMCC--A Unified Framework for Modelling Nondeterministic, Probabilistic and Quantum Programs-- (Linearity/TLLA) On the Taylor expansion of λ-terms and the groupoid structure of their rigid approximants
Taylor expansion of lambda-terms	(HOR) Normalization and Taylor expansion of lambda-terms
Taylor models	(CAV) Inner and Outer Approximating Flowpipes for Delay Differential Equations
TCP server	(UITP) Isabelle/PIDE after 10 years of development
teaching	(WST) TTT2 with Termination Templates for Teaching
Teaching computer science with proof assistants	(ITP) CalcCheck: a Proof Checker for Teaching the “Logical Approach to Discrete Math”
Technical failure	(GraMSec) Combining Bayesian Networks and Fishbone Diagrams to Distinguish between Intentional Attacks and Accidental Technical Failures
technological systems	(ReMOTE) Elements of a Model of Trust in Technology
Technology	(Isabelle) Further Scaling of Isabelle Technology
templates	(WST) TTT2 with Termination Templates for Teaching
Temporal Answer Set Programming	(ICLP) Temporal Answer Set Programming on Finite Traces
temporal logic	(CAV) Synthesis Of Asynchronous Reactive Programs From Temporal Specifications (SYNT) Maximum Realizability for Linear Temporal Logic Specifications (PAAR) Evaluating Pre-Processing Techniques for the Separated Normal Form for Temporal Logics
temporal logic of repeating values	(LICS) Playing with Repetitions in Data Words Using Energy Games
Temporal logics	(VaVAS) Policy Generation with Probabilistic Guarantees for Long-term Autonomy of a Mobile Service Robot
Temporal Verification	(CAV) Propositional Dynamic Logic for Higher-Order Functional Programs (LICS) A Fixpoint Logic and Dependent Effects for Temporal Property Verification
Tense logic	(EICNCL) Effective Translations between Display and Labelled Proofs for Tense Logics
Tensor logic	(LICS) Around Classical and Intuitionistic Linear Logics
tensorflow	(LICS) The Geometry of Computation-Graph Abstraction
tensorial logic	(LICS) Ribbon tensorial logic
Term graph transformation	(TERMGRAPH) Semantics-Preserving DPO-Based Term Graph Rewriting
term orderings	(IJCAR) MaedMax: A Maximal Ordered Completion Tool
term rewriting	(IWC) Towards a Verified Decision Procedure for Confluence of Ground Term Rewrite Systems in Isabelle/HOL (FSCD) ProTeM: A Proof Term Manipulator (FSCD) Term rewriting characterisation of LOGSPACE for finite and infinite data (TERMGRAPH) Drags: an algebraic framework for graph rewriting (HOR) Orthogonality and sequentiality in substructural Linear HRSs (WPTE) On Transforming Narrowing Trees into Regular Tree Grammars Generating Ranges of Substitutions
term rewriting systems	(FSCD) Completeness of Tree Automata Completion (TERMGRAPH) Programming by Term Rewriting (Coq) ComplCoq: Rewrite Hint Construction with Completion Procedures
termination	(IWC) Convergence of Simultaneously and Sequentially Unraveled TRSs for Normal Conditional TRSs (WST) Embracing Infinity - Termination of String Rewriting by Almost Linear Weight Functions (WST) Procedure-Modular Termination Analysis (WST) GPO: A Path Ordering for Graphs (WST) Comparing on Strings: Semantic Kachinuki Order (WST) Termination of Lambda-Pi modulo rewriting using the size-change principle (LICS) Efficient Algorithms for Asymptotic Bounds on Termination Time in VASS (HDRA) Termination in linear (2,2)-categories with braidings and duals (WPTE) Reducing Total Correctness to Partial Correctness by a Transformation of the Language Semantics
termination analysis	(WST) Improving Static Dependency Pairs for Higher-Order Rewriting (WST) Control-Flow Refinement via Partial Evaluation
termination proofs	(TERMGRAPH) On quasi ordinal diagram systems (IJCAR) Well-Founded Unions
Termination Proving	(CAV) Syntax-Guided Termination Analysis
termination tools	(WST) TTT2 with Termination Templates for Teaching
test case generation	(CAV) The JKind Model Checker
text documents	(F-IDE) Isabelle/jEdit as IDE for domain-specific formal languages and informal text documents
text-based interaction	(UITP) Adding Text-Based Interaction to a Direct-Manipulation Interface for Program Verification -- Lessons Learned
textual inference	(NLCS) Graph Knowledge Representations for SICK
The Coq Proof Assistant	(ITP) A Coq Tactic for Equality Learning in Linear Arithmetic
the MRDP theorem	(LICS) A parameterized halting problem, the linear time hierarchy, and the MRDP theorem
The Santa Claus Problem	(REFINE) Refining Santa: An Excercise in Efficient Synchronization
theorem proving	(FSCD) Completion for Logically Constrained Rewriting (FM) Z3 and SMT in Industrial R&D (SMT) What is the Point of an SMT-LIB Problem? (PAAR) Set of Support for Higher-Order Reasoning (PAAR) Dynamic Strategy Priority: Empower the strong and abandon the weak (IJCAR) An abstraction-refinement framework for reasoning with large theories (IJCAR) Superposition with Datatypes and Codatatypes (IJCAR) MaedMax: A Maximal Ordered Completion Tool (F-IDE) Experience Report on Formally Verifying Parts of OpenJDK's API with KeY (ITP) Understanding Parameters of Deductive Verification: an Empirical Investigation of KeY (VaVAS) RoboTool: Modelling and Verification with RoboChart (VSTTE) Formalising Executable Specifications of Low-Level Systems (VSTTE) Verified Certificate Checking for Counting Votes (RCRA) Shaving with Occam's Razor: Deriving Minimalist Theorem Provers for Minimal Logic (ICLP) Certified Graph View Maintenance with Regular Datalog
Theorem Proving by Induction	(CAV) Formally Verified Montgomery Multiplication
theories	(IJCAR) Theories as Types
theory	(VSTTE) Store Buffer Reduction in The Presence of Mixed-Size Accesses and Misalignment
Theory combination	(SMT) Proofs in conflict-driven theory combination
theory of arrays	(VSTTE) The Map Equality Domain
theory of bit-vectors	(SMT) Building Better Bit-Blasting for Floating-Point Problems
Theory of Computation	(LICS) A General Framework for Relational Parametricity
threads	(FM) A lightweight deadlock analysis technique of object-oriented programs
Time complexity Analysis	(IJCAR) Verifying Asymptotic Time Complexity of Imperative Programs in Isabelle
Time Models	(REFINE) Ordering strict partial orders to model behavioural refinement
Time Refinement	(REFINE) Ordering strict partial orders to model behavioural refinement
Time-varying graphs	(DCM) A Category Theoretic Interpretation of Gandy’s Principles for Mechanisms
Timed automata	(AVOCS) Backward reachability analysis for timed automata with data variables (ITP) MDP + TA = PTA: Probabilistic Timed Automata, Formalized (Short Paper)
timed systems	(CAV) Start Pruning When Time Gets Urgent: Partial Order Reduction for Timed Systems (FM) The Compound Interest in Relaxing Punctuality
timed-arc Petri nets	(CAV) Start Pruning When Time Gets Urgent: Partial Order Reduction for Timed Systems
timing	(REFINE) a Theory of Lazy Imperative Timing
timing attacks	(FCS) A Study on the Preservation on Cryptographic Constant-Time Security in the CompCert Compiler
timing transformations	(ITP) Verified Timing Transformations in Synchronous Circuits with LambdaPi-Ware
TLS	(CSF) Composition Theorems for CryptoVerif and Application to TLS 1.3
tool	(Isabelle) The remote_build Tool
Tool paper	(FM) QFLan: A Tool for the Quantitative Analysis of Highly Reconfigurable Systems
toolkit	(SAT) PySAT: A Python Toolkit for Prototyping with SAT Oracles
top tree	(IWC) Complete Axiom System of Cluster Algebra
top-down	(ICLP) Top-down and Bottom-up Evaluation Procedurally Integrated
topologicai logics	(WiL) About the unification type of topological logics over Euclidean spaces
Topological Quantum Computation	(DCM) Towards a Formal System for Topological Quantum Computation
topology	(Domains13) Invited Talk: Topology and Domain Theory Interfaces
total correctness	(WPTE) Reducing Total Correctness to Partial Correctness by a Transformation of the Language Semantics
Total Store Ordering	(CAV) Reasoning About TSO Programs Using Reduction and Abstraction
Totalizer	(SAT) Dynamic Polynomial Watchdog Encoding for Solving Weighted MaxSAT
tptp	(PAAR) TFX: The TPTP Extended Typed First-order Form
Trace semantics	(CSF) Guided design of attack trees: a system-based approach
traceability	(CAV) The JKind Model Checker
traced monoidal categories	(Linearity/TLLA) From Linear Logic to Cyclic Sharing
Traffic Scenarios	(SCSC) EA: Constraint Systems from Traffic Scenarios for the Validation of Autonomous Driving
Trajectory	(ICLP) A Trajectory Calculus for Qualitative Spatial Reasoning Using Answer Set Programming
transcendental syntax	(Linearity/TLLA) Coherent interaction graphs: a nondeterministic geometry of interaction for MLL
transducers	(LICS) Regular Transducer Expressions for Regular Transformations over infinite words
transduction	(LICS) Logics for Word Transductions with Synthesis (LICS) Definable decompositions for graphs of bounded linear cliquewidth
transition system	(FM) Deadlock Detection for Actor-based Coroutines (FM) Approximate Partial Order Reduction
Transition systems	(GraMSec) Deciding the Non-Emptiness of Attack trees
Transitive Closure	(PARIS) Transitive Closure Logic: Infinitary and Cyclic Proof Systems
Transitive closure logic	(WiL) Non-well-founded proof system for Transitive Closure Logic
Translation	(PAAR) Efficient translation of sequent calculus proofs into natural deduction proofs (CSF) Types for Information Flow Control: Labeling Granularity and Semantic Models
Translation Lookaside Buffer (TLB)	(ITP) Program Verification in the Presence of Cached Address Translation
translations	(Linearity/TLLA) Benchmarking Linear Logic Translations
treap	(ITP) Verified Analysis of Random Binary Tree Structures
Tree	(HDRA) Generalizations of the associative operad and convergent rewrite systems
tree automata	(FSCD) Completeness of Tree Automata Completion (LICS) Automaton-Based Criteria for Membership in CTL (LearnAut) Learning Tree Distributions by Hidden Markov Models (VSTTE) A Tree-Based Approach to Data Flow Proofs
tree automata completion	(FSCD) Completeness of Tree Automata Completion
tree constraints	(IJCAR) Deciding the First-Order Theory of an Algebra of Feature Trees with Updates
Tree Decompositions	(LaSh) Solving #SAT by Parameterized Algorithms: Exploiting Small Treewidth (SAT) Exploiting Treewidth for Projected Model Counting and its Limits
tree-depth	(LICS) Tree depth, quantifier elimination, and quantifier rank
Trees	(LICS) MSO Queries on Trees: Enumerating Answers under Updates Using Forest Algebras
treewidth	(LaSh) Solving #SAT by Parameterized Algorithms: Exploiting Small Treewidth (QBF) Tractability results for structured quantified CNF-formulas via knowledge compilation (SAT) QBF as an Alternative to Courcelle's Theorem
tripos	(ITP) Formalizing Implicative Algebras in Coq
Tripwires	(GraMSec) A state machine system for insider threat detection
True Concurrency	(TYDI) Truely Concurrent Processes in the Calculus of Structures (LICS) An Asynchronous Soundness Theorem for Concurrent Separation Logic
truncation levels	(LICS) Free Higher Groups in Homotopy Type Theory
trust	(ReMOTE) Elements of a Model of Trust in Technology
Trust Management	(LPOP) Security Policies in Constraint Handling Rules
trusted code base	(ITP) Software Verification with ITPs Should Use Binary Code Extraction to Reduce the TCB (Short Paper)
trusted computing base	(ITP) Software Verification with ITPs Should Use Binary Code Extraction to Reduce the TCB (Short Paper)
Tseitin formulas	(SAT) Cops-Robber games and the resolution of Tseitin formulas
tuple-generating dependencies	(IJCAR) Efficient Model Construction for Horn Logic with VLog: System Description
Turing degrees	(LICS) An answer to the Gamma question
tutoring	(ThEdu) Lucas Interpretation from Programmers’ Perspective
Two player games	(LICS) Playing with Repetitions in Data Words Using Energy Games
two-player games	(MoRe) Parameterized complexity of games with monotonically ordered omega-regular objectives
Two-player win/lose	(SR) Concurrent games and semi-random determinacy
two-variable logic	(LICS) Weighted model counting beyond two-variable logic
type classes	(ICLP-DC) Proof-relevant resolution for elaboration of programming languages
Type Inference	(CAV) MaxSMT-Based Type Inference for Python 3 (ITP) Formalization of a Polymorphic Subtyping Algorithm (ICLP) Proof-relevant Horn Clauses for Dependent Type Inference and Term Synthesis
type inference and type inhabitation	(RCRA) Shaving with Occam's Razor: Deriving Minimalist Theorem Provers for Minimal Logic
Type Inhabitation	(FSCD) A Unifying Framework for Type Inhabitation (F-IDE) User Support for the Combinator Logic Synthesizer Framework
Type reduction	(CL&C) A Denotational Model of the Typed Lambda-Mu Calculus
type refinement systems	(HOR) The next 700 (type-theoretical) denotational models ?
type system	(FM) A lightweight deadlock analysis technique of object-oriented programs (LICS) Causal Computational Complexity of Distributed Processes (CSF) Types for Information Flow Control: Labeling Granularity and Semantic Models (CSF) A Permission-Dependent Type System for Secure Information Flow Analysis
type systems	(SYNT) Scalable Synthesis with Symbolic Syntax Graphs (LICS) A Generalized Modality for Recursion (LICS) Work Analysis with Resource-Aware Session Types (LICS) A theory of linear typings as flows on 3-valent graphs (CSF) Enforcing ideal-world leakage bounds in real-world secret sharing MPC frameworks (VSTTE) Constructing Independently Verifiable Privacy-Compliant Type Systems for Message Passing between Black-Box Components
Type theory	(FSCD) Call-by-name Gradual Type Theory (FSCD) The clocks they are adjunctions. Denotational semantics for Clocked Type Theory (PARIS) What makes guarded types tick? (WiL) On Expanding Standard Notions of Constructivity (LICS) Computability Beyond Church-Turing via Choice Sequences (LICS) The Syntax and Semantics of Quantitative Type Theory (LICS) Guarded Computational Type Theory (IJCAR) Theories as Types (NLCS) Propositional Forms of Judgemental Interpretations (HoTT/UF) A Yoneda lemma-formulation of the univalence axiom (ITP) Efficient Mendler-Style Lambda-Encodings in Cedille (ITP) The Coinductive Formulation of Common Knowledge (Linearity/TLLA) Quantum programming made easy (VSTTE) Constructing Independently Verifiable Privacy-Compliant Type Systems for Message Passing between Black-Box Components
type-and-effect-systems	(LOLA) Experimenting with graded monads: certified grading-based program transformations
Type-based Development	(F-IDE) User Support for the Combinator Logic Synthesizer Framework
type-logical grammar	(IJCAR) A Logical Framework with Commutative and Non-Commutative Subexponentials
typed assembly languages	(LFMTP) Property-Based Testing of Abstract Machines: an Experience Report
typed lambda calculus	(NLCS) Do different syntactic trees yield different logical readings? Some remarks on head variables in typed lambda calculus.
Typed lambda-mu calculus	(CL&C) A Denotational Model of the Typed Lambda-Mu Calculus
typing results	(CSF) A Typing Result for Stateful Protocols
U
UD	(NLCS) OpenWordNet-PT: Taking Stock
Ultrametrics	(ITP) An Agda Formalization of Üresin & Dubois' Asynchronous Fixed-Point Theory
UML	(LPOP) Security Policies in Constraint Handling Rules
unambiguous	(LICS) Regular Transducer Expressions for Regular Transformations over infinite words
unary negation fragment	(LICS) Unary negation fragment with equivalence relations has the finite model property
unbounded vocabulary	(MLP) Deep Learning On Code with an Unbounded Vocabulary
Uncertain planning	(FM) Multi-Robot LTL Planning Under Uncertainty
Uncertainty	(PRUV) Evidential Group Decision Making Model with Belief-Based Preferences
Uncountability	(ThEdu) Proving in the Isabelle Proof Assistant that the Set of Real Numbers is not Countable
undecidability	(ITP) Verification of PCP-Related Computational Reductions in Coq (LOLA) Towards a library of formalised undecidable problems in Coq: The undecidability of intuitionistic linear logic
under-approximations	(CAV) Inner and Outer Approximating Flowpipes for Delay Differential Equations
unification	(UNIF) ACUI Unification modulo Ground Theories (UNIF) About the unification type of topological logics over Euclidean spaces (UNIF) Bounded ACh Unification (UNIF) Efficiency of a good but not linear nominal unification algorithm (LICS) Unification nets: canonical proof net quantifiers (UITP) Partial Regularization of First-Order Resolution Proofs
unification problem	(WiL) About the unification type of topological logics over Euclidean spaces
uniform interpolation	(IJCAR) FAME: An Automated Tool for Semantic Forgetting in Expressive Description Logics
uniform intersection types	(ITRS) Strong normalization of simple types through uniform intersection types.
uniform one-dimensional fragment	(LICS) Weighted model counting beyond two-variable logic
uniform proof	(PARIS) Coinductive Uniform Proofs: An Extended Abstract (speaker: Yue LI)
Uniform quasi-wideness	(LICS) On the number of types in sparse graphs
uniform substitution	(IJCAR) Uniform Substitution for Differential Game Logic
Unifying Theories of Programming	(Isabelle) Using Isabelle/UTP for the Verification of Sorting Algorithms: A Case Study
Uninterpreted Function Symbols	(CAV) The Proof Complexity of SMT Solvers
unions	(LICS) Degrees of Relatedness - A Unified Framework for Parametricity, Irrelevance, Ad Hoc Polymorphism, Intersections, Unions and Algebra in Dependent Type Theory
unions of relations	(IJCAR) Well-Founded Unions
unique normal form property	(IWC) Complete Axiom System of Cluster Algebra
unit equality	(IJCAR) Efficient encodings of first-order Horn formulas in equational logic
unit propagation	(IJCAR) QRAT+: Generalizing QRAT by a More Powerful QBF Redundancy Property (SAT) Approximately Propagation Complete and Conflict Propagating Constraint Encodings
unit testing	(Overture) Enhancing Testing of VDM-SL models
Univalence	(FCS) A Homotopical Approach to Cryptography
univalence axiom	(HoTT/UF) A Yoneda lemma-formulation of the univalence axiom
univalent foundations	(FSCD) Internal Universes in Models of Homotopy Type Theory (LICS) On Higher Inductive Types in Cubical Type Theory (HoTT/UF) A Yoneda lemma-formulation of the univalence axiom (HoTT/UF) Univalent Foundations and the Constructive View of Theories
universal algebra	(LICS) A universal-algebraic proof of the complexity dichotomy for Monotone Monadic SNP
universal IDE	(F-IDE) Isabelle/jEdit as IDE for domain-specific formal languages and informal text documents
Universe	(FCS) A Homotopical Approach to Cryptography
universes	(FSCD) Cumulative Inductive Types in Coq (FSCD) Internal Universes in Models of Homotopy Type Theory (LICS) Extensional and Intensional Semantic Universes: A Denotational Model of Dependent Types (LICS) Guarded Computational Type Theory
Unmanned Aircraft Systems	(FM) From Formal Requirements to Highly Assured Software for Unmanned Aircraft Systems
unraveling	(IWC) Convergence of Simultaneously and Sequentially Unraveled TRSs for Normal Conditional TRSs
Unsatisfiability proof generation	(POS) Two flavors of DRAT
untyped call by value lambda calculus	(ITP) A Formal Equational Theory for Call-by-Push-Value
untyped lambda calculus	(HOR) Refining Properties of Filter Models: Sensibility, Approximability and Reducibility
Unweighted Partial MaxSAT	(SAT) Solving MaxSAT with Bit-Vector Optimization
UPPAAL	(FM) 20 Years of "Real" Real-Time Model Checking
Usability	(F-IDE) User Support for the Combinator Logic Synthesizer Framework
user interface	(UITP) Automated Theorem Proving in a Chat Environment
User Studies	(SYNT) Programming by example: efficient, but not “helpful”
Utility Theory	(ITP) Towards Formal Foundations for Game Theory (Short Paper)
V
vacuity	(FM) Timed Vacuity
Vacuity Checking	(DS-FM) Consistency Checking of Functional Requirements
validation	(SAT) Polynomial-Time Validation of QCDCL Certificates (ITP) Fast Machine Words in Isabelle/HOL
Validation and verification	(VaVAS)
Value Iteration	(CAV) Value Iteration for Simple Stochastic Games: Stopping Criterion and Learning Algorithm (CAV) Sound Value Iteration
vampire	(Vampire) Experimenting with Theory Instantiation in Vampire (Vampire) Testing ATP folklore: a statistical analysis of Vampire proofs. (Vampire) Developments in Higher-order Theorem proving within Vampire (IJCAR) A FOOLish Encoding of the Next State Relations of Imperative Programs
variant analysis	(FM) Variant Analysis with QL
VC-density	(LICS) On the number of types in sparse graphs
VC-dimension	(LICS) On the number of types in sparse graphs
VDM	(Overture) Transforming an industrial case study from VDM++ to VDM-SL (Overture) Enhancing Testing of VDM-SL models
VDM-RT	(Overture) Overture FMU: Export VDM-RT Models as Tool-Wrapper FMUs
VDMJ	(Overture) VDM at large: analysing the EMV Next Generation Kernel
vector addition systems with states	(LICS) Efficient Algorithms for Asymptotic Bounds on Termination Time in VASS
vector Lyapunov functions	(FM) Vector Barrier Certificates and Comparison Systems
vector space	(ASPOCP) Partial Evaluation of Logic Programs in Vector Spaces
Vehicle-to-Vehicle	(CAV) Formal Verification of a Vehicle-to-Vehicle (V2V) Messaging System
verifiable electronic voting	(CSF) Machine-checked proofs for electronic voting: privacy and verifiability for Belenios
Verification	(DS-FM) A Formal Study of MANET Routing Protocols (CAV) Rabinizer 4: From LTL to Your Favourite Deterministic Automaton (CAV) Continuous formal verification of Amazon s2n (CAV) SCInfer: Refinement-based Verification of Software Countermeasures against Side-Channel Attacks (TERMGRAPH) Programming by Term Rewriting (FM) IPL: An Integration Property Language for Multi-Model Cyber-Physical Systems (FM) Towards `Verifying' a Water Treatment System (AVOCS) Analyzing Consistency of Formal Requirements (WST) Verification of Rewriting-based Query Optimizers (WST) Procedure-Modular Termination Analysis (SAT) Effective use of SMT solvers for Program Equivalence Checking through Invariant Sketching and Query Decomposition (ITP) Verified Timing Transformations in Synchronous Circuits with LambdaPi-Ware (ITP) A Formal Equational Theory for Call-by-Push-Value (CSF) Enforcing ideal-world leakage bounds in real-world secret sharing MPC frameworks (CSF) A little more conversation, a little less action, a lot more satisfaction: Global states in ProVerif. (VaVAS) RoboTool: Modelling and Verification with RoboChart (VSTTE) Formalising Executable Specifications of Low-Level Systems (VSTTE) A Formalization of the ABNF Notation and a Verified Parser of ABNF Grammars (VSTTE) Verification of Binarized Neural Networks via Inter-Neuron Factoring (VSTTE) SideTrail: Verifying Time-Balancing of Cryptosystems (FCS) LISA: Predicting the Impact of DoS Attacks on Real-World Low Power IoT Systems (SR) Quantifying Bounds in Strategy Logic (WPTE) Automating the Diagram Method to Prove Correctness of Program Transformations
verified compilation	(FCS) A Study on the Preservation on Cryptographic Constant-Time Security in the CompCert Compiler
verified compiler	(ITP) Software Verification with ITPs Should Use Binary Code Extraction to Reduce the TCB (Short Paper)
Verified Prover	(PAAR) A Verified Simple Prover for First-Order Logic
version control data	(MLP) Measuring software development productivity: a machine learning approach
Vienna Development Method (VDM)	(Overture) Integrating VDM-SL into the continuous delivery pipelines of cloud-based software
view	(FM) IPL: An Integration Property Language for Multi-Model Cyber-Physical Systems (LICS) Can One Escape Red Chains? Regular Path Queries Determinacy is Undecidable.
View abstraction	(FM) View abstraction for systems with component identities
Virtual Machine	(Overture) ViennaVM: a Virtual Machine for VDM-SL development
virtual physiological human	(RCRA) Computing Personalised Treatments through In Silico Clinical Trials. A Case Study on Downregulation in Assisted Reproduction.
Visualization	(ICLP) Experimenting with robotic intra-logistics domains (ICLP) CHRvis: Syntax and Semantics
Volume Computation	(PRUV) VolCE: An Efficient Tool for Solving #SMT(LA) Problems
Volume Estimation	(PRUV) VolCE: An Efficient Tool for Solving #SMT(LA) Problems
Von Neumann-Morgenstern Utility Theorem	(ITP) Towards Formal Foundations for Game Theory (Short Paper)
VSCode	(UITP) Isabelle/PIDE after 10 years of development
W
warm-start	(SYNT) Warm-Starting Fixed-Point Based Control Synthesis
Warren Abstract Machine	(VSTTE) TWAM: A Certifying Abstract Machine for Logic Programs
watchlist guidance	(ITP) ProofWatch: Watchlist Guidance for Large Theories in E
WCET analysis	(F-IDE) A Notebook Format for the Holistic Design of Embedded Systems
Weak Abstractness	(Domains13) Abstractness of Continuation Semantics for Asynchronous Concurrency
weak diamond property	(FSCD) Decreasing diagrams with two labels are complete for confluence of countable systems
weak memory	(IJCAR) Cubicle-W: Parameterized Model Checking on Weak Memory (LOLA) Denotational Event structure for relaxed memory
weak memory models	(FM) A wide-spectrum language for verification of programs on weak memory models (REFINE) Correctness of Concurrent Objects under Weak Memory Models
Weak omega category theory	(HDRA) Towards a fully formalized definition of syllepsis in weak higher categories
weak subgame perfect equilibria	(MoRe) Constraint Problem for Weak Subgame Perfect Equilibria with omega-regular Boolean Objectives
weak units	(HDRA) Merge-bicategories: towards semi-strictification of higher categories
Weakest precondition	(AVOCS) Backward reachability analysis for timed automata with data variables (ITP) Backwards and Forwards with Separation Logic
weakness	(FM) A Weakness Measure for GR(1) Formulae
Web Service Composition	(ICLP-DC) Natural Language Generation From Ontologies
Web services	(ICLP) Phylotastic: An Experiment in Creating, Manipulating, and Evolving Phylogenetic Biology Workflows Using Logic Programming
Web services composition	(ICLP) Phylotastic: An Experiment in Creating, Manipulating, and Evolving Phylogenetic Biology Workflows Using Logic Programming
Weighted MaxSAT	(SAT) Dynamic Polynomial Watchdog Encoding for Solving Weighted MaxSAT
weighted model counting	(LICS) Weighted model counting beyond two-variable logic
Weighted timed automata	(FM) Optimal and Robust Controller Synthesis Using Energy Timed Automata with Uncertainty
well-founded relations	(IJCAR) Well-Founded Unions
Well-foundedness	(WST) Well-founded models in proofs of termination
while programs with atoms	(LICS) On computability and tractability for infinite sets
wide-spectrum language	(FM) A wide-spectrum language for verification of programs on weak memory models
Wireless Networks	(RCRA) Optimal Fault-Tolerant Placement of Relay Nodes in a Mission Critical Wireless Network
Wireless Sensor Networks	(AVOCS) Formal Verification of Synchronisation, Gossip and Environmental Effects for Wireless Sensor Networks
witness generation	(IJCAR) FORT 2.0 (SAT) Fast Sampling of Perfectly Uniform Satisfying Assignments
Witnessing	(PC) Towards theories for positive polynomial time and monotone proofs with extension
witnessing theorems	(PC)
Word Sense Disambiguation	(Vampire) Towards Word Sense Disambiguation by Reasoning
wordnet	(Vampire) Towards Word Sense Disambiguation by Reasoning (NLCS) OpenWordNet-PT: Taking Stock
Workflow	(GraMSec) Disclosure Analysis of SQL Workflows
Workflows	(ICLP) Phylotastic: An Experiment in Creating, Manipulating, and Evolving Phylogenetic Biology Workflows Using Logic Programming
World View Constraints	(ICLP) Epistemic Logic Programs with World View Constraints
World View Rules	(ICLP) Epistemic Logic Programs with World View Constraints
World Views	(ASPOCP) A Survey of Advances in Epistemic Logic Program Solvers
Wreath Products	(LICS) Wreath Products of Distributive Forest Algebras
WS1S	(LaSh) A Derivative-Based Decision Procedure for WS1S
WSN	(SMT) Puli - A Problem-Specific OMT Solver
WV Facts	(ICLP) Epistemic Logic Programs with World View Constraints
X
XORSAT	(SAT) XORSAT Set Membership Filters
XSB	(LPOP) LPOP2018 XSB Position Paper
Y
yoneda	(MSFP) Profunctor Optics and the Yoneda Lemma
Yoneda isomorphism	(Linearity/TLLA) Proof nets, coends and the Yoneda isomorphism
Z
Zariski topology	(LICS) Polynomial Invariants for Affine Programs
Zielonka' s Algorithm	(PLR) An Efficient Zielonka's Algorithm for Parallel Parity Games
zw calculus	(FSCD) A diagrammatic axiomatisation of fermionic quantum circuits
zx calculus	(FSCD) A diagrammatic axiomatisation of fermionic quantum circuits
α
α-conversion	(UNIF) Efficiency of a good but not linear nominal unification algorithm