FLOC 2018: FEDERATED LOGIC CONFERENCE 2018

A
Abate, Alessandro	(MoRe) Logically-Constrained Reinforcement Learning (CAV) Synthesis Modulo Theories (SYNT) Safe, Automated and Formal Synthesis of Digital Controllers for Continuous Plants (VEMDP) Bayesian Verification of Chemical Reaction Networks (ADHS) Optimization-Based Design of Bounded-Error Estimators Robust to Missing Data (ADHS) Symbolic Models for Incrementally Stable Switched Systems with Aperiodic Time Sampling (ADHS) Data-Driven Switched Affine Modeling for Model Predictive Control (ADHS) On invariance and reachability on semialgebraic sets for linear dynamics (ADHS) On Generating A Variety of Unsafe Counterexamples for Linear Dynamical Systems (ADHS) Algorithm for Bernstein Polynomial Control Design (ADHS) Sufficient Conditions for Temporal Logic Specifications in Hybrid Dynamical Systems (ADHS) Control Synthesis and Classification for Unicycle Dynamics Using the Gradient and Value Sampling Particle Filters (ADHS) Learning and Verification of Feedback Control Systems Using Feedforward Neural Networks (ADHS) Input Design for Nonlinear Model Discrimination Via Affine Abstraction (ADHS) Mission Planning for Multiple Vehicles with Temporal Specifications using UxAS (ADHS) Temporal Logic Control of POMDPs Via Label-Based Stochastic Simulation Relations (ADHS) Computing Controlled Invariant Sets for Hybrid Systems with Applications to Model-Predictive Control (ADHS) Falsification of Temporal Logic Requirements Using Gradient Based Local Search in Space and Time (ADHS) An Interval-Based Sliding Horizon Motion Planning Method (ADHS) A controlled sewer system should be treated as a sampled data system with events (ADHS) Interacting Particle System-Based Estimation of Reach Probability for a Generalized Stochastic Hybrid System (ADHS) Language constrained stabilization of discrete- time switched linear systems: an LMI approach (ADHS) Compositional Analysis of Hybrid Systems Defined Over Finite Alphabets (ADHS) Temporal Logic Control of General Markov Decision Processes by Approximate Policy Refinement (ADHS) Benchmarks for Cyber-Physical Systems: A Modular Model Library for Building Automation Systems (ADHS) Nonuniform abstractions, refinement and controller synthesis with novel BDD encodings (ADHS) Compositional Abstraction-based Synthesis for Cascade Discrete-Time Control Systems (ADHS) Control Synthesis for Stochastic Switched Systems Using the Tamed Euler Method (ADHS) Approximate Abstractions of Markov Chains with Interval Decision Processes (ADHS) T-Barrier Certificates: A Continuous Analogy to K-Induction (ADHS) Compositional Synthesis of Finite Abstractions for Continuous-Space Stochastic Control Systems: A Small-Gain Approach (ADHS) Generating Dominant Strategies for Continuous Two-Player Zero-Sum Games (ADHS) Multi-Energy Scheduling Using a Hybrid Systems Approach (ADHS) Bounding Errors Due to Switching Delays in Incrementally Stable Switched Systems (ADHS) Tracking Control via Variable-gain Integrator and Lookahead Simulation: Application to Leader-follower Multiagent Networks (ADHS) CoasterX: A Case Study in Component-Driven Hybrid Systems Proof Automation (ADHS) Hybrid System Modeling of Multi-Agent Coverage Problems with Energy Depletion and Repletion (ADHS) On Approximate Predictability of Metric Systems (ADHS) Occupation Measure Methods for Modelling and Analysis of Biological Hybrid Systems (ADHS) Optimal Symbolic Controllers Determinization for BDD storage. (ADHS) Concentration of Measure for Chance-Constrained Optimization (ADHS) Stability of switched systems on non-uniform time domains with non commuting matrices (ADHS) Verifying nonlinear analog and mixed-signal circuits with inputs (ADHS) Higher-Dimensional Timed Automata (ADHS) Razumikhin-type Theorems on Practical Stability of Dynamic Equations on Time Scales (ADHS) A switched system approach to optimize mixing of fluids (ADHS) Safety Control, a Quantitative Approach (ADHS) Reachability Analysis for One Dimensional Linear Parabolic Equation (ADHS) Space-Time Budget Allocation for Marketing Over Social Networks (ADHS) Network-Aware Design of State-Feedback Controllers for Linear Wireless Networked Control Systems (ADHS) Hierarchical Model Predictive Control for Building Energy Management of Hybrid Systems (ADHS) Switch induced instabilities for stable power system DAE models (ADHS) Observability of Linear Hybrid Systems with Unknown Inputs and Discrete Dynamics Modeled by Petri Nets (ADHS) Statistical Verification of PCTL Using Stratified Samples (ADHS) Old-established methods in a new look: How HyPro speeds up reachability computations for hybrid systems (ADHS) Formal Synthesis of Control Strategies for Dynamical Systems (ADHS) Provably efficient algorithms on hybrid automata
Abate, Alessandro	(ADHS) Approximate Abstractions of Markov Chains with Interval Decision Processes
Abate, Alessandro	(ADHS) Benchmarks for Cyber-Physical Systems: A Modular Model Library for Building Automation Systems
Abate, Alessandro	(ADHS) Temporal Logic Control of General Markov Decision Processes by Approximate Policy Refinement
Abbas, Houssam	(rv4rise) Using the F1/10 Autonomous Racing Platform for Runtime Verification Research
Abbasizanjani, Hoda	(SAT) Minimal unsatisfiability and minimal strongly connected digraphs
Abbott, John	(SCSC) EA: New in CoCoA-5.2.4 and CoCoALib-0.99570 for SC-Square
Abdennadher, Slim	(ICLP) CHRvis: Syntax and Semantics
Abou-Msabah, Slimane	(RCRA) An Enhanced Genetic Algorithm with the BLF2G Guillotine Placement Heuristic for the Orthogonal Cutting-Stock Problem
Abrahamsson, Oskar	(IJCAR) Proof-Producing Synthesis of CakeML with I/O and Local State from Monadic HOL Functions
Abramsky, Samson	(GS) TBA (Domains13) Invited Talk: Approximating partial by total: fixpoint characterizations of back-and-forth equivalences (COALG) Coalgebra Dreams
Accattoli, Beniamino	(IFIP WG 1.6) TBA
Acclavio, Matteo	(IJCAR) From Syntactic Proofs to Combinatorial Proofs
Achermann, Reto	(ITP) Physical Addressing on Real Hardware in Isabelle/HOL
Achlioptas, Dimitris	(SAT) Fast Sampling of Perfectly Uniform Satisfying Assignments (SAT) Fast and Flexible Probabilistic Model Counting
Adams, Robin	(VSTTE) Constructing Independently Verifiable Privacy-Compliant Type Systems for Message Passing between Black-Box Components
Adjé, Assalé	(NSV) The Policy Iterations Algorithm is Actually a Newton Method
Aerts, Bram	(ICLP) Application of Logic-Based Methods to Machine Component Design
Affeldt, Reynald	(Coq) Classical Analysis with Coq
Afshari, Bahareh	(PARIS) Riding Modal Cycles
Agha-Mohammadi, Ali-Akbar	(ADHS) Temporal Logic Control of POMDPs Via Label-Based Stochastic Simulation Relations
Agrafiotis, Ioannis	(GraMSec) A state machine system for insider threat detection
Ahmadi, Mohamadreza	(ADHS) Compositional Analysis of Hybrid Systems Defined Over Finite Alphabets
Ahmed, Mansoor	(GraMSec) Tendrils of Crime: Visualizing the Diffusion of Stolen Bitcoins
Ahn, Ki Yung	(LICS) Quasi-Open Bisimilarity with Mismatch is Intuitionistic
Akazaki, Takumi	(FM) Falsification of Cyber-Physical Systems Using Deep Reinforcement Learning
Akgun, Ozgur	(LaSh) Automated Constraint Modelling with Conjure
Akiba, Ken	(CL&C) A Denotational Model of the Typed Lambda-Mu Calculus
Akshay, S.	(CAV) What’s hard about Boolean Functional Synthesis? (LICS) Distribution-based objectives for Markov Decision Processes
Al-Nuaimi, Mohammed	(VaVAS) Towards a verifiable decision making framework for self-driving vehicles
Alami, Rachid	(ReMOTE) TBA
Albarghouthi, Aws	(CAV) Constraint-Based Synthesis of Coupling Proofs
Albert, Elvira	(CAV) Constrained Dynamic Partial Order Reduction (FM) SDN-Actors: Modeling and Verification of SDN Programs (ICLP) Avoiding redundancies in the exploration of concurrent programs
Alcolei, Aurore	(GS) Resource-Tracking Concurrent Games
Alglave, Jade	(LOLA) Denotational Event structure for relaxed memory
All Workshop Participants,	(LPOP) Questions about RBAC challenge solutions (LPOP) Panel: Practice of Modeling and Programming (LPOP) Questions about logic and constraints in real-world applications (LPOP) Panel: Future of Programming with Logic and Knowledge (LPOP) Closing (LPOP) Role-Based Access Control via LogicBlox
Allamanis, Miltos	(MLP) Understanding & Generating Source Code with Graph Neural Networks
Allred, Joel	(LICS) A Simple and Optimal Complementation Algorithm for Büchi Automata
Almeida, José Bacelar	(CSF) Enforcing ideal-world leakage bounds in real-world secret sharing MPC frameworks
Alrajeh, Dalal	(FM) A Weakness Measure for GR(1) Formulae
Alt, Leonardo	(SMT) SMT-based Compile-time Verification of Safety Properties for Smart Contracts
Altenkirch, Thorsten	(LICS) Free Higher Groups in Homotopy Type Theory (HoTT/UF) Towards the syntax and semantics of higher dimensional type theory
Alturki, Musab A.	(FCS) Statistical Model Checking of Guessing and Timing Attacks on Distance-bounding Protocols
Alves, Gleifer	(VaVAS) Formalisation of the Rules of the Road for embedding into an Autonomous Vehicle Agent
Alves, Sandra	(FSCD) A Unifying Framework for Type Inhabitation (Linearity/TLLA) Termination of lambda-calculus linearization methods
Alviano, Mario	(ASPOCP) Invited Talk: Optimization Problems in Answer Set Programming (ICLP) A Trajectory Calculus for Qualitative Spatial Reasoning Using Answer Set Programming (ICLP) Cautious Reasoning in ASP via Minimal models and Unsatisfiable Cores (ICLP) Shared aggregate sets in answer set programming
Alvim, Mario S.	(FM) An Algebraic Approach for Reasoning About Information Flow
Amarioarei, Alexandru	(VEMDP) Computational Approaches for the Programmed Assembly of Nanocellulose Meshes
Amendola, Giovanni	(RCRA) Externally Supported Models for Efficient Computation of Paracoherent Answer Sets
Ames, Aaron	(ADHS) Temporal Logic Control of POMDPs Via Label-Based Stochastic Simulation Relations
Amiridze, Nino	(NLCS) Anti-Unification and Natural Language Processing
Amortila, Philip	(LearnAut) Learning Graph Weighted Models on Pictures
Américo, Arthur	(FM) An Algebraic Approach for Reasoning About Information Flow
Anand, Abhishek	(ITP) Towards Certified Meta-Programming with Typed Template-Coq
Anandkumar, Anima	(MLP) Deep Learning On Code with an Unbounded Vocabulary
Andersen, Jakob Lykke	(VEMDP) Rule-Based Gillespie Simulation of Chemical Systems
Anderson, David	(VEMDP) Noise control for molecular computing
Anderson, Greg	(CAV) Learning Abstractions for Program Synthesis
Anderson, Patrick	(ADHS) A switched system approach to optimize mixing of fluids
Anderson, Ross	(GraMSec) Tendrils of Crime: Visualizing the Diffusion of Stolen Bitcoins
Angelos, Daniella	(WiL) On the Combination of Resolution and SAT Procedures for Modal Theorem-Proving
Angiuli, Carlo	(HoTT/UF) Cubical Computational Type Theory
Antoniou, Grigoris	(ICLP) A Trajectory Calculus for Qualitative Spatial Reasoning Using Answer Set Programming
Antunes, Duarte	(ADHS) A switched system approach to optimize mixing of fluids
Aoto, Takahito	(FSCD) Confluence Competition 2018
Araki, Keijiro	(Overture) ViennaVM: a Virtual Machine for VDM-SL development
Arcaini, Paolo	(F-IDE) AsmetaF: a flattener for the ASMETA framework
Arcucci, Rossella	(PLR) An Efficient Zielonka's Algorithm for Parallel Parity Games
Argyros, George	(LearnAut) The Learnability of Symbolic Automata
Argyros, George	(CAV) The Learnability of Symbolic Automata
Arias, Joaquin	(ICLP) Constraint Answer Set Programming without Grounding
Arnaboldi, Luca	(FCS) LISA: Predicting the Impact of DoS Attacks on Real-World Low Power IoT Systems
Arndt, Hannah	(CAV) Let this Graph be your Witness! An Attestor for Verifying Java Pointer Programs
Aryal, Deepak	(Isabelle) Hilbert Meets Isabelle: Formalisation of the DPRM Theorem in Isabelle
Asada, Kazuyuki	(LICS) Species, Profunctors and Taylor Expansion Weighted by SMCC--A Unified Framework for Modelling Nondeterministic, Probabilistic and Quantum Programs--
Asadi, Sepideh	(VSTTE) Lattice-Based Refinement in Bounded Model Checking
Aschieri, Federico	(ITRS) Natural Deduction and Normalization Proofs for the Intersection Type Discipline (CL&C) On Natural Deduction for Herbrand Constructive Logics III: The Strange Case of the Intuitionistic Logic of Constant Domains
Athanasiou, Konstantinos	(VSTTE) SideTrail: Verifying Time-Balancing of Cryptosystems
Atkey, Robert	(LICS) The Syntax and Semantics of Quantitative Type Theory
Atkinson, Liam	(MLP) Learning to Type
Atserias, Albert	(LICS) Definable Ellipsoid Method, Sums-of-Squares Proofs, and the Isomorphism Problem
Audinot, Maxime	(GraMSec) Deciding the Non-Emptiness of Attack trees (CSF) Guided design of attack trees: a system-based approach
Avanzini, Martin	(IFIP WG 1.6) TBA
Avelar, Andréia B.	(ITP) Formalizing Ring Theory in PVS (Short Paper)
Avellaneda, Florent	(FM) FSM Inference from Long Traces
Avgustinov, Pavel	(FM) Variant Analysis with QL
Avni, Guy	(SR) Infinite-Duration Richman Bidding Games
Awodey, Steve	(LICS) Impredicative Encodings of (Higher) Inductive Types
Ayala-Rincon, Mauricio	(FSCD) Fixed-Point Constraints for Nominal Equational Unification
Azadbakht, Keyvan	(FM) Deadlock Detection for Actor-based Coroutines
Azizi-Sultan, Ahmad-Saher	(ARQNL) Pseudo-Propositional Logic
B
Baader, Franz	(UNIF) ACUI Unification modulo Ground Theories
Baba Ali, Ahmed Riadh	(RCRA) An Enhanced Genetic Algorithm with the BLF2G Guillotine Placement Heuristic for the Orthogonal Cutting-Stock Problem
Babic, Domagoj	(FLoC) Business Perspective on Software Analysis
Bacchus, Fahiem	(IJCAR) Implicit Hitting Set Algorithms for Maximum Satisfiability Modulo Theories (SAT) MaxSAT Evaluation 2018
Bacci, Giorgio	(LICS) An algebraic theory of Markov processes (LICS) Boolean-Valued Semantics for Stochastic Lambda-Calculus
Bacci, Giovanni	(FM) Optimal and Robust Controller Synthesis Using Energy Timed Automata with Uncertainty
Bacciu, Davide	(LearnAut) Learning Tree Distributions by Hidden Markov Models
Backeman, Peter	(SMT) The next 10^4 UppSAT Approximations (IJCAR) Exploring Approximations for Floating-Point Arithmetic using UppSAT
Backes, John	(CAV) The JKind Model Checker
Backhouse, Kevin	(FM) Variant Analysis with QL
Badelt, Stefan	(VEMDP) Equivalence of chemical reaction networks in a CRN-to-DNA compiler framework.
Badonnel, Rémi	(AVOCS) Rule-Based Synthesis of Chains of Security Functions for Software-Defined Networks
Baelde, David	(PARIS) Workshop introduction
Baeta, Nuno	(ThEdu) Rating of Geometric Automated Theorem Provers
Bahr, Patrick	(FSCD) Strict Ideal Completions of the Lambda Calculus (PARIS) What makes guarded types tick?
Baier, Christel	(MoRe) Conditioning and quantiles in Markovian models (LICS) Stochastic Shortest Paths and Weight-Bounded Properties in Markov Decision Processes
Baioletti, Marco	(RCRA) Algebraic Crossover Operators for Permutations
Bak, Stanley	(ADHS) Reachability Analysis for One Dimensional Linear Parabolic Equation
Bakker, Bert G.J.	(ADHS) Interacting Particle System-Based Estimation of Reach Probability for a Generalized Stochastic Hybrid System
Balco, Samuel	(ITP) Software Tool Support for Modular Reasoning in Modal Logics of Actions
Balduccini, Marcello	(ICLP) An ASP Methodology for Understanding Narratives about Stereotypical Activities
Balle, Borja	(FoPSS) Automata learning I (FoPSS) Automata learning II
Ban Kirigin, Tajana	(FCS) Statistical Model Checking of Guessing and Timing Attacks on Distance-bounding Protocols
Bannister, Callum	(ITP) Backwards and Forwards with Separation Logic
Bansal, Sorav	(SAT) Effective use of SMT solvers for Program Equivalence Checking through Invariant Sketching and Query Decomposition
Bansal, Suguman	(CAV) Automata vs Linear-Programming Discounted-Sum Inclusion (CAV) Synthesis Of Asynchronous Reactive Programs From Temporal Specifications
Barad, Gefry	(VEMDP) Computational Approaches for the Programmed Assembly of Nanocellulose Meshes
Baral, Chitta	(ICLP) Incremental and Iterative Learning of Answer Set Programs from Mutually Distinct Examples
Barany, Gergö	(LOLA) A more precise, more correct stack and register model for CompCert
Barbosa, Haniel	(SMT) Revisiting Enumerative Instantiation (SMT) Higher-Order SMT Solving (SMT) Rewrites for SMT Solvers using Syntax-Guided Enumeration (IJCAR) Datatypes with Shared Selectors
Barbosa, Manuel	(CSF) Enforcing ideal-world leakage bounds in real-world secret sharing MPC frameworks
Bardin, Sebastien	(CAV) Model Generation for Quantified Formulas: A Taint-Based Approach
Barendregt, Henk	(FSCD) Corrado Böhm: the white magician in programming and its semantics
Baritel-Ruet, Cécile	(CSF) Formal Security Proof of CMAC and its Variants
Barnett, Lee	(TERMGRAPH) Programming by Term Rewriting
Barr, Earl	(MLP) Bimodal Software Engineering
Barrett, Clark	(CAV) Solving Quantified Bit-Vectors using Invertibility Conditions (SMT) Rewrites for SMT Solvers using Syntax-Guided Enumeration (IJCAR) Datatypes with Shared Selectors
Barthe, Gilles	(LMW) Relational verification of probabilistic programs (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”
Bartocci, Ezio	(CAV) Reachable Set Over-approximation for Nonlinear Systems Using Piecewise Barrier Tubes (CAV) A Counting Semantics for Monitoring LTL Specifications over Finite Traces
Bartocci, Ezio	(ADHS) Verifying nonlinear analog and mixed-signal circuits with inputs
Baryannis, George	(ICLP) A Trajectory Calculus for Qualitative Spatial Reasoning Using Answer Set Programming
Basin, David	(CSF) Alethea: A Provably Secure Random Sample Voting Protocol
Basset, Nicolas	(LearnAut) Toward Learning Boolean Functions from Positive Examples (SR) Beyond admissibility: Dominance between chains of strategies
Baston, Colm	(ITP) The Coinductive Formulation of Common Knowledge
Batsakis, Sotiris	(ICLP) A Trajectory Calculus for Qualitative Spatial Reasoning Using Answer Set Programming
Batty, Mark	(QBF) PrideMM: QBFEVAL Benchmarks (QBFEval18 Contribution)
Bauer, Matthew	(CAV) Model checking indistinguishability of randomized security protocols
Bauer, Sabine	(LaSh) Decidable Linear Tree Constraints
Baumgartner, Alexander	(FSCD) Term-Graph Anti-Unification
Bayer, Jonas	(Isabelle) Hilbert Meets Isabelle: Formalisation of the DPRM Theorem in Isabelle
Becchi, Anna	(CAV) A Direct Encoding for NNC Polyhedra
Becker, Bernd	(SAT) Dynamic Polynomial Watchdog Encoding for Solving Weighted MaxSAT
Becker, Bernd	(QBF) Preprocessing for (D)QBF
Becker, Heiko	(FM) Combining Tools for Optimization and Analysis of Floating-Point Computations
Becker, Jan Steffen	(AVOCS) Analyzing Consistency of Formal Requirements
Beckert, Bernhard	(VSTTE) Relational Equivalence Proofs Between Imperative and MapReduce Algorithms
Bekki, Daisuke	(NLCS) Paychecks, Presupposition, and Dependent Types
Belardinelli, Francesco	(SR) Verification of Multi-agent Systems with Imperfect Information and Public Actions
Bellin, Gianluigi	(FSCD) Proof nets for bi-intuitionistic linear logic
Belta, Calin	(rv4rise) Signal classification using temporal logic (VaVAS) Formal Synthesis of Control Strategies for Dynamical Systems
Bembenek, Aaron	(ASPOCP) Datalog for Static Analysis Involving Logical Formulae
Ben Abdelali, Marwa	(REFINE) Programming Without Refinement
Ben Salah, Kais	(PRUV) Evidential Group Decision Making Model with Belief-Based Preferences
Bendkowski, Maciej	(FSCD) Counting Environments and Closures (HOR) Combinatorics of explicit substitutions (extended abstract)
Benjamin, Thibaut	(HDRA) Towards a fully formalized definition of syllepsis in weak higher categories
Bentkamp, Alexander	(IJCAR) Superposition for Lambda-Free Higher-Order Logic
Benton, Nick	(LOLA) Invited talk: Semantic Equivalence Checking for HHVM Bytecode
Bentzen, Martin Mose	(ReMOTE) Moral Permissibility of Actions in Smart Home Systems
Benzaken, Véronique	(Coq) A Coq mechanised formal semantics for real life SQL queries : Formally reconciling SQL and (extended) relational algebra. (ITP) A Coq Formalisation of SQL’S Execution Engines
Benzmüller, Christoph	(ARQNL) System Demonstration: The Higher-Order Prover Leo-III (SMT) Invited talk: Experiments in Universal Logical Reasoning --- How to utilise ATPs and SMT solvers for the exploration of axiom systems for category theory in free logic (IJCAR) The Higher-Order Prover Leo-III
Benzmüller, Christoph	(WiL) Embedding Intuitionistic Modal Logics in Higher-Order Logic. An Easy Task?
Berger, Philipp	(FM) Verifying Auto-Generated C Code from Simulink
Berger, Ulrich	(Domains13) Invited Talk: Scott Domains for Denotational Semantics and Program Extraction
Berkholz, Christoph	(PC) A Comparison of Algebraic and Semi-Algebraic Proof Systems
Berryhill, Ryan	(SAT) Finding all Minimal Safe Inductive Sets
Berthon, Raphaël	(SR) Strategy Logic with Imperfect Information
Bertozzi, Davide	(RCRA) Logic Programming approaches for routing fault-free and maximally-parallel Wavelength Routed Optical Networks on Chip (Application paper)
Bertrand, Nathalie	(LICS) Stochastic Shortest Paths and Weight-Bounded Properties in Markov Decision Processes
Berzish, Murphy	(CAV) StringFuzz: A Fuzzer for String Solvers
Bessa, Iury	(SYNT) Safe, Automated and Formal Synthesis of Digital Controllers for Continuous Plants
Bessai, Jan	(F-IDE) User Support for the Combinator Logic Synthesizer Framework
Beyene, Tewodros A.	(FM) Evidential and Continuous Integration of Software Verification Tools (WPTE) Verification of Ada Programs with AdaHorn
Beyersdorff, Olaf	(QBF) Discussion (SAT) Welcome to SAT 2018 (SAT) Award Ceremony
Beyersdorff, Olaf	(QBF) Size, Cost and Capacity: A Semantic Technique for Hard Random QBFs
Bhagyanath, Anoop	(ICLP) Optimal Scheduling for Exposed Datapath Architectures with Buffered Processing Units by ASP
Bhaskar, Siddharth	(LCC) Computability over locally finite structures from algebra
Bhatt, Devesh	(F-IDE) The CLEAR Way To Transparent Formal Methods
Bhayat, Ahmed	(Vampire) Developments in Higher-order Theorem proving within Vampire (PAAR) Set of Support for Higher-Order Reasoning
Bichler, Manuel	(ASPOCP) selp: A Single-Shot Epistemic Logic Program Solver
Bickford, Mark	(LICS) Computability Beyond Church-Turing via Choice Sequences
Bienmüller, Tom	(SCSC) EA: Constraint Systems from Traffic Scenarios for the Validation of Autonomous Driving
Biere, Armin	(CAV) BTOR2, BtorMC and Boolector 3.0 (SCSC) RP: A Practical Polynomial Calculus for Arithmetic Circuit Verification (IJCAR) Implicit Hitting Set Algorithms for Maximum Satisfiability Modulo Theories (POS) The Effect of Scrambling CNFs (POS) Two flavors of DRAT
Bigatti, Anna Maria	(SCSC) EA: New in CoCoA-5.2.4 and CoCoALib-0.99570 for SC-Square
Bingmann, Timo	(VSTTE) Relational Equivalence Proofs Between Imperative and MapReduce Algorithms
Birkedal, Lars	(LICS) ReLoC: A Mechanised Relational Logic for Fine-Grained Concurrency (HoTT/UF) Dependent Right Adjoint Types
Biró, Csaba	(SMT) Puli - A Problem-Specific OMT Solver
Bjorner, Nikolaj	(FM) Z3 and SMT in Industrial R&D (SAT) Constrained Image Generation Using Binarized Neural Networks with Decision Procedures
Blaauwbroek, Lasse	(Coq) Proof Construction by Tactic Learning
Blair, Richard	(ITP) Efficient Mendler-Style Lambda-Encodings in Cedille
Blanchet, Bruno	(CSF) Composition Theorems for CryptoVerif and Application to TLS 1.3
Blanchette, Jasmin Christian	(Isabelle) A Verified SAT Solver with Watched Literals Using Imperative HOL (Extended Abstract) (IJCAR) Superposition with Datatypes and Codatatypes (IJCAR) Formalizing Bachmair and Ganzinger's Ordered Resolution Prover (IJCAR) Superposition for Lambda-Free Higher-Order Logic
Blanchette, Jasmin Christian	(VDMW) Hands-on: Elevator pitch
Blanqui, Frédéric	(WST) Termination of Lambda-Pi modulo rewriting using the size-change principle
Blinkhorn, Joshua	(QBF) Size, Cost and Capacity: A Semantic Technique for Hard Random QBFs
Bliutze, Simon	(AVOCS) Using SMT engine to generate Symbolic Automata
Bloem, Roderick	(CAV) A Counting Semantics for Monitoring LTL Specifications over Finite Traces
Blondin, Michael	(CAV) Peregrine: A Tool for the Analysis of Population Protocols
Blot, Valentin	(LICS) Extensional and Intensional Semantic Universes: A Denotational Model of Dependent Types
Blotsky, Dmitry	(CAV) StringFuzz: A Fuzzer for String Solvers
Boag, Simon	(WiL) Towards a Logical Framework for Latent Variable Modelling
Bobot, Francois	(FM) A Formally Verified Floating-Point Implementation of the Compact Position Reporting Algorithm (SMT) Centralizing Equality Reasoning in MCSAT
Bockenek, Joshua	(Isabelle) Using Isabelle/UTP for the Verification of Sorting Algorithms: A Case Study
Bodik, Rastislav	(SYNT) Scalable Synthesis with Symbolic Syntax Graphs
Bodirsky, Manuel	(LICS) A universal-algebraic proof of the complexity dichotomy for Monotone Monadic SNP (IJCAR) Complexity of Combinations of Qualitative Constraint Satisfaction Problems
Bohrer, Brandon	(LICS) A Hybrid, Dynamic Logic for Hybrid-Dynamic Information Flow (VSTTE) TWAM: A Certifying Abstract Machine for Logic Programs
Boisseau, Guillaume	(MSFP) Profunctor Optics and the Yoneda Lemma
Bojanczyk, Mikolaj	(LCC) On polynomial time for infinite structures (LICS) On computability and tractability for infinite sets (LICS) Regular and First Order List Functions (LICS) Definable decompositions for graphs of bounded linear cliquewidth
Boker, Udi	(LICS) Automaton-Based Criteria for Membership in CTL
Bonacina, Maria Paola	(SMT) Proofs in conflict-driven theory combination
Bonakdarpour, Borzoo	(CSF) The Complexity of Monitoring Hyperproperties
Bonchi, Filippo	(LICS) Sound up-to techniques and Complete abstract domains (LICS) Rewriting with Frobenius
Bonet, Maria	(PC) On Dual-Rail Based MaxSAT Solving
Bonichon, Richard	(CAV) Model Generation for Quantified Formulas: A Taint-Based Approach
Bonifati, Angela	(ICLP) Certified Graph View Maintenance with Regular Datalog
Boralv, Arne	(FM) Interlocking Design Automation using Prover Trident
Bouajjani, Ahmed	(CAV) Reasoning About TSO Programs Using Reduction and Abstraction (CAV) On the Completeness of Verifying Message Passing Programs under Bounded Asynchrony (REFINE) Automated verification of linearizability
Boulier, Simon	(ITP) Towards Certified Meta-Programming with Typed Template-Coq
Boulmé, Sylvain	(Coq) What is the Foreign Function Interface of the Coq Programming Language? (ITP) A Coq Tactic for Equality Learning in Linear Arithmetic
Bourdais, Romain	(ADHS) Hierarchical Model Predictive Control for Building Energy Management of Hybrid Systems
Bouyer-Decitre, Patricia	(FM) Optimal and Robust Controller Synthesis Using Energy Timed Automata with Uncertainty (SR) Dependences in Strategy Logic
Bradford, Russell	(SCSC) RP: Non-linear Real Arithmetic Benchmarks derived from Automated Reasoning in Economics
Brain, Martin	(SMT) Building Better Bit-Blasting for Floating-Point Problems
Brandt, Kasper Fabæch	(UNIF) Formalization of First-Order Syntactic Unification
Brauer, Joerg	(FM) Model-Based Testing for Avionics Systems
Brazdil, Tomas	(LICS) Efficient Algorithms for Asymptotic Bounds on Termination Time in VASS
Brede, Nuria	(CL&C) The “duality of computation” from a fibrational perspective
Breik, Keenan	(VEMDP) Computing properties of stable configurations of thermodynamic binding networks
Brendel, Elliot	(ADHS) An Interval-Based Sliding Horizon Motion Planning Method
Breuvart, Flavien	(HOR) Refining Properties of Filter Models: Sensibility, Approximability and Reducibility
Breza, Michael	(AVOCS) Formal Verification of Synchronisation, Gossip and Environmental Effects for Wireless Sensor Networks
Brihaye, Thomas	(MoRe) Constraint Problem for Weak Subgame Perfect Equilibria with omega-regular Boolean Objectives (MoRe) Stochastic o-minimal hybrid systems
Brim, Lubos	(VEMDP) Executable Biochemical Space for Specification and Analysis of Biochemical Systems
Brockmeyer, Udo	(SCSC) EA: Constraint Systems from Traffic Scenarios for the Validation of Autonomous Driving
Broda, Krysia	(ThEdu) Towards intuitive reasoning in axiomatic geometry
Broda, Sabine	(FSCD) A Unifying Framework for Type Inhabitation
Bromberger, Martin	(IJCAR) A Reduction from Unbounded Linear Mixed Arithmetic Problems into Bounded Problems
Brookes, Stephen	(Domains13) Invited Talk: A Brief History of Denotational Semantics
Brotherston, James	(PARIS) An Introduction to Cyclic Proofs (PARIS) An Introduction to Cyclic Proofs (ADSL) On the Complexity of Pointer Arithmetic in Separation Logic
Bruni, Roberto	(LICS) Concurrency and Probability: Removing Confusion, Compositionally
Bruse, Florian	(PARIS) Collapses of Fixpoint Alternation Hierarchies in Low Type-Levels of Higher-Order Fixpoint Logic
Bruyère, Véronique	(MoRe) Parameterized complexity of games with monotonically ordered omega-regular objectives (MoRe) Constraint Problem for Weak Subgame Perfect Equilibria with omega-regular Boolean Objectives
Bryant, Aubrey	(GraMSec) On Linear Logic, Functional Programming, and Attack Trees
Buchholtz, Ulrik	(LICS) Cellular Cohomology in Homotopy Type Theory (LICS) Higher Groups in Homotopy Type Theory (HoTT/UF) (Truncated) Simplicial Models of Type Theory
Buchman, Ethan	(FRIDA) The latest gossip on BFT consensus
Bulychev, Egor	(MLP) Splitting source code identifiers using Bidirectional LSTM Recurrent Neural Network
Buruiana, Sebastian	(WPTE) Reducing Total Correctness to Partial Correctness by a Transformation of the Language Semantics
Bury, Guillaume	(SMT) Centralizing Equality Reasoning in MCSAT (SMT) SMT Solving Modulo Tableau and Rewriting Theories
Busard, Simon	(FM) Producing Explanations for Rich Logics
Busoniu, Lucian	(ADHS) Space-Time Budget Allocation for Marketing Over Social Networks
Buss, Sam	(PC) On OBBD Proofs (PC) On Dual-Rail Based MaxSAT Solving (PC) Complexity of expander-based reasoning and the power of monotone proofs
Butler, Michael	(VaVAS) Policing Functions for Machine Learning Systems
Bønneland, Frederik M.	(CAV) Start Pruning When Time Gets Urgent: Partial Order Reduction for Timed Systems
Büning, Julian	(CAV) Symbolic Liveness Analysis of Real-World Software
C
C. D. S. Oliveira, Bruno	(ITP) Formalization of a Polymorphic Subtyping Algorithm
Cabalar, Pedro	(ICLP) Functional ASP with Intensional Sets; Application to Gelfond-Zhang Agreggates (ICLP) Temporal Answer Set Programming on Finite Traces
Calinescu, Radu	(VaVAS) Towards a Hierarchical-Control Architecture for Distributed Autonomous Systems (Extended Abstract - Paper)
Cantor, Anthony	(CL&C) Towards a Dualized Sequent Calculus with Canonicity
Capelli, Florent	(PC) Proof systems for #SAT based on restricted circuits (QBF) Tractability results for structured quantified CNF-formulas via knowledge compilation
Capretta, Venanzio	(ITP) The Coinductive Formulation of Common Knowledge
Carbin, Michael	(LICS) Computable decision making on the reals and other spaces via partiality and nondeterminism
Cardelli, Luca	(VEMDP) Molecular Filters for Noise Reduction
Carette, Jacques	(ITP) HOL Light QE
Carlier, Sébastien	(LFMTP) What Does This Notation Mean Anyway? BNF-style notation as it is actually used
Carral, David	(IJCAR) Efficient Model Construction for Horn Logic with VLog: System Description
Carro, Manuel	(ICLP) Constraint Answer Set Programming without Grounding
Cassandras, Christos G.	(ADHS) Hybrid System Modeling of Multi-Agent Coverage Problems with Energy Depletion and Repletion
Castellan, Simon	(LOLA) Denotational Event structure for relaxed memory
Castellan, Simon	(LICS) The concurrent game semantics of Probabilistic PCF
Castellana, Daniele	(LearnAut) Learning Tree Distributions by Hidden Markov Models
Catta, Davide	(NLCS) Do different syntactic trees yield different logical readings? Some remarks on head variables in typed lambda calculus.
Cattaruzza, Dario	(SYNT) Safe, Automated and Formal Synthesis of Digital Controllers for Continuous Plants
Cauderlier, Raphaël	(ITP) Tactics and Certificates in Meta Dedukti
Cavalcanti, Ana	(VaVAS) RoboTool: Modelling and Verification with RoboChart
Cavallo, Evan	(HoTT/UF) Cubical Computational Type Theory
Cavezza, Davide Giacomo	(DS-FM) Heuristic-Based GR(1) Assumptions Refinement (FM) A Weakness Measure for GR(1) Formulae
Cerna, David	(FSCD) Higher-Order Equational Pattern Anti-Unification (PARIS) Towards the Automatic Construction of Schematic Proofs (UNIF) Towards Generalization Methods for Purely Idempotent Equational Theories
Cerone, Andrea	(FRIDA) Making Parallel Snapshot Isolation Serializable
Cervesato, Iliano	(Linearity/TLLA) Formalization of Automated Trading Systems in a Concurrent Linear Framework
Ceska, Milan	(CAV) ADAC: Automated Design of Approximate Circuits
Chadha, Rohit	(CAV) Model checking indistinguishability of randomized security protocols
Chakraborty, Supratik	(CAV) What’s hard about Boolean Functional Synthesis?
Chalub, Fabricio	(NLCS) OpenWordNet-PT: Taking Stock
Chand, Saksham	(TLA) Invariants in Distributed Algorithms
Chanseau Saint-Germain, Ken	(VEMDP) Conservative approximations of polymers
Chapoutot, Alexandre	(NSV) Discussion
Chapoutot, Alexandre	(ADHS) An Interval-Based Sliding Horizon Motion Planning Method
Charalambidis, Angelos	(ICLP) Approximation Fixpoint Theory and the Well-Founded Semantics of Higher-Order Logic Programs
Chatterjee, Krishnendu	(CAV) Symbolic Algorithms for Graphs and Markov Decision Processes with Fairness Objectives (LICS) Efficient Algorithms for Asymptotic Bounds on Termination Time in VASS
Chatzikyriakidis, Stergios	(NLCS) Propositional Forms of Judgemental Interpretations
Chaudhuri, Kaustuv	(LFMTP) Computation-as-deduction in Abella: work in progress
Chaudhuri, Swarat	(CAV) Automata vs Linear-Programming Discounted-Sum Inclusion (MLP) Program Synthesis as High-Level Machine Learning
Chen, Hongxu	(CSF) A Permission-Dependent Type System for Secure Information Flow Analysis
Chen, Hubie	(QBF) Discussion
Chen, Taolue	(CAV) Android Stack Systems
Chen, Yijia	(LICS) Tree depth, quantifier elimination, and quantifier rank (LICS) A parameterized halting problem, the linear time hierarchy, and the MRDP theorem
Chenavier, Cyrille	(IWC) The diamond lemma for free modules (HDRA) Generalizations of the associative operad and convergent rewrite systems
Cheng, Chih-Hong	(VSTTE) Verification of Binarized Neural Networks via Inter-Neuron Factoring
Cherif, Mohamed Sami	(VSTTE) Formalising Executable Specifications of Low-Level Systems
Cheung, Wai-Tak	(LICS) The Geometry of Computation-Graph Abstraction
Cheval, Vincent	(CAV) The DEEPSEC prover (CSF) A little more conversation, a little less action, a lot more satisfaction: Global states in ProVerif.
Chifflier, Pierre	(FM) Modular Verification of Programs with Effects and Effect Handlers in Coq
Chirkova, Rada	(FCS) An Expressive, Flexible and Uniform Logical Formalism for Attribute-based Access Control
Chlipala, Adam	(LICS) Computable decision making on the reals and other spaces via partiality and nondeterminism (ITP) Reification by Parametricity
Chockalingam, Sabarathinam	(GraMSec) Combining Bayesian Networks and Fishbone Diagrams to Distinguish between Intentional Attacks and Accidental Technical Failures
Chockler, Hana	(FM) Timed Vacuity (VSTTE) Lattice-Based Refinement in Bounded Model Checking
Chonev, Ventsislav	(SR) Infinite-Duration Richman Bidding Games
Chong, Stephen	(ASPOCP) Datalog for Static Analysis Involving Logical Formulae
Christiansen, David	(UNIF) Efficiency of a good but not linear nominal unification algorithm
Christiansen, Henning	(IWC) Confluence in Constraint Handling Rules: An overview from early, fundamental results to recent extensions including state invariants and conf. modulo equivalence.
Chrząszcz, Jacek	(VSTTE) A Java bytecode formalisation
Chuang, Xue An	(ADHS) CoasterX: A Case Study in Component-Driven Hybrid Systems Proof Automation
Chudnov, Andrey	(CAV) Continuous formal verification of Amazon s2n (CSF) Assuming you know: epistemic semantics of relational annotations for expressive flow policies
Ciabattoni, Agata	(EICNCL) Effective Translations between Display and Labelled Proofs for Tense Logics
Cimatti, Alessandro	(FM) Formal Specification and Verification of Dynamic Parametrized Architectures (SAT) Experimenting on Solving Nonlinear Integer Arithmetic with Incremental Linearization
Ciobaca, Stefan	(IJCAR) A Coinductive Approach to Proving Reachability in Logically Constrained Term Rewriting Systems (WPTE) Reducing Total Correctness to Partial Correctness by a Transformation of the Language Semantics
Ciobanu, Gabriel	(Domains13) Abstractness of Continuation Semantics for Asynchronous Concurrency
Cirstea, Corina	(COALG) Coalgebraic Logics: From Branching Time to Linear Time
Ciurezu, Bogdan	(Isabelle) Hilbert Meets Isabelle: Formalisation of the DPRM Theorem in Isabelle
Claessen, Koen	(IJCAR) Efficient encodings of first-order Horn formulas in equational logic (NLCS) Automatic test suite generation for PMCFG grammars
Clairambault, Pierre	(GS) Resource-Tracking Concurrent Games (GS) A definable game semantics for the linear quantum lambda-calculus (GS) Making parallel-or deterministic again: intentional full abstraction for por (LICS) The concurrent game semantics of Probabilistic PCF
Clark, Alexander	(LearnAut) Weak and Strong learning of Probabilistic Context-Free Grammars: theoretical and empirical perspectives
Clark, John	(REFINE) A more relaxed way to make concrete: uses of heuristic search to discover implementations
Claus, Maximilian	(WiL) Embedding Intuitionistic Modal Logics in Higher-Order Logic. An Easy Task?
Clouston, Ranald	(HoTT/UF) Dependent Right Adjoint Types
Clymo, Judith	(QBF) Short Proofs in QBF Expansion
Cock, David	(ITP) Physical Addressing on Real Hardware in Isabelle/HOL
Coglio, Alessandro	(VSTTE) A Formalization of the ABNF Notation and a Verified Parser of ABNF Grammars
Cohen, Cyril	(Coq) Classical Analysis with Coq (ITP) Towards Certified Meta-Programming with Typed Template-Coq
Cohen, Ernie	(FM) Object-Oriented Security Proofs
Cohen, Liron	(PARIS) Transitive Closure Logic: Infinitary and Cyclic Proof Systems (WiL) Non-well-founded proof system for Transitive Closure Logic (WiL) On Expanding Standard Notions of Constructivity (LICS) Computability Beyond Church-Turing via Choice Sequences
Cohen, William	(MLP) Answering Cloze-style Software Questions Using Stack Overflow
Cok, David	(VSTTE) Practical Methods for Reasoning about Java 8's Functional Programming Features
Colange, Maximilien	(SYNT) Reactive Synthesis from LTL Specification with Spot
Collins, Nathan	(CAV) Formal Verification of a Vehicle-to-Vehicle (V2V) Messaging System (CAV) Continuous formal verification of Amazon s2n
Colvin, Robert	(FM) A wide-spectrum language for verification of programs on weak memory models (REFINE) Correctness of Concurrent Objects under Weak Memory Models
Combette, Guillaume	(ITP) A Formal Proof of the Minor-Exclusion Property for Treewidth-Two Graphs (LOLA) A resource modality for RAII
Conchon, Sylvain	(DS-FM) Cubicle: a model checker for parameterized array-based transition systems (SMT) Alt-Ergo 2.2 (IJCAR) Cubicle-W: Parameterized Model Checking on Weak Memory (HCVS) Declarative Parameterized Verification of Topology-sensitive Distributed Protocols
Condie, Tyson	(ICLP) Declarative Algorithms in Datalog with Aggregates: user-friendly formal semantics conducive to performance and scalability
Condoluci, Andrea	(CL&C) Admissible tools in the kitchen of intuitionistic logic
Constable, Robert	(LICS) Computability Beyond Church-Turing via Choice Sequences
Contejean, Évelyne	(Coq) A Coq mechanised formal semantics for real life SQL queries : Formally reconciling SQL and (extended) relational algebra. (ITP) A Coq Formalisation of SQL’S Execution Engines
Cook, Byron	(FLoC) Amazon’s Automated Reasoning Group: Combining Amazon’s 14 foundational principles with the Strachey philosophy (VDMW) Learning from failure
Cook, Byron	(FLoC) Formal Reasoning about the Security of Amazon Web Services (CAV) Continuous formal verification of Amazon s2n (CAV) Model Checking Boot Code from AWS Data Centers (VSTTE) SideTrail: Verifying Time-Balancing of Cryptosystems
Cooksey, Simon	(QBF) PrideMM: QBFEVAL Benchmarks (QBFEval18 Contribution)
Copello, Ernesto	(LFMTP) Formalisation of Barendregt's Variable Convention for Generic Structures with Binders
Copes, Matrín	(LFMTP) Formalization in Constructive Type Theory of the Standardization Theorem
Copestake, Ann	(NLCS) Is compositionality all it's cracked up to be?
Coq Development Team,	(Coq) Discussion with the Coq development team
Coquand, Thierry	(LICS) On Higher Inductive Types in Cubical Type Theory (LICS) Univalent Type Theory
Coquereau, Albin	(SMT) Alt-Ergo 2.2
Cordeiro, Lucas	(CAV) JBMC: A Bounded Model Checking Tool for Verifying Java Bytecode (SYNT) Safe, Automated and Formal Synthesis of Digital Controllers for Continuous Plants
Cordero, Christophe	(HDRA) Generalizations of the associative operad and convergent rewrite systems
Corsi, Giovanna	(ARQNL) Labelled Calculi for QMLs with Non-Rigid and Non-Denoting Terms
Cortier, Véronique	(CSF) Machine-checked proofs for electronic voting: privacy and verifiability for Belenios (CSF) A little more conversation, a little less action, a lot more satisfaction: Global states in ProVerif.
Costa, Oswaldo Luiz V.	(ADHS) Network-Aware Design of State-Feedback Controllers for Linear Wireless Networked Control Systems
Costabile, Roberta	(LPOP) Role-Based Access Control via JASP
Coti, Camille	(CAV) Quasi-Optimal Partial Order Reduction
Cottrell, Thomas	(Domains13) Higher-dimensional categories: recursion on extensivity
Courcelle, Bruno	(LaSh) Monadic Second-Order Model Checking with Fly-Automata
Cousot, Patrick	(CAV) Program Analysis is Harder than Verification: A Computability Perspective
Couto, Rui	(F-IDE) Improving the Visualization of Alloy Instances
Cowen-Rivers, Alexander	(SCSC) RP: Towards Incremental Cylindrical Algebraic Decomposition in Maple
Crary, Karl	(LICS) Strong Sums in Focused Logic (VSTTE) TWAM: A Certifying Abstract Machine for Logic Programs
Creese, Sadie	(GraMSec) A state machine system for insider threat detection
Creissac Campos, José	(F-IDE) Improving the Visualization of Alloy Instances
Cropper, Andrew	(TERMGRAPH) SLD-Resolution Reduction of Second-Order Horn Fragments - Extended Abstract
Crouch, Richard	(NLCS) Graph Knowledge Representations for SICK
Cruanes, Simon	(SMT) SMT Solving Modulo Tableau and Rewriting Theories
Cruanes, Simon	(IJCAR) Superposition for Lambda-Free Higher-Order Logic
Crubillé, Raphaëlle	(LICS) Probabilistic stable functions on discrete cones are power series.
Csikász-Nagy, Attila	(VEMDP) Molecular Filters for Noise Reduction
Cunha, Alcino	(F-IDE) Improving the Visualization of Alloy Instances
Cuteri, Bernardo	(LPOP) Invited Talk: On the Development of Industrial Applications with ASP
Cvitkovic, Milan	(MLP) Deep Learning On Code with an Unbounded Vocabulary
Czajka, Łukasz	(FSCD) Term rewriting characterisation of LOGSPACE for finite and infinite data
Czarnik, Patryk	(VSTTE) A Java bytecode formalisation
Czeizler, Eugen	(VEMDP) Computational Approaches for the Programmed Assembly of Nanocellulose Meshes
Côrte-Real, Joana	(ICLP) Improving Candidate Quality of Probabilistic Logic Models
D
D'Antoni, Loris	(CAV) Syntax Guided Synthesis with Quantitative Syntactic Objectives (CAV) The Learnability of Symbolic Automata
D'Innocenzo, Alessandro	(ADHS) Approximate Abstractions of Markov Chains with Interval Decision Processes
D'Innocenzo, Alessandro	(ADHS) Data-Driven Switched Affine Modeling for Model Predictive Control
Daafouz, Jamal	(ADHS) Network-Aware Design of State-Feedback Controllers for Linear Wireless Networked Control Systems
Dabrowski, Yoann	(Linearity/TLLA) Models of Linear Logic based on the Schwartz epsilon product
Daggitt, Matthew L.	(ITP) An Agda Formalization of Üresin & Dubois' Asynchronous Fixed-Point Theory
Dahlem, Marc	(ICLP) Optimal Scheduling for Exposed Datapath Architectures with Buffered Processing Units by ASP
Daian, Philip	(CSF) KEVM: A Complete Formal Semantics of the Ethereum Virtual Machine
Dailler, Sylvain	(F-IDE) Lightweight Interactive Proving inside an Automatic Program Verifier
Dal Lago, Ugo	(DCM) On Higher-Order Probabilistic Computation. (GS) The Geometry of Concurrent Interaction: Handling Multiple Ports by Way of Multiple Tokens (LCC) Characterizing Complexity Classes in Presence of Higher-Order Functions — How Martin Hofmann Contributed to Shaping ICC
Dallmeyer, Nils	(WPTE) Optimizing Space of Parallel Processes
Dalmonte, Tiziano	(EICNCL) Toward intuitionistic non-normal modal logic and its calculi
Dang, Thao	(ADHS) Occupation Measure Methods for Modelling and Analysis of Biological Hybrid Systems
Danielski, Daniel	(LICS) Unary negation fragment with equivalence relations has the finite model property
Dantchev, Stefan	(PC) Resolution and the binary encoding of combinatorial principles
Dardha, Ornela	(WiL) A New Linear Logic for Deadlock-Free Session-Typed Processes (Talk Abstract)
Dartois, Luc	(LICS) Logics for Word Transductions with Synthesis
Darulova, Eva	(FM) Combining Tools for Optimization and Analysis of Floating-Point Computations
Darwiche, Adnan	(SoMLMFM) What Just Happened in AI (SoMLMFM) Panel session
Das, Ankush	(LICS) Work Analysis with Resource-Aware Session Types
Das, Anupam	(PC) Towards theories for positive polynomial time and monotone proofs with extension (TYDI) Proof complexity of deep inference: a survey (PARIS) On the Logical Complexity of Cyclic Arithmetic (LCC) A recursion-theoretic characterisation of the positive polynomial-time functions (IJCAR) Focussing, MALL and the polynomial hierarchy (CL&C) Some ideas on cut-elimination for cyclic arithmetic proofs (EICNCL) Cyclic proofs, hypersequents and Kleene algebra - Invited Talk
Das, Ariyam	(ICLP) Declarative Algorithms in Datalog with Aggregates: user-friendly formal semantics conducive to performance and scalability
Datta, Anupam	(SoMLMFM) Influence-directed explanations for machine learning systems
Dave, Vrunda	(LICS) Regular Transducer Expressions for Regular Transformations over infinite words
Davenport, James H.	(SCSC) RP: Non-linear Real Arithmetic Benchmarks derived from Automated Reasoning in Economics
Daviaud, Laure	(LICS) Regular and First Order List Functions (LICS) A pseudo-quasi-polynomial algorithm for solving mean-payoff parity games
David, Cristina	(CAV) Synthesis Modulo Theories (SYNT) Safe, Automated and Formal Synthesis of Digital Controllers for Continuous Plants (WST) Procedure-Modular Termination Analysis
David, Cristina	(VDMW) Should I join a startup?
David, Marco	(Isabelle) Hilbert Meets Isabelle: Formalisation of the DPRM Theorem in Isabelle
Dawson, Jeremy	(IJCAR) Well-Founded Unions
De Angelis, Emanuele	(HCVS) Metaprogramming and symbolic execution for detecting runtime errors in Erlang programs (ICLP) Solving Horn Clauses on Inductive Data Types Without Induction
De Boer, Frank	(FM) Deadlock Detection for Actor-based Coroutines
de Felice, Giovanni	(FSCD) A diagrammatic axiomatisation of fermionic quantum circuits
de Lima, Thaynara A.	(ITP) Formalizing Ring Theory in PVS (Short Paper)
de Lima, Tiago	(IJCAR) An Assumption-Based Approach for Solving The Minimal S5-Satisfiability Problem
de Melo, Gerard	(NLCS) OpenWordNet-PT: Taking Stock
de Moura, Leonardo	(FM) Efficient verification and metaprogramming in Lean
de Paiva, Valeria	(NLCS) Graph Knowledge Representations for SICK (NLCS) OpenWordNet-PT: Taking Stock (Linearity/TLLA) Benchmarking Linear Logic Translations (Linearity/TLLA) On the Lambek Calculus with an Exchange Modality
de Putter, Sander	(FM) To Compose, Or Not to Compose, That is the Question: An Analysis of Compositional State Space Generation
De Santis, Elena	(ADHS) On Approximate Predictability of Metric Systems
de Silva, Nadish	(LICS) Logical paradoxes in quantum computation
de Vink, Erik	(FM) Deadlock Detection for Actor-based Coroutines
De Visme, Marc	(GS) A definable game semantics for the linear quantum lambda-calculus
De Vos, Marina	(VaVAS) Social Consequence Engines (Abstract)
de Wolff, Timo	(PC) Optimization over the Boolean Hypercube via Sums of Nonnegative Circuit Polynomials
Debant, Alexandre	(FCS) Proving physical proximity using symbolic models
Declerck, David	(IJCAR) Cubicle-W: Parameterized Model Checking on Weak Memory
Defoort, Michael	(ADHS) Razumikhin-type Theorems on Practical Stability of Dynamic Equations on Time Scales
Defoort, Michael	(ADHS) Stability of switched systems on non-uniform time domains with non commuting matrices
Delahaye, David	(SMT) SMT Solving Modulo Tableau and Rewriting Theories
Delaune, Stephanie	(FSCD) Analysing privacy-type properties in cryptographic protocols (FCS) Proving physical proximity using symbolic models
Delpeuch, Antonin	(HDRA) Normal forms for planar connected string diagrams
Delzanno, Giorgio	(FRIDA) Formal Verification of Internet of Things Protocols (HCVS) Declarative Parameterized Verification of Topology-sensitive Distributed Protocols
Demangeon, Romain	(LICS) Causal Computational Complexity of Distributed Processes
Demirović, Emir	(POS) Local-Style Search in the Linear MaxSAT Algorithm: A Computational Study of Solution-Based Phase Saving
Demri, Stéphane	(ADSL) A Complete Proof System for Basic Symbolic Heaps with Permissions
Denecker, Marc	(LPOP) Opening and introduction (LPOP) The RBAC challenge in the Knowledge Base Paradigm
Denecker, Marc	(LPOP) Closing
Deng, Yiping	(Isabelle) Hilbert Meets Isabelle: Formalisation of the DPRM Theorem in Isabelle
Dennis, Louise	(ReMOTE) Moral Permissibility of Actions in Smart Home Systems (VaVAS) Formalisation of the Rules of the Road for embedding into an Autonomous Vehicle Agent
Dershowitz, Nachum	(DCM) Generic Graph Semantics (TERMGRAPH) Drags: an algebraic framework for graph rewriting (WST) GPO: A Path Ordering for Graphs (IJCAR) Well-Founded Unions
Deshmukh, Jyotirmoy	(SYNT) Synthesizing safe AI-based controllers for cyber-physical systems
Despeyroux, Joëlle	(LSB) A logical framework for systems biology and biomedicine
Devadas, Srini	(CSF) Sanctum: Towards an Open-Source, Formally Verified Secure Processor
Devambu, Prem	(MLP) Why is Software Natural? and how can Naturalness be exploited?
Devkota, Prabhat	(Isabelle) Hilbert Meets Isabelle: Formalisation of the DPRM Theorem in Isabelle
Devriese, Dominique	(LICS) Degrees of Relatedness - A Unified Framework for Parametricity, Irrelevance, Ad Hoc Polymorphism, Intersections, Unions and Algebra in Dependent Type Theory (HoTT/UF) Internalizing Presheaf Semantics: Charting the Design Space
Dhingra, Bhuwan	(MLP) Answering Cloze-style Software Questions Using Stack Overflow
Di Benedetto, Maria Domenica	(ADHS) On Approximate Predictability of Metric Systems
Di Pierro, Alessandra	(DCM) Towards a Formal System for Topological Quantum Computation
Di Pompeo, Silvia	(RCRA) Optimal Fault-Tolerant Placement of Relay Nodes in a Mission Critical Wireless Network
Di Stasio, Antonio	(SR) Solving Parity Games: Explicit vs Symbolic
Dietsch, Daniel	(VSTTE) The Map Equality Domain
Diez, Stefan	(VEMDP) Formal Verification of Network-Based Biocomputation Circuits
Diller, Martin	(QBF) Initial study on the effect of different QBF solvers and preprocessors on link-information sensitive QBF encodings for Abstract Dialectical Frameworks
Dillig, Isil	(CAV) Learning Abstractions for Program Synthesis
Ding, Yuhao	(ADHS) Input Design for Nonlinear Model Discrimination Via Affine Abstraction
Divasón, Jose	(WST) A Perron-Frobenius Theorem for Jordan Blocks for Complexity Proving (ITP) A Formalization of the LLL Basis Reduction Algorithm
Dixon, Clare	(AVOCS) Formal Verification of Synchronisation, Gossip and Environmental Effects for Wireless Sensor Networks (PAAR) Evaluating Pre-Processing Techniques for the Separated Normal Form for Temporal Logics
Djemai, Mohamed	(ADHS) Razumikhin-type Theorems on Practical Stability of Dynamic Equations on Time Scales
Djemai, Mohamed	(ADHS) Stability of switched systems on non-uniform time domains with non commuting matrices
Djouadi, Seddik	(ADHS) Stability of switched systems on non-uniform time domains with non commuting matrices
Dobre, Ana Maria	(VEMDP) Computational Approaches for the Programmed Assembly of Nanocellulose Meshes
Doczkal, Christian	(ITP) A Formal Proof of the Minor-Exclusion Property for Treewidth-Two Graphs
Dodaro, Carmine	(RCRA) Externally Supported Models for Efficient Computation of Paracoherent Answer Sets (ICLP) Cautious Reasoning in ASP via Minimal models and Unsatisfiable Cores (ICLP) Shared aggregate sets in answer set programming
Dodds, Josiah	(CAV) Continuous formal verification of Amazon s2n
Dohrau, Jérôme	(CAV) Permission Inference for Array Programs (PLR) Permission Inference for Array Programs
Doménech, Jesús	(WST) Control-Flow Refinement via Partial Evaluation
Doré, Maximilian	(ThEdu) Towards intuitive reasoning in axiomatic geometry
Dougherty, Daniel	(FCS) Homomorphisms and Minimality for Enrich-by-Need Security Analysis
Doumane, Amina	(Linearity/TLLA) Infinitary Proof Theory: the Multiplicative Additive Case
Dovier, Agostino	(PLR) MASP-Reduce: a proposal for distributed computation of stable models (ICLP) MASP-Reduce: a proposal for distributed computation of stable models
Doyle, Jon	(FCS) An Expressive, Flexible and Uniform Logical Formalism for Attribute-based Access Control
Dragan, Constantin Cătălin	(CSF) Machine-checked proofs for electronic voting: privacy and verifiability for Belenios
Dragoste, Irina	(IJCAR) Efficient Model Construction for Horn Logic with VLog: System Description
Dreier, Jannik	(CSF) Automated Unbounded Verification of Stateful Cryptographic Protocols with Exclusive OR
Dreossi, Tommaso	(rv4rise) Systematic analysis and improvement of CNNs.
Dressler, Mareike	(PC) Optimization over the Boolean Hypercube via Sums of Nonnegative Circuit Polynomials
Dries, Anton	(ICLP) Improving Candidate Quality of Probabilistic Logic Models
Dross, Claire	(AVOCS) Climbing the Software Assurance Ladder - Practical Formal Verification for Reliable Software
Duan, Yihai	(FM) Falsification of Cyber-Physical Systems Using Deep Reinforcement Learning
Dubischar, Simon	(Isabelle) Hilbert Meets Isabelle: Formalisation of the DPRM Theorem in Isabelle
Dubois, Catherine	(Tetrapod) Modularity in Proof Checking
Dubslaff, Clemens	(LICS) Stochastic Shortest Paths and Weight-Bounded Properties in Markov Decision Processes
Duck, Gregory	(ICLP) Shape Neutral Analysis of Graph-based Data-structures
Duggirala, Parasara Sridhar	(ADHS) On Generating A Variety of Unsafe Counterexamples for Linear Dynamical Systems
Dullerud, Geir E.	(ADHS) Statistical Verification of PCTL Using Stratified Samples
Dumas, Marlon	(GraMSec) Disclosure Analysis of SQL Workflows
Dumbrava, Stefania	(ICLP) Certified Graph View Maintenance with Regular Datalog
Dunn, Sara-Jane	(VEMDP) Uncovering the Biological Programs that Govern Development
Dupont, Benjamin	(IWC) Coherence modulo relations (HDRA) Termination in linear (2,2)-categories with braidings and duals
Dupressoir, François	(CSF) Machine-checked proofs for electronic voting: privacy and verifiability for Belenios (CSF) Formal Security Proof of CMAC and its Variants
Durand, Arnaud	(LICS) Model-Theoretic Characterizations of Boolean and Arithmetic Circuit Classes of Small Depth
Durand, Irène	(LaSh) Monadic Second-Order Model Checking with Fly-Automata
Dureja, Rohit	(CAV) SimpleCAR: An Efficient Bug-Finding Tool Based On Approximate Reachability
Durier, Adrien	(LICS) Eager Functions as Processes
Dutle, Aaron	(FM) From Formal Requirements to Highly Assured Software for Unmanned Aircraft Systems (FM) A Formally Verified Floating-Point Implementation of the Compact Position Reporting Algorithm
Dutra, Inês	(ICLP) Improving Candidate Quality of Probabilistic Logic Models
Dvijotham, Krishnamurthy	(SMT) Invited talk: Verifying Learners and Learning Verifiers
E
Eades Iii, Harley	(GraMSec) On Linear Logic, Functional Programming, and Attack Trees (Linearity/TLLA) On the Lambek Calculus with an Exchange Modality
Eberhart, Clovis	(LICS) What's in a game? A theory of game models
Eberl, Manuel	(ITP) Verified Analysis of Random Binary Tree Structures
Ebner, Gabriel	(PAAR) Efficient translation of sequent calculus proofs into natural deduction proofs (CL&C) Fast cut-elimination using proof terms: an empirical study
Echenim, Mnacho	(IJCAR) A Generic Framework for Implicate Generation Modulo Theories (ADSL) The Complexity of Prenex Separation Logic with One Selector
Edalat, Abbas	(Domains13) A logical view of complex analytic maps
Eeralla, Ajay Kumar	(UNIF) Bounded ACh Unification
Egerstedt, Magnus	(ADHS) Tracking Control via Variable-gain Integrator and Lookahead Simulation: Application to Leader-follower Multiagent Networks
Eggers, Andreas	(SCSC) EA: Constraint Systems from Traffic Scenarios for the Validation of Autonomous Driving
Egly, Uwe	(IJCAR) QRAT+: Generalizing QRAT by a More Powerful QBF Redundancy Property
Egly, Uwe	(QBF) Initial study on the effect of different QBF solvers and preprocessors on link-information sensitive QBF encodings for Abstract Dialectical Frameworks
Ehlers, Rüdiger	(SAT) Approximately Propagation Complete and Conflict Propagating Constraint Encodings
Ehlers, Thorsten	(PLR) Tuning Parallel SAT Solvers (POS) Tuning Parallel SAT Solvers
Ehrig, Rainald	(RCRA) Computing Personalised Treatments through In Silico Clinical Trials. A Case Study on Downregulation in Assisted Reproduction.
Eilers, Marco	(CAV) MaxSMT-Based Type Inference for Python 3 (CAV) Nagini: A Static Verifier for Python
Eiter, Thomas	(ASPOCP) Towards Abstraction in ASP with an Application on Reasoning about Agent Policies (ICLP) Answer Set Programs go 30: Past and Future (ICLP) Exploiting Answer Set Programming with External Sources for Meta-Interpretive Learning
El Ouraoui, Daniel	(SMT) Higher-Order SMT Solving
Elffers, Jan	(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
Elkind, Edith	(SR) Strategic behavior in social choice - Part 1 (SR) Strategic behavior in social choice - Part 2
Emmi, Michael	(CAV) Monitoring Weak Consistency (AVOCS) Automatic Verification of Concurrent Objects (FRIDA) Specifying Non-Atomic Methods of Concurrent Objects (VSTTE) SideTrail: Verifying Time-Balancing of Cryptosystems
Endrullis, Joerg	(FSCD) Decreasing diagrams with two labels are complete for confluence of countable systems
Ene, Nneka	(TERMGRAPH) A Port-graph Model for Finance
Enea, Constantin	(CAV) Reasoning About TSO Programs Using Reduction and Abstraction (CAV) Monitoring Weak Consistency (CAV) On the Completeness of Verifying Message Passing Programs under Bounded Asynchrony (FRIDA) Specifying and Verifying Concurrent Objects
England, Matthew	(SCSC) RP: Towards Incremental Cylindrical Algebraic Decomposition in Maple (SCSC) RP: Non-linear Real Arithmetic Benchmarks derived from Automated Reasoning in Economics
Ensan, Alireza	(PRUV) A Model-Theoretic View on Preferences in Declarative Specifications of Search Problems
Erban, Radek	(VEMDP) Noise control for molecular computing
Erbatur, Serdar	(UNIF) Knowledge Problems in Equational Extensions of Subterm Convergent Theories
Erbsen, Andres	(ITP) Reification by Parametricity
Erdélyi, Balázs	(SMT) Puli - A Problem-Specific OMT Solver
Erola, Arnau	(GraMSec) A state machine system for insider threat detection
Escardó, Martín	(HoTT/UF) Injective types and searchable types in univalent mathematics
Esparza, Javier	(CAV) Peregrine: A Tool for the Analysis of Population Protocols (LICS) One Theorem to Rule Them All: A Unified Translation of LTL into ω-Automata (LICS) Verification of population protocols
Etessami, Kousha	(LearnAut) Algorithms for Weighted and Probabilistic Context-Free Grammars and Convex Optimization
Eugster, Patrick Thomas	(CSF) A Cryptographic Look at Multi-Party Channels
Evans, Richard	(FoPSS) Inductive logic programming and deep learning I (FoPSS) Inductive logic programming and deep learning II
Even-Mendoza, Karine	(VSTTE) Lattice-Based Refinement in Bounded Model Checking
F
Faber, Wolfgang	(RCRA) Externally Supported Models for Efficient Computation of Paracoherent Answer Sets
Faggian, Claudia	(GS) The Geometry of Parallelism: Probabilistic and Quantum Effects
Fahrenberg, Uli	(FM) Optimal and Robust Controller Synthesis Using Energy Timed Automata with Uncertainty
Fainekos, Georgios	(ADHS) Falsification of Temporal Logic Requirements Using Gradient Based Local Search in Space and Time
Fainekos, Georgios	(ADHS) Mission Planning for Multiple Vehicles with Temporal Specifications using UxAS
Faisal, Aldo	(ReMOTE) The computational neuroscience of human-robot relationships
Falappa, Marcelo A.	(PRUV) Leveraging Probabilistic Existential Rules for Adversarial Deduplication
Fan, Chuchu	(CAV) Controller Synthesis Made Real: Reach-avoid Specifications and Linear Dynamics (FM) Approximate Partial Order Reduction
Fanchon, Eric	(ADHS) Occupation Measure Methods for Modelling and Analysis of Biological Hybrid Systems
Fandinno, Jorge	(ICLP) Functional ASP with Intensional Sets; Application to Gelfond-Zhang Agreggates
Farinas Del Cerro, Luis	(ICLP) Functional ASP with Intensional Sets; Application to Gelfond-Zhang Agreggates
Farinier, Benjamin	(CAV) Model Generation for Quantified Formulas: A Taint-Based Approach
Farka, Frantisek	(ICLP-DC) Proof-relevant resolution for elaboration of programming languages (ICLP) Proof-relevant Horn Clauses for Dependent Type Inference and Term Synthesis
Farkas, Rebeka	(AVOCS) Backward reachability analysis for timed automata with data variables
Farmer, William	(ITP) HOL Light QE
Fava, Daniel	(FM) Operational Semantics of a Weak Memory Model with Channel Synchronization
Fazekas, Katalin	(IJCAR) Implicit Hitting Set Algorithms for Maximum Satisfiability Modulo Theories
Fedyukovich, Grigory	(CAV) Syntax-Guided Termination Analysis (CAV) Exploiting Synchrony and Symmetry in Relational Verification
Felgenhauer, Bertram	(IWC) Towards a Verified Decision Procedure for Confluence of Ground Term Rewrite Systems in Isabelle/HOL
Feliu Gabaldon, Marco Antonio	(ITP) Boosting the Reuse of Formal Specifications
Feller, David	(LFMTP) What Does This Notation Mean Anyway? BNF-style notation as it is actually used
Feng, Lu	(ReMOTE) Safety and Trust in Autonomous Driving
Feng, Yijun	(CAV) Monitoring CTMCs By Multi-Clock Timed Automata
Ferdinand, Christian	(FM) Software Safety and Security and AI
Feret, Jerome	(VEMDP) Conservative approximations of polymers
Fernandez, Maribel	(FSCD) Fixed-Point Constraints for Nominal Equational Unification (LMW) Rewriting and Applications
Ferrando, Angelo	(HCVS) Declarative Parameterized Verification of Topology-sensitive Distributed Protocols
Ferrari, Alberto	(NSV) Challenges on the Application of Formal Methods for Validation and Verification in Aerospace Systems Engineering
Ferrari, Mauro	(EICNCL) A Forward Calculus for Countermodel Construction in IPL
Ferreira, Joao F.	(ITP) Towards Verified Handwritten Calculational Proofs (Short Paper)
Ferrère, Thomas	(rv4rise) First order temporal properties of continuous signals (FM) The Compound Interest in Relaxing Punctuality (LICS) A Theory of Register Monitors
Fiacchini, Mirko	(ADHS) Language constrained stabilization of discrete- time switched linear systems: an LMI approach
Fichte, Johannes	(LaSh) Solving #SAT by Parameterized Algorithms: Exploiting Small Treewidth (SAT) Exploiting Treewidth for Projected Model Counting and its Limits
Fiedor, Tomas	(LaSh) Lazy Automata Techniques for WS1S
Figueira, Diego	(LICS) Playing with Repetitions in Data Words Using Energy Games
Fijalkow, Nathanaël	(LICS) The State Complexity of Alternating Automata (SR) Quantifying Bounds in Strategy Logic
Filiot, Emmanuel	(LICS) Logics for Word Transductions with Synthesis (LICS) Rational Synthesis Under Imperfect Information
Filippidis, Ioannis	(TLA) Proving properties of a minimal covering algorithm
Filliatre, Jean-Christophe	(F-IDE) Auto-active verification using Why3's IDE (ITP) Deductive Program Verification
Finger, Marcelo	(IJCAR) Probably Half True: Probabilistic Satisfiability over Lukasiewicz Infinitely-valued Logic (PRUV) Quantitative Logic Reasoning -- Combining logical reasoning with probabilities and counting (invited talk)
Finkbeiner, Bernd	(CAV) Synthesizing Reactive Systems from Hyperproperties (CAV) Model Checking Quantitative Hyperproperties (SYNT) On the Expressiveness of HyperLTL Synthesis (CSF) The Complexity of Monitoring Hyperproperties
Finzi, Alberto	(RCRA) Optimal Fault-Tolerant Placement of Relay Nodes in a Mission Critical Wireless Network
Fioravanti, Fabio	(ICLP) Solving Horn Clauses on Inductive Data Types Without Induction
Fioravanti, Fabio	(HCVS) Metaprogramming and symbolic execution for detecting runtime errors in Erlang programs
Fiore, Marcelo	(LOLA) Algebraic Theories and Control Effects, Back and Forth
Fiorentini, Camillo	(EICNCL) A Forward Calculus for Countermodel Construction in IPL
Fiorentino, Alessio	(LPOP) Role-Based Access Control via JASP
Firsov, Denis	(ITP) Efficient Mendler-Style Lambda-Encodings in Cedille
Fischlin, Marc	(CSF) Backdoored Hash Functions: Immunizing HMAC and HKDF (CSF) Self-Guarding Cryptographic Protocols against Algorithm Substitution Attacks
Fisher, Michael	(AVOCS) Formal Verification of Synchronisation, Gossip and Environmental Effects for Wireless Sensor Networks (ReMOTE) Moral Permissibility of Actions in Smart Home Systems (VaVAS) Formalisation of the Rules of the Road for embedding into an Autonomous Vehicle Agent
Fisk, Mike	(GraMSec) Intrusion Tolerance in Complex Cyber Systems
Fisman, Dana	(SYNT) Competition Report: SyGuS-COMP
Fitzgerald, John	(Overture) Design Space Exploration for Secure Building Control
Flamm, Christoph	(VEMDP) Rule-Based Gillespie Simulation of Chemical Systems
Fleury, Mathias	(Isabelle) A Verified SAT Solver with Watched Literals Using Imperative HOL (Extended Abstract)
Florido, Mário	(ITRS) Gradual Intersection Types
Flum, Jörg	(LICS) Tree depth, quantifier elimination, and quantifier rank
Foliard, Guillaume	(AVOCS) Climbing the Software Assurance Ladder - Practical Formal Verification for Reliable Software
Fontaine, Pascal	(SCSC) EA: Wrapping Computer Algebra is Surprisingly Successful for Non-Linear SMT (SMT) Revisiting Enumerative Instantiation (SMT) Higher-Order SMT Solving
Foo, Yi Shyh Eddy	(ADHS) Multi-Energy Scheduling Using a Hybrid Systems Approach
Forest, Simon	(IWC) Critical pairs for Gray categories (FSCD) Coherence of Gray categories via rewriting
Forets, Marcelo	(ADHS) Occupation Measure Methods for Modelling and Analysis of Biological Hybrid Systems
Forrest, Stephen A.	(SCSC) EA: SMT-like Queries in Maple
Forster, Yannick	(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
Foster, Simon	(VaVAS) RoboTool: Modelling and Verification with RoboChart
Fouque, Pierre-Alain	(CSF) Formal Security Proof of CMAC and its Variants
Fourman, Michael	(Domains13) A Brouwerian proof of the Fan Theorem
Francalanza, Adrian	(DCM) Pointing to Private Names
Fraser, Simon	(Overture) Integrating VDM-SL into the continuous delivery pipelines of cloud-based software
Fredrikson, Matt	(CSF) Privacy Risk in Machine Learning: Analyzing the Connection to Overfitting
Frehse, Goran	(CAV) Spacetime Interpolants
Freitas, Leo	(Overture) VDM at large: analysing the EMV Next Generation Kernel
Fremont, Daniel J.	(CAV) Reactive Control Improvisation
Frerix, Steffen	(UITP) Text-Orientated Formal Mathematics
Frey, Jonas	(LICS) Impredicative Encodings of (Higher) Inductive Types
Fribourg, Laurent	(ADHS) Control Synthesis for Stochastic Switched Systems Using the Tamed Euler Method
Fried, Dror	(LICS) Sequential Relational Decomposition
Friedman, Daniel	(UNIF) Efficiency of a good but not linear nominal unification algorithm
Friedrich, Tobias	(SAT) Sharpness of the Satisfiability Threshold for Non-Uniform Random k-SAT
Frisch, Alan	(LaSh) ESSENCE, A Language for Specifying Combinatorial Problems: What, Why and So What?
Frittella, Sabine	(ITP) Software Tool Support for Modular Reasoning in Modal Logics of Actions
Frohn, Florian	(WST) Complexity Analysis for Bitvector Programs
From, Andreas Halkjær	(ThEdu) Students' Proof Assistant (SPA) (ThEdu) Natural Deduction Assistant (NaDeA) (Isabelle) Substitutionless First-Order Logic: A Formal Soundness Proof (PAAR) A Verified Simple Prover for First-Order Logic (UITP) Drawing Trees
Fruehwirth, Thom	(LPOP) Security Policies in Constraint Handling Rules (LPOP) A Rule-Based Tool for Analysis and Generation of Graphs Applied to Mason's Marks (ICLP) CHRvis: Syntax and Semantics
Frumin, Dan	(LICS) ReLoC: A Mechanised Relational Logic for Fine-Grained Concurrency
Fuhs, Carsten	(WST) Improving Static Dependency Pairs for Higher-Order Rewriting
Fujii, Soichiro	(Domains13) Higher-dimensional categories: recursion on extensivity
Fukui, Kousuke	(IWC) Complete Axiom System of Cluster Algebra
Furber, Robert	(LICS) Boolean-Valued Semantics for Stochastic Lambda-Calculus
Férée, Hugo	(VSTTE) Program Verification in the Presence of I/O: Semantics, verified library routines, and verified applications
G
Gaboardi, Marco	(LMW) Research as a collaborative effort
Gacek, Andrew	(CAV) The JKind Model Checker
Gadducci, Fabio	(LICS) Rewriting with Frobenius
Galal, Zeinab	(Linearity/TLLA) Towards a Functional Language for Species of Structures
Galdino, André Luiz	(ITP) Formalizing Ring Theory in PVS (Short Paper)
Galesi, Nicola	(PC) Space Proof Complexity beyond Resolution (PC) Resolution and the binary encoding of combinatorial principles (SAT) Cops-Robber games and the resolution of Tseitin formulas
Gall, Daniel	(LPOP) Confluence Analysis of Cognitive Models with Constraint Handling Rules
Gallagher, John P.	(WST) Control-Flow Refinement via Partial Evaluation (ICLP) An iterative approach to precondition inference using constrained Horn clauses
Gallego Arias, Emilio Jesús	(ICLP) Certified Graph View Maintenance with Regular Datalog
Galmiche, Didier	(ARQNL) Labelled Connection-based Proof Search for Multiplicative Intuitionistic Linear Logic (ADSL) Labelled Cyclic Proofs for Separation Logic (EICNCL) Proof Translations in BI logic
Gamble, Carl	(Overture) Multi-modelling of Cooperative Swarms
Gamble, Carl	(Overture) Design Space Exploration for Secure Building Control
Ganesh, Vijay	(CAV) The Proof Complexity of SMT Solvers (CAV) StringFuzz: A Fuzzer for String Solvers (SAT) Machine Learning-based Restart Policy for CDCL SAT Solvers
Gange, Graeme	(ICLP) An iterative approach to precondition inference using constrained Horn clauses
Ganty, Pierre	(LICS) Sound up-to techniques and Complete abstract domains (HCVS) Tree dimension in verification of constrained Horn clauses
Gao, Pengfei	(CAV) SCInfer: Refinement-based Verification of Software Countermeasures against Side-Channel Attacks
Gao, Sicun	(CAV) Delta-Decision Procedures for Exists-Forall Problems over the Reals
Gao, Tiantian	(ICLP-DC) Knowledge Authoring and Question Answering via Controlled Natural Language
Garbuzov, Dmitri	(ITP) A Formal Equational Theory for Call-by-Push-Value
Garcia, Sergio	(FM) Multi-Robot LTL Planning Under Uncertainty
Garcia-Contreras, Isabel	(ICLP) Towards Incremental and Modular Context-sensitive Analysis
García-Bañuelos, Luciano	(GraMSec) Disclosure Analysis of SQL Workflows
Gardy, Patrick	(SR) Dependences in Strategy Logic
Garg, Deepak	(CSF) Types for Information Flow Control: Labeling Granularity and Semantic Models
Garlan, David	(FM) IPL: An Integration Property Language for Multi-Model Cyber-Physical Systems
Garoche, Pierre-Loïc	(NSV) Automatic Generation and Formal Verification of an Interior Point Algorithm
Gascón, Adrià	(UNIF) Compressed Term Unification: Results, uses, open problems, and hopes
Gastin, Paul	(LICS) Regular Transducer Expressions for Regular Transformations over infinite words
Gavanelli, Marco	(RCRA) Logic Programming approaches for routing fault-free and maximally-parallel Wavelength Routed Optical Networks on Chip (Application paper)
Gavazzo, Francesco	(LICS) Quantitative Behavioural Reasoning for Higher-order Effectful Programs: Applicative Distances
Gay, Simon	(WiL) A New Linear Logic for Deadlock-Free Session-Typed Processes (Talk Abstract)
Gburek, Daniel	(LICS) Stochastic Shortest Paths and Weight-Bounded Properties in Markov Decision Processes
Ge, Cunjing	(IJCAR) Investigating the Existence of Large Sets of Idempotent Quasigroups via Satisfiability Testing (IJCAR) A New Probabilistic Algorithm for Approximate Model Counting (PRUV) VolCE: An Efficient Tool for Solving #SMT(LA) Problems (PRUV) A New Probabilistic Algorithm for Approximate Model Counting
Gebser, Martin	(ICLP) Routing Driverless Transport Vehicles in Car Assembly with Answer Set Programming (ICLP) Experimenting with robotic intra-logistics domains
Geeraerts, Gilles	(MoRe) Safe and Optimal Scheduling of Hard and Soft Tasks
Genaim, Samir	(WST) Inference of Linear Upper-Bounds on the Expected Cost by Solving Cost Relations (WST) Control-Flow Refinement via Partial Evaluation
Gencer, Çigdem	(UNIF) About the unification type of topological logics over Euclidean spaces (WiL) About the unification type of topological logics over Euclidean spaces
Genest, Blaise	(LICS) Distribution-based objectives for Markov Decision Processes
Genestier, Guillaume	(WST) Termination of Lambda-Pi modulo rewriting using the size-change principle
Genet, Thomas	(FSCD) Completeness of Tree Automata Completion
Gentilini, Raffaella	(LICS) Rational Synthesis Under Imperfect Information
Geoffroy, Guillaume	(LICS) Classical realizability as a classifier for nondeterminism
Gericke, Moritz	(AVOCS) Writing a Model Checker in 80 Days: Reusable Libraries and Custom Implementation
Geser, Alfons	(WST) Comparing on Strings: Semantic Kachinuki Order
Ghani, Neil	(LICS) Compositional game theory (SR) Compositional Game Theory
Ghardallou, Wided	(REFINE) Programming Without Refinement
Ghasemi, Mahsa	(SYNT) Maximum Realizability for Linear Temporal Logic Specifications
Ghassabani, Elaheh	(CAV) The JKind Model Checker
Ghedira, Khaled	(PRUV) Evidential Group Decision Making Model with Belief-Based Preferences
Ghica, Dan	(GS) How to denotational an operational semantics (LICS) The Geometry of Computation-Graph Abstraction (LOLA) A graph-rewriting perspective of the beta-law
Ghilardi, Silvio	(UNIF) Handling substitutions via duality
Ghorbal, Khalil	(FM) Vector Barrier Certificates and Comparison Systems
Ghosh, Shromona	(ADHS) Generating Dominant Strategies for Continuous Two-Player Zero-Sum Games
Giacobazzi, Roberto	(CAV) Program Analysis is Harder than Verification: A Computability Perspective (LICS) Sound up-to techniques and Complete abstract domains
Giacobbe, Mirco	(CAV) Spacetime Interpolants
Giacomelli, Irene	(CSF) Privacy Risk in Machine Learning: Analyzing the Connection to Overfitting
Giannini, Paola	(DCM) A syntactic model of mutation and aliasing
Giaquinta, Ruben	(VaVAS) Probabilistic Model Checking for Autonomous Agent Strategy Synthesis - Extended Abstract
Gibbons, Jeremy	(MSFP) Profunctor Optics and the Yoneda Lemma
Giegerich, Robert	(LaSh) Declarative Dynamic Programming with Inverse Coupled Rewrite Systems
Gierasimczuk, Nina	(FoPSS) Learning and epistemic modal logic I (FoPSS) Learning and epistemic modal logic II
Giese, Martin	(IJCAR) Industrial Data Access – What are the Reasoning Problems? And is Reasoning the Problem?
Giesl, Jürgen	(WST) Complexity Analysis for Bitvector Programs
Giordano, Laura	(PRUV) Reasoning about exceptions in ontologies: from the lexicographic closure to the skeptical closure
Girard, Antoine	(ADHS) Safety Control, a Quantitative Approach
Girard, Antoine	(ADHS) Compositional Abstraction-based Synthesis for Cascade Discrete-Time Control Systems
Girard, Antoine	(ADHS) Language constrained stabilization of discrete- time switched linear systems: an LMI approach
Girard, Antoine	(ADHS) Symbolic Models for Incrementally Stable Switched Systems with Aperiodic Time Sampling
Giraudo, Samuele	(HDRA) Generalizations of the associative operad and convergent rewrite systems
Girlando, Marianna	(EICNCL) Hypersequent calculus for the logic of conditional belief: preliminary results
Giráldez-Cru, Jesus	(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
Giunti, Marco	(DCM) Pointing to Private Names
Gleiss, Bernhard	(Vampire) Foundations of SPECTRE (SAT) Local Soundness for QBF Calculi
Gliozzi, Valentina	(PRUV) Reasoning about exceptions in ontologies: from the lexicographic closure to the skeptical closure
Gocht, Stephan	(POS) Seeking Practical CDCL Insights from Theoretical SAT Benchmarks (SAT) In Between Resolution and Cutting Planes: A Study of Proof Systems for Pseudo-Boolean SAT Solving
Goel, Shubham	(CAV) What’s hard about Boolean Functional Synthesis?
Goeminne, Aline	(MoRe) Constraint Problem for Weak Subgame Perfect Equilibria with omega-regular Boolean Objectives
Goertzel, Zarathustra	(ITP) ProofWatch: Watchlist Guidance for Large Theories in E
Goldman, Drew	(SYNT) Programming by example: efficient, but not “helpful”
Goldsmith, Michael	(GraMSec) A state machine system for insider threat detection
Goldwasser, Shafi	(FLoC) Pseudo deterministic algorithms and proofs
Gomez-Zamalloa, Miguel	(CAV) Constrained Dynamic Partial Order Reduction (FM) SDN-Actors: Modeling and Verification of SDN Programs
Gonthier, Georges	(FLoC) The Logic of Real Proofs (Tetrapod) Modularity in Large Proofs
Gonzalez-Dios, Itziar	(Vampire) Towards Word Sense Disambiguation by Reasoning
Gooi, H. B.	(ADHS) Multi-Energy Scheduling Using a Hybrid Systems Approach
Gore, Rajeev	(IJCAR) Well-Founded Unions
Gorzny, Jan	(UITP) Partial Regularization of First-Order Resolution Proofs
Goubault, Eric	(CAV) Inner and Outer Approximating Flowpipes for Delay Differential Equations
Gouveia, Filipe	(ICLP-DC) Model Revision of Logical Regulatory Networks using Logic-based Tools
Grabmayer, Clemens	(TERMGRAPH) Modeling terms by graphs with structure constraints (two illustrations)
Graham-Lengrand, Stéphane	(SMT) Proofs in conflict-driven theory combination (SMT) Centralizing Equality Reasoning in MCSAT
Grayson, Daniel R.	(ITP) Voevodsky's Work on Formalization of Proofs and the Foundations of Mathematics
Grebing, Sarah	(UITP) Adding Text-Based Interaction to a Direct-Manipulation Interface for Program Verification -- Lessons Learned
Greco, Giuseppe	(ITP) Software Tool Support for Modular Reasoning in Modal Logics of Actions
Greiner, Johannes	(IJCAR) Complexity of Combinations of Qualitative Constraint Satisfaction Problems
Grellois, Charles	(EICNCL) Toward intuitionistic non-normal modal logic and its calculi
Griffin, Timothy G.	(ITP) An Agda Formalization of Üresin & Dubois' Asynchronous Fixed-Point Theory
Griggio, Alberto	(SAT) Experimenting on Solving Nonlinear Integer Arithmetic with Incremental Linearization
Grigore, Radu	(QBF) PrideMM: QBFEVAL Benchmarks (QBFEval18 Contribution)
Grimaud, Gilles	(AVOCS) Proof-Oriented Design of a Separation Kernel with Minimal Trusted Computing Base
Grohe, Martin	(LICS) Definable decompositions for graphs of bounded linear cliquewidth
Gross, Jason	(Coq) Teaching Your Rooster to Crow in C (ITP) Reification by Parametricity
Grosu, Radu	(VaVAS) Work-in-Progress: Adaptive Neighborhood Resizing for Stochastic Reachability in Distributed Flocking
Grumberg, Orna	(VDMW) Model checking and its applications
Grädel, Erich	(LICS) LICS Awards: The Kleene Award and the Test of Time Award
Grégoire, Benjamin	(CSF) Secure compilation of side-channel countermeasures: the case of cryptographic “constant-time” (CSF) Formal Security Proof of CMAC and its Variants
Gu, Ronghui	(CAV) Partial Order Aware Concurrency Sampling
Guarneri, Riccardo	(RCRA) Optimal Fault-Tolerant Placement of Relay Nodes in a Mission Critical Wireless Network
Guatto, Adrien	(LICS) A Generalized Modality for Recursion
Gueguen, Herve	(ADHS) Hierarchical Model Predictive Control for Building Energy Management of Hybrid Systems
Guerrieri, Giulio	(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
Guglielmi, Alessio	(TYDI) Two Unifying Structural Principles
Guha, Shibashis	(MoRe) Safe and Optimal Scheduling of Hard and Soft Tasks (FM) Timed Vacuity
Guiochet, Jérémie	(VaVAS) Trust me I am autonomous
Guldstrand Larsen, Kim	(MoRe) Comfort and Energy Optimization for Floor Heating Systems (CAV) Start Pruning When Time Gets Urgent: Partial Order Reduction for Timed Systems (FM) 20 Years of "Real" Real-Time Model Checking (FM) Optimal and Robust Controller Synthesis Using Energy Timed Automata with Uncertainty
Gulwani, Sumit	(SoMLMFM) Programming from examples: PL meets ML
Gupta, Aarti	(CAV) Syntax-Guided Termination Analysis (CAV) Exploiting Synchrony and Symmetry in Relational Verification (CAV) Lazy Self-Composition for Security Verification
Gupta, Gopal	(ICLP) Constraint Answer Set Programming without Grounding (ICLP) Cumulative Scoring-based Induction of Default Theories
Gupta, Piyush	(WST) Verification of Rewriting-based Query Optimizers
Gupta, Shubhani	(SAT) Effective use of SMT solvers for Program Equivalence Checking through Invariant Sketching and Query Decomposition
Gurfinkel, Arie	(SMT) Discovering Universally Quantified Solutions for Constrained Horn Clauses (VSTTE) Executable Counterexamples in Software Model Checking (HCVS) Report on the CHC competition
Guth, Dwight	(CSF) KEVM: A Complete Formal Semantics of the Ethereum Virtual Machine
Gutierrez, Julian	(SR) Local Equilibria in Logic-Based Multi-Player Games
Guttman, Joshua	(FCS) Homomorphisms and Minimality for Enrich-by-Need Security Analysis
Guéneau, Armaël	(Coq) Procrastination, A proof engineering technique
Gyorgy, Andras	(FM) A Weakness Measure for GR(1) Formulae
Gérard, Ulysse	(LFMTP) Functional programming with λ-tree syntax: a progress report (LFMTP) Computation-as-deduction in Abella: work in progress
Gómez-Gutiérrez, David	(ADHS) Observability of Linear Hybrid Systems with Unknown Inputs and Discrete Dynamics Modeled by Petri Nets
Głuch, Grzegorz	(LICS) Can One Escape Red Chains? Regular Path Queries Determinacy is Undecidable.
H
Haagh, Helene	(CSF) Computer-aided proofs for multiparty computation with active security
Haak, Anselm	(LICS) Model-Theoretic Characterizations of Boolean and Arithmetic Circuit Classes of Small Depth
Hadzihasanovic, Amar	(FSCD) A diagrammatic axiomatisation of fermionic quantum circuits (LICS) Two complete axiomatisations of pure-state qubit quantum computing (HDRA) Merge-bicategories: towards semi-strictification of higher categories
Haehn, Rebecca	(SCSC) RP: Evaluation of Equational Constraints for CAD in SMT Solving
Hage, Nohra	(IWC) Coherence of monoids by insertions (HDRA) String data structures for Chinese monoids
Hahn, Christopher	(CAV) Synthesizing Reactive Systems from Hyperproperties (CAV) Model Checking Quantitative Hyperproperties (SYNT) On the Expressiveness of HyperLTL Synthesis
Hahn, Michael	(LICS) Wreath Products of Distributive Forest Algebras
Hai Tran, Thanh	(TLA) BMCMT – Bounded Model Checking of TLA+ Specifications with SMT
Hajdu, Ákos	(AVOCS) Backward reachability analysis for timed automata with data variables
Hajnal, Matej	(VEMDP) Executable Biochemical Space for Specification and Analysis of Biochemical Systems
Hall, Brendan	(F-IDE) The CLEAR Way To Transparent Formal Methods
Hamana, Makoto	(FSCD) Confluence Competition 2018
Hammond, Kevin	(ICLP) Proof-relevant Horn Clauses for Dependent Type Inference and Term Synthesis
Hammoudeh, Zayd	(SAT) Fast Sampling of Perfectly Uniform Satisfying Assignments (SAT) Fast and Flexible Probabilistic Model Counting
Hamza, Jad	(SYNT) Minimal Synthesis of String To String Functions From Examples
Hannula, Miika	(IJCAR) Automated Reasoning about Key Sets
Hao, Jianye	(FM) Falsification of Cyber-Physical Systems Using Deep Reinforcement Learning
Hardy, Jörg	(ReMOTE) Understanding Ethical Reasoning
Harper, Robert	(LICS) Guarded Computational Type Theory (HoTT/UF) Cubical Computational Type Theory (ITP) Verified Tail Bounds for Randomized Programs
Harrenstein, Paul	(SR) Local Equilibria in Logic-Based Multi-Player Games
Harris, William	(HCVS) Solving Constrained Horn Clauses Using Dependence-Disjoint Expansions
Harrison, John	(ITP) Mike Gordon: Tribute to a Pioneer in Theorem Proving and Formal Verification
Hartmanns, Arnd	(MoRe) Multiple Objectives and Cost Bounds in MDP
Hasanbeig, Mohammadhosein	(MoRe) Logically-Constrained Reinforcement Learning
Hasegawa, Masahito	(Linearity/TLLA) From Linear Logic to Cyclic Sharing
Haslbeck, Max W.	(Isabelle) Formal Verification of Bounds for the LLL Basis Reduction Algorithm (ITP) Verified Analysis of Random Binary Tree Structures
Haslbeck, Maximilian P. L.	(IJCAR) Verifying Asymptotic Time Complexity of Imperative Programs in Isabelle
Hassan, Mostafa	(CAV) MaxSMT-Based Type Inference for Python 3
Hassler, Malte Sophian	(Isabelle) Hilbert Meets Isabelle: Formalisation of the DPRM Theorem in Isabelle
Hasuo, Ichiro	(GS) Coalgebras and Higher-Order Computation: a GoI Approach (COALG) Martingale-Based Methods for Reachability Probabilities: Excitements and Afterthoughts about Coalgebras
Hasuo, Ichiro	(ADHS) Bounding Errors Due to Switching Delays in Incrementally Stable Switched Systems
Hautem, Quentin	(MoRe) Parameterized complexity of games with monotonically ordered omega-regular objectives
Hawes, Nick	(VaVAS) Policy Generation with Probabilistic Guarantees for Long-term Autonomy of a Mobile Service Robot
Hawes, Nick	(VaVAS) Robot Demonstration
Haxthausen, Signe Geisler And Anne E.	(FM) Stepwise Development and Model Checking of a Distributed Interlocking System - using RAISE
Hayes, Ian J.	(FM) Encoding fairness in a synchronous concurrent program algebra (REFINE) Challenges of specifying concurrent program components
He, Jinlong	(CAV) Android Stack Systems
He, Yilun	(Isabelle) PaMpeR: A Proof Method Recommendation System for Isabelle/HOL
Heath, David	(HCVS) Solving Constrained Horn Clauses Using Dependence-Disjoint Expansions
Hecher, Markus	(SAT) Exploiting Treewidth for Projected Model Counting and its Limits
Hedges, Jules	(LICS) Compositional game theory (MSFP) Backward induction for repeated games (SR) Compositional Game Theory
Heemels, Maurice	(ADHS) A switched system approach to optimize mixing of fluids
Hehner, Eric	(WST) Objective and Subjective Specifications (REFINE) a Theory of Lazy Imperative Timing
Heijltjes, Willem	(FSCD) Proof nets for bi-intuitionistic linear logic (TYDI) Deep-Inference Intersection Types (TYDI) An introduction to deep inference
Heiter, Edith	(ITP) Verification of PCP-Related Computational Reductions in Coq
Heizmann, Matthias	(VSTTE) The Map Equality Domain
Helfer, Joseph	(HoTT/UF) First-order homotopical logic and Grothendieck fibrations
Helie, Jean	(MLP) Measuring software development productivity: a machine learning approach
Hencey, Brandon	(ADHS) Compositional Analysis of Hybrid Systems Defined Over Finite Alphabets
Hensel, Jera	(WST) Complexity Analysis for Bitvector Programs
Henzinger, Monika	(CAV) Symbolic Algorithms for Graphs and Markov Decision Processes with Fairness Objectives
Henzinger, Thomas	(CAV) Spacetime Interpolants (CAV) Reachable Set Over-approximation for Nonlinear Systems Using Piecewise Barrier Tubes (LICS) A Theory of Register Monitors (SR) Infinite-Duration Richman Bidding Games
Heo, Kihong	(MLP) Difflog: Beyond Deductive Methods in Program Analysis
Herbelin, Hugo	(HoTT/UF) The definitional symmetric cubical structure of types in type theory with equality defined by abstraction over an interval
Herbelot, Aurelie	(NLCS) Speakers in vats: simulating model-theoretic alignment with distributional semantics
Hermenegildo, Manuel V.	(LCC) A General Equational Framework for Static Profiling of Parametric Resource Usage (ICLP) Towards Static Performance Guarantees for Programs with Run-time Checks (ICLP) Towards Incremental and Modular Context-sensitive Analysis
Herrera, Christian	(WPTE) Verification of Ada Programs with AdaHorn
Hess, Andreas Viktor	(CSF) A Typing Result for Stateful Protocols
Heule, Marijn	(VEMDP) Computing properties of stable configurations of thermodynamic binding networks (IJCAR) Extended Resolution Simulates DRAT (POS) The Effect of Scrambling CNFs (SAT) Computable Short Proofs (SAT) SAT Competition 2018
Hiet, Guillaume	(FM) Modular Verification of Programs with Effects and Effect Handlers in Coq
Hildenbrandt, Everett	(CSF) KEVM: A Complete Formal Semantics of the Ethereum Virtual Machine
Hinde, Luke	(QBF) Size, Cost and Capacity: A Semantic Technique for Hard Random QBFs
Hirokawa, Nao	(IWC) IWC Business Meeting (FSCD) Confluence Competition 2018 (IJCAR) Cops and CoCoWeb: Infrastructure for Confluence Tools
Hirschi, Lucca	(CSF) Automated Unbounded Verification of Stateful Cryptographic Protocols with Exclusive OR
Hirschkoff, Daniel	(LICS) Eager Functions as Processes
Hirschowitz, Tom	(GS) What's in a game? (LICS) What's in a game? A theory of game models
Ho, Son	(IJCAR) Proof-Producing Synthesis of CakeML with I/O and Local State from Monadic HOL Functions
Ho, Son	(VSTTE) Program Verification in the Presence of I/O: Semantics, verified library routines, and verified applications
Ho Thanh, Cédric	(HDRA) The equivalence between opetopic sets and many-to-one polygraphs
Hoang, Thai Son	(VaVAS) Policing Functions for Machine Learning Systems
Hoenicke, Jochen	(IJCAR) Efficient Interpolation for the Theory of Arrays (VSTTE) The Map Equality Domain (VSTTE) A Tree-Based Approach to Data Flow Proofs
Hofbauer, Dieter	(WST) Embracing Infinity - Termination of String Rewriting by Almost Linear Weight Functions (WST) Comparing on Strings: Semantic Kachinuki Order
Hoffmann, Jan	(LICS) Work Analysis with Resource-Aware Session Types
Hoffmann, Ruth	(VaVAS) Probabilistic Model Checking for Autonomous Agent Strategy Synthesis - Extended Abstract
Holik, Lukas	(LaSh) Lazy Automata Techniques for WS1S
Holmes, Chris	(SoMLMFM) Panel session
Hooker, John	(LPOP) Invited Talk: A Modeling Language Based on Semantic Typing
Hoos, Holger	(QBF) Portfolio-Based Algorithm Selection for Circuit QBFs
Hoos, Holger	(SAT) Sparkle SAT Challenge 2018
Horacek, Jan	(SCSC) RP: Refutation of Products of Linear Polynomials
Horne, Ross	(TYDI) Truely Concurrent Processes in the Calculus of Structures (GraMSec) The Attacker Does not Always Hold the Initiative: Attack Trees with External Refinement (LICS) Quasi-Open Bisimilarity with Mismatch is Intuitionistic
Hou Favonia, Kuen-Bang	(LFMTP) Invited talk: Cubical Computational Type Theory and RedPRL (LICS) Cellular Cohomology in Homotopy Type Theory (HoTT/UF) Cubical Computational Type Theory
Houshmand, Arian	(ADHS) Hybrid System Modeling of Multi-Agent Coverage Problems with Energy Depletion and Repletion
Hoxha, Bardh	(ADHS) Mission Planning for Multiple Vehicles with Temporal Specifications using UxAS
Hrushovski, Ehud	(LICS) Polynomial Invariants for Affine Programs
Hsu, Justin	(CAV) Constraint-Based Synthesis of Coupling Proofs
Hu, Hai	(NLCS) Automated Reasoning from Polarized Parse Trees
Hu, Qinheping	(CAV) Syntax Guided Synthesis with Quantitative Syntactic Objectives
Hu, Shuwei	(ITP) Verified Memoization and Dynamic Programming
Huang, Chung-Hao	(VSTTE) Verification of Binarized Neural Networks via Inter-Neuron Factoring
Huang, Kai	(FM) Resource-aware Design for Reliable Autonomous Applications with Multiple Periods
Huang, Pei	(IJCAR) Investigating the Existence of Large Sets of Idempotent Quasigroups via Satisfiability Testing
Huang, Zhenqi	(FM) Approximate Partial Order Reduction
Huber, Simon	(LICS) On Higher Inductive Types in Cubical Type Theory
Huffman, Brian	(CAV) Continuous formal verification of Amazon s2n
Hughes, Dominic	(TYDI) Some incoherent musings on deep inference and combinatorial proofs (LICS) Unification nets: canonical proof net quantifiers
Humbel, Lukas	(ITP) Physical Addressing on Real Hardware in Isabelle/HOL
Husson, Adrien	(LSB) Introducing iota, a logic for biological modelling
Hustadt, Ullrich	(PAAR) Evaluating Pre-Processing Techniques for the Separated Normal Form for Temporal Logics
Hym, Samuel	(AVOCS) Proof-Oriented Design of a Separation Kernel with Minimal Trusted Computing Base
Hyvernat, Pierre	(PARIS) The size-change principle and circular proofs: checking totality of (co)recursive definitions
Hyvärinen, Antti	(VSTTE) Lattice-Based Refinement in Bounded Model Checking
Höfner, Peter	(ITP) Backwards and Forwards with Separation Logic
Hölzl, Johannes	(ITP) MDP + TA = PTA: Probabilistic Timed Automata, Formalized (Short Paper)
I
Icard, Thomas	(NLCS) Automated Reasoning from Polarized Parse Trees
Iden, Joachim	(ReMOTE) Elements of a Model of Trust in Technology
Idziak, Pawel	(LICS) Satisfiability in multi-valued circuits
Ignatiev, Alexey	(PC) On Dual-Rail Based MaxSAT Solving (IJCAR) A SAT-Based Approach to Learn Explainable Decision Sets (SAT) PySAT: A Python Toolkit for Prototyping with SAT Oracles
Igne, Federico	(PLR) MASP-Reduce: a proposal for distributed computation of stable models (ICLP) MASP-Reduce: a proposal for distributed computation of stable models
Iguernlala, Mohamed	(SMT) Alt-Ergo 2.2
Ikebuchi, Mirai	(FSCD) On repetitive right application of B-terms (Coq) ComplCoq: Rewrite Hint Construction with Completion Procedures
Inclezan, Daniela	(ICLP) An ASP Methodology for Understanding Narratives about Stereotypical Activities
Inoue, Katsumi	(ASPOCP) Partial Evaluation of Logic Programs in Vector Spaces (ICLP) Exploiting Answer Set Programming with External Sources for Meta-Interpretive Learning (ICLP) Learning Commonsense Knowledge through Interactive Dialogue
Interlandi, Matteo	(ICLP) Declarative Algorithms in Datalog with Aggregates: user-friendly formal semantics conducive to performance and scalability
Iosif, Radu	(AVOCS) An Entailment Checker for Separation Logic with Inductive Definitions (ADSL) The Complexity of Prenex Separation Logic with One Selector
Iraci, Grant	(FM) IPL: An Integration Property Language for Multi-Model Cyber-Physical Systems
Ireland, Murray	(VaVAS) Probabilistic Model Checking for Autonomous Agent Strategy Synthesis - Extended Abstract
Irfan, Ahmed	(SAT) Experimenting on Solving Nonlinear Integer Arithmetic with Incremental Linearization
Isabel, Miguel	(CAV) Constrained Dynamic Partial Order Reduction
Iser, Markus	(POS) A Problem Meta-Data Library for Research in SAT
Israney, Ankush	(ICLP) An ASP Methodology for Understanding Narratives about Stereotypical Activities
Itcus, Corina	(VEMDP) Computational Approaches for the Programmed Assembly of Nanocellulose Meshes
Ivrii, Alexander	(SAT) Finding all Minimal Safe Inductive Sets
J
Jaax, Stefan	(CAV) Peregrine: A Tool for the Analysis of Population Protocols (FRIDA) Peregrine - A Tool for Population Protocols
Jacob-Rao, Rohan	(FSCD) Index-Stratified Types
Jacobs, Bart	(COALG) Coalgebras and Kleisli Maps for Probability
Jacobs, Ceriel	(IJCAR) Efficient Model Construction for Horn Logic with VLog: System Description
Jacobs, Swen	(SYNT) Competition Report: SYNTCOMP
Jacomme, Charlie	(CSF) An extensive formal analysis of multi-factor authentication protocols
Jaffar, Joxan	(ICLP) Shape Neutral Analysis of Graph-based Data-structures
Jagadeesan, Radha	(GS) "Operational'' Game Semantics
Jagtap, Pushpak	(ADHS) Compositional Abstraction-based Synthesis for Cascade Discrete-Time Control Systems
Jain, Achin	(ADHS) Data-Driven Switched Affine Modeling for Model Predictive Control
Jakubuv, Jan	(ITP) ProofWatch: Watchlist Guidance for Large Theories in E
Jamali, Sima	(SAT) Centrality-Based Improvements to CDCL Heuristics
Janku, Petr	(LaSh) Lazy Automata Techniques for WS1S
Janota, Mikolas	(QBF) RAReQS, QFUN, QESTO (QBFEval'18 Contribution) (SAT) Circuit-based Search Space Pruning in QBF
Janota, Mikolas	(QBF) PrideMM: QBFEVAL Benchmarks (QBFEval18 Contribution)
Jansen, Christina	(CAV) Let this Graph be your Witness! An Attestor for Verifying Java Pointer Programs
Janson, Christian	(CSF) Backdoored Hash Functions: Immunizing HMAC and HKDF
Janssens, Gerda	(QBF) A Grounder From Second-Order Logic To QBF
Jantsch, Simon	(ITP) Verifying the LTL to Büchi Automata Translation via Very Weak Alternating Automata
Jaskelioff, Mauro	(LICS) Syntax and Semantics for Operations with Scopes
Jay, Barry	(Domains13) Domain Theory for Intensional Computation
Jeandel, Emmanuel	(LICS) Diagrammatic Reasoning beyond Clifford+T Quantum Mechanics (LICS) A Complete Axiomatisation of the ZX-Calculus for Clifford+T Quantum Mechanics
Jeannerod, Nicolas	(IJCAR) Deciding the First-Order Theory of an Algebra of Feature Trees with Updates
Jebelean, Tudor	(SCSC) EA: Techniques for Natural-style Proofs in Elementary Analysis
Jecker, Ismaël	(SR) Beyond admissibility: Dominance between chains of strategies
Jensen, Peter Gjøl	(CAV) Start Pruning When Time Gets Urgent: Partial Order Reduction for Timed Systems
Jeppu, Yogananda	(F-IDE) The CLEAR Way To Transparent Formal Methods
Jha, Somesh	(CAV) Semantic Adversarial Deep Learning (CSF) Privacy Risk in Machine Learning: Analyzing the Connection to Overfitting
Jha, Susmit	(ADHS) Learning and Verification of Feedback Control Systems Using Feedforward Neural Networks
Ji, Kailiang	(CAV) On the Completeness of Verifying Message Passing Programs under Bounded Asynchrony
Jia, Limin	(CSF) Knowledge-based Security of Dynamic Secrets for Reactive Programs
Jia, Yifan	(FM) Towards `Verifying' a Water Treatment System
Jiang, Jiaming	(GraMSec) On Linear Logic, Functional Programming, and Attack Trees (Linearity/TLLA) On the Lambek Calculus with an Exchange Modality (FCS) An Expressive, Flexible and Uniform Logical Formalism for Attribute-based Access Control
Johann, Patricia	(LICS) A General Framework for Relational Parametricity
Johnson, Andrew	(POS) Stedman and Erin Triples encoded as a SAT Problem
Johnson, Robert F.	(VEMDP) Using Transitivity and Modularity in Chemical Reaction Network Bisimulation
Johnson, Taylor T	(ADHS) Reachability Analysis for One Dimensional Linear Parabolic Equation
Johnson, Taylor T	(ADHS) Mission Planning for Multiple Vehicles with Temporal Specifications using UxAS
Jomaa, Narjes	(AVOCS) Proof-Oriented Design of a Separation Kernel with Minimal Trusted Computing Base (VSTTE) Formalising Executable Specifications of Low-Level Systems
Joosten, Sebastiaan	(WST) A Perron-Frobenius Theorem for Jordan Blocks for Complexity Proving (ITP) A Formalization of the LLL Basis Reduction Algorithm
Jost, Steffen	(LCC) Static Prediction of Heap Space Usage for First-Order Functional Programs -- A Retrospective on my First Paper with Martin Hofmann
Jouannaud, Jean-Pierre	(TERMGRAPH) Drags: an algebraic framework for graph rewriting (WST) GPO: A Path Ordering for Graphs (WPTE) A framework for graph rewriting.
Jouanny, Théo	(AVOCS) Climbing the Software Assurance Ladder - Practical Formal Verification for Reliable Software
Jovanović, Dejan	(SMT) Selfless Interpolation for Infinite-State Model Checking (IJCAR) A Separation Logic with Data: Small Models and Automation (ADSL) Sloth: Separation Logic and Theories via Small Models
Jung, Achim	(Domains13) Extending Stone Duality to Relations
Jungers, Raphaël M.	(ADHS) Computing Controlled Invariant Sets for Hybrid Systems with Applications to Model-Predictive Control
Jungers, Raphaël M.	(ADHS) On invariance and reachability on semialgebraic sets for linear dynamics
Junges, Sebastian	(MoRe) Multiple Objectives and Cost Bounds in MDP
Jurdzinski, Marcin	(LICS) A pseudo-quasi-polynomial algorithm for solving mean-payoff parity games (SR) Parity Games - Part 1 (SR) Parity Games - Part 2
Järvisalo, Matti	(POS) Questions and Answers (SAT) SAT Competition 2018 (SAT) MaxSAT Evaluation 2018 (ICLP) Cautious Reasoning in ASP via Minimal models and Unsatisfiable Cores
K
Kabanets, Valentine	(PC) Complexity of expander-based reasoning and the power of monotone proofs
Kabir, Ifaz	(CAV) StringFuzz: A Fuzzer for String Solvers
Kaestner, Daniel	(FM) Software Safety and Security and AI
Kafle, Bishoksan	(ICLP) An iterative approach to precondition inference using constrained Horn clauses
Kahl, Patrick	(ASPOCP) A Survey of Advances in Epistemic Logic Program Solvers (ICLP) Epistemic Logic Programs with World View Constraints
Kahl, Wolfram	(TERMGRAPH) Semantics-Preserving DPO-Based Term Graph Rewriting (ITP) CalcCheck: a Proof Checker for Teaching the “Logical Approach to Discrete Math”
Kahsai, Temesghen	(VSTTE) Executable Counterexamples in Software Model Checking
Kaliszyk, Cezary	(ITP) Towards Formal Foundations for Game Theory (Short Paper)
Kalouli, Aikaterini-Lida	(NLCS) Graph Knowledge Representations for SICK
Kamali, Mojgan	(DS-FM) A Formal Study of MANET Routing Protocols
Kamareddine, Fairouz	(LFMTP) What Does This Notation Mean Anyway? BNF-style notation as it is actually used
Kamburjan, Eduard	(AVOCS) Detecting Deadlocks in Formal System Models with Condition Synchronization
Kaminski, Roland	(ICLP) Temporal Answer Set Programming on Finite Traces
Kaminski, Tobias	(ICLP) Exploiting Answer Set Programming with External Sources for Meta-Interpretive Learning
Kammar, Ohad	(Domains13) Diffeological Spaces and Semantics for Differential Programming (Domains13) Algebra semantics of recursive computation types (Domains13) Invited Talk: A domain theory for quasi-Borel spaces and statistical probabilistic programming
Kanade, Varun	(FoPSS) Statistical learning theory I (FoPSS) Statistical learning theory II
Kanazawa, Makoto	(LearnAut) Decision problems for Clark-congruential languages
Kanazawa, Yoshiaki	(IWC) Convergence of Simultaneously and Sequentially Unraveled TRSs for Normal Conditional TRSs (WPTE) On Transforming Functions Accessing Global Variables into Logically Constrained Term Rewriting Systems
Kanovich, Max	(IJCAR) A Logical Framework with Commutative and Non-Commutative Subexponentials (ADSL) On the Complexity of Pointer Arithmetic in Separation Logic (FCS) Statistical Model Checking of Guessing and Timing Attacks on Distance-bounding Protocols
Kapinski, Jim	(rv4rise) Formalizing Requirements for Cyber-Physical Systems: Real-World Experiences and Challenges
Kaposi, Ambrus	(FSCD) A Syntax for Higher Inductive-Inductive Types
Kappé, Tobias	(LearnAut) Decision problems for Clark-congruential languages
Kapron, Bruce	(LICS) Type-two polynomial-time and restricted lookahead.
Karbyshev, Aleksandr	(CSF) Computer-aided proofs for multiparty computation with active security
Karpiński, Michał	(POS) Competitive Sorter-based Encoding of PB-Constraints into SAT
Katelaan, Jens	(IJCAR) A Separation Logic with Data: Small Models and Automation (ADSL) Sloth: Separation Logic and Theories via Small Models
Katoen, Joost-Pieter	(MoRe) Multiple Objectives and Cost Bounds in MDP (CAV) Sound Value Iteration (CAV) Let this Graph be your Witness! An Attestor for Verifying Java Pointer Programs (CAV) Monitoring CTMCs By Multi-Clock Timed Automata (FM) Formal Verification of Automotive Simulink Controller Models: Empirical Technical Challenges, Evaluation and Recommendations (FM) Verifying Auto-Generated C Code from Simulink
Katz, Guy	(FoPSS) Verification of machine learning programs I (FoPSS) Verification of machine learning programs II
Kauers, Manuel	(SCSC) RP: A Practical Polynomial Calculus for Arithmetic Circuit Verification (SAT) Symmetries for QBF
Kauers, Manuel	(QBF) The Symmetry Rule for Quantified Boolean Formulas
Kawai, Tatsuji	(Domains13) Applications of entailments: de Groot duality
Kawano, Tomoaki	(EICNCL) Sequent Calculi for Logic that Includes an Infinite Number of Modalities
Kazakov, Yevgeny	(IJCAR) Enumerating Justifications using Resolution
Keller, Chantal	(ITP) A Coq Formalisation of SQL’S Execution Engines
Kellison, Ariel	(WiL) On Expanding Standard Notions of Constructivity
Kelmendi, Edon	(CAV) Value Iteration for Simple Stochastic Games: Stopping Criterion and Learning Algorithm
Keramitas, Romain	(MLP) Splitting source code identifiers using Bidirectional LSTM Recurrent Neural Network
Kerjean, Marie	(LICS) A Logical Account for Linear Partial Differential Equations (Linearity/TLLA) Models of Linear Logic based on the Schwartz epsilon product
Kesner, Delia	(DCM) Quantitative types: from Foundations to Applications (LFMTP) Invited talk: A fresh view of call-by-need
Kesseli, Pascal	(CAV) Synthesis Modulo Theories (CAV) JBMC: A Bounded Model Checking Tool for Verifying Java Bytecode
Kesseli, Pascal	(SYNT) Safe, Automated and Formal Synthesis of Digital Controllers for Continuous Plants
Ketab Ghale, Milad	(VSTTE) Verified Certificate Checking for Counting Votes
Khakzad, Nima	(GraMSec) Combining Bayesian Networks and Fishbone Diagrams to Distinguish between Intentional Attacks and Accidental Technical Failures
Khan, Sharjeel	(Linearity/TLLA) Formalization of Automated Trading Systems in a Concurrent Linear Framework
Khanna, Dhriti	(DS-FM) Analysis and Verification of Message Passing based Parallel Programs (FM) Dynamic Symbolic Verification of MPI Programs
Khazem, Kareem	(CAV) Model Checking Boot Code from AWS Data Centers
Khouzani, Mhr	(CSF) Symbolic Side-Channel Analysis for Probabilistic Programs
Kiefer, Moritz	(VSTTE) Relational Equivalence Proofs Between Imperative and MapReduce Algorithms
Kieronski, Emanuel	(LICS) Unary negation fragment with equivalence relations has the finite model property
Kiesl, Benjamin	(IJCAR) Extended Resolution Simulates DRAT
Kimura, Daisuke	(ADSL) Cyclic Theorem Prover for Separation Logic by Magic Wand
Kirchner, Helene	(IFIP WG 1.6) Informal Report on FSCD
Kirkeby, Maja Hanne	(IWC) Confluence in Constraint Handling Rules: An overview from early, fundamental results to recent extensions including state invariants and conf. modulo equivalence.
Kissinger, Aleks	(LICS) Rewriting with Frobenius
Kjellerstrand, Håkan	(LPOP) A Picat-based XCSP Solver - from Parsing, Modeling, to SAT Encoding (RCRA) Encoding PB Constraints into SAT via Binary Adders and BDDs -- Revisited
Klein, Gerwin	(ITP) Backwards and Forwards with Separation Logic (ITP) Program Verification in the Presence of Cached Address Translation
Klemen, Maximiliano	(LCC) A General Equational Framework for Static Profiling of Parametric Resource Usage (ICLP) Towards Static Performance Guarantees for Programs with Run-time Checks
Klop, Jan Willem	(FSCD) Decreasing diagrams with two labels are complete for confluence of countable systems
Kneis, Joachim	(LaSh) Courcelle’s Theorem – A Game-Theoretic Approach
Knop, Alexander	(PC) Branching Program Complexity of Canonical Search Problems and Proof Complexity of Formulas
Knüppel, Alexander	(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
Kobayashi, Naoki	(HOR) On Two Kinds of Higher-Order Model Checking and Higher-Order Program Verification
Kochemazov, Stepan	(SAT) ALIAS: A Modular Tool for Finding Backdoors for SAT
Koepke, Peter	(UITP) Text-Orientated Formal Mathematics
Kohl, Christina	(FSCD) ProTeM: A Proof Term Manipulator
Kohlhase, Michael	(IJCAR) Theories as Types
Kohli, Pushmeet	(SoMLMFM) Towards Robust and Explainable Artificial Intelligence (MLP) Program synthesis and its connections to AGI
Kokke, Wen	(Linearity/TLLA) Taking Linear Logic Apart
Kolechkina, Alla G.	(ADHS) A controlled sewer system should be treated as a sampled data system with events
Kolokolova, Antonina	(CAV) The Proof Complexity of SMT Solvers (PC) Complexity of expander-based reasoning and the power of monotone proofs
Komauli, Francesco	(LFMTP) Property-Based Testing of Abstract Machines: an Experience Report
Komendantskaya, Ekaterina	(PARIS) Coinductive Uniform Proofs: An Extended Abstract (speaker: Yue LI) (COALG) Coalgebra and Automated Reasoning (HCVS) Towards Coinductive Theory Exploration in Horn Clause Logic: Extended Abstract (ICLP) Proof-relevant Horn Clauses for Dependent Type Inference and Term Synthesis
Kong, Hui	(CAV) Reachable Set Over-approximation for Nonlinear Systems Using Piecewise Barrier Tubes
Kong, Soonho	(CAV) Delta-Decision Procedures for Exists-Forall Problems over the Reals
Konnov, Igor	(TLA) BMCMT – Bounded Model Checking of TLA+ Specifications with SMT
Kop, Cynthia	(WST) Improving Static Dependency Pairs for Higher-Order Rewriting (HOR) Wanda: a higher-order termination tool
Kordy, Barbara	(GraMSec) Opening remarks and introductions (GraMSec) Closing remarks and discussions (CSF) Guided design of attack trees: a system-based approach
Korneev, Svyatoslav	(SAT) Constrained Image Generation Using Binarized Neural Networks with Decision Procedures
Korovin, Konstantin	(IJCAR) An abstraction-refinement framework for reasoning with large theories (PRUV) An abstraction-refinement framework for automated reasoning -- a pragmatic approach (invited talk)
Korten, Till	(VEMDP) Formal Verification of Network-Based Biocomputation Circuits
Koskinen, Eric	(LICS) A Fixpoint Logic and Dependent Effects for Temporal Property Verification
Kotelnikov, Evgenii	(PAAR) TFX: The TPTP Extended Typed First-order Form (IJCAR) A FOOLish Encoding of the Next State Relations of Imperative Programs
Kotsireas, Ilias	(SCSC) Hard Combinatorial Problems: A Challenge for Satisfiability
Koucky, Michal	(PC) Complexity of expander-based reasoning and the power of monotone proofs
Kovacs, Laura	(Vampire) Foundations of SPECTRE (IJCAR) A FOOLish Encoding of the Next State Relations of Imperative Programs
Kovács, András	(FSCD) A Syntax for Higher Inductive-Inductive Types
Kovásznai, Gergely	(SMT) Puli - A Problem-Specific OMT Solver
Kozen, Dexter	(LICS) Boolean-Valued Semantics for Stochastic Lambda-Calculus (COALG) Coalgebraic Tools for Randomness-Conserving Protocols
Kragl, Bernhard	(CAV) Proving a concurrent program correct by demonstrating it does nothing (CAV) Proving a concurrent program correct by demonstrating it does nothing (continued)
Kraus, Nicolai	(LICS) Free Higher Groups in Homotopy Type Theory
Krebbers, Robbert	(LICS) ReLoC: A Mechanised Relational Logic for Fine-Grained Concurrency
Krebs, Andreas	(LICS) Wreath Products of Distributive Forest Algebras
Kremer, Gereon	(SCSC) RP: Evaluation of Equational Constraints for CAD in SMT Solving
Kremer, Steve	(CAV) The DEEPSEC prover (CSF) An extensive formal analysis of multi-factor authentication protocols
Kretinsky, Jan	(CAV) Rabinizer 4: From LTL to Your Favourite Deterministic Automaton (CAV) Value Iteration for Simple Stochastic Games: Stopping Criterion and Learning Algorithm (FoPSS) Learning in Verification I (FoPSS) Learning in Verification II (LICS) Conditional Value-at-Risk for Reachability and Mean Payoff in Markov Decision Processes (LICS) One Theorem to Rule Them All: A Unified Translation of LTL into ω-Automata
Kreuzer, Martin	(SCSC) RP: Refutation of Products of Linear Polynomials
Krings, Sebastian	(AVOCS) Writing a Model Checker in 80 Days: Reusable Libraries and Custom Implementation
Krishna, Siddharth	(ADSL) Automating the Flow Framework
Krishnamurthi, Shriram	(FM) CompoSAT: Specification-Guided Coverage for Model Finding
Krishnamurthy, Balaji	(WST) Verification of Rewriting-based Query Optimizers
Krishnawami, Neel	(LMW) Can Logic Make Us Better People?
Kroening, Daniel	(MoRe) Logically-Constrained Reinforcement Learning (CAV) Synthesis Modulo Theories (CAV) JBMC: A Bounded Model Checking Tool for Verifying Java Bytecode (CAV) Model Checking Boot Code from AWS Data Centers (SYNT) Safe, Automated and Formal Synthesis of Digital Controllers for Continuous Plants (WST) Procedure-Modular Termination Analysis
Krzaczkowski, Jacek	(LICS) Satisfiability in multi-valued circuits
Krämer, Julia	(CAV) Value Iteration for Simple Stochastic Games: Stopping Criterion and Learning Algorithm
Krötzsch, Markus	(IJCAR) Efficient Model Construction for Horn Logic with VLog: System Description
Kucera, Antonin	(LICS) Efficient Algorithms for Asymptotic Bounds on Termination Time in VASS
Kugler, Hillel	(VEMDP) Formal Verification of Network-Based Biocomputation Circuits
Kukovec, Jure	(FRIDA) Parameterized Reachability for All Flavors of Threshold Automata
Kukovec, Jure	(TLA) BMCMT – Bounded Model Checking of TLA+ Specifications with SMT
Kulal, Sumith	(CAV) What’s hard about Boolean Functional Synthesis? (SYNT) Scalable Synthesis with Symbolic Syntax Graphs
Kulkarni, Sulekha	(MLP) Difflog: Beyond Deductive Methods in Program Analysis
Kullmann, Oliver	(SAT) Minimal unsatisfiability and minimal strongly connected digraphs
Kumar, Ramana	(IJCAR) Proof-Producing Synthesis of CakeML with I/O and Local State from Monadic HOL Functions (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) Verified Certificate Checking for Counting Votes
Kunčak, Viktor	(SYNT) Minimal Synthesis of String To String Functions From Examples (MLP) Opening and demos
Kupferman, Orna	(FM) Timed Vacuity
Kuppe, Markus	(TLA) State Space Explosion or: How To Fight An Uphill Battle
Kurpisz, Adam	(PC) Optimization over the Boolean Hypercube via Sums of Nonnegative Circuit Polynomials
Kurz, Alexander	(Domains13) Extending Stone Duality to Relations (ITP) Software Tool Support for Modular Reasoning in Modal Logics of Actions
Kutsia, Temur	(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
Kutz, Yunus David Kerem	(UNIF) Rewriting with Generalized Nominal Unification
Kuusisto, Antti	(LICS) Weighted model counting beyond two-variable logic
Kuznetsov, Stepan	(IJCAR) A Logical Framework with Commutative and Non-Commutative Subexponentials
Kwiatkowska, Marta	(SoMLMFM) Safety verification for deep neural networks with provable guarantees (VEMDP) Molecular Filters for Noise Reduction
König, Barbara	(LICS) A van Benthem Theorem for Fuzzy Modal Logic
L
Labed Jilani, Lamia	(REFINE) Programming Without Refinement
Lacerda, Bruno	(VaVAS) Policy Generation with Probabilistic Guarantees for Long-term Autonomy of a Mobile Service Robot (VaVAS) Robot Demonstration
Lachnitt, Hanna	(WiL) Embedding Intuitionistic Modal Logics in Higher-Order Logic. An Easy Task?
Lagniez, Jean Marie	(IJCAR) An Assumption-Based Approach for Solving The Minimal S5-Satisfiability Problem
Lahijanian, Morteza	(ReMOTE) Welcome and Introduction
Lahmadi, Abdelkader	(AVOCS) Rule-Based Synthesis of Chains of Security Functions for Software-Defined Networks
Laird, James	(GS) Games and the Lambda Cube (LICS) Extensional and Intensional Semantic Universes: A Denotational Model of Dependent Types
Lakin, Matthew	(VEMDP) Rule-based design of computational DNA devices
Laleg-Kirati, Taous-Meriem	(ADHS) Razumikhin-type Theorems on Practical Stability of Dynamic Equations on Time Scales
Lammich, Peter	(Isabelle) Using Isabelle/UTP for the Verification of Sorting Algorithms: A Case Study (Isabelle) A Verified SAT Solver with Watched Literals Using Imperative HOL (Extended Abstract)
Lampis, Michael	(SAT) QBF as an Alternative to Courcelle's Theorem
Lanciotti, Filiberto	(RCRA) Optimal Fault-Tolerant Placement of Relay Nodes in a Mission Critical Wireless Network
Laneve, Cosimo	(FM) A lightweight deadlock analysis technique of object-oriented programs
Lange, Martin	(PARIS) Collapses of Fixpoint Alternation Hierarchies in Low Type-Levels of Higher-Order Fixpoint Logic
Langer, Alexander	(LaSh) Courcelle’s Theorem – A Game-Theoretic Approach
Langworthy, David	(TLA) TLA+ in Engineering Systems: Quinceañera
Laporte, Vincent	(CSF) Secure compilation of side-channel countermeasures: the case of cryptographic “constant-time”
Larchey-Wendling, Dominique	(IJCAR) Constructive Decision via Redundancy-free Proof-Search (ITP) Proof Pearl: Constructive Extraction of Cycle Finding Algorithms (LOLA) Towards a library of formalised undecidable problems in Coq: The undecidability of intuitionistic linear logic
Larsen, John Bruntse	(Isabelle) Substitutionless First-Order Logic: A Formal Soundness Proof
Larsen, Peter Gorm	(Overture) Transforming an industrial case study from VDM++ to VDM-SL (Overture) ViennaVM: a Virtual Machine for VDM-SL development (Overture) Overture FMU: Export VDM-RT Models as Tool-Wrapper FMUs
Lasaulce, Samson	(ADHS) Space-Time Budget Allocation for Marketing Over Social Networks
Laskowski, Patrick	(ITP) HOL Light QE
Laud, Peeter	(GraMSec) Disclosure Analysis of SQL Workflows
Laurent, Jonathan	(LSB) Counterfactual resimulation for causal analysis of rule-based models
Laurent, Olivier	(ITRS) Intersection Subtyping with Constructors (GS) Resource-Tracking Concurrent Games (LICS) Around Classical and Intuitionistic Linear Logics (Coq) Preliminary Report on the Yalla Library
Laurenti, Luca	(VEMDP) Molecular Filters for Noise Reduction
Lauret, Menno	(ADHS) A switched system approach to optimize mixing of fluids
Lausdahl, Kenneth	(Overture) Transforming an industrial case study from VDM++ to VDM-SL (Overture) Overture FMU: Export VDM-RT Models as Tool-Wrapper FMUs (Overture) Enhancing Testing of VDM-SL models
Law, Mark	(ICLP) Learning Commonsense Knowledge through Interactive Dialogue
Lawson, Jimmie	(Domains13) Invited Talk: Topology and Domain Theory Interfaces
Lazic, Ranko	(LICS) A pseudo-quasi-polynomial algorithm for solving mean-payoff parity games
Le Berre, Daniel	(IJCAR) An Assumption-Based Approach for Solving The Minimal S5-Satisfiability Problem (POS) On the use of solvers with docker technology
Le Coent, Adrien	(MoRe) Comfort and Energy Optimization for Floor Heating Systems
Le Roux, Stephane	(SR) Concurrent games and semi-random determinacy
Leblanc, Emily	(ICLP-DC) Explaining Actual Causation via Reasoning about Actions and Change
Leclerc, Anthony	(ASPOCP) A Survey of Advances in Epistemic Logic Program Solvers (ICLP) Epistemic Logic Programs with World View Constraints
Lecomte, Thierry	(FM) Disruptive Innovations for the Development and the Deployment of Fault-Free Software
Lee, Joohyung	(ICLP) A Probabilistic Extension of Action Language BC+ (ICLP) Translating LPOD and CR-Prolog2 into Standard Answer Set Programs
Lee, Woosuk	(MLP) Difflog: Beyond Deductive Methods in Program Analysis
Leeners, Brigitte	(RCRA) Computing Personalised Treatments through In Silico Clinical Trials. A Case Study on Downregulation in Assisted Reproduction.
Legay, Axel	(FM) Statistical Model Checking of LLVM Code (FM) QFLan: A Tool for the Quantitative Analysis of Highly Reconfigurable Systems (LICS) Sequential Relational Decomposition
Lehtinen, Karoliina	(LICS) A modal mu perspective on solving parity games in quasipolynomial time.
Leigh, Graham	(CL&C) Herbrand's Theorem as Higher-Order Recursion
Leino, Rustan	(LPOP) Invited Talk: The Young Software Engineer’s Guide to Using Formal Methods
Lellmann, Bjoern	(TYDI) Sequentialising nested systems (EICNCL) Hypersequent calculus for the logic of conditional belief: preliminary results
Lemay, Jean-Simon	(FSCD) Lifting Coalgebra Modalities and IMELL Model Structure to Eilenberg-Moore Categories
Lengal, Ondrej	(LaSh) Lazy Automata Techniques for WS1S
Lenisa, Marina	(GS) Games, Geometry of Interaction, Reversible Computations, Lambda Calculus
Lennartz, Werner	(POS) CryptoMiniSat Parameter-Optimization for Solving Cryptographic Instances
Leone, Nicola	(LPOP) Role-Based Access Control via JASP (LPOP) Invited Talk: On the Development of Industrial Applications with ASP
Lepigre, Rodolphe	(LFMTP) Abstract Representation of Binders in OCaml using the Bindlib Library
Lescanne, Pierre	(FSCD) Counting Environments and Closures (Linearity/TLLA) How to count linear and affine closed lambda terms? (HOR) Combinatorics of explicit substitutions (extended abstract)
Letan, Thomas	(FM) Modular Verification of Programs with Effects and Effect Handlers in Coq
Lettmann, Michael	(PARIS) Towards the Automatic Construction of Schematic Proofs (IJCAR) A Tableaux Calculus for Reducing Proof Size
Leucker, Martin	(rv4rise) Hardware-based runtime verification with Tessla
Leuschel, Michael	(LPOP) Invited Talk: Practical uses of Logic, Formal Methods, B and ProB
Leventi-Peetz, Anastasia	(POS) CryptoMiniSat Parameter-Optimization for Solving Cryptographic Instances
Leventis, Thomas	(LICS) Probabilistic Böhm Trees and Probabilistic Separation
Levy, Jordi	(FSCD) Term-Graph Anti-Unification
Levy, Paul	(GS) Game semantics: from call-by-push-value and CPS to coalgebra (Domains13) Algebra semantics of recursive computation types (LOLA) Heaps denote finitely partitioned trees
Lhote, Nathan	(LICS) Logics for Word Transductions with Synthesis
Li, Baiyu	(CSF) Symbolic security of garbled circuits
Li, Chunxiao	(SAT) Machine Learning-based Restart Policy for CDCL SAT Solvers
Li, Haokun	(CAV) Monitoring CTMCs By Multi-Clock Timed Automata
Li, Jianwen	(CAV) SimpleCAR: An Efficient Bug-Finding Tool Based On Approximate Reachability
Li, Wei	(VaVAS) RoboTool: Modelling and Verification with RoboChart
Li, Wenchao	(CAV) Safety-Aware Apprenticeship Learning
Li, Yue	(PARIS) Coinductive Uniform Proofs: An Extended Abstract (speaker: Yue LI) (HCVS) Towards Coinductive Theory Exploration in Horn Clause Logic: Extended Abstract
Liang, Jia	(SAT) Machine Learning-based Restart Policy for CDCL SAT Solvers
Libal, Tomer	(ARQNL) An Outline for Simple Semi-automated Proof Assistants for First-order Modal Logics (UITP) Interfacing with a Prover using Focusing and Logic Programming
Licata, Daniel	(FSCD) Call-by-name Gradual Type Theory (FSCD) Internal Universes in Models of Homotopy Type Theory
Lier, Florian	(VaVAS) Reproducibility in Robotics - The Big 5 Issues
Lierler, Yuliya	(ICLP) SMT-based Answer Set Solver CMODELS(DIFF) (System Description)
Lifschitz, Vladimir	(ASPOCP) anthem: Transforming gringo Programs into First-Order Theories (Preliminary Report)
Liiva, Kristjan	(NSV) Compositional Taylor Model Based Validated Integration
Limbrée, Christophe	(AVOCS) A Framework for the Formal Verification of Networks of Railway Interlockings - Application to the Belgian Railways
Lin, Fangzhen	(VSTTE) Extending VIAP to Handle Array Programs
Lin, Shang-Wei	(FM) Compositional Reasoning for Shared-variable Concurrent Programs (LICS) Quasi-Open Bisimilarity with Mismatch is Intuitionistic
Linard, Alexis	(LearnAut) Learning Several Languages from Labeled Strings: State Merging and Evolutionary Approaches
Lindell, Steven	(LCC) Traversal-invariant definability and Logarithmic-space computation
Lindenhovius, Bert	(LICS) Enriching a Linear/Non-linear Lambda Calculus: A Programming Language for String Diagrams
Lindner, Felix	(ReMOTE) Moral Permissibility of Actions in Smart Home Systems
Link, Sebastian	(IJCAR) Automated Reasoning about Key Sets
Liqat, Umer	(LCC) A General Equational Framework for Static Profiling of Parametric Resource Usage
Liquori, Luigi	(IFIP WG 1.6) TBA
Listenmaa, Inari	(NLCS) Automatic test suite generation for PMCFG grammars
Liu, Heng	(PRUV) A Model-Theoretic View on Preferences in Declarative Specifications of Search Problems
Liu, Shuang	(FM) Falsification of Cyber-Physical Systems Using Deep Reinforcement Learning
Liu, Tian	(IJCAR) A New Probabilistic Algorithm for Approximate Model Counting (PRUV) A New Probabilistic Algorithm for Approximate Model Counting
Liu, Yang	(FM) Compositional Reasoning for Shared-variable Concurrent Programs (CSF) A Permission-Dependent Type System for Secure Information Flow Analysis
Liu, Yanhong A.	(LPOP) Easier Rules and Constraints for Programming (LPOP) Introduction: Role-Based Access Control as a Programming Challenge (TLA) Invariants in Distributed Algorithms
Liu, Yufei	(Isabelle) Hilbert Meets Isabelle: Formalisation of the DPRM Theorem in Isabelle
Liu, Zexiang	(SYNT) Warm-Starting Fixed-Point Based Control Synthesis
Lluch Lafuente, Alberto	(FM) QFLan: A Tool for the Quantitative Analysis of Highly Reconfigurable Systems
Lochbihler, Andreas	(Isabelle) Lazy Algebraic Types in Isabelle/HOL (ITP) Relational Parametricity and Quotient Preservation for Modular (Co)Datatypes (ITP) Fast Machine Words in Isabelle/HOL
Loitzenbauer, Veronika	(CAV) Symbolic Algorithms for Graphs and Markov Decision Processes with Fairness Objectives
Lomuscio, Alessio	(SR) Verification of Multi-agent Systems with Imperfect Information and Public Actions
Long, Waren	(MLP) Splitting source code identifiers using Bidirectional LSTM Recurrent Neural Network
Longley, John	(GS) Characterizing observational equivalence for PCF terms within richer languages (Domains13) Robust computability notions for types arising in classical analysis
Lonsing, Florian	(IJCAR) QRAT+: Generalizing QRAT by a More Powerful QBF Redundancy Property (QBF) DepQBF (QBFEval'18 Contribution)
Lonsing, Florian	(QBF) Discussion
Lopez Hernandez, Julio Cesar	(IJCAR) An abstraction-refinement framework for reasoning with large theories
Lopez Pombo, Carlos	(ITP) Boosting the Reuse of Formal Specifications
Lopez-Garcia, Pedro	(LCC) A General Equational Framework for Static Profiling of Parametric Resource Usage (ICLP) Towards Static Performance Guarantees for Programs with Run-time Checks
Lowe, Gavin	(FM) View abstraction for systems with component identities
Lowndes, Alison	(SoMLMFM) The realities of applied AI
Lozes, Etienne	(PARIS) Collapses of Fixpoint Alternation Hierarchies in Low Type-Levels of Higher-Order Fixpoint Logic (ADSL) A Complete Proof System for Basic Symbolic Heaps with Permissions
Lucanu, Dorel	(IJCAR) A Coinductive Approach to Proving Reachability in Logically Constrained Term Rewriting Systems
Lucas, Salvador	(WST) Well-founded models in proofs of termination
Luckow, Kasper	(CSF) Symbolic Side-Channel Analysis for Probabilistic Programs
Lugiez, Denis	(ADSL) A Complete Proof System for Basic Symbolic Heaps with Permissions
Lukert, Philip	(CAV) Synthesizing Reactive Systems from Hyperproperties (SYNT) On the Expressiveness of HyperLTL Synthesis
Lukina, Anna	(VaVAS) Work-in-Progress: Adaptive Neighborhood Resizing for Stochastic Reachability in Distributed Flocking
Luo, Adriel	(ADHS) CoasterX: A Case Study in Component-Driven Hybrid Systems Proof Automation
Luo, Chuan	(SAT) Sparkle SAT Challenge 2018
Luo, Zhaohui	(NLCS) Propositional Forms of Judgemental Interpretations (Linearity/TLLA) Substructural Calculi with Dependent Types
Lustig, Daniel	(PLR) RTLCheck: Automatically Verifying the Memory Consistency of Processor RTL
Luttenberger, Michael	(CAV) Strix: Explicit Reactive Synthesis Strikes Back!
Lutz, Carsten	(LICS) Weighted model counting beyond two-variable logic
Lv, Yiqi	(FM) Resource-aware Design for Reliable Autonomous Applications with Multiple Periods
Lynce, Ines	(ICLP-DC) Model Revision of Logical Regulatory Networks using Logic-based Tools
Lynch, Christopher	(UNIF) Bounded ACh Unification
Lyon, Tim	(EICNCL) Effective Translations between Display and Labelled Proofs for Tense Logics
Légaré, Sébastien	(LSB) Bio-curation and rule-based modelling of protein interaction networks in KAMI
Lühne, Patrick	(ASPOCP) anthem: Transforming gringo Programs into First-Order Theories (Preliminary Report)
M
Ma, Feifei	(IJCAR) Investigating the Existence of Large Sets of Idempotent Quasigroups via Satisfiability Testing (IJCAR) A New Probabilistic Algorithm for Approximate Model Counting (PRUV) VolCE: An Efficient Tool for Solving #SMT(LA) Problems (PRUV) A New Probabilistic Algorithm for Approximate Model Counting
Ma, Hao	(ADHS) Interacting Particle System-Based Estimation of Reach Probability for a Generalized Stochastic Hybrid System
Ma, Weixi	(UNIF) Efficiency of a good but not linear nominal unification algorithm
Ma, Xutong	(IJCAR) A New Probabilistic Algorithm for Approximate Model Counting (PRUV) A New Probabilistic Algorithm for Approximate Model Counting
MacCarthaigh, Colm	(CAV) Continuous formal verification of Amazon s2n (VSTTE) SideTrail: Verifying Time-Balancing of Cryptosystems
Mace, John	(Overture) Design Space Exploration for Secure Building Control
Macedo, Hugo Daniel	(Overture) Transforming an industrial case study from VDM++ to VDM-SL
Macedo, Nuno	(F-IDE) Improving the Visualization of Alloy Instances
Mackie, Ian	(DCM) Models of Computation that Conserve Data
Madelaine, Eric	(AVOCS) Using SMT engine to generate Symbolic Automata
Madelaine, Florent	(LICS) A universal-algebraic proof of the complexity dichotomy for Monotone Monadic SNP
Madiot, Jean-Marie	(LOLA) Denotational Event structure for relaxed memory
Maeda, Yuya	(FSCD) Narrowing Trees for Syntactically Deterministic Conditional Term Rewriting Systems (WPTE) On Transforming Narrowing Trees into Regular Tree Grammars Generating Ranges of Substitutions
Maffei, Matteo	(CAV) Foundations and Techniques for the Static Analysis of Ethereum Smart Contracts
Magill, Stephen	(CAV) Continuous formal verification of Amazon s2n
Magron, Victor	(ADHS) Occupation Measure Methods for Modelling and Analysis of Biological Hybrid Systems
Mahajan, Anmol	(SAT) Effective use of SMT solvers for Program Equivalence Checking through Invariant Sketching and Query Decomposition
Mahajan, Meena	(QBF) Lower Bound Techniques for QBF Proof Systems
Mahboubi, Assia	(Coq) Classical Analysis with Coq
Maieli, Roberto	(Linearity/TLLA) The structure of non decomposable connectives of linear logic
Maier, Jürgen	(ADHS) Verifying nonlinear analog and mixed-signal circuits with inputs
Majumdar, Rupak	(ADHS) Concentration of Measure for Chance-Constrained Optimization
Malacaria, Pasquale	(GS) Some reflections on algorithmic game semantics (CSF) Symbolic Side-Channel Analysis for Probabilistic Programs
Malbos, Philippe	(IWC) Coherence of monoids by insertions (IWC) Coherence modulo relations
Maleki, Mehrdad	(Domains13) A logical view of complex analytic maps
Maler, Oded	(LearnAut) Toward Learning Boolean Functions from Positive Examples
Malik, Sharad	(CAV) Lazy Self-Composition for Security Verification
Malioutov, Dmitry	(POS) MLIC: A MaxSAT-Based framework for learning interpretable classification rules
Malle, Bertram F.	(ReMOTE) Human morality, robots’ moral competence, and the deepest kind of trust
Maly, Jan	(PRUV) A new logic for jointly representing hard and soft constraints
Mancini, Toni	(RCRA) Computing Personalised Treatments through In Silico Clinical Trials. A Case Study on Downregulation in Assisted Reproduction. (RCRA) Optimal Fault-Tolerant Placement of Relay Nodes in a Mission Critical Wireless Network
Manerkar, Yatin	(PLR) RTLCheck: Automatically Verifying the Memory Consistency of Processor RTL
Mangharam, Rahul	(ADHS) Data-Driven Switched Affine Modeling for Model Predictive Control
Mangin, Cyprien	(Coq) Towards a formalization of the guard condition
Manighetti, Matteo	(CL&C) Admissible tools in the kitchen of intuitionistic logic
Manna, Marco	(LPOP) Role-Based Access Control via JASP (LPOP) Invited Talk: On the Development of Industrial Applications with ASP
Mannaa, Bassel	(FSCD) The clocks they are adjunctions. Denotational semantics for Clocked Type Theory (PARIS) What makes guarded types tick? (HoTT/UF) Dependent Right Adjoint Types
Mansfield, Martin	(Overture) Design Space Exploration for Secure Building Control
Manzonetto, Giulio	(Linearity/TLLA) The Bang Calculus and the Two Girard's Translations
Marantidis, Pavlos	(UNIF) ACUI Unification modulo Ground Theories
Maratea, Marco	(ICLP) Cautious Reasoning in ASP via Minimal models and Unsatisfiable Cores (ICLP) Shared aggregate sets in answer set programming
Marché, Claude	(F-IDE) Lightweight Interactive Proving inside an Automatic Program Verifier
Marcinkowski, Jerzy	(LICS) Can One Escape Red Chains? Regular Path Queries Determinacy is Undecidable.
Mardare, Radu	(LICS) An algebraic theory of Markov processes (LICS) Boolean-Valued Semantics for Stochastic Lambda-Calculus
Mari, Federico	(RCRA) Computing Personalised Treatments through In Silico Clinical Trials. A Case Study on Downregulation in Assisted Reproduction.
Marin, Sonia	(TYDI) Nested sequents for modal logics and beyond (WiL) Decomposing labelled proof theory for intuitionistic modal logic
Markey, Nicolas	(FM) Optimal and Robust Controller Synthesis Using Energy Timed Automata with Uncertainty (SR) Dependences in Strategy Logic
Markovtsev, Vadim	(MLP) Splitting source code identifiers using Bidirectional LSTM Recurrent Neural Network
Markowski, Gabor	(MLP) Splitting source code identifiers using Bidirectional LSTM Recurrent Neural Network
Marnette, Bruno	(MLP) Open Business Meeting for Future of Machine Learning for Programming
Marotta, Umberto	(PLR) An Efficient Zielonka's Algorithm for Parallel Parity Games
Marple, Kyle	(ICLP) Constraint Answer Set Programming without Grounding
Marques-Silva, Joao	(PC) On Dual-Rail Based MaxSAT Solving (IJCAR) A SAT-Based Approach to Learn Explainable Decision Sets (SAT) PySAT: A Python Toolkit for Prototyping with SAT Oracles
Marre, Bruno	(SMT) Centralizing Equality Reasoning in MCSAT
Marsden, Dan	(MSFP) Some No-Go Theorems for Distributive Laws (extended abstract)
Marshall, Andrew M.	(UNIF) Knowledge Problems in Equational Extensions of Subterm Convergent Theories
Marson, Giorgia Azzurra	(CSF) A Cryptographic Look at Multi-Party Channels
Marti, Michel	(EICNCL) Proof Translations in BI logic
Martin, Barnaby	(PC) Resolution and the binary encoding of combinatorial principles
Martin, Ursula	(LICS) On Diversity
Martinez, Maria Vanina	(PRUV) Leveraging Probabilistic Existential Rules for Adversarial Deduplication
Martins, Eunice	(ITP) A Coq Formalisation of SQL’S Execution Engines
Martins, Ruben	(SAT) MaxSAT Evaluation 2018
Martonosi, Margaret	(PLR) RTLCheck: Automatically Verifying the Memory Consistency of Processor RTL
Maréchal, Alexandre	(ITP) A Coq Tactic for Equality Learning in Linear Arithmetic
Masci, Paolo	(F-IDE) Integrating user design and formal models within PVSio-Web
Massini, Annalisa	(RCRA) Computing Personalised Treatments through In Silico Clinical Trials. A Case Study on Downregulation in Assisted Reproduction.
Matheja, Christoph	(CAV) Let this Graph be your Witness! An Attestor for Verifying Java Pointer Programs
Mathews, Minu	(SAT) Machine Learning-based Restart Policy for CDCL SAT Solvers
Mathur, Umang	(CAV) Controller Synthesis Made Real: Reach-avoid Specifications and Linear Dynamics
Matias, Lionel	(AVOCS) Climbing the Software Assurance Ladder - Practical Formal Verification for Reliable Software
Matthews, Stuart	(AVOCS) Climbing the Software Assurance Ladder - Practical Formal Verification for Reliable Software (VSTTE) Verified Software: Theories, Tools, ... and Engineering
Matyas, Jiri	(CAV) ADAC: Automated Design of Approximate Circuits
Maubert, Bastien	(SR) Quantifying Bounds in Strategy Logic (SR) Strategy Logic with Imperfect Information
Mauborgne, Laurent	(FM) Software Safety and Security and AI
Mauw, Sjouke	(GraMSec) The Attacker Does not Always Hold the Initiative: Attack Trees with External Refinement
Mazaheri, Sogol	(CSF) Backdoored Hash Functions: Immunizing HMAC and HKDF (CSF) Self-Guarding Cryptographic Protocols against Algorithm Substitution Attacks
Mazaitis, Kathryn	(MLP) Answering Cloze-style Software Questions Using Stack Overflow
Mazo Jr., Manuel	(ADHS) Optimal Symbolic Controllers Determinization for BDD storage.
Mazza, Damiano	(ITRS) Polyadic approximations and intersection types (ITRS/DCM joint invited talk) (HOR) The next 700 (type-theoretical) denotational models ?
McBride, Conor	(MSFP) Everybody's Got To Be Somewhere
McCall, Mckenna	(CSF) Knowledge-based Security of Dynamic Secrets for Reactive Programs
McCann, Julie	(AVOCS) Formal Verification of Synchronisation, Gossip and Environmental Effects for Wireless Sensor Networks
McCusker, Guy	(GS) Incomplete information and uniformity in game semantics
McIver, Annabelle	(FM) An Algebraic Approach for Reasoning About Information Flow (FM) Privacy in Text Processing: An information flow perspective
McMillan, Kenneth	(CAV) Eager Abstraction for Symbolic Model Checking (CAV) Learning Abstractions for Program Synthesis (FRIDA) Building verified distributed systems with IVy
Meel, Kuldeep S.	(POS) MLIC: A MaxSAT-Based framework for learning interpretable classification rules
Meggendorfer, Tobias	(CAV) Rabinizer 4: From LTL to Your Favourite Deterministic Automaton (LICS) Conditional Value-at-Risk for Reachability and Mean Payoff in Markov Decision Processes
Meinicke, Larissa	(FM) Encoding fairness in a synchronous concurrent program algebra
Melatti, Igor	(RCRA) Computing Personalised Treatments through In Silico Clinical Trials. A Case Study on Downregulation in Assisted Reproduction.
Melgratti, Hernan	(LICS) Concurrency and Probability: Removing Confusion, Compositionally
Melham, Tom	(CAV) Proof Scripting from HOL to Goaled (VDMW) How to attend a conference?
Melioli, Riccardo	(F-IDE) AsmetaF: a flattener for the ASMETA framework
Melliès, Paul-André	(GS) Asynchronous games fifteen years later (LICS) Ribbon tensorial logic (LICS) An Asynchronous Soundness Theorem for Concurrent Separation Logic (LOLA) Asynchronous games fifteen years later
Melquiond, Guillaume	(IJCAR) A Why3 framework for reflection proofs and its application to GMP's algorithms
Mendes, Alexandra	(ITP) Towards Verified Handwritten Calculational Proofs (Short Paper)
Meng, Yu	(ADHS) Verifying nonlinear analog and mixed-signal circuits with inputs
Mengel, Stefan	(QBF) Tractability results for structured quantified CNF-formulas via knowledge compilation (SAT) QBF as an Alternative to Courcelle's Theorem
Menghi, Claudio	(FM) Multi-Robot LTL Planning Under Uncertainty
Mens, Irini-Eleftheria	(LearnAut) Toward Learning Boolean Functions from Positive Examples
Merayo, Alicia	(WST) Inference of Linear Upper-Bounds on the Expected Cost by Solving Cost Relations
Merkle, Daniel	(VEMDP) Rule-Based Gillespie Simulation of Chemical Systems
Mertens, Eric	(CAV) Continuous formal verification of Amazon s2n
Mery, Daniel	(ARQNL) Labelled Connection-based Proof Search for Multiplicative Intuitionistic Linear Logic (ADSL) Labelled Cyclic Proofs for Separation Logic (EICNCL) Proof Translations in BI logic
Merz, Stephan	(AVOCS) Rule-Based Synthesis of Chains of Security Functions for Software-Defined Networks
Meyer, Philipp J.	(CAV) Strix: Explicit Reactive Synthesis Strikes Back!
Meßner, Florian	(ITP) A Formally Verified Solver for Homogeneous Linear Diophantine Equations
Micali, Silvio	(FSCD) ALGORAND A Truly Distributed Ledger
Micciancio, Daniele	(CSF) Symbolic security of garbled circuits
Michaud, Thibaud	(SYNT) Reactive Synthesis from LTL Specification with Spot
Middeldorp, Aart	(IWC) Towards a Verified Decision Procedure for Confluence of Ground Term Rewrite Systems in Isabelle/HOL (IWC) IWC Business Meeting (FSCD) Completion for Logically Constrained Rewriting (FSCD) ProTeM: A Proof Term Manipulator (FSCD) Confluence Competition 2018 (IJCAR) Cops and CoCoWeb: Infrastructure for Confluence Tools (IJCAR) FORT 2.0
Milani, Alfredo	(RCRA) Algebraic Crossover Operators for Permutations
Mili, Ali	(REFINE) Programming Without Refinement
Miller, Alice	(VaVAS) Probabilistic Model Checking for Autonomous Agent Strategy Synthesis - Extended Abstract
Miller, Dale	(LFMTP) Functional programming with λ-tree syntax: a progress report (LFMTP) Computation-as-deduction in Abella: work in progress
Mimram, Samuel	(FSCD) Coherence of Gray categories via rewriting
Mineshima, Koji	(NLCS) Paychecks, Presupposition, and Dependent Types
Miné, Antoine	(AVOCS) Experiences with thread-modular static analysis of concurrent embedded systems by abstract interpretation
Mio, Matteo	(LICS) Riesz Modal Logic with Threshold Operators
Miquey, Étienne	(LICS) A sequent calculus with dependent types for classical arithmetic (ITP) Formalizing Implicative Algebras in Coq
Mislove, Michael	(LICS) Enriching a Linear/Non-linear Lambda Calculus: A Programming Language for String Diagrams (Domains13) A Domain-theoretic Skorohod’s Theorem
Mitchell, David	(SAT) Centrality-Based Improvements to CDCL Heuristics
Mitchell, Ian M.	(ADHS) Control Synthesis and Classification for Unicycle Dynamics Using the Gradient and Value Sampling Particle Filters
Mitra, Arindam	(ICLP-DC) The Learning-Knowledge-Reasoning Paradigm For Natural Language Understanding and Question Answering (ICLP) Incremental and Iterative Learning of Answer Set Programs from Mutually Distinct Examples
Mitra, Sayan	(CAV) Controller Synthesis Made Real: Reach-avoid Specifications and Linear Dynamics (FM) Approximate Partial Order Reduction
Mitra, Sayan	(ADHS) Verifying nonlinear analog and mixed-signal circuits with inputs
Mitsou, Valia	(SAT) QBF as an Alternative to Courcelle's Theorem
Miyazawa, Alvaro	(VaVAS) RoboTool: Modelling and Verification with RoboChart
Mo, Man Yue	(FM) Variant Analysis with QL
Molyneux, Gareth	(VEMDP) Bayesian Verification of Chemical Reaction Networks
Momigliano, Alberto	(LFMTP) Property-Based Testing of Abstract Machines: an Experience Report
Monin, Benoit	(LICS) An answer to the Gamma question
Monmege, Benjamin	(MoRe) A journey through negatively-weighted timed games: undecidability, decidability, approximability
Montanari, Ugo	(LICS) Concurrency and Probability: Removing Confusion, Compositionally
Monteiro, Pedro T.	(ICLP-DC) Model Revision of Logical Regulatory Networks using Logic-based Tools
Montesi, Fabrizio	(Linearity/TLLA) Taking Linear Logic Apart
Montin, Mathieu	(REFINE) Ordering strict partial orders to model behavioural refinement
Montmirail, Valentin	(IJCAR) An Assumption-Based Approach for Solving The Minimal S5-Satisfiability Problem
Moore, Brandon	(CSF) KEVM: A Complete Formal Semantics of the Ethereum Virtual Machine
Moot, Richard	(NLCS) Do different syntactic trees yield different logical readings? Some remarks on head variables in typed lambda calculus.
Mora, Federico	(CAV) StringFuzz: A Fuzzer for String Solvers
Morak, Michael	(ASPOCP) selp: A Single-Shot Epistemic Logic Program Solver (SAT) Exploiting Treewidth for Projected Model Counting and its Limits
Morales, Jose F.	(ICLP) Towards Static Performance Guarantees for Programs with Run-time Checks (ICLP) Towards Incremental and Modular Context-sensitive Analysis
Morales, Marianela	(WiL) Decomposing labelled proof theory for intuitionistic modal logic
Morarescu, Irinel Constantin	(ADHS) Network-Aware Design of State-Feedback Controllers for Linear Wireless Networked Control Systems
Morehouse, Edward	(HoTT/UF) Ordered Cubes
Morgado, Antonio	(PC) On Dual-Rail Based MaxSAT Solving (SAT) PySAT: A Python Toolkit for Prototyping with SAT Oracles
Morisset, Charles	(Overture) Design Space Exploration for Secure Building Control (FCS) LISA: Predicting the Impact of DoS Attacks on Real-World Low Power IoT Systems
Moscato, Mariano	(FM) A Formally Verified Floating-Point Implementation of the Compact Position Reporting Algorithm (ITP) Boosting the Reuse of Formal Specifications
Moser, Georg	(IFIP WG 1.6) Discussion on Reviewing Culture in TCS (IFIP WG 1.6) Discussion on IFIP (IJCAR) MaedMax: A Maximal Ordered Completion Tool
Moshier, M. Andrew	(Domains13) Extending Stone Duality to Relations (Domains13) Frames and frame relations
Moss, Larry	(ARQNL) Automated Reasoning In Natural Language: Current Directions (NLCS) Automated Reasoning from Polarized Parse Trees
Moss, Sean	(LICS) Dialectica models of type theory
Mota, Jean-Marc	(AVOCS) Climbing the Software Assurance Ladder - Practical Formal Verification for Reliable Software
Mottet, Antoine	(UNIF) ACUI Unification modulo Ground Theories (LICS) A universal-algebraic proof of the complexity dichotomy for Monotone Monadic SNP
Moy, Yannick	(AVOCS) Climbing the Software Assurance Ladder - Practical Formal Verification for Reliable Software (AVOCS) Mostly harmless - luring programmers into proof with SPARK (F-IDE) Lightweight Interactive Proving inside an Automatic Program Verifier
Mozo Carollo, Imanol	(Domains13) Frames and frame relations
Mrazek, Vojtech	(CAV) ADAC: Automated Design of Approximate Circuits
Mueller, Moritz	(LICS) A parameterized halting problem, the linear time hierarchy, and the MRDP theorem
Muggleton, Stephen H.	(FoPSS) Inductive logic programming I (FoPSS) Inductive logic programming II (SYNT) Meta-Interpretive Learning of Logic Programs
Mullen, Eric	(CAV) Continuous formal verification of Amazon s2n (ITP) Software Verification with ITPs Should Use Binary Code Extraction to Reduce the TCB (Short Paper)
Mulligan, Casey	(SCSC) RP: Non-linear Real Arithmetic Benchmarks derived from Automated Reasoning in Economics
Munch-Maccagnoni, Guillaume	(LOLA) A resource modality for RAII
Muniz, Marco	(MoRe) Comfort and Energy Optimization for Floor Heating Systems (CAV) Start Pruning When Time Gets Urgent: Partial Order Reduction for Timed Systems
Munoz, Cesar	(FM) From Formal Requirements to Highly Assured Software for Unmanned Aircraft Systems (FM) A Formally Verified Floating-Point Implementation of the Compact Position Reporting Algorithm (ITP) Boosting the Reuse of Formal Specifications
Murano, Aniello	(PLR) An Efficient Zielonka's Algorithm for Parallel Parity Games (SR) Verification of Multi-agent Systems with Imperfect Information and Public Actions (SR) Quantifying Bounds in Strategy Logic (SR) Strategy Logic with Imperfect Information (SR) Solving Parity Games: Explicit vs Symbolic
Murawski, Andrzej	(GS) Automata Theory and Game Semantics
Muroya, Koko	(LICS) The Geometry of Computation-Graph Abstraction (LOLA) A graph-rewriting perspective of the beta-law
Murray, Richard M.	(TLA) Proving properties of a minimal covering algorithm
Murray, Richard M.	(ADHS) Temporal Logic Control of POMDPs Via Label-Based Stochastic Simulation Relations
Murugesan, Anitha	(F-IDE) The CLEAR Way To Transparent Formal Methods
Mutluergil, Suha Orhun	(CAV) Reasoning About TSO Programs Using Reduction and Abstraction
Myojin, Tomoyuki	(VaVAS) Policing Functions for Machine Learning Systems
Myreen, Magnus	(CAV) From Processor Verification Upwards (PAAR) The CakeML Verified Compiler and Toolchain (IJCAR) Proof-Producing Synthesis of CakeML with I/O and Local State from Monadic HOL Functions (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
Mödersheim, Sebastian A.	(CSF) A Typing Result for Stateful Protocols
Mörtberg, Anders	(LICS) On Higher Inductive Types in Cubical Type Theory
Møgelberg, Rasmus	(FSCD) The clocks they are adjunctions. Denotational semantics for Clocked Type Theory (PARIS) What makes guarded types tick? (HoTT/UF) Dependent Right Adjoint Types
Müller, Christian	(CSF) Inductive Invariants for Noninterference in Multi-agent Workflows
Müller, Dennis	(IJCAR) Theories as Types (Tetrapod) Discussion 1 (Tetrapod) Discussion 2
Müller, Moritz	(LCC) Feasibly constructive proofs of succinct weak circuit lower bounds
Müller, Peter	(CAV) Permission Inference for Array Programs (CAV) MaxSMT-Based Type Inference for Python 3 (CAV) Nagini: A Static Verifier for Python (PLR) Permission Inference for Array Programs
Münger, Severin	(CAV) Permission Inference for Array Programs (PLR) Permission Inference for Array Programs
N
Nadel, Alexander	(SAT) Chronological Backtracking (SAT) Solving MaxSAT with Bit-Vector Optimization
Nagashima, Yutaka	(Isabelle) PaMpeR: A Proof Method Recommendation System for Isabelle/HOL
Nagele, Julian	(FSCD) Confluence Competition 2018 (IJCAR) Cops and CoCoWeb: Infrastructure for Confluence Tools
Naik, Mayur	(MLP) Difflog: Beyond Deductive Methods in Program Analysis
Nakagawa, Yuichiroh	(VaVAS) Policing Functions for Machine Learning Systems
Nakano, Keisuke	(FSCD) On repetitive right application of B-terms (Coq) ComplCoq: Rewrite Hint Construction with Completion Procedures
Nakazawa, Koji	(IWC) Complete Axiom System of Cluster Algebra (ADSL) Cyclic Theorem Prover for Separation Logic by Magic Wand
Nalon, Cláudia	(WiL) On the Combination of Resolution and SAT Procedures for Modal Theorem-Proving (PAAR) Evaluating Pre-Processing Techniques for the Separated Normal Form for Temporal Logics (IJCAR) A Resolution-Based Calculus for Preferential Logics
Namjoshi, Kedar	(CAV) Synthesis Of Asynchronous Reactive Programs From Temporal Specifications
Nampally, Arun	(ICLP) Constraint-Based Inference in Probabilistic Logic Programs
Nanjo, Yoji	(LICS) A Fixpoint Logic and Dependent Effects for Temporal Property Verification
Nantes-Sobrinho, Daniele	(FSCD) Fixed-Point Constraints for Nominal Equational Unification
Narboux, Julien	(ThEdu) GeoCoq: formalized foundations of geometry
Narkawicz, Anthony	(FM) From Formal Requirements to Highly Assured Software for Unmanned Aircraft Systems
Narodytska, Nina	(IJCAR) A SAT-Based Approach to Learn Explainable Decision Sets (SAT) Constrained Image Generation Using Binarized Neural Networks with Decision Procedures
Naumann, David	(CSF) Assuming you know: epistemic semantics of relational annotations for expressive flow policies
Navas, Jorge A	(VSTTE) Executable Counterexamples in Software Model Checking
Negri, Sara	(EICNCL) Proof theory for quantified monotone modal logics
Nellen, Johanna	(FM) Formal Verification of Automotive Simulink Controller Models: Empirical Technical Challenges, Evaluation and Recommendations
Nelson, Tim	(FM) CompoSAT: Specification-Guided Coverage for Model Finding
Nemouchi, Yakoub	(Isabelle) Using Isabelle/UTP for the Verification of Sorting Algorithms: A Case Study
Neubig, Graham	(MLP) Answering Cloze-style Software Questions Using Stack Overflow
Neuper, Walther	(ThEdu) ThEdu'18 business meeting (ThEdu) Lucas Interpretation from Programmers’ Perspective
New, Max	(FSCD) Call-by-name Gradual Type Theory
Newstead, Clive	(HoTT/UF) Algebraic models of dependent type theory
Ng, Kang Feng	(FSCD) A diagrammatic axiomatisation of fermionic quantum circuits (LICS) Two complete axiomatisations of pure-state qubit quantum computing
Nguyen, Hien	(ASPOCP) Partial Evaluation of Logic Programs in Vector Spaces
Nguyen, Huyen T.T.	(CAV) Quasi-Optimal Partial Order Reduction
Nguyen, Thanh	(ICLP) Phylotastic: An Experiment in Creating, Manipulating, and Evolving Phylogenetic Biology Workflows Using Logic Programming
Nguyen, Van	(ICLP-DC) Natural Language Generation From Ontologies (ICLP) Experimenting with robotic intra-logistics domains (ICLP) Natural Language Generation From Ontologies: Application Paper
Nguyễn, Lê Thành Dũng	(FSCD) Unique perfect matchings and proof nets (Linearity/TLLA) A semantic conjecture on second-order MLL and its complexity consequences (work in progress) (Linearity/TLLA) Coherent interaction graphs: a nondeterministic geometry of interaction for MLL
Nickovic, Dejan	(CAV) A Counting Semantics for Monitoring LTL Specifications over Finite Traces
Nicolau Jr., Dan	(VEMDP) Formal Verification of Network-Based Biocomputation Circuits
Niemetz, Aina	(CAV) BTOR2, BtorMC and Boolector 3.0 (CAV) Solving Quantified Bit-Vectors using Invertibility Conditions (SMT) Rewrites for SMT Solvers using Syntax-Guided Enumeration
Niewerth, Matthias	(LICS) MSO Queries on Trees: Enumerating Answers under Updates Using Forest Algebras
Nigam, Vivek	(LCC) My Journey through Observational Equivalence Research with Martin Hofmann (IJCAR) A Logical Framework with Commutative and Non-Commutative Subexponentials (FCS) Statistical Model Checking of Guessing and Timing Attacks on Distance-bounding Protocols
Nigam, Vivek	(WPTE) Verification of Ada Programs with AdaHorn
Nilsson, Petter	(ADHS) Nonuniform abstractions, refinement and controller synthesis with novel BDD encodings
Nilsson, Petter	(ADHS) Temporal Logic Control of POMDPs Via Label-Based Stochastic Simulation Relations
Nilsson, René Søndergaard	(Overture) Transforming an industrial case study from VDM++ to VDM-SL (Overture) Enhancing Testing of VDM-SL models
Nipkow, Tobias	(ITP) Verified Memoization and Dynamic Programming (ITP) Verified Analysis of Random Binary Tree Structures
Nirina, Andrianarivelo	(FSCD) Confluence of Prefix-Constrained Rewrite Systems
Nishida, Naoki	(IWC) Convergence of Simultaneously and Sequentially Unraveled TRSs for Normal Conditional TRSs (FSCD) Narrowing Trees for Syntactically Deterministic Conditional Term Rewriting Systems (FSCD) Confluence Competition 2018 (VSTTE) Loop Detection by Logically Constrained Term Rewriting (WPTE) On Transforming Narrowing Trees into Regular Tree Grammars Generating Ranges of Substitutions (WPTE) On Transforming Functions Accessing Global Variables into Logically Constrained Term Rewriting Systems
Noetzli, Andres	(SMT) Rewrites for SMT Solvers using Syntax-Guided Enumeration
Noll, Thomas	(CAV) Let this Graph be your Witness! An Attestor for Verifying Java Pointer Programs (CAV) Symbolic Liveness Analysis of Real-World Software
Nollet, Rémi	(PARIS) Local Validity for Circular Proofs in Linear Logic with Fixed Points
Nonato, Maddalena	(RCRA) Logic Programming approaches for routing fault-free and maximally-parallel Wavelength Routed Optical Networks on Chip (Application paper)
Nordstrom, Jakob	(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
Norman, Gethin	(VaVAS) Probabilistic Model Checking for Autonomous Agent Strategy Synthesis - Extended Abstract
Norrish, Michael	(CAV) HOL Developed and HOL Used: Interconnected Stories of Real-World Applications (IJCAR) Proof-Producing Synthesis of CakeML with I/O and Local State from Monadic HOL Functions (ITP) Verifying the LTL to Büchi Automata Translation via Very Weak Alternating Automata
North, Paige	(HDRA) A homotopy type theory for directed homotopy theory
Novotný, Petr	(LICS) Efficient Algorithms for Asymptotic Bounds on Termination Time in VASS
Nowak, David	(AVOCS) Proof-Oriented Design of a Separation Kernel with Minimal Trusted Computing Base (VSTTE) Formalising Executable Specifications of Low-Level Systems
Nowland, Trisha	(WiL) Towards a Logical Framework for Latent Variable Modelling
Nowotka, Dirk	(PLR) Tuning Parallel SAT Solvers (FM) Statistical Model Checking of LLVM Code (POS) Tuning Parallel SAT Solvers
Nutz, Alexander	(VSTTE) The Map Equality Domain (VSTTE) A Tree-Based Approach to Data Flow Proofs
Nuyts, Andreas	(LICS) Degrees of Relatedness - A Unified Framework for Parametricity, Irrelevance, Ad Hoc Polymorphism, Intersections, Unions and Algebra in Dependent Type Theory (HoTT/UF) Robust Notions of Contextual Fibrancy (HoTT/UF) Internalizing Presheaf Semantics: Charting the Design Space
Nührenberg, Georg	(DS-FM) Formal verification of neural networks (VSTTE) Verification of Binarized Neural Networks via Inter-Neuron Factoring
O
O'Hearn, Peter	(FLoC) Continuous Reasoning: Scaling the Impact of Formal Methods (FLoC) Formal Reasoning and the Hacker Way
Oberhauser, Jonas	(VSTTE) Store Buffer Reduction in The Presence of Mixed-Size Accesses and Misalignment
Obermeier, Philipp	(ICLP-DC) Scalable Robotic Intra-Logistics with Answer Set Programming (ICLP) Routing Driverless Transport Vehicles in Car Assembly with Answer Set Programming (ICLP) Experimenting with robotic intra-logistics domains
Ochremiak, Joanna	(LICS) Definable Ellipsoid Method, Sums-of-Squares Proofs, and the Isomorphism Problem
Oda, Tomohiro	(Overture) ViennaVM: a Virtual Machine for VDM-SL development
Oddi, Angelo	(RCRA) Greedy Randomized Search for Scalable Compilation of Quantum Circuits
Oechsner, Sabine	(CSF) Computer-aided proofs for multiparty computation with active security
Oepen, Jan-Hendrik	(AVOCS) Writing a Model Checker in 80 Days: Reusable Libraries and Custom Implementation
Ogawa, Hideto	(VaVAS) Policing Functions for Machine Learning Systems
Ogawa, Mizuhito	(SCSC) EA: Wrapping Computer Algebra is Surprisingly Successful for Non-Linear SMT
Oh, Chanseok	(SAT) Machine Learning-based Restart Policy for CDCL SAT Solvers
Oitavem, Isabel	(LCC) A recursion-theoretic characterisation of the positive polynomial-time functions
Okada, Mitsuhiro	(TERMGRAPH) On quasi ordinal diagram systems
Olarte, Carlos	(Linearity/TLLA) Benchmarking Linear Logic Translations
Olimpieri, Federico	(Linearity/TLLA) On the Taylor expansion of λ-terms and the groupoid structure of their rigid approximants (HOR) Normalization and Taylor expansion of lambda-terms
Olivetti, Nicola	(EICNCL) Hypersequent calculus for the logic of conditional belief: preliminary results (EICNCL) Toward intuitionistic non-normal modal logic and its calculi
Ong, Luke	(LMW) Constrained Horn clauses as a basis of automatic program verification: the higher-order case (GS) Strategies as sheaves on plays (LICS) Species, Profunctors and Taylor Expansion Weighted by SMCC--A Unified Framework for Modelling Nondeterministic, Probabilistic and Quantum Programs--
Oprea, Maria Antonia	(Isabelle) Hilbert Meets Isabelle: Formalisation of the DPRM Theorem in Isabelle
Oraee, Simin	(CAV) Symbolic Algorithms for Graphs and Markov Decision Processes with Fairness Objectives
Orejas, Fernando	(TERMGRAPH) Critical Pairs in Graph Transformation Systems
Orlandelli, Eugenio	(ARQNL) Labelled Calculi for QMLs with Non-Rigid and Non-Denoting Terms (EICNCL) Proof theory for quantified monotone modal logics
Orton, Ian	(FSCD) Internal Universes in Models of Homotopy Type Theory
Osama, Muhammad	(PLR) GPU Accelerated SAT solving
Ostropolski-Nalewaja, Piotr	(LICS) Can One Escape Red Chains? Regular Path Queries Determinacy is Undecidable.
Otten, Jens	(PAAR) Proof Search Optimizations for Non-clausal Connection Calculi
Otto, Thomas	(ICLP) Experimenting with robotic intra-logistics domains
Ouaknine, Joel	(LICS) Sequential Relational Decomposition (LICS) Polynomial Invariants for Affine Programs
Overbeek, Roy	(FSCD) Decreasing diagrams with two labels are complete for confluence of countable systems
Owens, Scott	(VSTTE) Program Verification in the Presence of I/O: Semantics, verified library routines, and verified applications
Ozay, Necmiye	(SYNT) Towards correct-by-construction controller synthesis for self-driving cars (SYNT) Warm-Starting Fixed-Point Based Control Synthesis
Ozay, Necmiye	(ADHS) Nonuniform abstractions, refinement and controller synthesis with novel BDD encodings
Ozay, Necmiye	(ADHS) Input Design for Nonlinear Model Discrimination Via Affine Abstraction
Ozay, Necmiye	(ADHS) Optimization-Based Design of Bounded-Error Estimators Robust to Missing Data
P
Pacheco, Hugo	(CSF) Enforcing ideal-world leakage bounds in real-world secret sharing MPC frameworks
Padget, Julian	(VaVAS) Social Consequence Engines (Abstract)
Pagani, Michele	(Linearity/TLLA) Applying linear logic semantics to probabilistic programming
Page, Charlie	(VaVAS) Social Consequence Engines (Abstract)
Pal, Abhik	(Isabelle) Hilbert Meets Isabelle: Formalisation of the DPRM Theorem in Isabelle
Palacios, Adrián	(HCVS) Metaprogramming and symbolic execution for detecting runtime errors in Erlang programs
Palamidessi, Catuscia	(LICS) The 2018 Alonzo Church Award for Outstanding Contributions to Logic and Computation (CSF) Local Differential Privacy on Metric Spaces: optimizing the trade-off with utility
Palau Romero, Francisco	(SAT) Approximately Propagation Complete and Conflict Propagating Constraint Encodings
Palezzato, Elisa	(SCSC) EA: New in CoCoA-5.2.4 and CoCoALib-0.99570 for SC-Square
Palmigiano, Alessandra	(ITP) Software Tool Support for Modular Reasoning in Modal Logics of Actions
Panangaden, Prakash	(LICS) An algebraic theory of Markov processes (LICS) Boolean-Valued Semantics for Stochastic Lambda-Calculus
Panchekha, Pavel	(FM) Combining Tools for Optimization and Analysis of Floating-Point Computations
Pantel, Marc	(REFINE) Ordering strict partial orders to model behavioural refinement
Paolini, Luca	(Linearity/TLLA) Quantum programming made easy
Paquet, Hugo	(GS) Continuous probability distributions in concurrent games (LICS) The concurrent game semantics of Probabilistic PCF
Pardo, Raúl	(FM) Timed Epistemic Knowledge Bases for Social Networks
Pardylla, Carsten	(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
Paredes, José	(PRUV) Leveraging Probabilistic Existential Rules for Adversarial Deduplication
Park, Daejun	(CSF) KEVM: A Complete Formal Semantics of the Ethereum Virtual Machine
Park, Spencer	(F-IDE) A Notebook Format for the Holistic Design of Embedded Systems
Parker, David	(VaVAS) Policy Generation with Probabilistic Guarantees for Long-term Autonomy of a Mobile Service Robot (VaVAS) Robot Demonstration
Parsert, Julian	(ITP) A Formally Verified Solver for Homogeneous Linear Diophantine Equations (ITP) Towards Formal Foundations for Game Theory (Short Paper)
Part, Fedor	(PC) Resolution with Counting: Different Moduli and Tree-Like Lower Bounds
Parys, Paweł	(FSCD) Homogeneity without Loss of Generality (ITRS) Intersection Types for Unboundedness Problems (ITRS invited talk)
Pasareanu, Corina	(CSF) Symbolic Side-Channel Analysis for Probabilistic Programs
Patil, Bhagyesh	(ADHS) Multi-Energy Scheduling Using a Hybrid Systems Approach
Pattinson, Dirk	(LICS) A van Benthem Theorem for Fuzzy Modal Logic (IJCAR) A Resolution-Based Calculus for Preferential Logics (EICNCL) Title TBA - Invited talk (VSTTE) Verified Certificate Checking for Counting Votes
Pau, Cleo	(UNIF) Proximity-Based Generalization
Paulson, Lawrence C.	(VDMW) How to get a paper accepted?
Paulus, Joseph	(TYDI) Deep-Inference Intersection Types
Pauly, Arno	(Domains13) T^\omega-representations of compact sets through dyadic subbases (SR) Beyond admissibility: Dominance between chains of strategies
Paun, Andrei	(VEMDP) Computational Approaches for the Programmed Assembly of Nanocellulose Meshes
Paun, Mihaela	(VEMDP) Computational Approaches for the Programmed Assembly of Nanocellulose Meshes
Pautasso, Daniele	(ITRS) Strong normalization of simple types through uniform intersection types.
Pavlogiannis, Andreas	(FRIDA) Stateless model-checking under the data-centric view
Pavlovic, Dusko	(LICS) Sound up-to techniques and Complete abstract domains
Paxian, Tobias	(SAT) Dynamic Polynomial Watchdog Encoding for Solving Weighted MaxSAT
Payet, Etienne	(IJCAR) Checking Array Bounds by Abstract Interpretation and Symbolic Expressions
Peano, Andrea	(RCRA) Logic Programming approaches for routing fault-free and maximally-parallel Wavelength Routed Optical Networks on Chip (Application paper)
Pearce, David	(ICLP) Functional ASP with Intensional Sets; Application to Gelfond-Zhang Agreggates
Pecheur, Charles	(FM) Producing Explanations for Rich Logics (AVOCS) A Framework for the Formal Verification of Networks of Railway Interlockings - Application to the Belgian Railways
Peitl, Tomas	(QBF) Chess Solving and Composing (QBFEval18 Contribution)
Peitl, Tomáš	(QBF) Portfolio-Based Algorithm Selection for Circuit QBFs (SAT) Polynomial-Time Validation of QCDCL Certificates
Pelgrom, Nemi	(WiL) Can every real proof be represented by a formal proof? The Hilbert-Gentzen thesis
Pellauer, Michael	(PLR) RTLCheck: Automatically Verifying the Memory Consistency of Processor RTL
Pelliccione, Patrizio	(FM) Multi-Robot LTL Planning Under Uncertainty
Pellissier, Luc	(Linearity/TLLA) Generalized generalized species of structure and resource modalities (Linearity/TLLA) Entropy and Complexity Lower Bounds
Peltier, Nicolas	(IJCAR) Superposition with Datatypes and Codatatypes (IJCAR) A Generic Framework for Implicate Generation Modulo Theories (IJCAR) A Tableaux Calculus for Reducing Proof Size (ADSL) The Complexity of Prenex Separation Logic with One Selector
Perdrix, Simon	(LICS) Diagrammatic Reasoning beyond Clifford+T Quantum Mechanics (LICS) A Complete Axiomatisation of the ZX-Calculus for Clifford+T Quantum Mechanics
Pereira, Filipe	(IJCAR) A SAT-Based Approach to Learn Explainable Decision Sets
Pereira, Vitor	(CSF) Enforcing ideal-world leakage bounds in real-world secret sharing MPC frameworks
Peressotti, Marco	(Linearity/TLLA) Taking Linear Logic Apart
Perrin, Nicolas	(SYNT) Warm-Starting Fixed-Point Based Control Synthesis
Petrakis, Iosif	(HoTT/UF) A Yoneda lemma-formulation of the univalence axiom
Petrasch, Jessica	(AVOCS) Writing a Model Checker in 80 Days: Reusable Libraries and Custom Implementation
Petrenko, Alexandre	(FM) FSM Inference from Long Traces
Petrucci, Laure	(CAV) Quasi-Optimal Partial Order Reduction
Pettorossi, Alberto	(HCVS) Metaprogramming and symbolic execution for detecting runtime errors in Erlang programs (ICLP) Solving Horn Clauses on Inductive Data Types Without Induction
Peuter, Dennis	(SYNT) On Inductive Verification and Synthesis
Pfenning, Frank	(LICS) Work Analysis with Resource-Aware Session Types (Linearity/TLLA) A shared memory semantics for session types
Phan, Quoc-Sang	(CSF) Symbolic Side-Channel Analysis for Probabilistic Programs
Phan, Vu	(ASPOCP) Syntactic Conditions for Antichain Property in Consistency Restoring Prolog
Phillips, Andrew	(VEMDP) Rule-based design of computational DNA devices
Pich, Ján	(LCC) Feasibly constructive proofs of succinct weak circuit lower bounds
Pick, Lauren	(CAV) Exploiting Synchrony and Symmetry in Relational Verification
Pientka, Brigitte	(FSCD) Index-Stratified Types (WiL) POPLMark Reloaded: Mechanizing Logical Relations Proofs (LMW) How to get the most out of a conference like FLOC? (LMW) Panel Discussion
Pierce, Benjamin C.	(LICS) Remembering Martin Hofmann
Pierce, Ken	(Overture) Multi-modelling of Cooperative Swarms (Overture) Design Space Exploration for Secure Building Control (Overture) Welcome to the Overture Workshop
Pieters, Wolter	(GraMSec) Combining Bayesian Networks and Fishbone Diagrams to Distinguish between Intentional Attacks and Accidental Technical Failures
Pignard, Pascal	(AVOCS) Climbing the Software Assurance Ladder - Practical Formal Verification for Reliable Software
Pike, Lee	(CAV) Formal Verification of a Vehicle-to-Vehicle (V2V) Messaging System
Pilipczuk, Michał	(LICS) On the number of types in sparse graphs (LICS) Parameterized circuit complexity of model-checking on sparse structures (LICS) Definable decompositions for graphs of bounded linear cliquewidth
Pimentel, Elaine	(TYDI) Sequentialising nested systems (WiL) A semantical view of sequent based systems (Linearity/TLLA) Benchmarking Linear Logic Translations
Pin, Edwin	(LCC) Completeness in the Second Level of the Polynomial Time Hierarchy through Syntactic Properties
Pinchinat, Sophie	(GraMSec) Deciding the Non-Emptiness of Attack trees (CSF) Guided design of attack trees: a system-based approach
Piotrowski, Bartosz	(IJCAR) ATPboost: Learning Premise Selection in Binary Setting with ATP Feedback
Piotrów, Marek	(POS) Competitive Sorter-based Encoding of PB-Constraints into SAT
Piróg, Maciej	(LICS) Syntax and Semantics for Operations with Scopes
Piskac, Ruzica	(SYNT) Programming by example: efficient, but not “helpful”
Pistone, Paolo	(Linearity/TLLA) Proof nets, coends and the Yoneda isomorphism
Pitts, Andrew M.	(FSCD) Internal Universes in Models of Homotopy Type Theory (HoTT/UF) Axiomatizing Cubical Sets Models of Univalent Foundations (HoTT/UF) Dependent Right Adjoint Types
Pizani Flor, João Paulo	(ITP) Verified Timing Transformations in Synchronous Circuits with LambdaPi-Ware
Plaisted, David	(TERMGRAPH) Programming by Term Rewriting
Platzer, Andre	(ADHS) CoasterX: A Case Study in Component-Driven Hybrid Systems Proof Automation
Platzer, André	(SoMLMFM) Safe reinforcement learning via formal methods (FM) Vector Barrier Certificates and Comparison Systems (LICS) A Hybrid, Dynamic Logic for Hybrid-Dynamic Information Flow (LICS) Differential Equation Axiomatization: The Impressive Power of Differential Ghosts (IJCAR) Uniform Substitution for Differential Game Logic
Plesa, Tomislav	(VEMDP) Noise control for molecular computing
Plotkin, Gordon	(LICS) An algebraic theory of Markov processes (Domains13) First-order differential programming
Podelski, Andreas	(VSTTE) The Map Equality Domain (VSTTE) A Tree-Based Approach to Data Flow Proofs
Poettering, Bertram	(CSF) A Cryptographic Look at Multi-Party Channels
Pohjola, Johannes Åman	(VSTTE) Program Verification in the Presence of I/O: Semantics, verified library routines, and verified applications
Pola, Giordano	(ADHS) On Approximate Predictability of Metric Systems
Polgreen, Elizabeth	(CAV) Synthesis Modulo Theories (SYNT) Safe, Automated and Formal Synthesis of Digital Controllers for Continuous Plants
Pontelli, Enrico	(PLR) MASP-Reduce: a proposal for distributed computation of stable models (ICLP) Phylotastic: An Experiment in Creating, Manipulating, and Evolving Phylogenetic Biology Workflows Using Logic Programming (ICLP) MASP-Reduce: a proposal for distributed computation of stable models (ICLP) Natural Language Generation From Ontologies: Application Paper
Pope, Jeremy	(MSFP) Formalizing Constructive Quantifier Elimination in Agda
Porncharoenwase, Sorawee	(FM) CompoSAT: Specification-Guided Coverage for Model Finding
Portela, Bernardo	(CSF) Enforcing ideal-world leakage bounds in real-world secret sharing MPC frameworks
Postan, Ezequiel	(UITP) Partial Regularization of First-Order Resolution Proofs
Postoyan, Romain	(ADHS) Network-Aware Design of State-Feedback Controllers for Linear Wireless Networked Control Systems
Potet, Marie-Laure	(CAV) Model Generation for Quantified Formulas: A Taint-Based Approach
Potyka, Nico	(PRUV) Measuring Disagreement among Knowledge Bases
Poulsen, Danny Bøgsted	(FM) Statistical Model Checking of LLVM Code
Pouly, Amaury	(LICS) Polynomial Invariants for Affine Programs
Pous, Damien	(LICS) Allegories: decidability and graph homomorphisms (ITP) A Formal Proof of the Minor-Exclusion Property for Treewidth-Two Graphs
Powell, Thomas	(LICS) A functional interpretation with state
Power, John	(Domains13) Higher-dimensional categories: recursion on extensivity
Pradel, Michael	(MLP) DeepBugs: A Learning Approach to Name-based Bug Detection
Pradic, Pierre	(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
Prathamesh, T. V. H.	(IWC) Towards a Verified Decision Procedure for Confluence of Ground Term Rewrite Systems in Isabelle/HOL (SCSC) RP: Unknot Recognition Through Quantifier Elimination
Praveen, M.	(LICS) Playing with Repetitions in Data Words Using Energy Games
Precup, Doina	(FoPSS) Reinforcement learning III (FoPSS) Reinforcement learning IV (LearnAut) Methods for learning weighted finite automata and their use in reinforcement learning
Preiner, Mathias	(CAV) BTOR2, BtorMC and Boolector 3.0 (CAV) Solving Quantified Bit-Vectors using Invertibility Conditions (SMT) Rewrites for SMT Solvers using Syntax-Guided Enumeration
Preto, Sandro	(IJCAR) Probably Half True: Probabilistic Satisfiability over Lukasiewicz Infinitely-valued Logic
Previti, Alessandro	(ICLP) Cautious Reasoning in ASP via Minimal models and Unsatisfiable Cores
Proietti, Maurizio	(HCVS) Metaprogramming and symbolic execution for detecting runtime errors in Erlang programs (ICLP) Solving Horn Clauses on Inductive Data Types Without Induction
Pu, Geguang	(CAV) SimpleCAR: An Efficient Bug-Finding Tool Based On Approximate Reachability (WiL) First-Order vs. Second-Order Encodings for LTLf-to-Automata Translation
Pulina, Luca	(QBF) QBFEval 2018 (SAT) Constrained Image Generation Using Binarized Neural Networks with Decision Procedures (SAT) QBFEVAL’18
Purandare, Rahul	(FM) Dynamic Symbolic Verification of MPI Programs
Putot, Sylvie	(CAV) Inner and Outer Approximating Flowpipes for Delay Differential Equations
Pym, David	(ADSL) Resource semantics: substructural logic as a modelling technology (keynote)
Püschel, Markus	(CAV) Fast Numerical Program Analysis with Reinforcement Learning
Q
Qadeer, Shaz	(CAV) Proving a concurrent program correct by demonstrating it does nothing (CAV) On the Completeness of Verifying Message Passing Programs under Bounded Asynchrony (CAV) Proving a concurrent program correct by demonstrating it does nothing (continued)
Qin, Shengchao	(FM) Towards `Verifying' a Water Treatment System
Qin, Xudong	(AVOCS) Using SMT engine to generate Symbolic Automata
Qu, Hongyang	(VaVAS) Towards a verifiable decision making framework for self-driving vehicles
Quaresma, Pedro	(ThEdu) ThEdu'18 business meeting (ThEdu) Rating of Geometric Automated Theorem Provers
Quatmann, Tim	(MoRe) Multiple Objectives and Cost Bounds in MDP (CAV) Sound Value Iteration
R
Rabe, Florian	(IJCAR) Theories as Types
Rabe, Markus N.	(CAV) Understanding and Extending Incremental Determinization for 2QBF (QBF) Understanding and Extending Incremental Determinization for 2QBF
Rabusseau, Guillaume	(LearnAut) Learning Graph Weighted Models on Pictures
Rademaker, Alexandre	(NLCS) OpenWordNet-PT: Taking Stock
Radomirovic, Sasa	(CSF) Alethea: A Provably Secure Random Sample Voting Protocol (CSF) Automated Unbounded Verification of Stateful Cryptographic Protocols with Exclusive OR
Raffaeli, Laurent	(NSV) Needs in formal methods for the validation of naval systems
Raffalli, Christophe	(LFMTP) Abstract Representation of Binders in OCaml using the Bindlib Library
Raghothaman, Mukund	(MLP) Difflog: Beyond Deductive Methods in Program Analysis
Rahli, Vincent	(LICS) Computability Beyond Church-Turing via Choice Sequences
Rajani, Vineet	(CSF) Types for Information Flow Control: Labeling Granularity and Semantic Models
Rajkhowa, Pritom	(VSTTE) Extending VIAP to Handle Array Programs
Rakotonirina, Itsaka	(CAV) The DEEPSEC prover
Ralph, Benjamin	(TYDI) Deep Inference, Herbrand's Theorem and Expansion Proofs
Ramakrishnan, C. R.	(ICLP) Constraint-Based Inference in Probabilistic Logic Programs
Raman, Vasumathi	(ADHS) Generating Dominant Strategies for Continuous Two-Player Zero-Sum Games
Ramanayake, Revantha	(TYDI) Sequentialising nested systems (EICNCL) Effective Translations between Display and Labelled Proofs for Tense Logics
Rambow, Thomas	(FM) Formal Verification of Automotive Simulink Controller Models: Empirical Technical Challenges, Evaluation and Recommendations (FM) Verifying Auto-Generated C Code from Simulink
Ramirez-Trevino, Antonio	(ADHS) Observability of Linear Hybrid Systems with Unknown Inputs and Discrete Dynamics Modeled by Petri Nets
Ramsdell, John	(FCS) Homomorphisms and Minimality for Enrich-by-Need Security Analysis
Randour, Mickael	(MoRe) Stochastic o-minimal hybrid systems
Ranzato, Francesco	(CAV) Program Analysis is Harder than Verification: A Computability Perspective
Rapp, Franziska	(IWC) Towards a Verified Decision Procedure for Confluence of Ground Term Rewrite Systems in Isabelle/HOL (IJCAR) FORT 2.0
Rasconi, Riccardo	(RCRA) Greedy Randomized Search for Scalable Compilation of Quantum Circuits
Raskin, Jean-Francois	(MoRe) Safe and Optimal Scheduling of Hard and Soft Tasks (MoRe) Parameterized complexity of games with monotonically ordered omega-regular objectives (MoRe) Constraint Problem for Weak Subgame Perfect Equilibria with omega-regular Boolean Objectives (LICS) Rational Synthesis Under Imperfect Information (SR) Beyond admissibility: Dominance between chains of strategies
Rasmussen, Cameron	(CAV) Understanding and Extending Incremental Determinization for 2QBF
Rasmussen, Cameron	(QBF) Understanding and Extending Incremental Determinization for 2QBF
Ratsch-Heitmann, Michel	(ICLP) Routing Driverless Transport Vehicles in Car Assembly with Answer Set Programming
Ravara, António	(DCM) Pointing to Private Names (HCVS) A simple functional presentation and an inductive correctness proof of the Horn algorithm
Rawson, Michael	(Vampire) Testing ATP folklore: a statistical analysis of Vampire proofs. (PAAR) Dynamic Strategy Priority: Empower the strong and abandon the weak
Ray, Rajarshi	(NSV) Parallel reachability analysis of hybrid systems in XSpeed
Razavi, Joseph	(DCM) A Category Theoretic Interpretation of Gandy’s Principles for Mechanisms
Real, Livy	(NLCS) Graph Knowledge Representations for SICK (NLCS) OpenWordNet-PT: Taking Stock
Reale, Kristian	(LPOP) Role-Based Access Control via JASP (LPOP) Invited Talk: On the Development of Industrial Applications with ASP
Rebola-Pardo, Adrian	(IJCAR) Extended Resolution Simulates DRAT (POS) Two flavors of DRAT
Reeves, Steve	(F-IDE) Integrating user design and formal models within PVSio-Web
Reger, Giles	(ARQNL) Going Beyond First-Order Logic with Vampire (SMT) What is the Point of an SMT-LIB Problem? (Vampire) Vampire: where have we come from, where are we going (Vampire) Giving AVATAR Quantifiers to Play With (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 (PAAR) Set of Support for Higher-Order Reasoning (PAAR) Dynamic Strategy Priority: Empower the strong and abandon the weak
Reimer, Sven	(SAT) Dynamic Polynomial Watchdog Encoding for Solving Weighted MaxSAT
Reimer, Sven	(QBF) Preprocessing for (D)QBF
Reis, Giselle	(WiL) Towards a Playground for Logicians (Linearity/TLLA) Formalization of Automated Trading Systems in a Concurrent Linear Framework (Linearity/TLLA) Benchmarking Linear Logic Translations
Reitwiessner, Christian	(SMT) SMT-based Compile-time Verification of Safety Properties for Smart Contracts
Remy, Didier	(MSFP) Ornamentation put into practice in ML
Ren, Hao	(F-IDE) The CLEAR Way To Transparent Formal Methods
Resch, Stefan	(TLA) Applying TLA+ in a Safety-Critical Railway Project
Retoré, Christian	(NLCS) Do different syntactic trees yield different logical readings? Some remarks on head variables in typed lambda calculus.
Rety, Pierre	(FSCD) Confluence of Prefix-Constrained Rewrite Systems
Reynier, Pierre-Alain	(FM) Optimal and Robust Controller Synthesis Using Energy Timed Automata with Uncertainty
Reynolds, Andrew	(CAV) Solving Quantified Bit-Vectors using Invertibility Conditions (SMT) Revisiting Enumerative Instantiation (SMT) Higher-Order SMT Solving (SMT) Rewrites for SMT Solvers using Syntax-Guided Enumeration (Vampire) Giving AVATAR Quantifiers to Play With (Vampire) Counterexample-Guided Quantifier Instantiation in Logical Theories (IJCAR) Datatypes with Shared Selectors (NSV) Towards Enumerative Invariant Synthesis in SMT Solvers
Riba, Colin	(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
Ribeiro, Pedro	(VaVAS) RoboTool: Modelling and Verification with RoboChart
Ricca, Francesco	(LPOP) Role-Based Access Control via JASP (LPOP) Invited Talk: On the Development of Industrial Applications with ASP (RCRA) Externally Supported Models for Efficient Computation of Paracoherent Answer Sets
Riccobene, Elvinia	(F-IDE) AsmetaF: a flattener for the ASMETA framework
Riehl, Emily	(HDRA) Homotopy coherent adjunctions and other structures
Riener, Martin	(SMT) What is the Point of an SMT-LIB Problem? (Vampire) Experimenting with Theory Instantiation in Vampire
Rieu-Helft, Raphaël	(IJCAR) A Why3 framework for reflection proofs and its application to GMP's algorithms
Rigau, German	(Vampire) Towards Word Sense Disambiguation by Reasoning
Rijke, Egbert	(LICS) Higher Groups in Homotopy Type Theory
Ringeissen, Christophe	(UNIF) Knowledge Problems in Equational Extensions of Subterm Convergent Theories
Ritirc, Daniela	(SCSC) RP: A Practical Polynomial Calculus for Arithmetic Circuit Verification
Rivas, Exequiel	(MSFP) Relating Idioms, Arrows and Monads from Monoidal Adjunctions
Rivière, Cédric	(MoRe) Stochastic o-minimal hybrid systems
Rizkallah, Christine	(ITP) A Formal Equational Theory for Call-by-Push-Value
Robere, Robert	(CAV) The Proof Complexity of SMT Solvers
Roberts, Hannah	(SAT) XORSAT Set Membership Filters
Robillard, Simon	(Vampire) Foundations of SPECTRE (IJCAR) Superposition with Datatypes and Codatatypes
Rocha, Ricardo	(ICLP) Improving Candidate Quality of Probabilistic Logic Models
Rodin, Andrei	(HoTT/UF) Univalent Foundations and the Constructive View of Theories
Rodrigues, Nishant	(CSF) KEVM: A Complete Formal Semantics of the Ethereum Virtual Machine
Rodriguez, Cesar	(CAV) Quasi-Optimal Partial Order Reduction (FM) Dynamic Symbolic Verification of MPI Programs
Roeck, Franz	(CAV) A Counting Semantics for Monitoring LTL Specifications over Finite Traces
Rohan, Thakker	(ADHS) Temporal Logic Control of POMDPs Via Label-Based Stochastic Simulation Relations
Romica, Trandafir	(VEMDP) Computational Approaches for the Programmed Assembly of Nanocellulose Meshes
Ronchi Della Rocca, Simona	(ITRS) Strong normalization of simple types through uniform intersection types.
Rondogiannis, Panos	(ICLP) Approximation Fixpoint Theory and the Well-Founded Semantics of Higher-Order Logic Programs
Roohi, Nima	(ADHS) Statistical Verification of PCTL Using Stratified Samples
Roscoe, Timothy	(ITP) Physical Addressing on Real Hardware in Isabelle/HOL
Rosenthal, Arnon	(FCS) An Expressive, Flexible and Uniform Logical Formalism for Attribute-based Access Control
Rossi, Francesca	(SoMLMFM) Ethically Aligned AI Systems
Rossmanith, Peter	(LaSh) Courcelle’s Theorem – A Game-Theoretic Approach
Rosu, Grigore	(FSCD) Formal Design, Implementation and Verification of Blockchain Languages (LFMTP) Invited talk: Why and How Does K work? The Logical Infrastructure Behind It (CSF) KEVM: A Complete Formal Semantics of the Ethereum Virtual Machine
Rothenberger, Ralf	(SAT) Sharpness of the Satisfiability Threshold for Non-Uniform Random k-SAT
Rouahi, Aouatef	(PRUV) Evidential Group Decision Making Model with Belief-Based Preferences
Rouhling, Damien	(Coq) Classical Analysis with Coq
Roveri, Marco	(SAT) Experimenting on Solving Nonlinear Integer Arithmetic with Incremental Linearization
Roversi, Luca	(Linearity/TLLA) Quantum programming made easy
Rowe, Reuben	(PARIS) Transitive Closure Logic: Infinitary and Cyclic Proof Systems (WiL) Non-well-founded proof system for Transitive Closure Logic
Roy, Dan	(FoPSS) Bayesian learning I (FoPSS) Bayesian learning II
Rozier, Kristin Yvonne	(CAV) SimpleCAR: An Efficient Bug-Finding Tool Based On Approximate Reachability
Rubin, Sasha	(SR) Verification of Multi-agent Systems with Imperfect Information and Public Actions (SR) Quantifying Bounds in Strategy Logic (SR) Strategy Logic with Imperfect Information
Rubio, Albert	(CAV) Constrained Dynamic Partial Order Reduction (FM) SDN-Actors: Modeling and Verification of SDN Programs
Ruchkin, Ivan	(FM) IPL: An Integration Property Language for Multi-Model Cyber-Physical Systems
Ruemmer, Philipp	(SMT) The next 10^4 UppSAT Approximations (IJCAR) Exploring Approximations for Floating-Point Arithmetic using UppSAT
Ruess, Harald	(FM) Evidential and Continuous Integration of Software Verification Tools (VSTTE) Verification of Binarized Neural Networks via Inter-Neuron Factoring
Runge, Mario	(ICLP) Routing Driverless Transport Vehicles in Car Assembly with Answer Set Programming
Ruoppolo, Domenico	(HOR) The next 700 (type-theoretical) denotational models ?
Russell, Stuart	(FLoC) Unifying Logic and Probability: the BLOG Language (SoMLMFM) Provably beneficial artificial intelligence (SoMLMFM) Panel session
Russo, Alessandra	(ICLP) Learning Commonsense Knowledge through Interactive Dialogue
Rutten, Jan	(COALG) The Method of Coalgebra: Exercises in Coinduction
Ryvchin, Vadim	(SAT) Chronological Backtracking
Régis-Gianas, Yann	(FM) Modular Verification of Programs with Effects and Effect Handlers in Coq
Röblitz, Susanna	(RCRA) Computing Personalised Treatments through In Silico Clinical Trials. A Case Study on Downregulation in Assisted Reproduction.
S
S, Krishna	(LICS) Regular Transducer Expressions for Regular Transformations over infinite words (LICS) Regular and First Order List Functions
Sa'Ar, Yaniv	(CAV) Synthesis Of Asynchronous Reactive Programs From Temporal Specifications
Sabel, David	(FSCD) Nominal Unification with Atom and Context Variables (WPTE) Automating the Diagram Method to Prove Correctness of Program Transformations
Sabuncu, Orkunt	(ICLP) Experimenting with robotic intra-logistics domains
Safranek, David	(PLR) Parallel Algorithms for Parameter Synthesis from Temporal Logic Specifications (VEMDP) Executable Biochemical Space for Specification and Analysis of Biochemical Systems
Sagiv, Mooly	(SAT) Constrained Image Generation Using Binarized Neural Networks with Decision Procedures
Sagr, Basma	(RCRA) An Enhanced Genetic Algorithm with the BLF2G Guillotine Placement Heuristic for the Orthogonal Cutting-Stock Problem
Sahlman, Lorenz	(CAV) Inner and Outer Approximating Flowpipes for Delay Differential Equations
Sakama, Chiaki	(ASPOCP) Partial Evaluation of Logic Programs in Vector Spaces
Salazar, Elmer	(ICLP) Constraint Answer Set Programming without Grounding
Salvo, Ivano	(RCRA) Computing Personalised Treatments through In Silico Clinical Trials. A Case Study on Downregulation in Assisted Reproduction.
Sammartino, Matteo	(FM) SDN-Actors: Modeling and Verification of SDN Programs
Sampath, Mohasha Isuru	(ADHS) Multi-Energy Scheduling Using a Hybrid Systems Approach
Sanan, David	(FM) Compositional Reasoning for Shared-variable Concurrent Programs
Sanchez, Cesar	(FM) Timed Epistemic Knowledge Bases for Social Networks
Sanders, Peter	(VSTTE) Relational Equivalence Proofs Between Imperative and MapReduce Algorithms
Sanfelice, Ricardo	(ADHS) Sufficient Conditions for Temporal Logic Specifications in Hybrid Dynamical Systems
Sangiorgi, Davide	(LICS) Eager Functions as Processes
Sangiovanni-Vincentelli, Alberto	(ADHS) Generating Dominant Strategies for Continuous Two-Player Zero-Sum Games
Sankaranarayanan, Sriram	(ADHS) Learning and Verification of Feedback Control Systems Using Feedforward Neural Networks
Sankur, Ocan	(LICS) Stochastic Shortest Paths and Weight-Bounded Properties in Markov Decision Processes
Sannella, Don	(LCC) Memories of Martin
Santhanam, Rahul	(SAT) Modelling SAT
Santolucito, Mark	(SYNT) Programming by example: efficient, but not “helpful”
Santucci, Valentino	(RCRA) Algebraic Crossover Operators for Permutations
Saoud, Adnane	(ADHS) Symbolic Models for Incrementally Stable Switched Systems with Aperiodic Time Sampling
Sarac, N Ege	(LICS) A Theory of Register Monitors
Saribatur, Zeynep G.	(ASPOCP) Towards Abstraction in ASP with an Application on Reasoning about Agent Policies
Sasse, Ralf	(CSF) Automated Unbounded Verification of Stateful Cryptographic Protocols with Exclusive OR
Satake, Yuki	(CAV) Propositional Dynamic Logic for Higher-Order Functional Programs
Sato, Genki	(HoTT/UF) Geometric realization of truncated semi-simplicial sets meta-constructed within HoTT
Sato, Naoto	(VaVAS) Policing Functions for Machine Learning Systems
Sato, Taisuke	(ASPOCP) Partial Evaluation of Logic Programs in Vector Spaces
Saurin, Alexis	(PARIS) Workshop introduction
Saxena, Aseem	(SAT) Effective use of SMT solvers for Program Equivalence Checking through Invariant Sketching and Query Decomposition
Saxena, Manasvi	(CSF) KEVM: A Complete Formal Semantics of the Ethereum Virtual Machine
Scedrov, Andre	(IJCAR) A Logical Framework with Commutative and Non-Commutative Subexponentials (FCS) Statistical Model Checking of Guessing and Timing Attacks on Distance-bounding Protocols
Schachte, Peter	(ICLP) An iterative approach to precondition inference using constrained Horn clauses
Schaefer, Ina	(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
Schalk, Andrea	(DCM) A Category Theoretic Interpretation of Gandy’s Principles for Mechanisms
Schanda, Florian	(SMT) Building Better Bit-Blasting for Floating-Point Problems
Schaub, Torsten	(LPOP) How to upgrade ASP for true dynamic modelling and solving? (ASPOCP) anthem: Transforming gringo Programs into First-Order Theories (Preliminary Report) (ICLP) Routing Driverless Transport Vehicles in Car Assembly with Answer Set Programming (ICLP) Experimenting with robotic intra-logistics domains (ICLP) Temporal Answer Set Programming on Finite Traces
Scheftelowitsch, Dimitri	(MoRe) Multi-Scenario Uncertainty in Markov Decision Processes
Schemmel, Daniel	(CAV) Symbolic Liveness Analysis of Real-World Software
Scherer, Gabriel	(LMW) Asking questions to yourself and others
Schindler, Tanja	(SMT) Selfless Interpolation for Infinite-State Model Checking (IJCAR) Efficient Interpolation for the Theory of Arrays
Schlaipfer, Matthias	(PAAR) Efficient translation of sequent calculus proofs into natural deduction proofs
Schlichtkrull, Anders	(UNIF) Formalization of First-Order Syntactic Unification (ARQNL) Formalization of a Paraconsistent Infinite-Valued Logic (ThEdu) Students' Proof Assistant (SPA) (ThEdu) Natural Deduction Assistant (NaDeA) (Isabelle) Substitutionless First-Order Logic: A Formal Soundness Proof (PAAR) A Verified Simple Prover for First-Order Logic (IJCAR) Formalizing Bachmair and Ganzinger's Ordered Resolution Prover (UITP) Drawing Trees
Schmerl, Bradley	(FM) IPL: An Integration Property Language for Multi-Model Cyber-Physical Systems
Schmid, Lara	(CSF) Alethea: A Provably Secure Random Sample Voting Protocol
Schmid, Ulrich	(ADHS) Verifying nonlinear analog and mixed-signal circuits with inputs
Schmidt, Renate A.	(IJCAR) FAME: An Automated Tool for Semantic Forgetting in Expressive Description Logics
Schmidt-Schauss, Manfred	(FSCD) Nominal Unification with Atom and Context Variables (UNIF) Rewriting with Generalized Nominal Unification (WPTE) Optimizing Space of Parallel Processes
Schneider, Gerardo	(FM) Timed Epistemic Knowledge Bases for Social Networks
Schneider, Joshua	(ITP) Relational Parametricity and Quotient Preservation for Modular (Co)Datatypes
Schneider, Klaus	(ICLP) Optimal Scheduling for Exposed Datapath Architectures with Buffered Processing Units by ASP
Schneider, Valentin	(TLA) Modeling Virtual Machines and Interrupts in TLA+ & PlusCal
Schneidewind, Clara	(CAV) Foundations and Techniques for the Static Analysis of Ethereum Smart Contracts
Schnepf, Nicolas	(AVOCS) Rule-Based Synthesis of Chains of Security Functions for Software-Defined Networks
Scholl, Christoph	(SAT) Dependency Quantified Boolean Formulas: An Overview of Solution Methods and Applications
Scholl, Christoph	(QBF) Preprocessing for (D)QBF
Schrammel, Peter	(CAV) JBMC: A Bounded Model Checking Tool for Verifying Java Bytecode (WST) Procedure-Modular Termination Analysis
Schrijvers, Tom	(LICS) Syntax and Semantics for Operations with Scopes (ITP) Formalization of a Polymorphic Subtyping Algorithm
Schröder, Lutz	(LICS) A van Benthem Theorem for Fuzzy Modal Logic
Schubert, Aleksy	(VSTTE) A Java bytecode formalisation (ICLP) First-order answer set programming as constructive proof search
Schuhmann, Anna	(ICLP) Temporal Answer Set Programming on Finite Traces
Schultz, William	(TLA) An Animation Module for TLA+
Schulz, Stephan	(ITP) ProofWatch: Watchlist Guidance for Large Theories in E
Schulze, Uwe	(FM) Model-Based Testing for Avionics Systems
Schupp, Sibylle	(VSTTE) Constructing Independently Verifiable Privacy-Compliant Type Systems for Message Passing between Black-Box Components
Schwartz-Narbonne, Daniel	(VSTTE) SideTrail: Verifying Time-Balancing of Cryptosystems
Schwarzentruber, Francois	(GraMSec) Deciding the Non-Emptiness of Attack trees
Schwitter, Rolf	(ICLP) Specifying and Verbalising Answer Set Programs in Controlled Natural Language
Schöpf, Jonas	(WST) TTT2 with Termination Templates for Teaching (ITP) A Formally Verified Solver for Homogeneous Linear Diophantine Equations
Scialanca, Agostino	(RCRA) Optimal Fault-Tolerant Placement of Relay Nodes in a Mission Critical Wireless Network
Sciarappa, Luke	(LICS) Computable decision making on the reals and other spaces via partiality and nondeterminism
Scott, Dana	(LICS) Boolean-Valued Semantics for Stochastic Lambda-Calculus (Domains13) Invited Talk: Looking Backward; Looking Forward
Seatzu, Carla	(ADHS) Tracking Control via Variable-gain Integrator and Lookahead Simulation: Application to Leader-follower Multiagent Networks
Sebastiani, Roberto	(SAT) Experimenting on Solving Nonlinear Integer Arithmetic with Incremental Linearization
Sedwards, Sean	(ADHS) Bounding Errors Due to Switching Delays in Incrementally Stable Switched Systems
Seidl, Helmut	(CSF) Inductive Invariants for Noninterference in Multi-agent Workflows
Seidl, Martina	(QBF) The Symmetry Rule for Quantified Boolean Formulas (SAT) Symmetries for QBF (SAT) QBFEVAL’18
Seidl, Martina	(QBF) Discussion
Seiller, Thomas	(Linearity/TLLA) A semantic conjecture on second-order MLL and its complexity consequences (work in progress) (Linearity/TLLA) Entropy and Complexity Lower Bounds (Linearity/TLLA) Coherent interaction graphs: a nondeterministic geometry of interaction for MLL
Sekanina, Lukas	(CAV) ADAC: Automated Design of Approximate Circuits
Sekerinski, Emil	(F-IDE) A Notebook Format for the Holistic Design of Embedded Systems (REFINE) Refining Santa: An Excercise in Efficient Synchronization
Selinger, Peter	(FSCD) Challenges in quantum programming languages
Sellami, Yanis	(IJCAR) A Generic Framework for Implicate Generation Modulo Theories
Sellis, Timos	(ICLP) A Trajectory Calculus for Qualitative Spatial Reasoning Using Answer Set Programming
Serban, Cristina	(AVOCS) An Entailment Checker for Separation Logic with Inductive Definitions
Servetto, Marco	(DCM) A syntactic model of mutation and aliasing
Seshia, Sanjit	(ADHS) Generating Dominant Strategies for Continuous Two-Player Zero-Sum Games
Seshia, Sanjit A.	(CAV) Reactive Control Improvisation (CAV) Understanding and Extending Incremental Determinization for 2QBF (ReMOTE) Specification and Verification for Robots that Learn
Seshia, Sanjit A.	(QBF) Understanding and Extending Incremental Determinization for 2QBF
Shah, Rohin	(SYNT) Scalable Synthesis with Symbolic Syntax Graphs
Shah, Shetal	(CAV) What’s hard about Boolean Functional Synthesis?
Shakerin, Farhad	(ICLP) Cumulative Scoring-based Induction of Default Theories
Shankar, Natarajan	(SMT) Proofs in conflict-driven theory combination (VDMW) Computation and inference (Tetrapod) Modularity in Proof Assistants
Sharaf, Nada	(ICLP) CHRvis: Syntax and Semantics
Sharma, Subodh	(FM) Dynamic Symbolic Verification of MPI Programs
Sharygina, Natasha	(VSTTE) Lattice-Based Refinement in Bounded Model Checking
Shasha, Dennis	(ADSL) Automating the Flow Framework
Shaulian, Yariv	(LICS) Automaton-Based Criteria for Membership in CTL
Shen, Da	(ICLP) SMT-based Answer Set Solver CMODELS(DIFF) (System Description)
Sherman, Benjamin	(LICS) Computable decision making on the reals and other spaces via partiality and nondeterminism
Shimi, Adam	(FRIDA) From Asynchronous Message-Passing Models To Rounds
Shintani, Kiraku	(FSCD) Confluence Competition 2018
Shkapsky, Alex	(ICLP) Declarative Algorithms in Datalog with Aggregates: user-friendly formal semantics conducive to performance and scalability
Shoham, Sharon	(SMT) Discovering Universally Quantified Solutions for Constrained Horn Clauses (VDMW) Verification of infinite-state systems using decidable logic
Shumailov, Ilia	(GraMSec) Tendrils of Crime: Visualizing the Diffusion of Stolen Bitcoins
Si, Xujie	(MLP) Difflog: Beyond Deductive Methods in Program Analysis
Sickert, Salomon	(CAV) Rabinizer 4: From LTL to Your Favourite Deterministic Automaton (CAV) Strix: Explicit Reactive Synthesis Strikes Back! (LICS) One Theorem to Rule Them All: A Unified Translation of LTL into ω-Automata
Siebertz, Sebastian	(LICS) On the number of types in sparse graphs (LICS) Parameterized circuit complexity of model-checking on sparse structures
Siek, Jeremy	(UNIF) Efficiency of a good but not linear nominal unification algorithm
Siekmann, Joerg	(UNIF) Unification based on generalized embedding
Sighireanu, Mihaela	(ADSL) Presentation of Results from SL-COMP 2018
Silva, Alexandra	(FM) SDN-Actors: Modeling and Verification of SDN Programs
Simari, Gerardo	(PRUV) Leveraging Probabilistic Existential Rules for Adversarial Deduplication
Simon, Laurent	(POS) Seeking Practical CDCL Insights from Theoretical SAT Benchmarks
Simpson, Alex	(CL&C) Sheaf models of classical logic extended by independence relations
Singh, Badal	(MLP) Deep Learning On Code with an Unbounded Vocabulary
Singh, Gagandeep	(CAV) Fast Numerical Program Analysis with Reinforcement Learning
Singh, Rishabh	(MLP) Neural Meta Program Synthesis
Singh, Vasu	(SoMLMFM) Panel session
Sinisi, Stefano	(RCRA) Computing Personalised Treatments through In Silico Clinical Trials. A Case Study on Downregulation in Assisted Reproduction.
Sinz, Carsten	(POS) A Problem Meta-Data Library for Research in SAT
Sistla, Prasad	(CAV) Model checking indistinguishability of randomized security protocols
Skočovský, Peter	(IJCAR) Enumerating Justifications using Resolution
Slavnov, Konstantin	(MLP) Splitting source code identifiers using Bidirectional LSTM Recurrent Neural Network
Slivovsky, Friedrich	(QBF) Portfolio-Based Algorithm Selection for Circuit QBFs (QBF) Qute (QBFEval'18 Contribution) (SAT) Polynomial-Time Validation of QCDCL Certificates
Smallbone, Nicholas	(IJCAR) Efficient encodings of first-order Horn formulas in equational logic
Smith, Connor	(HOR) Orthogonality and sequentiality in substructural Linear HRSs
Smith, Douglas	(Tetrapod) Modularity in Software Synthesis
Smith, Graeme	(FM) A wide-spectrum language for verification of programs on weak memory models (REFINE) Correctness of Concurrent Objects under Weak Memory Models
Smith, Michael	(SAT) XORSAT Set Membership Filters
Smolka, Gert	(ITP) Verification of PCP-Related Computational Reductions in Coq
Smolka, Scott	(VaVAS) Work-in-Progress: Adaptive Neighborhood Resizing for Stochastic Reachability in Distributed Flocking
Smt-Comp Organizers,	(SMT) SMT-COMP 2018 Report (SYNT) Maximum Realizability for Linear Temporal Logic Specifications (VSTTE) Synthesis of Surveillance Strategies for Mobile Sensors
Sobocinski, Pawel	(LICS) Rewriting with Frobenius
Sofronie-Stokkermans, Viorica	(SYNT) On Inductive Verification and Synthesis
Sogokon, Andrew	(FM) Vector Barrier Certificates and Comparison Systems
Sojakova, Kristina	(LICS) A General Framework for Relational Parametricity
Sokolova, Ana	(COALG) Coalgebra meets Convexity in Probabilistic Systems
Solar-Lezama, Armando	(CAV) Delta-Decision Procedures for Exists-Forall Problems over the Reals
Soloveichik, David	(VEMDP) Computing properties of stable configurations of thermodynamic binding networks
Son, Tran	(ICLP) Phylotastic: An Experiment in Creating, Manipulating, and Evolving Phylogenetic Biology Workflows Using Logic Programming (ICLP) Experimenting with robotic intra-logistics domains (ICLP) Natural Language Generation From Ontologies: Application Paper
Sondergaard, Harald	(ICLP) An iterative approach to precondition inference using constrained Horn clauses
Song, Fu	(CAV) SCInfer: Refinement-based Verification of Software Countermeasures against Side-Channel Attacks (CAV) Android Stack Systems
Soria Dustmann, Oscar	(CAV) Symbolic Liveness Analysis of Real-World Software
Sorrentino, Loredana	(PLR) An Efficient Zielonka's Algorithm for Parallel Parity Games
Soudjani, Sadegh	(ADHS) Compositional Synthesis of Finite Abstractions for Continuous-Space Stochastic Control Systems: A Small-Gain Approach
Soudjani, Sadegh	(ADHS) Temporal Logic Control of General Markov Decision Processes by Approximate Policy Refinement
Soulat, Romain	(AVOCS) Climbing the Software Assurance Ladder - Practical Formal Verification for Reliable Software
Sousa, Marcelo	(CAV) Quasi-Optimal Partial Order Reduction
Sozeau, Matthieu	(FSCD) Cumulative Inductive Types in Coq (Coq) Towards a formalization of the guard condition (ITP) Towards Certified Meta-Programming with Typed Template-Coq
Spaccasassi, Carlo	(VEMDP) Rule-based design of computational DNA devices
Speight, Sam	(LICS) Impredicative Encodings of (Higher) Inductive Types
Spencer, Frankie	(VEMDP) Computational Approaches for the Programmed Assembly of Nanocellulose Meshes
Spitters, Bas	(FSCD) Internal Universes in Models of Homotopy Type Theory (HoTT/UF) Dependent Right Adjoint Types (CSF) Computer-aided proofs for multiparty computation with active security
Spoto, Fausto	(IJCAR) Checking Array Bounds by Abstract Interpretation and Symbolic Expressions
Srba, Jiri	(MoRe) Comfort and Energy Optimization for Floor Heating Systems (CAV) Start Pruning When Time Gets Urgent: Partial Order Reduction for Timed Systems
Stadler, Peter F.	(VEMDP) Rule-Based Gillespie Simulation of Chemical Systems
Stasch, Matthias	(SCSC) EA: Constraint Systems from Traffic Scenarios for the Validation of Autonomous Driving
Statman, Richard	(HDRA) Minimal Bacus FP is Turing Complete
Staton, Sam	(Domains13) Diffeological Spaces and Semantics for Differential Programming
Steen, Alexander	(ARQNL) System Demonstration: The Higher-Order Prover Leo-III (IJCAR) The Higher-Order Prover Leo-III
Steeples, Thomas	(SR) Local Equilibria in Logic-Based Multi-Player Games
Stefanesco, Léo	(LICS) An Asynchronous Soundness Theorem for Concurrent Separation Logic
Stefanescu, Andrei	(CSF) KEVM: A Complete Formal Semantics of the Ethereum Virtual Machine
Steffen, Martin	(FM) Operational Semantics of a Weak Memory Model with Channel Synchronization
Steinberg, Florian	(LICS) Type-two polynomial-time and restricted lookahead.
Steinfeld, Aaron	(ReMOTE) Trust, Failure, and Self-Assessment During Human-Robot Interaction
Stenger, Marvin	(CAV) Synthesizing Reactive Systems from Hyperproperties
Sterling, Jonathan	(LICS) Guarded Computational Type Theory (HoTT/UF) Cubical Computational Type Theory
Sterling, Mark	(UITP) Automated Theorem Proving in a Chat Environment
Sternagel, Christian	(IWC) Certified Ordered Completion (Isabelle) The remote_build Tool (WST) TTT2 with Termination Templates for Teaching (ITP) A Formally Verified Solver for Homogeneous Linear Diophantine Equations
Stevens, Perdita	(WiL) Logic and Software Engineering: Are We Nearly There Yet?
Stock, Benedikt	(Isabelle) Hilbert Meets Isabelle: Formalisation of the DPRM Theorem in Isabelle
Stoilkovska, Ilina	(FRIDA) Parameterized Model Checking of Synchronous Distributed Algorithms by Abstraction
Stojic, Ivan	(FM) Formal Specification and Verification of Dynamic Parametrized Architectures
Stoller, Scott	(LPOP) Easier Rules and Constraints for Programming (TLA) Invariants in Distributed Algorithms
Stolz, Volker	(FM) Operational Semantics of a Weak Memory Model with Channel Synchronization
Stoop, Pascal	(Isabelle) Lazy Algebraic Types in Isabelle/HOL
Stratulat, Sorin	(PARIS) Useless Explicit Induction Reasoning (CL&C) Validating Back-links of FOL-ID Cyclic Pre-proofs
Straubing, Howard	(LICS) Wreath Products of Distributive Forest Algebras
Straßburger, Lutz	(WiL) Decomposing labelled proof theory for intuitionistic modal logic (IJCAR) From Syntactic Proofs to Combinatorial Proofs
Strub, Pierre-Yves	(Coq) Classical Analysis with Coq (CSF) Computer-aided proofs for multiparty computation with active security
Stuckey, Peter J.	(POS) Local-Style Search in the Linear MaxSAT Algorithm: A Computational Study of Solution-Based Phase Saving (ICLP) An iterative approach to precondition inference using constrained Horn clauses
Stulova, Nataliia	(ICLP) Towards Static Performance Guarantees for Programs with Run-time Checks
Stump, Aaron	(ITP) Efficient Mendler-Style Lambda-Encodings in Cedille (CL&C) Towards a Dualized Sequent Calculus with Canonicity
Sturm, Thomas	(SCSC) EA: Wrapping Computer Algebra is Surprisingly Successful for Non-Linear SMT
Stéphan, Igor	(ICLP) A New Proof-theoretical Linear Semantics for CHR
Subramanyan, Pramod	(CAV) Lazy Self-Composition for Security Verification
Suda, Martin	(Vampire) Giving AVATAR Quantifiers to Play With (QBF) Towards the Semantics of QBF Clauses (SAT) Local Soundness for QBF Calculi (SAT) SAT Competition 2018
Summers, Alexander J	(CAV) Permission Inference for Array Programs (PLR) Permission Inference for Array Programs
Sun, Jun	(FM) Compositional Reasoning for Shared-variable Concurrent Programs (FM) Towards `Verifying' a Water Treatment System
Sun, Youcheng	(SMT) Building Better Bit-Blasting for Floating-Point Problems
Sunshine, Joshua	(FM) IPL: An Integration Property Language for Multi-Model Cyber-Physical Systems
Sutcliffe, Geoff	(PAAR) TFX: The TPTP Extended Typed First-order Form (IJCAR) IJCAR competition presentations
Swierstra, Wouter	(ITP) Verified Timing Transformations in Synchronous Circuits with LambdaPi-Ware
Syed Mohammad, Meesum	(SCSC) RP: Unknot Recognition Through Quantifier Elimination
Syeda, Hira	(ITP) Program Verification in the Presence of Cached Address Translation
Symeonidou, Ioanna	(ICLP) Approximation Fixpoint Theory and the Well-Founded Semantics of Higher-Order Logic Programs
Szabo, Peter	(UNIF) Unification based on generalized embedding
Szasz, Nora	(LFMTP) Formalisation of Barendregt's Variable Convention for Generic Structures with Binders (LFMTP) Formalization in Constructive Type Theory of the Standardization Theorem
Szegedy, Christian	(SoMLMFM) Deep Learning Methods for Large Scale Theorem Proving
Szeider, Stefan	(QBF) Portfolio-Based Algorithm Selection for Circuit QBFs (SAT) Polynomial-Time Validation of QCDCL Certificates
T
Tabareau, Nicolas	(ITP) Towards Certified Meta-Programming with Typed Template-Coq
Tabuada, Paulo	(ADHS) Computing Controlled Invariant Sets for Hybrid Systems with Applications to Model-Predictive Control
Tacchella, Armando	(SAT) Constrained Image Generation Using Binarized Neural Networks with Decision Procedures
Tachmazidis, Ilias	(ICLP) A Trajectory Calculus for Qualitative Spatial Reasoning Using Answer Set Programming
Takahashi, Yuta	(TERMGRAPH) On quasi ordinal diagram systems
Talcott, Carolyn	(LSB) Pathway Logic: Symbolic executable models for reasoning about cellular processes (FCS) Statistical Model Checking of Guessing and Timing Attacks on Distance-bounding Protocols
Talebanfard, Navid	(SAT) Cops-Robber games and the resolution of Tseitin formulas
Talvik, Tõnn	(LOLA) Experimenting with graded monads: certified grading-based program transformations
Tamaroff, Pedro	(HDRA) Minimal models for monomial algebras
Tan, Yong Kiam	(FM) Vector Barrier Certificates and Comparison Systems (LICS) Differential Equation Axiomatization: The Impressive Power of Differential Ghosts (IJCAR) Proof-Producing Synthesis of CakeML with I/O and Local State from Monadic HOL Functions
Tanaka, Ribeka	(NLCS) Paychecks, Presupposition, and Dependent Types
Tang, Qiyi	(CAV) Deciding Probabilistic Bisimilarity Distance One for Labelled Markov Chains
Tannen, Val	(LICS) Provenance Analysis for First-order Model Checking
Tarau, Paul	(RCRA) Shaving with Occam's Razor: Deriving Minimalist Theorem Provers for Minimal Logic
Tarlow, Danny	(MLP) Neural Network Models of Code Edits
Tasiran, Serdar	(CAV) Reasoning About TSO Programs Using Reduction and Abstraction (CAV) Continuous formal verification of Amazon s2n (CAV) Model Checking Boot Code from AWS Data Centers (VSTTE) Practical Methods for Reasoning about Java 8's Functional Programming Features (VSTTE) SideTrail: Verifying Time-Balancing of Cryptosystems
Tasistro, Alvaro	(LFMTP) Formalisation of Barendregt's Variable Convention for Generic Structures with Binders (LFMTP) Formalization in Constructive Type Theory of the Standardization Theorem
Tassarotti, Joseph	(ITP) Verified Tail Bounds for Randomized Programs
Tatlock, Zachary	(FM) Combining Tools for Optimization and Analysis of Floating-Point Computations (Coq) Verifying Distributed Systems (ITP) Software Verification with ITPs Should Use Binary Code Extraction to Reduce the TCB (Short Paper)
Tatsuta, Makoto	(ADSL) Cyclic Theorem Prover for Separation Logic by Magic Wand
Taupe, Richard	(ICLP-DC) Speeding Up Lazy-Grounding Answer Set Solving
Tautschnig, Michael	(CAV) Model Checking Boot Code from AWS Data Centers (AVOCS) Formal Methods at Amazon Web Services
Tba, N.N.	(IFIP WG 1.6) Report on ISR
Tbd, Tbd	(ICLP) TEST OF TIME 10
Tbd, Tbd	(ICLP) Best DC Paper
Tbd, Tbd	(ICLP) Test of time 20
Teige, Tino	(SCSC) EA: Constraint Systems from Traffic Scenarios for the Validation of Autonomous Driving
Teixeira, Andre	(GraMSec) Combining Bayesian Networks and Fishbone Diagrams to Distinguish between Intentional Attacks and Accidental Technical Failures
Tentrup, Leander	(CAV) Synthesizing Reactive Systems from Hyperproperties (CAV) Understanding and Extending Incremental Determinization for 2QBF (SYNT) On the Expressiveness of HyperLTL Synthesis
Tentrup, Leander	(QBF) Understanding and Extending Incremental Determinization for 2QBF
Ter Beek, Maurice H.	(FM) QFLan: A Tool for the Quantitative Analysis of Highly Reconfigurable Systems
Terauchi, Tachio	(LICS) A Fixpoint Logic and Dependent Effects for Temporal Property Verification
Ternovska, Eugenia	(LaSh) A Logic of Information Flows (PRUV) A Model-Theoretic View on Preferences in Declarative Specifications of Search Problems
Thachuk, Chris	(VEMDP) Computing properties of stable configurations of thermodynamic binding networks
Thakkar, Aalok	(WST) Verification of Rewriting-based Query Optimizers
Theodoropoulos, Panos	(SAT) Fast Sampling of Perfectly Uniform Satisfying Assignments (SAT) Fast and Flexible Probabilistic Model Counting
Thibodeau, David	(FSCD) Index-Stratified Types
Thiemann, René	(Isabelle) Formal Verification of Bounds for the LLL Basis Reduction Algorithm (WST) A Perron-Frobenius Theorem for Jordan Blocks for Complexity Proving (ITP) A Formalization of the LLL Basis Reduction Algorithm
Thiery, Nicolas	(Tetrapod) Modularity in Mathematical Computation
Thiré, François	(LFMTP) Sharing a library between proof assistants: reaching out to the HOL family
Thomas, Ciza	(SAT) Machine Learning-based Restart Policy for CDCL SAT Solvers
Thule, Casper	(Overture) Overture FMU: Export VDM-RT Models as Tool-Wrapper FMUs
Thüm, Thomas	(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
Tien Luong, An Thuy	(UITP) Adding Text-Based Interaction to a Direct-Manipulation Interface for Program Verification -- Lessons Learned
Timany, Amin	(FSCD) Cumulative Inductive Types in Coq
Timmis, Jon	(VaVAS) RoboTool: Modelling and Verification with RoboChart
Tinelli, Cesare	(CAV) Solving Quantified Bit-Vectors using Invertibility Conditions (SMT) Higher-Order SMT Solving (SMT) Rewrites for SMT Solvers using Syntax-Guided Enumeration (Vampire) Counterexample-Guided Quantifier Instantiation in Logical Theories (IJCAR) Datatypes with Shared Selectors (VSTTE) Contract-based Compositional Verification of Infinite-State Reactive Systems
Titolo, Laura	(FM) A Formally Verified Floating-Point Implementation of the Compact Position Reporting Algorithm
Tiu, Alwen	(FM) Compositional Reasoning for Shared-variable Concurrent Programs (GraMSec) The Attacker Does not Always Hold the Initiative: Attack Trees with External Refinement (LICS) Quasi-Open Bisimilarity with Mismatch is Intuitionistic (CSF) A Permission-Dependent Type System for Secure Information Flow Analysis (EICNCL) Effective Translations between Display and Labelled Proofs for Tense Logics
Tiwari, Ashish	(VaVAS) Work-in-Progress: Adaptive Neighborhood Resizing for Stochastic Reachability in Distributed Flocking
Tiwari, Ashish	(ADHS) Learning and Verification of Feedback Control Systems Using Feedforward Neural Networks
To, Van Khanh	(SCSC) EA: Wrapping Computer Algebra is Surprisingly Successful for Non-Linear SMT
Tobalina Segura, Luis	(LSB) A logic modelling workflow for systems pharmacology
Todoran, Eneia Nicolae	(Domains13) Abstractness of Continuation Semantics for Asynchronous Concurrency
Toman, Viktor	(CAV) Symbolic Algorithms for Graphs and Markov Decision Processes with Fairness Objectives
Tomb, Aaron	(CAV) Formal Verification of a Vehicle-to-Vehicle (V2V) Messaging System (CAV) Continuous formal verification of Amazon s2n
Tonetta, Stefano	(FM) Formal Specification and Verification of Dynamic Parametrized Architectures
Tonks, Zak	(SCSC) RP: Non-linear Real Arithmetic Benchmarks derived from Automated Reasoning in Economics
Topcu, Ufuk	(SYNT) Maximum Realizability for Linear Temporal Logic Specifications
Topcu, Ufuk	(ADHS) Compositional Analysis of Hybrid Systems Defined Over Finite Alphabets
Toran, Jacobo	(SAT) Cops-Robber games and the resolution of Tseitin formulas
Torfah, Hazem	(CAV) Model Checking Quantitative Hyperproperties (rv4rise) Real-time Stream Processing with RTLola
Torrini, Paolo	(AVOCS) Proof-Oriented Design of a Separation Kernel with Minimal Trusted Computing Base (VSTTE) Formalising Executable Specifications of Low-Level Systems
Toruńczyk, Szymon	(LICS) On computability and tractability for infinite sets (LICS) On the number of types in sparse graphs (LICS) Parameterized circuit complexity of model-checking on sparse structures
Tourret, Sophie	(TERMGRAPH) SLD-Resolution Reduction of Second-Order Horn Fragments - Extended Abstract
Traonouez, Louis-Marie	(FM) Statistical Model Checking of LLVM Code
Traytel, Dmitriy	(LaSh) A Derivative-Based Decision Procedure for WS1S (IJCAR) Formalizing Bachmair and Ganzinger's Ordered Resolution Prover
Treinen, Ralf	(IJCAR) Deciding the First-Order Theory of an Algebra of Feature Trees with Updates
Trenn, Stephan	(ADHS) Switch induced instabilities for stable power system DAE models
Trieu, Alix	(FCS) A Study on the Preservation on Cryptographic Constant-Time Security in the CompCert Compiler
Troják, Matej	(VEMDP) Executable Biochemical Space for Specification and Analysis of Biochemical Systems
Tronci, Enrico	(RCRA) Computing Personalised Treatments through In Silico Clinical Trials. A Case Study on Downregulation in Assisted Reproduction. (RCRA) Optimal Fault-Tolerant Placement of Relay Nodes in a Mission Critical Wireless Network
Trtik, Marek	(CAV) JBMC: A Bounded Model Checking Tool for Verifying Java Bytecode
Tsai, Pei-Wei	(ICLP) A Trajectory Calculus for Qualitative Spatial Reasoning Using Answer Set Programming
Tsuiki, Hideki	(Domains13) T^\omega-representations of compact sets through dyadic subbases
Tsukada, Takeshi	(GS) Generalised Species of Plays (LICS) Species, Profunctors and Taylor Expansion Weighted by SMCC--A Unified Framework for Modelling Nondeterministic, Probabilistic and Quantum Programs--
Tsuruta, Yuta	(IWC) Convergence of Simultaneously and Sequentially Unraveled TRSs for Normal Conditional TRSs
Tullsen, Mark	(CAV) Formal Verification of a Vehicle-to-Vehicle (V2V) Messaging System
Tumova, Jana	(FM) Multi-Robot LTL Planning Under Uncertainty
Turberfield, Andrew	(VEMDP) Controlling Assembly and Function of DNA Nanostructures and Molecular Machinery
Turhan, Anni-Yasmin	(PRUV) Welcome to PRUV
Turuani, Mathieu	(CSF) A little more conversation, a little less action, a lot more satisfaction: Global states in ProVerif.
Tusa, Iris	(VEMDP) Computational Approaches for the Programmed Assembly of Nanocellulose Meshes
Tuttle, Mark R.	(CAV) Model Checking Boot Code from AWS Data Centers
Tzameret, Iddo	(PC) Resolution with Counting: Different Moduli and Tree-Like Lower Bounds
Tzevelekos, Nikos	(GS) Game Semantics 25 years on
Tóth, Tamás	(AVOCS) Backward reachability analysis for timed automata with data variables
U
Uemura, Taichi	(HoTT/UF) Cubical Assemblies and the Independence of the Propositional Resizing Axiom
Ulbrich, Mattias	(VSTTE) Relational Equivalence Proofs Between Imperative and MapReduce Algorithms
Ultes-Nitsche, Ulrich	(LICS) A Simple and Optimal Complementation Algorithm for Büchi Automata
Unno, Hiroshi	(CAV) Propositional Dynamic Logic for Higher-Order Functional Programs (LICS) A Fixpoint Logic and Dependent Effects for Temporal Property Verification (HCVS) Horn Clauses and Beyond for Relational and Temporal Program Verification
Urban, Caterina	(CAV) Permission Inference for Array Programs (CAV) MaxSMT-Based Type Inference for Python 3 (PLR) Permission Inference for Array Programs
Urban, Josef	(IJCAR) ATPboost: Learning Premise Selection in Binary Setting with ATP Feedback (ITP) ProofWatch: Watchlist Guidance for Large Theories in E
Urbani, Jacopo	(IJCAR) Efficient Model Construction for Horn Logic with VLog: System Description
Urzyczyn, Pawel	(ICLP) First-order answer set programming as constructive proof search
Uustalu, Tarmo	(LOLA) Experimenting with graded monads: certified grading-based program transformations
V
Vacher, Jonathan	(ADHS) Control Synthesis for Stochastic Switched Systems Using the Tamed Euler Method
Vafeiadis, Viktor	(ADSL) Weak memory made easy by separation logic (keynote)
Vallati, Mauro	(RCRA) On the Configuration of SAT Formulae
van Breugel, Franck	(CAV) Deciding Probabilistic Bisimilarity Distance One for Labelled Markov Chains
Van Den Bogaard, Marie	(SR) Beyond admissibility: Dominance between chains of strategies
van der Hallen, Matthias	(QBF) A Grounder From Second-Order Logic To QBF
van Dijk, Tom	(CAV) Attracting Tangles to Solve Parity Games (PLR) Using work-stealing to parallelize symbolic algorithms and parity game solvers
van Doorn, Floris	(LICS) Higher Groups in Homotopy Type Theory
van Gelder, Pieter	(GraMSec) Combining Bayesian Networks and Fishbone Diagrams to Distinguish between Intentional Attacks and Accidental Technical Failures
van Hasselt, Hado	(FoPSS) Reinforcement learning I (FoPSS) Reinforcement learning II
Van Roy, Peter	(LPOP) A software system should be declarative except where it interacts with the real world
Vandin, Andrea	(FM) QFLan: A Tool for the Quantitative Analysis of Highly Reconfigurable Systems
Vardi, Moshe	(CAV) Automata vs Linear-Programming Discounted-Sum Inclusion (SoMLMFM) Machine learning and logic: Fast and slow thinking (WiL) First-Order vs. Second-Order Encodings for LTLf-to-Automata Translation (LICS) Sequential Relational Decomposition (LICS) Constraints, Graphs, Algebra, Logic, and Complexity (SR) Strategy Logic with Imperfect Information (SR) Solving Parity Games: Explicit vs Symbolic
Vardi, Moshe	(CAV) SimpleCAR: An Efficient Bug-Finding Tool Based On Approximate Reachability
Varga, János	(TERMGRAPH) Finding the Transitive Closure of Functional Dependencies using Strategic Port Graph Rewriting
Varma, Vineeth Satheeskumar	(ADHS) Network-Aware Design of State-Feedback Controllers for Linear Wireless Networked Control Systems
Varma, Vineeth Satheeskumar	(ADHS) Space-Time Budget Allocation for Marketing Over Social Networks
Vasicek, Zdenek	(CAV) ADAC: Automated Design of Approximate Circuits
Vasile, Cristian-Ioan	(ADHS) Temporal Logic Control of POMDPs Via Label-Based Stochastic Simulation Relations
Vasileva, Anna	(F-IDE) User Support for the Combinator Logic Synthesizer Framework
Vaux Auclair, Lionel	(Linearity/TLLA) On the Taylor expansion of λ-terms and the groupoid structure of their rigid approximants
Vechev, Martin	(CAV) Fast Numerical Program Analysis with Reinforcement Learning (SoMLMFM) AI2: AI Safety and Robustness with Abstract Interpretation (SYNT) Probabilistic and Interpretable Models of Code (MLP) Learning to Analyze Programs at Scale
Velan, Dominik	(LICS) Efficient Algorithms for Asymptotic Bounds on Termination Time in VASS
Veneris, Andreas	(SAT) Finding all Minimal Safe Inductive Sets
Vennekens, Joost	(LPOP) Logic-based Methods for Software Engineers and Business People (ICLP) Application of Logic-Based Methods to Machine Component Design
Verdier, Cees	(ADHS) Optimal Symbolic Controllers Determinization for BDD storage.
Veres, Sandor	(VaVAS) Towards a verifiable decision making framework for self-driving vehicles
Verhoef, Marcel	(Overture) The Overture Strategic Research Agenda
Vial, Pierre	(LICS) Every λ-Term is Meaningful for the Infinitary Relational Model (HOR) Some applications of quantitative types inside and outside type theory
Vicary, Jamie	(HDRA) Normal forms for planar connected string diagrams (UITP) Designing Globular: formal proofs as geometrical objects (Invited Talk)
Vigano, Luca	(FCS) A Formal Approach to Cyber-Physical Attacks
Vignudelli, Valeria	(FSCD) Proof techniques for program equivalence in probabilistic higher-order languages (LICS) Allegories: decidability and graph homomorphisms
Villadsen, Jørgen	(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) Substitutionless First-Order Logic: A Formal Soundness Proof (PAAR) A Verified Simple Prover for First-Order Logic (UITP) Drawing Trees
Villard, Jules	(MLP) Static Analysis for Developer Efficiency with Infer
Villaret, Mateu	(FSCD) Term-Graph Anti-Unification
Vilmart, Renaud	(LICS) Diagrammatic Reasoning beyond Clifford+T Quantum Mechanics (LICS) A Complete Axiomatisation of the ZX-Calculus for Clifford+T Quantum Mechanics
Vinyals, Marc	(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
Viswanathan, Arjun	(IJCAR) Datatypes with Shared Selectors
Viswanathan, Mahesh	(CAV) Model checking indistinguishability of randomized security protocols (CAV) Controller Synthesis Made Real: Reach-avoid Specifications and Linear Dynamics
Viswanathan, Mahesh	(ADHS) Statistical Verification of PCTL Using Stratified Samples
Vivekanandan, Paventhan	(FCS) A Homotopical Approach to Cryptography
Vizel, Yakir	(CAV) Lazy Self-Composition for Security Verification (SMT) Discovering Universally Quantified Solutions for Constrained Horn Clauses
Vojnar, Tomas	(CAV) ADAC: Automated Design of Approximate Circuits (LaSh) Lazy Automata Techniques for WS1S
Vollmer, Heribert	(LICS) Model-Theoretic Characterizations of Boolean and Arithmetic Circuit Classes of Small Depth
von Glehn, Tamara	(LICS) Dialectica models of type theory (MSFP) Polynomial models of type theory
Voronkov, Andrei	(IJCAR) A FOOLish Encoding of the Next State Relations of Imperative Programs
Vu, Xuan Tung	(SCSC) EA: Wrapping Computer Algebra is Surprisingly Successful for Non-Linear SMT
Vuotto, Simone	(DS-FM) Consistency Checking of Functional Requirements
Vyas, Nikhil	(LICS) Distribution-based objectives for Markov Decision Processes
Vákár, Matthijs	(Domains13) Diffeological Spaces and Semantics for Differential Programming
Vörös, András	(AVOCS) Backward reachability analysis for timed automata with data variables
W
W. V. Tran-Jørgensen, Peter	(Overture) Enhancing Testing of VDM-SL models
Wacheux, Florence	(GraMSec) Deciding the Non-Emptiness of Attack trees
Waez, Md Tawhid Bin	(FM) Formal Verification of Automotive Simulink Controller Models: Empirical Technical Challenges, Evaluation and Recommendations (FM) Verifying Auto-Generated C Code from Simulink
Wagner, Lucas	(CAV) The JKind Model Checker
Waldmann, Johannes	(WST) Comparing on Strings: Semantic Kachinuki Order
Waldmann, Uwe	(IJCAR) Formalizing Bachmair and Ganzinger's Ordered Resolution Prover (IJCAR) Superposition for Lambda-Free Higher-Order Logic
Wallace, Richard	(RCRA) Replaceability for constraint satisfaction problems: Algorithms, Inferences, and Complexity Patterns (RCRA) Partial (Neighbourhood) Singleton Arc Consistency for Constraint Satisfaction Problems
Walther, Christoph	(CAV) Formally Verified Montgomery Multiplication
Wang, Chao	(CAV) SCInfer: Refinement-based Verification of Software Countermeasures against Side-Channel Attacks
Wang, Guozhen	(CAV) Android Stack Systems
Wang, Jingyi	(FM) Towards `Verifying' a Water Treatment System
Wang, Quanlong	(LICS) Two complete axiomatisations of pure-state qubit quantum computing
Wang, Xinyu	(CAV) Learning Abstractions for Program Synthesis
Wang, Yi	(ICLP-DC) Probabalistic Action Language pBC+ (ICLP) A Probabilistic Extension of Action Language BC+
Warinschi, Bogdan	(CSF) Machine-checked proofs for electronic voting: privacy and verifiability for Belenios
Warren, David S.	(LPOP) LPOP2018 XSB Position Paper (ICLP) Top-down and Bottom-up Evaluation Procedurally Integrated
Watson, Nathaniel	(F-IDE) Integrating user design and formal models within PVSio-Web
Waugh Ambridge, Todd	(LOLA) A graph-rewriting perspective of the beta-law
Weaver, Sean	(SAT) XORSAT Set Membership Filters
Weber, Kai	(POS) CryptoMiniSat Parameter-Optimization for Solving Cryptographic Instances
Webster, Matt	(AVOCS) Formal Verification of Synchronisation, Gossip and Environmental Effects for Wireless Sensor Networks
Wehrle, Klaus	(CAV) Symbolic Liveness Analysis of Real-World Software
Weigl, Alexander	(UITP) Adding Text-Based Interaction to a Direct-Manipulation Interface for Program Verification -- Lessons Learned (VSTTE) Relational Equivalence Proofs Between Imperative and MapReduce Algorithms
Weinberger, Jonathan	(HoTT/UF) (Truncated) Simplicial Models of Type Theory
Weininger, Maximilian	(CAV) Value Iteration for Simple Stochastic Games: Stopping Criterion and Learning Algorithm
Weinstein, Scott	(LCC) Traversal-invariant definability and Logarithmic-space computation
Weissenbacher, Georg	(IJCAR) A Separation Logic with Data: Small Models and Automation (ADSL) Sloth: Separation Logic and Theories via Small Models
Wellen, Felix	(HoTT/UF) Cohesive Covering Theory
Wells, Joe	(LFMTP) What Does This Notation Mean Anyway? BNF-style notation as it is actually used
Weng, Xuetian	(TLA) Invariants in Distributed Algorithms
Wenzel, Makarius	(Isabelle) Further Scaling of Isabelle Technology (UITP) Isabelle/PIDE after 10 years of development (F-IDE) Isabelle/jEdit as IDE for domain-specific formal languages and informal text documents
Weseley, Allyson	(SYNT) Programming by example: efficient, but not “helpful”
Wesselink, Wieger	(ARQNL) Evidence Extraction from Parameterised Boolean Equation Systems
West, Adam	(SAT) Satalia's SolveEngine
West, Matthew	(ADHS) Statistical Verification of PCTL Using Stratified Samples
Westbrook, Edwin	(CAV) Continuous formal verification of Amazon s2n
Whalen, Michael	(CAV) The JKind Model Checker
Wheatley, Jack	(ADHS) Approximate Abstractions of Markov Chains with Interval Decision Processes
White, David	(REFINE) A more relaxed way to make concrete: uses of heuristic search to discover implementations
Wiedling, Cyrille	(FCS) Proving physical proximity using symbolic models
Wies, Thomas	(SMT) Invited talk: Automating Separation Logics using SMT (ADSL) Automating the Flow Framework
Wijesuriya, Viraj Brian	(VEMDP) Bayesian Verification of Chemical Reaction Networks
Wijs, Anton	(PLR) GPU Accelerated SAT solving (FM) To Compose, Or Not to Compose, That is the Question: An Analysis of Compositional State Space Generation
Wild, Paul	(LICS) A van Benthem Theorem for Fuzzy Modal Logic
Willemse, Tim	(ARQNL) Evidence Extraction from Parameterised Boolean Equation Systems
Wimmer, Karina	(QBF) Preprocessing for (D)QBF
Wimmer, Ralf	(QBF) Preprocessing for (D)QBF
Wimmer, Simon	(ITP) Verified Memoization and Dynamic Programming (ITP) MDP + TA = PTA: Probabilistic Timed Automata, Formalized (Short Paper)
Winfree, Erik	(VEMDP) Equivalence of chemical reaction networks in a CRN-to-DNA compiler framework.
Winkler, Sarah	(IWC) Certified Ordered Completion (FSCD) Completion for Logically Constrained Rewriting (IJCAR) MaedMax: A Maximal Ordered Completion Tool (VSTTE) Loop Detection by Logically Constrained Term Rewriting
Winschel, Viktor	(LICS) Compositional game theory (SR) Compositional Game Theory
Winskel, Glynn	(GS) A definable game semantics for the linear quantum lambda-calculus (GS) Probabilistic strategies (LICS) The concurrent game semantics of Probabilistic PCF (Domains13) Games and domains
Winskel, Glynn	(GS) Continuous probability distributions in concurrent games
Winston, Ezra	(MLP) Answering Cloze-style Software Questions Using Stack Overflow
Winter, Kirsten	(REFINE) Correctness of Concurrent Objects under Weak Memory Models
Wintersteiger, Christoph M.	(SMT) The next 10^4 UppSAT Approximations (IJCAR) Exploring Approximations for Floating-Point Arithmetic using UppSAT (SAT) Welcome to SAT 2018 (SAT) Award Ceremony
Wirsen, Andreas	(ADHS) Switch induced instabilities for stable power system DAE models
Wisniewski, Rafal	(ADHS) Algorithm for Bernstein Polynomial Control Design
Więckowski, Bartosz	(EICNCL) Intuitionistic multi-agent subatomic natural deduction for belief and knowledge
Wolf, Clifford	(CAV) BTOR2, BtorMC and Boolector 3.0
Wolff, Burkhart	(Isabelle) Using Isabelle/UTP for the Verification of Sorting Algorithms: A Case Study
Woltran, Stefan	(ASPOCP) selp: A Single-Shot Epistemic Logic Program Solver (SAT) Exploiting Treewidth for Projected Model Counting and its Limits (PRUV) A new logic for jointly representing hard and soft constraints
Woltzenlogel Paleo, Bruno	(UITP) Partial Regularization of First-Order Resolution Proofs
Woodcock, Jim	(VaVAS) RoboTool: Modelling and Verification with RoboChart
Wooldridge, Michael	(ReMOTE) How to Free Yourself from the Curse of Bad Equilibria (SR) Local Equilibria in Logic-Based Multi-Player Games
Worrell, James	(FoPSS) Computational learning theory I (FoPSS) Computational learning theory II (WST) Termination Checking and Invariant Synthesis for Affine Programs (LICS) Polynomial Invariants for Affine Programs
Wright, Ian	(MLP) Measuring software development productivity: a machine learning approach
Wu, Benjamin	(ICLP) Learning Commonsense Knowledge through Interactive Dialogue
Wu, Nicolas	(LICS) Syntax and Semantics for Operations with Scopes
Wu, Zhilin	(CAV) Android Stack Systems
X
Xia, Bican	(CAV) Monitoring CTMCs By Multi-Clock Timed Automata
Xiang, Weiming	(ADHS) Reachability Analysis for One Dimensional Linear Parabolic Equation
Xu, Zhiwu	(FM) Towards `Verifying' a Water Treatment System (CSF) A Permission-Dependent Type System for Secure Information Flow Analysis
Xue, Tao	(NLCS) Propositional Forms of Judgemental Interpretations
Y
Yahav, Eran	(CAV) From Programs to interpretable Deep Models, and Back (MLP) code2vec: Learning Distributed Representations of Code
Yamada, Akihisa	(WST) Towards a Unified Method for Termination (WST) A Perron-Frobenius Theorem for Jordan Blocks for Complexity Proving (ITP) A Formalization of the LLL Basis Reduction Algorithm
Yamagata, Yoriyuki	(FM) Falsification of Cyber-Physical Systems Using Deep Reinforcement Learning
Yan, Jun	(CAV) Android Stack Systems
Yan, Rongjie	(FM) Resource-aware Design for Reliable Autonomous Applications with Multiple Periods
Yang, Junfeng	(CAV) Partial Order Aware Concurrency Sampling
Yang, Junjie	(FM) Resource-aware Design for Reliable Autonomous Applications with Multiple Periods
Yang, Mohan	(ICLP) Declarative Algorithms in Datalog with Aggregates: user-friendly formal semantics conducive to performance and scalability
Yang, Weikun	(CAV) Lazy Self-Composition for Security Verification
Yang, Zhun	(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
Yao, Shucai	(REFINE) Refining Santa: An Excercise in Efficient Synchronization
Yap, Roland	(ICLP) Shape Neutral Analysis of Graph-based Data-structures
Yeom, Samuel	(CSF) Privacy Risk in Machine Learning: Analyzing the Connection to Overfitting
Yokoyama, Keita	(LICS) A parameterized halting problem, the linear time hierarchy, and the MRDP theorem
Yonbawi, Saud	(VaVAS) Towards a Hierarchical-Control Architecture for Distributed Autonomous Systems (Extended Abstract - Paper)
Yong, Sze Zheng	(ADHS) Input Design for Nonlinear Model Discrimination Via Affine Abstraction
Yong, Sze Zheng	(ADHS) Optimization-Based Design of Bounded-Error Estimators Robust to Missing Data
Yoshida, Nobuko	(LICS) Causal Computational Complexity of Distributed Processes
Yuan, Xinhao	(CAV) Partial Order Aware Concurrency Sampling
Z
Zaffanella, Enea	(CAV) A Direct Encoding for NNC Polyhedra
Zahn, Philipp	(LICS) Compositional game theory (SR) Compositional Game Theory
Zaidi, Fatiha	(IJCAR) Cubicle-W: Parameterized Model Checking on Weak Memory
Zaikin, Oleg	(SAT) ALIAS: A Modular Tool for Finding Backdoors for SAT
Zakrzewski, Jakub	(VSTTE) Towards verification of Ethereum smart contracts: a formalization of core of Solidity
Zalinescu, Eugen	(CSF) Inductive Invariants for Noninterference in Multi-agent Workflows
Zamani, Majid	(ADHS) Compositional Synthesis of Finite Abstractions for Continuous-Space Stochastic Control Systems: A Small-Gain Approach
Zamani, Majid	(ADHS) Compositional Abstraction-based Synthesis for Cascade Discrete-Time Control Systems
Zamdzhiev, Vladimir	(TERMGRAPH) A framework for rewriting families of string diagrams (LICS) Enriching a Linear/Non-linear Lambda Calculus: A Programming Language for String Diagrams
Zanasi, Fabio	(LICS) Rewriting with Frobenius
Zaniolo, Carlo	(ICLP) Declarative Algorithms in Datalog with Aggregates: user-friendly formal semantics conducive to performance and scalability
Zankl, Harald	(FSCD) Confluence Competition 2018
Zdancewic, Steve	(ITP) A Formal Equational Theory for Call-by-Push-Value
Zeilberger, Noam	(LICS) A theory of linear typings as flows on 3-valent graphs
Zeljić, Aleksandar	(SMT) The next 10^4 UppSAT Approximations (IJCAR) Exploring Approximations for Floating-Point Arithmetic using UppSAT
Zendel, Oliver	(POS) CryptoMiniSat Parameter-Optimization for Solving Cryptographic Instances
Zervakis, Georgios	(Overture) Multi-modelling of Cooperative Swarms
Zetzsche, Georg	(LICS) Separability by piecewise testable languages and downward closures beyond subwords
Zhan, Bohua	(IJCAR) Verifying Asymptotic Time Complexity of Imperative Programs in Isabelle
Zhan, Naijun	(CAV) Monitoring CTMCs By Multi-Clock Timed Automata
Zhang, Fan	(FM) Resource-aware Design for Reliable Autonomous Applications with Multiple Periods
Zhang, Fuyuan	(FM) Compositional Reasoning for Shared-variable Concurrent Programs
Zhang, Hantao	(IJCAR) Investigating the Existence of Large Sets of Idempotent Quasigroups via Satisfiability Testing
Zhang, Haozhe	(GraMSec) A state machine system for insider threat detection
Zhang, Hengruo	(CSF) Knowledge-based Security of Dynamic Secrets for Reactive Programs
Zhang, Jian	(IJCAR) Investigating the Existence of Large Sets of Idempotent Quasigroups via Satisfiability Testing (IJCAR) A New Probabilistic Algorithm for Approximate Model Counting (PRUV) VolCE: An Efficient Tool for Solving #SMT(LA) Problems (PRUV) A New Probabilistic Algorithm for Approximate Model Counting
Zhang, Jun	(CAV) SCInfer: Refinement-based Verification of Software Countermeasures against Side-Channel Attacks
Zhang, Min	(AVOCS) Using SMT engine to generate Symbolic Automata
Zhang, Qinglin	(ICLP) An ASP Methodology for Understanding Narratives about Stereotypical Activities
Zhang, Richard	(MLP) Difflog: Beyond Deductive Methods in Program Analysis
Zhang, Timothy	(ICLP) Constraint-Based Inference in Probabilistic Logic Programs
Zhang, Yi	(CSF) KEVM: A Complete Formal Semantics of the Ethereum Virtual Machine
Zhang, Yueling	(CAV) Syntax-Guided Termination Analysis
Zhang, Zhizheng	(ICLP) Introspecting Preferences In Answer Set Programming
Zhao, Jinxu	(ITP) Formalization of a Polymorphic Subtyping Algorithm
Zhao, Yizheng	(IJCAR) FAME: An Automated Tool for Semantic Forgetting in Expressive Description Logics
Zhao, Yongwang	(FM) Compositional Reasoning for Shared-variable Concurrent Programs
Zhao, Yuhang	(TERMGRAPH) Semantics-Preserving DPO-Based Term Graph Rewriting
Zheng, Yunhui	(CAV) StringFuzz: A Fuzzer for String Solvers
Zhou, Neng-Fa	(LPOP) A Picat-based XCSP Solver - from Parsing, Modeling, to SAT Encoding (RCRA) Encoding PB Constraints into SAT via Binary Adders and BDDs -- Revisited
Zhou, Qi	(HCVS) Solving Constrained Horn Clauses Using Dependence-Disjoint Expansions
Zhou, Weichao	(CAV) Safety-Aware Apprenticeship Learning
Zhu, Di	(FM) Resource-aware Design for Reliable Autonomous Applications with Multiple Periods
Zhu, Shufang	(WiL) First-Order vs. Second-Order Encodings for LTLf-to-Automata Translation
Zhu, Xiaoran	(CSF) KEVM: A Complete Formal Semantics of the Ethereum Virtual Machine
Zhumagambetov, Rustam	(UITP) Automated Theorem Proving in a Chat Environment
Ziegler, Albert	(MLP) Measuring software development productivity: a machine learning approach
Zmigrod, Ran	(ITP) An Agda Formalization of Üresin & Dubois' Asynchronous Fixed-Point Theory
Zorzi, Margherita	(Linearity/TLLA) Quantum programming made easy
Zucca, Elena	(DCM) A syntactic model of mutation and aliasing
Zuleger, Florian	(LICS) Efficient Algorithms for Asymptotic Bounds on Termination Time in VASS
Zuliani, Paolo	(NSV) Verified Probabilistic Reachability in Parametric Hybrid Systems: Theory and Tool Implementation
Zunic, Dragisa	(Linearity/TLLA) Formalization of Automated Trading Systems in a Concurrent Linear Framework
Zwanziger, Colin	(NLCS) Propositional Attitude Operators in Homotopy Type Theory
Zwart, Maaike	(MSFP) Some No-Go Theorems for Distributive Laws (extended abstract)
Zygalakis, Konstantinos	(VEMDP) Noise control for molecular computing
Á
Ábrahám, Erika	(SCSC) RP: Evaluation of Equational Constraints for CAD in SMT Solving (FM) Formal Verification of Automotive Simulink Controller Models: Empirical Technical Challenges, Evaluation and Recommendations (FM) Verifying Auto-Generated C Code from Simulink (IJCAR) Symbolic Computation Techniques in SMT Solving: Mathematical Beauty meets Efficient Heuristics
Álvez, Javier	(Vampire) Towards Word Sense Disambiguation by Reasoning
Â
Ângelo, Pedro	(ITRS) Gradual Intersection Types
Č
Červený, Jan	(VEMDP) Executable Biochemical Space for Specification and Analysis of Biochemical Systems
Š
Šalagovič, Jakub	(VEMDP) Executable Biochemical Space for Specification and Analysis of Biochemical Systems