FLOC 2018: FEDERATED LOGIC CONFERENCE 2018

A
Abate, Alessandro	(ADHS) Approximate Abstractions of Markov Chains with Interval Decision Processes (PDF, talk)
Abate, Alessandro	(ADHS) Benchmarks for Cyber-Physical Systems: A Modular Model Library for Building Automation Systems (PDF, talk)
Abate, Alessandro	(ADHS) Temporal Logic Control of General Markov Decision Processes by Approximate Policy Refinement (PDF, talk)
Abbasizanjani, Hoda	(SAT) Minimal unsatisfiability and minimal strongly connected digraphs (PDF, talk)
Abbott, John	(SCSC) New in CoCoA-5.2.4 and CoCoALib-0.99570 for SC-Square (PDF, talk)
Abdennadher, Slim	(ICLP) CHRvis: Syntax and Semantics (PDF, talk)
Abou-Msabah, Slimane	(RCRA) An Enhanced Genetic Algorithm with the BLF2G Guillotine Placement Heuristic for the Orthogonal Cutting-Stock Problem (PDF, talk)
Abrahamsson, Oskar	(IJCAR) Proof-Producing Synthesis of CakeML with I/O and Local State from Monadic HOL Functions (PDF, talk)
Acclavio, Matteo	(IJCAR) From Syntactic Proofs to Combinatorial Proofs (PDF, talk)
Achermann, Reto	(ITP) Physical addressing on real hardware in Isabelle/HOL (PDF, talk)
Achlioptas, Dimitris	(SAT) Fast Sampling of Perfectly Uniform Satisfying Assignments (PDF, talk) (SAT) Fast and Flexible Probabilistic Model Counting (PDF, talk)
Aerts, Bram	(ICLP) Application of Logic-Based Methods to Machine Component Design (PDF, talk)
Affeldt, Reynald	(Coq) Classical Analysis with Coq (PDF, talk)
Agha-Mohammadi, Ali-Akbar	(ADHS) Temporal Logic Control of POMDPs Via Label-Based Stochastic Simulation Relations (PDF, talk)
Ahmadi, Mohamadreza	(ADHS) Compositional Analysis of Hybrid Systems Defined Over Finite Alphabets (PDF, talk)
Ahn, Ki Yung	(LICS) Quasi-Open Bisimilarity with Mismatch is Intuitionistic (PDF, talk)
Akazaki, Takumi	(FM) Falsification of Cyber-Physical Systems Using Deep Reinforcement Learning (PDF, talk)
Akgün, Özgür	(LaSh) Automated Constraint Modelling with Conjure (PDF, talk)
Akshay, S.	(CAV) What’s hard about Boolean Functional Synthesis? (PDF, talk) (LICS) Distribution-based objectives for Markov Decision Processes (PDF, talk)
Al-Nuaimi, Mohammed	(VaVAS) Towards a verifiable decision making framework for self-driving vehicles (PDF, talk)
Albarghouthi, Aws	(CAV) Constraint-Based Synthesis of Coupling Proofs (PDF, talk)
Albert, Elvira	(FM) SDN-Actors: Modeling and Verification of SDN Programs (PDF, talk) (CAV) Constrained Dynamic Partial Order Reduction (PDF, talk)
Allred, Joel	(LICS) A Simple and Optimal Complementation Algorithm for Büchi Automata (PDF, talk)
Almeida, José Bacelar	(CSF) Enforcing ideal-world leakage bounds in real-world secret sharing MPC frameworks (PDF, talk)
Alrajeh, Dalal	(FM) A Weakness Measure for GR(1) Formulae (PDF, talk)
Alt, Leonardo	(SMT) SMT-based Compile-time Verification of Safety Properties for Smart Contracts (PDF, talk)
Altenkirch, Thorsten	(HoTT/UF) Towards the syntax and semantics of higher dimensional type theory (PDF, talk) (LICS) Free Higher Groups in Homotopy Type Theory (PDF, talk)
Alturki, Musab A.	(FCS) Statistical Model Checking of Guessing and Timing Attacks on Distance-bounding Protocols (PDF, talk)
Alves, Gleifer	(VaVAS) Formalisation of the Rules of the Road for embedding into an Autonomous Vehicle Agent (PDF, talk)
Alves, Sandra	(FSCD) A Unifying Framework for Type Inhabitation (PDF, talk) (Linearity/TLLA) Termination of lambda-calculus linearization methods (PDF)
Alviano, Mario	(ICLP) Shared aggregate sets in answer set programming (PDF, talk) (ICLP) Cautious Reasoning in ASP via Minimal models and Unsatisfiable Cores (PDF, talk) (ICLP) A Trajectory Calculus for Qualitative Spatial Reasoning Using Answer Set Programming (PDF, talk)
Alvim, Mario S.	(FM) An Algebraic Approach for Reasoning About Information Flow (PDF, talk) (CSF) Local Differential Privacy on Metric Spaces: optimizing the trade-off with utility (PDF)
Amarioarei, Alexandru	(VEMDP) Computational Approaches for the Programmed Assembly of Nanocellulose Meshes (PDF, talk)
Amendola, Giovanni	(RCRA) Externally Supported Models for Efficient Computation of Paracoherent Answer Sets (PDF, talk)
Ames, Aaron	(ADHS) Temporal Logic Control of POMDPs Via Label-Based Stochastic Simulation Relations (PDF, talk)
Amiridze, Nino	(NLCS) Anti-Unification and Natural Language Processing (PDF, talk)
Américo, Arthur	(FM) An Algebraic Approach for Reasoning About Information Flow (PDF, talk)
Anand, Abhishek	(ITP) Towards Certified Meta-Programming with Typed Template-Coq (PDF, talk)
Andersen, Jakob Lykke	(VEMDP) Rule-Based Gillespie Simulation of Chemical Systems (PDF, talk)
Anderson, David	(VEMDP) Noise Control for Molecular Computing (PDF, talk)
Anderson, Greg	(CAV) Learning Abstractions for Program Synthesis (PDF, talk)
Anderson, Patrick	(ADHS) A switched system approach to optimize mixing of fluids (PDF, talk)
Andrianarivelo, Nirina	(FSCD) Confluence of Prefix-Constrained Rewrite Systems (PDF, talk)
Angelos, Daniella	(WiL) On the Combination of Resolution and SAT Procedures for Modal Theorem-Proving (PDF, talk)
Angiuli, Carlo	(HoTT/UF) Cubical Computational Type Theory (PDF, talk) (LFMTP) The RedPRL Proof Assistant (PDF)
Antoniou, Grigoris	(ICLP) A Trajectory Calculus for Qualitative Spatial Reasoning Using Answer Set Programming (PDF, talk)
Antunes, Duarte	(ADHS) A switched system approach to optimize mixing of fluids (PDF, talk)
Aoto, Takahito	(FSCD) Confluence Competition 2018 (PDF)
Araki, Keijiro	(Overture) ViennaVM: a Virtual Machine for VDM-SL development (PDF, talk)
Arcaini, Paolo	(F-IDE) AsmetaF: a flattener for the ASMETA framework (PDF, talk)
Argyros, George	(CAV) The Learnability of Symbolic Automata (PDF, talk)
Arias, Joaquin	(ICLP) Constraint Answer Set Programming without Grounding (PDF, talk)
Arnaboldi, Luca	(FCS) LISA: Predicting the Impact of DoS Attacks on Real-World Low Power IoT Systems (PDF, talk)
Arndt, Hannah	(CAV) Let this Graph be your Witness! An Attestor for Verifying Java Pointer Programs (PDF, talk)
Aryal, Deepak	(Isabelle) Hilbert Meets Isabelle: Formalisation of the DPRM Theorem in Isabelle (PDF, talk)
Asada, Kazuyuki	(LICS) Species, Profunctors and Taylor Expansion Weighted by SMCC--A Unified Framework for Modelling Nondeterministic, Probabilistic and Quantum Programs-- (PDF, talk)
Asadi, Sepideh	(VSTTE) Lattice-Based Refinement in Bounded Model Checking (PDF, talk)
Aschieri, Federico	(CL&C) On Natural Deduction for Herbrand Constructive Logics III: The Strange Case of the Intuitionistic Logic of Constant Domains (PDF, talk) (ITRS) Natural Deduction and Normalization Proofs for the Intersection Type Discipline (PDF, talk)
Atkey, Robert	(LICS) The Syntax and Semantics of Quantitative Type Theory (PDF, talk)
Atserias, Albert	(LICS) Definable Ellipsoid Method, Sums-of-Squares Proofs, and the Isomorphism Problem (PDF, talk)
Audinot, Maxime	(CSF) Guided design of attack trees: a system-based approach (PDF, talk)
Avelar, Andréia B.	(ITP) Formalizing Ring Theory in PVS (short paper) (PDF, talk)
Avellaneda, Florent	(FM) FSM Inference from Long Traces (PDF, talk)
Avgustinov, Pavel	(FM) Variant analysis with QL (PDF, talk)
Avni, Guy	(SR) Infinite-Duration Richman Bidding Games (PDF, talk)
Awodey, Steve	(LICS) Impredicative Encodings of (Higher) Inductive Types (PDF, talk)
Ayala-Rincon, Mauricio	(FSCD) Fixed-Point Constraints for Nominal Equational Unification (PDF, talk) (UNIF) Preface of the 32nd International Workshop on Unification UNIF 2018 (PDF)
Azadbakht, Keyvan	(FM) Deadlock Detection for Actor-based Coroutines (PDF, talk)
Azizi-Sultan, Ahmad-Saher	(ARQNL) Pseudo-Propositional Logic (PDF, talk)
B
Baader, Franz	(UNIF) ACUI Unification Modulo Ground Theories (PDF, talk)
Baba Ali, Ahmed Riadh	(RCRA) An Enhanced Genetic Algorithm with the BLF2G Guillotine Placement Heuristic for the Orthogonal Cutting-Stock Problem (PDF, talk)
Bacchus, Fahiem	(IJCAR) Implicit Hitting Set Algorithms for Maximum Satisfiability Modulo Theories (PDF, talk)
Bacci, Giorgio	(LICS) Boolean-Valued Semantics for Stochastic Lambda-Calculus (PDF, talk) (LICS) An algebraic theory of Markov processes (PDF, talk)
Bacci, Giovanni	(FM) Optimal and Robust Controller Synthesis Using Energy Timed Automata with Uncertainty (PDF, talk)
Backeman, Peter	(IJCAR) Exploring Approximations for Floating-Point Arithmetic using UppSAT (PDF, talk) (SMT) The next 10^4 UppSAT Approximations (PDF, talk)
Backes, John	(CAV) The JKind Model Checker (PDF, talk)
Backhouse, Kevin	(FM) Variant analysis with QL (PDF, talk)
Badelt, Stefan	(VEMDP) Equivalence of Chemical Reaction Networks in a CRN-to-DNA Compiler Framework (PDF, talk)
Badonnel, Rémi	(AVOCS) Rule-Based Synthesis of Chains of Security Functions for Software-Defined Networks (PDF, talk)
Baeta, Nuno	(ThEdu) Rating of Geometric Automated Theorem Provers (PDF, talk)
Bahr, Patrick	(FSCD) Strict Ideal Completions of the Lambda Calculus (PDF, talk) (PARIS) What makes guarded types tick? (PDF, talk)
Baier, Christel	(LICS) Stochastic Shortest Paths and Weight-Bounded Properties in Markov Decision Processes (PDF, talk)
Baioletti, Marco	(RCRA) Algebraic Crossover Operators for Permutations (PDF, talk)
Bak, Stanley	(ADHS) Reachability Analysis for One Dimensional Linear Parabolic Equation (PDF, talk)
Bakker, Bert G.J.	(ADHS) Interacting Particle System-Based Estimation of Reach Probability for a Generalized Stochastic Hybrid System (PDF, talk)
Balbiani, Philippe	(UNIF) Preface of the 32nd International Workshop on Unification UNIF 2018 (PDF)
Balco, Samuel	(ITP) Software tool support for modular reasoning in modal logics of actions (PDF, talk)
Balduccini, Marcello	(ICLP) An ASP Methodology for Understanding Narratives about Stereotypical Activities (PDF, talk)
Ban Kirigin, Tajana	(FCS) Statistical Model Checking of Guessing and Timing Attacks on Distance-bounding Protocols (PDF, talk)
Bannister, Callum	(ITP) Backwards and Forwards with Separation Logic (PDF, talk)
Bansal, Sorav	(SAT) Effective use of SMT solvers for Program Equivalence Checking through Invariant Sketching and Query Decomposition (PDF, talk)
Bansal, Suguman	(CAV) Synthesis Of Asynchronous Reactive Programs From Temporal Specifications (PDF, talk) (CAV) Automata vs Linear-Programming Discounted-Sum Inclusion (PDF, talk)
Barad, Gefry	(VEMDP) Computational Approaches for the Programmed Assembly of Nanocellulose Meshes (PDF, talk)
Baral, Chitta	(ICLP) Incremental and Iterative Learning of Answer Set Programs from Mutually Distinct Examples (PDF, talk)
Barbosa, Haniel	(IJCAR) Datatypes with Shared Selectors (PDF, talk) (SMT) Rewrites for SMT Solvers using Syntax-Guided Enumeration (PDF, talk) (SMT) Higher-Order SMT Solving (PDF, talk)
Barbosa, Manuel	(CSF) Enforcing ideal-world leakage bounds in real-world secret sharing MPC frameworks (PDF, talk)
Bardin, Sebastien	(CAV) Model Generation for Quantified Formulas: A Taint-Based Approach (PDF, talk)
Baritel-Ruet, Cécile	(CSF) Formal Security Proof of CMAC and its Variants (PDF, talk)
Barnett, Lee	(TERMGRAPH) Programming by Term Rewriting (PDF, talk)
Barrett, Clark	(IJCAR) Datatypes with Shared Selectors (PDF, talk) (CAV) Solving Quantified Bit-Vectors using Invertibility Conditions (PDF, talk) (SMT) Rewrites for SMT Solvers using Syntax-Guided Enumeration (PDF, talk)
Barthe, Gilles	(CSF) Enforcing ideal-world leakage bounds in real-world secret sharing MPC frameworks (PDF, talk) (CSF) Secure compilation of side-channel countermeasures: the case of cryptographic “constant-time” (PDF, talk)
Bartocci, Ezio	(CAV) Reachable Set Over-approximation for Nonlinear Systems Using Piecewise Barrier Tubes (PDF, talk) (CAV) A Counting Semantics for Monitoring LTL Specifications over Finite Traces (PDF, talk)
Bartocci, Ezio	(ADHS) Verifying nonlinear analog and mixed-signal circuits with inputs (PDF, talk)
Baryannis, George	(ICLP) A Trajectory Calculus for Qualitative Spatial Reasoning Using Answer Set Programming (PDF, talk)
Basin, David	(CSF) Alethea: A Provably Secure Random Sample Voting Protocol (PDF, talk)
Basset, Nicolas	(SR) Beyond admissibility: Dominance between chains of strategies (PDF, talk)
Baston, Colm	(ITP) The Coinductive Formulation of Common Knowledge (PDF, talk)
Batsakis, Sotiris	(ICLP) A Trajectory Calculus for Qualitative Spatial Reasoning Using Answer Set Programming (PDF, talk)
Bauer, Matthew	(CAV) Model checking indistinguishability of randomized security protocols (PDF, talk)
Bauer, Sabine	(LaSh) Decidable Linear Tree Constraints (PDF, talk) (LaSh) Decidable Linear Tree Constraints - Extended Abstract (PDF)
Baumgartner, Alexander	(FSCD) Term-Graph Anti-Unification (PDF, talk)
Bayer, Jonas	(Isabelle) Hilbert Meets Isabelle: Formalisation of the DPRM Theorem in Isabelle (PDF, talk)
Becchi, Anna	(CAV) A Direct Encoding for NNC Polyhedra (PDF, talk)
Becker, Bernd	(SAT) Dynamic Polynomial Watchdog Encoding for Solving Weighted MaxSAT (PDF, talk)
Becker, Heiko	(FM) Combining Tools for Optimization and Analysis of Floating-Point Computations (PDF, talk)
Becker, Jan Steffen	(AVOCS) Analyzing Consistency of Formal Requirements (PDF, talk)
Bekki, Daisuke	(NLCS) Paychecks, Presupposition, and Dependent Types (PDF, talk)
Belardinelli, Francesco	(SR) Verification of Multi-agent Systems with Imperfect Information and Public Actions (PDF, talk)
Bellin, Gianluigi	(FSCD) Proof nets for bi-intuitionistic linear logic (PDF, talk)
Belta, Calin	(VaVAS) Formal Synthesis of Control Strategies for Dynamical Systems (PDF) (VaVAS) Trust me - I am autonomous (PDF) (VaVAS) Reproducibility in Robotics - The Big 5 Issues (PDF)
Ben Abdelali, Marwa	(REFINE) Programming Without Refinement (PDF, talk)
Ben Salah, Kais	(PRUV) Evidential Group Decision Making Model with Belief-Based Preferences (PDF, talk)
Bendkowski, Maciej	(FSCD) Counting Environments and Closures (PDF, talk) (HOR) Combinatorics of explicit substitutions (extended abstract) (PDF, talk)
Benjamin, Thibaut	(HDRA) Towards a fully formalized definition of syllepsis in weak higher categories (PDF, talk)
Bentkamp, Alexander	(IJCAR) Superposition for Lambda-Free Higher-Order Logic (PDF, talk)
Benzaken, Véronique	(ITP) A Coq formalisation of SQL’s execution engines (PDF, talk)
Benzmüller, Christoph	(IJCAR) The Higher-Order Prover Leo-III (PDF, talk) (ARQNL) System Demonstration: The Higher-Order Prover Leo-III (PDF, talk)
Benzmüller, Christoph	(WiL) Embedding Intuitionistic Modal Logics in Higher-Order Logic. An Easy Task? (PDF, talk)
Berger, Philipp	(FM) Verifying Auto-Generated C Code from Simulink (PDF, talk)
Berryhill, Ryan	(SAT) Finding all Minimal Safe Inductive Sets (PDF, talk)
Berthon, Raphaël	(SR) Strategy Logic with Imperfect Information (PDF, talk)
Bertozzi, Davide	(RCRA) Logic Programming approaches for routing fault-free and maximally-parallel Wavelength Routed Optical Networks on Chip (Application paper) (PDF, talk)
Bertrand, Nathalie	(LICS) Stochastic Shortest Paths and Weight-Bounded Properties in Markov Decision Processes (PDF, talk)
Berzish, Murphy	(CAV) StringFuzz: A Fuzzer for String Solvers (PDF, talk)
Bessai, Jan	(F-IDE) User Support for the Combinator Logic Synthesizer Framework (PDF, talk)
Beyene, Tewodros A.	(FM) Evidential and Continuous Integration of Software Verification Tools (PDF, talk) (WPTE) Verification of Ada Programs with AdaHorn (PDF, talk)
Beyersdorff, Olaf	(PC) Size, Cost and Capacity: A Semantic Technique for Hard Random QBFs (PDF)
Bhagyanath, Anoop	(ICLP) Optimal Scheduling for Exposed Datapath Architectures with Buffered Processing Units by ASP (PDF, talk)
Bhaskar, Siddharth	(LCC) Computability over locally finite structures from algebra (PDF, talk)
Bhatt, Devesh	(F-IDE) The CLEAR Way To Transparent Formal Methods (PDF, talk)
Bhayat, Ahmed	(PAAR) Set of Support for Higher-Order Reasoning (PDF, talk)
Bickford, Mark	(LICS) Computability Beyond Church-Turing via Choice Sequences (PDF, talk)
Bienmüller, Tom	(SCSC) Constraint Systems from Traffic Scenarios for the Validation of Autonomous Driving (PDF, talk)
Biere, Armin	(SCSC) A Practical Polynomial Calculus for Arithmetic Circuit Verification (PDF, talk) (IJCAR) Implicit Hitting Set Algorithms for Maximum Satisfiability Modulo Theories (PDF, talk) (CAV) BTOR2, BtorMC and Boolector 3.0 (PDF, talk) (POS) Two flavors of DRAT (PDF, talk) (POS) The Effect of Scrambling CNFs (PDF, talk)
Bigatti, Anna Maria	(SCSC) New in CoCoA-5.2.4 and CoCoALib-0.99570 for SC-Square (PDF, talk)
Birkedal, Lars	(HoTT/UF) Dependent Right Adjoint Types (PDF, talk) (LICS) ReLoC: A Mechanised Relational Logic for Fine-Grained Concurrency (PDF, talk)
Biró, Csaba	(SMT) Puli - A Problem-Specific OMT Solver (PDF, talk)
Bjorner, Nikolaj	(SAT) Constrained Image Generation Using Binarized Neural Networks with Decision Procedures (PDF, talk) (FM) Z3 and SMT in Industrial R&D (PDF, talk)
Blaauwbroek, Lasse	(Coq) Proof Construction by Tactic Learning (PDF, talk)
Blair, Richard	(ITP) Efficient Mendler-Style Lambda-Encodings in Cedille (PDF, talk)
Blanchet, Bruno	(CSF) Composition Theorems for CryptoVerif and Application to TLS 1.3 (PDF, talk)
Blanchette, Jasmin Christian	(IJCAR) Superposition for Lambda-Free Higher-Order Logic (PDF, talk) (IJCAR) Formalizing Bachmair and Ganzinger's Ordered Resolution Prover (PDF, talk) (IJCAR) Superposition with Datatypes and Codatatypes (PDF, talk) (Isabelle) A Verified SAT Solver with Watched Literals Using Imperative HOL (Extended Abstract) (PDF, talk)
Blanqui, Frédéric	(WST) Termination of Lambda-Pi modulo rewriting using the size-change principle (PDF, talk)
Blinkhorn, Joshua	(PC) Size, Cost and Capacity: A Semantic Technique for Hard Random QBFs (PDF)
Bliutze, Simon	(AVOCS) Using SMT engine to generate Symbolic Automata (PDF, talk)
Bloem, Roderick	(CAV) A Counting Semantics for Monitoring LTL Specifications over Finite Traces (PDF, talk)
Blondin, Michael	(CAV) Peregrine: A Tool for the Analysis of Population Protocols (PDF, talk) (LICS) Black Ninjas in the Dark: Formal Analysis of Population Protocols (PDF)
Blot, Valentin	(LICS) Extensional and Intensional Semantic Universes: A Denotational Model of Dependent Types (PDF, talk)
Blotsky, Dmitry	(CAV) StringFuzz: A Fuzzer for String Solvers (PDF, talk)
Boag, Simon	(WiL) Towards a Logical Framework for Latent Variable Modelling (PDF, talk)
Bobot, Francois	(FM) A Formally Verified Floating-Point Implementation of the Compact Position Reporting Algorithm (PDF, talk) (SMT) Centralizing Equality Reasoning in MCSAT (PDF, talk)
Bockenek, Joshua	(Isabelle) Using Isabelle/UTP for the Verification of Sorting Algorithms: A Case Study (PDF, talk)
Bodirsky, Manuel	(IJCAR) Complexity of Combinations of Qualitative Constraint Satisfaction Problems (PDF, talk) (LICS) A universal-algebraic proof of the complexity dichotomy for Monotone Monadic SNP (PDF, talk)
Bohrer, Brandon	(LICS) A Hybrid, Dynamic Logic for Hybrid-Dynamic Information Flow (PDF, talk)
Bojanczyk, Mikolaj	(LICS) Regular and First Order List Functions (PDF, talk) (LICS) Definable decompositions for graphs of bounded linear cliquewidth (PDF, talk) (LICS) On computability and tractability for infinite sets (PDF, talk)
Boker, Udi	(LICS) Automaton-Based Criteria for Membership in CTL (PDF, talk)
Bonakdarpour, Borzoo	(CSF) The Complexity of Monitoring Hyperproperties (PDF, talk)
Bonchi, Filippo	(LICS) Rewriting with Frobenius (PDF, talk) (LICS) Sound up-to techniques and Complete abstract domains (PDF, talk)
Bonet, Maria	(PC) On Dual-Rail Based MaxSAT Solving (PDF, talk)
Bonichon, Richard	(CAV) Model Generation for Quantified Formulas: A Taint-Based Approach (PDF, talk)
Bonifati, Angela	(ICLP) Certified Graph View Maintenance with Regular Datalog (PDF, talk)
Boralv, Arne	(FM) Interlocking Design Automation using Prover Trident (PDF, talk)
Bouajjani, Ahmed	(CAV) Reasoning About TSO Programs Using Reduction and Abstraction (PDF, talk) (CAV) On the Completeness of Verifying Message Passing Programs under Bounded Asynchrony (PDF, talk)
Boulier, Simon	(ITP) Towards Certified Meta-Programming with Typed Template-Coq (PDF, talk)
Boulmé, Sylvain	(ITP) A Coq Tactic for Equality Learning in Linear Arithmetic (PDF, talk) (Coq) What is the Foreign Function Interface of the Coq Programming Language? (PDF, talk)
Bourdais, Romain	(ADHS) Hierarchical Model Predictive Control for Building Energy Management of Hybrid Systems (PDF, talk)
Bouyer-Decitre, Patricia	(FM) Optimal and Robust Controller Synthesis Using Energy Timed Automata with Uncertainty (PDF, talk) (SR) Dependences in Strategy Logic (PDF, talk)
Bradford, Russell	(SCSC) Non-linear Real Arithmetic Benchmarks derived from Automated Reasoning in Economics (PDF, talk)
Brandt, Kasper Fabæch	(UNIF) Formalization of First-Order Syntactic Unification (PDF, talk)
Brauer, Joerg	(FM) Model-Based Testing for Avionics Systems (PDF, talk)
Brazdil, Tomas	(LICS) Efficient Algorithms for Asymptotic Bounds on Termination Time in VASS (PDF, talk)
Breik, Keenan	(VEMDP) Computing Properties of Stable Configurations of Thermodynamic Binding Networks (PDF, talk)
Brendel, Elliot	(ADHS) An Interval-Based Sliding Horizon Motion Planning Method (PDF, talk)
Breuvart, Flavien	(HOR) Refining Properties of Filter Models: Sensibility, Approximability and Reducibility (PDF, talk)
Breza, Michael	(AVOCS) Formal Verification of Synchronisation, Gossip and Environmental Effects for Critical IoT Systems (PDF, talk)
Brihaye, Thomas	(MoRe) Constraint Problem for Weak Subgame Perfect Equilibria with omega-regular Boolean Objectives (PDF, talk) (MoRe) Stochastic o-minimal hybrid systems (PDF, talk)
Brim, Luboš	(VEMDP) Executable Biochemical Space for Specification and Analysis of Biochemical Systems (PDF, talk)
Brockmeyer, Udo	(SCSC) Constraint Systems from Traffic Scenarios for the Validation of Autonomous Driving (PDF, talk)
Broda, Krysia	(ThEdu) Towards intuitive reasoning in axiomatic geometry (PDF, talk)
Broda, Sabine	(FSCD) A Unifying Framework for Type Inhabitation (PDF, talk)
Bromberger, Martin	(IJCAR) A Reduction from Unbounded Linear Mixed Arithmetic Problems into Bounded Problems (PDF, talk)
Brotherston, James	(ADSL) On the Complexity of Pointer Arithmetic in Separation Logic (PDF, talk)
Bruni, Roberto	(LICS) Concurrency and Probability: Removing Confusion, Compositionally (PDF, talk)
Bruse, Florian	(PARIS) Collapses of Fixpoint Alternation Hierarchies in Low Type-Levels of Higher-Order Fixpoint Logic (PDF, talk)
Bruyère, Véronique	(MoRe) Constraint Problem for Weak Subgame Perfect Equilibria with omega-regular Boolean Objectives (PDF, talk) (MoRe) Parameterized complexity of games with monotonically ordered omega-regular objectives (PDF, talk)
Buchholtz, Ulrik	(HoTT/UF) (Truncated) Simplicial Models of Type Theory (PDF, talk) (LICS) Higher Groups in Homotopy Type Theory (PDF, talk) (LICS) Cellular Cohomology in Homotopy Type Theory (PDF, talk)
Buruiana, Sebastian	(WPTE) Reducing Total Correctness to Partial Correctness by a Transformation of the Language Semantics (PDF, talk)
Bury, Guillaume	(SMT) Centralizing Equality Reasoning in MCSAT (PDF, talk) (SMT) SMT Solving Modulo Tableau and Rewriting Theories (PDF, talk)
Busard, Simon	(FM) Producing Explanations for Rich Logics (PDF, talk)
Busoniu, Lucian	(ADHS) Space-Time Budget Allocation for Marketing Over Social Networks (PDF, talk)
Buss, Sam	(PC) On Dual-Rail Based MaxSAT Solving (PDF, talk)
Butler, Michael	(VaVAS) Policing Functions for Machine Learning Systems (PDF, talk)
Bønneland, Frederik M.	(CAV) Start Pruning When Time Gets Urgent: Partial Order Reduction for Timed Systems (PDF, talk)
Büning, Julian	(CAV) Symbolic Liveness Analysis of Real-World Software (PDF, talk)
C
C. D. S. Oliveira, Bruno	(ITP) Formalization of a Polymorphic Subtyping Algorithm (PDF, talk)
Cabalar, Pedro	(ICLP) Temporal Answer Set Programming on Finite Traces (PDF, talk) (ICLP) Functional ASP with Intensional Sets; Application to Gelfond-Zhang Agreggates (PDF, talk)
Calinescu, Radu	(VaVAS) Towards a Hierarchical-Control Architecture for Distributed Autonomous Systems (Extended Abstract - Paper) (PDF, talk)
Cantor, Anthony	(CL&C) (Short Paper) Towards a Dualized Sequent Calculus with Canonicity (PDF, talk)
Capelli, Florent	(QBF) Tractability results for structured quantified CNF-formulas via knowledge compilation (PDF, talk) (PC) Proof systems for #SAT based on restricted circuits (PDF, talk)
Capretta, Venanzio	(ITP) The Coinductive Formulation of Common Knowledge (PDF, talk)
Carbin, Michael	(LICS) Computable decision-making on the reals and other spaces via partiality and nondeterminism (PDF, talk)
Cardelli, Luca	(VEMDP) Molecular Filters for Noise Reduction (PDF, talk)
Carette, Jacques	(ITP) HOL Light QE (PDF, talk)
Carlier, Sébastien	(LFMTP) What Does This Notation Mean Anyway? BNF-Style Notation as it is actually used (PDF, talk)
Carral, David	(IJCAR) Efficient Model Construction for Horn Logic with VLog: System Description (PDF, talk)
Carro, Manuel	(ICLP) Constraint Answer Set Programming without Grounding (PDF, talk)
Cassandras, Christos G.	(ADHS) Hybrid System Modeling of Multi-Agent Coverage Problems with Energy Depletion and Repletion (PDF, talk)
Castellan, Simon	(LICS) The concurrent game semantics of Probabilistic PCF (PDF, talk)
Catta, Davide	(NLCS) Do different syntactic trees yield different logical readings? Some remarks on head variables in typed lambda calculus. (PDF, talk)
Cauderlier, Raphaël	(ITP) Tactics and certificates in Meta Dedukti (PDF, talk)
Cavalcanti, Ana	(VaVAS) RoboTool: Modelling and Verification with RoboChart (PDF, talk)
Cavallo, Evan	(HoTT/UF) Cubical Computational Type Theory (PDF, talk) (LFMTP) The RedPRL Proof Assistant (PDF)
Cavezza, Davide Giacomo	(FM) A Weakness Measure for GR(1) Formulae (PDF, talk) (DS-FM) Heuristic-Based GR(1) Assumptions Refinement (PDF, talk)
Cerna, David	(FSCD) Higher-Order Equational Pattern Anti-Unification (PDF, talk) (UNIF) Towards Generalization Methods for Purely Idempotent Equational Theories (PDF, talk) (PARIS) Towards the Automatic Construction of Schematic Proofs (PDF, talk)
Cervesato, Iliano	(Linearity/TLLA) Formalization of Automated Trading Systems in a Concurrent Linear Framework (PDF, talk)
Ceska, Milan	(CAV) ADAC: Automated Design of Approximate Circuits (PDF, talk)
Chadha, Rohit	(CAV) Model checking indistinguishability of randomized security protocols (PDF, talk)
Chakraborty, Supratik	(CAV) What’s hard about Boolean Functional Synthesis? (PDF, talk)
Chalub, Fabricio	(NLCS) OpenWordNet-PT: Taking Stock (PDF, talk)
Chand, Saksham	(TLA) Invariants in Distributed Algorithms (PDF)
Chanseau Saint-Germain, Ken	(VEMDP) Conservative Approximations of Polymers (PDF, talk)
Chapoutot, Alexandre	(ADHS) An Interval-Based Sliding Horizon Motion Planning Method (PDF, talk)
Charalambidis, Angelos	(ICLP) Approximation Fixpoint Theory and the Well-Founded Semantics of Higher-Order Logic Programs (PDF, talk)
Chatterjee, Krishnendu	(CAV) Symbolic Algorithms for Graphs and Markov Decision Processes with Fairness Objectives (PDF, talk) (LICS) Efficient Algorithms for Asymptotic Bounds on Termination Time in VASS (PDF, talk)
Chatzikokolakis, Kostas	(CSF) Local Differential Privacy on Metric Spaces: optimizing the trade-off with utility (PDF)
Chatzikyriakidis, Stergios	(NLCS) Propositional Forms of Judgemental Interpretations (PDF, talk)
Chaudhuri, Kaustuv	(LFMTP) Computation-as-deduction in Abella: work in progress (PDF, talk)
Chaudhuri, Swarat	(CAV) Automata vs Linear-Programming Discounted-Sum Inclusion (PDF, talk)
Chen, Hongxu	(CSF) A Permission-Dependent Type System for Secure Information Flow Analysis (PDF, talk)
Chen, Taolue	(CAV) Android Stack Machine (PDF, talk)
Chen, Yijia	(LICS) Tree depth, quantifier elimination, and quantifier rank (PDF, talk) (LICS) A parameterized halting problem, the linear time hierarchy, and the MRDP theorem (PDF, talk)
Chenavier, Cyrille	(IWC) The diamond lemma for free modules (PDF, talk) (HDRA) Generalizations of the associative operad and convergent rewrite systems (PDF, talk)
Cheung, Wai-Tak	(LICS) The Geometry of Computation-Graph Abstraction (PDF, talk)
Cheval, Vincent	(CAV) The DEEPSEC prover (PDF, talk) (CSF) A little more conversation, a little less action, a lot more satisfaction: Global states in ProVerif. (PDF, talk)
Chifflier, Pierre	(FM) Modular Verification of Programs with Effects and Effect Handlers in Coq (PDF, talk)
Chirkova, Rada	(FCS) An Expressive, Flexible and Uniform Logical Formalism for Attribute-based Access Control (PDF, talk)
Chlipala, Adam	(ITP) Reification by Parametricity (PDF, talk) (LICS) Computable decision-making on the reals and other spaces via partiality and nondeterminism (PDF, talk)
Chockler, Hana	(FM) Timed Vacuity (PDF, talk) (VSTTE) Lattice-Based Refinement in Bounded Model Checking (PDF, talk)
Chonev, Ventsislav	(SR) Infinite-Duration Richman Bidding Games (PDF, talk)
Christiansen, David	(UNIF) Efficiency of a Good but not Linear Nominal Unification Algorithm (PDF, talk)
Christiansen, Henning	(IWC) Confluence in Constraint Handling Rules (PDF)
Chuang, Xue An	(ADHS) CoasterX: A Case Study in Component-Driven Hybrid Systems Proof Automation (PDF, talk)
Chudnov, Andrey	(CAV) Continuous formal verification of Amazon s2n (PDF, talk) (CSF) Assuming you know: epistemic semantics of relational annotations for expressive flow policies (PDF, talk)
Cimatti, Alessandro	(SAT) Experimenting on Solving Nonlinear Integer Arithmetic with Incremental Linearization (PDF, talk) (FM) Formal Specification and Verification of Dynamic Parametrized Architectures (PDF, talk)
Ciobaca, Stefan	(IJCAR) A Coinductive Approach to Proving Reachability in Logically Constrained Term Rewriting Systems (PDF, talk) (WPTE) Reducing Total Correctness to Partial Correctness by a Transformation of the Language Semantics (PDF, talk)
Ciurezu, Bogdan	(Isabelle) Hilbert Meets Isabelle: Formalisation of the DPRM Theorem in Isabelle (PDF, talk)
Claessen, Koen	(NLCS) Automatic test suite generation for PMCFG grammars (PDF, talk) (IJCAR) Efficient encodings of first-order Horn formulas in equational logic (PDF, talk)
Clairambault, Pierre	(LICS) The concurrent game semantics of Probabilistic PCF (PDF, talk)
Claus, Maximilian	(WiL) Embedding Intuitionistic Modal Logics in Higher-Order Logic. An Easy Task? (PDF, talk)
Clouston, Ranald	(HoTT/UF) Dependent Right Adjoint Types (PDF, talk)
Clymo, Judith	(PC) Short Proofs in QBF Expansion (PDF)
Cock, David	(ITP) Physical addressing on real hardware in Isabelle/HOL (PDF, talk)
Cohen, Cyril	(ITP) Towards Certified Meta-Programming with Typed Template-Coq (PDF, talk) (Coq) Classical Analysis with Coq (PDF, talk)
Cohen, Ernie	(FM) Object-Oriented Security Proofs (PDF, talk)
Cohen, Liron	(WiL) On Expanding Standard Notions of Constructivity (PDF, talk) (WiL) Non-well-founded proof system for Transitive Closure Logic (PDF, talk) (LICS) Computability Beyond Church-Turing via Choice Sequences (PDF, talk) (PARIS) Transitive Closure Logic: Infinitary and Cyclic Proof Systems (PDF, talk)
Collins, Nathan	(CAV) Formal Verification of a Vehicle-to-Vehicle (V2V) Messaging System (PDF, talk) (CAV) Continuous formal verification of Amazon s2n (PDF, talk)
Colvin, Robert	(FM) A wide-spectrum language for verification of programs on weak memory models (PDF, talk) (REFINE) Correctness of Concurrent Objects under Weak Memory Models (PDF, talk)
Combette, Guillaume	(ITP) A Formal Proof of the Minor-Exclusion Property for Treewidth-Two Graphs (PDF, talk)
Conchon, Sylvain	(HCVS) Declarative Parameterized Verification of Topology-sensitive Distributed Protocols (PDF, talk) (IJCAR) Cubicle-W: Parameterized Model Checking on Weak Memory (PDF, talk) (SMT) Alt-Ergo 2.2 (PDF, talk)
Condie, Tyson	(ICLP) Declarative Algorithms in Datalog with Aggregates: user-friendly formal semantics conducive to performance and scalability (PDF, talk)
Condoluci, Andrea	(CL&C) Admissible tools in the kitchen of intuitionistic logic (PDF, talk)
Constable, Robert	(LICS) Computability Beyond Church-Turing via Choice Sequences (PDF, talk)
Contejean, Evelyne	(ITP) A Coq formalisation of SQL’s execution engines (PDF, talk)
Cook, Byron	(CAV) Formal reasoning about the security of AWS (PDF)
Cook, Byron	(CAV) Continuous formal verification of Amazon s2n (PDF, talk) (CAV) Model Checking Boot Code from AWS Data Centers (PDF, talk)
Copello, Ernesto	(LFMTP) Formalisation of Barendregt's Variable Convention for Generic Structures with Binders (PDF, talk)
Copes, Martin	(LFMTP) Formalization in Constructive Type Theory of the Standardization Theorem (PDF, talk)
Coquand, Thierry	(LICS) Inner Models of Univalence (PDF) (LICS) On Higher Inductive Types in Cubical Type Theory (PDF, talk)
Coquereau, Albin	(SMT) Alt-Ergo 2.2 (PDF, talk)
Cordeiro, Lucas	(CAV) JBMC: A Bounded Model Checking Tool for Verifying Java Bytecode (PDF, talk)
Cordero, Christophe	(HDRA) Generalizations of the associative operad and convergent rewrite systems (PDF, talk)
Corsi, Giovanna	(ARQNL) Labelled calculi for QMLs with non-rigid and non-denoting terms (PDF, talk)
Cortier, Véronique	(CSF) Machine-checked proofs for electronic voting: privacy and verifiability for Belenios (PDF, talk) (CSF) A little more conversation, a little less action, a lot more satisfaction: Global states in ProVerif. (PDF, talk)
Costa, Oswaldo Luiz V.	(ADHS) Network-Aware Design of State-Feedback Controllers for Linear Wireless Networked Control Systems (PDF, talk)
Costabile, Roberta	(LPOP) Role-Based Access Control via JASP (PDF, talk)
Coti, Camille	(CAV) Quasi-Optimal Partial Order Reduction (PDF, talk)
Courcelle, Bruno	(LaSh) Monadic Second-Order Model Checking with Fly-Automata (PDF, talk) (LaSh) Monadic Second-Order Model Checking with Fly-Automata - Slides (PDF)
Cousot, Patrick	(CAV) Program Analysis is Harder than Verification: A Computability Perspective (PDF, talk)
Couto, Rui	(F-IDE) Improving the Visualization of Alloy Instances (PDF, talk)
Cowen-Rivers, Alexander	(SCSC) Towards Incremental Cylindrical Algebraic Decomposition in Maple (PDF, talk)
Crary, Karl	(LICS) Strong Sums in Focused Logic (PDF, talk)
Creissac Campos, José	(F-IDE) Improving the Visualization of Alloy Instances (PDF, talk)
Cropper, Andrew	(TERMGRAPH) SLD-Resolution Reduction of Second-Order Horn Fragments - Extended Abstract (PDF, talk)
Crouch, Richard	(NLCS) Graph Knowledge Representations for SICK (PDF, talk)
Cruanes, Simon	(SMT) SMT Solving Modulo Tableau and Rewriting Theories (PDF, talk)
Cruanes, Simon	(IJCAR) Superposition for Lambda-Free Higher-Order Logic (PDF, talk)
Crubillé, Raphaëlle	(LICS) Probabilistic stable functions on discrete cones are power series. (PDF, talk)
Csikász-Nagy, Attila	(VEMDP) Molecular Filters for Noise Reduction (PDF, talk)
Cunha, Alcino	(F-IDE) Improving the Visualization of Alloy Instances (PDF, talk)
Cuteri, Bernardo	(LPOP) On the Development of Industrial Applications with ASP (PDF, talk)
Czajka, Łukasz	(FSCD) Term rewriting characterisation of LOGSPACE for finite and infinite data (PDF, talk)
Czeizler, Eugen	(VEMDP) Computational Approaches for the Programmed Assembly of Nanocellulose Meshes (PDF, talk)
Côrte-Real, Joana	(ICLP) Improving Candidate Quality of Probabilistic Logic Models (PDF, talk)
D
D'Antoni, Loris	(CAV) Syntax Guided Synthesis with Quantitative Syntactic Objectives (PDF, talk) (CAV) The Learnability of Symbolic Automata (PDF, talk)
D'Innocenzo, Alessandro	(ADHS) Approximate Abstractions of Markov Chains with Interval Decision Processes (PDF, talk)
D'Innocenzo, Alessandro	(ADHS) Data-Driven Switched Affine Modeling for Model Predictive Control (PDF, talk)
Daafouz, Jamal	(ADHS) Network-Aware Design of State-Feedback Controllers for Linear Wireless Networked Control Systems (PDF, talk)
Dabrowski, Yoann	(Linearity/TLLA) Models of Linear Logic based on the Schwartz epsilon product (PDF, talk)
Daggitt, Matthew L.	(ITP) An Agda Formalization of Üresin & Dubois' Asynchronous Fixed-Point Theory (PDF, talk)
Dahlem, Marc	(ICLP) Optimal Scheduling for Exposed Datapath Architectures with Buffered Processing Units by ASP (PDF, talk)
Daian, Philip	(CSF) KEVM: A Complete Formal Semantics of the Ethereum Virtual Machine (PDF, talk)
Dailler, Sylvain	(F-IDE) Lightweight Interactive Proving inside an Automatic Program Verifier (PDF, talk)
Dal Lago, Ugo	(DCM) On Higher-Order Probabilistic Computation (PDF)
Dallmeyer, Nils	(WPTE) Optimizing Space of Parallel Processes (PDF, talk)
Dang, Thao	(ADHS) Occupation Measure Methods for Modelling and Analysis of Biological Hybrid Systems (PDF, talk)
Danielski, Daniel	(LICS) Unary negation fragment with equivalence relations has the finite model property (PDF, talk)
Dantchev, Stefan	(PC) Resolution and the binary encoding of combinatorial principles (PDF, talk)
Dardha, Ornela	(WiL) A New Linear Logic for Deadlock-Free Session-Typed Processes (Talk Abstract) (PDF, talk)
Dartois, Luc	(LICS) Logics for Word Transductions with Synthesis (PDF, talk)
Darulova, Eva	(FM) Combining Tools for Optimization and Analysis of Floating-Point Computations (PDF, talk)
Das, Ankush	(LICS) Work Analysis with Resource-Aware Session Types (PDF, talk)
Das, Anupam	(TYDI) Proof complexity of deep inference: a survey (PDF, talk) (CL&C) Some ideas on cut-elimination for cyclic arithmetic proofs (PDF, talk) (LCC) A recursion-theoretic characterisation of the positive polynomial-time functions (PDF, talk) (IJCAR) Focussing, MALL and the polynomial hierarchy (PDF, talk) (PARIS) On the logical complexity of cyclic arithmetic (PDF, talk) (PC) Towards theories for positive polynomial time and monotone proofs with extension (PDF, talk)
Das, Ariyam	(ICLP) Declarative Algorithms in Datalog with Aggregates: user-friendly formal semantics conducive to performance and scalability (PDF, talk)
Dave, Vrunda	(LICS) Regular Transducer Expressions for Regular Transformations over infinite words (PDF, talk)
Davenport, James H.	(SCSC) Non-linear Real Arithmetic Benchmarks derived from Automated Reasoning in Economics (PDF, talk)
Daviaud, Laure	(LICS) Regular and First Order List Functions (PDF, talk) (LICS) A pseudo-quasi-polynomial algorithm for solving mean-payoff parity games (PDF, talk)
David, Cristina	(WST) Procedure-Modular Termination Analysis (PDF, talk) (CAV) Counterexample Guided Inductive Synthesis Modulo Theories (PDF, talk)
David, Marco	(Isabelle) Hilbert Meets Isabelle: Formalisation of the DPRM Theorem in Isabelle (PDF, talk)
Dawar, Anuj	(LICS) Preface (PDF)
Dawson, Jeremy	(IJCAR) Well-Founded Unions (PDF, talk)
De Angelis, Emanuele	(HCVS) Metaprogramming and symbolic execution for detecting runtime errors in Erlang programs (PDF, talk) (ICLP) Solving Horn Clauses on Inductive Data Types Without Induction (PDF, talk)
De Boer, Frank	(FM) Deadlock Detection for Actor-based Coroutines (PDF, talk)
de Felice, Giovanni	(FSCD) A diagrammatic axiomatisation of fermionic quantum circuits (PDF, talk)
de Lima, Thaynara A.	(ITP) Formalizing Ring Theory in PVS (short paper) (PDF, talk)
de Lima, Tiago	(IJCAR) An Assumption-Based Approach for Solving The Minimal S5-Satisfiability Problem (PDF, talk)
de Melo, Gerard	(NLCS) OpenWordNet-PT: Taking Stock (PDF, talk)
de Paiva, Valeria	(NLCS) OpenWordNet-PT: Taking Stock (PDF, talk) (NLCS) Graph Knowledge Representations for SICK (PDF, talk) (Linearity/TLLA) On the Lambek Calculus with an Exchange Modality (PDF, talk) (Linearity/TLLA) Benchmarking Linear Logic Translations (PDF, talk)
de Putter, Sander	(FM) To Compose, Or Not to Compose, That is the Question: An Analysis of Compositional State Space Generation (PDF, talk)
De Santis, Elena	(ADHS) On Approximate Predictability of Metric Systems (PDF, talk)
de Silva, Nadish	(LICS) Logical paradoxes in quantum computation (PDF, talk)
de Vink, Erik	(FM) Deadlock Detection for Actor-based Coroutines (PDF, talk)
De Vos, Marina	(VaVAS) Social Consequence Engines (Abstract) (PDF, talk)
de Wolff, Timo	(PC) Optimization over the Boolean Hypercube via Sums of Nonnegative Circuit Polynomials (PDF, talk)
Debant, Alexandre	(FCS) Proving physical proximity using symbolic models (PDF, talk)
Declerck, David	(IJCAR) Cubicle-W: Parameterized Model Checking on Weak Memory (PDF, talk)
Defoort, Michael	(ADHS) Razumikhin-type Theorems on Practical Stability of Dynamic Equations on Time Scales (PDF, talk)
Defoort, Michael	(ADHS) Stability of switched systems on non-uniform time domains with non commuting matrices (PDF, talk)
Delahaye, David	(SMT) SMT Solving Modulo Tableau and Rewriting Theories (PDF, talk)
Delaune, Stéphanie	(FSCD) Analysing privacy-type properties in cryptographic protocols (PDF) (FCS) Proving physical proximity using symbolic models (PDF, talk)
Delpeuch, Antonin	(HDRA) Normal forms for planar connected string diagrams (PDF, talk)
Delzanno, Giorgio	(HCVS) Declarative Parameterized Verification of Topology-sensitive Distributed Protocols (PDF, talk)
Demangeon, Romain	(LICS) Causal Computational Complexity of Distributed Processes (PDF, talk)
Demri, Stéphane	(ADSL) A Complete Proof System for Basic Symbolic Heaps with Permissions (PDF, talk)
Denecker, Marc	(LPOP) The RBAC challenge in the KB-paradigm (PDF)
Deng, Yiping	(Isabelle) Hilbert Meets Isabelle: Formalisation of the DPRM Theorem in Isabelle (PDF, talk)
Dennis, Louise	(VaVAS) Formalisation of the Rules of the Road for embedding into an Autonomous Vehicle Agent (PDF, talk)
Dershowitz, Nachum	(TERMGRAPH) Drags: an algebraic framework for graph rewriting (PDF, talk) (DCM) Generic Graph Semantics (PDF, talk) (IJCAR) Well-Founded Unions (PDF, talk) (WST) GPO: A Path Ordering for Graphs (PDF, talk)
Devadas, Srini	(CSF) Secure Boot and Remote Attestation in the Sanctum Processor (PDF)
Devkota, Prabhat	(Isabelle) Hilbert Meets Isabelle: Formalisation of the DPRM Theorem in Isabelle (PDF, talk)
Devriendt, Jo	(LPOP) The RBAC challenge in the KB-paradigm (PDF)
Devriese, Dominique	(HoTT/UF) Internalizing Presheaf Semantics: Charting the Design Space (PDF, talk) (LICS) Degrees of Relatedness - A Unified Framework for Parametricity, Irrelevance, Ad Hoc Polymorphism, Intersections, Unions and Algebra in Dependent Type Theory (PDF, talk)
Di Benedetto, Maria Domenica	(ADHS) On Approximate Predictability of Metric Systems (PDF, talk)
Di Pierro, Alessandra	(DCM) Towards a Formal System for Topological Quantum Computation (PDF, talk)
Di Pompeo, Silvia	(RCRA) Optimal Fault-Tolerant Placement of Relay Nodes in a Mission Critical Wireless Network (PDF, talk)
Di Stasio, Antonio	(SR) Solving Parity Games: Explicit vs Symbolic (PDF, talk)
Diez, Stefan	(VEMDP) Formal Verification of Network-Based Biocomputation Circuits (PDF, talk)
Dillig, Isil	(CAV) Learning Abstractions for Program Synthesis (PDF, talk)
Ding, Yuhao	(ADHS) Input Design for Nonlinear Model Discrimination Via Affine Abstraction (PDF, talk)
Divasón, Jose	(ITP) A Formalization of the LLL Basis Reduction Algorithm (PDF, talk) (WST) A Perron-Frobenius Theorem for Jordan Blocks for Complexity Proving (PDF, talk)
Dixon, Clare	(PAAR) Evaluating Pre-Processing Techniques for the Separated Normal Form for Temporal Logics (PDF, talk) (AVOCS) Formal Verification of Synchronisation, Gossip and Environmental Effects for Critical IoT Systems (PDF, talk)
Djemai, Mohamed	(ADHS) Razumikhin-type Theorems on Practical Stability of Dynamic Equations on Time Scales (PDF, talk)
Djemai, Mohamed	(ADHS) Stability of switched systems on non-uniform time domains with non commuting matrices (PDF, talk)
Djouadi, Seddik	(ADHS) Stability of switched systems on non-uniform time domains with non commuting matrices (PDF, talk)
Dobre, Ana Maria	(VEMDP) Computational Approaches for the Programmed Assembly of Nanocellulose Meshes (PDF, talk)
Doczkal, Christian	(ITP) A Formal Proof of the Minor-Exclusion Property for Treewidth-Two Graphs (PDF, talk)
Dodaro, Carmine	(ICLP) Shared aggregate sets in answer set programming (PDF, talk) (ICLP) Cautious Reasoning in ASP via Minimal models and Unsatisfiable Cores (PDF, talk) (RCRA) Externally Supported Models for Efficient Computation of Paracoherent Answer Sets (PDF, talk)
Dodds, Josiah	(CAV) Continuous formal verification of Amazon s2n (PDF, talk)
Dohrau, Jérôme	(CAV) Permission Inference for Array Programs (PDF, talk)
Doménech, Jesús J.	(WST) Control-Flow Refinement via Partial Evaluation (PDF, talk)
Doré, Maximilian	(ThEdu) Towards intuitive reasoning in axiomatic geometry (PDF, talk)
Dougherty, Daniel	(FCS) Homomorphisms and Minimality for Enrich-by-Need Security Analysis (PDF, talk)
Dovier, Agostino	(ICLP) MASP-Reduce: a proposal for distributed computation of stable models (PDF, talk)
Doyle, Jon	(FCS) An Expressive, Flexible and Uniform Logical Formalism for Attribute-based Access Control (PDF, talk)
Dragan, Constantin Cătălin	(CSF) Machine-checked proofs for electronic voting: privacy and verifiability for Belenios (PDF, talk)
Dragoste, Irina	(IJCAR) Efficient Model Construction for Horn Logic with VLog: System Description (PDF, talk)
Dras, Mark	(FM) Processing text for privacy: An information flow perspective (PDF)
Dreier, Jannik	(CSF) Automated Unbounded Verification of Stateful Cryptographic Protocols with Exclusive OR (PDF, talk)
Dressler, Mareike	(PC) Optimization over the Boolean Hypercube via Sums of Nonnegative Circuit Polynomials (PDF, talk)
Dries, Anton	(ICLP) Improving Candidate Quality of Probabilistic Logic Models (PDF, talk)
Dross, Claire	(AVOCS) Climbing the Software Assurance Ladder - Practical Formal Verification for Reliable Software (PDF, talk)
Duan, Yihai	(FM) Falsification of Cyber-Physical Systems Using Deep Reinforcement Learning (PDF, talk)
Dubischar, Simon	(Isabelle) Hilbert Meets Isabelle: Formalisation of the DPRM Theorem in Isabelle (PDF, talk)
Dubslaff, Clemens	(LICS) Stochastic Shortest Paths and Weight-Bounded Properties in Markov Decision Processes (PDF, talk)
Duck, Gregory	(ICLP) Shape Neutral Analysis of Graph-based Data-structures (PDF, talk)
Duggirala, Parasara Sridhar	(ADHS) On Generating A Variety of Unsafe Counterexamples for Linear Dynamical Systems (PDF, talk)
Dullerud, Geir E.	(ADHS) Statistical Verification of PCTL Using Stratified Samples (PDF, talk)
Dumbrava, Stefania	(ICLP) Certified Graph View Maintenance with Regular Datalog (PDF, talk)
Dunn, Sara-Jane	(VEMDP) Uncovering the Biological Programs that Govern Development (PDF)
Dupont, Benjamin	(IWC) Coherence modulo relations (PDF, talk) (HDRA) Termination in linear (2,2)-categories with braidings and duals (PDF, talk)
Dupressoir, François	(CSF) Formal Security Proof of CMAC and its Variants (PDF, talk) (CSF) Machine-checked proofs for electronic voting: privacy and verifiability for Belenios (PDF, talk)
Durand, Arnaud	(LICS) Model-Theoretic Characterizations of Boolean and Arithmetic Circuit Classes of Small Depth (PDF, talk)
Durand, Irène	(LaSh) Monadic Second-Order Model Checking with Fly-Automata (PDF, talk)
Durazo-Cardenas, Isidro	(VaVAS) Towards validation and verification of an autonomous railway inspection and repair system (PDF, )
Dureja, Rohit	(CAV) SimpleCAR: An Efficient Bug-Finding Tool Based On Approximate Reachability (PDF, talk)
Durier, Adrien	(LICS) Eager Functions as Processes (PDF, talk)
Dutle, Aaron	(FM) A Formally Verified Floating-Point Implementation of the Compact Position Reporting Algorithm (PDF, talk) (FM) From Formal Requirements to Highly Assured Software for Unmanned Aircraft Systems (PDF, talk)
Dutra, Inês	(ICLP) Improving Candidate Quality of Probabilistic Logic Models (PDF, talk)
E
Eades Iii, Harley	(Linearity/TLLA) On the Lambek Calculus with an Exchange Modality (PDF, talk)
Eberhart, Clovis	(LICS) What's in a game? A theory of game models (PDF, talk)
Eberl, Manuel	(ITP) Verified Analysis of Random Binary Tree Structures (PDF, talk)
Ebner, Gabriel	(CL&C) Fast cut-elimination using proof terms: an empirical study (PDF, talk) (PAAR) Efficient translation of sequent calculus proofs into natural deduction proofs (PDF, talk)
Echenim, Mnacho	(ADSL) The Complexity of Prenex Separation Logic with One Selector (PDF, talk) (IJCAR) A Generic Framework for Implicate Generation Modulo Theories (PDF, talk)
Eeralla, Ajay Kumar	(UNIF) Bounded ACh Unification (PDF, talk)
Egerstedt, Magnus	(ADHS) Tracking Control via Variable-gain Integrator and Lookahead Simulation: Application to Leader-follower Multiagent Networks (PDF, talk)
Eggers, Andreas	(SCSC) Constraint Systems from Traffic Scenarios for the Validation of Autonomous Driving (PDF, talk)
Egly, Uwe	(IJCAR) QRAT+: Generalizing QRAT by a More Powerful QBF Redundancy Property (PDF, talk)
Ehlers, Rüdiger	(SAT) Approximately Propagation Complete and Conflict Propagating Constraint Encodings (PDF, talk)
Ehlers, Thorsten	(POS) Tuning Parallel SAT Solvers (PDF, talk)
Ehrig, Rainald	(RCRA) Computing Personalised Treatments through In Silico Clinical Trials. A Case Study on Downregulation in Assisted Reproduction. (PDF, talk)
Eilers, Marco	(CAV) Nagini: A Static Verifier for Python (PDF, talk) (CAV) MaxSMT-Based Type Inference for Python 3 (PDF, talk)
Eiter, Thomas	(ICLP) Exploiting Answer Set Programming with External Sources for Meta-Interpretive Learning (PDF, talk)
El Ouraoui, Daniel	(SMT) Higher-Order SMT Solving (PDF, talk)
Elffers, Jan	(SAT) Using Combinatorial Benchmarks to Probe the Reasoning Power of Pseudo-Boolean Solvers (PDF, talk) (SAT) In Between Resolution and Cutting Planes: A Study of Proof Systems for Pseudo-Boolean SAT Solving (PDF, talk)
Emmi, Michael	(CAV) Monitoring Weak Consistency (PDF, talk)
Endrullis, Joerg	(FSCD) Decreasing diagrams with two labels are complete for confluence of countable systems (PDF, talk)
Ene, Nneka	(TERMGRAPH) A Port-graph Model for Finance (PDF, talk)
Enea, Constantin	(CAV) Monitoring Weak Consistency (PDF, talk) (CAV) Reasoning About TSO Programs Using Reduction and Abstraction (PDF, talk) (CAV) On the Completeness of Verifying Message Passing Programs under Bounded Asynchrony (PDF, talk)
England, Matthew	(SCSC) Towards Incremental Cylindrical Algebraic Decomposition in Maple (PDF, talk) (SCSC) Non-linear Real Arithmetic Benchmarks derived from Automated Reasoning in Economics (PDF, talk)
Ensan, Alireza	(PRUV) A Model-Theoretic View on Preferences in Declarative Specifications of Search Problems (PDF, talk)
Erban, Radek	(VEMDP) Noise Control for Molecular Computing (PDF, talk)
Erbatur, Serdar	(UNIF) Knowledge Problems in Equational Extensions of Subterm Convergent Theories (PDF, talk)
Erbsen, Andres	(ITP) Reification by Parametricity (PDF, talk)
Erdélyi, Balázs	(SMT) Puli - A Problem-Specific OMT Solver (PDF, talk)
Esparza, Javier	(CAV) Peregrine: A Tool for the Analysis of Population Protocols (PDF, talk) (LICS) Black Ninjas in the Dark: Formal Analysis of Population Protocols (PDF) (LICS) One Theorem to Rule Them All: A Unified Translation of LTL into $\omega$-Automata (PDF, talk)
Eugster, Patrick Thomas	(CSF) A Cryptographic Look at Multi-Party Channels (PDF, talk)
Even-Mendoza, Karine	(VSTTE) Lattice-Based Refinement in Bounded Model Checking (PDF, talk)
F
Faber, Eric	(HoTT/UF) Towards a geometric model theory of type theory (PDF)
Faber, Wolfgang	(RCRA) Externally Supported Models for Efficient Computation of Paracoherent Answer Sets (PDF, talk)
Fahrenberg, Uli	(FM) Optimal and Robust Controller Synthesis Using Energy Timed Automata with Uncertainty (PDF, talk)
Fainekos, Georgios	(ADHS) Falsification of Temporal Logic Requirements Using Gradient Based Local Search in Space and Time (PDF, talk)
Fainekos, Georgios	(ADHS) Mission Planning for Multiple Vehicles with Temporal Specifications using UxAS (PDF, talk)
Falappa, Marcelo A.	(PRUV) Leveraging Probabilistic Existential Rules for Adversarial Deduplication (PDF, talk)
Fan, Chuchu	(FM) Approximate Partial Order Reduction (PDF, talk) (CAV) Controller Synthesis Made Real: Reach-avoid Specifications and Linear Dynamics (PDF, talk)
Fanchon, Eric	(ADHS) Occupation Measure Methods for Modelling and Analysis of Biological Hybrid Systems (PDF, talk)
Fandinno, Jorge	(ICLP) Functional ASP with Intensional Sets; Application to Gelfond-Zhang Agreggates (PDF, talk)
Farinas Del Cerro, Luis	(ICLP) Functional ASP with Intensional Sets; Application to Gelfond-Zhang Agreggates (PDF, talk)
Farinier, Benjamin	(CAV) Model Generation for Quantified Formulas: A Taint-Based Approach (PDF, talk)
Farka, Frantisek	(ICLP) Proof-relevant Horn Clauses for Dependent Type Inference and Term Synthesis (PDF, talk) (ICLP-DC) Proof-relevant resolution for elaboration of programming languages (PDF, talk)
Farkas, Rebeka	(AVOCS) Backward reachability analysis for timed automata with data variables (PDF, talk)
Farmer, William	(ITP) HOL Light QE (PDF, talk)
Fava, Daniel	(FM) Operational Semantics of a Weak Memory Model with Channel Synchronization (PDF, talk)
Fazekas, Katalin	(IJCAR) Implicit Hitting Set Algorithms for Maximum Satisfiability Modulo Theories (PDF, talk)
Fedyukovich, Grigory	(CAV) Syntax-Guided Termination Analysis (PDF, talk) (CAV) Exploiting Synchrony and Symmetry in Relational Verification (PDF, talk)
Felgenhauer, Bertram	(IWC) Towards a Verified Decision Procedure for Confluence of Ground Term Rewrite Systems in Isabelle/HOL (PDF, talk)
Feliu Gabaldon, Marco Antonio	(ITP) Boosting the Reuse of Formal Specifications (PDF, talk)
Feller, David	(LFMTP) What Does This Notation Mean Anyway? BNF-Style Notation as it is actually used (PDF, talk)
Feng, Yijun	(CAV) Monitoring CTMCs By Multi-Clock Timed Automata (PDF, talk)
Ferdinand, Christian	(FM) On Software Safety, Security, and Abstract Interpretation (PDF, talk)
Feret, Jérôme	(VEMDP) Conservative Approximations of Polymers (PDF, talk)
Fernandes, Natasha	(FM) Processing text for privacy: An information flow perspective (PDF)
Fernandez, Maribel	(FSCD) Fixed-Point Constraints for Nominal Equational Unification (PDF, talk)
Ferrando, Angelo	(HCVS) Declarative Parameterized Verification of Topology-sensitive Distributed Protocols (PDF, talk)
Ferreira, Joao F.	(ITP) Towards Verified Handwritten Calculational Proofs (short paper) (PDF, talk)
Ferrère, Thomas	(FM) The Compound Interest in Relaxing Punctuality (PDF, talk) (LICS) A Theory of Register Monitors (PDF, talk)
Fiacchini, Mirko	(ADHS) Language constrained stabilization of discrete- time switched linear systems: an LMI approach (PDF, talk)
Fichte, Johannes K.	(SAT) Exploiting Treewidth for Projected Model Counting and its Limits (PDF, talk) (LaSh) Solving #SAT by Parameterized Algorithms: Exploiting Small Treewidth (PDF, talk)
Fiedor, Tomas	(LaSh) Lazy Automata Techniques for WS1S (PDF, talk)
Figueira, Diego	(LICS) Playing with Repetitions in Data Words Using Energy Games (PDF, talk)
Fijalkow, Nathanaël	(SR) Quantifying Bounds in Strategy Logic (PDF, talk) (LICS) The State Complexity of Alternating Automata (PDF, talk)
Filiot, Emmanuel	(LICS) Logics for Word Transductions with Synthesis (PDF, talk) (LICS) Rational Synthesis Under Imperfect Information (PDF, talk)
Filippidis, Ioannis	(TLA) Proving properties of a minimal covering algorithm (PDF)
Filliâtre, Jean-Christophe	(F-IDE) Auto-active verification using Why3's IDE (PDF) (ITP) Deductive Program Verification (PDF)
Finger, Marcelo	(IJCAR) Probably Half True: Probabilistic Satisfiability over Lukasiewicz Infinitely-valued Logic (PDF, talk)
Finkbeiner, Bernd	(CAV) Model Checking Quantitative Hyperproperties (PDF, talk) (CAV) Synthesizing Reactive Systems from Hyperproperties (PDF, talk) (CSF) The Complexity of Monitoring Hyperproperties (PDF, talk)
Finzi, Alberto	(RCRA) Optimal Fault-Tolerant Placement of Relay Nodes in a Mission Critical Wireless Network (PDF, talk)
Fioravanti, Fabio	(ICLP) Solving Horn Clauses on Inductive Data Types Without Induction (PDF, talk)
Fioravanti, Fabio	(HCVS) Metaprogramming and symbolic execution for detecting runtime errors in Erlang programs (PDF, talk)
Fiorentino, Alessio	(LPOP) Role-Based Access Control via JASP (PDF, talk)
Firsov, Denis	(ITP) Efficient Mendler-Style Lambda-Encodings in Cedille (PDF, talk)
Fischlin, Marc	(CSF) Self-Guarding Cryptographic Protocols against Algorithm Substitution Attacks (PDF, talk) (CSF) Backdoored Hash Functions: Immunizing HMAC and HKDF (PDF, talk)
Fisher, Michael	(AVOCS) Formal Verification of Synchronisation, Gossip and Environmental Effects for Critical IoT Systems (PDF, talk) (VaVAS) Formalisation of the Rules of the Road for embedding into an Autonomous Vehicle Agent (PDF, talk)
Fitzgerald, John	(Overture) Design Space Exploration for Secure Building Control (PDF, talk)
Flamm, Christoph	(VEMDP) Rule-Based Gillespie Simulation of Chemical Systems (PDF, talk)
Fleury, Mathias	(Isabelle) A Verified SAT Solver with Watched Literals Using Imperative HOL (Extended Abstract) (PDF, talk)
Florido, Mário	(ITRS) Gradual Intersection Types (PDF, talk)
Flum, Jörg	(LICS) Tree depth, quantifier elimination, and quantifier rank (PDF, talk)
Foliard, Guillaume	(AVOCS) Climbing the Software Assurance Ladder - Practical Formal Verification for Reliable Software (PDF, talk)
Fontaine, Pascal	(SCSC) Wrapping Computer Algebra is Surprisingly Successful for Non-Linear SMT (PDF, talk) (SMT) Higher-Order SMT Solving (PDF, talk)
Foo, Yi Shyh Eddy	(ADHS) Multi-Energy Scheduling Using a Hybrid Systems Approach (PDF, talk)
Forest, Simon	(FSCD) Coherence of Gray categories via rewriting (PDF, talk) (IWC) Critical pairs for Gray categories (PDF, talk)
Forets, Marcelo	(ADHS) Occupation Measure Methods for Modelling and Analysis of Biological Hybrid Systems (PDF, talk)
Forrest, Stephen A.	(SCSC) SMT-like Queries in Maple (PDF, talk)
Forster, Yannick	(ITP) Verification of PCP-Related Computational Reductions in Coq (PDF, talk)
Foster, Simon	(VaVAS) RoboTool: Modelling and Verification with RoboChart (PDF, talk)
Fouque, Pierre-Alain	(CSF) Formal Security Proof of CMAC and its Variants (PDF, talk)
Francalanza, Adrian	(DCM) Pointing to Private Names (PDF, talk)
Fraser, Simon	(Overture) Integrating VDM-SL into the continuous delivery pipelines of cloud-based software (PDF, talk)
Fredrikson, Matt	(CSF) Privacy Risk in Machine Learning: Analyzing the Connection to Overfitting (PDF, talk)
Frehse, Goran	(CAV) Space-time Interpolants (PDF, talk)
Freitas, Leo	(F-IDE) VDM at large: Modelling the EMVCo 2nd Generation Kernel (PDF) (Overture) VDM at large: analysing the EMV Next Generation Kernel (PDF, talk)
Fremont, Daniel J.	(CAV) Reactive Control Improvisation (PDF, talk)
Frerix, Steffen	(UITP) Text-Orientated Formal Mathematics (PDF, talk)
Frey, Jonas	(LICS) Impredicative Encodings of (Higher) Inductive Types (PDF, talk)
Fribourg, Laurent	(ADHS) Control Synthesis for Stochastic Switched Systems Using the Tamed Euler Method (PDF, talk)
Fried, Dror	(LICS) Sequential Relational Decomposition (PDF, talk)
Friedman, Daniel	(UNIF) Efficiency of a Good but not Linear Nominal Unification Algorithm (PDF, talk)
Friedrich, Tobias	(SAT) Sharpness of the Satisfiability Threshold for Non-Uniform Random k-SAT (PDF, talk)
Frisch, Alan	(LaSh) ESSENCE, A Language for Specifying Combinatorial Problems: What, Why and So What? (PDF, talk)
Frittella, Sabine	(ITP) Software tool support for modular reasoning in modal logics of actions (PDF, talk)
Frohn, Florian	(WST) Complexity Analysis for Bitvector Programs (PDF, talk)
From, Andreas Halkjær	(ThEdu) Natural Deduction Assistant (NaDeA) (PDF, talk) (ThEdu) Students' Proof Assistant (SPA) (PDF, talk) (PAAR) A Verified Simple Prover for First-Order Logic (PDF, talk) (Isabelle) Drawing Trees (PDF) (Isabelle) Substitutionless First-Order Logic: A Formal Soundness Proof (PDF, talk)
Fruehwirth, Thom	(ICLP) CHRvis: Syntax and Semantics (PDF, talk) (LPOP) A Rule-Based Tool for Analysis and Generation of Graphs Applied to Mason's Marks (PDF, talk) (LPOP) Security Policies in Constraint Handling Rules (PDF, talk)
Frumin, Dan	(LICS) ReLoC: A Mechanised Relational Logic for Fine-Grained Concurrency (PDF, talk)
Fuhs, Carsten	(WST) Improving Static Dependency Pairs for Higher-Order Rewriting (PDF, talk)
Fukui, Kousuke	(IWC) Complete Axiom System of Cluster Algebra (PDF, talk)
Furber, Robert	(LICS) Boolean-Valued Semantics for Stochastic Lambda-Calculus (PDF, talk)
G
Gacek, Andrew	(CAV) The JKind Model Checker (PDF, talk)
Gadducci, Fabio	(LICS) Rewriting with Frobenius (PDF, talk)
Galal, Zeinab	(Linearity/TLLA) Towards a Functional Language for Species of Structures (PDF, talk)
Galdino, André Luiz	(ITP) Formalizing Ring Theory in PVS (short paper) (PDF, talk)
Galesi, Nicola	(SAT) Cops-Robber games and the resolution of Tseitin formulas (PDF, talk) (PC) Resolution and the binary encoding of combinatorial principles (PDF, talk)
Gall, Daniel	(LPOP) Confluence Analysis of Cognitive Models with Constraint Handling Rules (PDF, talk)
Gallagher, John	(ICLP) An iterative approach to precondition inference using constrained Horn clauses (PDF, talk) (WST) Control-Flow Refinement via Partial Evaluation (PDF, talk)
Gallego Arias, Emilio Jesús	(ICLP) Certified Graph View Maintenance with Regular Datalog (PDF, talk)
Galmiche, Didier	(ADSL) Labelled Cyclic Proofs for Separation Logic (PDF, talk) (ARQNL) Labelled Connection-based Proof Search for Multiplicative Intuitionistic Linear Logic (PDF, talk)
Gamble, Carl	(Overture) Multi-modelling of Cooperative Swarms (PDF, talk)
Gamble, Carl	(Overture) Design Space Exploration for Secure Building Control (PDF, talk)
Ganesh, Vijay	(SAT) Machine Learning-based Restart Policy for CDCL SAT Solvers (PDF, talk) (CAV) StringFuzz: A Fuzzer for String Solvers (PDF, talk) (CAV) The Proof Complexity of SMT Solvers (PDF, talk)
Gange, Graeme	(ICLP) An iterative approach to precondition inference using constrained Horn clauses (PDF, talk)
Ganty, Pierre	(HCVS) Tree dimension in verification of constrained Horn clauses (PDF) (LICS) Sound up-to techniques and Complete abstract domains (PDF, talk)
Gao, Pengfei	(CAV) SCInfer: Refinement-based Verification of Software Countermeasures against Side-Channel Attacks (PDF, talk)
Gao, Sicun	(CAV) Delta-Decision Procedures for Exists-Forall Problems over the Reals (PDF, talk)
Gao, Tiantian	(ICLP-DC) Knowledge Authoring and Question Answering via Controlled Natural Language (PDF, talk)
Garbuzov, Dmitri	(ITP) A Formal Equational Theory for Call-By-Push-Value (PDF, talk)
Garcia, Sergio	(FM) Multi-Robot LTL Planning Under Uncertainty (PDF, talk)
Garcia-Contreras, Isabel	(ICLP) Towards Incremental and Modular Context-sensitive Analysis (PDF, talk)
Gardy, Patrick	(SR) Dependences in Strategy Logic (PDF, talk)
Garg, Deepak	(CSF) Types for Information Flow Control: Labeling Granularity and Semantic Models (PDF, talk)
Garlan, David	(FM) IPL: An Integration Property Language for Multi-Model Cyber-Physical Systems (PDF, talk)
Gascón, Adrià	(UNIF) Compressed Term Unification: Results, Applications, Open problems, and Hopes (PDF)
Gastin, Paul	(LICS) Regular Transducer Expressions for Regular Transformations over infinite words (PDF, talk)
Gavanelli, Marco	(RCRA) Logic Programming approaches for routing fault-free and maximally-parallel Wavelength Routed Optical Networks on Chip (Application paper) (PDF, talk)
Gavazzo, Francesco	(LICS) Quantitative Behavioural Reasoning for Higher-order Effectful Programs: Applicative Distances (PDF, talk)
Gay, Simon J.	(WiL) A New Linear Logic for Deadlock-Free Session-Typed Processes (Talk Abstract) (PDF, talk)
Gburek, Daniel	(LICS) Stochastic Shortest Paths and Weight-Bounded Properties in Markov Decision Processes (PDF, talk)
Ge, Cunjing	(PRUV) A New Probabilistic Algorithm for Approximate Model Counting (PDF, talk) (PRUV) VolCE: An Efficient Tool for Solving #SMT(LA) Problems (PDF, talk) (IJCAR) A New Probabilistic Algorithm for Approximate Model Counting (PDF, talk) (IJCAR) Investigating the Existence of Large Sets of Idempotent Quasigroups via Satisfiability Testing (PDF, talk)
Gebser, Martin	(ICLP) Experimenting with robotic intra-logistics domains (PDF, talk) (ICLP) Routing Driverless Transport Vehicles in Car Assembly with Answer Set Programming (PDF, talk)
Geeraerts, Gilles	(MoRe) Safe and Optimal Scheduling of Hard and Soft Tasks (PDF, talk)
Geisler, Signe	(FM) Stepwise Development and Model Checking of a Distributed Interlocking System - using RAISE (PDF, talk)
Genaim, Samir	(WST) Control-Flow Refinement via Partial Evaluation (PDF, talk) (WST) Inference of Linear Upper-Bounds on the Expected Cost by Solving Cost Relations (PDF, talk)
Gencer, Çigdem	(WiL) About the unification type of topological logics over Euclidean spaces (PDF, talk) (UNIF) About the Unification Type of Topological Logics over Euclidean Spaces (PDF, talk)
Genest, Blaise	(LICS) Distribution-based objectives for Markov Decision Processes (PDF, talk)
Genestier, Guillaume	(WST) Termination of Lambda-Pi modulo rewriting using the size-change principle (PDF, talk)
Genet, Thomas	(FSCD) Completeness of Tree Automata Completion (PDF, talk)
Gentilini, Raffaella	(LICS) Rational Synthesis Under Imperfect Information (PDF, talk)
Geoffroy, Guillaume	(LICS) Classical realizability as a classifier for nondeterminism (PDF, talk)
Gericke, Moritz	(AVOCS) Writing a Model Checker in 80 Days: Reusable Libraries and Custom Implementation (PDF, talk)
Geser, Alfons	(WST) Semantic Kachinuki Order (PDF, talk)
Ghani, Neil	(SR) Compositional Game Theory (PDF, talk) (LICS) Compositional game theory (PDF, talk)
Ghardallou, Wided	(REFINE) Programming Without Refinement (PDF, talk)
Ghassabani, Elaheh	(CAV) The JKind Model Checker (PDF, talk)
Ghedira, Khaled	(PRUV) Evidential Group Decision Making Model with Belief-Based Preferences (PDF, talk)
Ghica, Dan	(LICS) The Geometry of Computation-Graph Abstraction (PDF, talk)
Ghilardi, Silvio	(UNIF) Handling Substitutions via Duality (PDF)
Ghorbal, Khalil	(FM) Vector Barrier Certificates and Comparison Systems (PDF, talk)
Ghosh, Shromona	(ADHS) Generating Dominant Strategies for Continuous Two-Player Zero-Sum Games (PDF, talk)
Giacobazzi, Roberto	(CAV) Program Analysis is Harder than Verification: A Computability Perspective (PDF, talk) (LICS) Sound up-to techniques and Complete abstract domains (PDF, talk)
Giacobbe, Mirco	(CAV) Space-time Interpolants (PDF, talk)
Giacomelli, Irene	(CSF) Privacy Risk in Machine Learning: Analyzing the Connection to Overfitting (PDF, talk)
Giannini, Paola	(DCM) A syntactic model of mutation and aliasing (PDF, talk)
Giaquinta, Ruben	(VaVAS) Probabilistic Model Checking for Autonomous Agent Strategy Synthesis - Extended Abstract (PDF, talk)
Giegerich, Robert	(LaSh) Declarative Dynamic Programming with Inverse Coupled Rewrite Systems (PDF, talk)
Giese, Martin	(IJCAR) Industrial Data Access (PDF)
Giesl, Jürgen	(WST) Complexity Analysis for Bitvector Programs (PDF, talk)
Giordano, Laura	(PRUV) Reasoning about exceptions in ontologies: from the lexicographic closure to the skeptical closure (PDF, talk)
Girard, Antoine	(ADHS) Safety Control, a Quantitative Approach (PDF, talk)
Girard, Antoine	(ADHS) Compositional Abstraction-based Synthesis for Cascade Discrete-Time Control Systems (PDF, talk)
Girard, Antoine	(ADHS) Language constrained stabilization of discrete- time switched linear systems: an LMI approach (PDF, talk)
Girard, Antoine	(ADHS) Symbolic Models for Incrementally Stable Switched Systems with Aperiodic Time Sampling (PDF, talk)
Giraudo, Samuele	(HDRA) Generalizations of the associative operad and convergent rewrite systems (PDF, talk)
Giráldez-Cru, Jesus	(SAT) Using Combinatorial Benchmarks to Probe the Reasoning Power of Pseudo-Boolean Solvers (PDF, talk) (SAT) In Between Resolution and Cutting Planes: A Study of Proof Systems for Pseudo-Boolean SAT Solving (PDF, talk)
Giunti, Marco	(DCM) Pointing to Private Names (PDF, talk)
Gleiss, Bernhard	(SAT) Local Soundness for QBF Calculi (PDF, talk)
Gliozzi, Valentina	(PRUV) Reasoning about exceptions in ontologies: from the lexicographic closure to the skeptical closure (PDF, talk)
Gocht, Stephan	(SAT) In Between Resolution and Cutting Planes: A Study of Proof Systems for Pseudo-Boolean SAT Solving (PDF, talk)
Goel, Shubham	(CAV) What’s hard about Boolean Functional Synthesis? (PDF, talk)
Goeminne, Aline	(MoRe) Constraint Problem for Weak Subgame Perfect Equilibria with omega-regular Boolean Objectives (PDF, talk)
Goertzel, Zarathustra	(ITP) ProofWatch: Watchlist Guidance for Large Theories in E (PDF, talk)
Gomez-Zamalloa, Miguel	(FM) SDN-Actors: Modeling and Verification of SDN Programs (PDF, talk) (CAV) Constrained Dynamic Partial Order Reduction (PDF, talk)
Gooi, H. B.	(ADHS) Multi-Energy Scheduling Using a Hybrid Systems Approach (PDF, talk)
Gore, Rajeev	(IJCAR) Well-Founded Unions (PDF, talk)
Gorzny, Jan	(UITP) Partial Regularization of First-Order Resolution Proofs (PDF, talk)
Goubault, Eric	(CAV) Inner and Outer Approximating Flowpipes for Delay Differential Equations (PDF, talk)
Gouveia, Filipe	(ICLP-DC) Model Revision of Logical Regulatory Networks using Logic-based Tools (PDF, talk)
Grabmayer, Clemens	(TERMGRAPH) Modeling Terms by Graphs with Structure Constraints (Two Illustrations) (PDF)
Graham-Lengrand, Stephane	(SMT) Centralizing Equality Reasoning in MCSAT (PDF, talk)
Grayson, Daniel	(ITP) Voevodsky's work on formalization of proofs and the foundations of mathematics (PDF)
Grebing, Sarah	(UITP) Adding Text-Based Interaction to a Direct-Manipulation Interface for Program Verification -- Lessons Learned (PDF, talk)
Greco, Giuseppe	(ITP) Software tool support for modular reasoning in modal logics of actions (PDF, talk)
Greiner, Johannes	(IJCAR) Complexity of Combinations of Qualitative Constraint Satisfaction Problems (PDF, talk)
Griffin, Timothy G.	(ITP) An Agda Formalization of Üresin & Dubois' Asynchronous Fixed-Point Theory (PDF, talk)
Griggio, Alberto	(SAT) Experimenting on Solving Nonlinear Integer Arithmetic with Incremental Linearization (PDF, talk)
Grimaud, Gilles	(AVOCS) Proof-Oriented Design of a Separation Kernel with Minimal Trusted Computing Base (PDF, talk)
Grishchenko, Ilya	(CAV) Foundations and Tools for the Static Analysis of Ethereum smart contracts (PDF)
Grohe, Martin	(LICS) Definable decompositions for graphs of bounded linear cliquewidth (PDF, talk)
Gross, Jason	(ITP) Reification by Parametricity (PDF, talk) (Coq) Teaching Your Rooster to Crow in C (PDF, talk)
Grosu, Radu	(VaVAS) Adaptive Neighborhood Resizing for Stochastic Reachability in Multi-Agent Systems (PDF, talk)
Grädel, Erich	(LICS) Preface (PDF)
Grégoire, Benjamin	(CSF) Formal Security Proof of CMAC and its Variants (PDF, talk) (CSF) Secure compilation of side-channel countermeasures: the case of cryptographic “constant-time” (PDF, talk)
Gu, Ronghui	(CAV) Partial Order Aware Concurrency Sampling (PDF, talk)
Guarneri, Riccardo	(RCRA) Optimal Fault-Tolerant Placement of Relay Nodes in a Mission Critical Wireless Network (PDF, talk)
Guatto, Adrien	(LICS) A Generalized Modality for Recursion (PDF, talk)
Gueguen, Herve	(ADHS) Hierarchical Model Predictive Control for Building Energy Management of Hybrid Systems (PDF, talk)
Guerrieri, Giulio	(Linearity/TLLA) The Bang Calculus and the Two Girard's Translations (PDF, talk) (ITRS) Towards a Semantic Measure of the Execution Time in Call-by-Value lambda-Calculus (PDF, talk)
Guglielmi, Alessio	(TYDI) Two Unifying Structural Principles (PDF, talk)
Guha, Shibashis	(MoRe) Safe and Optimal Scheduling of Hard and Soft Tasks (PDF, talk) (FM) Timed Vacuity (PDF, talk)
Guldstrand Larsen, Kim	(FM) 20 Years of Real Real Time Model Validation (PDF) (FM) Optimal and Robust Controller Synthesis Using Energy Timed Automata with Uncertainty (PDF, talk) (CAV) Start Pruning When Time Gets Urgent: Partial Order Reduction for Timed Systems (PDF, talk)
Gupta, Aarti	(CAV) Syntax-Guided Termination Analysis (PDF, talk) (CAV) Exploiting Synchrony and Symmetry in Relational Verification (PDF, talk) (CAV) Lazy Self-Composition for Security Verification (PDF, talk)
Gupta, Gopal	(ICLP) Cumulative Scoring-based Induction of Default Theories (PDF, talk) (ICLP) Constraint Answer Set Programming without Grounding (PDF, talk)
Gupta, Piyush	(WST) Verification of Rewriting-based Query Optimizers (PDF, talk)
Gupta, Shubhani	(SAT) Effective use of SMT solvers for Program Equivalence Checking through Invariant Sketching and Query Decomposition (PDF, talk)
Gurfinkel, Arie	(SMT) Discovering Universally Quantified Solutions for Constrained Horn Clauses (PDF, talk)
Guth, Dwight	(CSF) KEVM: A Complete Formal Semantics of the Ethereum Virtual Machine (PDF, talk)
Gutierrez, Julian	(SR) Local Equilibria in Logic-Based Multi-Player Games (PDF, talk)
Guttman, Joshua	(FCS) Homomorphisms and Minimality for Enrich-by-Need Security Analysis (PDF, talk)
Guéneau, Armaël	(Coq) Procrastination, A proof engineering technique (PDF, talk)
Gyorgy, Andras	(FM) A Weakness Measure for GR(1) Formulae (PDF, talk)
Gérard, Ulysse	(LFMTP) Functional programming with λ-tree syntax: a progress report (PDF, talk) (LFMTP) Computation-as-deduction in Abella: work in progress (PDF, talk)
Gómez-Gutiérrez, David	(ADHS) Observability of Linear Hybrid Systems with Unknown Inputs and Discrete Dynamics Modeled by Petri Nets (PDF, talk)
Głuch, Grzegorz	(LICS) Can One Escape Red Chains? Regular Path Queries Determinacy is Undecidable. (PDF, talk)
H
Haagh, Helene	(CSF) Computer-aided proofs for multiparty computation with active security (PDF, talk)
Haak, Anselm	(LICS) Model-Theoretic Characterizations of Boolean and Arithmetic Circuit Classes of Small Depth (PDF, talk)
Hadzihasanovic, Amar	(FSCD) A diagrammatic axiomatisation of fermionic quantum circuits (PDF, talk) (LICS) Two complete axiomatisations of pure-state qubit quantum computing (PDF, talk) (HDRA) Merge-bicategories: towards semi-strictification of higher categories (PDF, talk)
Haehn, Rebecca	(SCSC) Evaluation of Equational Constraints for CAD in SMT Solving (PDF, talk)
Hage, Nohra	(IWC) Coherence of monoids by insertions (PDF, talk) (HDRA) String data structures for Chinese monoids (PDF, talk)
Hahn, Christopher	(CAV) Model Checking Quantitative Hyperproperties (PDF, talk) (CAV) Synthesizing Reactive Systems from Hyperproperties (PDF, talk)
Hahn, Michael	(LICS) Wreath Products of Distributive Forest Algebras (PDF, talk)
Hajdu, Ákos	(AVOCS) Backward reachability analysis for timed automata with data variables (PDF, talk)
Hajnal, Matej	(VEMDP) Executable Biochemical Space for Specification and Analysis of Biochemical Systems (PDF, talk)
Hall, Brendan	(F-IDE) The CLEAR Way To Transparent Formal Methods (PDF, talk)
Hamana, Makoto	(FSCD) Confluence Competition 2018 (PDF)
Hammond, Kevin	(ICLP) Proof-relevant Horn Clauses for Dependent Type Inference and Term Synthesis (PDF, talk)
Hammoudeh, Zayd	(SAT) Fast Sampling of Perfectly Uniform Satisfying Assignments (PDF, talk) (SAT) Fast and Flexible Probabilistic Model Counting (PDF, talk)
Hannula, Miika	(IJCAR) Automated Reasoning about Key Sets (PDF, talk)
Hao, Jianye	(FM) Falsification of Cyber-Physical Systems Using Deep Reinforcement Learning (PDF, talk)
Harper, Robert	(ITP) Verified Tail Bounds for Randomized Programs (PDF, talk) (HoTT/UF) Cubical Computational Type Theory (PDF, talk) (LFMTP) The RedPRL Proof Assistant (PDF) (LICS) Guarded Computational Type Theory (PDF, talk)
Harrenstein, Paul	(SR) Local Equilibria in Logic-Based Multi-Player Games (PDF, talk)
Harris, William	(HCVS) Solving Constrained Horn Clauses Using Dependence-Disjoint Expansions (PDF, talk)
Harrison, John	(ITP) Mike Gordon: Tribute to a pioneer in theorem proving and formal verification (PDF)
Hartmanns, Arnd	(MoRe) Multiple Objectives and Cost Bounds in MDP (PDF, talk)
Hasanbeig, Mohammadhosein	(MoRe) Logically-Constrained Reinforcement Learning (PDF, talk)
Hasegawa, Masahito	(Linearity/TLLA) From Linear Logic to Cyclic Sharing (PDF, talk)
Haslbeck, Max W.	(ITP) Verified Analysis of Random Binary Tree Structures (PDF, talk) (Isabelle) Formal Verification of Bounds for the LLL Basis Reduction Algorithm (PDF, talk)
Haslbeck, Maximilian P. L.	(IJCAR) Verifying Asymptotic Time Complexity of Imperative Programs in Isabelle (PDF, talk)
Hassan, Mostafa	(CAV) MaxSMT-Based Type Inference for Python 3 (PDF, talk)
Hassler, Malte Sophian	(Isabelle) Hilbert Meets Isabelle: Formalisation of the DPRM Theorem in Isabelle (PDF, talk)
Hasuo, Ichiro	(ADHS) Bounding Errors Due to Switching Delays in Incrementally Stable Switched Systems (PDF, talk)
Hautem, Quentin	(MoRe) Parameterized complexity of games with monotonically ordered omega-regular objectives (PDF, talk)
Hawes, Nick	(VaVAS) Policy Generation with Probabilistic Guarantees for Long-term Autonomy of a Mobile Service Robot (PDF, talk)
Haxthausen, Anne E.	(FM) Stepwise Development and Model Checking of a Distributed Interlocking System - using RAISE (PDF, talk)
Hayes, Ian J.	(FM) Encoding fairness in a synchronous concurrent program algebra (PDF, talk) (REFINE) Challenges of specifying concurrent program components (PDF, talk)
He, Jinlong	(CAV) Android Stack Machine (PDF, talk)
He, Yilun	(Isabelle) PaMpeR: A Proof Method Recommendation System for Isabelle/HOL (PDF, talk)
Heath, David	(HCVS) Solving Constrained Horn Clauses Using Dependence-Disjoint Expansions (PDF, talk)
Hecher, Markus	(SAT) Exploiting Treewidth for Projected Model Counting and its Limits (PDF, talk)
Hedges, Jules	(SR) Compositional Game Theory (PDF, talk) (LICS) Compositional game theory (PDF, talk)
Heemels, Maurice	(ADHS) A switched system approach to optimize mixing of fluids (PDF, talk)
Hehner, Eric	(WST) Objective and Subjective Specifications (PDF, talk) (REFINE) A Theory of Lazy Imperative Timing (PDF, talk)
Heijltjes, Willem	(FSCD) Proof nets for bi-intuitionistic linear logic (PDF, talk) (TYDI) An introduction to deep inference (PDF, talk) (TYDI) Deep-Inference Intersection Types (PDF, talk)
Heiter, Edith	(ITP) Verification of PCP-Related Computational Reductions in Coq (PDF, talk)
Helfer, Joseph	(HoTT/UF) First-order homotopical logic and Grothendieck fibrations (PDF, talk)
Hencey, Brandon	(ADHS) Compositional Analysis of Hybrid Systems Defined Over Finite Alphabets (PDF, talk)
Hensel, Jera	(WST) Complexity Analysis for Bitvector Programs (PDF, talk)
Henzinger, Monika	(CAV) Symbolic Algorithms for Graphs and Markov Decision Processes with Fairness Objectives (PDF, talk)
Henzinger, Thomas A.	(SR) Infinite-Duration Richman Bidding Games (PDF, talk) (CAV) Reachable Set Over-approximation for Nonlinear Systems Using Piecewise Barrier Tubes (PDF, talk) (CAV) Space-time Interpolants (PDF, talk) (LICS) A Theory of Register Monitors (PDF, talk)
Herbelin, Hugo	(HoTT/UF) The definitional symmetric cubical structure of types in type theory with equality defined by abstraction over an interval (PDF, talk)
Hermenegildo, Manuel V.	(ICLP) Towards Incremental and Modular Context-sensitive Analysis (PDF, talk) (ICLP) Towards Static Performance Guarantees for Programs with Run-time Checks (PDF, talk) (LCC) A General Equational Framework for Static Profiling of Parametric Resource Usage (PDF, talk)
Herrera, Christian	(WPTE) Verification of Ada Programs with AdaHorn (PDF, talk)
Hess, Andreas Viktor	(CSF) A Typing Result for Stateful Protocols (PDF, talk)
Heule, Marijn	(VEMDP) Computing Properties of Stable Configurations of Thermodynamic Binding Networks (PDF, talk) (SAT) Computable Short Proofs (PDF, talk) (IJCAR) Extended Resolution Simulates DRAT (PDF, talk) (POS) The Effect of Scrambling CNFs (PDF, talk)
Hiet, Guillaume	(FM) Modular Verification of Programs with Effects and Effect Handlers in Coq (PDF, talk)
Hildenbrandt, Everett	(CSF) KEVM: A Complete Formal Semantics of the Ethereum Virtual Machine (PDF, talk)
Hinde, Luke	(PC) Size, Cost and Capacity: A Semantic Technique for Hard Random QBFs (PDF)
Hirokawa, Nao	(IJCAR) Cops and CoCoWeb: Infrastructure for Confluence Tools (PDF, talk)
Hirokawa, Nao	(FSCD) Confluence Competition 2018 (PDF)
Hirschi, Lucca	(CSF) Automated Unbounded Verification of Stateful Cryptographic Protocols with Exclusive OR (PDF, talk)
Hirschkoff, Daniel	(LICS) Eager Functions as Processes (PDF, talk)
Hirschowitz, Tom	(LICS) What's in a game? A theory of game models (PDF, talk)
Ho, Son	(IJCAR) Proof-Producing Synthesis of CakeML with I/O and Local State from Monadic HOL Functions (PDF, talk)
Ho Thanh, Cédric	(HDRA) The equivalence between opetopic sets and many-to-one polygraphs (PDF, talk)
Hoang, Thai Son	(VaVAS) Policing Functions for Machine Learning Systems (PDF, talk)
Hoenicke, Jochen	(IJCAR) Efficient Interpolation for the Theory of Arrays (PDF, talk)
Hofbauer, Dieter	(WST) Semantic Kachinuki Order (PDF, talk) (WST) Embracing Infinity - Termination of String Rewriting by Almost Linear Weight Functions (PDF, talk)
Hoffmann, Jan	(LICS) Work Analysis with Resource-Aware Session Types (PDF, talk)
Hoffmann, Ruth	(VaVAS) Probabilistic Model Checking for Autonomous Agent Strategy Synthesis - Extended Abstract (PDF, talk)
Hogan, Kyle	(CSF) Secure Boot and Remote Attestation in the Sanctum Processor (PDF)
Holik, Lukas	(LaSh) Lazy Automata Techniques for WS1S (PDF, talk)
Hoos, Holger	(QBF) Portfolio-Based Algorithm Selection for Circuit QBFs (PDF, talk)
Horacek, Jan	(SCSC) Refutation of Products of Linear Polynomials (PDF, talk)
Horne, Ross	(TYDI) Truely Concurrent Processes in the Calculus of Structures (PDF, talk) (LICS) Quasi-Open Bisimilarity with Mismatch is Intuitionistic (PDF, talk)
Hou Favonia, Kuen-Bang	(HoTT/UF) Cubical Computational Type Theory (PDF, talk) (LFMTP) Cubical Computational Type Theory and RedPRL (PDF) (LFMTP) The RedPRL Proof Assistant (PDF) (LICS) Cellular Cohomology in Homotopy Type Theory (PDF, talk)
Houshmand, Arian	(ADHS) Hybrid System Modeling of Multi-Agent Coverage Problems with Energy Depletion and Repletion (PDF, talk)
Hoxha, Bardh	(ADHS) Mission Planning for Multiple Vehicles with Temporal Specifications using UxAS (PDF, talk)
Hrushovski, Ehud	(LICS) Polynomial Invariants for Affine Programs (PDF, talk)
Hsu, Justin	(CAV) Constraint-Based Synthesis of Coupling Proofs (PDF, talk)
Hu, Hai	(NLCS) Automated Reasoning from Polarized Parse Trees (PDF, talk)
Hu, Qinheping	(CAV) Syntax Guided Synthesis with Quantitative Syntactic Objectives (PDF, talk)
Hu, Shuwei	(ITP) Verified Memoization and Dynamic Programming (PDF, talk)
Huang, Kai	(FM) Resource-aware Design for Reliable Autonomous Applications with Multiple Periods (PDF, talk)
Huang, Pei	(IJCAR) Investigating the Existence of Large Sets of Idempotent Quasigroups via Satisfiability Testing (PDF, talk)
Huang, Zhenqi	(FM) Approximate Partial Order Reduction (PDF, talk)
Huber, Simon	(LICS) On Higher Inductive Types in Cubical Type Theory (PDF, talk)
Huffman, Brian	(CAV) Continuous formal verification of Amazon s2n (PDF, talk)
Hughes, Dominic	(TYDI) Some incoherent musings on deep inference and combinatorial proofs (PDF, talk) (LICS) Unification nets: canonical proof net quantifiers (PDF, talk)
Humbel, Lukas	(ITP) Physical addressing on real hardware in Isabelle/HOL (PDF, talk)
Hustadt, Ullrich	(PAAR) Evaluating Pre-Processing Techniques for the Separated Normal Form for Temporal Logics (PDF, talk)
Hym, Samuel	(AVOCS) Proof-Oriented Design of a Separation Kernel with Minimal Trusted Computing Base (PDF, talk)
Hyvärinen, Antti	(VSTTE) Lattice-Based Refinement in Bounded Model Checking (PDF, talk)
Höfner, Peter	(ITP) Backwards and Forwards with Separation Logic (PDF, talk)
Hölzl, Johannes	(ITP) MDP + TA = PTA: Probabilistic Timed Automata, Formalized (Short Paper) (PDF, talk)
I
Icard, Thomas	(NLCS) Automated Reasoning from Polarized Parse Trees (PDF, talk)
Idziak, Pawel	(LICS) Satisfiability in multi-valued circuits (PDF, talk)
Ignatiev, Alexey	(SAT) PySAT: A Python Toolkit for Prototyping with SAT Oracles (PDF, talk) (IJCAR) A SAT-Based Approach to Learn Explainable Decision Sets (PDF, talk) (PC) On Dual-Rail Based MaxSAT Solving (PDF, talk)
Igne, Federico	(ICLP) MASP-Reduce: a proposal for distributed computation of stable models (PDF, talk)
Iguernlala, Mohamed	(SMT) Alt-Ergo 2.2 (PDF, talk)
Ikebuchi, Mirai	(FSCD) On repetitive right application of B-terms (PDF, talk) (Coq) ComplCoq: Rewrite Hint Construction with Completion Procedures (PDF, talk)
Inclezan, Daniela	(ICLP) An ASP Methodology for Understanding Narratives about Stereotypical Activities (PDF, talk)
Inoue, Katsumi	(ICLP) Learning Commonsense Knowledge through Interactive Dialogue (PDF, talk) (ICLP) Exploiting Answer Set Programming with External Sources for Meta-Interpretive Learning (PDF, talk)
Interlandi, Matteo	(ICLP) Declarative Algorithms in Datalog with Aggregates: user-friendly formal semantics conducive to performance and scalability (PDF, talk)
Iosif, Radu	(ADSL) The Complexity of Prenex Separation Logic with One Selector (PDF, talk) (AVOCS) An Entailment Checker for Separation Logic with Inductive Definitions (PDF, talk)
Iraci, Grant	(FM) IPL: An Integration Property Language for Multi-Model Cyber-Physical Systems (PDF, talk)
Ireland, Murray	(VaVAS) Probabilistic Model Checking for Autonomous Agent Strategy Synthesis - Extended Abstract (PDF, talk)
Irfan, Ahmed	(SAT) Experimenting on Solving Nonlinear Integer Arithmetic with Incremental Linearization (PDF, talk)
Isabel, Miguel	(CAV) Constrained Dynamic Partial Order Reduction (PDF, talk)
Iser, Markus	(POS) A Problem Meta-Data Library for Research in SAT (PDF, talk)
Israney, Ankush	(ICLP) An ASP Methodology for Understanding Narratives about Stereotypical Activities (PDF, talk)
Itcus, Corina	(VEMDP) Computational Approaches for the Programmed Assembly of Nanocellulose Meshes (PDF, talk)
Ivrii, Alexander	(SAT) Finding all Minimal Safe Inductive Sets (PDF, talk)
J
Jaax, Stefan	(CAV) Peregrine: A Tool for the Analysis of Population Protocols (PDF, talk) (LICS) Black Ninjas in the Dark: Formal Analysis of Population Protocols (PDF)
Jacob-Rao, Rohan	(FSCD) Index-Stratified Types (PDF, talk)
Jacobs, Ceriel	(IJCAR) Efficient Model Construction for Horn Logic with VLog: System Description (PDF, talk)
Jacomme, Charlie	(CSF) An extensive formal analysis of multi-factor authentication protocols (PDF, talk)
Jaffar, Joxan	(ICLP) Shape Neutral Analysis of Graph-based Data-structures (PDF, talk)
Jagtap, Pushpak	(ADHS) Compositional Abstraction-based Synthesis for Cascade Discrete-Time Control Systems (PDF, talk)
Jain, Achin	(ADHS) Data-Driven Switched Affine Modeling for Model Predictive Control (PDF, talk)
Jakubuv, Jan	(ITP) ProofWatch: Watchlist Guidance for Large Theories in E (PDF, talk)
Jamali, Sima	(SAT) Centrality-Based Improvements to CDCL Heuristics (PDF, talk)
Janku, Petr	(LaSh) Lazy Automata Techniques for WS1S (PDF, talk)
Janota, Mikolas	(SAT) Circuit-based Search Space Pruning in QBF (PDF, talk)
Jansen, Christina	(CAV) Let this Graph be your Witness! An Attestor for Verifying Java Pointer Programs (PDF, talk)
Janson, Christian	(CSF) Backdoored Hash Functions: Immunizing HMAC and HKDF (PDF, talk)
Janssens, Gerda	(QBF) A Grounder From Second-Order Logic To QBF (PDF, talk)
Jantsch, Simon	(ITP) Verifying the LTL to Büchi Automata Translation via Very Weak Alternating Automata (PDF, talk)
Jaskelioff, Mauro	(LICS) Syntax and Semantics for Operations with Scopes (PDF, talk)
Jeandel, Emmanuel	(LICS) A Complete Axiomatisation of the ZX-Calculus for Clifford+T Quantum Mechanics (PDF, talk) (LICS) Diagrammatic Reasoning beyond Clifford+T Quantum Mechanics (PDF, talk)
Jeannerod, Nicolas	(IJCAR) Deciding the First-Order Theory of an Algebra of Feature Trees with Updates (PDF, talk)
Jebelean, Tudor	(SCSC) Techniques for Natural-style Proofs in Elementary Analysis (PDF, talk)
Jecker, Ismaël	(SR) Beyond admissibility: Dominance between chains of strategies (PDF, talk)
Jensen, Peter Gjøl	(CAV) Start Pruning When Time Gets Urgent: Partial Order Reduction for Timed Systems (PDF, talk)
Jeppu, Yogananda	(F-IDE) The CLEAR Way To Transparent Formal Methods (PDF, talk)
Jeřábek, Emil	(PC) Bounded induction without parameters (PDF, )
Jha, Somesh	(CAV) Semantic Adversarial Deep Learning (PDF, talk) (CSF) Privacy Risk in Machine Learning: Analyzing the Connection to Overfitting (PDF, talk)
Jha, Susmit	(ADHS) Learning and Verification of Feedback Control Systems Using Feedforward Neural Networks (PDF, talk)
Ji, Kailiang	(CAV) On the Completeness of Verifying Message Passing Programs under Bounded Asynchrony (PDF, talk)
Jia, Limin	(CSF) Knowledge-based Security of Dynamic Secrets for Reactive Programs (PDF, talk)
Jia, Yifan	(FM) Towards `Verifying' a Water Treatment System (PDF, talk)
Jiang, Jiaming	(FCS) An Expressive, Flexible and Uniform Logical Formalism for Attribute-based Access Control (PDF, talk) (Linearity/TLLA) On the Lambek Calculus with an Exchange Modality (PDF, talk)
Johann, Patricia	(LICS) A General Framework for Relational Parametricity (PDF, talk)
Johnson, Robert F.	(VEMDP) Using Transitivity and Modularity in Chemical Reaction Network Bisimulation (PDF, talk)
Johnson, Taylor T	(ADHS) Reachability Analysis for One Dimensional Linear Parabolic Equation (PDF, talk)
Johnson, Taylor T	(ADHS) Mission Planning for Multiple Vehicles with Temporal Specifications using UxAS (PDF, talk)
Jomaa, Najes	(AVOCS) Proof-Oriented Design of a Separation Kernel with Minimal Trusted Computing Base (PDF, talk)
Joosten, Sebastiaan	(ITP) A Formalization of the LLL Basis Reduction Algorithm (PDF, talk) (WST) A Perron-Frobenius Theorem for Jordan Blocks for Complexity Proving (PDF, talk)
Jouannaud, Jean-Pierre	(TERMGRAPH) Drags: an algebraic framework for graph rewriting (PDF, talk) (WST) GPO: A Path Ordering for Graphs (PDF, talk)
Jouanny, Théo	(AVOCS) Climbing the Software Assurance Ladder - Practical Formal Verification for Reliable Software (PDF, talk)
Jovanović, Dejan	(ADSL) Sloth: Separation Logic and Theories via Small Models (PDF, talk) (IJCAR) A Separation Logic with Data: Small Models and Automation (PDF, talk)
Jungers, Raphaël M.	(ADHS) Computing Controlled Invariant Sets for Hybrid Systems with Applications to Model-Predictive Control (PDF, talk)
Jungers, Raphaël M.	(ADHS) On invariance and reachability on semialgebraic sets for linear dynamics (PDF, talk)
Junges, Sebastian	(MoRe) Multiple Objectives and Cost Bounds in MDP (PDF, talk)
Jurdzinski, Marcin	(LICS) A pseudo-quasi-polynomial algorithm for solving mean-payoff parity games (PDF, talk)
Järvisalo, Matti	(ICLP) Cautious Reasoning in ASP via Minimal models and Unsatisfiable Cores (PDF, talk)
K
Kabir, Ifaz	(CAV) StringFuzz: A Fuzzer for String Solvers (PDF, talk)
Kaestner, Daniel	(FM) On Software Safety, Security, and Abstract Interpretation (PDF, talk)
Kafle, Bishoksan	(ICLP) An iterative approach to precondition inference using constrained Horn clauses (PDF, talk)
Kahl, Patrick	(ICLP) Epistemic Logic Programs with World View Constraints (PDF, talk)
Kahl, Wolfram	(ITP) CalcCheck: A Proof Checker for Teaching the “Logical Approach to Discrete Math” (PDF, talk) (TERMGRAPH) Semantics-Preserving DPO-Based Term Graph Rewriting (PDF, talk)
Kaliszyk, Cezary	(ITP) Towards Formal Foundations for Game Theory (short paper) (PDF, talk)
Kalouli, Aikaterini-Lida	(NLCS) Graph Knowledge Representations for SICK (PDF, talk)
Kamareddine, Fairouz	(LFMTP) What Does This Notation Mean Anyway? BNF-Style Notation as it is actually used (PDF, talk)
Kamburjan, Eduard	(AVOCS) Detecting Deadlocks in Formal System Models with Condition Synchronization (PDF, talk)
Kaminski, Roland	(ICLP) Temporal Answer Set Programming on Finite Traces (PDF, talk)
Kaminski, Tobias	(ICLP) Exploiting Answer Set Programming with External Sources for Meta-Interpretive Learning (PDF, talk)
Kanazawa, Yoshiaki	(IWC) Convergence of Simultaneously and Sequentially Unraveled TRSs for Normal Conditional TRSs (PDF, talk) (WPTE) On Transforming Functions Accessing Global Variables into Logically Constrained Term Rewriting Systems (PDF, talk)
Kanovich, Max	(ADSL) On the Complexity of Pointer Arithmetic in Separation Logic (PDF, talk) (IJCAR) A Logical Framework with Commutative and Non-Commutative Subexponentials (PDF, talk) (FCS) Statistical Model Checking of Guessing and Timing Attacks on Distance-bounding Protocols (PDF, talk)
Kaposi, Ambrus	(FSCD) A Syntax for Higher Inductive-Inductive Types (PDF, talk)
Kapron, Bruce	(LICS) Type-two polynomial-time and restricted lookahead. (PDF, talk)
Karbyshev, Aleksandr	(CSF) Computer-aided proofs for multiparty computation with active security (PDF, talk)
Karpiński, Michał	(POS) Competitive Sorter-based Encoding of PB-Constraints into SAT (PDF, talk)
Katelaan, Jens	(ADSL) Sloth: Separation Logic and Theories via Small Models (PDF, talk) (IJCAR) A Separation Logic with Data: Small Models and Automation (PDF, talk)
Katoen, Joost-Pieter	(MoRe) Multiple Objectives and Cost Bounds in MDP (PDF, talk) (FM) Verifying Auto-Generated C Code from Simulink (PDF, talk) (FM) Formal Verification of Automotive Simulink Controller Models: Empirical Technical Challenges, Evaluation and Recommendations (PDF, talk) (CAV) Monitoring CTMCs By Multi-Clock Timed Automata (PDF, talk) (CAV) Sound Value Iteration (PDF, talk) (CAV) Let this Graph be your Witness! An Attestor for Verifying Java Pointer Programs (PDF, talk)
Kauers, Manuel	(SCSC) A Practical Polynomial Calculus for Arithmetic Circuit Verification (PDF, talk) (SAT) Symmetries for QBF (PDF, talk) (PC) The Symmetry Rule for Quantified Boolean Formulas (PDF)
Kazakov, Yevgeny	(IJCAR) Enumerating Justifications using Resolution (PDF, talk)
Keller, Chantal	(ITP) A Coq formalisation of SQL’s execution engines (PDF, talk)
Kellison, Ariel	(WiL) On Expanding Standard Notions of Constructivity (PDF, talk)
Kelmendi, Edon	(CAV) Value Iteration for Simple Stochastic Games: Stopping Criterion and Learning Algorithm (PDF, talk)
Kerjean, Marie	(Linearity/TLLA) Models of Linear Logic based on the Schwartz epsilon product (PDF, talk) (LICS) A Logical Account for Linear Partial Differential Equations (PDF, talk)
Kesner, Delia	(DCM) Quantitative Types: from Foundations to Applications (PDF) (LFMTP) A fresh view of call-by-need (PDF) (ITRS) Quantitative Types: from Foundations to Applications (PDF)
Kesseli, Pascal	(CAV) JBMC: A Bounded Model Checking Tool for Verifying Java Bytecode (PDF, talk) (CAV) Counterexample Guided Inductive Synthesis Modulo Theories (PDF, talk)
Khan, Sharjeel	(Linearity/TLLA) Formalization of Automated Trading Systems in a Concurrent Linear Framework (PDF, talk)
Khanna, Dhriti	(FM) Dynamic Symbolic Verification of MPI Programs (PDF, talk) (DS-FM) Analysis and Verification of Message Passing based Parallel Programs (PDF, talk)
Khazem, Kareem	(CAV) Model Checking Boot Code from AWS Data Centers (PDF, talk)
Khouzani, Mhr	(CSF) Symbolic Side-Channel Analysis for Probabilistic Programs (PDF, talk)
Kieronski, Emanuel	(LICS) Unary negation fragment with equivalence relations has the finite model property (PDF, talk)
Kiesl, Benjamin	(IJCAR) Extended Resolution Simulates DRAT (PDF, talk)
Kimura, Daisuke	(ADSL) Cyclic Theorem Prover for Separation Logic by Magic Wand (PDF, talk)
Kirkeby, Maja H.	(IWC) Confluence in Constraint Handling Rules (PDF)
Kissinger, Aleks	(LICS) Rewriting with Frobenius (PDF, talk)
Kjellerstrand, Håkan	(LPOP) A Picat-based XCSP Solver - from Parsing, Modeling, to SAT Encoding (PDF, talk) (RCRA) Encoding PB Constraints into SAT via Binary Adders and BDDs -- Revisited (PDF, talk)
Klein, Gerwin	(ITP) Backwards and Forwards with Separation Logic (PDF, talk) (ITP) Program Verification in the Presence of Cached Address Translation (PDF, talk)
Klemen, Maximiliano	(ICLP) Towards Static Performance Guarantees for Programs with Run-time Checks (PDF, talk) (LCC) A General Equational Framework for Static Profiling of Parametric Resource Usage (PDF, talk)
Klop, Jan Willem	(FSCD) Decreasing diagrams with two labels are complete for confluence of countable systems (PDF, talk)
Kneis, Joachim	(LaSh) Courcelle’s Theorem – A Game-Theoretic Approach (PDF, talk)
Knop, Alexander	(PC) Branching Program Complexity of Canonical Search Problems and Proof Complexity of Formulas (PDF, talk)
Knüppel, Alexander	(F-IDE) Experience Report on Formally Verifying Parts of OpenJDK's API with KeY (PDF, talk) (ITP) Understanding Parameters of Deductive Verification: An Empirical Investigation of KeY (PDF, talk)
Kobayashi, Naoki	(HOR) On Two Kinds of Higher-Order Model Checking and Higher-Order Program Verification (PDF)
Kochemazov, Stepan	(SAT) ALIAS: A Modular Tool for Finding Backdoors for SAT (PDF, talk)
Koepke, Peter	(UITP) Text-Orientated Formal Mathematics (PDF, talk)
Kohl, Christina	(FSCD) ProTeM: A Proof Term Manipulator (PDF, talk)
Kohlhase, Michael	(IJCAR) Theories as Types (PDF, talk)
Kokke, Wen	(Linearity/TLLA) Taking Linear Logic Apart (PDF, talk)
Kolechkina, Alla G.	(ADHS) A controlled sewer system should be treated as a sampled data system with events (PDF, talk)
Kolokolova, Antonina	(CAV) The Proof Complexity of SMT Solvers (PDF, talk) (PC) Complexity of expander-based reasoning and the power of monotone proofs (PDF, talk)
Komauli, Francesco	(LFMTP) Property-Based Testing of Abstract Machines: an Experience Report (PDF, talk)
Komendantskaya, Ekaterina	(HCVS) Towards Coinductive Theory Exploration in Horn Clause Logic: Extended Abstract (PDF, talk) (ICLP) Proof-relevant Horn Clauses for Dependent Type Inference and Term Synthesis (PDF, talk) (PARIS) Coinductive Uniform Proofs: An Extended Abstract (PDF, talk)
Kong, Hui	(CAV) Reachable Set Over-approximation for Nonlinear Systems Using Piecewise Barrier Tubes (PDF, talk)
Kong, Soonho	(CAV) Delta-Decision Procedures for Exists-Forall Problems over the Reals (PDF, talk)
Konnov, Igor	(TLA) BMCMT: Bounded Model Checking of TLA+ Specifications with SMT (PDF)
Kop, Cynthia	(WST) Improving Static Dependency Pairs for Higher-Order Rewriting (PDF, talk) (HOR) Automatic Termination Analysis Using WANDA (PDF)
Kordy, Barbara	(CSF) Guided design of attack trees: a system-based approach (PDF, talk)
Korneev, Svyatoslav	(SAT) Constrained Image Generation Using Binarized Neural Networks with Decision Procedures (PDF, talk)
Korovin, Konstantin	(IJCAR) An abstraction-refinement framework for reasoning with large theories (PDF, talk)
Korten, Till	(VEMDP) Formal Verification of Network-Based Biocomputation Circuits (PDF, talk)
Koskinen, Eric	(LICS) Dependent Temporal Effects and Fixpoint Logic for Verification (PDF, talk)
Kotelnikov, Evgenii	(IJCAR) A FOOLish Encoding of the Next State Relations of Imperative Programs (PDF, talk) (PAAR) TFX: The TPTP Extended Typed First-order Form (PDF, talk)
Kotsireas, Ilias	(SCSC) Hard Combinatorial Problems: A Challenge for Satisfiability (PDF, talk)
Kovacs, Laura	(IJCAR) A FOOLish Encoding of the Next State Relations of Imperative Programs (PDF, talk)
Kovács, András	(FSCD) A Syntax for Higher Inductive-Inductive Types (PDF, talk)
Kovásznai, Gergely	(SMT) Puli - A Problem-Specific OMT Solver (PDF, talk)
Kozen, Dexter	(LICS) Boolean-Valued Semantics for Stochastic Lambda-Calculus (PDF, talk)
Kragl, Bernhard	(CAV) Layered Concurrent Programs (PDF)
Kraus, Nicolai	(LICS) Free Higher Groups in Homotopy Type Theory (PDF, talk)
Krebbers, Robbert	(LICS) ReLoC: A Mechanised Relational Logic for Fine-Grained Concurrency (PDF, talk)
Krebs, Andreas	(LICS) Wreath Products of Distributive Forest Algebras (PDF, talk)
Kremer, Gereon	(SCSC) Evaluation of Equational Constraints for CAD in SMT Solving (PDF, talk)
Kremer, Steve	(CAV) The DEEPSEC prover (PDF, talk) (CSF) An extensive formal analysis of multi-factor authentication protocols (PDF, talk)
Kretinsky, Jan	(CAV) Rabinizer 4: From LTL to Your Favourite Deterministic Automaton (PDF, talk) (CAV) Value Iteration for Simple Stochastic Games: Stopping Criterion and Learning Algorithm (PDF, talk) (LICS) One Theorem to Rule Them All: A Unified Translation of LTL into $\omega$-Automata (PDF, talk) (LICS) Conditional Value-at-Risk for Reachability and Mean Payoff in Markov Decision Processes (PDF, talk)
Kreuzer, Martin	(SCSC) Refutation of Products of Linear Polynomials (PDF, talk)
Krings, Sebastian	(AVOCS) Writing a Model Checker in 80 Days: Reusable Libraries and Custom Implementation (PDF, talk)
Krishnamurthi, Shriram	(FM) CompoSAT: Specification-Guided Coverage for Model Finding (PDF, talk)
Krishnamurthy, Balaji	(WST) Verification of Rewriting-based Query Optimizers (PDF, talk)
Kroening, Daniel	(MoRe) Logically-Constrained Reinforcement Learning (PDF, talk) (WST) Procedure-Modular Termination Analysis (PDF, talk) (CAV) JBMC: A Bounded Model Checking Tool for Verifying Java Bytecode (PDF, talk) (CAV) Counterexample Guided Inductive Synthesis Modulo Theories (PDF, talk) (CAV) Model Checking Boot Code from AWS Data Centers (PDF, talk)
Krzaczkowski, Jacek	(LICS) Satisfiability in multi-valued circuits (PDF, talk)
Krämer, Julia	(CAV) Value Iteration for Simple Stochastic Games: Stopping Criterion and Learning Algorithm (PDF, talk)
Krötzsch, Markus	(IJCAR) Efficient Model Construction for Horn Logic with VLog: System Description (PDF, talk)
Kugler, Hillel	(VEMDP) Formal Verification of Network-Based Biocomputation Circuits (PDF, talk)
Kukovec, Jure	(TLA) BMCMT: Bounded Model Checking of TLA+ Specifications with SMT (PDF)
Kulal, Sumith	(CAV) What’s hard about Boolean Functional Synthesis? (PDF, talk)
Kullmann, Oliver	(SAT) Minimal unsatisfiability and minimal strongly connected digraphs (PDF, talk)
Kumar, Ramana	(ITP) Software Verification with ITPs Should Use Binary Code Extraction to Reduce the TCB (short paper) (PDF, talk) (IJCAR) Proof-Producing Synthesis of CakeML with I/O and Local State from Monadic HOL Functions (PDF, talk)
Kupferman, Orna	(FM) Timed Vacuity (PDF, talk)
Kuppe, Markus	(TLA) State Space Explosion or: How To Fight An Uphill Battle (PDF)
Kurpisz, Adam	(PC) Optimization over the Boolean Hypercube via Sums of Nonnegative Circuit Polynomials (PDF, talk)
Kurz, Alexander	(ITP) Software tool support for modular reasoning in modal logics of actions (PDF, talk)
Kutsia, Temur	(FSCD) Term-Graph Anti-Unification (PDF, talk) (FSCD) Higher-Order Equational Pattern Anti-Unification (PDF, talk) (NLCS) Anti-Unification and Natural Language Processing (PDF, talk) (UNIF) Towards Generalization Methods for Purely Idempotent Equational Theories (PDF, talk) (UNIF) Proximity-Based Generalization (PDF, talk)
Kutz, Yunus David Kerem	(UNIF) Rewriting with Generalized Nominal Unification (PDF, talk)
Kuusisto, Antti	(LICS) Weighted model counting beyond two-variable logic (PDF, talk)
Kuznetsov, Stepan	(IJCAR) A Logical Framework with Commutative and Non-Commutative Subexponentials (PDF, talk)
Kučera, Antonin	(LICS) Black Ninjas in the Dark: Formal Analysis of Population Protocols (PDF) (LICS) Efficient Algorithms for Asymptotic Bounds on Termination Time in VASS (PDF, talk)
Kwiatkowska, Marta	(VEMDP) Molecular Filters for Noise Reduction (PDF, talk)
König, Barbara	(LICS) A van Benthem Theorem for Fuzzy Modal Logic (PDF, talk)
L
Labed Jilani, Lamia	(REFINE) Programming Without Refinement (PDF, talk)
Lacerda, Bruno	(VaVAS) Policy Generation with Probabilistic Guarantees for Long-term Autonomy of a Mobile Service Robot (PDF, talk)
Lachnitt, Hanna	(WiL) Embedding Intuitionistic Modal Logics in Higher-Order Logic. An Easy Task? (PDF, talk)
Lagniez, Jean Marie	(IJCAR) An Assumption-Based Approach for Solving The Minimal S5-Satisfiability Problem (PDF, talk)
Lahmadi, Abdelkader	(AVOCS) Rule-Based Synthesis of Chains of Security Functions for Software-Defined Networks (PDF, talk)
Laird, James	(LICS) Extensional and Intensional Semantic Universes: A Denotational Model of Dependent Types (PDF, talk)
Lakin, Matthew	(VEMDP) Rule-based Design of Computational DNA Devices (PDF, talk)
Laleg-Kirati, Taous-Meriem	(ADHS) Razumikhin-type Theorems on Practical Stability of Dynamic Equations on Time Scales (PDF, talk)
Lammich, Peter	(Isabelle) A Verified SAT Solver with Watched Literals Using Imperative HOL (Extended Abstract) (PDF, talk) (Isabelle) Using Isabelle/UTP for the Verification of Sorting Algorithms: A Case Study (PDF, talk)
Lampis, Michael	(SAT) QBF as an Alternative to Courcelle's Theorem (PDF, talk)
Lanciotti, Filiberto	(RCRA) Optimal Fault-Tolerant Placement of Relay Nodes in a Mission Critical Wireless Network (PDF, talk)
Laneve, Cosimo	(FM) A lightweight deadlock analysis for programs with threads and reentrant locks (PDF, talk)
Lange, Martin	(PARIS) Collapses of Fixpoint Alternation Hierarchies in Low Type-Levels of Higher-Order Fixpoint Logic (PDF, talk)
Langer, Alexander	(LaSh) Courcelle’s Theorem – A Game-Theoretic Approach (PDF, talk)
Langworthy, David	(TLA) TLA+ in Engineering Systems – Quinceañera (PDF)
Laporte, Vincent	(CSF) Secure compilation of side-channel countermeasures: the case of cryptographic “constant-time” (PDF, talk)
Larchey-Wendling, Dominique	(ITP) Proof Pearl: Constructive Extraction of Cycle Finding Algorithms (PDF, talk) (IJCAR) Constructive Decision via Redundancy-free Proof-Search (PDF, talk)
Larsen, John Bruntse	(Isabelle) Substitutionless First-Order Logic: A Formal Soundness Proof (PDF, talk)
Larsen, Peter Gorm	(Overture) Overture FMU: Export VDM-RT Models as Tool-Wrapper FMUs (PDF, talk) (Overture) ViennaVM: a Virtual Machine for VDM-SL development (PDF, talk) (Overture) Transforming an industrial case study from VDM++ to VDM-SL (PDF, talk)
Lasaulce, Samson	(ADHS) Space-Time Budget Allocation for Marketing Over Social Networks (PDF, talk)
Laskowski, Patrick	(ITP) HOL Light QE (PDF, talk)
Laurent, Olivier	(Coq) Preliminary Report on the Yalla Library (PDF, talk) (LICS) Around Classical and Intuitionistic Linear Logics (PDF, talk) (ITRS) Intersection Subtyping with Constructors (PDF, talk)
Laurenti, Luca	(VEMDP) Molecular Filters for Noise Reduction (PDF, talk)
Lauret, Menno	(ADHS) A switched system approach to optimize mixing of fluids (PDF, talk)
Lausdahl, Kenneth	(Overture) Enhancing Testing of VDM-SL models (PDF, talk) (Overture) Overture FMU: Export VDM-RT Models as Tool-Wrapper FMUs (PDF, talk) (Overture) Transforming an industrial case study from VDM++ to VDM-SL (PDF, talk)
Law, Mark	(ICLP) Learning Commonsense Knowledge through Interactive Dialogue (PDF, talk)
Lazic, Ranko	(LICS) A pseudo-quasi-polynomial algorithm for solving mean-payoff parity games (PDF, talk)
Le Berre, Daniel	(IJCAR) An Assumption-Based Approach for Solving The Minimal S5-Satisfiability Problem (PDF, talk)
Le Roux, Stephane	(SR) Concurrent games and semi-random determinacy (PDF, talk)
Lebedev, Ilia	(CSF) Secure Boot and Remote Attestation in the Sanctum Processor (PDF)
Leblanc, Emily	(ICLP-DC) Explaining Actual Causation via Reasoning about Actions and Change (PDF, talk)
Leclerc, Anthony	(ICLP) Epistemic Logic Programs with World View Constraints (PDF, talk)
Lecomte, Thierry	(FM) Disruptive Innovations for the Development and the Deployment of Fault-Free Software (PDF, talk)
Lee, Joohyung	(ICLP) Translating LPOD and CR-Prolog2 into Standard Answer Set Programs (PDF, talk) (ICLP) A Probabilistic Extension of Action Language BC+ (PDF, talk)
Leeners, Brigitte	(RCRA) Computing Personalised Treatments through In Silico Clinical Trials. A Case Study on Downregulation in Assisted Reproduction. (PDF, talk)
Legay, Axel	(FM) QFLan: A Tool for the Quantitative Analysis of Highly Reconfigurable Systems (PDF, talk) (FM) Statistical Model Checking of LLVM Code (PDF, talk) (LICS) Sequential Relational Decomposition (PDF, talk)
Lehtinen, Karoliina	(LICS) A modal mu perspective on solving parity games in quasipolynomial time. (PDF, talk)
Leigh, Graham	(CL&C) Herbrand's Theorem as Higher-Order Recursion (PDF, talk)
Lellmann, Bjoern	(TYDI) Sequentialising nested systems (PDF, talk)
Lemay, Jean-Simon	(FSCD) Lifting Coalgebra Modalities and IMELL Model Structure to Eilenberg-Moore Categories (PDF, talk)
Lengal, Ondrej	(LaSh) Lazy Automata Techniques for WS1S (PDF, talk)
Lennartz, Werner	(POS) CryptoMiniSat Parameter-Optimization for Solving Cryptographic Instances (PDF, talk)
Leone, Nicola	(LPOP) Role-Based Access Control via JASP (PDF, talk) (LPOP) On the Development of Industrial Applications with ASP (PDF, talk)
Lepigre, Rodolphe	(LFMTP) Abstract Representation of Binders in OCaml using the Bindlib Library (PDF, talk)
Lescanne, Pierre	(FSCD) Counting Environments and Closures (PDF, talk) (Linearity/TLLA) How to count linear and affine closed lambda terms? (PDF, talk) (HOR) Combinatorics of explicit substitutions (extended abstract) (PDF, talk)
Letan, Thomas	(FM) Modular Verification of Programs with Effects and Effect Handlers in Coq (PDF, talk)
Lettmann, Michael Peter	(IJCAR) A Tableaux Calculus for Reducing Proof Size (PDF, talk) (PARIS) Towards the Automatic Construction of Schematic Proofs (PDF, talk)
Leventi-Peetz, Anastasia	(POS) CryptoMiniSat Parameter-Optimization for Solving Cryptographic Instances (PDF, talk)
Leventis, Thomas	(LICS) Probabilistic Böhm Trees and Probabilistic Separation (PDF, talk)
Levy, Jordi	(FSCD) Term-Graph Anti-Unification (PDF, talk)
Lhote, Nathan	(LICS) Logics for Word Transductions with Synthesis (PDF, talk)
Li, Baiyu	(CSF) Symbolic security of garbled circuits (PDF, talk)
Li, Chunxiao	(SAT) Machine Learning-based Restart Policy for CDCL SAT Solvers (PDF, talk)
Li, Haokun	(CAV) Monitoring CTMCs By Multi-Clock Timed Automata (PDF, talk)
Li, Jianwen	(CAV) SimpleCAR: An Efficient Bug-Finding Tool Based On Approximate Reachability (PDF, talk)
Li, Wei	(VaVAS) RoboTool: Modelling and Verification with RoboChart (PDF, talk)
Li, Wenchao	(CAV) Safety-Aware Apprenticeship Learning (PDF, talk)
Li, Yue	(HCVS) Towards Coinductive Theory Exploration in Horn Clause Logic: Extended Abstract (PDF, talk) (PARIS) Coinductive Uniform Proofs: An Extended Abstract (PDF, talk)
Liang, Jia	(SAT) Machine Learning-based Restart Policy for CDCL SAT Solvers (PDF, talk)
Libal, Tomer	(UITP) Implementing a Proof Assistant using Focusing and Logic Programming (PDF, talk) (ARQNL) A Simple Semi-automated Proof Assistant for First-order Modal Logics (PDF, talk)
Licata, Daniel R.	(FSCD) Internal Universes in Models of Homotopy Type Theory (PDF, talk) (FSCD) Call-by-name Gradual Type Theory (PDF, talk)
Lierler, Yuliya	(ICLP) SMT-based Answer Set Solver CMODELS(DIFF) (System Description) (PDF, talk)
Limbrée, Christophe	(AVOCS) A Framework for the Formal Verification of Networks of Railway Interlockings - Application to the Belgian Railways (PDF, talk)
Lin, Shang-Wei	(FM) Compositional Reasoning for Shared-variable Concurrent Programs (PDF, talk) (LICS) Quasi-Open Bisimilarity with Mismatch is Intuitionistic (PDF, talk)
Lindell, Steven	(LCC) Traversal-invariant definability and Logarithmic-space computation (PDF, talk)
Lindenhovius, Bert	(LICS) Enriching a Linear/Non-linear Lambda Calculus: A Programming Language for String Diagrams (PDF, talk)
Link, Sebastian	(IJCAR) Automated Reasoning about Key Sets (PDF, talk)
Liqat, Umer	(LCC) A General Equational Framework for Static Profiling of Parametric Resource Usage (PDF, talk)
Listenmaa, Inari	(NLCS) Automatic test suite generation for PMCFG grammars (PDF, talk)
Liu, Heng	(PRUV) A Model-Theoretic View on Preferences in Declarative Specifications of Search Problems (PDF, talk)
Liu, Shuang	(FM) Falsification of Cyber-Physical Systems Using Deep Reinforcement Learning (PDF, talk)
Liu, Tian	(PRUV) A New Probabilistic Algorithm for Approximate Model Counting (PDF, talk) (IJCAR) A New Probabilistic Algorithm for Approximate Model Counting (PDF, talk)
Liu, Yang	(FM) Compositional Reasoning for Shared-variable Concurrent Programs (PDF, talk) (CSF) A Permission-Dependent Type System for Secure Information Flow Analysis (PDF, talk)
Liu, Yanhong A.	(LPOP) Easier Rules and Constraints for Programming (PDF, talk) (TLA) Invariants in Distributed Algorithms (PDF)
Liu, Yufei	(Isabelle) Hilbert Meets Isabelle: Formalisation of the DPRM Theorem in Isabelle (PDF, talk)
Lluch Lafuente, Alberto	(FM) QFLan: A Tool for the Quantitative Analysis of Highly Reconfigurable Systems (PDF, talk)
Lochbihler, Andreas	(ITP) Fast machine words in Isabelle/HOL (PDF, talk) (ITP) Relational parametricity and quotient preservation for modular (co)datatypes (PDF, talk) (Isabelle) Lazy Algebraic Types in Isabelle/HOL (PDF, talk)
Loitzenbauer, Veronika	(CAV) Symbolic Algorithms for Graphs and Markov Decision Processes with Fairness Objectives (PDF, talk)
Lomuscio, Alessio	(SR) Verification of Multi-agent Systems with Imperfect Information and Public Actions (PDF, talk)
Lonsing, Florian	(IJCAR) QRAT+: Generalizing QRAT by a More Powerful QBF Redundancy Property (PDF, talk)
Lopez Hernandez, Julio Cesar	(IJCAR) An abstraction-refinement framework for reasoning with large theories (PDF, talk)
Lopez Pombo, Carlos	(ITP) Boosting the Reuse of Formal Specifications (PDF, talk)
Lorber, Florian	(FM) 20 Years of Real Real Time Model Validation (PDF)
Lowe, Gavin	(FM) View abstraction for systems with component identities (PDF, talk)
Lozes, Etienne	(ADSL) A Complete Proof System for Basic Symbolic Heaps with Permissions (PDF, talk) (PARIS) Collapses of Fixpoint Alternation Hierarchies in Low Type-Levels of Higher-Order Fixpoint Logic (PDF, talk)
Lucanu, Dorel	(IJCAR) A Coinductive Approach to Proving Reachability in Logically Constrained Term Rewriting Systems (PDF, talk)
Lucas, Salvador	(WST) Presentation of the WST 2018 proceedings (PDF) (WST) Well-founded models in proofs of termination (PDF, talk)
Luckow, Kasper	(CSF) Symbolic Side-Channel Analysis for Probabilistic Programs (PDF, talk)
Lugiez, Denis	(ADSL) A Complete Proof System for Basic Symbolic Heaps with Permissions (PDF, talk)
Lukert, Philip	(CAV) Synthesizing Reactive Systems from Hyperproperties (PDF, talk)
Lukina, Anna	(VaVAS) Adaptive Neighborhood Resizing for Stochastic Reachability in Multi-Agent Systems (PDF, talk)
Luo, Adriel	(ADHS) CoasterX: A Case Study in Component-Driven Hybrid Systems Proof Automation (PDF, talk)
Luo, Zhaohui	(NLCS) Propositional Forms of Judgemental Interpretations (PDF, talk) (Linearity/TLLA) Substructural Calculi with Dependent Types (PDF, talk)
Luttenberger, Michael	(CAV) Strix: Explicit Reactive Synthesis Strikes Back! (PDF, talk)
Lutz, Carsten	(LICS) Weighted model counting beyond two-variable logic (PDF, talk)
Lv, Yiqi	(FM) Resource-aware Design for Reliable Autonomous Applications with Multiple Periods (PDF, talk)
Lynce, Ines	(ICLP-DC) Model Revision of Logical Regulatory Networks using Logic-based Tools (PDF, talk)
Lynch, Christopher	(UNIF) Bounded ACh Unification (PDF, talk)
López-García, Pedro	(ICLP) Towards Static Performance Guarantees for Programs with Run-time Checks (PDF, talk) (LCC) A General Equational Framework for Static Profiling of Parametric Resource Usage (PDF, talk)
M
Ma, Feifei	(PRUV) A New Probabilistic Algorithm for Approximate Model Counting (PDF, talk) (PRUV) VolCE: An Efficient Tool for Solving #SMT(LA) Problems (PDF, talk) (IJCAR) A New Probabilistic Algorithm for Approximate Model Counting (PDF, talk) (IJCAR) Investigating the Existence of Large Sets of Idempotent Quasigroups via Satisfiability Testing (PDF, talk)
Ma, Hao	(ADHS) Interacting Particle System-Based Estimation of Reach Probability for a Generalized Stochastic Hybrid System (PDF, talk)
Ma, Weixi	(UNIF) Efficiency of a Good but not Linear Nominal Unification Algorithm (PDF, talk)
Ma, Xutong	(PRUV) A New Probabilistic Algorithm for Approximate Model Counting (PDF, talk) (IJCAR) A New Probabilistic Algorithm for Approximate Model Counting (PDF, talk)
MacCarthaigh, Colm	(CAV) Continuous formal verification of Amazon s2n (PDF, talk)
Mace, John	(Overture) Design Space Exploration for Secure Building Control (PDF, talk)
Macedo, Hugo Daniel	(Overture) Transforming an industrial case study from VDM++ to VDM-SL (PDF, talk)
Macedo, Nuno	(F-IDE) Improving the Visualization of Alloy Instances (PDF, talk)
Mackie, Ian	(DCM) Models of Computation that Conserve Data (PDF, talk)
Madelaine, Eric	(AVOCS) Using SMT engine to generate Symbolic Automata (PDF, talk)
Madelaine, Florent	(LICS) A universal-algebraic proof of the complexity dichotomy for Monotone Monadic SNP (PDF, talk)
Maeda, Yuya	(FSCD) Narrowing Trees for Syntactically Deterministic Conditional Term Rewriting Systems (PDF, talk) (WPTE) On Transforming Narrowing Trees into Regular Tree Grammars Generating Ranges of Substitutions (PDF, talk)
Maffei, Matteo	(CAV) Foundations and Tools for the Static Analysis of Ethereum smart contracts (PDF)
Magill, Stephen	(CAV) Continuous formal verification of Amazon s2n (PDF, talk)
Magron, Victor	(ADHS) Occupation Measure Methods for Modelling and Analysis of Biological Hybrid Systems (PDF, talk)
Mahajan, Anmol	(SAT) Effective use of SMT solvers for Program Equivalence Checking through Invariant Sketching and Query Decomposition (PDF, talk)
Mahboubi, Assia	(Coq) Classical Analysis with Coq (PDF, talk)
Maieli, Roberto	(Linearity/TLLA) The structure of non decomposable connectives of linear logic (PDF, talk)
Maier, Jürgen	(ADHS) Verifying nonlinear analog and mixed-signal circuits with inputs (PDF, talk)
Majumdar, Rupak	(ADHS) Concentration of Measure for Chance-Constrained Optimization (PDF, talk)
Malacaria, Pasquale	(CSF) Symbolic Side-Channel Analysis for Probabilistic Programs (PDF, talk)
Malbos, Philippe	(IWC) Coherence of monoids by insertions (PDF, talk) (IWC) Coherence modulo relations (PDF, talk)
Malik, Sharad	(CAV) Lazy Self-Composition for Security Verification (PDF, talk)
Maly, Jan	(PRUV) A new logic for jointly representing hard and soft constraints (PDF, talk)
Mancini, Toni	(RCRA) Optimal Fault-Tolerant Placement of Relay Nodes in a Mission Critical Wireless Network (PDF, talk) (RCRA) Computing Personalised Treatments through In Silico Clinical Trials. A Case Study on Downregulation in Assisted Reproduction. (PDF, talk)
Mangharam, Rahul	(ADHS) Data-Driven Switched Affine Modeling for Model Predictive Control (PDF, talk)
Mangin, Cyprien	(Coq) Towards a formalization of the guard condition (PDF, talk)
Manighetti, Matteo	(CL&C) Admissible tools in the kitchen of intuitionistic logic (PDF, talk)
Manna, Marco	(LPOP) Role-Based Access Control via JASP (PDF, talk) (LPOP) On the Development of Industrial Applications with ASP (PDF, talk)
Mannaa, Bassel	(FSCD) The clocks they are adjunctions. Denotational semantics for Clocked Type Theory (PDF, talk) (HoTT/UF) Dependent Right Adjoint Types (PDF, talk) (PARIS) What makes guarded types tick? (PDF, talk)
Mansfield, Martin	(Overture) Design Space Exploration for Secure Building Control (PDF, talk)
Manzonetto, Giulio	(Linearity/TLLA) The Bang Calculus and the Two Girard's Translations (PDF, talk)
Marantidis, Pavlos	(UNIF) ACUI Unification Modulo Ground Theories (PDF, talk)
Maratea, Marco	(ICLP) Shared aggregate sets in answer set programming (PDF, talk) (ICLP) Cautious Reasoning in ASP via Minimal models and Unsatisfiable Cores (PDF, talk)
Marché, Claude	(F-IDE) Lightweight Interactive Proving inside an Automatic Program Verifier (PDF, talk)
Marcinkowski, Jerzy	(LICS) Can One Escape Red Chains? Regular Path Queries Determinacy is Undecidable. (PDF, talk)
Mardare, Radu	(LICS) Boolean-Valued Semantics for Stochastic Lambda-Calculus (PDF, talk) (LICS) An algebraic theory of Markov processes (PDF, talk)
Mari, Federico	(RCRA) Computing Personalised Treatments through In Silico Clinical Trials. A Case Study on Downregulation in Assisted Reproduction. (PDF, talk)
Marin, Sonia	(WiL) Decomposing labelled proof theory for intuitionistic modal logic (PDF, talk) (TYDI) Nested sequents for modal logics and beyond (PDF, talk)
Markey, Nicolas	(FM) Optimal and Robust Controller Synthesis Using Energy Timed Automata with Uncertainty (PDF, talk) (SR) Dependences in Strategy Logic (PDF, talk)
Marple, Kyle	(ICLP) Constraint Answer Set Programming without Grounding (PDF, talk)
Marques-Silva, Joao	(SAT) PySAT: A Python Toolkit for Prototyping with SAT Oracles (PDF, talk) (IJCAR) A SAT-Based Approach to Learn Explainable Decision Sets (PDF, talk) (PC) On Dual-Rail Based MaxSAT Solving (PDF, talk)
Marre, Bruno	(SMT) Centralizing Equality Reasoning in MCSAT (PDF, talk)
Marshall, Andrew M.	(UNIF) Knowledge Problems in Equational Extensions of Subterm Convergent Theories (PDF, talk)
Marson, Giorgia Azzurra	(CSF) A Cryptographic Look at Multi-Party Channels (PDF, talk)
Martin, Barnaby	(PC) Resolution and the binary encoding of combinatorial principles (PDF, talk)
Martinez, Maria Vanina	(PRUV) Leveraging Probabilistic Existential Rules for Adversarial Deduplication (PDF, talk)
Martins, Eunice	(ITP) A Coq formalisation of SQL’s execution engines (PDF, talk)
Maréchal, Alexandre	(ITP) A Coq Tactic for Equality Learning in Linear Arithmetic (PDF, talk)
Masci, Paolo	(F-IDE) Integrating user design and formal models within PVSio-Web (PDF, talk)
Massini, Annalisa	(RCRA) Computing Personalised Treatments through In Silico Clinical Trials. A Case Study on Downregulation in Assisted Reproduction. (PDF, talk)
Matheja, Christoph	(CAV) Let this Graph be your Witness! An Attestor for Verifying Java Pointer Programs (PDF, talk)
Mathews, Minu	(SAT) Machine Learning-based Restart Policy for CDCL SAT Solvers (PDF, talk)
Mathur, Umang	(CAV) Controller Synthesis Made Real: Reach-avoid Specifications and Linear Dynamics (PDF, talk)
Matias, Lionel	(AVOCS) Climbing the Software Assurance Ladder - Practical Formal Verification for Reliable Software (PDF, talk)
Matthews, Stuart	(AVOCS) Climbing the Software Assurance Ladder - Practical Formal Verification for Reliable Software (PDF, talk)
Matyas, Jiri	(CAV) ADAC: Automated Design of Approximate Circuits (PDF, talk)
Maubert, Bastien	(SR) Strategy Logic with Imperfect Information (PDF, talk) (SR) Quantifying Bounds in Strategy Logic (PDF, talk)
Mauborgne, Laurent	(FM) On Software Safety, Security, and Abstract Interpretation (PDF, talk)
Mazaheri, Sogol	(CSF) Self-Guarding Cryptographic Protocols against Algorithm Substitution Attacks (PDF, talk) (CSF) Backdoored Hash Functions: Immunizing HMAC and HKDF (PDF, talk)
Mazo Jr., Manuel	(ADHS) Optimal Symbolic Controllers Determinization for BDD storage. (PDF, talk)
Mazza, Damiano	(DCM) Polyadic Approximations and Intersection Types (PDF) (HOR) The next 700 (type-theoretical) denotational models ? (PDF, talk) (ITRS) Polyadic Approximations and Intersection Types (PDF)
McCall, Mckenna	(CSF) Knowledge-based Security of Dynamic Secrets for Reactive Programs (PDF, talk)
McCann, Julie	(AVOCS) Formal Verification of Synchronisation, Gossip and Environmental Effects for Critical IoT Systems (PDF, talk)
McIver, Annabelle	(FM) Processing text for privacy: An information flow perspective (PDF) (FM) An Algebraic Approach for Reasoning About Information Flow (PDF, talk)
McMillan, Kenneth	(CAV) Eager Abstraction for Symbolic Model Checking (PDF, talk) (CAV) Learning Abstractions for Program Synthesis (PDF, talk)
Meggendorfer, Tobias	(CAV) Rabinizer 4: From LTL to Your Favourite Deterministic Automaton (PDF, talk) (LICS) Conditional Value-at-Risk for Reachability and Mean Payoff in Markov Decision Processes (PDF, talk)
Meinicke, Larissa	(FM) Encoding fairness in a synchronous concurrent program algebra (PDF, talk)
Melatti, Igor	(RCRA) Computing Personalised Treatments through In Silico Clinical Trials. A Case Study on Downregulation in Assisted Reproduction. (PDF, talk)
Melgratti, Hernan	(LICS) Concurrency and Probability: Removing Confusion, Compositionally (PDF, talk)
Melioli, Riccardo	(F-IDE) AsmetaF: a flattener for the ASMETA framework (PDF, talk)
Melliès, Paul-André	(LICS) Ribbon tensorial logic (PDF, talk) (LICS) An Asynchronous Soundness Theorem for Concurrent Separation Logic (PDF, talk)
Melquiond, Guillaume	(IJCAR) A Why3 framework for reflection proofs and its application to GMP's algorithms (PDF, talk)
Mendes, Alexandra	(ITP) Towards Verified Handwritten Calculational Proofs (short paper) (PDF, talk)
Meng, Yu	(ADHS) Verifying nonlinear analog and mixed-signal circuits with inputs (PDF, talk)
Mengel, Stefan	(SAT) QBF as an Alternative to Courcelle's Theorem (PDF, talk) (QBF) Tractability results for structured quantified CNF-formulas via knowledge compilation (PDF, talk)
Menghi, Claudio	(FM) Multi-Robot LTL Planning Under Uncertainty (PDF, talk)
Merayo Corcoba, Alicia	(WST) Inference of Linear Upper-Bounds on the Expected Cost by Solving Cost Relations (PDF, talk)
Merkle, Daniel	(VEMDP) Rule-Based Gillespie Simulation of Chemical Systems (PDF, talk)
Mertens, Eric	(CAV) Continuous formal verification of Amazon s2n (PDF, talk)
Mery, Daniel	(ADSL) Labelled Cyclic Proofs for Separation Logic (PDF, talk) (ARQNL) Labelled Connection-based Proof Search for Multiplicative Intuitionistic Linear Logic (PDF, talk)
Merz, Stephan	(AVOCS) Rule-Based Synthesis of Chains of Security Functions for Software-Defined Networks (PDF, talk)
Meyer, Philipp J.	(CAV) Strix: Explicit Reactive Synthesis Strikes Back! (PDF, talk)
Meßner, Florian	(ITP) A Formally Verified Solver for Homogeneous Linear Diophantine Equations (PDF, talk)
Micciancio, Daniele	(CSF) Symbolic security of garbled circuits (PDF, talk)
Middeldorp, Aart	(FSCD) Completion for Logically Constrained Rewriting (PDF, talk) (FSCD) ProTeM: A Proof Term Manipulator (PDF, talk) (FSCD) Confluence Competition 2018 (PDF) (IJCAR) FORT 2.0 (PDF, talk) (IJCAR) Cops and CoCoWeb: Infrastructure for Confluence Tools (PDF, talk) (IWC) Towards a Verified Decision Procedure for Confluence of Ground Term Rewrite Systems in Isabelle/HOL (PDF, talk)
Milani, Alfredo	(RCRA) Algebraic Crossover Operators for Permutations (PDF, talk)
Mili, Ali	(REFINE) Programming Without Refinement (PDF, talk)
Miller, Alice	(VaVAS) Probabilistic Model Checking for Autonomous Agent Strategy Synthesis - Extended Abstract (PDF, talk)
Miller, Dale	(LFMTP) Functional programming with λ-tree syntax: a progress report (PDF, talk) (LFMTP) Computation-as-deduction in Abella: work in progress (PDF, talk)
Mimram, Samuel	(FSCD) Coherence of Gray categories via rewriting (PDF, talk)
Mineshima, Koji	(NLCS) Paychecks, Presupposition, and Dependent Types (PDF, talk)
Mio, Matteo	(LICS) Riesz Modal Logic with Threshold Operators (PDF, talk)
Miquey, Étienne	(ITP) Formalizing Implicative Algebras in Coq (PDF, talk) (LICS) A sequent calculus with dependent types for classical arithmetic (PDF, talk)
Mislove, Michael	(LICS) Enriching a Linear/Non-linear Lambda Calculus: A Programming Language for String Diagrams (PDF, talk)
Mitchell, David	(SAT) Centrality-Based Improvements to CDCL Heuristics (PDF, talk)
Mitchell, Ian M.	(ADHS) Control Synthesis and Classification for Unicycle Dynamics Using the Gradient and Value Sampling Particle Filters (PDF, talk)
Mitra, Arindam	(ICLP) Incremental and Iterative Learning of Answer Set Programs from Mutually Distinct Examples (PDF, talk) (ICLP-DC) The Learning-Knowledge-Reasoning Paradigm For Natural Language Understanding and Question Answering (PDF, talk)
Mitra, Sayan	(FM) Approximate Partial Order Reduction (PDF, talk) (CAV) Controller Synthesis Made Real: Reach-avoid Specifications and Linear Dynamics (PDF, talk)
Mitra, Sayan	(ADHS) Verifying nonlinear analog and mixed-signal circuits with inputs (PDF, talk)
Mitsou, Valia	(SAT) QBF as an Alternative to Courcelle's Theorem (PDF, talk)
Miyazawa, Alvaro	(VaVAS) RoboTool: Modelling and Verification with RoboChart (PDF, talk)
Mo, Man Yue	(FM) Variant analysis with QL (PDF, talk)
Molyneux, Gareth	(VEMDP) Bayesian Verification of Chemical Reaction Networks (PDF, talk)
Momigliano, Alberto	(LFMTP) Property-Based Testing of Abstract Machines: an Experience Report (PDF, talk)
Monin, Benoit	(LICS) An answer to the Gamma question (PDF, talk)
Montanari, Ugo	(LICS) Concurrency and Probability: Removing Confusion, Compositionally (PDF, talk)
Monteiro, Pedro T.	(ICLP-DC) Model Revision of Logical Regulatory Networks using Logic-based Tools (PDF, talk)
Montesi, Fabrizio	(Linearity/TLLA) Taking Linear Logic Apart (PDF, talk)
Montin, Mathieu	(REFINE) Ordering strict partial orders to model behavioural refinement (PDF, talk)
Montmirail, Valentin	(IJCAR) An Assumption-Based Approach for Solving The Minimal S5-Satisfiability Problem (PDF, talk)
Moore, Brandon	(CSF) KEVM: A Complete Formal Semantics of the Ethereum Virtual Machine (PDF, talk)
Moot, Richard	(NLCS) Do different syntactic trees yield different logical readings? Some remarks on head variables in typed lambda calculus. (PDF, talk)
Mora, Federico	(CAV) StringFuzz: A Fuzzer for String Solvers (PDF, talk)
Morak, Michael	(SAT) Exploiting Treewidth for Projected Model Counting and its Limits (PDF, talk)
Morales, Jose F.	(ICLP) Towards Incremental and Modular Context-sensitive Analysis (PDF, talk) (ICLP) Towards Static Performance Guarantees for Programs with Run-time Checks (PDF, talk)
Morales, Marianela	(WiL) Decomposing labelled proof theory for intuitionistic modal logic (PDF, talk)
Morarescu, Irinel Constantin	(ADHS) Network-Aware Design of State-Feedback Controllers for Linear Wireless Networked Control Systems (PDF, talk)
Morehouse, Edward	(HoTT/UF) Ordered Cubes (PDF, talk)
Morgado, Antonio	(SAT) PySAT: A Python Toolkit for Prototyping with SAT Oracles (PDF, talk) (PC) On Dual-Rail Based MaxSAT Solving (PDF, talk)
Morisset, Charles	(Overture) Design Space Exploration for Secure Building Control (PDF, talk) (FCS) LISA: Predicting the Impact of DoS Attacks on Real-World Low Power IoT Systems (PDF, talk)
Moscato, Mariano	(ITP) Boosting the Reuse of Formal Specifications (PDF, talk) (FM) A Formally Verified Floating-Point Implementation of the Compact Position Reporting Algorithm (PDF, talk)
Moser, Georg	(IJCAR) MaedMax: A Maximal Ordered Completion Tool (PDF, talk)
Moss, Larry	(NLCS) Automated Reasoning from Polarized Parse Trees (PDF, talk) (ARQNL) Implementations of Natural Logics (PDF)
Moss, Sean	(LICS) Dialectica models of type theory (PDF, talk)
Mota, Jean-Marc	(AVOCS) Climbing the Software Assurance Ladder - Practical Formal Verification for Reliable Software (PDF, talk)
Mottet, Antoine	(UNIF) ACUI Unification Modulo Ground Theories (PDF, talk) (LICS) A universal-algebraic proof of the complexity dichotomy for Monotone Monadic SNP (PDF, talk)
Moy, Yannick	(F-IDE) Lightweight Interactive Proving inside an Automatic Program Verifier (PDF, talk) (AVOCS) Climbing the Software Assurance Ladder - Practical Formal Verification for Reliable Software (PDF, talk)
Mrazek, Vojtech	(CAV) ADAC: Automated Design of Approximate Circuits (PDF, talk)
Mueller, Moritz	(LICS) A parameterized halting problem, the linear time hierarchy, and the MRDP theorem (PDF, talk)
Mullen, Eric	(ITP) Software Verification with ITPs Should Use Binary Code Extraction to Reduce the TCB (short paper) (PDF, talk) (CAV) Continuous formal verification of Amazon s2n (PDF, talk)
Mulligan, Casey	(SCSC) Non-linear Real Arithmetic Benchmarks derived from Automated Reasoning in Economics (PDF, talk)
Munoz, Cesar	(ITP) Boosting the Reuse of Formal Specifications (PDF, talk) (FM) A Formally Verified Floating-Point Implementation of the Compact Position Reporting Algorithm (PDF, talk) (FM) From Formal Requirements to Highly Assured Software for Unmanned Aircraft Systems (PDF, talk)
Murano, Aniello	(SR) Verification of Multi-agent Systems with Imperfect Information and Public Actions (PDF, talk) (SR) Strategy Logic with Imperfect Information (PDF, talk) (SR) Solving Parity Games: Explicit vs Symbolic (PDF, talk) (SR) Quantifying Bounds in Strategy Logic (PDF, talk)
Muroya, Koko	(LICS) The Geometry of Computation-Graph Abstraction (PDF, talk)
Murray, Richard M.	(ADHS) Temporal Logic Control of POMDPs Via Label-Based Stochastic Simulation Relations (PDF, talk)
Murray, Richard M.	(TLA) Proving properties of a minimal covering algorithm (PDF)
Murugesan, Anitha	(F-IDE) The CLEAR Way To Transparent Formal Methods (PDF, talk)
Mutluergil, Suha Orhun	(CAV) Reasoning About TSO Programs Using Reduction and Abstraction (PDF, talk)
Muñiz, Marco	(CAV) Start Pruning When Time Gets Urgent: Partial Order Reduction for Timed Systems (PDF, talk)
Myojin, Tomoyuki	(VaVAS) Policing Functions for Machine Learning Systems (PDF, talk)
Myreen, Magnus O.	(ITP) Software Verification with ITPs Should Use Binary Code Extraction to Reduce the TCB (short paper) (PDF, talk) (IJCAR) Proof-Producing Synthesis of CakeML with I/O and Local State from Monadic HOL Functions (PDF, talk) (PAAR) The CakeML Verified Compiler and Toolchain (PDF, talk)
Mödersheim, Sebastian A.	(CSF) A Typing Result for Stateful Protocols (PDF, talk)
Mörtberg, Anders	(LICS) On Higher Inductive Types in Cubical Type Theory (PDF, talk)
Møgelberg, Rasmus	(FSCD) The clocks they are adjunctions. Denotational semantics for Clocked Type Theory (PDF, talk) (HoTT/UF) Dependent Right Adjoint Types (PDF, talk) (PARIS) What makes guarded types tick? (PDF, talk)
Müller, Christian	(CSF) Inductive Invariants for Noninterference in Multi-agent Workflows (PDF, talk)
Müller, Dennis	(IJCAR) Theories as Types (PDF, talk)
Müller, Moritz	(LCC) Feasibly constructive proofs of succinct weak circuit lower bounds (PDF, talk)
Müller, Peter	(CAV) Nagini: A Static Verifier for Python (PDF, talk) (CAV) MaxSMT-Based Type Inference for Python 3 (PDF, talk) (CAV) Permission Inference for Array Programs (PDF, talk)
Münger, Severin	(CAV) Permission Inference for Array Programs (PDF, talk)
N
Nadel, Alexander	(SAT) Solving MaxSAT with Bit-Vector Optimization (PDF, talk) (SAT) Chronological Backtracking (PDF, talk)
Nagashima, Yutaka	(Isabelle) PaMpeR: A Proof Method Recommendation System for Isabelle/HOL (PDF, talk)
Nagele, Julian	(IJCAR) Cops and CoCoWeb: Infrastructure for Confluence Tools (PDF, talk)
Nagele, Julian	(FSCD) Confluence Competition 2018 (PDF)
Nakagawa, Yuichiroh	(VaVAS) Policing Functions for Machine Learning Systems (PDF, talk)
Nakano, Keisuke	(FSCD) On repetitive right application of B-terms (PDF, talk) (Coq) ComplCoq: Rewrite Hint Construction with Completion Procedures (PDF, talk)
Nakazawa, Koji	(ADSL) Cyclic Theorem Prover for Separation Logic by Magic Wand (PDF, talk) (IWC) Complete Axiom System of Cluster Algebra (PDF, talk)
Nalon, Cláudia	(WiL) On the Combination of Resolution and SAT Procedures for Modal Theorem-Proving (PDF, talk) (IJCAR) A Resolution-Based Calculus for Preferential Logics (PDF, talk) (PAAR) Evaluating Pre-Processing Techniques for the Separated Normal Form for Temporal Logics (PDF, talk)
Namjoshi, Kedar	(CAV) Synthesis Of Asynchronous Reactive Programs From Temporal Specifications (PDF, talk)
Nampally, Arun	(ICLP) Constraint-Based Inference in Probabilistic Logic Programs (PDF, talk)
Nanjo, Yoji	(LICS) Dependent Temporal Effects and Fixpoint Logic for Verification (PDF, talk)
Nantes-Sobrinho, Daniele	(FSCD) Fixed-Point Constraints for Nominal Equational Unification (PDF, talk)
Narboux, Julien	(ThEdu) GeoCoq: Formalized Foundations of Geometry (PDF)
Narkawicz, Anthony	(FM) From Formal Requirements to Highly Assured Software for Unmanned Aircraft Systems (PDF, talk)
Narodytska, Nina	(SAT) Constrained Image Generation Using Binarized Neural Networks with Decision Procedures (PDF, talk) (IJCAR) A SAT-Based Approach to Learn Explainable Decision Sets (PDF, talk)
Naumann, David	(CSF) Assuming you know: epistemic semantics of relational annotations for expressive flow policies (PDF, talk)
Nellen, Johanna	(FM) Formal Verification of Automotive Simulink Controller Models: Empirical Technical Challenges, Evaluation and Recommendations (PDF, talk)
Nelson, Tim	(FM) CompoSAT: Specification-Guided Coverage for Model Finding (PDF, talk)
Nemouchi, Yakoub	(Isabelle) Using Isabelle/UTP for the Verification of Sorting Algorithms: A Case Study (PDF, talk)
Neuper, Walther	(ThEdu) Lucas Interpretation from Programmers’ Perspective (PDF, talk)
New, Max	(FSCD) Call-by-name Gradual Type Theory (PDF, talk)
Newstead, Clive	(HoTT/UF) Algebraic models of dependent type theory (PDF, talk)
Ng, Kang Feng	(FSCD) A diagrammatic axiomatisation of fermionic quantum circuits (PDF, talk) (LICS) Two complete axiomatisations of pure-state qubit quantum computing (PDF, talk)
Nguyen, Huyen T.T.	(CAV) Quasi-Optimal Partial Order Reduction (PDF, talk)
Nguyen, Thanh	(ICLP) Phylotastic: An Experiment in Creating, Manipulating, and Evolving Phylogenetic Biology Workflows Using Logic Programming (PDF, talk)
Nguyen, Van	(ICLP) Experimenting with robotic intra-logistics domains (PDF, talk) (ICLP) Natural Language Generation From Ontologies: Application Paper (PDF, talk) (ICLP-DC) Natural Language Generation From Ontologies (PDF, talk)
Nguyễn, Lê Thành Dũng	(FSCD) Unique perfect matchings and proof nets (PDF, talk) (Linearity/TLLA) Coherent interaction graphs: a nondeterministic geometry of interaction for MLL (PDF, talk) (Linearity/TLLA) A semantic conjecture on second-order MLL and its complexity consequences (work in progress) (PDF, talk)
Nickovic, Dejan	(CAV) A Counting Semantics for Monitoring LTL Specifications over Finite Traces (PDF, talk)
Nicolau Jr., Dan	(VEMDP) Formal Verification of Network-Based Biocomputation Circuits (PDF, talk)
Nielsen, Brian	(FM) 20 Years of Real Real Time Model Validation (PDF)
Niemetz, Aina	(CAV) BTOR2, BtorMC and Boolector 3.0 (PDF, talk) (CAV) Solving Quantified Bit-Vectors using Invertibility Conditions (PDF, talk) (SMT) Rewrites for SMT Solvers using Syntax-Guided Enumeration (PDF, talk)
Niewerth, Matthias	(LICS) MSO Queries on Trees: Enumerating Answers under Updates Using Forest Algebras (PDF, talk)
Nigam, Vivek	(IJCAR) A Logical Framework with Commutative and Non-Commutative Subexponentials (PDF, talk) (FCS) Statistical Model Checking of Guessing and Timing Attacks on Distance-bounding Protocols (PDF, talk)
Nigam, Vivek	(WPTE) Verification of Ada Programs with AdaHorn (PDF, talk)
Nilsson, Petter	(ADHS) Nonuniform abstractions, refinement and controller synthesis with novel BDD encodings (PDF, talk)
Nilsson, Petter	(ADHS) Temporal Logic Control of POMDPs Via Label-Based Stochastic Simulation Relations (PDF, talk)
Nilsson, René Søndergaard	(Overture) Enhancing Testing of VDM-SL models (PDF, talk) (Overture) Transforming an industrial case study from VDM++ to VDM-SL (PDF, talk)
Nipkow, Tobias	(ITP) Verified Analysis of Random Binary Tree Structures (PDF, talk) (ITP) Verified Memoization and Dynamic Programming (PDF, talk)
Nishida, Naoki	(FSCD) Narrowing Trees for Syntactically Deterministic Conditional Term Rewriting Systems (PDF, talk) (IWC) Convergence of Simultaneously and Sequentially Unraveled TRSs for Normal Conditional TRSs (PDF, talk) (WPTE) On Transforming Functions Accessing Global Variables into Logically Constrained Term Rewriting Systems (PDF, talk) (WPTE) On Transforming Narrowing Trees into Regular Tree Grammars Generating Ranges of Substitutions (PDF, talk)
Nishida, Naoki	(FSCD) Confluence Competition 2018 (PDF)
Noetzli, Andres	(SMT) Rewrites for SMT Solvers using Syntax-Guided Enumeration (PDF, talk)
Noll, Thomas	(CAV) Let this Graph be your Witness! An Attestor for Verifying Java Pointer Programs (PDF, talk) (CAV) Symbolic Liveness Analysis of Real-World Software (PDF, talk)
Nollet, Rémi	(PARIS) Local validity for circular proofs in linear logic with fixed points (PDF, talk)
Nonato, Maddalena	(RCRA) Logic Programming approaches for routing fault-free and maximally-parallel Wavelength Routed Optical Networks on Chip (Application paper) (PDF, talk)
Nordstrom, Jakob	(SAT) Using Combinatorial Benchmarks to Probe the Reasoning Power of Pseudo-Boolean Solvers (PDF, talk) (SAT) In Between Resolution and Cutting Planes: A Study of Proof Systems for Pseudo-Boolean SAT Solving (PDF, talk)
Norman, Gethin	(VaVAS) Probabilistic Model Checking for Autonomous Agent Strategy Synthesis - Extended Abstract (PDF, talk)
Norrish, Michael	(ITP) Verifying the LTL to Büchi Automata Translation via Very Weak Alternating Automata (PDF, talk) (IJCAR) Proof-Producing Synthesis of CakeML with I/O and Local State from Monadic HOL Functions (PDF, talk)
Novotný, Petr	(LICS) Efficient Algorithms for Asymptotic Bounds on Termination Time in VASS (PDF, talk)
Nowak, David	(AVOCS) Proof-Oriented Design of a Separation Kernel with Minimal Trusted Computing Base (PDF, talk)
Nowland, Trisha	(WiL) Towards a Logical Framework for Latent Variable Modelling (PDF, talk)
Nowotka, Dirk	(FM) Statistical Model Checking of LLVM Code (PDF, talk) (POS) Tuning Parallel SAT Solvers (PDF, talk)
Nuyts, Andreas	(HoTT/UF) Internalizing Presheaf Semantics: Charting the Design Space (PDF, talk) (HoTT/UF) Robust Notions of Contextual Fibrancy (PDF, talk) (LICS) Degrees of Relatedness - A Unified Framework for Parametricity, Irrelevance, Ad Hoc Polymorphism, Intersections, Unions and Algebra in Dependent Type Theory (PDF, talk)
Nührenberg, Georg	(DS-FM) Formal verification of neural networks (PDF, talk)
O
O'Hearn, Peter	(LICS) Continuous Reasoning: Scaling the Impact of Formal Methods (PDF)
Obermeier, Philipp	(ICLP) Experimenting with robotic intra-logistics domains (PDF, talk) (ICLP) Routing Driverless Transport Vehicles in Car Assembly with Answer Set Programming (PDF, talk) (ICLP-DC) Scalable Robotic Intra-Logistics with Answer Set Programming (PDF, talk)
Ochremiak, Joanna	(LICS) Definable Ellipsoid Method, Sums-of-Squares Proofs, and the Isomorphism Problem (PDF, talk)
Oda, Tomohiro	(Overture) ViennaVM: a Virtual Machine for VDM-SL development (PDF, talk)
Oddi, Angelo	(RCRA) Greedy Randomized Search for Scalable Compilation of Quantum Circuits (PDF, talk)
Oechsner, Sabine	(CSF) Computer-aided proofs for multiparty computation with active security (PDF, talk)
Oepen, Jan-Hendrik	(AVOCS) Writing a Model Checker in 80 Days: Reusable Libraries and Custom Implementation (PDF, talk)
Ogawa, Hideto	(VaVAS) Policing Functions for Machine Learning Systems (PDF, talk)
Ogawa, Mizuhito	(SCSC) Wrapping Computer Algebra is Surprisingly Successful for Non-Linear SMT (PDF, talk)
Oh, Chanseok	(SAT) Machine Learning-based Restart Policy for CDCL SAT Solvers (PDF, talk)
Oitavem, Isabel	(LCC) A recursion-theoretic characterisation of the positive polynomial-time functions (PDF, talk)
Okada, Mitsuhiro	(TERMGRAPH) On quasi ordinal diagram systems (PDF, talk)
Olarte, Carlos	(Linearity/TLLA) Benchmarking Linear Logic Translations (PDF, talk)
Olimpieri, Federico	(Linearity/TLLA) On the Taylor expansion of λ-terms and the groupoid structure of their rigid approximants (PDF, talk) (HOR) Normalization and Taylor expansion of lambda-terms (PDF, talk)
Ong, Luke	(LICS) Species, Profunctors and Taylor Expansion Weighted by SMCC--A Unified Framework for Modelling Nondeterministic, Probabilistic and Quantum Programs-- (PDF, talk)
Oprea, Maria Antonia	(Isabelle) Hilbert Meets Isabelle: Formalisation of the DPRM Theorem in Isabelle (PDF, talk)
Oraee, Simin	(CAV) Symbolic Algorithms for Graphs and Markov Decision Processes with Fairness Objectives (PDF, talk)
Orlandelli, Eugenio	(ARQNL) Labelled calculi for QMLs with non-rigid and non-denoting terms (PDF, talk)
Orton, Ian	(FSCD) Internal Universes in Models of Homotopy Type Theory (PDF, talk)
Ostropolski-Nalewaja, Piotr	(LICS) Can One Escape Red Chains? Regular Path Queries Determinacy is Undecidable. (PDF, talk)
Otten, Jens	(PAAR) Proof Search Optimizations for Non-clausal Connection Calculi (PDF, talk)
Otto, Thomas	(ICLP) Experimenting with robotic intra-logistics domains (PDF, talk)
Ouaknine, Joel	(LICS) Sequential Relational Decomposition (PDF, talk) (LICS) Polynomial Invariants for Affine Programs (PDF, talk)
Overbeek, Roy	(FSCD) Decreasing diagrams with two labels are complete for confluence of countable systems (PDF, talk)
Ozay, Necmiye	(ADHS) Nonuniform abstractions, refinement and controller synthesis with novel BDD encodings (PDF, talk)
Ozay, Necmiye	(ADHS) Input Design for Nonlinear Model Discrimination Via Affine Abstraction (PDF, talk)
Ozay, Necmiye	(ADHS) Optimization-Based Design of Bounded-Error Estimators Robust to Missing Data (PDF, talk)
P
Pacheco, Hugo	(CSF) Enforcing ideal-world leakage bounds in real-world secret sharing MPC frameworks (PDF, talk)
Padget, Julian	(VaVAS) Social Consequence Engines (Abstract) (PDF, talk)
Page, Charlie	(VaVAS) Social Consequence Engines (Abstract) (PDF, talk)
Pal, Abhik	(Isabelle) Hilbert Meets Isabelle: Formalisation of the DPRM Theorem in Isabelle (PDF, talk)
Palacios, Adrián	(HCVS) Metaprogramming and symbolic execution for detecting runtime errors in Erlang programs (PDF, talk)
Palamidessi, Catuscia	(CSF) Local Differential Privacy on Metric Spaces: optimizing the trade-off with utility (PDF)
Palau Romero, Francisco	(SAT) Approximately Propagation Complete and Conflict Propagating Constraint Encodings (PDF, talk)
Palezzato, Elisa	(SCSC) New in CoCoA-5.2.4 and CoCoALib-0.99570 for SC-Square (PDF, talk)
Palmigiano, Alessandra	(ITP) Software tool support for modular reasoning in modal logics of actions (PDF, talk)
Panangaden, Prakash	(LICS) Boolean-Valued Semantics for Stochastic Lambda-Calculus (PDF, talk) (LICS) An algebraic theory of Markov processes (PDF, talk)
Panchekha, Pavel	(FM) Combining Tools for Optimization and Analysis of Floating-Point Computations (PDF, talk)
Pantel, Marc	(REFINE) Ordering strict partial orders to model behavioural refinement (PDF, talk)
Paolini, Luca	(Linearity/TLLA) Quantum programming made easy (PDF, talk)
Paquet, Hugo	(LICS) The concurrent game semantics of Probabilistic PCF (PDF, talk)
Pardo, Raúl	(FM) Timed Epistemic Knowledge Bases for Social Networks (PDF, talk)
Pardylla, Carsten	(F-IDE) Experience Report on Formally Verifying Parts of OpenJDK's API with KeY (PDF, talk) (ITP) Understanding Parameters of Deductive Verification: An Empirical Investigation of KeY (PDF, talk)
Paredes, José	(PRUV) Leveraging Probabilistic Existential Rules for Adversarial Deduplication (PDF, talk)
Park, Daejun	(CSF) KEVM: A Complete Formal Semantics of the Ethereum Virtual Machine (PDF, talk)
Park, Spencer	(F-IDE) A Notebook Format for the Holistic Design of Embedded Systems (PDF, talk)
Parker, David	(VaVAS) Policy Generation with Probabilistic Guarantees for Long-term Autonomy of a Mobile Service Robot (PDF, talk)
Parsert, Julian	(ITP) A Formally Verified Solver for Homogeneous Linear Diophantine Equations (PDF, talk) (ITP) Towards Formal Foundations for Game Theory (short paper) (PDF, talk)
Part, Fedor	(PC) Resolution with Counting: Different Moduli and Tree-Like Lower Bounds (PDF, talk)
Parys, Paweł	(FSCD) Homogeneity without Loss of Generality (PDF, talk) (ITRS) Intersection Types for Unboundedness Problems (PDF)
Pasareanu, Corina	(CSF) Symbolic Side-Channel Analysis for Probabilistic Programs (PDF, talk)
Patil, Bhagyesh	(ADHS) Multi-Energy Scheduling Using a Hybrid Systems Approach (PDF, talk)
Pattinson, Dirk	(IJCAR) A Resolution-Based Calculus for Preferential Logics (PDF, talk) (LICS) A van Benthem Theorem for Fuzzy Modal Logic (PDF, talk)
Pau, Cleo	(UNIF) Proximity-Based Generalization (PDF, talk)
Paulus, Joseph	(TYDI) Deep-Inference Intersection Types (PDF, talk)
Pauly, Arno	(SR) Beyond admissibility: Dominance between chains of strategies (PDF, talk)
Paun, Andrei	(VEMDP) Computational Approaches for the Programmed Assembly of Nanocellulose Meshes (PDF, talk)
Paun, Mihaela	(VEMDP) Computational Approaches for the Programmed Assembly of Nanocellulose Meshes (PDF, talk)
Pautasso, Daniele	(ITRS) Strong normalization of simple types through uniform intersection types. (PDF, talk)
Pavlovic, Dusko	(LICS) Sound up-to techniques and Complete abstract domains (PDF, talk)
Paxian, Tobias	(SAT) Dynamic Polynomial Watchdog Encoding for Solving Weighted MaxSAT (PDF, talk)
Payet, Etienne	(IJCAR) Checking Array Bounds by Abstract Interpretation and Symbolic Expressions (PDF, talk)
Pazii, Anna	(CSF) Local Differential Privacy on Metric Spaces: optimizing the trade-off with utility (PDF)
Peano, Andrea	(RCRA) Logic Programming approaches for routing fault-free and maximally-parallel Wavelength Routed Optical Networks on Chip (Application paper) (PDF, talk)
Pearce, David	(ICLP) Functional ASP with Intensional Sets; Application to Gelfond-Zhang Agreggates (PDF, talk)
Pecheur, Charles	(FM) Producing Explanations for Rich Logics (PDF, talk) (AVOCS) A Framework for the Formal Verification of Networks of Railway Interlockings - Application to the Belgian Railways (PDF, talk)
Peitl, Tomáš	(SAT) Polynomial-Time Validation of QCDCL Certificates (PDF, talk) (QBF) Portfolio-Based Algorithm Selection for Circuit QBFs (PDF, talk)
Pelliccione, Patrizio	(FM) Multi-Robot LTL Planning Under Uncertainty (PDF, talk)
Pellissier, Luc	(Linearity/TLLA) Generalized generalized species of structure and resource modalities (PDF, talk) (Linearity/TLLA) Entropy and Complexity Lower Bounds (PDF, talk)
Peltier, Nicolas	(ADSL) The Complexity of Prenex Separation Logic with One Selector (PDF, talk) (IJCAR) A Tableaux Calculus for Reducing Proof Size (PDF, talk) (IJCAR) A Generic Framework for Implicate Generation Modulo Theories (PDF, talk) (IJCAR) Superposition with Datatypes and Codatatypes (PDF, talk)
Perdrix, Simon	(LICS) A Complete Axiomatisation of the ZX-Calculus for Clifford+T Quantum Mechanics (PDF, talk) (LICS) Diagrammatic Reasoning beyond Clifford+T Quantum Mechanics (PDF, talk)
Pereira, Filipe	(IJCAR) A SAT-Based Approach to Learn Explainable Decision Sets (PDF, talk)
Pereira, Vitor	(CSF) Enforcing ideal-world leakage bounds in real-world secret sharing MPC frameworks (PDF, talk)
Peressotti, Marco	(Linearity/TLLA) Taking Linear Logic Apart (PDF, talk)
Petrakis, Iosif	(HoTT/UF) A Yoneda lemma-formulation of the univalence axiom (PDF, talk)
Petrasch, Jessica	(AVOCS) Writing a Model Checker in 80 Days: Reusable Libraries and Custom Implementation (PDF, talk)
Petrenko, Alexandre	(FM) FSM Inference from Long Traces (PDF, talk)
Petrucci, Laure	(CAV) Quasi-Optimal Partial Order Reduction (PDF, talk)
Pettorossi, Alberto	(HCVS) Metaprogramming and symbolic execution for detecting runtime errors in Erlang programs (PDF, talk) (ICLP) Solving Horn Clauses on Inductive Data Types Without Induction (PDF, talk)
Pfenning, Frank	(LICS) Work Analysis with Resource-Aware Session Types (PDF, talk)
Phan, Quoc-Sang	(CSF) Symbolic Side-Channel Analysis for Probabilistic Programs (PDF, talk)
Phillips, Andrew	(VEMDP) Rule-based Design of Computational DNA Devices (PDF, talk)
Pich, Ján	(LCC) Feasibly constructive proofs of succinct weak circuit lower bounds (PDF, talk)
Pick, Lauren	(CAV) Exploiting Synchrony and Symmetry in Relational Verification (PDF, talk)
Pientka, Brigitte	(FSCD) Index-Stratified Types (PDF, talk)
Pierce, Ken	(Overture) Design Space Exploration for Secure Building Control (PDF, talk) (Overture) Multi-modelling of Cooperative Swarms (PDF, talk)
Pignard, Pascal	(AVOCS) Climbing the Software Assurance Ladder - Practical Formal Verification for Reliable Software (PDF, talk)
Pike, Lee	(CAV) Formal Verification of a Vehicle-to-Vehicle (V2V) Messaging System (PDF, talk)
Pilipczuk, Michał	(LICS) Definable decompositions for graphs of bounded linear cliquewidth (PDF, talk) (LICS) Parameterized circuit complexity of model-checking on sparse structures (PDF, talk) (LICS) On the number of types in sparse graphs (PDF, talk)
Pimentel, Elaine	(WiL) A semantical view of sequent based systems (PDF, talk) (TYDI) Sequentialising nested systems (PDF, talk) (Linearity/TLLA) Benchmarking Linear Logic Translations (PDF, talk)
Pin, Edwin	(LCC) Completeness in the Second Level of the Polynomial Time Hierarchy through Syntactic Properties (PDF, talk)
Pinchinat, Sophie	(CSF) Guided design of attack trees: a system-based approach (PDF, talk)
Piotrowski, Bartosz	(IJCAR) ATPboost: Learning Premise Selection in Binary Setting with ATP Feedback (PDF, talk)
Piotrów, Marek	(POS) Competitive Sorter-based Encoding of PB-Constraints into SAT (PDF, talk)
Piróg, Maciej	(LICS) Syntax and Semantics for Operations with Scopes (PDF, talk)
Pistone, Paolo	(Linearity/TLLA) Proof nets, coends and the Yoneda isomorphism (PDF, talk)
Pitts, Andrew M.	(FSCD) Internal Universes in Models of Homotopy Type Theory (PDF, talk) (HoTT/UF) Dependent Right Adjoint Types (PDF, talk)
Pizani Flor, João Paulo	(ITP) Verified Timing Transformations in Synchronous Circuits with LambdaPi-Ware (PDF, talk)
Plaisted, David	(TERMGRAPH) Programming by Term Rewriting (PDF, talk)
Platzer, Andre	(ADHS) CoasterX: A Case Study in Component-Driven Hybrid Systems Proof Automation (PDF, talk)
Platzer, André	(FM) Vector Barrier Certificates and Comparison Systems (PDF, talk) (IJCAR) Uniform Substitution for Differential Game Logic (PDF, talk) (LICS) A Hybrid, Dynamic Logic for Hybrid-Dynamic Information Flow (PDF, talk) (LICS) Differential Equation Axiomatization: The Impressive Power of Differential Ghosts (PDF, talk)
Plesa, Tomislav	(VEMDP) Noise Control for Molecular Computing (PDF, talk)
Plotkin, Gordon	(LICS) An algebraic theory of Markov processes (PDF, talk)
Poettering, Bertram	(CSF) A Cryptographic Look at Multi-Party Channels (PDF, talk)
Pola, Giordano	(ADHS) On Approximate Predictability of Metric Systems (PDF, talk)
Polgreen, Elizabeth	(CAV) Counterexample Guided Inductive Synthesis Modulo Theories (PDF, talk)
Pontelli, Enrico	(ICLP) Natural Language Generation From Ontologies: Application Paper (PDF, talk) (ICLP) Phylotastic: An Experiment in Creating, Manipulating, and Evolving Phylogenetic Biology Workflows Using Logic Programming (PDF, talk) (ICLP) MASP-Reduce: a proposal for distributed computation of stable models (PDF, talk)
Porncharoenwase, Sorawee	(FM) CompoSAT: Specification-Guided Coverage for Model Finding (PDF, talk)
Portela, Bernardo	(CSF) Enforcing ideal-world leakage bounds in real-world secret sharing MPC frameworks (PDF, talk)
Postan, Ezequiel	(UITP) Partial Regularization of First-Order Resolution Proofs (PDF, talk)
Postoyan, Romain	(ADHS) Network-Aware Design of State-Feedback Controllers for Linear Wireless Networked Control Systems (PDF, talk)
Potet, Marie-Laure	(CAV) Model Generation for Quantified Formulas: A Taint-Based Approach (PDF, talk)
Potyka, Nico	(PRUV) Measuring Disagreement among Knowledge Bases (PDF, talk)
Poulsen, Danny Bøgsted	(FM) Statistical Model Checking of LLVM Code (PDF, talk)
Pouly, Amaury	(LICS) Polynomial Invariants for Affine Programs (PDF, talk)
Pous, Damien	(ITP) A Formal Proof of the Minor-Exclusion Property for Treewidth-Two Graphs (PDF, talk) (LICS) Allegories: decidability and graph homomorphisms (PDF, talk)
Powell, Thomas	(LICS) A functional interpretation with state (PDF, talk)
Pradic, Pierre	(LICS) LMSO: A Curry-Howard Approach to Church's Synthesis via Linear Logic (PDF, talk) (PARIS) LMSO: A Curry-Howard Approach to Church’s Synthesis via Linear Logic (PDF, talk)
Praveen, M.	(LICS) Playing with Repetitions in Data Words Using Energy Games (PDF, talk)
Preiner, Mathias	(CAV) BTOR2, BtorMC and Boolector 3.0 (PDF, talk) (CAV) Solving Quantified Bit-Vectors using Invertibility Conditions (PDF, talk) (SMT) Rewrites for SMT Solvers using Syntax-Guided Enumeration (PDF, talk)
Preto, Sandro	(IJCAR) Probably Half True: Probabilistic Satisfiability over Lukasiewicz Infinitely-valued Logic (PDF, talk)
Previti, Alessandro	(ICLP) Cautious Reasoning in ASP via Minimal models and Unsatisfiable Cores (PDF, talk)
Proietti, Maurizio	(HCVS) Metaprogramming and symbolic execution for detecting runtime errors in Erlang programs (PDF, talk) (ICLP) Solving Horn Clauses on Inductive Data Types Without Induction (PDF, talk)
Pu, Geguang	(WiL) First-Order vs. Second-Order Encodings for LTLf-to-Automata: An Extended Abstract (PDF, talk) (CAV) SimpleCAR: An Efficient Bug-Finding Tool Based On Approximate Reachability (PDF, talk)
Pulina, Luca	(SAT) Constrained Image Generation Using Binarized Neural Networks with Decision Procedures (PDF, talk)
Purandare, Rahul	(FM) Dynamic Symbolic Verification of MPI Programs (PDF, talk)
Putot, Sylvie	(CAV) Inner and Outer Approximating Flowpipes for Delay Differential Equations (PDF, talk)
Püschel, Markus	(CAV) Fast Numerical Program Analysis with Reinforcement Learning (PDF, talk)
Q
Qadeer, Shaz	(CAV) Layered Concurrent Programs (PDF) (CAV) On the Completeness of Verifying Message Passing Programs under Bounded Asynchrony (PDF, talk)
Qin, Shengchao	(FM) Towards `Verifying' a Water Treatment System (PDF, talk)
Qin, Xudong	(AVOCS) Using SMT engine to generate Symbolic Automata (PDF, talk)
Qu, Hongyang	(VaVAS) Towards a verifiable decision making framework for self-driving vehicles (PDF, talk)
Quaresma, Pedro	(ThEdu) Rating of Geometric Automated Theorem Provers (PDF, talk)
Quatmann, Tim	(MoRe) Multiple Objectives and Cost Bounds in MDP (PDF, talk) (CAV) Sound Value Iteration (PDF, talk)
R
Rabe, Florian	(IJCAR) Theories as Types (PDF, talk)
Rabe, Markus N.	(CAV) Understanding and Extending Incremental Determinization for 2QBF (PDF, talk)
Rademaker, Alexandre	(NLCS) OpenWordNet-PT: Taking Stock (PDF, talk)
Radomirovic, Sasa	(CSF) Alethea: A Provably Secure Random Sample Voting Protocol (PDF, talk) (CSF) Automated Unbounded Verification of Stateful Cryptographic Protocols with Exclusive OR (PDF, talk)
Raffalli, Christophe	(LFMTP) Abstract Representation of Binders in OCaml using the Bindlib Library (PDF, talk)
Rahli, Vincent	(LICS) Computability Beyond Church-Turing via Choice Sequences (PDF, talk)
Rajani, Vineet	(CSF) Types for Information Flow Control: Labeling Granularity and Semantic Models (PDF, talk)
Rakotonirina, Itsaka	(CAV) The DEEPSEC prover (PDF, talk)
Ralph, Benjamin	(TYDI) Deep Inference, Herbrand's Theorem and Expansion Proofs (PDF, talk)
Ramakrishnan, C. R.	(ICLP) Constraint-Based Inference in Probabilistic Logic Programs (PDF, talk)
Raman, Vasumathi	(ADHS) Generating Dominant Strategies for Continuous Two-Player Zero-Sum Games (PDF, talk)
Ramanayake, Revantha	(TYDI) Sequentialising nested systems (PDF, talk)
Rambow, Thomas	(FM) Verifying Auto-Generated C Code from Simulink (PDF, talk) (FM) Formal Verification of Automotive Simulink Controller Models: Empirical Technical Challenges, Evaluation and Recommendations (PDF, talk)
Ramirez-Trevino, Antonio	(ADHS) Observability of Linear Hybrid Systems with Unknown Inputs and Discrete Dynamics Modeled by Petri Nets (PDF, talk)
Ramsdell, John	(FCS) Homomorphisms and Minimality for Enrich-by-Need Security Analysis (PDF, talk)
Randour, Mickael	(MoRe) Stochastic o-minimal hybrid systems (PDF, talk)
Ranzato, Francesco	(CAV) Program Analysis is Harder than Verification: A Computability Perspective (PDF, talk)
Rapp, Franziska	(IJCAR) FORT 2.0 (PDF, talk) (IWC) Towards a Verified Decision Procedure for Confluence of Ground Term Rewrite Systems in Isabelle/HOL (PDF, talk)
Rasconi, Riccardo	(RCRA) Greedy Randomized Search for Scalable Compilation of Quantum Circuits (PDF, talk)
Raskin, Jean-François	(MoRe) Constraint Problem for Weak Subgame Perfect Equilibria with omega-regular Boolean Objectives (PDF, talk) (MoRe) Parameterized complexity of games with monotonically ordered omega-regular objectives (PDF, talk) (MoRe) Safe and Optimal Scheduling of Hard and Soft Tasks (PDF, talk) (SR) Beyond admissibility: Dominance between chains of strategies (PDF, talk) (LICS) Rational Synthesis Under Imperfect Information (PDF, talk)
Rasmussen, Cameron	(CAV) Understanding and Extending Incremental Determinization for 2QBF (PDF, talk)
Ratsch-Heitmann, Michel	(ICLP) Routing Driverless Transport Vehicles in Car Assembly with Answer Set Programming (PDF, talk)
Ravara, António	(HCVS) A simple functional presentation and an inductive correctness proof of the Horn algorithm (PDF, talk) (DCM) Pointing to Private Names (PDF, talk)
Rawson, Michael	(PAAR) Dynamic Strategy Priority: Empower the strong and abandon the weak (PDF, talk)
Razavi, Joseph	(DCM) A Category Theoretic Interpretation of Gandy’s Principles for Mechanisms (PDF, talk)
Real, Livy	(NLCS) OpenWordNet-PT: Taking Stock (PDF, talk) (NLCS) Graph Knowledge Representations for SICK (PDF, talk)
Reale, Kristian	(LPOP) Role-Based Access Control via JASP (PDF, talk) (LPOP) On the Development of Industrial Applications with ASP (PDF, talk)
Rebola-Pardo, Adrian	(IJCAR) Extended Resolution Simulates DRAT (PDF, talk) (POS) Two flavors of DRAT (PDF, talk)
Reeves, Steve	(F-IDE) Integrating user design and formal models within PVSio-Web (PDF, talk)
Reger, Giles	(PAAR) Set of Support for Higher-Order Reasoning (PDF, talk) (PAAR) Dynamic Strategy Priority: Empower the strong and abandon the weak (PDF, talk) (SMT) What is the Point of an SMT-LIB Problem? (PDF, talk) (ARQNL) Some thoughts about FOL-translations in Vampire (PDF)
Reimer, Sven	(SAT) Dynamic Polynomial Watchdog Encoding for Solving Weighted MaxSAT (PDF, talk)
Reis, Giselle	(WiL) Towards a Playground for Logicians (PDF, talk) (Linearity/TLLA) Formalization of Automated Trading Systems in a Concurrent Linear Framework (PDF, talk) (Linearity/TLLA) Benchmarking Linear Logic Translations (PDF, talk)
Reitwiessner, Christian	(SMT) SMT-based Compile-time Verification of Safety Properties for Smart Contracts (PDF, talk)
Ren, Hao	(F-IDE) The CLEAR Way To Transparent Formal Methods (PDF, talk)
Resch, Stefan	(TLA) Applying TLA+ in a Safety-Critical Railway Project (PDF)
Retoré, Christian	(NLCS) Do different syntactic trees yield different logical readings? Some remarks on head variables in typed lambda calculus. (PDF, talk)
Rety, Pierre	(FSCD) Confluence of Prefix-Constrained Rewrite Systems (PDF, talk)
Reynier, Pierre-Alain	(FM) Optimal and Robust Controller Synthesis Using Energy Timed Automata with Uncertainty (PDF, talk)
Reynolds, Andrew	(IJCAR) Datatypes with Shared Selectors (PDF, talk) (CAV) Solving Quantified Bit-Vectors using Invertibility Conditions (PDF, talk) (SMT) Rewrites for SMT Solvers using Syntax-Guided Enumeration (PDF, talk) (SMT) Higher-Order SMT Solving (PDF, talk)
Riba, Colin	(LICS) LMSO: A Curry-Howard Approach to Church's Synthesis via Linear Logic (PDF, talk) (PARIS) LMSO: A Curry-Howard Approach to Church’s Synthesis via Linear Logic (PDF, talk)
Ribeiro, Pedro	(VaVAS) RoboTool: Modelling and Verification with RoboChart (PDF, talk)
Ricca, Francesco	(LPOP) Role-Based Access Control via JASP (PDF, talk) (LPOP) On the Development of Industrial Applications with ASP (PDF, talk) (RCRA) Externally Supported Models for Efficient Computation of Paracoherent Answer Sets (PDF, talk)
Riccobene, Elvinia	(F-IDE) AsmetaF: a flattener for the ASMETA framework (PDF, talk)
Riener, Martin	(SMT) What is the Point of an SMT-LIB Problem? (PDF, talk)
Rieu-Helft, Raphaël	(IJCAR) A Why3 framework for reflection proofs and its application to GMP's algorithms (PDF, talk)
Rijke, Egbert	(LICS) Higher Groups in Homotopy Type Theory (PDF, talk)
Ringeissen, Christophe	(UNIF) Knowledge Problems in Equational Extensions of Subterm Convergent Theories (PDF, talk)
Ritirc, Daniela	(SCSC) A Practical Polynomial Calculus for Arithmetic Circuit Verification (PDF, talk)
Rivière, Cédric	(MoRe) Stochastic o-minimal hybrid systems (PDF, talk)
Rizkallah, Christine	(ITP) A Formal Equational Theory for Call-By-Push-Value (PDF, talk)
Robere, Robert	(CAV) The Proof Complexity of SMT Solvers (PDF, talk)
Roberts, Hannah	(SAT) XORSAT Set Membership Filters (PDF, talk)
Robillard, Simon	(IJCAR) Superposition with Datatypes and Codatatypes (PDF, talk)
Rocha, Ricardo	(ICLP) Improving Candidate Quality of Probabilistic Logic Models (PDF, talk)
Rodrigues, Nishant	(CSF) KEVM: A Complete Formal Semantics of the Ethereum Virtual Machine (PDF, talk)
Rodríguez, César	(FM) Dynamic Symbolic Verification of MPI Programs (PDF, talk) (CAV) Quasi-Optimal Partial Order Reduction (PDF, talk)
Roeck, Franz	(CAV) A Counting Semantics for Monitoring LTL Specifications over Finite Traces (PDF, talk)
Rohan, Thakker	(ADHS) Temporal Logic Control of POMDPs Via Label-Based Stochastic Simulation Relations (PDF, talk)
Ronchi Della Rocca, Simona	(ITRS) Strong normalization of simple types through uniform intersection types. (PDF, talk)
Rondogiannis, Panos	(ICLP) Approximation Fixpoint Theory and the Well-Founded Semantics of Higher-Order Logic Programs (PDF, talk)
Roohi, Nima	(ADHS) Statistical Verification of PCTL Using Stratified Samples (PDF, talk)
Roscoe, Timothy	(ITP) Physical addressing on real hardware in Isabelle/HOL (PDF, talk)
Rosenthal, Arnon	(FCS) An Expressive, Flexible and Uniform Logical Formalism for Attribute-based Access Control (PDF, talk)
Rossmanith, Peter	(LaSh) Courcelle’s Theorem – A Game-Theoretic Approach (PDF, talk)
Rosu, Grigore	(FSCD) Formal Design, Implementation and Verification of Blockchain Languages (PDF) (LFMTP) Why and How Does K work? The Logical Infrastructure Behind It (PDF) (CSF) KEVM: A Complete Formal Semantics of the Ethereum Virtual Machine (PDF, talk)
Rothenberger, Ralf	(SAT) Sharpness of the Satisfiability Threshold for Non-Uniform Random k-SAT (PDF, talk)
Rouahi, Aouatef	(PRUV) Evidential Group Decision Making Model with Belief-Based Preferences (PDF, talk)
Rouhling, Damien	(Coq) Classical Analysis with Coq (PDF, talk)
Roveri, Marco	(SAT) Experimenting on Solving Nonlinear Integer Arithmetic with Incremental Linearization (PDF, talk)
Roversi, Luca	(Linearity/TLLA) Quantum programming made easy (PDF, talk)
Rowe, Reuben	(WiL) Non-well-founded proof system for Transitive Closure Logic (PDF, talk) (PARIS) Transitive Closure Logic: Infinitary and Cyclic Proof Systems (PDF, talk)
Rozier, Kristin Yvonne	(CAV) SimpleCAR: An Efficient Bug-Finding Tool Based On Approximate Reachability (PDF, talk)
Rubin, Sasha	(SR) Verification of Multi-agent Systems with Imperfect Information and Public Actions (PDF, talk) (SR) Strategy Logic with Imperfect Information (PDF, talk) (SR) Quantifying Bounds in Strategy Logic (PDF, talk)
Rubio, Albert	(FM) SDN-Actors: Modeling and Verification of SDN Programs (PDF, talk) (CAV) Constrained Dynamic Partial Order Reduction (PDF, talk)
Ruchkin, Ivan	(FM) IPL: An Integration Property Language for Multi-Model Cyber-Physical Systems (PDF, talk)
Ruess, Harald	(FM) Evidential and Continuous Integration of Software Verification Tools (PDF, talk)
Runge, Mario	(ICLP) Routing Driverless Transport Vehicles in Car Assembly with Answer Set Programming (PDF, talk)
Ruoppolo, Domenico	(HOR) The next 700 (type-theoretical) denotational models ? (PDF, talk)
Russo, Alessandra	(ICLP) Learning Commonsense Knowledge through Interactive Dialogue (PDF, talk)
Ryvchin, Vadim	(SAT) Chronological Backtracking (PDF, talk)
Régis-Gianas, Yann	(FM) Modular Verification of Programs with Effects and Effect Handlers in Coq (PDF, talk)
Röblitz, Susanna	(RCRA) Computing Personalised Treatments through In Silico Clinical Trials. A Case Study on Downregulation in Assisted Reproduction. (PDF, talk)
Rümmer, Philipp	(IJCAR) Exploring Approximations for Floating-Point Arithmetic using UppSAT (PDF, talk) (SMT) The next 10^4 UppSAT Approximations (PDF, talk)
S
Sa'Ar, Yaniv	(CAV) Synthesis Of Asynchronous Reactive Programs From Temporal Specifications (PDF, talk)
Sabel, David	(FSCD) Nominal Unification with Atom and Context Variables (PDF, talk) (WPTE) Automating the Diagram Method to Prove Correctness of Program Transformations (PDF, talk)
Sabuncu, Orkunt	(ICLP) Experimenting with robotic intra-logistics domains (PDF, talk)
SAGER, Basma	(RCRA) An Enhanced Genetic Algorithm with the BLF2G Guillotine Placement Heuristic for the Orthogonal Cutting-Stock Problem (PDF, talk)
Sagiv, Mooly	(SAT) Constrained Image Generation Using Binarized Neural Networks with Decision Procedures (PDF, talk)
Sahlman, Lorenz	(CAV) Inner and Outer Approximating Flowpipes for Delay Differential Equations (PDF, talk)
Salazar, Elmer	(ICLP) Constraint Answer Set Programming without Grounding (PDF, talk)
Salvo, Ivano	(RCRA) Computing Personalised Treatments through In Silico Clinical Trials. A Case Study on Downregulation in Assisted Reproduction. (PDF, talk)
Sammartino, Matteo	(FM) SDN-Actors: Modeling and Verification of SDN Programs (PDF, talk)
Sampath, Mohasha Isuru	(ADHS) Multi-Energy Scheduling Using a Hybrid Systems Approach (PDF, talk)
Sanan, David	(FM) Compositional Reasoning for Shared-variable Concurrent Programs (PDF, talk)
Sanchez, Cesar	(FM) Timed Epistemic Knowledge Bases for Social Networks (PDF, talk)
Sanfelice, Ricardo	(ADHS) Sufficient Conditions for Temporal Logic Specifications in Hybrid Dynamical Systems (PDF, talk)
Sangiorgi, Davide	(LICS) Eager Functions as Processes (PDF, talk)
Sangiovanni-Vincentelli, Alberto	(ADHS) Generating Dominant Strategies for Continuous Two-Player Zero-Sum Games (PDF, talk)
Sankaranarayanan, Sriram	(ADHS) Learning and Verification of Feedback Control Systems Using Feedforward Neural Networks (PDF, talk)
Sankur, Ocan	(LICS) Stochastic Shortest Paths and Weight-Bounded Properties in Markov Decision Processes (PDF, talk)
Santhanam, Rahul	(SAT) Modelling SAT (PDF)
Santucci, Valentino	(RCRA) Algebraic Crossover Operators for Permutations (PDF, talk)
Saoud, Adnane	(ADHS) Symbolic Models for Incrementally Stable Switched Systems with Aperiodic Time Sampling (PDF, talk)
Sarac, N Ege	(LICS) A Theory of Register Monitors (PDF, talk)
Sasse, Ralf	(CSF) Automated Unbounded Verification of Stateful Cryptographic Protocols with Exclusive OR (PDF, talk)
Satake, Yuki	(CAV) Propositional Dynamic Logic for Higher-Order Functional Programs (PDF, talk)
Sato, Genki	(HoTT/UF) Geometric realization of truncated semi-simplicial sets meta-constructed within HoTT (PDF, talk)
Sato, Naoto	(VaVAS) Policing Functions for Machine Learning Systems (PDF, talk)
Saxena, Aseem	(SAT) Effective use of SMT solvers for Program Equivalence Checking through Invariant Sketching and Query Decomposition (PDF, talk)
Saxena, Manasvi	(CSF) KEVM: A Complete Formal Semantics of the Ethereum Virtual Machine (PDF, talk)
Scedrov, Andre	(IJCAR) A Logical Framework with Commutative and Non-Commutative Subexponentials (PDF, talk) (FCS) Statistical Model Checking of Guessing and Timing Attacks on Distance-bounding Protocols (PDF, talk)
Schachte, Peter	(ICLP) An iterative approach to precondition inference using constrained Horn clauses (PDF, talk)
Schaefer, Ina	(F-IDE) Experience Report on Formally Verifying Parts of OpenJDK's API with KeY (PDF, talk) (ITP) Understanding Parameters of Deductive Verification: An Empirical Investigation of KeY (PDF, talk)
Schalk, Andrea	(DCM) A Category Theoretic Interpretation of Gandy’s Principles for Mechanisms (PDF, talk)
Schaub, Torsten	(ICLP) Temporal Answer Set Programming on Finite Traces (PDF, talk) (ICLP) Experimenting with robotic intra-logistics domains (PDF, talk) (ICLP) Routing Driverless Transport Vehicles in Car Assembly with Answer Set Programming (PDF, talk) (LPOP) How to upgrade ASP for true dynamic modelling and solving? (PDF, talk)
Scheftelowitsch, Dimitri	(MoRe) Multi-Scenario Uncertainty in Markov Decision Processes (PDF, talk)
Schemmel, Daniel	(CAV) Symbolic Liveness Analysis of Real-World Software (PDF, talk)
Schindler, Tanja	(IJCAR) Efficient Interpolation for the Theory of Arrays (PDF, talk)
Schlaipfer, Matthias	(PAAR) Efficient translation of sequent calculus proofs into natural deduction proofs (PDF, talk)
Schlichtkrull, Anders	(UNIF) Formalization of First-Order Syntactic Unification (PDF, talk) (ThEdu) Natural Deduction Assistant (NaDeA) (PDF, talk) (ThEdu) Students' Proof Assistant (SPA) (PDF, talk) (IJCAR) Formalizing Bachmair and Ganzinger's Ordered Resolution Prover (PDF, talk) (PAAR) A Verified Simple Prover for First-Order Logic (PDF, talk) (Isabelle) Drawing Trees (PDF) (Isabelle) Substitutionless First-Order Logic: A Formal Soundness Proof (PDF, talk)
Schmerl, Bradley	(FM) IPL: An Integration Property Language for Multi-Model Cyber-Physical Systems (PDF, talk)
Schmid, Lara	(CSF) Alethea: A Provably Secure Random Sample Voting Protocol (PDF, talk)
Schmid, Ulrich	(ADHS) Verifying nonlinear analog and mixed-signal circuits with inputs (PDF, talk)
Schmidt, Renate A.	(IJCAR) FAME: An Automated Tool for Semantic Forgetting in Expressive Description Logics (PDF, talk)
Schmidt-Schauss, Manfred	(FSCD) Nominal Unification with Atom and Context Variables (PDF, talk) (UNIF) Rewriting with Generalized Nominal Unification (PDF, talk) (WPTE) Optimizing Space of Parallel Processes (PDF, talk)
Schneider, Gerardo	(FM) Timed Epistemic Knowledge Bases for Social Networks (PDF, talk)
Schneider, Joshua	(ITP) Relational parametricity and quotient preservation for modular (co)datatypes (PDF, talk)
Schneider, Klaus	(ICLP) Optimal Scheduling for Exposed Datapath Architectures with Buffered Processing Units by ASP (PDF, talk)
Schneider, Valentin	(TLA) Modeling Virtual Machines and Interrupts in TLA+ & PlusCal (PDF)
Schneidewind, Clara	(CAV) Foundations and Tools for the Static Analysis of Ethereum smart contracts (PDF)
Schnepf, Nicolas	(AVOCS) Rule-Based Synthesis of Chains of Security Functions for Software-Defined Networks (PDF, talk)
Scholl, Christoph	(SAT) Dependency Quantified Boolean Formulas: An Overview of Solution Methods and Applications (PDF)
Schrammel, Peter	(WST) Procedure-Modular Termination Analysis (PDF, talk) (CAV) JBMC: A Bounded Model Checking Tool for Verifying Java Bytecode (PDF, talk)
Schrijvers, Tom	(ITP) Formalization of a Polymorphic Subtyping Algorithm (PDF, talk) (LICS) Syntax and Semantics for Operations with Scopes (PDF, talk)
Schröder, Lutz	(LICS) A van Benthem Theorem for Fuzzy Modal Logic (PDF, talk)
Schubert, Aleksy	(ICLP) First-order answer set programming as constructive proof search (PDF, talk)
Schuhmann, Anna	(ICLP) Temporal Answer Set Programming on Finite Traces (PDF, talk)
Schultz, William	(TLA) An Animation Module For TLA+ (PDF)
Schulz, Stephan	(ITP) ProofWatch: Watchlist Guidance for Large Theories in E (PDF, talk)
Schulze, Uwe	(FM) Model-Based Testing for Avionics Systems (PDF, talk)
Schwitter, Rolf	(ICLP) Specifying and Verbalising Answer Set Programs in Controlled Natural Language (PDF, talk)
Schöpf, Jonas	(ITP) A Formally Verified Solver for Homogeneous Linear Diophantine Equations (PDF, talk) (WST) TTT2 with Termination Templates for Teaching (PDF, talk)
Scialanca, Agostino	(RCRA) Optimal Fault-Tolerant Placement of Relay Nodes in a Mission Critical Wireless Network (PDF, talk)
Sciarappa, Luke	(LICS) Computable decision-making on the reals and other spaces via partiality and nondeterminism (PDF, talk)
Scott, Dana	(LICS) Boolean-Valued Semantics for Stochastic Lambda-Calculus (PDF, talk)
Seatzu, Carla	(ADHS) Tracking Control via Variable-gain Integrator and Lookahead Simulation: Application to Leader-follower Multiagent Networks (PDF, talk)
Sebastiani, Roberto	(SAT) Experimenting on Solving Nonlinear Integer Arithmetic with Incremental Linearization (PDF, talk)
Sedwards, Sean	(ADHS) Bounding Errors Due to Switching Delays in Incrementally Stable Switched Systems (PDF, talk)
Seidl, Helmut	(CSF) Inductive Invariants for Noninterference in Multi-agent Workflows (PDF, talk)
Seidl, Martina	(SAT) Symmetries for QBF (PDF, talk) (PC) The Symmetry Rule for Quantified Boolean Formulas (PDF)
Seiller, Thomas	(Linearity/TLLA) Coherent interaction graphs: a nondeterministic geometry of interaction for MLL (PDF, talk) (Linearity/TLLA) A semantic conjecture on second-order MLL and its complexity consequences (work in progress) (PDF, talk) (Linearity/TLLA) Entropy and Complexity Lower Bounds (PDF, talk)
Sekanina, Lukas	(CAV) ADAC: Automated Design of Approximate Circuits (PDF, talk)
Sekerinski, Emil	(F-IDE) A Notebook Format for the Holistic Design of Embedded Systems (PDF, talk) (REFINE) Refining Santa: An Excercise in Efficient Synchronization (PDF, talk)
Selinger, Peter	(FSCD) Challenges in quantum programming languages (PDF)
Sellami, Yanis	(IJCAR) A Generic Framework for Implicate Generation Modulo Theories (PDF, talk)
Sellis, Timos	(ICLP) A Trajectory Calculus for Qualitative Spatial Reasoning Using Answer Set Programming (PDF, talk)
Serban, Cristina	(AVOCS) An Entailment Checker for Separation Logic with Inductive Definitions (PDF, talk)
Servetto, Marco	(DCM) A syntactic model of mutation and aliasing (PDF, talk)
Seshia, Sanjit	(ADHS) Generating Dominant Strategies for Continuous Two-Player Zero-Sum Games (PDF, talk)
Seshia, Sanjit A.	(CAV) Reactive Control Improvisation (PDF, talk) (CAV) Understanding and Extending Incremental Determinization for 2QBF (PDF, talk)
Shah, Shetal	(CAV) What’s hard about Boolean Functional Synthesis? (PDF, talk)
Shakerin, Farhad	(ICLP) Cumulative Scoring-based Induction of Default Theories (PDF, talk)
Shankara Narayanan, Krishna	(LICS) Regular and First Order List Functions (PDF, talk) (LICS) Regular Transducer Expressions for Regular Transformations over infinite words (PDF, talk)
Sharaf, Nada	(ICLP) CHRvis: Syntax and Semantics (PDF, talk)
Sharma, Subodh	(FM) Dynamic Symbolic Verification of MPI Programs (PDF, talk)
Sharygina, Natasha	(VSTTE) Lattice-Based Refinement in Bounded Model Checking (PDF, talk)
Shaulian, Yariv	(LICS) Automaton-Based Criteria for Membership in CTL (PDF, talk)
Shen, Da	(ICLP) SMT-based Answer Set Solver CMODELS(DIFF) (System Description) (PDF, talk)
Sherman, Benjamin	(LICS) Computable decision-making on the reals and other spaces via partiality and nondeterminism (PDF, talk)
Shintani, Kiraku	(FSCD) Confluence Competition 2018 (PDF)
Shkapsky, Alex	(ICLP) Declarative Algorithms in Datalog with Aggregates: user-friendly formal semantics conducive to performance and scalability (PDF, talk)
Shoham, Sharon	(SMT) Discovering Universally Quantified Solutions for Constrained Horn Clauses (PDF, talk)
Sickert, Salomon	(CAV) Rabinizer 4: From LTL to Your Favourite Deterministic Automaton (PDF, talk) (CAV) Strix: Explicit Reactive Synthesis Strikes Back! (PDF, talk) (LICS) One Theorem to Rule Them All: A Unified Translation of LTL into $\omega$-Automata (PDF, talk)
Siebertz, Sebastian	(LICS) Parameterized circuit complexity of model-checking on sparse structures (PDF, talk) (LICS) On the number of types in sparse graphs (PDF, talk)
Siek, Jeremy	(UNIF) Efficiency of a Good but not Linear Nominal Unification Algorithm (PDF, talk)
Siekmann, Joerg	(UNIF) Unification Based on Generalized Embedding (PDF, talk)
Silva, Alexandra	(FM) SDN-Actors: Modeling and Verification of SDN Programs (PDF, talk)
Simari, Gerardo	(PRUV) Leveraging Probabilistic Existential Rules for Adversarial Deduplication (PDF, talk)
Singh, Gagandeep	(CAV) Fast Numerical Program Analysis with Reinforcement Learning (PDF, talk)
Sinisi, Stefano	(RCRA) Computing Personalised Treatments through In Silico Clinical Trials. A Case Study on Downregulation in Assisted Reproduction. (PDF, talk)
Sinz, Carsten	(POS) A Problem Meta-Data Library for Research in SAT (PDF, talk)
Sistla, Prasad	(CAV) Model checking indistinguishability of randomized security protocols (PDF, talk)
Skočovský, Peter	(IJCAR) Enumerating Justifications using Resolution (PDF, talk)
Slivovsky, Friedrich	(SAT) Polynomial-Time Validation of QCDCL Certificates (PDF, talk) (QBF) Portfolio-Based Algorithm Selection for Circuit QBFs (PDF, talk)
Smallbone, Nicholas	(IJCAR) Efficient encodings of first-order Horn formulas in equational logic (PDF, talk)
Smith, Connor	(HOR) Orthogonality and sequentiality in substructural Linear HRSs (PDF, talk)
Smith, Graeme	(FM) A wide-spectrum language for verification of programs on weak memory models (PDF, talk) (REFINE) Correctness of Concurrent Objects under Weak Memory Models (PDF, talk)
Smith, Michael	(SAT) XORSAT Set Membership Filters (PDF, talk)
Smolka, Gert	(ITP) Verification of PCP-Related Computational Reductions in Coq (PDF, talk)
Smolka, Scott	(VaVAS) Adaptive Neighborhood Resizing for Stochastic Reachability in Multi-Agent Systems (PDF, talk)
Sobocinski, Pawel	(LICS) Rewriting with Frobenius (PDF, talk)
Sogokon, Andrew	(FM) Vector Barrier Certificates and Comparison Systems (PDF, talk)
Sojakova, Kristina	(LICS) A General Framework for Relational Parametricity (PDF, talk)
Solar-Lezama, Armando	(CAV) Delta-Decision Procedures for Exists-Forall Problems over the Reals (PDF, talk)
Soloveichik, David	(VEMDP) Computing Properties of Stable Configurations of Thermodynamic Binding Networks (PDF, talk)
Son, Tran Cao	(ICLP) Experimenting with robotic intra-logistics domains (PDF, talk) (ICLP) Natural Language Generation From Ontologies: Application Paper (PDF, talk) (ICLP) Phylotastic: An Experiment in Creating, Manipulating, and Evolving Phylogenetic Biology Workflows Using Logic Programming (PDF, talk)
Sondergaard, Harald	(ICLP) An iterative approach to precondition inference using constrained Horn clauses (PDF, talk)
Song, Fu	(CAV) SCInfer: Refinement-based Verification of Software Countermeasures against Side-Channel Attacks (PDF, talk) (CAV) Android Stack Machine (PDF, talk)
Soria Dustmann, Oscar	(CAV) Symbolic Liveness Analysis of Real-World Software (PDF, talk)
Soudjani, Sadegh	(ADHS) Compositional Synthesis of Finite Abstractions for Continuous-Space Stochastic Control Systems: A Small-Gain Approach (PDF, talk)
Soudjani, Sadegh	(ADHS) Temporal Logic Control of General Markov Decision Processes by Approximate Policy Refinement (PDF, talk)
Soulat, Romain	(AVOCS) Climbing the Software Assurance Ladder - Practical Formal Verification for Reliable Software (PDF, talk)
Sousa, Marcelo	(CAV) Quasi-Optimal Partial Order Reduction (PDF, talk)
Sozeau, Matthieu	(ITP) Towards Certified Meta-Programming with Typed Template-Coq (PDF, talk) (FSCD) Cumulative Inductive Types in Coq (PDF, talk) (Coq) Towards a formalization of the guard condition (PDF, talk)
Spaccasassi, Carlo	(VEMDP) Rule-based Design of Computational DNA Devices (PDF, talk)
Speight, Sam	(LICS) Impredicative Encodings of (Higher) Inductive Types (PDF, talk)
Spencer, Frankie	(VEMDP) Computational Approaches for the Programmed Assembly of Nanocellulose Meshes (PDF, talk)
Spitters, Bas	(FSCD) Internal Universes in Models of Homotopy Type Theory (PDF, talk) (HoTT/UF) Dependent Right Adjoint Types (PDF, talk) (CSF) Computer-aided proofs for multiparty computation with active security (PDF, talk)
Spoto, Fausto	(IJCAR) Checking Array Bounds by Abstract Interpretation and Symbolic Expressions (PDF, talk)
Srba, Jiri	(CAV) Start Pruning When Time Gets Urgent: Partial Order Reduction for Timed Systems (PDF, talk)
Stadler, Peter F.	(VEMDP) Rule-Based Gillespie Simulation of Chemical Systems (PDF, talk)
Starr, Andrew	(VaVAS) Towards validation and verification of an autonomous railway inspection and repair system (PDF, )
Stasch, Matthias	(SCSC) Constraint Systems from Traffic Scenarios for the Validation of Autonomous Driving (PDF, talk)
Statman, Richard	(ITRS) On sets of terms with a given intersection type (PDF, ) (HDRA) Minimal Bacus FP is Turing Complete (PDF, talk)
Steen, Alexander	(IJCAR) The Higher-Order Prover Leo-III (PDF, talk) (ARQNL) System Demonstration: The Higher-Order Prover Leo-III (PDF, talk)
Steeples, Thomas	(SR) Local Equilibria in Logic-Based Multi-Player Games (PDF, talk)
Stefanesco, Léo	(LICS) An Asynchronous Soundness Theorem for Concurrent Separation Logic (PDF, talk)
Stefanescu, Andrei	(CSF) KEVM: A Complete Formal Semantics of the Ethereum Virtual Machine (PDF, talk)
Steffen, Martin	(FM) Operational Semantics of a Weak Memory Model with Channel Synchronization (PDF, talk)
Steinberg, Florian	(LICS) Type-two polynomial-time and restricted lookahead. (PDF, talk)
Stenger, Marvin	(CAV) Synthesizing Reactive Systems from Hyperproperties (PDF, talk)
Sterling, Jonathan	(HoTT/UF) Cubical Computational Type Theory (PDF, talk) (LFMTP) The RedPRL Proof Assistant (PDF) (LICS) Guarded Computational Type Theory (PDF, talk)
Sterling, Mark	(UITP) Automated Theorem Proving in a Chat Environment (PDF, talk)
Sternagel, Christian	(ITP) A Formally Verified Solver for Homogeneous Linear Diophantine Equations (PDF, talk) (WST) TTT2 with Termination Templates for Teaching (PDF, talk) (IWC) Certified Ordered Completion (PDF, talk) (Isabelle) The remote_build Tool (PDF, talk)
Stock, Benedikt	(Isabelle) Hilbert Meets Isabelle: Formalisation of the DPRM Theorem in Isabelle (PDF, talk)
Stojic, Ivan	(FM) Formal Specification and Verification of Dynamic Parametrized Architectures (PDF, talk)
Stoller, Scott	(LPOP) Easier Rules and Constraints for Programming (PDF, talk) (TLA) Invariants in Distributed Algorithms (PDF)
Stolz, Volker	(FM) Operational Semantics of a Weak Memory Model with Channel Synchronization (PDF, talk)
Stoop, Pascal	(Isabelle) Lazy Algebraic Types in Isabelle/HOL (PDF, talk)
Stratulat, Sorin	(CL&C) Validating Back-links of FOL$_{\mbox{\normalsize ID}}$ Cyclic Pre-proofs (PDF, talk) (PARIS) Useless Explicit Induction Reasoning (PDF, talk)
Straubing, Howard	(LICS) Wreath Products of Distributive Forest Algebras (PDF, talk)
Straßburger, Lutz	(WiL) Decomposing labelled proof theory for intuitionistic modal logic (PDF, talk) (IJCAR) From Syntactic Proofs to Combinatorial Proofs (PDF, talk)
Strub, Pierre-Yves	(Coq) Classical Analysis with Coq (PDF, talk) (CSF) Computer-aided proofs for multiparty computation with active security (PDF, talk)
Stuckey, Peter J.	(ICLP) An iterative approach to precondition inference using constrained Horn clauses (PDF, talk)
Stulova, Nataliia	(ICLP) Towards Static Performance Guarantees for Programs with Run-time Checks (PDF, talk)
Stump, Aaron	(ITP) Efficient Mendler-Style Lambda-Encodings in Cedille (PDF, talk) (CL&C) (Short Paper) Towards a Dualized Sequent Calculus with Canonicity (PDF, talk)
Sturm, Thomas	(SCSC) Wrapping Computer Algebra is Surprisingly Successful for Non-Linear SMT (PDF, talk)
Stéphan, Igor	(ICLP) A New Proof-theoretical Linear Semantics for CHR (PDF, talk)
Subramanyan, Pramod	(CAV) Lazy Self-Composition for Security Verification (PDF, talk)
Suda, Martin	(SAT) Local Soundness for QBF Calculi (PDF, talk) (QBF) Towards the Semantics of QBF Clauses (PDF, talk)
Summers, Alexander J	(CAV) Permission Inference for Array Programs (PDF, talk)
Sun, Jun	(FM) Towards `Verifying' a Water Treatment System (PDF, talk) (FM) Compositional Reasoning for Shared-variable Concurrent Programs (PDF, talk)
Sunshine, Joshua	(FM) IPL: An Integration Property Language for Multi-Model Cyber-Physical Systems (PDF, talk)
Sutcliffe, Geoff	(PAAR) TFX: The TPTP Extended Typed First-order Form (PDF, talk)
Swierstra, Wouter	(ITP) Verified Timing Transformations in Synchronous Circuits with LambdaPi-Ware (PDF, talk)
Syed Mohammad, Meesum	(SCSC) Unknot Recognition Through Quantifier Elimination (PDF, talk)
Syeda, Hira	(ITP) Program Verification in the Presence of Cached Address Translation (PDF, talk)
Symeonidou, Ioanna	(ICLP) Approximation Fixpoint Theory and the Well-Founded Semantics of Higher-Order Logic Programs (PDF, talk)
Szabo, Peter	(UNIF) Unification Based on Generalized Embedding (PDF, talk)
Szasz, Nora	(LFMTP) Formalization in Constructive Type Theory of the Standardization Theorem (PDF, talk) (LFMTP) Formalisation of Barendregt's Variable Convention for Generic Structures with Binders (PDF, talk)
Szeider, Stefan	(SAT) Polynomial-Time Validation of QCDCL Certificates (PDF, talk) (QBF) Portfolio-Based Algorithm Selection for Circuit QBFs (PDF, talk)
T
T. V. H., Prathamesh	(SCSC) Unknot Recognition Through Quantifier Elimination (PDF, talk) (IWC) Towards a Verified Decision Procedure for Confluence of Ground Term Rewrite Systems in Isabelle/HOL (PDF, talk)
Tabareau, Nicolas	(ITP) Towards Certified Meta-Programming with Typed Template-Coq (PDF, talk)
Tabuada, Paulo	(ADHS) Computing Controlled Invariant Sets for Hybrid Systems with Applications to Model-Predictive Control (PDF, talk)
Tacchella, Armando	(SAT) Constrained Image Generation Using Binarized Neural Networks with Decision Procedures (PDF, talk)
Tachmazidis, Ilias	(ICLP) A Trajectory Calculus for Qualitative Spatial Reasoning Using Answer Set Programming (PDF, talk)
Takahashi, Yuta	(TERMGRAPH) On quasi ordinal diagram systems (PDF, talk)
Talcott, Carolyn	(FCS) Statistical Model Checking of Guessing and Timing Attacks on Distance-bounding Protocols (PDF, talk)
Talebanfard, Navid	(SAT) Cops-Robber games and the resolution of Tseitin formulas (PDF, talk)
Tamaroff, Pedro	(HDRA) Minimal models for monomial algebras (PDF, talk)
Tan, Yong Kiam	(FM) Vector Barrier Certificates and Comparison Systems (PDF, talk) (IJCAR) Proof-Producing Synthesis of CakeML with I/O and Local State from Monadic HOL Functions (PDF, talk) (LICS) Differential Equation Axiomatization: The Impressive Power of Differential Ghosts (PDF, talk)
Tanaka, Ribeka	(NLCS) Paychecks, Presupposition, and Dependent Types (PDF, talk)
Tang, Qiyi	(CAV) Deciding Probabilistic Bisimilarity Distance One for Labelled Markov Chains (PDF, talk)
Tarau, Paul	(RCRA) Shaving with Occam's Razor: Deriving Minimalist Theorem Provers for Minimal Logic (PDF, talk)
Tasiran, Serdar	(CAV) Reasoning About TSO Programs Using Reduction and Abstraction (PDF, talk) (CAV) Continuous formal verification of Amazon s2n (PDF, talk) (CAV) Model Checking Boot Code from AWS Data Centers (PDF, talk)
Tasistro, Alvaro	(LFMTP) Formalization in Constructive Type Theory of the Standardization Theorem (PDF, talk) (LFMTP) Formalisation of Barendregt's Variable Convention for Generic Structures with Binders (PDF, talk)
Tassarotti, Joseph	(ITP) Verified Tail Bounds for Randomized Programs (PDF, talk)
Tatlock, Zachary	(ITP) Software Verification with ITPs Should Use Binary Code Extraction to Reduce the TCB (short paper) (PDF, talk) (FM) Combining Tools for Optimization and Analysis of Floating-Point Computations (PDF, talk)
Tatsuta, Makoto	(ADSL) Cyclic Theorem Prover for Separation Logic by Magic Wand (PDF, talk)
Taupe, Richard	(ICLP-DC) Speeding Up Lazy-Grounding Answer Set Solving (PDF, talk)
Tautschnig, Michael	(CAV) Model Checking Boot Code from AWS Data Centers (PDF, talk)
Teige, Tino	(SCSC) Constraint Systems from Traffic Scenarios for the Validation of Autonomous Driving (PDF, talk)
Tekle, K. Tuncay	(LPOP) The RBAC challenge in LogiQL: Solutions and Limitations (PDF)
Tentrup, Leander	(CAV) Synthesizing Reactive Systems from Hyperproperties (PDF, talk) (CAV) Understanding and Extending Incremental Determinization for 2QBF (PDF, talk)
Ter Beek, Maurice H.	(FM) QFLan: A Tool for the Quantitative Analysis of Highly Reconfigurable Systems (PDF, talk)
Terauchi, Tachio	(LICS) Dependent Temporal Effects and Fixpoint Logic for Verification (PDF, talk)
Ternovska, Eugenia	(PRUV) A Model-Theoretic View on Preferences in Declarative Specifications of Search Problems (PDF, talk) (LaSh) A Logic of Information Flows (PDF, talk) (LaSh) A Logic of Information Flows - Paper (PDF)
Thachuk, Chris	(VEMDP) Computing Properties of Stable Configurations of Thermodynamic Binding Networks (PDF, talk)
Thakkar, Aalok	(WST) Verification of Rewriting-based Query Optimizers (PDF, talk)
Theodoropoulos, Panos	(SAT) Fast Sampling of Perfectly Uniform Satisfying Assignments (PDF, talk) (SAT) Fast and Flexible Probabilistic Model Counting (PDF, talk)
Thibodeau, David	(FSCD) Index-Stratified Types (PDF, talk)
Thiemann, René	(ITP) A Formalization of the LLL Basis Reduction Algorithm (PDF, talk) (WST) A Perron-Frobenius Theorem for Jordan Blocks for Complexity Proving (PDF, talk) (Isabelle) Formal Verification of Bounds for the LLL Basis Reduction Algorithm (PDF, talk)
Thiré, François	(LFMTP) Sharing a library between proof assistants: reaching out to the HOL family (PDF, talk)
Thomas, Ciza	(SAT) Machine Learning-based Restart Policy for CDCL SAT Solvers (PDF, talk)
Thule, Casper	(Overture) Overture FMU: Export VDM-RT Models as Tool-Wrapper FMUs (PDF, talk)
Thüm, Thomas	(F-IDE) Experience Report on Formally Verifying Parts of OpenJDK's API with KeY (PDF, talk) (ITP) Understanding Parameters of Deductive Verification: An Empirical Investigation of KeY (PDF, talk)
Tien Luong, An Thuy	(UITP) Adding Text-Based Interaction to a Direct-Manipulation Interface for Program Verification -- Lessons Learned (PDF, talk)
Timany, Amin	(FSCD) Cumulative Inductive Types in Coq (PDF, talk)
Timmis, Jon	(VaVAS) RoboTool: Modelling and Verification with RoboChart (PDF, talk)
Tinelli, Cesare	(IJCAR) Datatypes with Shared Selectors (PDF, talk) (CAV) Solving Quantified Bit-Vectors using Invertibility Conditions (PDF, talk) (SMT) Rewrites for SMT Solvers using Syntax-Guided Enumeration (PDF, talk) (SMT) Higher-Order SMT Solving (PDF, talk)
Titolo, Laura	(FM) A Formally Verified Floating-Point Implementation of the Compact Position Reporting Algorithm (PDF, talk)
Tiu, Alwen	(FM) Compositional Reasoning for Shared-variable Concurrent Programs (PDF, talk) (CSF) A Permission-Dependent Type System for Secure Information Flow Analysis (PDF, talk) (LICS) Quasi-Open Bisimilarity with Mismatch is Intuitionistic (PDF, talk)
Tiwari, Ashish	(VaVAS) Adaptive Neighborhood Resizing for Stochastic Reachability in Multi-Agent Systems (PDF, talk)
Tiwari, Ashish	(ADHS) Learning and Verification of Feedback Control Systems Using Feedforward Neural Networks (PDF, talk)
To, Van Khanh	(SCSC) Wrapping Computer Algebra is Surprisingly Successful for Non-Linear SMT (PDF, talk)
Toman, Viktor	(CAV) Symbolic Algorithms for Graphs and Markov Decision Processes with Fairness Objectives (PDF, talk)
Tomb, Aaron	(CAV) Formal Verification of a Vehicle-to-Vehicle (V2V) Messaging System (PDF, talk) (CAV) Continuous formal verification of Amazon s2n (PDF, talk)
Tomiyama, Tetsuo	(VaVAS) Towards validation and verification of an autonomous railway inspection and repair system (PDF, )
Tonetta, Stefano	(FM) Formal Specification and Verification of Dynamic Parametrized Architectures (PDF, talk)
Tonks, Zak	(SCSC) Non-linear Real Arithmetic Benchmarks derived from Automated Reasoning in Economics (PDF, talk)
Topcu, Ufuk	(ADHS) Compositional Analysis of Hybrid Systems Defined Over Finite Alphabets (PDF, talk)
Toran, Jacobo	(SAT) Cops-Robber games and the resolution of Tseitin formulas (PDF, talk)
Torfah, Hazem	(CAV) Model Checking Quantitative Hyperproperties (PDF, talk)
Torrini, Paolo	(AVOCS) Proof-Oriented Design of a Separation Kernel with Minimal Trusted Computing Base (PDF, talk)
Toruńczyk, Szymon	(LICS) On computability and tractability for infinite sets (PDF, talk) (LICS) Parameterized circuit complexity of model-checking on sparse structures (PDF, talk) (LICS) On the number of types in sparse graphs (PDF, talk)
Tourret, Sophie	(TERMGRAPH) SLD-Resolution Reduction of Second-Order Horn Fragments - Extended Abstract (PDF, talk)
Tran, Thanh Hai	(TLA) BMCMT: Bounded Model Checking of TLA+ Specifications with SMT (PDF)
Trandafir, Romica	(VEMDP) Computational Approaches for the Programmed Assembly of Nanocellulose Meshes (PDF, talk)
Traonouez, Louis-Marie	(FM) Statistical Model Checking of LLVM Code (PDF, talk)
Traytel, Dmitriy	(LaSh) A Derivative-Based Decision Procedure for WS1S (PDF, talk) (IJCAR) Formalizing Bachmair and Ganzinger's Ordered Resolution Prover (PDF, talk)
Treinen, Ralf	(IJCAR) Deciding the First-Order Theory of an Algebra of Feature Trees with Updates (PDF, talk)
Trenn, Stephan	(ADHS) Switch induced instabilities for stable power system DAE models (PDF, talk)
Trieu, Alix	(FCS) A Study on the Preservation on Cryptographic Constant-Time Security in the CompCert Compiler (PDF, talk)
Troják, Matej	(VEMDP) Executable Biochemical Space for Specification and Analysis of Biochemical Systems (PDF, talk)
Tronci, Enrico	(RCRA) Optimal Fault-Tolerant Placement of Relay Nodes in a Mission Critical Wireless Network (PDF, talk) (RCRA) Computing Personalised Treatments through In Silico Clinical Trials. A Case Study on Downregulation in Assisted Reproduction. (PDF, talk)
Trtik, Marek	(CAV) JBMC: A Bounded Model Checking Tool for Verifying Java Bytecode (PDF, talk)
Tsai, Pei-Wei	(ICLP) A Trajectory Calculus for Qualitative Spatial Reasoning Using Answer Set Programming (PDF, talk)
Tsukada, Takeshi	(LICS) Species, Profunctors and Taylor Expansion Weighted by SMCC--A Unified Framework for Modelling Nondeterministic, Probabilistic and Quantum Programs-- (PDF, talk)
Tsuruta, Yuta	(IWC) Convergence of Simultaneously and Sequentially Unraveled TRSs for Normal Conditional TRSs (PDF, talk)
Tullsen, Mark	(CAV) Formal Verification of a Vehicle-to-Vehicle (V2V) Messaging System (PDF, talk)
Tumova, Jana	(FM) Multi-Robot LTL Planning Under Uncertainty (PDF, talk)
Turberfield, Andrew J.	(VEMDP) Controlling Assembly and Function of DNA Nanostructures and Molecular Machinery (PDF)
Turuani, Mathieu	(CSF) A little more conversation, a little less action, a lot more satisfaction: Global states in ProVerif. (PDF, talk)
Tusa, Iris	(VEMDP) Computational Approaches for the Programmed Assembly of Nanocellulose Meshes (PDF, talk)
Tuttle, Mark R.	(CAV) Model Checking Boot Code from AWS Data Centers (PDF, talk)
Tzameret, Iddo	(PC) Resolution with Counting: Different Moduli and Tree-Like Lower Bounds (PDF, talk)
Tóth, Tamás	(AVOCS) Backward reachability analysis for timed automata with data variables (PDF, talk)
U
Uemura, Taichi	(HoTT/UF) Cubical Assemblies and the Independence of the Propositional Resizing Axiom (PDF, talk)
Ultes-Nitsche, Ulrich	(LICS) A Simple and Optimal Complementation Algorithm for Büchi Automata (PDF, talk)
Unno, Hiroshi	(HCVS) Horn Clauses and Beyond for Relational and Temporal Program Verification (PDF) (CAV) Propositional Dynamic Logic for Higher-Order Functional Programs (PDF, talk) (LICS) Dependent Temporal Effects and Fixpoint Logic for Verification (PDF, talk)
Urban, Caterina	(CAV) MaxSMT-Based Type Inference for Python 3 (PDF, talk) (CAV) Permission Inference for Array Programs (PDF, talk)
Urban, Josef	(ITP) ProofWatch: Watchlist Guidance for Large Theories in E (PDF, talk) (IJCAR) ATPboost: Learning Premise Selection in Binary Setting with ATP Feedback (PDF, talk)
Urbani, Jacopo	(IJCAR) Efficient Model Construction for Horn Logic with VLog: System Description (PDF, talk)
Urzyczyn, Pawel	(ICLP) First-order answer set programming as constructive proof search (PDF, talk)
V
Vacher, Jonathan	(ADHS) Control Synthesis for Stochastic Switched Systems Using the Tamed Euler Method (PDF, talk)
Vallati, Mauro	(RCRA) On the Configuration of SAT Formulae (PDF, talk)
van Breugel, Franck	(CAV) Deciding Probabilistic Bisimilarity Distance One for Labelled Markov Chains (PDF, talk)
Van Den Bogaard, Marie	(SR) Beyond admissibility: Dominance between chains of strategies (PDF, talk)
van der Hallen, Matthias	(QBF) A Grounder From Second-Order Logic To QBF (PDF, talk)
van Dijk, Tom	(CAV) Attracting Tangles to Solve Parity Games (PDF, talk)
van Doorn, Floris	(LICS) Higher Groups in Homotopy Type Theory (PDF, talk)
Van Roy, Peter	(LPOP) A software system should be declarative except where it interacts with the real world (PDF, talk)
Vandin, Andrea	(FM) QFLan: A Tool for the Quantitative Analysis of Highly Reconfigurable Systems (PDF, talk)
Vardi, Moshe	(WiL) First-Order vs. Second-Order Encodings for LTLf-to-Automata: An Extended Abstract (PDF, talk) (SR) Strategy Logic with Imperfect Information (PDF, talk) (SR) Solving Parity Games: Explicit vs Symbolic (PDF, talk) (CAV) Automata vs Linear-Programming Discounted-Sum Inclusion (PDF, talk)
Vardi, Moshe	(CAV) SimpleCAR: An Efficient Bug-Finding Tool Based On Approximate Reachability (PDF, talk)
Vardi, Moshe Y	(LICS) Sequential Relational Decomposition (PDF, talk)
Varga, János	(TERMGRAPH) Finding the Transitive Closure of Functional Dependencies using Strategic Port Graph Rewriting (PDF, talk)
Varma, Vineeth Satheeskumar	(ADHS) Network-Aware Design of State-Feedback Controllers for Linear Wireless Networked Control Systems (PDF, talk)
Varma, Vineeth Satheeskumar	(ADHS) Space-Time Budget Allocation for Marketing Over Social Networks (PDF, talk)
Vasicek, Zdenek	(CAV) ADAC: Automated Design of Approximate Circuits (PDF, talk)
Vasile, Cristian-Ioan	(ADHS) Temporal Logic Control of POMDPs Via Label-Based Stochastic Simulation Relations (PDF, talk)
Vasileva, Anna	(F-IDE) User Support for the Combinator Logic Synthesizer Framework (PDF, talk)
Vaux Auclair, Lionel	(Linearity/TLLA) On the Taylor expansion of λ-terms and the groupoid structure of their rigid approximants (PDF, talk)
Vechev, Martin	(CAV) Fast Numerical Program Analysis with Reinforcement Learning (PDF, talk)
Velan, Dominik	(LICS) Efficient Algorithms for Asymptotic Bounds on Termination Time in VASS (PDF, talk)
Veneris, Andreas	(SAT) Finding all Minimal Safe Inductive Sets (PDF, talk)
Vennekens, Joost	(ICLP) Application of Logic-Based Methods to Machine Component Design (PDF, talk) (LPOP) Logic-based Methods for Software Engineers and Business People (PDF, talk)
Verdier, Cees	(ADHS) Optimal Symbolic Controllers Determinization for BDD storage. (PDF, talk)
Veres, Sandor	(VaVAS) Towards a verifiable decision making framework for self-driving vehicles (PDF, talk)
Vial, Pierre	(LICS) Every λ-Term is Meaningful for the Infinitary Relational Model (PDF, talk) (HOR) Some applications of quantitative types inside and outside type theory (PDF)
Vicary, Jamie	(UITP) Designing Globular: formal proofs as geometrical objects (PDF) (HDRA) Normal forms for planar connected string diagrams (PDF, talk)
Vignudelli, Valeria	(FSCD) Proof techniques for program equivalence in probabilistic higher-order languages (PDF) (LICS) Allegories: decidability and graph homomorphisms (PDF, talk)
Villadsen, Jørgen	(UNIF) Formalization of First-Order Syntactic Unification (PDF, talk) (ThEdu) Natural Deduction Assistant (NaDeA) (PDF, talk) (ThEdu) Students' Proof Assistant (SPA) (PDF, talk) (ThEdu) Proving in the Isabelle Proof Assistant that the Set of Real Numbers is not Countable (PDF, talk) (PAAR) A Verified Simple Prover for First-Order Logic (PDF, talk) (Isabelle) Drawing Trees (PDF) (Isabelle) Substitutionless First-Order Logic: A Formal Soundness Proof (PDF, talk)
Villaret, Mateu	(FSCD) Term-Graph Anti-Unification (PDF, talk)
Vilmart, Renaud	(LICS) A Complete Axiomatisation of the ZX-Calculus for Clifford+T Quantum Mechanics (PDF, talk) (LICS) Diagrammatic Reasoning beyond Clifford+T Quantum Mechanics (PDF, talk)
Vinyals, Marc	(SAT) Using Combinatorial Benchmarks to Probe the Reasoning Power of Pseudo-Boolean Solvers (PDF, talk) (SAT) In Between Resolution and Cutting Planes: A Study of Proof Systems for Pseudo-Boolean SAT Solving (PDF, talk)
Viswanathan, Arjun	(IJCAR) Datatypes with Shared Selectors (PDF, talk)
Viswanathan, Mahesh	(CAV) Controller Synthesis Made Real: Reach-avoid Specifications and Linear Dynamics (PDF, talk) (CAV) Model checking indistinguishability of randomized security protocols (PDF, talk)
Viswanathan, Mahesh	(ADHS) Statistical Verification of PCTL Using Stratified Samples (PDF, talk)
Vivekanandan, Paventhan	(FCS) A Homotopical Approach to Cryptography (PDF, talk)
Vizel, Yakir	(CAV) Lazy Self-Composition for Security Verification (PDF, talk) (SMT) Discovering Universally Quantified Solutions for Constrained Horn Clauses (PDF, talk)
Vojnar, Tomas	(LaSh) Lazy Automata Techniques for WS1S (PDF, talk) (CAV) ADAC: Automated Design of Approximate Circuits (PDF, talk)
Vollmer, Heribert	(LICS) Model-Theoretic Characterizations of Boolean and Arithmetic Circuit Classes of Small Depth (PDF, talk)
von Glehn, Tamara	(LICS) Dialectica models of type theory (PDF, talk)
Voronkov, Andrei	(IJCAR) A FOOLish Encoding of the Next State Relations of Imperative Programs (PDF, talk)
Vu, Xuan Tung	(SCSC) Wrapping Computer Algebra is Surprisingly Successful for Non-Linear SMT (PDF, talk)
Vuotto, Simone	(DS-FM) Consistency Checking of Functional Requirements (PDF, talk)
Vyas, Nikhil	(LICS) Distribution-based objectives for Markov Decision Processes (PDF, talk)
Vörös, András	(AVOCS) Backward reachability analysis for timed automata with data variables (PDF, talk)
W
W. V. Tran-Jørgensen, Peter	(Overture) Enhancing Testing of VDM-SL models (PDF, talk)
Waez, Md Tawhid Bin	(FM) Verifying Auto-Generated C Code from Simulink (PDF, talk) (FM) Formal Verification of Automotive Simulink Controller Models: Empirical Technical Challenges, Evaluation and Recommendations (PDF, talk)
Wagner, Lucas	(CAV) The JKind Model Checker (PDF, talk)
Waldmann, Johannes	(WST) Semantic Kachinuki Order (PDF, talk)
Waldmann, Uwe	(IJCAR) Superposition for Lambda-Free Higher-Order Logic (PDF, talk) (IJCAR) Formalizing Bachmair and Ganzinger's Ordered Resolution Prover (PDF, talk)
Wallace, Richard	(RCRA) Partial (Neighbourhood) Singleton Arc Consistency for Constraint Satisfaction Problems (PDF, talk) (RCRA) Replaceability for constraint satisfaction problems: Algorithms, Inferences, and Complexity Patterns (PDF, talk)
Walther, Christoph	(CAV) Formally Verified Montgomery Multiplication (PDF, talk)
Wang, Chao	(CAV) SCInfer: Refinement-based Verification of Software Countermeasures against Side-Channel Attacks (PDF, talk)
Wang, Guozhen	(CAV) Android Stack Machine (PDF, talk)
Wang, Jingyi	(FM) Towards `Verifying' a Water Treatment System (PDF, talk)
Wang, Quanlong	(LICS) Two complete axiomatisations of pure-state qubit quantum computing (PDF, talk)
Wang, Xinyu	(CAV) Learning Abstractions for Program Synthesis (PDF, talk)
Wang, Yi	(ICLP) A Probabilistic Extension of Action Language BC+ (PDF, talk) (ICLP-DC) Probabilistic Action Language pBC+ (PDF, talk)
Wang, Yu	(ADHS) Statistical Verification of PCTL Using Stratified Samples (PDF, talk) (ADHS) Observability of Linear Hybrid Systems with Unknown Inputs and Discrete Dynamics Modeled by Petri Nets (PDF, talk) (ADHS) Switch induced instabilities for stable power system DAE models (PDF, talk) (ADHS) Hierarchical Model Predictive Control for Building Energy Management of Hybrid Systems (PDF, talk) (ADHS) Network-Aware Design of State-Feedback Controllers for Linear Wireless Networked Control Systems (PDF, talk) (ADHS) Space-Time Budget Allocation for Marketing Over Social Networks (PDF, talk) (ADHS) Reachability Analysis for One Dimensional Linear Parabolic Equation (PDF, talk) (ADHS) Safety Control, a Quantitative Approach (PDF, talk) (ADHS) A switched system approach to optimize mixing of fluids (PDF, talk) (ADHS) Razumikhin-type Theorems on Practical Stability of Dynamic Equations on Time Scales (PDF, talk) (ADHS) Higher-Dimensional Timed Automata (PDF, talk) (ADHS) Verifying nonlinear analog and mixed-signal circuits with inputs (PDF, talk) (ADHS) Stability of switched systems on non-uniform time domains with non commuting matrices (PDF, talk) (ADHS) Concentration of Measure for Chance-Constrained Optimization (PDF, talk) (ADHS) Optimal Symbolic Controllers Determinization for BDD storage. (PDF, talk) (ADHS) Occupation Measure Methods for Modelling and Analysis of Biological Hybrid Systems (PDF, talk) (ADHS) On Approximate Predictability of Metric Systems (PDF, talk) (ADHS) Hybrid System Modeling of Multi-Agent Coverage Problems with Energy Depletion and Repletion (PDF, talk) (ADHS) CoasterX: A Case Study in Component-Driven Hybrid Systems Proof Automation (PDF, talk) (ADHS) Tracking Control via Variable-gain Integrator and Lookahead Simulation: Application to Leader-follower Multiagent Networks (PDF, talk) (ADHS) Bounding Errors Due to Switching Delays in Incrementally Stable Switched Systems (PDF, talk) (ADHS) Multi-Energy Scheduling Using a Hybrid Systems Approach (PDF, talk) (ADHS) Generating Dominant Strategies for Continuous Two-Player Zero-Sum Games (PDF, talk) (ADHS) Compositional Synthesis of Finite Abstractions for Continuous-Space Stochastic Control Systems: A Small-Gain Approach (PDF, talk) (ADHS) T-Barrier Certificates: A Continuous Analogy to K-Induction (PDF, talk) (ADHS) Approximate Abstractions of Markov Chains with Interval Decision Processes (PDF, talk) (ADHS) Control Synthesis for Stochastic Switched Systems Using the Tamed Euler Method (PDF, talk) (ADHS) Compositional Abstraction-based Synthesis for Cascade Discrete-Time Control Systems (PDF, talk) (ADHS) Nonuniform abstractions, refinement and controller synthesis with novel BDD encodings (PDF, talk) (ADHS) Benchmarks for Cyber-Physical Systems: A Modular Model Library for Building Automation Systems (PDF, talk) (ADHS) Temporal Logic Control of General Markov Decision Processes by Approximate Policy Refinement (PDF, talk) (ADHS) Compositional Analysis of Hybrid Systems Defined Over Finite Alphabets (PDF, talk) (ADHS) Language constrained stabilization of discrete- time switched linear systems: an LMI approach (PDF, talk) (ADHS) Interacting Particle System-Based Estimation of Reach Probability for a Generalized Stochastic Hybrid System (PDF, talk) (ADHS) A controlled sewer system should be treated as a sampled data system with events (PDF, talk) (ADHS) An Interval-Based Sliding Horizon Motion Planning Method (PDF, talk) (ADHS) Falsification of Temporal Logic Requirements Using Gradient Based Local Search in Space and Time (PDF, talk) (ADHS) Computing Controlled Invariant Sets for Hybrid Systems with Applications to Model-Predictive Control (PDF, talk) (ADHS) Temporal Logic Control of POMDPs Via Label-Based Stochastic Simulation Relations (PDF, talk) (ADHS) Mission Planning for Multiple Vehicles with Temporal Specifications using UxAS (PDF, talk) (ADHS) Input Design for Nonlinear Model Discrimination Via Affine Abstraction (PDF, talk) (ADHS) Learning and Verification of Feedback Control Systems Using Feedforward Neural Networks (PDF, talk) (ADHS) Control Synthesis and Classification for Unicycle Dynamics Using the Gradient and Value Sampling Particle Filters (PDF, talk) (ADHS) Sufficient Conditions for Temporal Logic Specifications in Hybrid Dynamical Systems (PDF, talk) (ADHS) Algorithm for Bernstein Polynomial Control Design (PDF, talk) (ADHS) On Generating A Variety of Unsafe Counterexamples for Linear Dynamical Systems (PDF, talk) (ADHS) On invariance and reachability on semialgebraic sets for linear dynamics (PDF, talk) (ADHS) Data-Driven Switched Affine Modeling for Model Predictive Control (PDF, talk) (ADHS) Symbolic Models for Incrementally Stable Switched Systems with Aperiodic Time Sampling (PDF, talk) (ADHS) Optimization-Based Design of Bounded-Error Estimators Robust to Missing Data (PDF, talk) (MoRe) Logically-Constrained Reinforcement Learning (PDF, talk) (VEMDP) Bayesian Verification of Chemical Reaction Networks (PDF, talk) (CAV) Counterexample Guided Inductive Synthesis Modulo Theories (PDF, talk)
Warinschi, Bogdan	(CSF) Machine-checked proofs for electronic voting: privacy and verifiability for Belenios (PDF, talk)
Warren, David Scott	(ICLP) Top-down and Bottom-up Evaluation Reconciled (PDF, talk) (LPOP) LPOP2018 XSB Position Paper (PDF, talk)
Watson, Nathaniel	(F-IDE) Integrating user design and formal models within PVSio-Web (PDF, talk)
Weaver, Sean	(SAT) XORSAT Set Membership Filters (PDF, talk)
Weber, Kai	(POS) CryptoMiniSat Parameter-Optimization for Solving Cryptographic Instances (PDF, talk)
Webster, Matt	(AVOCS) Formal Verification of Synchronisation, Gossip and Environmental Effects for Critical IoT Systems (PDF, talk)
Wehrle, Klaus	(CAV) Symbolic Liveness Analysis of Real-World Software (PDF, talk)
Weigl, Alexander	(UITP) Adding Text-Based Interaction to a Direct-Manipulation Interface for Program Verification -- Lessons Learned (PDF, talk)
Weinberger, Jonathan	(HoTT/UF) (Truncated) Simplicial Models of Type Theory (PDF, talk)
Weininger, Maximilian	(CAV) Value Iteration for Simple Stochastic Games: Stopping Criterion and Learning Algorithm (PDF, talk)
Weinstein, Scott	(LCC) Traversal-invariant definability and Logarithmic-space computation (PDF, talk)
Weissenbacher, Georg	(ADSL) Sloth: Separation Logic and Theories via Small Models (PDF, talk) (IJCAR) A Separation Logic with Data: Small Models and Automation (PDF, talk)
Wellen, Felix	(HoTT/UF) Cohesive Covering Theory (PDF, talk)
Wells, Joe	(LFMTP) What Does This Notation Mean Anyway? BNF-Style Notation as it is actually used (PDF, talk)
Weng, Xuetian	(TLA) Invariants in Distributed Algorithms (PDF)
Wenzel, Makarius	(F-IDE) Isabelle/jEdit as IDE for domain-specific formal languages and informal text documents (PDF, talk) (UITP) Isabelle/PIDE after 10 years of development (PDF, talk) (Isabelle) Further Scaling of Isabelle Technology (PDF, talk)
Wesselink, Wieger	(ARQNL) Evidence Extraction from Parameterised Boolean Equation Systems (PDF, talk)
West, Matthew	(ADHS) Statistical Verification of PCTL Using Stratified Samples (PDF, talk)
Westbrook, Edwin	(CAV) Continuous formal verification of Amazon s2n (PDF, talk)
Whalen, Michael	(CAV) The JKind Model Checker (PDF, talk)
Wheatley, Jack	(ADHS) Approximate Abstractions of Markov Chains with Interval Decision Processes (PDF, talk)
Wiedling, Cyrille	(FCS) Proving physical proximity using symbolic models (PDF, talk)
Wijesuriya, Viraj Brian	(VEMDP) Bayesian Verification of Chemical Reaction Networks (PDF, talk)
Wijs, Anton	(FM) To Compose, Or Not to Compose, That is the Question: An Analysis of Compositional State Space Generation (PDF, talk)
Wild, Paul	(LICS) A van Benthem Theorem for Fuzzy Modal Logic (PDF, talk)
Willemse, Tim	(ARQNL) Evidence Extraction from Parameterised Boolean Equation Systems (PDF, talk)
Wimmer, Ralf	(SAT) Dependency Quantified Boolean Formulas: An Overview of Solution Methods and Applications (PDF)
Wimmer, Simon	(ITP) Verified Memoization and Dynamic Programming (PDF, talk) (ITP) MDP + TA = PTA: Probabilistic Timed Automata, Formalized (Short Paper) (PDF, talk)
Winfree, Erik	(VEMDP) Equivalence of Chemical Reaction Networks in a CRN-to-DNA Compiler Framework (PDF, talk)
Winkler, Sarah	(FSCD) Completion for Logically Constrained Rewriting (PDF, talk) (IJCAR) MaedMax: A Maximal Ordered Completion Tool (PDF, talk) (IWC) Certified Ordered Completion (PDF, talk)
Winschel, Viktor	(SR) Compositional Game Theory (PDF, talk) (LICS) Compositional game theory (PDF, talk)
Winskel, Glynn	(LICS) The concurrent game semantics of Probabilistic PCF (PDF, talk)
Winter, Kirsten	(REFINE) Correctness of Concurrent Objects under Weak Memory Models (PDF, talk)
Wintersteiger, Christoph M.	(IJCAR) Exploring Approximations for Floating-Point Arithmetic using UppSAT (PDF, talk) (SMT) The next 10^4 UppSAT Approximations (PDF, talk)
Wirsen, Andreas	(ADHS) Switch induced instabilities for stable power system DAE models (PDF, talk)
Wisniewski, Rafal	(ADHS) Algorithm for Bernstein Polynomial Control Design (PDF, talk)
Wolf, Clifford	(CAV) BTOR2, BtorMC and Boolector 3.0 (PDF, talk)
Wolff, Burkhart	(Isabelle) Using Isabelle/UTP for the Verification of Sorting Algorithms: A Case Study (PDF, talk)
Woltran, Stefan	(SAT) Exploiting Treewidth for Projected Model Counting and its Limits (PDF, talk) (PRUV) A new logic for jointly representing hard and soft constraints (PDF, talk)
Woltzenlogel Paleo, Bruno	(UITP) Partial Regularization of First-Order Resolution Proofs (PDF, talk)
Woodcock, Jim	(VaVAS) RoboTool: Modelling and Verification with RoboChart (PDF, talk)
Wooldridge, Michael	(SR) Local Equilibria in Logic-Based Multi-Player Games (PDF, talk)
Worrell, James	(LICS) Polynomial Invariants for Affine Programs (PDF, talk)
Wu, Benjamin	(ICLP) Learning Commonsense Knowledge through Interactive Dialogue (PDF, talk)
Wu, Nicolas	(LICS) Syntax and Semantics for Operations with Scopes (PDF, talk)
Wu, Zhilin	(CAV) Android Stack Machine (PDF, talk)
X
Xia, Bican	(CAV) Monitoring CTMCs By Multi-Clock Timed Automata (PDF, talk)
Xiang, Weiming	(ADHS) Reachability Analysis for One Dimensional Linear Parabolic Equation (PDF, talk)
Xu, Zhiwu	(FM) Towards `Verifying' a Water Treatment System (PDF, talk) (CSF) A Permission-Dependent Type System for Secure Information Flow Analysis (PDF, talk)
Xue, Tao	(NLCS) Propositional Forms of Judgemental Interpretations (PDF, talk)
Y
Yahav, Eran	(CAV) From Programs to Interpretable Deep Models and Back (PDF, talk)
Yamada, Akihisa	(ITP) A Formalization of the LLL Basis Reduction Algorithm (PDF, talk) (WST) A Perron-Frobenius Theorem for Jordan Blocks for Complexity Proving (PDF, talk)
Yamagata, Yoriyuki	(FM) Falsification of Cyber-Physical Systems Using Deep Reinforcement Learning (PDF, talk)
Yan, Jun	(CAV) Android Stack Machine (PDF, talk)
Yan, Rongjie	(FM) Resource-aware Design for Reliable Autonomous Applications with Multiple Periods (PDF, talk)
Yang, Junfeng	(CAV) Partial Order Aware Concurrency Sampling (PDF, talk)
Yang, Junjie	(FM) Resource-aware Design for Reliable Autonomous Applications with Multiple Periods (PDF, talk)
Yang, Mohan	(ICLP) Declarative Algorithms in Datalog with Aggregates: user-friendly formal semantics conducive to performance and scalability (PDF, talk)
Yang, Weikun	(CAV) Lazy Self-Composition for Security Verification (PDF, talk)
Yang, Zhun	(ICLP) Translating LPOD and CR-Prolog2 into Standard Answer Set Programs (PDF, talk) (ICLP-DC) Translating P-log, LP^{MLN}, LPOD, and CR-Prolog2 into Standard Answer Set Programs (PDF, talk)
Yao, Shucai	(REFINE) Refining Santa: An Excercise in Efficient Synchronization (PDF, talk)
Yap, Roland	(ICLP) Shape Neutral Analysis of Graph-based Data-structures (PDF, talk)
Yeom, Samuel	(CSF) Privacy Risk in Machine Learning: Analyzing the Connection to Overfitting (PDF, talk)
Yokoyama, Keita	(LICS) A parameterized halting problem, the linear time hierarchy, and the MRDP theorem (PDF, talk)
Yonbawi, Saud	(VaVAS) Towards a Hierarchical-Control Architecture for Distributed Autonomous Systems (Extended Abstract - Paper) (PDF, talk)
Yong, Sze Zheng	(ADHS) Input Design for Nonlinear Model Discrimination Via Affine Abstraction (PDF, talk)
Yong, Sze Zheng	(ADHS) Optimization-Based Design of Bounded-Error Estimators Robust to Missing Data (PDF, talk)
Yoshida, Nobuko	(LICS) Causal Computational Complexity of Distributed Processes (PDF, talk)
Yuan, Xinhao	(CAV) Partial Order Aware Concurrency Sampling (PDF, talk)
Z
Zaffanella, Enea	(CAV) A Direct Encoding for NNC Polyhedra (PDF, talk)
Zahn, Philipp	(SR) Compositional Game Theory (PDF, talk) (LICS) Compositional game theory (PDF, talk)
Zaidi, Fatiha	(IJCAR) Cubicle-W: Parameterized Model Checking on Weak Memory (PDF, talk)
Zaikin, Oleg	(SAT) ALIAS: A Modular Tool for Finding Backdoors for SAT (PDF, talk)
Zalinescu, Eugen	(CSF) Inductive Invariants for Noninterference in Multi-agent Workflows (PDF, talk)
Zamani, Majid	(ADHS) Compositional Synthesis of Finite Abstractions for Continuous-Space Stochastic Control Systems: A Small-Gain Approach (PDF, talk)
Zamani, Majid	(ADHS) Compositional Abstraction-based Synthesis for Cascade Discrete-Time Control Systems (PDF, talk)
Zamdzhiev, Vladimir	(TERMGRAPH) A Framework for Rewriting Families of String Diagrams (PDF, talk) (LICS) Enriching a Linear/Non-linear Lambda Calculus: A Programming Language for String Diagrams (PDF, talk)
Zanasi, Fabio	(LICS) Rewriting with Frobenius (PDF, talk)
Zaniolo, Carlo	(ICLP) Declarative Algorithms in Datalog with Aggregates: user-friendly formal semantics conducive to performance and scalability (PDF, talk)
Zankl, Harald	(FSCD) Confluence Competition 2018 (PDF)
Zdancewic, Steve	(ITP) A Formal Equational Theory for Call-By-Push-Value (PDF, talk)
Zeilberger, Noam	(LICS) A theory of linear typings as flows on 3-valent graphs (PDF, talk)
Zeljić, Aleksandar	(IJCAR) Exploring Approximations for Floating-Point Arithmetic using UppSAT (PDF, talk) (SMT) The next 10^4 UppSAT Approximations (PDF, talk)
Zendel, Oliver	(POS) CryptoMiniSat Parameter-Optimization for Solving Cryptographic Instances (PDF, talk)
Zervakis, Georgios	(Overture) Multi-modelling of Cooperative Swarms (PDF, talk)
Zetzsche, Georg	(LICS) PTL-separability and closures for WQOs on words (PDF, talk)
Zhan, Bohua	(IJCAR) Verifying Asymptotic Time Complexity of Imperative Programs in Isabelle (PDF, talk)
Zhan, Naijun	(CAV) Monitoring CTMCs By Multi-Clock Timed Automata (PDF, talk)
Zhang, Fan	(FM) Resource-aware Design for Reliable Autonomous Applications with Multiple Periods (PDF, talk)
Zhang, Fuyuan	(FM) Compositional Reasoning for Shared-variable Concurrent Programs (PDF, talk)
Zhang, Hantao	(IJCAR) Investigating the Existence of Large Sets of Idempotent Quasigroups via Satisfiability Testing (PDF, talk)
Zhang, Hengruo	(CSF) Knowledge-based Security of Dynamic Secrets for Reactive Programs (PDF, talk)
Zhang, Jian	(PRUV) A New Probabilistic Algorithm for Approximate Model Counting (PDF, talk) (PRUV) VolCE: An Efficient Tool for Solving #SMT(LA) Problems (PDF, talk) (IJCAR) A New Probabilistic Algorithm for Approximate Model Counting (PDF, talk) (IJCAR) Investigating the Existence of Large Sets of Idempotent Quasigroups via Satisfiability Testing (PDF, talk)
Zhang, Jun	(CAV) SCInfer: Refinement-based Verification of Software Countermeasures against Side-Channel Attacks (PDF, talk)
Zhang, Min	(AVOCS) Using SMT engine to generate Symbolic Automata (PDF, talk)
Zhang, Qinglin	(ICLP) An ASP Methodology for Understanding Narratives about Stereotypical Activities (PDF, talk)
Zhang, Timothy	(ICLP) Constraint-Based Inference in Probabilistic Logic Programs (PDF, talk)
Zhang, Yi	(CSF) KEVM: A Complete Formal Semantics of the Ethereum Virtual Machine (PDF, talk)
Zhang, Yueling	(CAV) Syntax-Guided Termination Analysis (PDF, talk)
Zhang, Zhizheng	(ICLP) Introspecting Preferences In Answer Set Programming (PDF, talk)
Zhao, Jinxu	(ITP) Formalization of a Polymorphic Subtyping Algorithm (PDF, talk)
Zhao, Yizheng	(IJCAR) FAME: An Automated Tool for Semantic Forgetting in Expressive Description Logics (PDF, talk)
Zhao, Yongwang	(FM) Compositional Reasoning for Shared-variable Concurrent Programs (PDF, talk)
Zhao, Yuhang	(TERMGRAPH) Semantics-Preserving DPO-Based Term Graph Rewriting (PDF, talk)
Zheng, Yunhui	(CAV) StringFuzz: A Fuzzer for String Solvers (PDF, talk)
Zhou, Neng-Fa	(LPOP) A Picat-based XCSP Solver - from Parsing, Modeling, to SAT Encoding (PDF, talk) (RCRA) Encoding PB Constraints into SAT via Binary Adders and BDDs -- Revisited (PDF, talk)
Zhou, Qi	(HCVS) Solving Constrained Horn Clauses Using Dependence-Disjoint Expansions (PDF, talk)
Zhou, Weichao	(CAV) Safety-Aware Apprenticeship Learning (PDF, talk)
Zhu, Di	(FM) Resource-aware Design for Reliable Autonomous Applications with Multiple Periods (PDF, talk)
Zhu, Shufang	(WiL) First-Order vs. Second-Order Encodings for LTLf-to-Automata: An Extended Abstract (PDF, talk)
Zhu, Xiaoran	(CSF) KEVM: A Complete Formal Semantics of the Ethereum Virtual Machine (PDF, talk)
Zhumagambetov, Rustam	(UITP) Automated Theorem Proving in a Chat Environment (PDF, talk)
Ziegler, Christopher	(CAV) Rabinizer 4: From LTL to Your Favourite Deterministic Automaton (PDF, talk)
Zmigrod, Ran	(ITP) An Agda Formalization of Üresin & Dubois' Asynchronous Fixed-Point Theory (PDF, talk)
Zorzi, Margherita	(Linearity/TLLA) Quantum programming made easy (PDF, talk)
Zucca, Elena	(DCM) A syntactic model of mutation and aliasing (PDF, talk)
Zuleger, Florian	(LICS) Efficient Algorithms for Asymptotic Bounds on Termination Time in VASS (PDF, talk)
Zunic, Dragisa	(Linearity/TLLA) Formalization of Automated Trading Systems in a Concurrent Linear Framework (PDF, talk)
Zwanziger, Colin	(NLCS) Propositional Attitude Operators in Homotopy Type Theory (PDF, talk)
Zygalakis, Konstantinos	(VEMDP) Noise Control for Molecular Computing (PDF, talk)
Á
Ábrahám, Erika	(SCSC) Evaluation of Equational Constraints for CAD in SMT Solving (PDF, talk) (FM) Verifying Auto-Generated C Code from Simulink (PDF, talk) (FM) Formal Verification of Automotive Simulink Controller Models: Empirical Technical Challenges, Evaluation and Recommendations (PDF, talk) (IJCAR) Symbolic Computation Techniques in SMT Solving: Mathematical Beauty meets Efficient Heuristics (PDF)
Â
Ângelo, Pedro	(ITRS) Gradual Intersection Types (PDF, talk)
Č
Červený, Jan	(VEMDP) Executable Biochemical Space for Specification and Analysis of Biochemical Systems (PDF, talk)
Š
Šafránek, David	(VEMDP) Executable Biochemical Space for Specification and Analysis of Biochemical Systems (PDF, talk)
Šalagovič, Jakub	(VEMDP) Executable Biochemical Space for Specification and Analysis of Biochemical Systems (PDF, talk)