FLOC 2018: FEDERATED LOGIC CONFERENCE 2018

Authors	Title	Conference	Paper	Talk
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