Trisha Nowland and Simon Boag | Towards a Logical Framework for Latent Variable Modelling | WiL | | Jul 08 16:30 |

Elaine Pimentel | A semantical view of sequent based systems | WiL | | Jul 08 11:30 |

Cláudia Nalon and Daniella Angelos | On the Combination of Resolution and SAT Procedures for Modal Theorem-Proving | WiL | | Jul 08 16:00 |

Liron Cohen and Ariel Kellison | On Expanding Standard Notions of Constructivity | WiL | | Jul 08 11:00 |

Giselle Reis | Towards a Playground for Logicians | WiL | | Jul 08 15:00 |

Çigdem Gencer | About the unification type of topological logics over Euclidean spaces | WiL | | Jul 08 12:00 |

Ornela Dardha and Simon J. Gay | A New Linear Logic for Deadlock-Free Session-Typed Processes (Talk Abstract) | WiL | | Jul 08 10:15 |

Hanna Lachnitt, Christoph Benzmüller and Maximilian Claus | Embedding Intuitionistic Modal Logics in Higher-Order Logic. An Easy Task? | WiL | | Jul 08 16:15 |

Liron Cohen and Reuben Rowe | Non-well-founded proof system for Transitive Closure Logic | WiL | | Jul 08 15:15 |

Shufang Zhu, Geguang Pu and Moshe Vardi | First-Order vs. Second-Order Encodings for LTLf-to-Automata: An Extended Abstract | WiL | | Jul 08 10:00 |

Sonia Marin, Marianela Morales and Lutz Straßburger | Decomposing labelled proof theory for intuitionistic modal logic | WiL | | Jul 08 11:45 |

Ilias Kotsireas | Hard Combinatorial Problems: A Challenge for Satisfiability | SCSC | | Jul 11 09:00 |

Alexander Cowen-Rivers and Matthew England | Towards Incremental Cylindrical Algebraic Decomposition in Maple | SCSC | | Jul 11 14:30 |

Rebecca Haehn, Gereon Kremer and Erika Ábrahám | Evaluation of Equational Constraints for CAD in SMT Solving | SCSC | | Jul 11 15:00 |

Jan Horacek and Martin Kreuzer | Refutation of Products of Linear Polynomials | SCSC | | Jul 11 16:00 |

Casey Mulligan, Russell Bradford, James H. Davenport, Matthew England and Zak Tonks | Non-linear Real Arithmetic Benchmarks derived from Automated Reasoning in Economics | SCSC | | Jul 11 14:00 |

Daniela Ritirc, Armin Biere and Manuel Kauers | A Practical Polynomial Calculus for Arithmetic Circuit Verification | SCSC | | Jul 11 16:30 |

Meesum Syed Mohammad and Prathamesh T. V. H. | Unknot Recognition Through Quantifier Elimination | SCSC | | Jul 11 17:00 |

John Abbott, Anna Maria Bigatti and Elisa Palezzato | New in CoCoA-5.2.4 and CoCoALib-0.99570 for SC-Square | SCSC | | Jul 11 11:25 |

Andreas Eggers, Matthias Stasch, Tino Teige, Tom Bienmüller and Udo Brockmeyer | Constraint Systems from Traffic Scenarios for the Validation of Autonomous Driving | SCSC | | Jul 11 10:05 |

Pascal Fontaine, Mizuhito Ogawa, Thomas Sturm, Van Khanh To and Xuan Tung Vu | Wrapping Computer Algebra is Surprisingly Successful for Non-Linear SMT | SCSC | | Jul 11 11:00 |

Stephen A. Forrest | SMT-like Queries in Maple | SCSC | | Jul 11 11:50 |

Tudor Jebelean | Techniques for Natural-style Proofs in Elementary Analysis | SCSC | | Jul 11 12:15 |

Jean-Christophe Filliâtre | Auto-active verification using Why3's IDE | F-IDE | | |

Leo Freitas | VDM at large: Modelling the EMVCo 2nd Generation Kernel | F-IDE | | |

Sylvain Dailler, Claude Marché and Yannick Moy | Lightweight Interactive Proving inside an Automatic Program Verifier | F-IDE | | Jul 14 10:00 |

Makarius Wenzel | Isabelle/jEdit as IDE for domain-specific formal languages and informal text documents | F-IDE | | Jul 14 16:00 |

Jan Bessai and Anna Vasileva | User Support for the Combinator Logic Synthesizer Framework | F-IDE | | Jul 14 11:00 |

Alexander Knüppel, Carsten Pardylla, Thomas Thüm and Ina Schaefer | Experience Report on Formally Verifying Parts of OpenJDK's API with KeY | F-IDE | | Jul 14 15:00 |

Paolo Arcaini, Riccardo Melioli and Elvinia Riccobene | AsmetaF: a flattener for the ASMETA framework | F-IDE | | Jul 14 11:30 |

Rui Couto, José Creissac Campos, Nuno Macedo and Alcino Cunha | Improving the Visualization of Alloy Instances | F-IDE | | Jul 14 12:00 |

Spencer Park and Emil Sekerinski | A Notebook Format for the Holistic Design of Embedded Systems | F-IDE | | Jul 14 16:30 |

Devesh Bhatt, Anitha Murugesan, Brendan Hall, Hao Ren and Yogananda Jeppu | The CLEAR Way To Transparent Formal Methods | F-IDE | | Jul 14 17:00 |

Nathaniel Watson, Steve Reeves and Paolo Masci | Integrating user design and formal models within PVSio-Web | F-IDE | | Jul 14 17:30 |

Yu Wang, Nima Roohi, Mahesh Viswanathan, Geir E. Dullerud and Matthew West | Statistical Verification of PCTL Using Stratified Samples | ADHS | | Jul 11 14:50 |

Carlos Renato Vazquez, David Gómez-Gutiérrez and Antonio Ramirez-Trevino | Observability of Linear Hybrid Systems with Unknown Inputs and Discrete Dynamics Modeled by Petri Nets | ADHS | | Jul 12 11:15 |

Tjorben Groß, Stephan Trenn and Andreas Wirsen | Switch induced instabilities for stable power system DAE models | ADHS | | Jul 11 17:00 |

Amanda Abreu, Romain Bourdais and Herve Gueguen | Hierarchical Model Predictive Control for Building Energy Management of Hybrid Systems | ADHS | | Jul 12 16:35 |

André Marcorin de Oliveira, Vineeth Satheeskumar Varma, Romain Postoyan, Irinel Constantin Morarescu, Jamal Daafouz and Oswaldo Luiz V. Costa | Network-Aware Design of State-Feedback Controllers for Linear Wireless Networked Control Systems | ADHS | | Jul 12 14:00 |

Irinel Constantin Morarescu, Vineeth Satheeskumar Varma, Lucian Busoniu and Samson Lasaulce | Space-Time Budget Allocation for Marketing Over Social Networks | ADHS | | Jul 12 14:25 |

Hoang-Dung Tran, Weiming Xiang, Stanley Bak and Taylor T Johnson | Reachability Analysis for One Dimensional Linear Parabolic Equation | ADHS | | Jul 12 10:50 |

Alina Eqtami and Antoine Girard | Safety Control, a Quantitative Approach | ADHS | | Jul 12 14:25 |

Victor Dolk, Menno Lauret, Duarte Antunes, Patrick Anderson and Maurice Heemels | A switched system approach to optimize mixing of fluids | ADHS | | Jul 11 11:15 |

Bacem Ben Nasser, Michael Defoort, Mohamed Djemai and Taous-Meriem Laleg-Kirati | Razumikhin-type Theorems on Practical Stability of Dynamic Equations on Time Scales | ADHS | | Jul 11 16:35 |

Ulrich Fahrenberg | Higher-Dimensional Timed Automata | ADHS | | Jul 11 17:00 |

Chuchu Fan, Yu Meng, Jürgen Maier, Ezio Bartocci, Sayan Mitra and Ulrich Schmid | Verifying nonlinear analog and mixed-signal circuits with inputs | ADHS | | Jul 12 17:00 |

Fatima Zohra Taousser, Michael Defoort, Mohamed Djemai and Seddik Djouadi | Stability of switched systems on non-uniform time domains with non commuting matrices | ADHS | | Jul 11 11:40 |

Sadegh Soudjani and Rupak Majumdar | Concentration of Measure for Chance-Constrained Optimization | ADHS | | Jul 13 11:40 |

Ivan Zapreev, Cees Verdier and Manuel Mazo Jr. | Optimal Symbolic Controllers Determinization for BDD storage. | ADHS | | Jul 11 10:50 |

Alexandre Rocca, Marcelo Forets, Victor Magron, Eric Fanchon and Thao Dang | Occupation Measure Methods for Modelling and Analysis of Biological Hybrid Systems | ADHS | | Jul 12 14:00 |

Gabriella Fiore, Elena De Santis, Giordano Pola and Maria Domenica Di Benedetto | On Approximate Predictability of Metric Systems | ADHS | | Jul 12 11:40 |

Xiangyu Meng, Arian Houshmand and Christos G. Cassandras | Hybrid System Modeling of Multi-Agent Coverage Problems with Energy Depletion and Repletion | ADHS | | Jul 12 15:15 |

Brandon Bohrer, Adriel Luo, Xue An Chuang and Andre Platzer | CoasterX: A Case Study in Component-Driven Hybrid Systems Proof Automation | ADHS | | Jul 11 14:25 |

Yorai Wardi, Carla Seatzu and Magnus Egerstedt | Tracking Control via Variable-gain Integrator and Lookahead Simulation: Application to Leader-follower Multiagent Networks | ADHS | | Jul 12 14:50 |

Kengo Kido, Sean Sedwards and Ichiro Hasuo | Bounding Errors Due to Switching Delays in Incrementally Stable Switched Systems | ADHS | | Jul 12 16:10 |

Ashok Krishnan, Mohasha Isuru Sampath, Yi Shyh Eddy Foo, Bhagyesh Patil and H. B. Gooi | Multi-Energy Scheduling Using a Hybrid Systems Approach | ADHS | | Jul 12 16:10 |

Marcell Vazquez-Chanlatte, Shromona Ghosh, Vasumathi Raman, Alberto Sangiovanni-Vincentelli and Sanjit Seshia | Generating Dominant Strategies for Continuous Two-Player Zero-Sum Games | ADHS | | Jul 11 11:15 |

Abolfazl Lavaei, Sadegh Soudjani and Majid Zamani | Compositional Synthesis of Finite Abstractions for Continuous-Space Stochastic Control Systems: A Small-Gain Approach | ADHS | | Jul 13 10:50 |

Stanley Bak | T-Barrier Certificates: A Continuous Analogy to K-Induction | ADHS | | Jul 12 11:40 |

Yuriy Zacchia Lun, Jack Wheatley, Alessandro D'Innocenzo and Alessandro Abate | Approximate Abstractions of Markov Chains with Interval Decision Processes | ADHS | | Jul 11 15:15 |

Adrien Le Coent, Laurent Fribourg and Jonathan Vacher | Control Synthesis for Stochastic Switched Systems Using the Tamed Euler Method | ADHS | | Jul 12 17:00 |

Adnane Saoud, Pushpak Jagtap, Majid Zamani and Antoine Girard | Compositional Abstraction-based Synthesis for Cascade Discrete-Time Control Systems | ADHS | | Jul 11 11:40 |

Oscar Bulancea Lindvall, Petter Nilsson and Necmiye Ozay | Nonuniform abstractions, refinement and controller synthesis with novel BDD encodings | ADHS | | Jul 11 12:05 |

Nathalie Margaret Cauchi and Alessandro Abate | Benchmarks for Cyber-Physical Systems: A Modular Model Library for Building Automation Systems | ADHS | | Jul 11 14:00 |

Sofie Haesaert, Sadegh Soudjani and Alessandro Abate | Temporal Logic Control of General Markov Decision Processes by Approximate Policy Refinement | ADHS | | Jul 11 14:00 |

Murat Cubuktepe, Mohamadreza Ahmadi, Ufuk Topcu and Brandon Hencey | Compositional Analysis of Hybrid Systems Defined Over Finite Alphabets | ADHS | | Jul 11 16:10 |

Marc Jungers, Antoine Girard and Mirko Fiacchini | Language constrained stabilization of discrete- time switched linear systems: an LMI approach | ADHS | | Jul 11 10:50 |

Henk A.P. Blom, Hao Ma and Bert G.J. Bakker | Interacting Particle System-Based Estimation of Reach Probability for a Generalized Stochastic Hybrid System | ADHS | | Jul 11 14:25 |

Ronald Robert Paul van Nooijen and Alla G. Kolechkina | A controlled sewer system should be treated as a sampled data system with events | ADHS | | Jul 11 14:50 |

Julien Alexandre Dit Sandretto, Elliot Brendel and Alexandre Chapoutot | An Interval-Based Sliding Horizon Motion Planning Method | ADHS | | Jul 13 14:50 |

Shakiba Yaghoubi and Georgios Fainekos | Falsification of Temporal Logic Requirements Using Gradient Based Local Search in Space and Time | ADHS | | Jul 11 16:35 |

Benoît Legat, Paulo Tabuada and Raphaël M. Jungers | Computing Controlled Invariant Sets for Hybrid Systems with Applications to Model-Predictive Control | ADHS | | Jul 12 14:50 |

Sofie Haesaert, Petter Nilsson, Cristian-Ioan Vasile, Thakker Rohan, Ali-Akbar Agha-Mohammadi, Aaron Ames and Richard M. Murray | Temporal Logic Control of POMDPs Via Label-Based Stochastic Simulation Relations | ADHS | | Jul 13 11:15 |

Luan Nguyen, Bardh Hoxha, Taylor T Johnson and Georgios Fainekos | Mission Planning for Multiple Vehicles with Temporal Specifications using UxAS | ADHS | | Jul 11 15:15 |

Kanishka Raj Singh, Yuhao Ding, Necmiye Ozay and Sze Zheng Yong | Input Design for Nonlinear Model Discrimination Via Affine Abstraction | ADHS | | Jul 12 12:05 |

Souradeep Dutta, Susmit Jha, Sriram Sankaranarayanan and Ashish Tiwari | Learning and Verification of Feedback Control Systems Using Feedforward Neural Networks | ADHS | | Jul 12 12:05 |

Ariadna Estrada and Ian M. Mitchell | Control Synthesis and Classification for Unicycle Dynamics Using the Gradient and Value Sampling Particle Filters | ADHS | | Jul 13 14:25 |

Hyejin Han and Ricardo Sanfelice | Sufficient Conditions for Temporal Logic Specifications in Hybrid Dynamical Systems | ADHS | | Jul 11 16:10 |

Tareq Hamadneh and Rafal Wisniewski | Algorithm for Bernstein Polynomial Control Design | ADHS | | Jul 13 14:00 |

Manish Goyal and Parasara Sridhar Duggirala | On Generating A Variety of Unsafe Counterexamples for Linear Dynamical Systems | ADHS | | Jul 12 11:15 |

Nikolaos Athanasopoulos and Raphaël M. Jungers | On invariance and reachability on semialgebraic sets for linear dynamics | ADHS | | Jul 11 12:05 |

Francesco Smarra, Achin Jain, Rahul Mangharam and Alessandro D'Innocenzo | Data-Driven Switched Affine Modeling for Model Predictive Control | ADHS | | Jul 12 15:15 |

Zohra Kader, Antoine Girard and Adnane Saoud | Symbolic Models for Incrementally Stable Switched Systems with Aperiodic Time Sampling | ADHS | | Jul 12 16:35 |

Kwesi Rutledge, Sze Zheng Yong and Necmiye Ozay | Optimization-Based Design of Bounded-Error Estimators Robust to Missing Data | ADHS | | Jul 12 10:50 |

Jean-Christophe Filliatre | Deductive Program Verification | ITP | | |

Daniel Grayson | Voevodsky's work on formalization of proofs and the foundations of mathematics | ITP | | |

John Harrison | Mike Gordon: Tribute to a pioneer in theorem proving and formal verification | ITP | | |

Reto Achermann, Lukas Humbel, David Cock and Timothy Roscoe | Physical addressing on real hardware in Isabelle/HOL | ITP | | Jul 11 09:30 |

Abhishek Anand, Simon Boulier, Cyril Cohen, Matthieu Sozeau and Nicolas Tabareau | Towards Certified Meta-Programming with Typed Template-Coq | ITP | | Jul 10 16:30 |

Andréia B. Avelar, Thaynara A. de Lima and André Luiz Galdino | Formalizing Ring Theory in PVS (short paper) | ITP | | Jul 11 17:00 |

Samuel Balco, Sabine Frittella, Giuseppe Greco, Alexander Kurz and Alessandra Palmigiano | Software tool support for modular reasoning in modal logics of actions | ITP | | Jul 09 14:30 |

Callum Bannister, Peter Höfner and Gerwin Klein | Backwards and Forwards with Separation Logic | ITP | | Jul 10 14:00 |

Véronique Benzaken, Evelyne Contejean, Chantal Keller and Eunice Martins | A Coq formalisation of SQL’s execution engines | ITP | | Jul 10 15:00 |

Sylvain Boulmé and Alexandre Maréchal | A Coq Tactic for Equality Learning in Linear Arithmetic | ITP | | Jul 10 12:00 |

Venanzio Capretta and Colm Baston | The Coinductive Formulation of Common Knowledge | ITP | | Jul 09 15:00 |

Raphaël Cauderlier | Tactics and certificates in Meta Dedukti | ITP | | Jul 11 12:00 |

Jose Divasón, Sebastiaan Joosten, René Thiemann and Akihisa Yamada | A Formalization of the LLL Basis Reduction Algorithm | ITP | | Jul 10 11:00 |

Christian Doczkal, Guillaume Combette and Damien Pous | A Formal Proof of the Minor-Exclusion Property for Treewidth-Two Graphs | ITP | | Jul 12 09:00 |

Manuel Eberl, Max W. Haslbeck and Tobias Nipkow | Verified Analysis of Random Binary Tree Structures | ITP | | Jul 12 16:30 |

William Farmer, Jacques Carette and Patrick Laskowski | HOL Light QE | ITP | | Jul 11 11:30 |

Denis Firsov, Richard Blair and Aaron Stump | Efficient Mendler-Style Lambda-Encodings in Cedille | ITP | | Jul 09 12:00 |

Yannick Forster, Edith Heiter and Gert Smolka | Verification of PCP-Related Computational Reductions in Coq | ITP | | Jul 12 10:00 |

Zarathustra Goertzel, Jan Jakubuv, Stephan Schulz and Josef Urban | ProofWatch: Watchlist Guidance for Large Theories in E | ITP | | Jul 12 15:00 |

Jason Gross, Andres Erbsen and Adam Chlipala | Reification by Parametricity | ITP | | Jul 10 14:30 |

Simon Jantsch and Michael Norrish | Verifying the LTL to Büchi Automata Translation via Very Weak Alternating Automata | ITP | | Jul 12 09:30 |

Wolfram Kahl | CalcCheck: A Proof Checker for Teaching the “Logical Approach to Discrete Math” | ITP | | Jul 10 10:00 |

Alexander Knüppel, Thomas Thüm, Carsten Pardylla and Ina Schaefer | Understanding Parameters of Deductive Verification: An Empirical Investigation of KeY | ITP | | Jul 09 16:00 |

Ramana Kumar, Eric Mullen, Zachary Tatlock and Magnus O. Myreen | Software Verification with ITPs Should Use Binary Code Extraction to Reduce the TCB (short paper) | ITP | | Jul 11 17:20 |

Dominique Larchey-Wendling | Proof Pearl: Constructive Extraction of Cycle Finding Algorithms | ITP | | Jul 12 12:00 |

Andreas Lochbihler | Fast machine words in Isabelle/HOL | ITP | | Jul 12 11:30 |

Andreas Lochbihler and Joshua Schneider | Relational parametricity and quotient preservation for modular (co)datatypes | ITP | | Jul 11 11:00 |

Alexandra Mendes and Joao F. Ferreira | Towards Verified Handwritten Calculational Proofs (short paper) | ITP | | Jul 11 16:40 |

Florian Meßner, Julian Parsert, Jonas Schöpf and Christian Sternagel | A Formally Verified Solver for Homogeneous Linear Diophantine Equations | ITP | | Jul 10 11:30 |

Étienne Miquey | Formalizing Implicative Algebras in Coq | ITP | | Jul 09 14:00 |

Mariano Moscato, Carlos Lopez Pombo, Cesar Munoz and Marco Antonio Feliu Gabaldon | Boosting the Reuse of Formal Specifications | ITP | | Jul 09 16:30 |

Julian Parsert and Cezary Kaliszyk | Towards Formal Foundations for Game Theory (short paper) | ITP | | Jul 11 16:00 |

João Paulo Pizani Flor and Wouter Swierstra | Verified Timing Transformations in Synchronous Circuits with LambdaPi-Ware | ITP | | Jul 11 10:00 |

Christine Rizkallah, Dmitri Garbuzov and Steve Zdancewic | A Formal Equational Theory for Call-By-Push-Value | ITP | | Jul 09 17:30 |

Hira Syeda and Gerwin Klein | Program Verification in the Presence of Cached Address Translation | ITP | | Jul 11 09:00 |

Joseph Tassarotti and Robert Harper | Verified Tail Bounds for Randomized Programs | ITP | | Jul 12 16:00 |

Simon Wimmer, Shuwei Hu and Tobias Nipkow | Verified Memoization and Dynamic Programming | ITP | | Jul 12 11:00 |

Simon Wimmer and Johannes Hölzl | MDP + TA = PTA: Probabilistic Timed Automata, Formalized (Short Paper) | ITP | | Jul 11 16:20 |

Jinxu Zhao, Bruno C. D. S. Oliveira and Tom Schrijvers | Formalization of a Polymorphic Subtyping Algorithm | ITP | | Jul 09 17:00 |

Ran Zmigrod, Matthew L. Daggitt and Timothy G. Griffin | An Agda Formalization of Üresin & Dubois' Asynchronous Fixed-Point Theory | ITP | | Jul 10 16:00 |

Stéphanie Delaune | Analysing privacy-type properties in cryptographic protocols | FSCD | | |

Grigore Rosu | Formal Design, Implementation and Verification of Blockchain Languages | FSCD | | |

Peter Selinger | Challenges in quantum programming languages | FSCD | | |

Valeria Vignudelli | Proof techniques for program equivalence in probabilistic higher-order languages | FSCD | | |

Sandra Alves and Sabine Broda | A Unifying Framework for Type Inhabitation | FSCD | | Jul 10 11:00 |

Nirina Andrianarivelo and Pierre Rety | Confluence of Prefix-Constrained Rewrite Systems | FSCD | | Jul 12 17:00 |

Mauricio Ayala-Rincon, Maribel Fernandez and Daniele Nantes-Sobrinho | Fixed-Point Constraints for Nominal Equational Unification | FSCD | | Jul 12 11:00 |

Patrick Bahr | Strict Ideal Completions of the Lambda Calculus | FSCD | | Jul 11 10:00 |

Alexander Baumgartner, Temur Kutsia, Jordi Levy and Mateu Villaret | Term-Graph Anti-Unification | FSCD | | Jul 12 10:00 |

Willem Heijltjes and Gianluigi Bellin | Proof nets for bi-intuitionistic linear logic | FSCD | | Jul 09 11:00 |

Maciej Bendkowski and Pierre Lescanne | Counting Environments and Closures | FSCD | | Jul 10 15:40 |

David Cerna and Temur Kutsia | Higher-Order Equational Pattern Anti-Unification | FSCD | | Jul 12 11:30 |

Łukasz Czajka | Term rewriting characterisation of LOGSPACE for finite and infinite data | FSCD | | Jul 10 16:10 |

Joerg Endrullis, Jan Willem Klop and Roy Overbeek | Decreasing diagrams with two labels are complete for confluence of countable systems | FSCD | | Jul 12 16:30 |

Simon Forest and Samuel Mimram | Coherence of Gray categories via rewriting | FSCD | | Jul 12 17:30 |

Thomas Genet | Completeness of Tree Automata Completion | FSCD | | Jul 11 12:00 |

Amar Hadzihasanovic, Giovanni de Felice and Kang Feng Ng | A diagrammatic axiomatisation of fermionic quantum circuits | FSCD | | Jul 09 15:00 |

Mirai Ikebuchi and Keisuke Nakano | On repetitive right application of B-terms | FSCD | | Jul 11 09:00 |

Rohan Jacob-Rao, Brigitte Pientka and David Thibodeau | Index-Stratified Types | FSCD | | Jul 10 12:00 |

Ambrus Kaposi and András Kovács | A Syntax for Higher Inductive-Inductive Types | FSCD | | Jul 10 15:00 |

Jean-Simon Lemay | Lifting Coalgebra Modalities and IMELL Model Structure to Eilenberg-Moore Categories | FSCD | | Jul 09 12:00 |

Daniel R. Licata, Ian Orton, Andrew M. Pitts and Bas Spitters | Internal Universes in Models of Homotopy Type Theory | FSCD | | Jul 10 10:00 |

Bassel Mannaa and Rasmus Møgelberg | The clocks they are adjunctions. Denotational semantics for Clocked Type Theory | FSCD | | Jul 10 09:30 |

Max New and Daniel Licata | Call-by-name Gradual Type Theory | FSCD | | Jul 10 09:00 |

Lê Thành Dũng Nguyễn | Unique perfect matchings and proof nets | FSCD | | Jul 09 11:30 |

Naoki Nishida and Yuya Maeda | Narrowing Trees for Syntactically Deterministic Conditional Term Rewriting Systems | FSCD | | Jul 11 11:00 |

Paweł Parys | Homogeneity without Loss of Generality | FSCD | | Jul 11 09:30 |

Manfred Schmidt-Schauss and David Sabel | Nominal Unification with Atom and Context Variables | FSCD | | Jul 12 12:00 |

Amin Timany and Matthieu Sozeau | Cumulative Inductive Types in Coq | FSCD | | Jul 10 11:30 |

Sarah Winkler and Aart Middeldorp | Completion for Logically Constrained Rewriting | FSCD | | Jul 11 11:30 |

Christina Kohl and Aart Middeldorp | ProTeM: A Proof Term Manipulator | FSCD | | Jul 12 15:00 |

Takahito Aoto, Makoto Hamana, Nao Hirokawa, Aart Middeldorp, Julian Nagele, Naoki Nishida, Kiraku Shintani and Harald Zankl | Confluence Competition 2018 | FSCD | | |

Willem Heijltjes | An introduction to deep inference | TYDI | | Jul 07 09:00 |

Alessio Guglielmi | Two Unifying Structural Principles | TYDI | | Jul 07 14:00 |

Dominic Hughes | Some incoherent musings on deep inference and combinatorial proofs | TYDI | | Jul 07 16:00 |

Anupam Das | Proof complexity of deep inference: a survey | TYDI | | Jul 07 17:00 |

Ross Horne | Truely Concurrent Processes in the Calculus of Structures | TYDI | | Jul 07 11:00 |

Bjoern Lellmann, Elaine Pimentel and Revantha Ramanayake | Sequentialising nested systems | TYDI | | Jul 07 11:30 |

Sonia Marin | Nested sequents for modal logics and beyond | TYDI | | Jul 07 12:00 |

Joseph Paulus and Willem Heijltjes | Deep-Inference Intersection Types | TYDI | | Jul 07 10:00 |

Benjamin Ralph | Deep Inference, Herbrand's Theorem and Expansion Proofs | TYDI | | Jul 07 15:00 |

Peter W. V. Tran-Jørgensen, René Søndergaard Nilsson and Kenneth Lausdahl | Enhancing Testing of VDM-SL models | Overture | | Jul 14 10:10 |

Casper Thule, Kenneth Lausdahl and Peter Gorm Larsen | Overture FMU: Export VDM-RT Models as Tool-Wrapper FMUs | Overture | | Jul 14 11:00 |

Tomohiro Oda, Keijiro Araki and Peter Gorm Larsen | ViennaVM: a Virtual Machine for VDM-SL development | Overture | | Jul 14 11:20 |

René Søndergaard Nilsson, Kenneth Lausdahl, Hugo Daniel Macedo and Peter Gorm Larsen | Transforming an industrial case study from VDM++ to VDM-SL | Overture | | Jul 14 14:50 |

Leo Freitas | VDM at large: analysing the EMV Next Generation Kernel | Overture | | Jul 14 14:00 |

Martin Mansfield, Charles Morisset, Carl Gamble, John Mace, Ken Pierce and John Fitzgerald | Design Space Exploration for Secure Building Control | Overture | | Jul 14 12:00 |

Simon Fraser | Integrating VDM-SL into the continuous delivery pipelines of cloud-based software | Overture | | Jul 14 15:10 |

Georgios Zervakis, Ken Pierce and Carl Gamble | Multi-modelling of Cooperative Swarms | Overture | | Jul 14 11:40 |

Thomas Brihaye, Véronique Bruyère, Aline Goeminne and Jean-François Raskin | Constraint Problem for Weak Subgame Perfect Equilibria with omega-regular Boolean Objectives | MoRe | | Jul 13 11:00 |

Thomas Brihaye, Mickael Randour and Cédric Rivière | Stochastic o-minimal hybrid systems | MoRe | | Jul 13 15:00 |

Véronique Bruyère, Quentin Hautem and Jean-Francois Raskin | Parameterized complexity of games with monotonically ordered omega-regular objectives | MoRe | | Jul 13 11:30 |

Gilles Geeraerts, Shibashis Guha and Jean-Francois Raskin | Safe and Optimal Scheduling of Hard and Soft Tasks | MoRe | | Jul 13 16:30 |

Arnd Hartmanns, Sebastian Junges, Joost-Pieter Katoen and Tim Quatmann | Multiple Objectives and Cost Bounds in MDP | MoRe | | Jul 13 10:00 |

Mohammadhosein Hasanbeig, Alessandro Abate and Daniel Kroening | Logically-Constrained Reinforcement Learning | MoRe | | Jul 13 17:00 |

Dimitri Scheftelowitsch | Multi-Scenario Uncertainty in Markov Decision Processes | MoRe | | Jul 13 16:00 |

Tao Xue, Zhaohui Luo and Stergios Chatzikyriakidis | Propositional Forms of Judgemental Interpretations | NLCS | | Jul 07 11:30 |

Valeria de Paiva, Alexandre Rademaker, Livy Real, Fabricio Chalub and Gerard de Melo | OpenWordNet-PT: Taking Stock | NLCS | | Jul 07 17:30 |

Aikaterini-Lida Kalouli, Richard Crouch, Valeria de Paiva and Livy Real | Graph Knowledge Representations for SICK | NLCS | | Jul 07 15:00 |

Colin Zwanziger | Propositional Attitude Operators in Homotopy Type Theory | NLCS | | Jul 07 11:00 |

Inari Listenmaa and Koen Claessen | Automatic test suite generation for PMCFG grammars | NLCS | | Jul 07 17:00 |

Nino Amiridze and Temur Kutsia | Anti-Unification and Natural Language Processing | NLCS | | Jul 07 10:00 |

Hai Hu, Thomas Icard and Larry Moss | Automated Reasoning from Polarized Parse Trees | NLCS | | Jul 07 16:00 |

Ribeka Tanaka, Koji Mineshima and Daisuke Bekki | Paychecks, Presupposition, and Dependent Types | NLCS | | Jul 07 12:00 |

Davide Catta, Richard Moot and Christian Retoré | Do different syntactic trees yield different logical readings? Some remarks on head variables in typed lambda calculus. | NLCS | | Jul 07 16:30 |

Hiroshi Unno | Horn Clauses and Beyond for Relational and Temporal Program Verification | HCVS | | |

Pierre Ganty | Tree dimension in verification of constrained Horn clauses | HCVS | | |

Qi Zhou, David Heath and William Harris | Solving Constrained Horn Clauses Using Dependence-Disjoint Expansions | HCVS | | Jul 13 11:00 |

Giorgio Delzanno, Sylvain Conchon and Angelo Ferrando | Declarative Parameterized Verification of Topology-sensitive Distributed Protocols | HCVS | | Jul 13 15:00 |

Ekaterina Komendantskaya and Yue Li | Towards Coinductive Theory Exploration in Horn Clause Logic: Extended Abstract | HCVS | | Jul 13 12:00 |

Emanuele De Angelis, Fabio Fioravanti, Adrián Palacios, Alberto Pettorossi and Maurizio Proietti | Metaprogramming and symbolic execution for detecting runtime errors in Erlang programs | HCVS | | Jul 13 10:00 |

António Ravara | A simple functional presentation and an inductive correctness proof of the Horn algorithm | HCVS | | Jul 13 11:30 |

Andreas Nuyts and Dominique Devriese | Internalizing Presheaf Semantics: Charting the Design Space | HoTT/UF | | Jul 07 11:00 |

Andreas Nuyts | Robust Notions of Contextual Fibrancy | HoTT/UF | | Jul 08 11:30 |

Lars Birkedal, Ranald Clouston, Bassel Mannaa, Rasmus Møgelberg, Andrew Pitts and Bas Spitters | Dependent Right Adjoint Types | HoTT/UF | | Jul 07 12:00 |

Clive Newstead | Algebraic models of dependent type theory | HoTT/UF | | Jul 07 16:30 |

Taichi Uemura | Cubical Assemblies and the Independence of the Propositional Resizing Axiom | HoTT/UF | | Jul 07 11:30 |

Iosif Petrakis | A Yoneda lemma-formulation of the univalence axiom | HoTT/UF | | Jul 08 11:00 |

Edward Morehouse | Ordered Cubes | HoTT/UF | | Jul 08 15:00 |

Eric Faber | Towards a geometric model theory of type theory | HoTT/UF | | |

Jonathan Weinberger and Ulrik Buchholtz | (Truncated) Simplicial Models of Type Theory | HoTT/UF | | Jul 08 16:00 |

Thorsten Altenkirch | Towards the syntax and semantics of higher dimensional type theory | HoTT/UF | | Jul 08 16:30 |

Genki Sato | Geometric realization of truncated semi-simplicial sets meta-constructed within HoTT | HoTT/UF | | Jul 07 15:00 |

Joseph Helfer | First-order homotopical logic and Grothendieck fibrations | HoTT/UF | | Jul 07 17:00 |

Felix Wellen | Cohesive Covering Theory | HoTT/UF | | Jul 08 12:00 |

Kuen-Bang Hou Favonia, Carlo Angiuli, Evan Cavallo, Robert Harper and Jonathan Sterling | Cubical Computational Type Theory | HoTT/UF | | Jul 08 14:00 |

Hugo Herbelin | The definitional symmetric cubical structure of types in type theory with equality defined by abstraction over an interval | HoTT/UF | | Jul 08 14:30 |

Mauricio Ayala-Rincón and Philippe Balbiani | Preface of the 32nd International Workshop on Unification UNIF 2018 | UNIF | | |

Silvio Ghilardi | Handling Substitutions via Duality | UNIF | | |

Adrià Gascón | Compressed Term Unification: Results, Applications, Open problems, and Hopes | UNIF | | |

Ajay Kumar Eeralla and Christopher Lynch | Bounded ACh Unification | UNIF | | Jul 07 11:30 |

David Cerna and Temur Kutsia | Towards Generalization Methods for Purely Idempotent Equational Theories | UNIF | | Jul 07 16:30 |

Temur Kutsia and Cleo Pau | Proximity-Based Generalization | UNIF | | Jul 07 16:00 |

Çiğdem Gencer | About the Unification Type of Topological Logics over Euclidean Spaces | UNIF | | Jul 07 12:00 |

Yunus David Kerem Kutz and Manfred Schmidt-Schauss | Rewriting with Generalized Nominal Unification | UNIF | | Jul 07 17:00 |

Franz Baader, Pavlos Marantidis and Antoine Mottet | ACUI Unification Modulo Ground Theories | UNIF | | Jul 07 15:00 |

Serdar Erbatur, Andrew M. Marshall and Christophe Ringeissen | Knowledge Problems in Equational Extensions of Subterm Convergent Theories | UNIF | | Jul 07 11:00 |

Joerg Siekmann and Peter Szabo | Unification Based on Generalized Embedding | UNIF | | Jul 07 10:00 |

Kasper Fabæch Brandt, Anders Schlichtkrull and Jørgen Villadsen | Formalization of First-Order Syntactic Unification | UNIF | | Jul 07 17:30 |

Weixi Ma, Jeremy Siek, David Christiansen and Daniel Friedman | Efficiency of a Good but not Linear Nominal Unification Algorithm | UNIF | | Jul 07 17:50 |

Sara-Jane Dunn | Uncovering the Biological Programs that Govern Development | VEMDP | | |

Andrew J. Turberfield | Controlling Assembly and Function of DNA Nanostructures and Molecular Machinery | VEMDP | | |

Luca Laurenti, Attila Csikász-Nagy, Marta Kwiatkowska and Luca Cardelli | Molecular Filters for Noise Reduction | VEMDP | | Jul 19 12:00 |

Hillel Kugler, Till Korten, Stefan Diez and Dan Nicolau Jr. | Formal Verification of Network-Based Biocomputation Circuits | VEMDP | | Jul 19 17:20 |

Matej Troják, Jakub Šalagovič, David Šafránek, Jan Červený, Luboš Brim and Matej Hajnal | Executable Biochemical Space for Specification and Analysis of Biochemical Systems | VEMDP | | Jul 19 17:00 |

Carlo Spaccasassi, Matthew Lakin and Andrew Phillips | Rule-based Design of Computational DNA Devices | VEMDP | | Jul 19 11:20 |

Tomislav Plesa, Konstantinos Zygalakis, David Anderson and Radek Erban | Noise Control for Molecular Computing | VEMDP | | Jul 19 11:40 |

Ken Chanseau Saint-Germain and Jérôme Feret | Conservative Approximations of Polymers | VEMDP | | Jul 19 16:40 |

Robert F. Johnson | Using Transitivity and Modularity in Chemical Reaction Network Bisimulation | VEMDP | | Jul 19 16:20 |

Stefan Badelt and Erik Winfree | Equivalence of Chemical Reaction Networks in a CRN-to-DNA Compiler Framework | VEMDP | | Jul 19 16:00 |

Keenan Breik, Chris Thachuk, Marijn Heule and David Soloveichik | Computing Properties of Stable Configurations of Thermodynamic Binding Networks | VEMDP | | Jul 19 10:00 |

Jakob Lykke Andersen, Christoph Flamm, Daniel Merkle and Peter F. Stadler | Rule-Based Gillespie Simulation of Chemical Systems | VEMDP | | Jul 19 11:00 |

Gareth Molyneux, Viraj Brian Wijesuriya and Alessandro Abate | Bayesian Verification of Chemical Reaction Networks | VEMDP | | Jul 19 15:00 |

Alexandru Amarioarei, Frankie Spencer, Corina Itcus, Iris Tusa, Ana Maria Dobre, Gefry Barad, Romica Trandafir, Mihaela Paun, Andrei Paun and Eugen Czeizler | Computational Approaches for the Programmed Assembly of Nanocellulose Meshes | VEMDP | | Jul 19 15:10 |

David Scott Warren | Top-down and Bottom-up Evaluation Reconciled | ICLP | | Jul 15 11:00 |

Patrick Kahl and Anthony Leclerc | Epistemic Logic Programs with World View Constraints | ICLP | | Jul 15 16:15 |

Rolf Schwitter | Specifying and Verbalising Answer Set Programs in Controlled Natural Language | ICLP | | Jul 16 09:30 |

Frantisek Farka, Ekaterina Komendantskaya and Kevin Hammond | Proof-relevant Horn Clauses for Dependent Type Inference and Term Synthesis | ICLP | | Jul 14 14:00 |

Pedro Cabalar, Roland Kaminski, Torsten Schaub and Anna Schuhmann | Temporal Answer Set Programming on Finite Traces | ICLP | | Jul 15 10:00 |

Martin Gebser, Van Nguyen, Philipp Obermeier, Thomas Otto, Orkunt Sabuncu, Torsten Schaub and Tran Cao Son | Experimenting with robotic intra-logistics domains | ICLP | | Jul 17 11:30 |

Farhad Shakerin and Gopal Gupta | Cumulative Scoring-based Induction of Default Theories | ICLP | | Jul 15 16:00 |

Joohyung Lee and Zhun Yang | Translating LPOD and CR-Prolog2 into Standard Answer Set Programs | ICLP | | Jul 14 17:30 |

Benjamin Wu, Alessandra Russo, Mark Law and Katsumi Inoue | Learning Commonsense Knowledge through Interactive Dialogue | ICLP | | Jul 17 17:00 |

Arindam Mitra and Chitta Baral | Incremental and Iterative Learning of Answer Set Programs from Mutually Distinct Examples | ICLP | | Jul 15 14:30 |

Bram Aerts and Joost Vennekens | Application of Logic-Based Methods to Machine Component Design | ICLP | | Jul 15 17:00 |

Angelos Charalambidis, Panos Rondogiannis and Ioanna Symeonidou | Approximation Fixpoint Theory and the Well-Founded Semantics of Higher-Order Logic Programs | ICLP | | Jul 14 12:00 |

Zhizheng Zhang | Introspecting Preferences In Answer Set Programming | ICLP | | Jul 15 16:45 |

Mario Alviano, Carmine Dodaro and Marco Maratea | Shared aggregate sets in answer set programming | ICLP | | Jul 14 11:30 |

Mario Alviano, Carmine Dodaro, Matti Järvisalo, Marco Maratea and Alessandro Previti | Cautious Reasoning in ASP via Minimal models and Unsatisfiable Cores | ICLP | | Jul 16 10:00 |

Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi and Maurizio Proietti | Solving Horn Clauses on Inductive Data Types Without Induction | ICLP | | Jul 14 15:00 |

Joana Côrte-Real, Anton Dries, Inês Dutra and Ricardo Rocha | Improving Candidate Quality of Probabilistic Logic Models | ICLP | | Jul 15 17:15 |

Joaquin Arias, Manuel Carro, Elmer Salazar, Kyle Marple and Gopal Gupta | Constraint Answer Set Programming without Grounding | ICLP | | Jul 14 17:00 |

Angela Bonifati, Stefania Dumbrava and Emilio Jesús Gallego Arias | Certified Graph View Maintenance with Regular Datalog | ICLP | | Jul 15 11:30 |

Tobias Kaminski, Thomas Eiter and Katsumi Inoue | Exploiting Answer Set Programming with External Sources for Meta-Interpretive Learning | ICLP | | Jul 15 14:00 |

George Baryannis, Ilias Tachmazidis, Sotiris Batsakis, Grigoris Antoniou, Mario Alviano, Timos Sellis and Pei-Wei Tsai | A Trajectory Calculus for Qualitative Spatial Reasoning Using Answer Set Programming | ICLP | | Jul 15 15:00 |

Marc Dahlem, Anoop Bhagyanath and Klaus Schneider | Optimal Scheduling for Exposed Datapath Architectures with Buffered Processing Units by ASP | ICLP | | Jul 17 12:00 |

Igor Stéphan | A New Proof-theoretical Linear Semantics for CHR | ICLP | | Jul 17 17:15 |

Van Nguyen, Tran Cao Son and Enrico Pontelli | Natural Language Generation From Ontologies: Application Paper | ICLP | | Jul 15 17:30 |

Thanh Nguyen, Enrico Pontelli and Tran Son | Phylotastic: An Experiment in Creating, Manipulating, and Evolving Phylogenetic Biology Workflows Using Logic Programming | ICLP | | Jul 17 11:00 |

Isabel Garcia-Contreras, Jose F. Morales and Manuel V. Hermenegildo | Towards Incremental and Modular Context-sensitive Analysis | ICLP | | Jul 17 16:45 |

Federico Igne, Agostino Dovier and Enrico Pontelli | MASP-Reduce: a proposal for distributed computation of stable models | ICLP | | Jul 15 17:45 |

Carlo Zaniolo, Ariyam Das, Mohan Yang, Alex Shkapsky, Matteo Interlandi and Tyson Condie | Declarative Algorithms in Datalog with Aggregates: user-friendly formal semantics conducive to performance and scalability | ICLP | | Jul 17 17:45 |

Daniela Inclezan, Qinglin Zhang, Marcello Balduccini and Ankush Israney | An ASP Methodology for Understanding Narratives about Stereotypical Activities | ICLP | | Jul 16 09:00 |

Arun Nampally, Timothy Zhang and C. R. Ramakrishnan | Constraint-Based Inference in Probabilistic Logic Programs | ICLP | | Jul 17 15:00 |

Joohyung Lee and Yi Wang | A Probabilistic Extension of Action Language BC+ | ICLP | | Jul 17 14:30 |

Bishoksan Kafle, John Gallagher, Graeme Gange, Peter Schachte, Harald Sondergaard and Peter J. Stuckey | An iterative approach to precondition inference using constrained Horn clauses | ICLP | | Jul 15 12:00 |

Gregory Duck, Joxan Jaffar and Roland Yap | Shape Neutral Analysis of Graph-based Data-structures | ICLP | | Jul 17 14:00 |

Martin Gebser, Philipp Obermeier, Michel Ratsch-Heitmann, Mario Runge and Torsten Schaub | Routing Driverless Transport Vehicles in Car Assembly with Answer Set Programming | ICLP | | Jul 16 11:00 |

Aleksy Schubert and Pawel Urzyczyn | First-order answer set programming as constructive proof search | ICLP | | Jul 14 14:30 |

Pedro Cabalar, Jorge Fandinno, Luis Farinas Del Cerro and David Pearce | Functional ASP with Intensional Sets; Application to Gelfond-Zhang Agreggates | ICLP | | Jul 14 11:00 |

Nada Sharaf, Slim Abdennadher and Thom Fruehwirth | CHRvis: Syntax and Semantics | ICLP | | Jul 17 17:30 |

Maximiliano Klemen, Nataliia Stulova, Pedro López-García, Jose F. Morales and Manuel V. Hermenegildo | Towards Static Performance Guarantees for Programs with Run-time Checks | ICLP | | Jul 17 16:30 |

Da Shen and Yuliya Lierler | SMT-based Answer Set Solver CMODELS(DIFF) (System Description) | ICLP | | Jul 15 16:30 |

Marijn Heule | Computable Short Proofs | SAT | | Jul 11 11:00 |

Christoph Scholl and Ralf Wimmer | Dependency Quantified Boolean Formulas: An Overview of Solution Methods and Applications | SAT | | |

Rahul Santhanam | Modelling SAT | SAT | | |

Rüdiger Ehlers and Francisco Palau Romero | Approximately Propagation Complete and Conflict Propagating Constraint Encodings | SAT | | Jul 09 14:00 |

Tobias Paxian, Sven Reimer and Bernd Becker | Dynamic Polynomial Watchdog Encoding for Solving Weighted MaxSAT | SAT | | Jul 09 14:30 |

Alexander Nadel | Solving MaxSAT with Bit-Vector Optimization | SAT | | Jul 09 15:00 |

Jan Elffers, Jesus Giráldez-Cru, Jakob Nordstrom and Marc Vinyals | Using Combinatorial Benchmarks to Probe the Reasoning Power of Pseudo-Boolean Solvers | SAT | | Jul 09 16:00 |

Jia Liang, Chanseok Oh, Minu Mathews, Ciza Thomas, Chunxiao Li and Vijay Ganesh | Machine Learning-based Restart Policy for CDCL SAT Solvers | SAT | | Jul 09 16:30 |

Vadim Ryvchin and Alexander Nadel | Chronological Backtracking | SAT | | Jul 09 17:00 |

Sima Jamali and David Mitchell | Centrality-Based Improvements to CDCL Heuristics | SAT | | Jul 09 17:30 |

Dimitris Achlioptas, Zayd Hammoudeh and Panos Theodoropoulos | Fast Sampling of Perfectly Uniform Satisfying Assignments | SAT | | Jul 10 09:00 |

Dimitris Achlioptas, Zayd Hammoudeh and Panos Theodoropoulos | Fast and Flexible Probabilistic Model Counting | SAT | | Jul 10 09:30 |

Johannes K. Fichte, Markus Hecher, Michael Morak and Stefan Woltran | Exploiting Treewidth for Projected Model Counting and its Limits | SAT | | Jul 10 10:00 |

Mikolas Janota | Circuit-based Search Space Pruning in QBF | SAT | | Jul 10 14:00 |

Manuel Kauers and Martina Seidl | Symmetries for QBF | SAT | | Jul 10 14:30 |

Martin Suda and Bernhard Gleiss | Local Soundness for QBF Calculi | SAT | | Jul 10 15:00 |

Michael Lampis, Stefan Mengel and Valia Mitsou | QBF as an Alternative to Courcelle's Theorem | SAT | | Jul 10 16:00 |

Tomáš Peitl, Friedrich Slivovsky and Stefan Szeider | Polynomial-Time Validation of QCDCL Certificates | SAT | | Jul 10 16:30 |

Tobias Friedrich and Ralf Rothenberger | Sharpness of the Satisfiability Threshold for Non-Uniform Random k-SAT | SAT | | Jul 11 09:00 |

Marc Vinyals, Jan Elffers, Jesús Giráldez-Crú, Stephan Gocht and Jakob Nordstrom | In Between Resolution and Cutting Planes: A Study of Proof Systems for Pseudo-Boolean SAT Solving | SAT | | Jul 11 09:30 |

Nicola Galesi, Navid Talebanfard and Jacobo Toran | Cops-Robber games and the resolution of Tseitin formulas | SAT | | Jul 11 10:00 |

Hoda Abbasizanjani and Oliver Kullmann | Minimal unsatisfiability and minimal strongly connected digraphs | SAT | | Jul 11 16:00 |

Ryan Berryhill, Alexander Ivrii and Andreas Veneris | Finding all Minimal Safe Inductive Sets | SAT | | Jul 11 16:30 |

Shubhani Gupta, Aseem Saxena, Anmol Mahajan and Sorav Bansal | Effective use of SMT solvers for Program Equivalence Checking through Invariant Sketching and Query Decomposition | SAT | | Jul 12 11:00 |

Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri and Roberto Sebastiani | Experimenting on Solving Nonlinear Integer Arithmetic with Incremental Linearization | SAT | | Jul 12 11:30 |

Sean Weaver, Hannah Roberts and Michael Smith | XORSAT Set Membership Filters | SAT | | Jul 12 12:00 |

Stepan Kochemazov and Oleg Zaikin | ALIAS: A Modular Tool for Finding Backdoors for SAT | SAT | | Jul 12 14:00 |

Alexey Ignatiev, Antonio Morgado and Joao Marques-Silva | PySAT: A Python Toolkit for Prototyping with SAT Oracles | SAT | | Jul 12 14:30 |

Svyatoslav Korneev, Nina Narodytska, Luca Pulina, Armando Tacchella, Nikolaj Bjorner and Mooly Sagiv | Constrained Image Generation Using Binarized Neural Networks with Decision Procedures | SAT | | Jul 12 15:00 |

Clemens Grabmayer | Modeling Terms by Graphs with Structure Constraints (Two Illustrations) | TERMGRAPH | | |

Lee Barnett and David Plaisted | Programming by Term Rewriting | TERMGRAPH | | Jul 07 17:30 |

Nachum Dershowitz and Jean-Pierre Jouannaud | Drags: an algebraic framework for graph rewriting | TERMGRAPH | | Jul 07 11:00 |

Nneka Ene | A Port-graph Model for Finance | TERMGRAPH | | Jul 07 16:30 |

Wolfram Kahl and Yuhang Zhao | Semantics-Preserving DPO-Based Term Graph Rewriting | TERMGRAPH | | Jul 07 15:00 |

Mitsuhiro Okada and Yuta Takahashi | On quasi ordinal diagram systems | TERMGRAPH | | Jul 07 12:00 |

Sophie Tourret and Andrew Cropper | SLD-Resolution Reduction of Second-Order Horn Fragments - Extended Abstract | TERMGRAPH | | Jul 07 16:00 |

János Varga | Finding the Transitive Closure of Functional Dependencies using Strategic Port Graph Rewriting | TERMGRAPH | | Jul 07 17:00 |

Vladimir Zamdzhiev | A Framework for Rewriting Families of String Diagrams | TERMGRAPH | | Jul 07 11:30 |

Tiantian Gao | Knowledge Authoring and Question Answering via Controlled Natural Language | ICLP-DC | | Jul 18 12:00 |

Van Nguyen | Natural Language Generation From Ontologies | ICLP-DC | | Jul 18 11:30 |

Yi Wang | Probabilistic Action Language pBC+ | ICLP-DC | | Jul 18 10:00 |

Richard Taupe | Speeding Up Lazy-Grounding Answer Set Solving | ICLP-DC | | Jul 18 15:00 |

Filipe Gouveia, Ines Lynce and Pedro T. Monteiro | Model Revision of Logical Regulatory Networks using Logic-based Tools | ICLP-DC | | Jul 18 16:00 |

Emily Leblanc | Explaining Actual Causation via Reasoning about Actions and Change | ICLP-DC | | Jul 18 09:30 |

Zhun Yang | Translating P-log, LP^{MLN}, LPOD, and CR-Prolog2 into Standard Answer Set Programs | ICLP-DC | | Jul 18 14:30 |

Philipp Obermeier | Scalable Robotic Intra-Logistics with Answer Set Programming | ICLP-DC | | Jul 18 14:00 |

Frantisek Farka | Proof-relevant resolution for elaboration of programming languages | ICLP-DC | | Jul 18 09:00 |

Arindam Mitra | The Learning-Knowledge-Reasoning Paradigm For Natural Language Understanding and Question Answering | ICLP-DC | | Jul 18 11:00 |

Jamie Vicary | Designing Globular: formal proofs as geometrical objects | UITP | | |

Tomer Libal | Implementing a Proof Assistant using Focusing and Logic Programming | UITP | | Jul 13 10:00 |

Jan Gorzny, Ezequiel Postan and Bruno Woltzenlogel Paleo | Partial Regularization of First-Order Resolution Proofs | UITP | | Jul 13 11:00 |

Sarah Grebing, An Thuy Tien Luong and Alexander Weigl | Adding Text-Based Interaction to a Direct-Manipulation Interface for Program Verification -- Lessons Learned | UITP | | Jul 13 11:30 |

Rustam Zhumagambetov and Mark Sterling | Automated Theorem Proving in a Chat Environment | UITP | | Jul 13 12:00 |

Makarius Wenzel | Isabelle/PIDE after 10 years of development | UITP | | Jul 13 14:00 |

Steffen Frerix and Peter Koepke | Text-Orientated Formal Mathematics | UITP | | Jul 13 14:30 |

Florent Capelli and Stefan Mengel | Tractability results for structured quantified CNF-formulas via knowledge compilation | QBF | | Jul 08 14:40 |

Holger Hoos, Tomáš Peitl, Friedrich Slivovsky and Stefan Szeider | Portfolio-Based Algorithm Selection for Circuit QBFs | QBF | | Jul 08 16:20 |

Martin Suda | Towards the Semantics of QBF Clauses | QBF | | Jul 08 10:00 |

Matthias van der Hallen and Gerda Janssens | A Grounder From Second-Order Logic To QBF | QBF | | Jul 08 15:00 |

Jan Maly and Stefan Woltran | A new logic for jointly representing hard and soft constraints | PRUV | | Jul 19 12:00 |

Alireza Ensan, Eugenia Ternovska and Heng Liu | A Model-Theoretic View on Preferences in Declarative Specifications of Search Problems | PRUV | | Jul 19 16:00 |

Nico Potyka | Measuring Disagreement among Knowledge Bases | PRUV | | Jul 19 11:00 |

Cunjing Ge, Feifei Ma, Tian Liu, Jian Zhang and Xutong Ma | A New Probabilistic Algorithm for Approximate Model Counting | PRUV | | Jul 19 16:30 |

José Paredes, Maria Vanina Martinez, Gerardo Simari and Marcelo A. Falappa | Leveraging Probabilistic Existential Rules for Adversarial Deduplication | PRUV | | Jul 19 17:00 |

Aouatef Rouahi, Kais Ben Salah and Khaled Ghedira | Evidential Group Decision Making Model with Belief-Based Preferences | PRUV | | Jul 19 11:30 |

Laura Giordano and Valentina Gliozzi | Reasoning about exceptions in ontologies: from the lexicographic closure to the skeptical closure | PRUV | | Jul 19 15:10 |

Cunjing Ge, Feifei Ma and Jian Zhang | VolCE: An Efficient Tool for Solving #SMT(LA) Problems | PRUV | | Jul 19 17:30 |

Özgür Akgün | Automated Constraint Modelling with Conjure | LaSh | | Jul 18 16:25 |

Sabine Bauer | Decidable Linear Tree Constraints | LaSh | | Jul 18 17:15 |

Bruno Courcelle and Irène Durand | Monadic Second-Order Model Checking with Fly-Automata | LaSh | | Jul 18 09:00 |

Johannes Fichte | Solving #SAT by Parameterized Algorithms: Exploiting Small Treewidth | LaSh | | Jul 18 16:50 |

Tomas Fiedor, Lukas Holik, Petr Janku, Ondrej Lengal and Tomas Vojnar | Lazy Automata Techniques for WS1S | LaSh | | Jul 18 10:05 |

Alan Frisch | ESSENCE, A Language for Specifying Combinatorial Problems: What, Why and So What? | LaSh | | Jul 18 16:00 |

Robert Giegerich | Declarative Dynamic Programming with Inverse Coupled Rewrite Systems | LaSh | | Jul 18 14:00 |

Joachim Kneis, Alexander Langer and Peter Rossmanith | Courcelle’s Theorem – A Game-Theoretic Approach | LaSh | | Jul 18 11:00 |

Eugenia Ternovska | A Logic of Information Flows | LaSh | | Jul 18 15:00 |

Dmitriy Traytel | A Derivative-Based Decision Procedure for WS1S | LaSh | | Jul 18 12:05 |

Eugenia Ternovska | A Logic of Information Flows - Paper | LaSh | | |

Sabine Bauer | Decidable Linear Tree Constraints - Extended Abstract | LaSh | | |

Bruno Courcelle | Monadic Second-Order Model Checking with Fly-Automata - Slides | LaSh | | |

Roberta Costabile, Alessio Fiorentino, Nicola Leone, Marco Manna, Kristian Reale and Francesco Ricca | Role-Based Access Control via JASP | LPOP | | Jul 18 11:30 |

Marc Denecker and Jo Devriendt | The RBAC challenge in the KB-paradigm | LPOP | | |

Thom Fruehwirth | A Rule-Based Tool for Analysis and Generation of Graphs Applied to Mason's Marks | LPOP | | Jul 18 16:50 |

Thom Fruehwirth | Security Policies in Constraint Handling Rules | LPOP | | Jul 18 11:10 |

Daniel Gall | Confluence Analysis of Cognitive Models with Constraint Handling Rules | LPOP | | Jul 18 15:20 |

Nicola Leone, Bernardo Cuteri, Marco Manna, Kristian Reale and Francesco Ricca | On the Development of Industrial Applications with ASP | LPOP | | Jul 18 09:50 |

Yanhong A. Liu and Scott Stoller | Easier Rules and Constraints for Programming | LPOP | | Jul 18 12:10 |

Torsten Schaub | How to upgrade ASP for true dynamic modelling and solving? | LPOP | | Jul 18 16:40 |

K. Tuncay Tekle | The RBAC challenge in LogiQL: Solutions and Limitations | LPOP | | |

Peter Van Roy | A software system should be declarative except where it interacts with the real world | LPOP | | Jul 18 17:00 |

Joost Vennekens | Logic-based Methods for Software Engineers and Business People | LPOP | | Jul 18 12:00 |

David S. Warren | LPOP2018 XSB Position Paper | LPOP | | Jul 18 11:20 |

Neng-Fa Zhou and Håkan Kjellerstrand | A Picat-based XCSP Solver - from Parsing, Modeling, to SAT Encoding | LPOP | | Jul 18 15:10 |

Julien Narboux | GeoCoq: Formalized Foundations of Geometry | ThEdu | | |

Nuno Baeta and Pedro Quaresma | Rating of Geometric Automated Theorem Provers | ThEdu | | Jul 18 10:00 |

Walther Neuper | Lucas Interpretation from Programmers’ Perspective | ThEdu | | Jul 18 11:00 |

Jørgen Villadsen, Andreas Halkjær From and Anders Schlichtkrull | Natural Deduction Assistant (NaDeA) | ThEdu | | Jul 18 09:30 |

Anders Schlichtkrull, Jørgen Villadsen and Andreas Halkjær From | Students' Proof Assistant (SPA) | ThEdu | | Jul 18 09:00 |

Jørgen Villadsen | Proving in the Isabelle Proof Assistant that the Set of Real Numbers is not Countable | ThEdu | | Jul 18 14:30 |

Maximilian Doré and Krysia Broda | Towards intuitive reasoning in axiomatic geometry | ThEdu | | Jul 18 14:00 |

Natasha Fernandes, Mark Dras and Annabelle McIver | Processing text for privacy: An information flow perspective | FM | | |

Kim Guldstrand Larsen, Florian Lorber and Brian Nielsen | 20 Years of Real Real Time Model Validation | FM | | |

Keyvan Azadbakht, Frank De Boer and Erik de Vink | Deadlock Detection for Actor-based Coroutines | FM | | Jul 15 09:00 |

Arthur Américo, Mario S. Alvim and Annabelle McIver | An Algebraic Approach for Reasoning About Information Flow | FM | | Jul 15 09:30 |

Jingyi Wang, Jun Sun, Yifan Jia, Shengchao Qin and Zhiwu Xu | Towards `Verifying' a Water Treatment System | FM | | Jul 15 10:00 |

Florent Avellaneda and Alexandre Petrenko | FSM Inference from Long Traces | FM | | Jul 15 12:00 |

Davide Giacomo Cavezza, Dalal Alrajeh and Andras Gyorgy | A Weakness Measure for GR(1) Formulae | FM | | Jul 15 15:00 |

Simon Busard and Charles Pecheur | Producing Explanations for Rich Logics | FM | | Jul 15 16:00 |

Thomas Ferrère | The Compound Interest in Relaxing Punctuality | FM | | Jul 15 16:30 |

Ivan Ruchkin, Joshua Sunshine, Grant Iraci, Bradley Schmerl and David Garlan | IPL: An Integration Property Language for Multi-Model Cyber-Physical Systems | FM | | Jul 15 17:00 |

Raúl Pardo, Cesar Sanchez and Gerardo Schneider | Timed Epistemic Knowledge Bases for Social Networks | FM | | Jul 15 17:30 |

Giovanni Bacci, Kim Guldstrand Larsen, Nicolas Markey, Patricia Bouyer-Decitre, Uli Fahrenberg and Pierre-Alain Reynier | Optimal and Robust Controller Synthesis Using Energy Timed Automata with Uncertainty | FM | | Jul 16 10:00 |

Ian J. Hayes and Larissa Meinicke | Encoding fairness in a synchronous concurrent program algebra | FM | | Jul 16 11:00 |

Robert Colvin and Graeme Smith | A wide-spectrum language for verification of programs on weak memory models | FM | | Jul 16 11:30 |

Daniel Fava, Martin Steffen and Volker Stolz | Operational Semantics of a Weak Memory Model with Channel Synchronization | FM | | Jul 16 12:00 |

Signe Geisler and Anne E. Haxthausen | Stepwise Development and Model Checking of a Distributed Interlocking System - using RAISE | FM | | Jul 16 11:00 |

Rongjie Yan, Di Zhu, Fan Zhang, Yiqi Lv, Junjie Yang and Kai Huang | Resource-aware Design for Reliable Autonomous Applications with Multiple Periods | FM | | Jul 16 11:30 |

Philipp Berger, Joost-Pieter Katoen, Erika Ábrahám, Md Tawhid Bin Waez and Thomas Rambow | Verifying Auto-Generated C Code from Simulink | FM | | Jul 16 12:00 |

Andrea Vandin, Maurice H. Ter Beek, Axel Legay and Alberto Lluch Lafuente | QFLan: A Tool for the Quantitative Analysis of Highly Reconfigurable Systems | FM | | Jul 16 16:00 |

Thomas Letan, Yann Régis-Gianas, Pierre Chifflier and Guillaume Hiet | Modular Verification of Programs with Effects and Effect Handlers in Coq | FM | | Jul 16 16:30 |

Heiko Becker, Pavel Panchekha, Eva Darulova and Zachary Tatlock | Combining Tools for Optimization and Analysis of Floating-Point Computations | FM | | Jul 16 17:00 |

Laura Titolo, Mariano Moscato, Cesar Munoz, Aaron Dutle and Francois Bobot | A Formally Verified Floating-Point Implementation of the Compact Position Reporting Algorithm | FM | | Jul 16 17:30 |

Johanna Nellen, Thomas Rambow, Md Tawhid Bin Waez, Erika Abraham and Joost-Pieter Katoen | Formal Verification of Automotive Simulink Controller Models: Empirical Technical Challenges, Evaluation and Recommendations | FM | | Jul 16 16:00 |

Claudio Menghi, Sergio Garcia, Patrizio Pelliccione and Jana Tumova | Multi-Robot LTL Planning Under Uncertainty | FM | | Jul 16 16:30 |

Andrew Sogokon, Khalil Ghorbal, Yong Kiam Tan and André Platzer | Vector Barrier Certificates and Comparison Systems | FM | | Jul 16 17:00 |

Hana Chockler, Shibashis Guha and Orna Kupferman | Timed Vacuity | FM | | Jul 16 17:30 |

Takumi Akazaki, Shuang Liu, Yoriyuki Yamagata, Yihai Duan and Jianye Hao | Falsification of Cyber-Physical Systems Using Deep Reinforcement Learning | FM | | Jul 17 09:00 |

Dhriti Khanna, Subodh Sharma, César Rodríguez and Rahul Purandare | Dynamic Symbolic Verification of MPI Programs | FM | | Jul 17 09:30 |

Sander de Putter and Anton Wijs | To Compose, Or Not to Compose, That is the Question: An Analysis of Compositional State Space Generation | FM | | Jul 17 10:00 |

Gavin Lowe | View abstraction for systems with component identities | FM | | Jul 17 12:00 |

Fuyuan Zhang, Yongwang Zhao, David Sanan, Yang Liu, Alwen Tiu, Shang-Wei Lin and Jun Sun | Compositional Reasoning for Shared-variable Concurrent Programs | FM | | Jul 17 14:00 |

Axel Legay, Dirk Nowotka, Danny Bøgsted Poulsen and Louis-Marie Traonouez | Statistical Model Checking of LLVM Code | FM | | Jul 17 14:30 |

Elvira Albert, Miguel Gomez-Zamalloa, Albert Rubio, Matteo Sammartino and Alexandra Silva | SDN-Actors: Modeling and Verification of SDN Programs | FM | | Jul 17 17:00 |

Sorawee Porncharoenwase, Tim Nelson and Shriram Krishnamurthi | CompoSAT: Specification-Guided Coverage for Model Finding | FM | | Jul 17 16:00 |

Chuchu Fan, Zhenqi Huang and Sayan Mitra | Approximate Partial Order Reduction | FM | | Jul 17 16:30 |

Cosimo Laneve | A lightweight deadlock analysis for programs with threads and reentrant locks | FM | | Jul 17 15:00 |

Alessandro Cimatti, Ivan Stojic and Stefano Tonetta | Formal Specification and Verification of Dynamic Parametrized Architectures | FM | | Jul 17 17:30 |

Cesar Munoz, Anthony Narkawicz and Aaron Dutle | From Formal Requirements to Highly Assured Software for Unmanned Aircraft Systems | FM | | Jul 17 09:00 |

Arne Boralv | Interlocking Design Automation using Prover Trident | FM | | Jul 17 09:30 |

Joerg Brauer and Uwe Schulze | Model-Based Testing for Avionics Systems | FM | | Jul 17 10:00 |

Daniel Kaestner, Laurent Mauborgne and Christian Ferdinand | On Software Safety, Security, and Abstract Interpretation | FM | | Jul 17 14:00 |

Pavel Avgustinov, Kevin Backhouse and Man Yue Mo | Variant analysis with QL | FM | | Jul 17 14:30 |

Ernie Cohen | Object-Oriented Security Proofs | FM | | Jul 17 15:00 |

Nikolaj Bjorner | Z3 and SMT in Industrial R&D | FM | | Jul 17 16:00 |

Tewodros A. Beyene and Harald Ruess | Evidential and Continuous Integration of Software Verification Tools | FM | | Jul 17 16:30 |

Thierry Lecomte | Disruptive Innovations for the Development and the Deployment of Fault-Free Software | FM | | Jul 17 17:00 |

Gabriel Ebner | Fast cut-elimination using proof terms: an empirical study | CL&C | | Jul 07 11:00 |

Anthony Cantor and Aaron Stump | (Short Paper) Towards a Dualized Sequent Calculus with Canonicity | CL&C | | Jul 07 10:00 |

Graham Leigh | Herbrand's Theorem as Higher-Order Recursion | CL&C | | Jul 07 14:45 |

Federico Aschieri | On Natural Deduction for Herbrand Constructive Logics III: The Strange Case of the Intuitionistic Logic of Constant Domains | CL&C | | Jul 07 14:00 |

Matteo Manighetti and Andrea Condoluci | Admissible tools in the kitchen of intuitionistic logic | CL&C | | Jul 07 16:00 |

Sorin Stratulat | Validating Back-links of FOL$_{\mbox{\normalsize ID}}$ Cyclic Pre-proofs | CL&C | | Jul 07 11:45 |

Anupam Das | Some ideas on cut-elimination for cyclic arithmetic proofs | CL&C | | Jul 07 17:30 |

Stéphane Demri, Etienne Lozes and Denis Lugiez | A Complete Proof System for Basic Symbolic Heaps with Permissions | ADSL | | Jul 13 12:00 |

Jens Katelaan, Dejan Jovanović and Georg Weissenbacher | Sloth: Separation Logic and Theories via Small Models | ADSL | | Jul 13 16:10 |

Mnacho Echenim, Radu Iosif and Nicolas Peltier | The Complexity of Prenex Separation Logic with One Selector | ADSL | | Jul 13 15:20 |

Didier Galmiche and Daniel Mery | Labelled Cyclic Proofs for Separation Logic | ADSL | | Jul 13 11:30 |

Koji Nakazawa, Makoto Tatsuta and Daisuke Kimura | Cyclic Theorem Prover for Separation Logic by Magic Wand | ADSL | | Jul 13 11:00 |

James Brotherston and Max Kanovich | On the Complexity of Pointer Arithmetic in Separation Logic | ADSL | | Jul 13 14:50 |

Jason Gross | Teaching Your Rooster to Crow in C | Coq | | Jul 08 17:00 |

Armaël Guéneau | Procrastination, A proof engineering technique | Coq | | Jul 08 10:00 |

Sylvain Boulmé | What is the Foreign Function Interface of the Coq Programming Language? | Coq | | Jul 08 11:30 |

Reynald Affeldt, Cyril Cohen, Assia Mahboubi, Damien Rouhling and Pierre-Yves Strub | Classical Analysis with Coq | Coq | | Jul 08 11:00 |

Olivier Laurent | Preliminary Report on the Yalla Library | Coq | | Jul 08 12:00 |

Mirai Ikebuchi and Keisuke Nakano | ComplCoq: Rewrite Hint Construction with Completion Procedures | Coq | | Jul 08 16:00 |

Lasse Blaauwbroek | Proof Construction by Tactic Learning | Coq | | Jul 08 17:30 |

Cyprien Mangin and Matthieu Sozeau | Towards a formalization of the guard condition | Coq | | Jul 08 16:30 |

Ugo Dal Lago | On Higher-Order Probabilistic Computation | DCM | | |

Delia Kesner | Quantitative Types: from Foundations to Applications | DCM | | |

Damiano Mazza | Polyadic Approximations and Intersection Types | DCM | | |

Ian Mackie | Models of Computation that Conserve Data | DCM | | Jul 08 10:00 |

Paola Giannini, Marco Servetto and Elena Zucca | A syntactic model of mutation and aliasing | DCM | | Jul 08 11:00 |

Adrian Francalanza, Marco Giunti and António Ravara | Pointing to Private Names | DCM | | Jul 08 11:30 |

Joseph Razavi and Andrea Schalk | A Category Theoretic Interpretation of Gandy’s Principles for Mechanisms | DCM | | Jul 08 12:00 |

Alessandra Di Pierro | Towards a Formal System for Topological Quantum Computation | DCM | | Jul 08 15:00 |

Nachum Dershowitz | Generic Graph Semantics | DCM | | Jul 08 16:00 |

Siddharth Bhaskar | Computability over locally finite structures from algebra | LCC | | Jul 13 11:45 |

Anupam Das and Isabel Oitavem | A recursion-theoretic characterisation of the positive polynomial-time functions | LCC | | Jul 13 11:15 |

Steven Lindell and Scott Weinstein | Traversal-invariant definability and Logarithmic-space computation | LCC | | Jul 13 11:00 |

Pedro Lopez-Garcia, Maximiliano Klemen, Umer Liqat and Manuel V. Hermenegildo | A General Equational Framework for Static Profiling of Parametric Resource Usage | LCC | | Jul 13 12:00 |

Moritz Müller and Ján Pich | Feasibly constructive proofs of succinct weak circuit lower bounds | LCC | | Jul 13 11:30 |

Edwin Pin | Completeness in the Second Level of the Polynomial Time Hierarchy through Syntactic Properties | LCC | | Jul 13 12:15 |

Martin Giese | Industrial Data Access | IJCAR | | |

Erika Abraham | Symbolic Computation Techniques in SMT Solving: Mathematical Beauty meets Efficient Heuristics | IJCAR | | |

Jean Marie Lagniez, Daniel Le Berre, Tiago de Lima and Valentin Montmirail | An Assumption-Based Approach for Solving The Minimal S5-Satisfiability Problem | IJCAR | | Jul 14 14:00 |

Yizheng Zhao and Renate A. Schmidt | FAME: An Automated Tool for Semantic Forgetting in Expressive Description Logics | IJCAR | | Jul 14 16:30 |

Alexander Bentkamp, Jasmin Christian Blanchette, Simon Cruanes and Uwe Waldmann | Superposition for Lambda-Free Higher-Order Logic | IJCAR | | Jul 16 11:30 |

Miika Hannula and Sebastian Link | Automated Reasoning about Key Sets | IJCAR | | Jul 17 11:30 |

Michael Peter Lettmann and Nicolas Peltier | A Tableaux Calculus for Reducing Proof Size | IJCAR | | Jul 15 10:00 |

Franziska Rapp and Aart Middeldorp | FORT 2.0 | IJCAR | | Jul 17 15:15 |

Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel and Uwe Waldmann | Formalizing Bachmair and Ganzinger's Ordered Resolution Prover | IJCAR | | Jul 15 12:00 |

Alexander Steen and Christoph Benzmüller | The Higher-Order Prover Leo-III | IJCAR | | Jul 17 14:00 |

Jeremy Dawson, Nachum Dershowitz and Rajeev Gore | Well-Founded Unions | IJCAR | | Jul 15 15:00 |

Katalin Fazekas, Fahiem Bacchus and Armin Biere | Implicit Hitting Set Algorithms for Maximum Satisfiability Modulo Theories | IJCAR | | Jul 14 11:30 |

Sylvain Conchon, David Declerck and Fatiha Zaidi | Cubicle-W: Parameterized Model Checking on Weak Memory | IJCAR | | Jul 17 14:30 |

Florian Lonsing and Uwe Egly | QRAT+: Generalizing QRAT by a More Powerful QBF Redundancy Property | IJCAR | | Jul 15 09:00 |

Guillaume Melquiond and Raphaël Rieu-Helft | A Why3 framework for reflection proofs and its application to GMP's algorithms | IJCAR | | Jul 15 17:30 |

Marcelo Finger and Sandro Preto | Probably Half True: Probabilistic Satisfiability over Lukasiewicz Infinitely-valued Logic | IJCAR | | Jul 17 11:00 |

André Platzer | Uniform Substitution for Differential Game Logic | IJCAR | | Jul 15 17:00 |

Max Kanovich, Stepan Kuznetsov, Vivek Nigam and Andre Scedrov | A Logical Framework with Commutative and Non-Commutative Subexponentials | IJCAR | | Jul 15 16:30 |

Peter Backeman, Aleksandar Zeljić, Christoph M. Wintersteiger and Philipp Rümmer | Exploring Approximations for Floating-Point Arithmetic using UppSAT | IJCAR | | Jul 15 11:00 |

Manuel Bodirsky and Johannes Greiner | Complexity of Combinations of Qualitative Constraint Satisfaction Problems | IJCAR | | Jul 16 09:30 |

Mnacho Echenim, Nicolas Peltier and Yanis Sellami | A Generic Framework for Implicate Generation Modulo Theories | IJCAR | | Jul 14 12:00 |

Stefan Ciobaca and Dorel Lucanu | A Coinductive Approach to Proving Reachability in Logically Constrained Term Rewriting Systems | IJCAR | | Jul 14 16:00 |

Cunjing Ge, Feifei Ma, Tian Liu, Jian Zhang and Xutong Ma | A New Probabilistic Algorithm for Approximate Model Counting | IJCAR | | Jul 14 15:00 |

Martin Bromberger | A Reduction from Unbounded Linear Mixed Arithmetic Problems into Bounded Problems | IJCAR | | Jul 15 12:00 |

Nao Hirokawa, Julian Nagele and Aart Middeldorp | Cops and CoCoWeb: Infrastructure for Confluence Tools | IJCAR | | Jul 17 15:00 |

Pei Huang, Feifei Ma, Jian Zhang, Cunjing Ge and Hantao Zhang | Investigating the Existence of Large Sets of Idempotent Quasigroups via Satisfiability Testing | IJCAR | | Jul 14 14:30 |

Jasmin Christian Blanchette, Nicolas Peltier and Simon Robillard | Superposition with Datatypes and Codatatypes | IJCAR | | Jul 16 11:00 |

Nicholas Smallbone and Koen Claessen | Efficient encodings of first-order Horn formulas in equational logic | IJCAR | | Jul 16 12:00 |

Evgenii Kotelnikov, Laura Kovacs and Andrei Voronkov | A FOOLish Encoding of the Next State Relations of Imperative Programs | IJCAR | | Jul 15 16:30 |

Dominique Larchey-Wendling | Constructive Decision via Redundancy-free Proof-Search | IJCAR | | Jul 15 11:00 |

Nicolas Jeannerod and Ralf Treinen | Deciding the First-Order Theory of an Algebra of Feature Trees with Updates | IJCAR | | Jul 16 09:00 |

Jens Katelaan, Dejan Jovanović and Georg Weissenbacher | A Separation Logic with Data: Small Models and Automation | IJCAR | | Jul 17 10:00 |

Sarah Winkler and Georg Moser | MaedMax: A Maximal Ordered Completion Tool | IJCAR | | Jul 17 14:45 |

Matteo Acclavio and Lutz Strassburger | From Syntactic Proofs to Combinatorial Proofs | IJCAR | | Jul 15 16:00 |

Cláudia Nalon and Dirk Pattinson | A Resolution-Based Calculus for Preferential Logics | IJCAR | | Jul 15 09:00 |

Benjamin Kiesl, Adrian Rebola-Pardo and Marijn Heule | Extended Resolution Simulates DRAT | IJCAR | | Jul 15 09:30 |

Bohua Zhan and Maximilian P. L. Haslbeck | Verifying Asymptotic Time Complexity of Imperative Programs in Isabelle | IJCAR | | Jul 15 11:30 |

Jochen Hoenicke and Tanja Schindler | Efficient Interpolation for the Theory of Arrays | IJCAR | | Jul 14 11:00 |

Bartosz Piotrowski and Josef Urban | ATPboost: Learning Premise Selection in Binary Setting with ATP Feedback | IJCAR | | Jul 17 14:15 |

Dennis Müller, Florian Rabe and Michael Kohlhase | Theories as Types | IJCAR | | Jul 15 17:30 |

Andrew Reynolds, Arjun Viswanathan, Haniel Barbosa, Cesare Tinelli and Clark Barrett | Datatypes with Shared Selectors | IJCAR | | Jul 15 11:30 |

Yevgeny Kazakov and Peter Skočovský | Enumerating Justifications using Resolution | IJCAR | | Jul 15 09:30 |

Alexey Ignatiev, Filipe Pereira, Nina Narodytska and Joao Marques-Silva | A SAT-Based Approach to Learn Explainable Decision Sets | IJCAR | | Jul 15 10:00 |

Son Ho, Oskar Abrahamsson, Ramana Kumar, Magnus O. Myreen, Yong Kiam Tan and Michael Norrish | Proof-Producing Synthesis of CakeML with I/O and Local State from Monadic HOL Functions | IJCAR | | Jul 15 17:00 |

Julio Cesar Lopez Hernandez and Konstantin Korovin | An abstraction-refinement framework for reasoning with large theories | IJCAR | | Jul 17 12:00 |

Jacopo Urbani, Markus Krötzsch, Ceriel Jacobs, Irina Dragoste and David Carral | Efficient Model Construction for Horn Logic with VLog: System Description | IJCAR | | Jul 14 16:45 |

Anupam Das | Focussing, MALL and the polynomial hierarchy | IJCAR | | Jul 16 10:00 |

Etienne Payet and Fausto Spoto | Checking Array Bounds by Abstract Interpretation and Symbolic Expressions | IJCAR | | Jul 15 16:00 |

Salvador Lucas | Presentation of the WST 2018 proceedings | WST | | |

Eric Hehner | Objective and Subjective Specifications | WST | | Jul 18 12:00 |

Guillaume Genestier and Frédéric Blanqui | Termination of Lambda-Pi modulo rewriting using the size-change principle | WST | | Jul 19 16:00 |

Jera Hensel, Florian Frohn and Jürgen Giesl | Complexity Analysis for Bitvector Programs | WST | | Jul 19 11:00 |

Alfons Geser, Dieter Hofbauer and Johannes Waldmann | Semantic Kachinuki Order | WST | | Jul 18 14:00 |

Nachum Dershowitz and Jean-Pierre Jouannaud | GPO: A Path Ordering for Graphs | WST | | Jul 18 11:30 |

Jose Divasón, Sebastiaan Joosten, René Thiemann and Akihisa Yamada | A Perron-Frobenius Theorem for Jordan Blocks for Complexity Proving | WST | | Jul 19 11:30 |

Jonas Schöpf and Christian Sternagel | TTT2 with Termination Templates for Teaching | WST | | Jul 19 15:00 |

Cristina David, Daniel Kroening and Peter Schrammel | Procedure-Modular Termination Analysis | WST | | Jul 18 11:00 |

Salvador Lucas | Well-founded models in proofs of termination | WST | | Jul 18 15:00 |

Aalok Thakkar, Balaji Krishnamurthy and Piyush Gupta | Verification of Rewriting-based Query Optimizers | WST | | Jul 19 14:30 |

Jesús J. Doménech, Samir Genaim and John P. Gallagher | Control-Flow Refinement via Partial Evaluation | WST | | Jul 19 14:00 |

Alicia Merayo Corcoba and Samir Genaim | Inference of Linear Upper-Bounds on the Expected Cost by Solving Cost Relations | WST | | Jul 19 12:00 |

Dieter Hofbauer | Embracing Infinity - Termination of String Rewriting by Almost Linear Weight Functions | WST | | Jul 18 14:30 |

Carsten Fuhs and Cynthia Kop | Improving Static Dependency Pairs for Higher-Order Rewriting | WST | | Jul 19 16:30 |

Guy Avni, Thomas A. Henzinger and Ventsislav Chonev | Infinite-Duration Richman Bidding Games | SR | | Jul 08 14:00 |

Nicolas Basset, Ismaël Jecker, Arno Pauly, Jean-Francois Raskin and Marie Van Den Bogaard | Beyond admissibility: Dominance between chains of strategies | SR | | Jul 07 17:20 |

Francesco Belardinelli, Alessio Lomuscio, Aniello Murano and Sasha Rubin | Verification of Multi-agent Systems with Imperfect Information and Public Actions | SR | | Jul 07 16:00 |

Raphaël Berthon, Bastien Maubert, Aniello Murano, Sasha Rubin and Moshe Vardi | Strategy Logic with Imperfect Information | SR | | Jul 08 16:40 |

Antonio Di Stasio, Aniello Murano and Moshe Vardi | Solving Parity Games: Explicit vs Symbolic | SR | | Jul 08 14:40 |

Nathanaël Fijalkow, Bastien Maubert, Aniello Murano and Sasha Rubin | Quantifying Bounds in Strategy Logic | SR | | Jul 08 16:00 |

Patrick Gardy, Patricia Bouyer and Nicolas Markey | Dependences in Strategy Logic | SR | | Jul 08 17:20 |

Neil Ghani, Jules Hedges, Philipp Zahn and Viktor Winschel | Compositional Game Theory | SR | | Jul 07 14:00 |

Julian Gutierrez, Paul Harrenstein, Thomas Steeples and Michael Wooldridge | Local Equilibria in Logic-Based Multi-Player Games | SR | | Jul 07 16:40 |

Stephane Le Roux | Concurrent games and semi-random determinacy | SR | | Jul 07 14:40 |

Henning Christiansen and Maja H. Kirkeby | Confluence in Constraint Handling Rules | IWC | | |

Simon Forest | Critical pairs for Gray categories | IWC | | Jul 07 11:30 |

Nohra Hage and Philippe Malbos | Coherence of monoids by insertions | IWC | | Jul 07 11:00 |

Benjamin Dupont and Philippe Malbos | Coherence modulo relations | IWC | | Jul 07 10:00 |

Cyrille Chenavier | The diamond lemma for free modules | IWC | | Jul 07 12:00 |

Christian Sternagel and Sarah Winkler | Certified Ordered Completion | IWC | | Jul 07 15:00 |

Bertram Felgenhauer, Aart Middeldorp, T. V. H. Prathamesh and Franziska Rapp | Towards a Verified Decision Procedure for Confluence of Ground Term Rewrite Systems in Isabelle/HOL | IWC | | Jul 07 14:30 |

Naoki Nishida, Yuta Tsuruta and Yoshiaki Kanazawa | Convergence of Simultaneously and Sequentially Unraveled TRSs for Normal Conditional TRSs | IWC | | Jul 07 14:00 |

Kousuke Fukui and Koji Nakazawa | Complete Axiom System of Cluster Algebra | IWC | | Jul 07 16:00 |

Manfred Schmidt-Schauss and Nils Dallmeyer | Optimizing Space of Parallel Processes | WPTE | | Jul 08 11:30 |

Yoshiaki Kanazawa and Naoki Nishida | On Transforming Functions Accessing Global Variables into Logically Constrained Term Rewriting Systems | WPTE | | Jul 08 12:00 |

Naoki Nishida and Yuya Maeda | On Transforming Narrowing Trees into Regular Tree Grammars Generating Ranges of Substitutions | WPTE | | Jul 08 14:30 |

David Sabel | Automating the Diagram Method to Prove Correctness of Program Transformations | WPTE | | Jul 08 11:00 |

Sebastian Buruiana and Stefan Ciobaca | Reducing Total Correctness to Partial Correctness by a Transformation of the Language Semantics | WPTE | | Jul 08 14:00 |

Christian Herrera, Tewodros A. Beyene and Vivek Nigam | Verification of Ada Programs with AdaHorn | WPTE | | Jul 08 15:00 |

Kuen-Bang Hou | Cubical Computational Type Theory and RedPRL | LFMTP | | |

Delia Kesner | A fresh view of call-by-need | LFMTP | | |

Grigore Rosu | Why and How Does K work? The Logical Infrastructure Behind It | LFMTP | | |

Carlo Angiuli, Evan Cavallo, Kuen-Bang Hou Favonia, Robert Harper and Jonathan Sterling | The RedPRL Proof Assistant | LFMTP | | |

Martin Copes, Nora Szasz and Alvaro Tasistro | Formalization in Constructive Type Theory of the Standardization Theorem | LFMTP | | Jul 07 14:00 |

Ernesto Copello, Nora Szasz and Alvaro Tasistro | Formalisation of Barendregt's Variable Convention for Generic Structures with Binders | LFMTP | | Jul 07 14:30 |

François Thiré | Sharing a library between proof assistants: reaching out to the HOL family | LFMTP | | Jul 07 10:00 |

Rodolphe Lepigre and Christophe Raffalli | Abstract Representation of Binders in OCaml using the Bindlib Library | LFMTP | | Jul 07 17:00 |

Ulysse Gérard and Dale Miller | Functional programming with λ-tree syntax: a progress report | LFMTP | | Jul 07 17:30 |

Kaustuv Chaudhuri, Ulysse Gérard and Dale Miller | Computation-as-deduction in Abella: work in progress | LFMTP | | Jul 07 12:00 |

Francesco Komauli and Alberto Momigliano | Property-Based Testing of Abstract Machines: an Experience Report | LFMTP | | Jul 07 12:20 |

David Feller, Joe Wells, Sébastien Carlier and Fairouz Kamareddine | What Does This Notation Mean Anyway? BNF-Style Notation as it is actually used | LFMTP | | Jul 07 15:00 |

Somesh Jha | Semantic Adversarial Deep Learning | CAV | | Jul 16 11:00 |

Eran Yahav | From Programs to Interpretable Deep Models and Back | CAV | | Jul 14 14:00 |

Byron Cook | Formal reasoning about the security of AWS | CAV | | |

Ilya Grishchenko, Matteo Maffei and Clara Schneidewind | Foundations and Tools for the Static Analysis of Ethereum smart contracts | CAV | | |

Bernhard Kragl and Shaz Qadeer | Layered Concurrent Programs | CAV | | |

Yuki Satake and Hiroshi Unno | Propositional Dynamic Logic for Higher-Order Functional Programs | CAV | | Jul 14 11:00 |

Grigory Fedyukovich, Yueling Zhang and Aarti Gupta | Syntax-Guided Termination Analysis | CAV | | Jul 14 11:15 |

Hazem Torfah, Bernd Finkbeiner and Christopher Hahn | Model Checking Quantitative Hyperproperties | CAV | | Jul 14 11:30 |

Lauren Pick, Grigory Fedyukovich and Aarti Gupta | Exploiting Synchrony and Symmetry in Relational Verification | CAV | | Jul 14 11:45 |

Lucas Cordeiro, Pascal Kesseli, Daniel Kroening, Peter Schrammel and Marek Trtik | JBMC: A Bounded Model Checking Tool for Verifying Java Bytecode | CAV | | Jul 14 12:00 |

Kenneth McMillan | Eager Abstraction for Symbolic Model Checking | CAV | | Jul 14 12:15 |

Gagandeep Singh, Markus Püschel and Martin Vechev | Fast Numerical Program Analysis with Reinforcement Learning | CAV | | Jul 14 15:00 |

Anna Becchi and Enea Zaffanella | A Direct Encoding for NNC Polyhedra | CAV | | Jul 14 15:15 |

S. Akshay, Supratik Chakraborty, Shubham Goel, Sumith Kulal and Shetal Shah | What’s hard about Boolean Functional Synthesis? | CAV | | Jul 14 16:00 |

Alessandro Abate, Cristina David, Pascal Kesseli, Daniel Kroening and Elizabeth Polgreen | Counterexample Guided Inductive Synthesis Modulo Theories | CAV | | Jul 14 16:15 |

Bernd Finkbeiner, Leander Tentrup, Marvin Stenger, Philip Lukert and Christopher Hahn | Synthesizing Reactive Systems from Hyperproperties | CAV | | Jul 14 16:30 |

Daniel J. Fremont and Sanjit A. Seshia | Reactive Control Improvisation | CAV | | Jul 14 16:45 |

Aws Albarghouthi and Justin Hsu | Constraint-Based Synthesis of Coupling Proofs | CAV | | Jul 14 17:00 |

Chuchu Fan, Umang Mathur, Sayan Mitra and Mahesh Viswanathan | Controller Synthesis Made Real: Reach-avoid Specifications and Linear Dynamics | CAV | | Jul 14 17:15 |

Suguman Bansal, Kedar Namjoshi and Yaniv Sa'Ar | Synthesis Of Asynchronous Reactive Programs From Temporal Specifications | CAV | | Jul 14 17:30 |

Qinheping Hu and Loris D'Antoni | Syntax Guided Synthesis with Quantitative Syntactic Objectives | CAV | | Jul 14 17:45 |

Xinyu Wang, Greg Anderson, Isil Dillig and Ken McMillan | Learning Abstractions for Program Synthesis | CAV | | Jul 15 10:00 |

George Argyros and Loris D'Antoni | The Learnability of Symbolic Automata | CAV | | Jul 15 10:15 |

Hui Kong, Ezio Bartocci and Tom Henzinger | Reachable Set Over-approximation for Nonlinear Systems Using Piecewise Barrier Tubes | CAV | | Jul 15 11:00 |

Goran Frehse, Mirco Giacobbe and Thomas Henzinger | Space-time Interpolants | CAV | | Jul 15 11:15 |

Michael Emmi and Constantin Enea | Monitoring Weak Consistency | CAV | | Jul 15 11:30 |

Yijun Feng, Joost-Pieter Katoen, Haokun Li, Bican Xia and Naijun Zhan | Monitoring CTMCs By Multi-Clock Timed Automata | CAV | | Jul 15 11:45 |

Frederik M. Bønneland, Peter Gjøl Jensen, Kim Guldstrand Larsen, Marco Muñiz and Jiri Srba | Start Pruning When Time Gets Urgent: Partial Order Reduction for Timed Systems | CAV | | Jul 15 12:00 |

Ezio Bartocci, Roderick Bloem, Dejan Nickovic and Franz Roeck | A Counting Semantics for Monitoring LTL Specifications over Finite Traces | CAV | | Jul 15 12:15 |

Jan Kretinsky, Tobias Meggendorfer, Salomon Sickert and Christopher Ziegler | Rabinizer 4: From LTL to Your Favourite Deterministic Automaton | CAV | | Jul 15 14:00 |

Philipp J. Meyer, Salomon Sickert and Michael Luttenberger | Strix: Explicit Reactive Synthesis Strikes Back! | CAV | | Jul 15 14:15 |

Aina Niemetz, Mathias Preiner, Clifford Wolf and Armin Biere | BTOR2, BtorMC and Boolector 3.0 | CAV | | Jul 15 14:30 |

Marco Eilers and Peter Müller | Nagini: A Static Verifier for Python | CAV | | Jul 15 14:45 |

Michael Blondin, Javier Esparza and Stefan Jaax | Peregrine: A Tool for the Analysis of Population Protocols | CAV | | Jul 15 15:00 |

Milan Ceska, Jiri Matyas, Vojtech Mrazek, Lukas Sekanina, Zdenek Vasicek and Tomas Vojnar | ADAC: Automated Design of Approximate Circuits | CAV | | Jul 15 15:15 |

Edon Kelmendi, Julia Krämer, Jan Kretinsky and Maximilian Weininger | Value Iteration for Simple Stochastic Games: Stopping Criterion and Learning Algorithm | CAV | | Jul 15 16:00 |

Tim Quatmann and Joost-Pieter Katoen | Sound Value Iteration | CAV | | Jul 15 16:15 |

Weichao Zhou and Wenchao Li | Safety-Aware Apprenticeship Learning | CAV | | Jul 15 16:30 |

Qiyi Tang and Franck van Breugel | Deciding Probabilistic Bisimilarity Distance One for Labelled Markov Chains | CAV | | Jul 15 16:45 |

Hannah Arndt, Christina Jansen, Joost-Pieter Katoen, Christoph Matheja and Thomas Noll | Let this Graph be your Witness! An Attestor for Verifying Java Pointer Programs | CAV | | Jul 16 09:00 |

Mostafa Hassan, Caterina Urban, Marco Eilers and Peter Müller | MaxSMT-Based Type Inference for Python 3 | CAV | | Jul 16 09:15 |

Andrew Gacek, John Backes, Michael Whalen, Lucas Wagner and Elaheh Ghassabani | The JKind Model Checker | CAV | | Jul 16 09:30 |

Vincent Cheval, Steve Kremer and Itsaka Rakotonirina | The DEEPSEC prover | CAV | | Jul 16 09:45 |

Jianwen Li, Rohit Dureja, Geguang Pu, Kristin Yvonne Rozier and Moshe Vardi | SimpleCAR: An Efficient Bug-Finding Tool Based On Approximate Reachability | CAV | | Jul 16 10:00 |

Dmitry Blotsky, Federico Mora, Murphy Berzish, Yunhui Zheng, Ifaz Kabir and Vijay Ganesh | StringFuzz: A Fuzzer for String Solvers | CAV | | Jul 16 10:15 |

Jérôme Dohrau, Alexander J Summers, Caterina Urban, Severin Münger and Peter Müller | Permission Inference for Array Programs | CAV | | Jul 16 12:00 |

Patrick Cousot, Roberto Giacobazzi and Francesco Ranzato | Program Analysis is Harder than Verification: A Computability Perspective | CAV | | Jul 16 12:15 |

Suguman Bansal, Swarat Chaudhuri and Moshe Vardi | Automata vs Linear-Programming Discounted-Sum Inclusion | CAV | | Jul 17 09:00 |

Matthew Bauer, Rohit Chadha, Mahesh Viswanathan and Prasad Sistla | Model checking indistinguishability of randomized security protocols | CAV | | Jul 17 09:15 |

Weikun Yang, Yakir Vizel, Pramod Subramanyan, Aarti Gupta and Sharad Malik | Lazy Self-Composition for Security Verification | CAV | | Jul 17 09:30 |

Jun Zhang, Pengfei Gao, Fu Song and Chao Wang | SCInfer: Refinement-based Verification of Software Countermeasures against Side-Channel Attacks | CAV | | Jul 17 09:45 |

Krishnendu Chatterjee, Monika Henzinger, Veronika Loitzenbauer, Simin Oraee and Viktor Toman | Symbolic Algorithms for Graphs and Markov Decision Processes with Fairness Objectives | CAV | | Jul 17 10:00 |

Tom van Dijk | Attracting Tangles to Solve Parity Games | CAV | | Jul 17 10:15 |

Soonho Kong, Armando Solar-Lezama and Sicun Gao | Delta-Decision Procedures for Exists-Forall Problems over the Reals | CAV | | Jul 17 11:00 |

Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark Barrett and Cesare Tinelli | Solving Quantified Bit-Vectors using Invertibility Conditions | CAV | | Jul 17 11:15 |

Markus N. Rabe, Leander Tentrup, Cameron Rasmussen and Sanjit A. Seshia | Understanding and Extending Incremental Determinization for 2QBF | CAV | | Jul 17 11:30 |

Robert Robere, Antonina Kolokolova and Vijay Ganesh | The Proof Complexity of SMT Solvers | CAV | | Jul 17 11:45 |

Benjamin Farinier, Sebastien Bardin, Richard Bonichon and Marie-Laure Potet | Model Generation for Quantified Formulas: A Taint-Based Approach | CAV | | Jul 17 12:00 |

Xinhao Yuan, Junfeng Yang and Ronghui Gu | Partial Order Aware Concurrency Sampling | CAV | | Jul 17 14:00 |

Ahmed Bouajjani, Constantin Enea, Suha Orhun Mutluergil and Serdar Tasiran | Reasoning About TSO Programs Using Reduction and Abstraction | CAV | | Jul 17 14:15 |

Huyen T.T. Nguyen, Cesar Rodriguez, Marcelo Sousa, Camille Coti and Laure Petrucci | Quasi-Optimal Partial Order Reduction | CAV | | Jul 17 14:30 |

Ahmed Bouajjani, Constantin Enea, Kailiang Ji and Shaz Qadeer | On the Completeness of Verifying Message Passing Programs under Bounded Asynchrony | CAV | | Jul 17 14:45 |

Elvira Albert, Miguel Gomez-Zamalloa, Miguel Isabel and Albert Rubio | Constrained Dynamic Partial Order Reduction | CAV | | Jul 17 15:00 |

Mark Tullsen, Lee Pike, Nathan Collins and Aaron Tomb | Formal Verification of a Vehicle-to-Vehicle (V2V) Messaging System | CAV | | Jul 17 16:00 |

Andrey Chudnov, Nathan Collins, Byron Cook, Josiah Dodds, Brian Huffman, Colm MacCarthaigh, Stephen Magill, Eric Mertens, Eric Mullen, Serdar Tasiran, Aaron Tomb and Edwin Westbrook | Continuous formal verification of Amazon s2n | CAV | | Jul 17 16:15 |

Daniel Schemmel, Julian Büning, Oscar Soria Dustmann, Thomas Noll and Klaus Wehrle | Symbolic Liveness Analysis of Real-World Software | CAV | | Jul 17 16:30 |

Byron Cook, Kareem Khazem, Daniel Kroening, Serdar Tasiran, Michael Tautschnig and Mark R. Tuttle | Model Checking Boot Code from AWS Data Centers | CAV | | Jul 17 16:45 |

Taolue Chen, Jinlong He, Fu Song, Guozhen Wang, Zhilin Wu and Jun Yan | Android Stack Machine | CAV | | Jul 17 17:00 |

Christoph Walther | Formally Verified Montgomery Multiplication | CAV | | Jul 17 17:15 |

Eric Goubault, Sylvie Putot and Lorenz Sahlman | Inner and Outer Approximating Flowpipes for Delay Differential Equations | CAV | | Jul 17 17:30 |

David Langworthy | TLA+ in Engineering Systems – Quinceañera | TLA | | |

Valentin Schneider | Modeling Virtual Machines and Interrupts in TLA+ & PlusCal | TLA | | |

William Schultz | An Animation Module For TLA+ | TLA | | |

Igor Konnov, Jure Kukovec and Thanh Hai Tran | BMCMT: Bounded Model Checking of TLA+ Specifications with SMT | TLA | | |

Stefan Resch | Applying TLA+ in a Safety-Critical Railway Project | TLA | | |

Markus Kuppe | State Space Explosion or: How To Fight An Uphill Battle | TLA | | |

Ioannis Filippidis and Richard M. Murray | Proving properties of a minimal covering algorithm | TLA | | |

Yanhong A. Liu, Scott D. Stoller, Saksham Chand and Xuetian Weng | Invariants in Distributed Algorithms | TLA | | |

Thorsten Ehlers and Dirk Nowotka | Tuning Parallel SAT Solvers | POS | | Jul 07 09:00 |

Anastasia Leventi-Peetz, Oliver Zendel, Werner Lennartz and Kai Weber | CryptoMiniSat Parameter-Optimization for Solving Cryptographic Instances | POS | | Jul 07 09:30 |

Adrian Rebola Pardo and Armin Biere | Two flavors of DRAT | POS | | Jul 07 11:00 |

Michał Karpiński and Marek Piotrów | Competitive Sorter-based Encoding of PB-Constraints into SAT | POS | | Jul 07 11:30 |

Markus Iser and Carsten Sinz | A Problem Meta-Data Library for Research in SAT | POS | | Jul 07 16:00 |

Armin Biere and Marijn Heule | The Effect of Scrambling CNFs | POS | | Jul 07 16:30 |

Richard Wallace | Partial (Neighbourhood) Singleton Arc Consistency for Constraint Satisfaction Problems | RCRA | | Jul 13 14:22 |

Neng-Fa Zhou and Håkan Kjellerstrand | Encoding PB Constraints into SAT via Binary Adders and BDDs -- Revisited | RCRA | | Jul 13 14:44 |

Slimane Abou-Msabah, Ahmed Riadh Baba Ali and Basma SAGER | An Enhanced Genetic Algorithm with the BLF2G Guillotine Placement Heuristic for the Orthogonal Cutting-Stock Problem | RCRA | | Jul 13 12:06 |

Marco Baioletti, Alfredo Milani and Valentino Santucci | Algebraic Crossover Operators for Permutations | RCRA | | Jul 13 11:44 |

Mauro Vallati | On the Configuration of SAT Formulae | RCRA | | Jul 13 15:06 |

Giovanni Amendola, Carmine Dodaro, Wolfgang Faber and Francesco Ricca | Externally Supported Models for Efficient Computation of Paracoherent Answer Sets | RCRA | | Jul 13 11:22 |

Marco Gavanelli, Maddalena Nonato, Andrea Peano and Davide Bertozzi | Logic Programming approaches for routing fault-free and maximally-parallel Wavelength Routed Optical Networks on Chip (Application paper) | RCRA | | Jul 13 10:06 |

Richard Wallace | Replaceability for constraint satisfaction problems: Algorithms, Inferences, and Complexity Patterns | RCRA | | Jul 13 14:00 |

Angelo Oddi and Riccardo Rasconi | Greedy Randomized Search for Scalable Compilation of Quantum Circuits | RCRA | | Jul 13 09:44 |

Paul Tarau | Shaving with Occam's Razor: Deriving Minimalist Theorem Provers for Minimal Logic | RCRA | | Jul 13 11:00 |

Toni Mancini, Enrico Tronci, Agostino Scialanca, Filiberto Lanciotti, Alberto Finzi, Riccardo Guarneri and Silvia Di Pompeo | Optimal Fault-Tolerant Placement of Relay Nodes in a Mission Critical Wireless Network | RCRA | | Jul 13 09:22 |

Toni Mancini, Federico Mari, Annalisa Massini, Igor Melatti, Ivano Salvo, Stefano Sinisi, Enrico Tronci, Rainald Ehrig, Susanna Röblitz and Brigitte Leeners | Computing Personalised Treatments through In Silico Clinical Trials. A Case Study on Downregulation in Assisted Reproduction. | RCRA | | Jul 13 09:00 |

Paventhan Vivekanandan | A Homotopical Approach to Cryptography | FCS | | Jul 08 15:00 |

Alexandre Debant, Stephanie Delaune and Cyrille Wiedling | Proving physical proximity using symbolic models | FCS | | Jul 08 11:30 |

Musab A. Alturki, Max Kanovich, Tajana Ban Kirigin, Vivek Nigam, Andre Scedrov and Carolyn Talcott | Statistical Model Checking of Guessing and Timing Attacks on Distance-bounding Protocols | FCS | | Jul 08 12:00 |

Alix Trieu | A Study on the Preservation on Cryptographic Constant-Time Security in the CompCert Compiler | FCS | | Jul 08 14:00 |

Daniel Dougherty, Joshua Guttman and John Ramsdell | Homomorphisms and Minimality for Enrich-by-Need Security Analysis | FCS | | Jul 08 14:30 |

Luca Arnaboldi and Charles Morisset | LISA: Predicting the Impact of DoS Attacks on Real-World Low Power IoT Systems | FCS | | Jul 08 10:00 |

Jiaming Jiang, Rada Chirkova, Jon Doyle and Arnon Rosenthal | An Expressive, Flexible and Uniform Logical Formalism for Attribute-based Access Control | FCS | | Jul 08 11:00 |

Charlie Jacomme and Steve Kremer | An extensive formal analysis of multi-factor authentication protocols | CSF | | Jul 09 11:00 |

Bruno Blanchet | Composition Theorems for CryptoVerif and Application to TLS 1.3 | CSF | | Jul 09 11:30 |

Patrick Thomas Eugster, Giorgia Azzurra Marson and Bertram Poettering | A Cryptographic Look at Multi-Party Channels | CSF | | Jul 09 12:00 |

Ilia Lebedev, Kyle Hogan and Srini Devadas | Secure Boot and Remote Attestation in the Sanctum Processor | CSF | | |

Maxime Audinot, Sophie Pinchinat and Barbara Kordy | Guided design of attack trees: a system-based approach | CSF | | Jul 09 15:00 |

Marc Fischlin and Sogol Mazaheri | Self-Guarding Cryptographic Protocols against Algorithm Substitution Attacks | CSF | | Jul 10 09:00 |

Cécile Baritel-Ruet, François Dupressoir, Pierre-Alain Fouque and Benjamin Grégoire | Formal Security Proof of CMAC and its Variants | CSF | | Jul 10 09:30 |

Marc Fischlin, Christian Janson and Sogol Mazaheri | Backdoored Hash Functions: Immunizing HMAC and HKDF | CSF | | Jul 10 10:00 |

Helene Haagh, Aleksandr Karbyshev, Sabine Oechsner, Bas Spitters and Pierre-Yves Strub | Computer-aided proofs for multiparty computation with active security | CSF | | Jul 10 11:00 |

José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Hugo Pacheco, Vitor Pereira and Bernardo Portela | Enforcing ideal-world leakage bounds in real-world secret sharing MPC frameworks | CSF | | Jul 10 11:30 |

Baiyu Li and Daniele Micciancio | Symbolic security of garbled circuits | CSF | | Jul 10 12:00 |

Borzoo Bonakdarpour and Bernd Finkbeiner | The Complexity of Monitoring Hyperproperties | CSF | | Jul 10 14:00 |

Mckenna McCall, Hengruo Zhang and Limin Jia | Knowledge-based Security of Dynamic Secrets for Reactive Programs | CSF | | Jul 10 14:30 |

Andrey Chudnov and David Naumann | Assuming you know: epistemic semantics of relational annotations for expressive flow policies | CSF | | Jul 10 15:00 |

Everett Hildenbrandt, Manasvi Saxena, Nishant Rodrigues, Xiaoran Zhu, Philip Daian, Dwight Guth, Brandon Moore, Daejun Park, Yi Zhang, Andrei Stefanescu and Grigore Rosu | KEVM: A Complete Formal Semantics of the Ethereum Virtual Machine | CSF | | Jul 10 16:00 |

Hongxu Chen, Alwen Tiu, Zhiwu Xu and Yang Liu | A Permission-Dependent Type System for Secure Information Flow Analysis | CSF | | Jul 11 09:00 |

Vineet Rajani and Deepak Garg | Types for Information Flow Control: Labeling Granularity and Semantic Models | CSF | | Jul 11 09:30 |

Christian Müller, Helmut Seidl and Eugen Zalinescu | Inductive Invariants for Noninterference in Multi-agent Workflows | CSF | | Jul 11 10:00 |

Mario S. Alvim, Kostas Chatzikokolakis, Catuscia Palamidessi and Anna Pazii | Local Differential Privacy on Metric Spaces: optimizing the trade-off with utility | CSF | | |

Samuel Yeom, Irene Giacomelli, Matt Fredrikson and Somesh Jha | Privacy Risk in Machine Learning: Analyzing the Connection to Overfitting | CSF | | Jul 11 12:00 |

David Basin, Sasa Radomirovic and Lara Schmid | Alethea: A Provably Secure Random Sample Voting Protocol | CSF | | Jul 11 16:00 |

Véronique Cortier, Constantin Cătălin Dragan, François Dupressoir and Bogdan Warinschi | Machine-checked proofs for electronic voting: privacy and verifiability for Belenios | CSF | | Jul 11 16:30 |

Pasquale Malacaria, Mhr Khouzani, Corina Pasareanu, Quoc-Sang Phan and Kasper Luckow | Symbolic Side-Channel Analysis for Probabilistic Programs | CSF | | Jul 12 09:30 |

Gilles Barthe, Benjamin Grégoire and Vincent Laporte | Secure compilation of side-channel countermeasures: the case of cryptographic “constant-time” | CSF | | Jul 12 10:00 |

Vincent Cheval, Veronique Cortier and Mathieu Turuani | A little more conversation, a little less action, a lot more satisfaction: Global states in ProVerif. | CSF | | Jul 12 11:00 |

Jannik Dreier, Lucca Hirschi, Sasa Radomirovic and Ralf Sasse | Automated Unbounded Verification of Stateful Cryptographic Protocols with Exclusive OR | CSF | | Jul 12 11:30 |

Andreas Viktor Hess and Sebastian A. Mödersheim | A Typing Result for Stateful Protocols | CSF | | Jul 12 12:00 |

Sandra Alves | Termination of lambda-calculus linearization methods | Linearity/TLLA | | |

Iliano Cervesato, Sharjeel Khan, Giselle Reis and Dragisa Zunic | Formalization of Automated Trading Systems in a Concurrent Linear Framework | Linearity/TLLA | | Jul 08 17:20 |

Zeinab Galal | Towards a Functional Language for Species of Structures | Linearity/TLLA | | Jul 08 09:00 |

Masahito Hasegawa | From Linear Logic to Cyclic Sharing | Linearity/TLLA | | Jul 07 14:55 |

Jiaming Jiang, Harley Eades Iii and Valeria de Paiva | On the Lambek Calculus with an Exchange Modality | Linearity/TLLA | | Jul 07 09:20 |

Marie Kerjean and Yoann Dabrowski | Models of Linear Logic based on the Schwartz epsilon product | Linearity/TLLA | | Jul 08 12:00 |

Wen Kokke, Fabrizio Montesi and Marco Peressotti | Taking Linear Logic Apart | Linearity/TLLA | | Jul 07 12:00 |

Pierre Lescanne | How to count linear and affine closed lambda terms? | Linearity/TLLA | | Jul 08 09:20 |

Zhaohui Luo | Substructural Calculi with Dependent Types | Linearity/TLLA | | Jul 07 09:00 |

Roberto Maieli | The structure of non decomposable connectives of linear logic | Linearity/TLLA | | Jul 07 14:00 |

Giulio Manzonetto and Giulio Guerrieri | The Bang Calculus and the Two Girard's Translations | Linearity/TLLA | | Jul 07 09:55 |

Lê Thành Dũng Nguyễn and Thomas Seiller | Coherent interaction graphs: a nondeterministic geometry of interaction for MLL | Linearity/TLLA | | Jul 08 14:55 |

Lê Thành Dũng Nguyễn and Thomas Seiller | A semantic conjecture on second-order MLL and its complexity consequences (work in progress) | Linearity/TLLA | | Jul 08 17:00 |

Carlos Olarte, Valeria de Paiva, Elaine Pimentel and Giselle Reis | Benchmarking Linear Logic Translations | Linearity/TLLA | | Jul 08 14:20 |

Luca Paolini, Luca Roversi and Margherita Zorzi | Quantum programming made easy | Linearity/TLLA | | Jul 07 17:35 |

Luc Pellissier | Generalized generalized species of structure and resource modalities | Linearity/TLLA | | Jul 08 14:00 |

Luc Pellissier and Thomas Seiller | Entropy and Complexity Lower Bounds | Linearity/TLLA | | Jul 08 09:55 |

Paolo Pistone | Proof nets, coends and the Yoneda isomorphism | Linearity/TLLA | | Jul 07 17:00 |

Lionel Vaux Auclair and Federico Olimpieri | On the Taylor expansion of λ-terms and the groupoid structure of their rigid approximants | Linearity/TLLA | | Jul 07 14:20 |

Magnus O. Myreen | The CakeML Verified Compiler and Toolchain | PAAR | | Jul 19 09:00 |

Ahmed Bhayat and Giles Reger | Set of Support for Higher-Order Reasoning | PAAR | | Jul 19 14:30 |

Gabriel Ebner and Matthias Schlaipfer | Efficient translation of sequent calculus proofs into natural deduction proofs | PAAR | | Jul 19 14:00 |

Ullrich Hustadt, Cláudia Nalon and Clare Dixon | Evaluating Pre-Processing Techniques for the Separated Normal Form for Temporal Logics | PAAR | | Jul 19 15:00 |

Jens Otten | Proof Search Optimizations for Non-clausal Connection Calculi | PAAR | | Jul 19 11:30 |

Michael Rawson and Giles Reger | Dynamic Strategy Priority: Empower the strong and abandon the weak | PAAR | | Jul 19 10:00 |

Geoff Sutcliffe and Evgenii Kotelnikov | TFX: The TPTP Extended Typed First-order Form | PAAR | | Jul 19 12:00 |

Jørgen Villadsen, Anders Schlichtkrull and Andreas Halkjær From | A Verified Simple Prover for First-Order Logic | PAAR | | Jul 19 11:00 |

Karine Even-Mendoza, Sepideh Asadi, Antti Hyvärinen, Hana Chockler and Natasha Sharygina | Lattice-Based Refinement in Bounded Model Checking | VSTTE | | Jul 18 12:00 |

Jan Steffen Becker | Analyzing Consistency of Formal Requirements | AVOCS | | Jul 18 16:00 |

Claire Dross, Guillaume Foliard, Théo Jouanny, Lionel Matias, Stuart Matthews, Jean-Marc Mota, Yannick Moy, Pascal Pignard and Romain Soulat | Climbing the Software Assurance Ladder - Practical Formal Verification for Reliable Software | AVOCS | | Jul 19 11:30 |

Rebeka Farkas, Tamás Tóth, Ákos Hajdu and András Vörös | Backward reachability analysis for timed automata with data variables | AVOCS | | Jul 18 11:30 |

Radu Iosif and Cristina Serban | An Entailment Checker for Separation Logic with Inductive Definitions | AVOCS | | Jul 18 12:00 |

Najes Jomaa, Paolo Torrini, David Nowak, Gilles Grimaud and Samuel Hym | Proof-Oriented Design of a Separation Kernel with Minimal Trusted Computing Base | AVOCS | | Jul 19 16:30 |

Eduard Kamburjan | Detecting Deadlocks in Formal System Models with Condition Synchronization | AVOCS | | Jul 18 11:00 |

Christophe Limbrée and Charles Pecheur | A Framework for the Formal Verification of Networks of Railway Interlockings - Application to the Belgian Railways | AVOCS | | Jul 19 12:00 |

Eric Madelaine, Simon Bliutze, Xudong Qin and Min Zhang | Using SMT engine to generate Symbolic Automata | AVOCS | | Jul 19 11:00 |

Jessica Petrasch, Jan-Hendrik Oepen, Sebastian Krings and Moritz Gericke | Writing a Model Checker in 80 Days: Reusable Libraries and Custom Implementation | AVOCS | | Jul 18 17:00 |

Nicolas Schnepf, Rémi Badonnel, Abdelkader Lahmadi and Stephan Merz | Rule-Based Synthesis of Chains of Security Functions for Software-Defined Networks | AVOCS | | Jul 19 16:00 |

Matt Webster, Michael Breza, Clare Dixon, Michael Fisher and Julie McCann | Formal Verification of Synchronisation, Gossip and Environmental Effects for Critical IoT Systems | AVOCS | | Jul 18 16:30 |

Anuj Dawar and Erich Grädel | Preface | LICS | | |

Michael Blondin, Javier Esparza, Stefan Jaax and Antonin Kučera | Black Ninjas in the Dark: Formal Analysis of Population Protocols | LICS | | |

Thierry Coquand | Inner Models of Univalence | LICS | | |

Peter O'Hearn | Continuous Reasoning: Scaling the Impact of Formal Methods | LICS | | |

Ki Yung Ahn, Ross Horne, Shang-Wei Lin and Alwen Tiu | Quasi-Open Bisimilarity with Mismatch is Intuitionistic | LICS | | Jul 09 15:00 |

S. Akshay, Blaise Genest and Nikhil Vyas | Distribution-based objectives for Markov Decision Processes | LICS | | Jul 10 15:40 |

Joel Allred and Ulrich Ultes-Nitsche | A Simple and Optimal Complementation Algorithm for Büchi Automata | LICS | | Jul 09 16:20 |

Robert Atkey | The Syntax and Semantics of Quantitative Type Theory | LICS | | Jul 11 12:20 |

Albert Atserias and Joanna Ochremiak | Definable Ellipsoid Method, Sums-of-Squares Proofs, and the Isomorphism Problem | LICS | | Jul 12 12:20 |

Steve Awodey, Jonas Frey and Sam Speight | Impredicative Encodings of (Higher) Inductive Types | LICS | | Jul 10 11:00 |

Christel Baier, Nathalie Bertrand, Clemens Dubslaff, Daniel Gburek and Ocan Sankur | Stochastic Shortest Paths and Weight-Bounded Properties in Markov Decision Processes | LICS | | Jul 10 16:00 |

Valentin Blot and James Laird | Extensional and Intensional Semantic Universes: A Denotational Model of Dependent Types | LICS | | Jul 11 11:20 |

Manuel Bodirsky, Florent Madelaine and Antoine Mottet | A universal-algebraic proof of the complexity dichotomy for Monotone Monadic SNP | LICS | | Jul 11 11:20 |

Brandon Bohrer and André Platzer | A Hybrid, Dynamic Logic for Hybrid-Dynamic Information Flow | LICS | | Jul 12 15:00 |

Mikolaj Bojanczyk, Laure Daviaud and Krishna Shankara Narayanan | Regular and First Order List Functions | LICS | | Jul 09 12:20 |

Mikołaj Bojańczyk, Martin Grohe and Michał Pilipczuk | Definable decompositions for graphs of bounded linear cliquewidth | LICS | | Jul 09 11:00 |

Mikołaj Bojańczyk and Szymon Toruńczyk | On computability and tractability for infinite sets | LICS | | Jul 12 12:00 |

Udi Boker and Yariv Shaulian | Automaton-Based Criteria for Membership in CTL | LICS | | Jul 09 17:00 |

Filippo Bonchi, Fabio Gadducci, Aleks Kissinger, Pawel Sobocinski and Fabio Zanasi | Rewriting with Frobenius | LICS | | Jul 12 15:00 |

Filippo Bonchi, Pierre Ganty, Roberto Giacobazzi and Dusko Pavlovic | Sound up-to techniques and Complete abstract domains | LICS | | Jul 09 17:00 |

Tomas Brazdil, Krishnendu Chatterjee, Antonin Kucera, Petr Novotný, Dominik Velan and Florian Zuleger | Efficient Algorithms for Asymptotic Bounds on Termination Time in VASS | LICS | | Jul 12 14:40 |

Roberto Bruni, Hernan Melgratti and Ugo Montanari | Concurrency and Probability: Removing Confusion, Compositionally | LICS | | Jul 09 14:00 |

Ulrik Buchholtz, Floris van Doorn and Egbert Rijke | Higher Groups in Homotopy Type Theory | LICS | | Jul 09 12:00 |

Simon Castellan, Pierre Clairambault, Hugo Paquet and Glynn Winskel | The concurrent game semantics of Probabilistic PCF | LICS | | Jul 10 16:20 |

Yijia Chen and Jörg Flum | Tree depth, quantifier elimination, and quantifier rank | LICS | | Jul 10 11:40 |

Yijia Chen, Moritz Mueller and Keita Yokoyama | A parameterized halting problem, the linear time hierarchy, and the MRDP theorem | LICS | | Jul 09 12:00 |

Liron Cohen, Vincent Rahli, Mark Bickford and Robert Constable | Computability Beyond Church-Turing via Choice Sequences | LICS | | Jul 11 12:00 |

Thierry Coquand, Simon Huber and Anders Mörtberg | On Higher Inductive Types in Cubical Type Theory | LICS | | Jul 11 10:20 |

Karl Crary | Strong Sums in Focused Logic | LICS | | Jul 09 12:20 |

Raphaëlle Crubillé | Probabilistic stable functions on discrete cones are power series. | LICS | | Jul 12 14:00 |

Daniel Danielski and Emanuel Kieronski | Unary negation fragment with equivalence relations has the finite model property | LICS | | Jul 11 11:40 |

Luc Dartois, Emmanuel Filiot and Nathan Lhote | Logics for Word Transductions with Synthesis | LICS | | Jul 10 14:40 |

Ankush Das, Jan Hoffmann and Frank Pfenning | Work Analysis with Resource-Aware Session Types | LICS | | Jul 10 11:40 |

Vrunda Dave, Paul Gastin and Krishna S | Regular Transducer Expressions for Regular Transformations over infinite words | LICS | | Jul 09 17:40 |

Laure Daviaud, Marcin Jurdzinski and Ranko Lazic | A pseudo-quasi-polynomial algorithm for solving mean-payoff parity games | LICS | | Jul 09 14:20 |

Nadish de Silva | Logical paradoxes in quantum computation | LICS | | Jul 12 09:20 |

Romain Demangeon and Nobuko Yoshida | Causal Computational Complexity of Distributed Processes | LICS | | Jul 09 15:20 |

Arnaud Durand, Anselm Haak and Heribert Vollmer | Model-Theoretic Characterizations of Boolean and Arithmetic Circuit Classes of Small Depth | LICS | | Jul 10 11:20 |

Adrien Durier, Daniel Hirschkoff and Davide Sangiorgi | Eager Functions as Processes | LICS | | Jul 09 14:40 |

Clovis Eberhart and Tom Hirschowitz | What's in a game? A theory of game models | LICS | | Jul 10 15:40 |

Javier Esparza, Jan Kretinsky and Salomon Sickert | One Theorem to Rule Them All: A Unified Translation of LTL into $\omega$-Automata | LICS | | Jul 09 16:00 |

Thomas Ferrère, Thomas A Henzinger and N Ege Sarac | A Theory of Register Monitors | LICS | | Jul 12 14:20 |

Diego Figueira and M. Praveen | Playing with Repetitions in Data Words Using Energy Games | LICS | | Jul 09 15:00 |

Nathanaël Fijalkow | The State Complexity of Alternating Automata | LICS | | Jul 09 16:40 |

Emmanuel Filiot, Raffaella Gentilini and Jean-Francois Raskin | Rational Synthesis Under Imperfect Information | LICS | | Jul 09 14:40 |

Dror Fried, Axel Legay, Joel Ouaknine and Moshe Y Vardi | Sequential Relational Decomposition | LICS | | Jul 09 11:40 |

Dan Frumin, Robbert Krebbers and Lars Birkedal | ReLoC: A Mechanised Relational Logic for Fine-Grained Concurrency | LICS | | Jul 09 14:20 |

Francesco Gavazzo | Quantitative Behavioural Reasoning for Higher-order Effectful Programs: Applicative Distances | LICS | | Jul 12 09:00 |

Guillaume Geoffroy | Classical realizability as a classifier for nondeterminism | LICS | | Jul 10 12:20 |

Neil Ghani, Jules Hedges, Viktor Winschel and Philipp Zahn | Compositional game theory | LICS | | Jul 09 15:20 |

Adrien Guatto | A Generalized Modality for Recursion | LICS | | Jul 12 09:20 |

Grzegorz Głuch, Jerzy Marcinkowski and Piotr Ostropolski-Nalewaja | Can One Escape Red Chains? Regular Path Queries Determinacy is Undecidable. | LICS | | Jul 11 12:20 |

Amar Hadzihasanovic, Kang Feng Ng and Quanlong Wang | Two complete axiomatisations of pure-state qubit quantum computing | LICS | | Jul 12 10:00 |

Michael Hahn, Andreas Krebs and Howard Straubing | Wreath Products of Distributive Forest Algebras | LICS | | Jul 10 12:00 |

Kuen-Bang Hou and Ulrik Buchholtz | Cellular Cohomology in Homotopy Type Theory | LICS | | Jul 09 11:20 |

Ehud Hrushovski, Joel Ouaknine, Amaury Pouly and James Worrell | Polynomial Invariants for Affine Programs | LICS | | Jul 10 10:00 |

Dominic Hughes | Unification nets: canonical proof net quantifiers | LICS | | Jul 10 14:40 |

Pawel Idziak and Jacek Krzaczkowski | Satisfiability in multi-valued circuits | LICS | | Jul 11 12:00 |

Emmanuel Jeandel, Simon Perdrix and Renaud Vilmart | A Complete Axiomatisation of the ZX-Calculus for Clifford+T Quantum Mechanics | LICS | | Jul 12 09:40 |

Emmanuel Jeandel, Simon Perdrix and Renaud Vilmart | Diagrammatic Reasoning beyond Clifford+T Quantum Mechanics | LICS | | Jul 12 10:20 |

Bruce Kapron and Florian Steinberg | Type-two polynomial-time and restricted lookahead. | LICS | | Jul 10 15:00 |

Marie Kerjean | A Logical Account for Linear Partial Differential Equations | LICS | | Jul 10 14:20 |

Nicolai Kraus and Thorsten Altenkirch | Free Higher Groups in Homotopy Type Theory | LICS | | Jul 09 11:40 |

Jan Kretinsky and Tobias Meggendorfer | Conditional Value-at-Risk for Reachability and Mean Payoff in Markov Decision Processes | LICS | | Jul 10 16:20 |

Antti Kuusisto and Carsten Lutz | Weighted model counting beyond two-variable logic | LICS | | Jul 11 11:00 |

Olivier Laurent | Around Classical and Intuitionistic Linear Logics | LICS | | Jul 10 15:00 |

Karoliina Lehtinen | A modal mu perspective on solving parity games in quasipolynomial time. | LICS | | Jul 09 14:00 |

Thomas Leventis | Probabilistic Böhm Trees and Probabilistic Separation | LICS | | Jul 09 17:40 |

Bert Lindenhovius, Michael Mislove and Vladimir Zamdzhiev | Enriching a Linear/Non-linear Lambda Calculus: A Programming Language for String Diagrams | LICS | | Jul 09 16:00 |

Radu Mardare, Prakash Panangaden, Dexter Kozen, Dana Scott, Robert Furber and Giorgio Bacci | Boolean-Valued Semantics for Stochastic Lambda-Calculus | LICS | | Jul 09 16:40 |

Radu Mardare, Prakash Panangaden, Gordon Plotkin and Giorgio Bacci | An algebraic theory of Markov processes | LICS | | Jul 09 16:20 |

Paul-André Melliès | Ribbon tensorial logic | LICS | | Jul 12 15:20 |

Paul-André Melliès and Léo Stefanesco | An Asynchronous Soundness Theorem for Concurrent Separation Logic | LICS | | Jul 10 16:00 |

Matteo Mio | Riesz Modal Logic with Threshold Operators | LICS | | Jul 10 14:20 |

Étienne Miquey | A sequent calculus with dependent types for classical arithmetic | LICS | | Jul 11 10:00 |

Benoit Monin | An answer to the Gamma question | LICS | | Jul 10 10:20 |

Sean Moss and Tamara von Glehn | Dialectica models of type theory | LICS | | Jul 11 11:00 |

Koko Muroya, Wai-Tak Cheung and Dan Ghica | The Geometry of Computation-Graph Abstraction | LICS | | Jul 12 10:00 |

Yoji Nanjo, Hiroshi Unno, Eric Koskinen and Tachio Terauchi | Dependent Temporal Effects and Fixpoint Logic for Verification | LICS | | Jul 11 11:40 |

Matthias Niewerth | MSO Queries on Trees: Enumerating Answers under Updates Using Forest Algebras | LICS | | Jul 10 12:20 |

Andreas Nuyts and Dominique Devriese | Degrees of Relatedness - A Unified Framework for Parametricity, Irrelevance, Ad Hoc Polymorphism, Intersections, Unions and Algebra in Dependent Type Theory | LICS | | Jul 12 10:20 |

Michał Pilipczuk, Sebastian Siebertz and Szymon Toruńczyk | Parameterized circuit complexity of model-checking on sparse structures | LICS | | Jul 09 11:20 |

Michał Pilipczuk, Sebastian Siebertz and Szymon Toruńczyk | On the number of types in sparse graphs | LICS | | Jul 10 11:00 |

Maciej Piróg, Tom Schrijvers, Nicolas Wu and Mauro Jaskelioff | Syntax and Semantics for Operations with Scopes | LICS | | Jul 12 14:40 |

André Platzer and Yong Kiam Tan | Differential Equation Axiomatization: The Impressive Power of Differential Ghosts | LICS | | Jul 12 15:20 |

Damien Pous and Valeria Vignudelli | Allegories: decidability and graph homomorphisms | LICS | | Jul 12 14:20 |

Thomas Powell | A functional interpretation with state | LICS | | Jul 12 09:40 |

Colin Riba and Pierre Pradic | LMSO: A Curry-Howard Approach to Church's Synthesis via Linear Logic | LICS | | Jul 10 14:00 |

Benjamin Sherman, Luke Sciarappa, Michael Carbin and Adam Chlipala | Computable decision-making on the reals and other spaces via partiality and nondeterminism | LICS | | Jul 12 14:00 |

Kristina Sojakova and Patricia Johann | A General Framework for Relational Parametricity | LICS | | Jul 10 12:00 |

Jonathan Sterling and Robert Harper | Guarded Computational Type Theory | LICS | | Jul 10 11:20 |

Takeshi Tsukada, Kazuyuki Asada and Luke Ong | Species, Profunctors and Taylor Expansion Weighted by SMCC--A Unified Framework for Modelling Nondeterministic, Probabilistic and Quantum Programs-- | LICS | | Jul 12 09:00 |

Pierre Vial | Every λ-Term is Meaningful for the Infinitary Relational Model | LICS | | Jul 09 17:20 |

Paul Wild, Lutz Schröder, Dirk Pattinson and Barbara König | A van Benthem Theorem for Fuzzy Modal Logic | LICS | | Jul 10 14:00 |

Noam Zeilberger | A theory of linear typings as flows on 3-valent graphs | LICS | | Jul 09 11:00 |

Georg Zetzsche | PTL-separability and closures for WQOs on words | LICS | | Jul 09 17:20 |

Patrick Bahr, Bassel Mannaa and Rasmus Ejlers Møgelberg | What makes guarded types tick? | PARIS | | Jul 07 17:15 |

Florian Bruse, Martin Lange and Etienne Lozes | Collapses of Fixpoint Alternation Hierarchies in Low Type-Levels of Higher-Order Fixpoint Logic | PARIS | | Jul 07 11:45 |

David Cerna and Michael Lettmann | Towards the Automatic Construction of Schematic Proofs | PARIS | | Jul 07 14:45 |

Anupam Das | On the logical complexity of cyclic arithmetic | PARIS | | Jul 08 16:45 |

Yue Li and Ekaterina Komendantskaya | Coinductive Uniform Proofs: An Extended Abstract | PARIS | | Jul 08 11:45 |

Rémi Nollet | Local validity for circular proofs in linear logic with fixed points | PARIS | | Jul 07 11:00 |

Colin Riba and Pierre Pradic | LMSO: A Curry-Howard Approach to Church’s Synthesis via Linear Logic | PARIS | | Jul 08 11:00 |

Reuben Rowe and Liron Cohen | Transitive Closure Logic: Infinitary and Cyclic Proof Systems | PARIS | | Jul 08 16:00 |

Sorin Stratulat | Useless Explicit Induction Reasoning | PARIS | | Jul 07 14:00 |

Joshua Blinkhorn, Olaf Beyersdorff and Luke Hinde | Size, Cost and Capacity: A Semantic Technique for Hard Random QBFs | PC | | |

Maria Bonet, Sam Buss, Alexey Ignatiev, Joao Marques-Silva and Antonio Morgado | On Dual-Rail Based MaxSAT Solving | PC | | Jul 08 17:30 |

Florent Capelli | Proof systems for #SAT based on restricted circuits | PC | | Jul 07 17:40 |

Judith Clymo | Short Proofs in QBF Expansion | PC | | |

Anupam Das | Towards theories for positive polynomial time and monotone proofs with extension | PC | | Jul 08 15:00 |

Mareike Dressler, Adam Kurpisz and Timo de Wolff | Optimization over the Boolean Hypercube via Sums of Nonnegative Circuit Polynomials | PC | | Jul 08 17:00 |

Emil Jeřábek | Bounded induction without parameters | PC | | |

Manuel Kauers and Martina Seidl | The Symmetry Rule for Quantified Boolean Formulas | PC | | |

Alexander Knop | Branching Program Complexity of Canonical Search Problems and Proof Complexity of Formulas | PC | | Jul 07 15:00 |

Antonina Kolokolova | Complexity of expander-based reasoning and the power of monotone proofs | PC | | Jul 08 14:30 |

Barnaby Martin, Stefan Dantchev and Nicola Galesi | Resolution and the binary encoding of combinatorial principles | PC | | Jul 07 17:00 |

Fedor Part and Iddo Tzameret | Resolution with Counting: Different Moduli and Tree-Like Lower Bounds | PC | | Jul 07 17:20 |

Calin Belta | Formal Synthesis of Control Strategies for Dynamical Systems | VaVAS | | |

Radu Calinescu and Saud Yonbawi | Towards a Hierarchical-Control Architecture for Distributed Autonomous Systems (Extended Abstract - Paper) | VaVAS | | Jul 18 10:00 |

Anna Lukina, Ashish Tiwari, Scott Smolka and Radu Grosu | Adaptive Neighborhood Resizing for Stochastic Reachability in Multi-Agent Systems | VaVAS | | Jul 18 11:00 |

Thai Son Hoang, Naoto Sato, Tomoyuki Myojin, Michael Butler, Yuichiroh Nakagawa and Hideto Ogawa | Policing Functions for Machine Learning Systems | VaVAS | | Jul 18 11:30 |

Julian Padget, Marina De Vos and Charlie Page | Social Consequence Engines (Abstract) | VaVAS | | Jul 18 12:00 |

Jérémie Guiochet | Trust me - I am autonomous | VaVAS | | |

Isidro Durazo-Cardenas, Andrew Starr and Tetsuo Tomiyama | Towards validation and verification of an autonomous railway inspection and repair system | VaVAS | | |

Ruben Giaquinta, Ruth Hoffmann, Murray Ireland, Alice Miller and Gethin Norman | Probabilistic Model Checking for Autonomous Agent Strategy Synthesis - Extended Abstract | VaVAS | | Jul 18 16:00 |

Mohammed Al-Nuaimi, Hongyang Qu and Sandor Veres | Towards a verifiable decision making framework for self-driving vehicles | VaVAS | | Jul 18 16:30 |

Gleifer Alves, Louise Dennis and Michael Fisher | Formalisation of the Rules of the Road for embedding into an Autonomous Vehicle Agent | VaVAS | | Jul 18 17:00 |

Florian Lier | Reproducibility in Robotics - The Big 5 Issues | VaVAS | | |

Alvaro Miyazawa, Ana Cavalcanti, Simon Foster, Wei Li, Pedro Ribeiro, Jon Timmis and Jim Woodcock | RoboTool: Modelling and Verification with RoboChart | VaVAS | | Jul 19 10:00 |

Bruno Lacerda, David Parker and Nick Hawes | Policy Generation with Probabilistic Guarantees for Long-term Autonomy of a Mobile Service Robot | VaVAS | | Jul 19 11:00 |

Mathias Fleury, Jasmin Christian Blanchette and Peter Lammich | A Verified SAT Solver with Watched Literals Using Imperative HOL (Extended Abstract) | Isabelle | | Jul 13 09:30 |

Andreas Lochbihler and Pascal Stoop | Lazy Algebraic Types in Isabelle/HOL | Isabelle | | Jul 13 10:00 |

Max W. Haslbeck and René Thiemann | Formal Verification of Bounds for the LLL Basis Reduction Algorithm | Isabelle | | Jul 13 11:00 |

Benedikt Stock, Abhik Pal, Maria Antonia Oprea, Yufei Liu, Malte Sophian Hassler, Simon Dubischar, Prabhat Devkota, Yiping Deng, Marco David, Bogdan Ciurezu, Jonas Bayer and Deepak Aryal | Hilbert Meets Isabelle: Formalisation of the DPRM Theorem in Isabelle | Isabelle | | Jul 13 11:30 |

Makarius Wenzel | Further Scaling of Isabelle Technology | Isabelle | | Jul 13 12:00 |

Andreas Halkjær From, Anders Schlichtkrull and Jørgen Villadsen | Drawing Trees | Isabelle | | |

Andreas Halkjær From, John Bruntse Larsen, Anders Schlichtkrull and Jørgen Villadsen | Substitutionless First-Order Logic: A Formal Soundness Proof | Isabelle | | Jul 13 16:00 |

Christian Sternagel | The remote_build Tool | Isabelle | | Jul 13 16:15 |

Yutaka Nagashima and Yilun He | PaMpeR: A Proof Method Recommendation System for Isabelle/HOL | Isabelle | | Jul 13 16:30 |

Joshua Bockenek, Peter Lammich, Yakoub Nemouchi and Burkhart Wolff | Using Isabelle/UTP for the Verification of Sorting Algorithms: A Case Study | Isabelle | | Jul 13 17:00 |

Eric Hehner | A Theory of Lazy Imperative Timing | REFINE | | Jul 18 16:30 |

Ian J. Hayes | Challenges of specifying concurrent program components | REFINE | | Jul 18 11:00 |

Mathieu Montin and Marc Pantel | Ordering strict partial orders to model behavioural refinement | REFINE | | Jul 18 12:00 |

Marwa Ben Abdelali, Lamia Labed Jilani, Wided Ghardallou and Ali Mili | Programming Without Refinement | REFINE | | Jul 18 11:30 |

Graeme Smith, Kirsten Winter and Robert Colvin | Correctness of Concurrent Objects under Weak Memory Models | REFINE | | Jul 18 10:00 |

Emil Sekerinski and Shucai Yao | Refining Santa: An Excercise in Efficient Synchronization | REFINE | | Jul 18 16:00 |

Cynthia Kop | Automatic Termination Analysis Using WANDA | HOR | | |

Naoki Kobayashi | On Two Kinds of Higher-Order Model Checking and Higher-Order Program Verification | HOR | | |

Pierre Vial | Some applications of quantitative types inside and outside type theory | HOR | | |

Maciej Bendkowski and Pierre Lescanne | Combinatorics of explicit substitutions (extended abstract) | HOR | | Jul 07 10:00 |

Federico Olimpieri | Normalization and Taylor expansion of lambda-terms | HOR | | Jul 07 16:00 |

Connor Smith | Orthogonality and sequentiality in substructural Linear HRSs | HOR | | Jul 07 12:00 |

Flavien Breuvart | Refining Properties of Filter Models: Sensibility, Approximability and Reducibility | HOR | | Jul 07 15:00 |

Damiano Mazza and Domenico Ruoppolo | The next 700 (type-theoretical) denotational models ? | HOR | | Jul 07 16:30 |

Davide Giacomo Cavezza | Heuristic-Based GR(1) Assumptions Refinement | DS-FM | | Jul 14 11:45 |

Georg Nührenberg | Formal verification of neural networks | DS-FM | | Jul 14 14:30 |

Dhriti Khanna | Analysis and Verification of Message Passing based Parallel Programs | DS-FM | | Jul 14 14:00 |

Simone Vuotto | Consistency Checking of Functional Requirements | DS-FM | | Jul 14 15:00 |

Peter Backeman, Aleksandar Zeljić, Philipp Ruemmer and Christoph M. Wintersteiger | The next 10^4 UppSAT Approximations | SMT | | Jul 12 11:30 |

Mohamed Iguernlala, Sylvain Conchon and Albin Coquereau | Alt-Ergo 2.2 | SMT | | Jul 12 12:00 |

Gergely Kovásznai, Csaba Biró and Balázs Erdélyi | Puli - A Problem-Specific OMT Solver | SMT | | Jul 12 15:00 |

Leonardo Alt and Christian Reitwiessner | SMT-based Compile-time Verification of Safety Properties for Smart Contracts | SMT | | Jul 12 16:00 |

Arie Gurfinkel, Sharon Shoham and Yakir Vizel | Discovering Universally Quantified Solutions for Constrained Horn Clauses | SMT | | Jul 13 14:00 |

Andrew Reynolds, Haniel Barbosa, Aina Niemetz, Andres Noetzli, Mathias Preiner, Clark Barrett and Cesare Tinelli | Rewrites for SMT Solvers using Syntax-Guided Enumeration | SMT | | Jul 12 17:00 |

Haniel Barbosa, Andrew Reynolds, Pascal Fontaine, Daniel El Ouraoui and Cesare Tinelli | Higher-Order SMT Solving | SMT | | Jul 13 10:00 |

François Bobot, Stephane Graham-Lengrand, Bruno Marre and Guillaume Bury | Centralizing Equality Reasoning in MCSAT | SMT | | Jul 13 11:00 |

Guillaume Bury, David Delahaye and Simon Cruanes | SMT Solving Modulo Tableau and Rewriting Theories | SMT | | Jul 12 16:30 |

Giles Reger and Martin Riener | What is the Point of an SMT-LIB Problem? | SMT | | Jul 13 14:30 |

Delia Kesner | Quantitative Types: from Foundations to Applications | ITRS | | |

Damiano Mazza | Polyadic Approximations and Intersection Types | ITRS | | |

Paweł Parys | Intersection Types for Unboundedness Problems | ITRS | | |

Federico Aschieri | Natural Deduction and Normalization Proofs for the Intersection Type Discipline | ITRS | | Jul 08 11:00 |

Giulio Guerrieri | Towards a Semantic Measure of the Execution Time in Call-by-Value lambda-Calculus | ITRS | | Jul 08 12:00 |

Olivier Laurent | Intersection Subtyping with Constructors | ITRS | | Jul 08 16:00 |

Simona Ronchi Della Rocca and Daniele Pautasso | Strong normalization of simple types through uniform intersection types. | ITRS | | Jul 08 11:30 |

Richard Statman | On sets of terms with a given intersection type | ITRS | | |

Pedro Ângelo and Mário Florido | Gradual Intersection Types | ITRS | | Jul 08 15:00 |

Thibaut Benjamin | Towards a fully formalized definition of syllepsis in weak higher categories | HDRA | | Jul 07 15:00 |

Cyrille Chenavier, Christophe Cordero and Samuele Giraudo | Generalizations of the associative operad and convergent rewrite systems | HDRA | | Jul 07 17:00 |

Antonin Delpeuch and Jamie Vicary | Normal forms for planar connected string diagrams | HDRA | | Jul 07 17:30 |

Benjamin Dupont | Termination in linear (2,2)-categories with braidings and duals | HDRA | | Jul 07 12:00 |

Amar Hadzihasanovic | Merge-bicategories: towards semi-strictification of higher categories | HDRA | | Jul 07 10:00 |

Nohra Hage | String data structures for Chinese monoids | HDRA | | Jul 07 16:30 |

Cédric Ho Thanh | The equivalence between opetopic sets and many-to-one polygraphs | HDRA | | Jul 07 11:00 |

Richard Statman | Minimal Bacus FP is Turing Complete | HDRA | | Jul 07 16:00 |

Pedro Tamaroff | Minimal models for monomial algebras | HDRA | | Jul 07 11:30 |

Lawrence Moss | Implementations of Natural Logics | ARQNL | | |

Giles Reger | Some thoughts about FOL-translations in Vampire | ARQNL | | |

Ahmad-Saher Azizi-Sultan | Pseudo-Propositional Logic | ARQNL | | Jul 18 15:00 |

Tomer Libal | A Simple Semi-automated Proof Assistant for First-order Modal Logics | ARQNL | | Jul 18 11:30 |

Daniel Mery and Didier Galmiche | Labelled Connection-based Proof Search for Multiplicative Intuitionistic Linear Logic | ARQNL | | Jul 18 12:00 |

Eugenio Orlandelli and Giovanna Corsi | Labelled calculi for QMLs with non-rigid and non-denoting terms | ARQNL | | Jul 18 11:00 |

Alexander Steen and Christoph Benzmüller | System Demonstration: The Higher-Order Prover Leo-III | ARQNL | | Jul 18 16:30 |

Wieger Wesselink and Tim Willemse | Evidence Extraction from Parameterised Boolean Equation Systems | ARQNL | | Jul 18 10:00 |