Trisha Nowland and Simon BoagTowards a Logical Framework for Latent Variable ModellingWiLJul 08 16:30
Elaine PimentelA semantical view of sequent based systemsWiLJul 08 11:30
Cláudia Nalon and Daniella AngelosOn the Combination of Resolution and SAT Procedures for Modal Theorem-ProvingWiLJul 08 16:00
Liron Cohen and Ariel KellisonOn Expanding Standard Notions of ConstructivityWiLJul 08 11:00
Giselle ReisTowards a Playground for LogiciansWiLJul 08 15:00
Çigdem GencerAbout the unification type of topological logics over Euclidean spacesWiLJul 08 12:00
Ornela Dardha and Simon J. GayA New Linear Logic for Deadlock-Free Session-Typed Processes (Talk Abstract)WiLJul 08 10:15
Hanna Lachnitt, Christoph Benzmüller and Maximilian ClausEmbedding Intuitionistic Modal Logics in Higher-Order Logic. An Easy Task?WiLJul 08 16:15
Liron Cohen and Reuben RoweNon-well-founded proof system for Transitive Closure LogicWiLJul 08 15:15
Shufang Zhu, Geguang Pu and Moshe VardiFirst-Order vs. Second-Order Encodings for LTLf-to-Automata: An Extended AbstractWiLJul 08 10:00
Sonia Marin, Marianela Morales and Lutz StraßburgerDecomposing labelled proof theory for intuitionistic modal logicWiLJul 08 11:45
Ilias KotsireasHard Combinatorial Problems: A Challenge for SatisfiabilitySCSCJul 11 09:00
Alexander Cowen-Rivers and Matthew EnglandTowards Incremental Cylindrical Algebraic Decomposition in MapleSCSCJul 11 14:30
Rebecca Haehn, Gereon Kremer and Erika ÁbrahámEvaluation of Equational Constraints for CAD in SMT SolvingSCSCJul 11 15:00
Jan Horacek and Martin KreuzerRefutation of Products of Linear PolynomialsSCSCJul 11 16:00
Casey Mulligan, Russell Bradford, James H. Davenport, Matthew England and Zak TonksNon-linear Real Arithmetic Benchmarks derived from Automated Reasoning in EconomicsSCSCJul 11 14:00
Daniela Ritirc, Armin Biere and Manuel KauersA Practical Polynomial Calculus for Arithmetic Circuit VerificationSCSCJul 11 16:30
Meesum Syed Mohammad and Prathamesh T. V. H.Unknot Recognition Through Quantifier EliminationSCSCJul 11 17:00
John Abbott, Anna Maria Bigatti and Elisa PalezzatoNew in CoCoA-5.2.4 and CoCoALib-0.99570 for SC-SquareSCSCJul 11 11:25
Andreas Eggers, Matthias Stasch, Tino Teige, Tom Bienmüller and Udo BrockmeyerConstraint Systems from Traffic Scenarios for the Validation of Autonomous DrivingSCSCJul 11 10:05
Pascal Fontaine, Mizuhito Ogawa, Thomas Sturm, Van Khanh To and Xuan Tung VuWrapping Computer Algebra is Surprisingly Successful for Non-Linear SMTSCSCJul 11 11:00
Stephen A. ForrestSMT-like Queries in MapleSCSCJul 11 11:50
Tudor JebeleanTechniques for Natural-style Proofs in Elementary AnalysisSCSCJul 11 12:15
Jean-Christophe FilliâtreAuto-active verification using Why3's IDEF-IDE
Leo FreitasVDM at large: Modelling the EMVCo 2nd Generation KernelF-IDE
Sylvain Dailler, Claude Marché and Yannick MoyLightweight Interactive Proving inside an Automatic Program VerifierF-IDEJul 14 10:00
Makarius WenzelIsabelle/jEdit as IDE for domain-specific formal languages and informal text documentsF-IDEJul 14 16:00
Jan Bessai and Anna VasilevaUser Support for the Combinator Logic Synthesizer FrameworkF-IDEJul 14 11:00
Alexander Knüppel, Carsten Pardylla, Thomas Thüm and Ina SchaeferExperience Report on Formally Verifying Parts of OpenJDK's API with KeYF-IDEJul 14 15:00
Paolo Arcaini, Riccardo Melioli and Elvinia RiccobeneAsmetaF: a flattener for the ASMETA frameworkF-IDEJul 14 11:30
Rui Couto, José Creissac Campos, Nuno Macedo and Alcino CunhaImproving the Visualization of Alloy InstancesF-IDEJul 14 12:00
Spencer Park and Emil SekerinskiA Notebook Format for the Holistic Design of Embedded SystemsF-IDEJul 14 16:30
Devesh Bhatt, Anitha Murugesan, Brendan Hall, Hao Ren and Yogananda JeppuThe CLEAR Way To Transparent Formal MethodsF-IDEJul 14 17:00
Nathaniel Watson, Steve Reeves and Paolo MasciIntegrating user design and formal models within PVSio-WebF-IDEJul 14 17:30
Yu Wang, Nima Roohi, Mahesh Viswanathan, Geir E. Dullerud and Matthew WestStatistical Verification of PCTL Using Stratified Samples ADHSJul 11 14:50
Carlos Renato Vazquez, David Gómez-Gutiérrez and Antonio Ramirez-TrevinoObservability of Linear Hybrid Systems with Unknown Inputs and Discrete Dynamics Modeled by Petri NetsADHSJul 12 11:15
Tjorben Groß, Stephan Trenn and Andreas WirsenSwitch induced instabilities for stable power system DAE modelsADHSJul 11 17:00
Amanda Abreu, Romain Bourdais and Herve GueguenHierarchical Model Predictive Control for Building Energy Management of Hybrid Systems ADHSJul 12 16:35
André Marcorin de Oliveira, Vineeth Satheeskumar Varma, Romain Postoyan, Irinel Constantin Morarescu, Jamal Daafouz and Oswaldo Luiz V. CostaNetwork-Aware Design of State-Feedback Controllers for Linear Wireless Networked Control SystemsADHSJul 12 14:00
Irinel Constantin Morarescu, Vineeth Satheeskumar Varma, Lucian Busoniu and Samson LasaulceSpace-Time Budget Allocation for Marketing Over Social Networks ADHSJul 12 14:25
Hoang-Dung Tran, Weiming Xiang, Stanley Bak and Taylor T JohnsonReachability Analysis for One Dimensional Linear Parabolic Equation ADHSJul 12 10:50
Alina Eqtami and Antoine GirardSafety Control, a Quantitative Approach ADHSJul 12 14:25
Victor Dolk, Menno Lauret, Duarte Antunes, Patrick Anderson and Maurice HeemelsA switched system approach to optimize mixing of fluidsADHSJul 11 11:15
Bacem Ben Nasser, Michael Defoort, Mohamed Djemai and Taous-Meriem Laleg-KiratiRazumikhin-type Theorems on Practical Stability of Dynamic Equations on Time ScalesADHSJul 11 16:35
Ulrich FahrenbergHigher-Dimensional Timed Automata ADHSJul 11 17:00
Chuchu Fan, Yu Meng, Jürgen Maier, Ezio Bartocci, Sayan Mitra and Ulrich SchmidVerifying nonlinear analog and mixed-signal circuits with inputsADHSJul 12 17:00
Fatima Zohra Taousser, Michael Defoort, Mohamed Djemai and Seddik DjouadiStability of switched systems on non-uniform time domains with non commuting matricesADHSJul 11 11:40
Sadegh Soudjani and Rupak MajumdarConcentration of Measure for Chance-Constrained Optimization ADHSJul 13 11:40
Ivan Zapreev, Cees Verdier and Manuel Mazo Jr.Optimal Symbolic Controllers Determinization for BDD storage.ADHSJul 11 10:50
Alexandre Rocca, Marcelo Forets, Victor Magron, Eric Fanchon and Thao DangOccupation Measure Methods for Modelling and Analysis of Biological Hybrid Systems ADHSJul 12 14:00
Gabriella Fiore, Elena De Santis, Giordano Pola and Maria Domenica Di BenedettoOn Approximate Predictability of Metric Systems ADHSJul 12 11:40
Xiangyu Meng, Arian Houshmand and Christos G. CassandrasHybrid System Modeling of Multi-Agent Coverage Problems with Energy Depletion and Repletion ADHSJul 12 15:15
Brandon Bohrer, Adriel Luo, Xue An Chuang and Andre PlatzerCoasterX: A Case Study in Component-Driven Hybrid Systems Proof AutomationADHSJul 11 14:25
Yorai Wardi, Carla Seatzu and Magnus EgerstedtTracking Control via Variable-gain Integrator and Lookahead Simulation: Application to Leader-follower Multiagent NetworksADHSJul 12 14:50
Kengo Kido, Sean Sedwards and Ichiro HasuoBounding Errors Due to Switching Delays in Incrementally Stable Switched SystemsADHSJul 12 16:10
Ashok Krishnan, Mohasha Isuru Sampath, Yi Shyh Eddy Foo, Bhagyesh Patil and H. B. GooiMulti-Energy Scheduling Using a Hybrid Systems ApproachADHSJul 12 16:10
Marcell Vazquez-Chanlatte, Shromona Ghosh, Vasumathi Raman, Alberto Sangiovanni-Vincentelli and Sanjit SeshiaGenerating Dominant Strategies for Continuous Two-Player Zero-Sum Games ADHSJul 11 11:15
Abolfazl Lavaei, Sadegh Soudjani and Majid ZamaniCompositional Synthesis of Finite Abstractions for Continuous-Space Stochastic Control Systems: A Small-Gain Approach ADHSJul 13 10:50
Stanley BakT-Barrier Certificates: A Continuous Analogy to K-Induction ADHSJul 12 11:40
Yuriy Zacchia Lun, Jack Wheatley, Alessandro D'Innocenzo and Alessandro AbateApproximate Abstractions of Markov Chains with Interval Decision Processes ADHSJul 11 15:15
Adrien Le Coent, Laurent Fribourg and Jonathan VacherControl Synthesis for Stochastic Switched Systems Using the Tamed Euler Method ADHSJul 12 17:00
Adnane Saoud, Pushpak Jagtap, Majid Zamani and Antoine GirardCompositional Abstraction-based Synthesis for Cascade Discrete-Time Control SystemsADHSJul 11 11:40
Oscar Bulancea Lindvall, Petter Nilsson and Necmiye OzayNonuniform abstractions, refinement and controller synthesis with novel BDD encodingsADHSJul 11 12:05
Nathalie Margaret Cauchi and Alessandro AbateBenchmarks for Cyber-Physical Systems: A Modular Model Library for Building Automation Systems ADHSJul 11 14:00
Sofie Haesaert, Sadegh Soudjani and Alessandro AbateTemporal Logic Control of General Markov Decision Processes by Approximate Policy RefinementADHSJul 11 14:00
Murat Cubuktepe, Mohamadreza Ahmadi, Ufuk Topcu and Brandon HenceyCompositional Analysis of Hybrid Systems Defined Over Finite Alphabets ADHSJul 11 16:10
Marc Jungers, Antoine Girard and Mirko FiacchiniLanguage constrained stabilization of discrete- time switched linear systems: an LMI approachADHSJul 11 10:50
Henk A.P. Blom, Hao Ma and Bert G.J. BakkerInteracting Particle System-Based Estimation of Reach Probability for a Generalized Stochastic Hybrid System ADHSJul 11 14:25
Ronald Robert Paul van Nooijen and Alla G. KolechkinaA controlled sewer system should be treated as a sampled data system with eventsADHSJul 11 14:50
Julien Alexandre Dit Sandretto, Elliot Brendel and Alexandre ChapoutotAn Interval-Based Sliding Horizon Motion Planning Method ADHSJul 13 14:50
Shakiba Yaghoubi and Georgios FainekosFalsification of Temporal Logic Requirements Using Gradient Based Local Search in Space and Time ADHSJul 11 16:35
Benoît Legat, Paulo Tabuada and Raphaël M. JungersComputing Controlled Invariant Sets for Hybrid Systems with Applications to Model-Predictive Control ADHSJul 12 14:50
Sofie Haesaert, Petter Nilsson, Cristian-Ioan Vasile, Thakker Rohan, Ali-Akbar Agha-Mohammadi, Aaron Ames and Richard M. MurrayTemporal Logic Control of POMDPs Via Label-Based Stochastic Simulation Relations ADHSJul 13 11:15
Luan Nguyen, Bardh Hoxha, Taylor T Johnson and Georgios FainekosMission Planning for Multiple Vehicles with Temporal Specifications using UxASADHSJul 11 15:15
Kanishka Raj Singh, Yuhao Ding, Necmiye Ozay and Sze Zheng YongInput Design for Nonlinear Model Discrimination Via Affine Abstraction ADHSJul 12 12:05
Souradeep Dutta, Susmit Jha, Sriram Sankaranarayanan and Ashish TiwariLearning and Verification of Feedback Control Systems Using Feedforward Neural Networks ADHSJul 12 12:05
Ariadna Estrada and Ian M. MitchellControl Synthesis and Classification for Unicycle Dynamics Using the Gradient and Value Sampling Particle Filters ADHSJul 13 14:25
Hyejin Han and Ricardo SanfeliceSufficient Conditions for Temporal Logic Specifications in Hybrid Dynamical SystemsADHSJul 11 16:10
Tareq Hamadneh and Rafal WisniewskiAlgorithm for Bernstein Polynomial Control Design ADHSJul 13 14:00
Manish Goyal and Parasara Sridhar DuggiralaOn Generating A Variety of Unsafe Counterexamples for Linear Dynamical SystemsADHSJul 12 11:15
Nikolaos Athanasopoulos and Raphaël M. JungersOn invariance and reachability on semialgebraic sets for linear dynamicsADHSJul 11 12:05
Francesco Smarra, Achin Jain, Rahul Mangharam and Alessandro D'InnocenzoData-Driven Switched Affine Modeling for Model Predictive Control ADHSJul 12 15:15
Zohra Kader, Antoine Girard and Adnane SaoudSymbolic Models for Incrementally Stable Switched Systems with Aperiodic Time Sampling ADHSJul 12 16:35
Kwesi Rutledge, Sze Zheng Yong and Necmiye OzayOptimization-Based Design of Bounded-Error Estimators Robust to Missing DataADHSJul 12 10:50
Jean-Christophe FilliatreDeductive Program VerificationITP
Daniel GraysonVoevodsky's work on formalization of proofs and the foundations of mathematicsITP
John HarrisonMike Gordon: Tribute to a pioneer in theorem proving and formal verificationITP
Reto Achermann, Lukas Humbel, David Cock and Timothy RoscoePhysical addressing on real hardware in Isabelle/HOLITPJul 11 09:30
Abhishek Anand, Simon Boulier, Cyril Cohen, Matthieu Sozeau and Nicolas TabareauTowards Certified Meta-Programming with Typed Template-CoqITPJul 10 16:30
Andréia B. Avelar, Thaynara A. de Lima and André Luiz GaldinoFormalizing Ring Theory in PVS (short paper)ITPJul 11 17:00
Samuel Balco, Sabine Frittella, Giuseppe Greco, Alexander Kurz and Alessandra PalmigianoSoftware tool support for modular reasoning in modal logics of actionsITPJul 09 14:30
Callum Bannister, Peter Höfner and Gerwin KleinBackwards and Forwards with Separation LogicITPJul 10 14:00
Véronique Benzaken, Evelyne Contejean, Chantal Keller and Eunice MartinsA Coq formalisation of SQL’s execution enginesITPJul 10 15:00
Sylvain Boulmé and Alexandre MaréchalA Coq Tactic for Equality Learning in Linear ArithmeticITPJul 10 12:00
Venanzio Capretta and Colm BastonThe Coinductive Formulation of Common KnowledgeITPJul 09 15:00
Raphaël CauderlierTactics and certificates in Meta DeduktiITPJul 11 12:00
Jose Divasón, Sebastiaan Joosten, René Thiemann and Akihisa YamadaA Formalization of the LLL Basis Reduction AlgorithmITPJul 10 11:00
Christian Doczkal, Guillaume Combette and Damien PousA Formal Proof of the Minor-Exclusion Property for Treewidth-Two GraphsITPJul 12 09:00
Manuel Eberl, Max W. Haslbeck and Tobias NipkowVerified Analysis of Random Binary Tree StructuresITPJul 12 16:30
William Farmer, Jacques Carette and Patrick LaskowskiHOL Light QEITPJul 11 11:30
Denis Firsov, Richard Blair and Aaron StumpEfficient Mendler-Style Lambda-Encodings in CedilleITPJul 09 12:00
Yannick Forster, Edith Heiter and Gert SmolkaVerification of PCP-Related Computational Reductions in CoqITPJul 12 10:00
Zarathustra Goertzel, Jan Jakubuv, Stephan Schulz and Josef UrbanProofWatch: Watchlist Guidance for Large Theories in EITPJul 12 15:00
Jason Gross, Andres Erbsen and Adam ChlipalaReification by ParametricityITPJul 10 14:30
Simon Jantsch and Michael NorrishVerifying the LTL to Büchi Automata Translation via Very Weak Alternating AutomataITPJul 12 09:30
Wolfram KahlCalcCheck: A Proof Checker for Teaching the “Logical Approach to Discrete Math”ITPJul 10 10:00
Alexander Knüppel, Thomas Thüm, Carsten Pardylla and Ina SchaeferUnderstanding Parameters of Deductive Verification: An Empirical Investigation of KeYITPJul 09 16:00
Ramana Kumar, Eric Mullen, Zachary Tatlock and Magnus O. MyreenSoftware Verification with ITPs Should Use Binary Code Extraction to Reduce the TCB (short paper)ITPJul 11 17:20
Dominique Larchey-WendlingProof Pearl: Constructive Extraction of Cycle Finding AlgorithmsITPJul 12 12:00
Andreas LochbihlerFast machine words in Isabelle/HOLITPJul 12 11:30
Andreas Lochbihler and Joshua SchneiderRelational parametricity and quotient preservation for modular (co)datatypesITPJul 11 11:00
Alexandra Mendes and Joao F. FerreiraTowards Verified Handwritten Calculational Proofs (short paper)ITPJul 11 16:40
Florian Meßner, Julian Parsert, Jonas Schöpf and Christian SternagelA Formally Verified Solver for Homogeneous Linear Diophantine EquationsITPJul 10 11:30
Étienne MiqueyFormalizing Implicative Algebras in CoqITPJul 09 14:00
Mariano Moscato, Carlos Lopez Pombo, Cesar Munoz and Marco Antonio Feliu GabaldonBoosting the Reuse of Formal SpecificationsITPJul 09 16:30
Julian Parsert and Cezary KaliszykTowards Formal Foundations for Game Theory (short paper)ITPJul 11 16:00
João Paulo Pizani Flor and Wouter SwierstraVerified Timing Transformations in Synchronous Circuits with LambdaPi-WareITPJul 11 10:00
Christine Rizkallah, Dmitri Garbuzov and Steve ZdancewicA Formal Equational Theory for Call-By-Push-ValueITPJul 09 17:30
Hira Syeda and Gerwin KleinProgram Verification in the Presence of Cached Address TranslationITPJul 11 09:00
Joseph Tassarotti and Robert HarperVerified Tail Bounds for Randomized ProgramsITPJul 12 16:00
Simon Wimmer, Shuwei Hu and Tobias NipkowVerified Memoization and Dynamic ProgrammingITPJul 12 11:00
Simon Wimmer and Johannes HölzlMDP + TA = PTA: Probabilistic Timed Automata, Formalized (Short Paper)ITPJul 11 16:20
Jinxu Zhao, Bruno C. D. S. Oliveira and Tom SchrijversFormalization of a Polymorphic Subtyping AlgorithmITPJul 09 17:00
Ran Zmigrod, Matthew L. Daggitt and Timothy G. GriffinAn Agda Formalization of Üresin & Dubois' Asynchronous Fixed-Point TheoryITPJul 10 16:00
Stéphanie DelauneAnalysing privacy-type properties in cryptographic protocolsFSCD
Grigore RosuFormal Design, Implementation and Verification of Blockchain LanguagesFSCD
Peter SelingerChallenges in quantum programming languagesFSCD
Valeria VignudelliProof techniques for program equivalence in probabilistic higher-order languagesFSCD
Sandra Alves and Sabine BrodaA Unifying Framework for Type InhabitationFSCDJul 10 11:00
Nirina Andrianarivelo and Pierre RetyConfluence of Prefix-Constrained Rewrite SystemsFSCDJul 12 17:00
Mauricio Ayala-Rincon, Maribel Fernandez and Daniele Nantes-SobrinhoFixed-Point Constraints for Nominal Equational UnificationFSCDJul 12 11:00
Patrick BahrStrict Ideal Completions of the Lambda CalculusFSCDJul 11 10:00
Alexander Baumgartner, Temur Kutsia, Jordi Levy and Mateu VillaretTerm-Graph Anti-UnificationFSCDJul 12 10:00
Willem Heijltjes and Gianluigi BellinProof nets for bi-intuitionistic linear logicFSCDJul 09 11:00
Maciej Bendkowski and Pierre LescanneCounting Environments and ClosuresFSCDJul 10 15:40
David Cerna and Temur KutsiaHigher-Order Equational Pattern Anti-UnificationFSCDJul 12 11:30
Łukasz CzajkaTerm rewriting characterisation of LOGSPACE for finite and infinite dataFSCDJul 10 16:10
Joerg Endrullis, Jan Willem Klop and Roy OverbeekDecreasing diagrams with two labels are complete for confluence of countable systemsFSCDJul 12 16:30
Simon Forest and Samuel MimramCoherence of Gray categories via rewritingFSCDJul 12 17:30
Thomas GenetCompleteness of Tree Automata CompletionFSCDJul 11 12:00
Amar Hadzihasanovic, Giovanni de Felice and Kang Feng NgA diagrammatic axiomatisation of fermionic quantum circuitsFSCDJul 09 15:00
Mirai Ikebuchi and Keisuke NakanoOn repetitive right application of B-termsFSCDJul 11 09:00
Rohan Jacob-Rao, Brigitte Pientka and David ThibodeauIndex-Stratified TypesFSCDJul 10 12:00
Ambrus Kaposi and András KovácsA Syntax for Higher Inductive-Inductive TypesFSCDJul 10 15:00
Jean-Simon LemayLifting Coalgebra Modalities and IMELL Model Structure to Eilenberg-Moore CategoriesFSCDJul 09 12:00
Daniel R. Licata, Ian Orton, Andrew M. Pitts and Bas SpittersInternal Universes in Models of Homotopy Type TheoryFSCDJul 10 10:00
Bassel Mannaa and Rasmus MøgelbergThe clocks they are adjunctions. Denotational semantics for Clocked Type TheoryFSCDJul 10 09:30
Max New and Daniel LicataCall-by-name Gradual Type TheoryFSCDJul 10 09:00
Lê Thành Dũng NguyễnUnique perfect matchings and proof netsFSCDJul 09 11:30
Naoki Nishida and Yuya MaedaNarrowing Trees for Syntactically Deterministic Conditional Term Rewriting SystemsFSCDJul 11 11:00
Paweł ParysHomogeneity without Loss of GeneralityFSCDJul 11 09:30
Manfred Schmidt-Schauss and David SabelNominal Unification with Atom and Context VariablesFSCDJul 12 12:00
Amin Timany and Matthieu SozeauCumulative Inductive Types in CoqFSCDJul 10 11:30
Sarah Winkler and Aart MiddeldorpCompletion for Logically Constrained RewritingFSCDJul 11 11:30
Christina Kohl and Aart MiddeldorpProTeM: A Proof Term ManipulatorFSCDJul 12 15:00
Takahito Aoto, Makoto Hamana, Nao Hirokawa, Aart Middeldorp, Julian Nagele, Naoki Nishida, Kiraku Shintani and Harald ZanklConfluence Competition 2018FSCD
Willem HeijltjesAn introduction to deep inferenceTYDIJul 07 09:00
Alessio GuglielmiTwo Unifying Structural PrinciplesTYDIJul 07 14:00
Dominic HughesSome incoherent musings on deep inference and combinatorial proofsTYDIJul 07 16:00
Anupam DasProof complexity of deep inference: a surveyTYDIJul 07 17:00
Ross HorneTruely Concurrent Processes in the Calculus of StructuresTYDIJul 07 11:00
Bjoern Lellmann, Elaine Pimentel and Revantha RamanayakeSequentialising nested systemsTYDIJul 07 11:30
Sonia MarinNested sequents for modal logics and beyondTYDIJul 07 12:00
Joseph Paulus and Willem HeijltjesDeep-Inference Intersection TypesTYDIJul 07 10:00
Benjamin RalphDeep Inference, Herbrand's Theorem and Expansion ProofsTYDIJul 07 15:00
Peter W. V. Tran-Jørgensen, René Søndergaard Nilsson and Kenneth LausdahlEnhancing Testing of VDM-SL modelsOvertureJul 14 10:10
Casper Thule, Kenneth Lausdahl and Peter Gorm LarsenOverture FMU: Export VDM-RT Models as Tool-Wrapper FMUsOvertureJul 14 11:00
Tomohiro Oda, Keijiro Araki and Peter Gorm LarsenViennaVM: a Virtual Machine for VDM-SL developmentOvertureJul 14 11:20
René Søndergaard Nilsson, Kenneth Lausdahl, Hugo Daniel Macedo and Peter Gorm LarsenTransforming an industrial case study from VDM++ to VDM-SLOvertureJul 14 14:50
Leo FreitasVDM at large: analysing the EMV Next Generation KernelOvertureJul 14 14:00
Martin Mansfield, Charles Morisset, Carl Gamble, John Mace, Ken Pierce and John FitzgeraldDesign Space Exploration for Secure Building ControlOvertureJul 14 12:00
Simon FraserIntegrating VDM-SL into the continuous delivery pipelines of cloud-based softwareOvertureJul 14 15:10
Georgios Zervakis, Ken Pierce and Carl GambleMulti-modelling of Cooperative SwarmsOvertureJul 14 11:40
Thomas Brihaye, Véronique Bruyère, Aline Goeminne and Jean-François RaskinConstraint Problem for Weak Subgame Perfect Equilibria with omega-regular Boolean ObjectivesMoReJul 13 11:00
Thomas Brihaye, Mickael Randour and Cédric RivièreStochastic o-minimal hybrid systemsMoReJul 13 15:00
Véronique Bruyère, Quentin Hautem and Jean-Francois RaskinParameterized complexity of games with monotonically ordered omega-regular objectivesMoReJul 13 11:30
Gilles Geeraerts, Shibashis Guha and Jean-Francois RaskinSafe and Optimal Scheduling of Hard and Soft TasksMoReJul 13 16:30
Arnd Hartmanns, Sebastian Junges, Joost-Pieter Katoen and Tim QuatmannMultiple Objectives and Cost Bounds in MDPMoReJul 13 10:00
Mohammadhosein Hasanbeig, Alessandro Abate and Daniel KroeningLogically-Constrained Reinforcement LearningMoReJul 13 17:00
Dimitri ScheftelowitschMulti-Scenario Uncertainty in Markov Decision ProcessesMoReJul 13 16:00
Tao Xue, Zhaohui Luo and Stergios ChatzikyriakidisPropositional Forms of Judgemental InterpretationsNLCSJul 07 11:30
Valeria de Paiva, Alexandre Rademaker, Livy Real, Fabricio Chalub and Gerard de MeloOpenWordNet-PT: Taking StockNLCSJul 07 17:30
Aikaterini-Lida Kalouli, Richard Crouch, Valeria de Paiva and Livy RealGraph Knowledge Representations for SICKNLCSJul 07 15:00
Colin ZwanzigerPropositional Attitude Operators in Homotopy Type TheoryNLCSJul 07 11:00
Inari Listenmaa and Koen ClaessenAutomatic test suite generation for PMCFG grammarsNLCSJul 07 17:00
Nino Amiridze and Temur KutsiaAnti-Unification and Natural Language ProcessingNLCSJul 07 10:00
Hai Hu, Thomas Icard and Larry MossAutomated Reasoning from Polarized Parse TreesNLCSJul 07 16:00
Ribeka Tanaka, Koji Mineshima and Daisuke BekkiPaychecks, Presupposition, and Dependent TypesNLCSJul 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.NLCSJul 07 16:30
Hiroshi UnnoHorn Clauses and Beyond for Relational and Temporal Program VerificationHCVS
Pierre GantyTree dimension in verification of constrained Horn clausesHCVS
Qi Zhou, David Heath and William HarrisSolving Constrained Horn Clauses Using Dependence-Disjoint ExpansionsHCVSJul 13 11:00
Giorgio Delzanno, Sylvain Conchon and Angelo FerrandoDeclarative Parameterized Verification of Topology-sensitive Distributed ProtocolsHCVSJul 13 15:00
Ekaterina Komendantskaya and Yue LiTowards Coinductive Theory Exploration in Horn Clause Logic: Extended AbstractHCVSJul 13 12:00
Emanuele De Angelis, Fabio Fioravanti, Adrián Palacios, Alberto Pettorossi and Maurizio ProiettiMetaprogramming and symbolic execution for detecting runtime errors in Erlang programsHCVSJul 13 10:00
António RavaraA simple functional presentation and an inductive correctness proof of the Horn algorithmHCVSJul 13 11:30
Andreas Nuyts and Dominique DevrieseInternalizing Presheaf Semantics: Charting the Design SpaceHoTT/UFJul 07 11:00
Andreas NuytsRobust Notions of Contextual FibrancyHoTT/UFJul 08 11:30
Lars Birkedal, Ranald Clouston, Bassel Mannaa, Rasmus Møgelberg, Andrew Pitts and Bas SpittersDependent Right Adjoint TypesHoTT/UFJul 07 12:00
Clive NewsteadAlgebraic models of dependent type theoryHoTT/UFJul 07 16:30
Taichi UemuraCubical Assemblies and the Independence of the Propositional Resizing AxiomHoTT/UFJul 07 11:30
Iosif PetrakisA Yoneda lemma-formulation of the univalence axiomHoTT/UFJul 08 11:00
Edward MorehouseOrdered CubesHoTT/UFJul 08 15:00
Eric FaberTowards a geometric model theory of type theoryHoTT/UF
Jonathan Weinberger and Ulrik Buchholtz(Truncated) Simplicial Models of Type TheoryHoTT/UFJul 08 16:00
Thorsten AltenkirchTowards the syntax and semantics of higher dimensional type theoryHoTT/UFJul 08 16:30
Genki SatoGeometric realization of truncated semi-simplicial sets meta-constructed within HoTTHoTT/UFJul 07 15:00
Joseph HelferFirst-order homotopical logic and Grothendieck fibrationsHoTT/UFJul 07 17:00
Felix WellenCohesive Covering TheoryHoTT/UFJul 08 12:00
Kuen-Bang Hou Favonia, Carlo Angiuli, Evan Cavallo, Robert Harper and Jonathan SterlingCubical Computational Type TheoryHoTT/UFJul 08 14:00
Hugo HerbelinThe definitional symmetric cubical structure of types in type theory with equality defined by abstraction over an intervalHoTT/UFJul 08 14:30
Mauricio Ayala-Rincón and Philippe BalbianiPreface of the 32nd International Workshop on Unification UNIF 2018UNIF
Silvio GhilardiHandling Substitutions via DualityUNIF
Adrià GascónCompressed Term Unification: Results, Applications, Open problems, and HopesUNIF
Ajay Kumar Eeralla and Christopher LynchBounded ACh UnificationUNIFJul 07 11:30
David Cerna and Temur KutsiaTowards Generalization Methods for Purely Idempotent Equational TheoriesUNIFJul 07 16:30
Temur Kutsia and Cleo PauProximity-Based GeneralizationUNIFJul 07 16:00
Çiğdem GencerAbout the Unification Type of Topological Logics over Euclidean SpacesUNIFJul 07 12:00
Yunus David Kerem Kutz and Manfred Schmidt-SchaussRewriting with Generalized Nominal UnificationUNIFJul 07 17:00
Franz Baader, Pavlos Marantidis and Antoine MottetACUI Unification Modulo Ground TheoriesUNIFJul 07 15:00
Serdar Erbatur, Andrew M. Marshall and Christophe RingeissenKnowledge Problems in Equational Extensions of Subterm Convergent TheoriesUNIFJul 07 11:00
Joerg Siekmann and Peter SzaboUnification Based on Generalized EmbeddingUNIFJul 07 10:00
Kasper Fabæch Brandt, Anders Schlichtkrull and Jørgen VilladsenFormalization of First-Order Syntactic UnificationUNIFJul 07 17:30
Weixi Ma, Jeremy Siek, David Christiansen and Daniel FriedmanEfficiency of a Good but not Linear Nominal Unification AlgorithmUNIFJul 07 17:50
Sara-Jane DunnUncovering the Biological Programs that Govern DevelopmentVEMDP
Andrew J. TurberfieldControlling Assembly and Function of DNA Nanostructures and Molecular MachineryVEMDP
Luca Laurenti, Attila Csikász-Nagy, Marta Kwiatkowska and Luca CardelliMolecular Filters for Noise ReductionVEMDPJul 19 12:00
Hillel Kugler, Till Korten, Stefan Diez and Dan Nicolau Jr.Formal Verification of Network-Based Biocomputation CircuitsVEMDPJul 19 17:20
Matej Troják, Jakub Šalagovič, David Šafránek, Jan Červený, Luboš Brim and Matej HajnalExecutable Biochemical Space for Specification and Analysis of Biochemical SystemsVEMDPJul 19 17:00
Carlo Spaccasassi, Matthew Lakin and Andrew PhillipsRule-based Design of Computational DNA DevicesVEMDPJul 19 11:20
Tomislav Plesa, Konstantinos Zygalakis, David Anderson and Radek ErbanNoise Control for Molecular ComputingVEMDPJul 19 11:40
Ken Chanseau Saint-Germain and Jérôme FeretConservative Approximations of PolymersVEMDPJul 19 16:40
Robert F. JohnsonUsing Transitivity and Modularity in Chemical Reaction Network BisimulationVEMDPJul 19 16:20
Stefan Badelt and Erik WinfreeEquivalence of Chemical Reaction Networks in a CRN-to-DNA Compiler FrameworkVEMDPJul 19 16:00
Keenan Breik, Chris Thachuk, Marijn Heule and David SoloveichikComputing Properties of Stable Configurations of Thermodynamic Binding NetworksVEMDPJul 19 10:00
Jakob Lykke Andersen, Christoph Flamm, Daniel Merkle and Peter F. StadlerRule-Based Gillespie Simulation of Chemical SystemsVEMDPJul 19 11:00
Gareth Molyneux, Viraj Brian Wijesuriya and Alessandro AbateBayesian Verification of Chemical Reaction NetworksVEMDPJul 19 15:00
Alexandru Amarioarei, Frankie Spencer, Corina Itcus, Iris Tusa, Ana Maria Dobre, Gefry Barad, Romica Trandafir, Mihaela Paun, Andrei Paun and Eugen CzeizlerComputational Approaches for the Programmed Assembly of Nanocellulose MeshesVEMDPJul 19 15:10
David Scott WarrenTop-down and Bottom-up Evaluation ReconciledICLPJul 15 11:00
Patrick Kahl and Anthony LeclercEpistemic Logic Programs with World View ConstraintsICLPJul 15 16:15
Rolf SchwitterSpecifying and Verbalising Answer Set Programs in Controlled Natural LanguageICLPJul 16 09:30
Frantisek Farka, Ekaterina Komendantskaya and Kevin HammondProof-relevant Horn Clauses for Dependent Type Inference and Term SynthesisICLPJul 14 14:00
Pedro Cabalar, Roland Kaminski, Torsten Schaub and Anna SchuhmannTemporal Answer Set Programming on Finite TracesICLPJul 15 10:00
Martin Gebser, Van Nguyen, Philipp Obermeier, Thomas Otto, Orkunt Sabuncu, Torsten Schaub and Tran Cao SonExperimenting with robotic intra-logistics domainsICLPJul 17 11:30
Farhad Shakerin and Gopal GuptaCumulative Scoring-based Induction of Default TheoriesICLPJul 15 16:00
Joohyung Lee and Zhun YangTranslating LPOD and CR-Prolog2 into Standard Answer Set ProgramsICLPJul 14 17:30
Benjamin Wu, Alessandra Russo, Mark Law and Katsumi InoueLearning Commonsense Knowledge through Interactive DialogueICLPJul 17 17:00
Arindam Mitra and Chitta BaralIncremental and Iterative Learning of Answer Set Programs from Mutually Distinct ExamplesICLPJul 15 14:30
Bram Aerts and Joost Vennekens Application of Logic-Based Methods to Machine Component DesignICLPJul 15 17:00
Angelos Charalambidis, Panos Rondogiannis and Ioanna SymeonidouApproximation Fixpoint Theory and the Well-Founded Semantics of Higher-Order Logic ProgramsICLPJul 14 12:00
Zhizheng ZhangIntrospecting Preferences In Answer Set ProgrammingICLPJul 15 16:45
Mario Alviano, Carmine Dodaro and Marco MarateaShared aggregate sets in answer set programmingICLPJul 14 11:30
Mario Alviano, Carmine Dodaro, Matti Järvisalo, Marco Maratea and Alessandro PrevitiCautious Reasoning in ASP via Minimal models and Unsatisfiable CoresICLPJul 16 10:00
Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi and Maurizio ProiettiSolving Horn Clauses on Inductive Data Types Without InductionICLPJul 14 15:00
Joana Côrte-Real, Anton Dries, Inês Dutra and Ricardo RochaImproving Candidate Quality of Probabilistic Logic ModelsICLPJul 15 17:15
Joaquin Arias, Manuel Carro, Elmer Salazar, Kyle Marple and Gopal GuptaConstraint Answer Set Programming without GroundingICLPJul 14 17:00
Angela Bonifati, Stefania Dumbrava and Emilio Jesús Gallego AriasCertified Graph View Maintenance with Regular DatalogICLPJul 15 11:30
Tobias Kaminski, Thomas Eiter and Katsumi InoueExploiting Answer Set Programming with External Sources for Meta-Interpretive LearningICLPJul 15 14:00
George Baryannis, Ilias Tachmazidis, Sotiris Batsakis, Grigoris Antoniou, Mario Alviano, Timos Sellis and Pei-Wei TsaiA Trajectory Calculus for Qualitative Spatial Reasoning Using Answer Set ProgrammingICLPJul 15 15:00
Marc Dahlem, Anoop Bhagyanath and Klaus SchneiderOptimal Scheduling for Exposed Datapath Architectures with Buffered Processing Units by ASPICLPJul 17 12:00
Igor StéphanA New Proof-theoretical Linear Semantics for CHRICLPJul 17 17:15
Van Nguyen, Tran Cao Son and Enrico PontelliNatural Language Generation From Ontologies: Application PaperICLPJul 15 17:30
Thanh Nguyen, Enrico Pontelli and Tran SonPhylotastic: An Experiment in Creating, Manipulating, and Evolving Phylogenetic Biology Workflows Using Logic ProgrammingICLPJul 17 11:00
Isabel Garcia-Contreras, Jose F. Morales and Manuel V. HermenegildoTowards Incremental and Modular Context-sensitive AnalysisICLPJul 17 16:45
Federico Igne, Agostino Dovier and Enrico PontelliMASP-Reduce: a proposal for distributed computation of stable modelsICLPJul 15 17:45
Carlo Zaniolo, Ariyam Das, Mohan Yang, Alex Shkapsky, Matteo Interlandi and Tyson CondieDeclarative Algorithms in Datalog with Aggregates: user-friendly formal semantics conducive to performance and scalabilityICLPJul 17 17:45
Daniela Inclezan, Qinglin Zhang, Marcello Balduccini and Ankush IsraneyAn ASP Methodology for Understanding Narratives about Stereotypical ActivitiesICLPJul 16 09:00
Arun Nampally, Timothy Zhang and C. R. RamakrishnanConstraint-Based Inference in Probabilistic Logic ProgramsICLPJul 17 15:00
Joohyung Lee and Yi WangA Probabilistic Extension of Action Language BC+ICLPJul 17 14:30
Bishoksan Kafle, John Gallagher, Graeme Gange, Peter Schachte, Harald Sondergaard and Peter J. StuckeyAn iterative approach to precondition inference using constrained Horn clausesICLPJul 15 12:00
Gregory Duck, Joxan Jaffar and Roland YapShape Neutral Analysis of Graph-based Data-structuresICLPJul 17 14:00
Martin Gebser, Philipp Obermeier, Michel Ratsch-Heitmann, Mario Runge and Torsten SchaubRouting Driverless Transport Vehicles in Car Assembly with Answer Set ProgrammingICLPJul 16 11:00
Aleksy Schubert and Pawel UrzyczynFirst-order answer set programming as constructive proof searchICLPJul 14 14:30
Pedro Cabalar, Jorge Fandinno, Luis Farinas Del Cerro and David PearceFunctional ASP with Intensional Sets; Application to Gelfond-Zhang AgreggatesICLPJul 14 11:00
Nada Sharaf, Slim Abdennadher and Thom FruehwirthCHRvis: Syntax and SemanticsICLPJul 17 17:30
Maximiliano Klemen, Nataliia Stulova, Pedro López-García, Jose F. Morales and Manuel V. HermenegildoTowards Static Performance Guarantees for Programs with Run-time ChecksICLPJul 17 16:30
Da Shen and Yuliya LierlerSMT-based Answer Set Solver CMODELS(DIFF) (System Description)ICLPJul 15 16:30
Marijn HeuleComputable Short ProofsSATJul 11 11:00
Christoph Scholl and Ralf WimmerDependency Quantified Boolean Formulas: An Overview of Solution Methods and ApplicationsSAT
Rahul SanthanamModelling SATSAT
Rüdiger Ehlers and Francisco Palau RomeroApproximately Propagation Complete and Conflict Propagating Constraint EncodingsSATJul 09 14:00
Tobias Paxian, Sven Reimer and Bernd BeckerDynamic Polynomial Watchdog Encoding for Solving Weighted MaxSATSATJul 09 14:30
Alexander NadelSolving MaxSAT with Bit-Vector OptimizationSATJul 09 15:00
Jan Elffers, Jesus Giráldez-Cru, Jakob Nordstrom and Marc VinyalsUsing Combinatorial Benchmarks to Probe the Reasoning Power of Pseudo-Boolean SolversSATJul 09 16:00
Jia Liang, Chanseok Oh, Minu Mathews, Ciza Thomas, Chunxiao Li and Vijay GaneshMachine Learning-based Restart Policy for CDCL SAT SolversSATJul 09 16:30
Vadim Ryvchin and Alexander NadelChronological BacktrackingSATJul 09 17:00
Sima Jamali and David MitchellCentrality-Based Improvements to CDCL HeuristicsSATJul 09 17:30
Dimitris Achlioptas, Zayd Hammoudeh and Panos TheodoropoulosFast Sampling of Perfectly Uniform Satisfying AssignmentsSATJul 10 09:00
Dimitris Achlioptas, Zayd Hammoudeh and Panos TheodoropoulosFast and Flexible Probabilistic Model CountingSATJul 10 09:30
Johannes K. Fichte, Markus Hecher, Michael Morak and Stefan WoltranExploiting Treewidth for Projected Model Counting and its LimitsSATJul 10 10:00
Mikolas JanotaCircuit-based Search Space Pruning in QBFSATJul 10 14:00
Manuel Kauers and Martina SeidlSymmetries for QBFSATJul 10 14:30
Martin Suda and Bernhard GleissLocal Soundness for QBF CalculiSATJul 10 15:00
Michael Lampis, Stefan Mengel and Valia MitsouQBF as an Alternative to Courcelle's TheoremSATJul 10 16:00
Tomáš Peitl, Friedrich Slivovsky and Stefan SzeiderPolynomial-Time Validation of QCDCL CertificatesSATJul 10 16:30
Tobias Friedrich and Ralf RothenbergerSharpness of the Satisfiability Threshold for Non-Uniform Random k-SATSATJul 11 09:00
Marc Vinyals, Jan Elffers, Jesús Giráldez-Crú, Stephan Gocht and Jakob NordstromIn Between Resolution and Cutting Planes: A Study of Proof Systems for Pseudo-Boolean SAT SolvingSATJul 11 09:30
Nicola Galesi, Navid Talebanfard and Jacobo ToranCops-Robber games and the resolution of Tseitin formulasSATJul 11 10:00
Hoda Abbasizanjani and Oliver KullmannMinimal unsatisfiability and minimal strongly connected digraphsSATJul 11 16:00
Ryan Berryhill, Alexander Ivrii and Andreas VenerisFinding all Minimal Safe Inductive SetsSATJul 11 16:30
Shubhani Gupta, Aseem Saxena, Anmol Mahajan and Sorav BansalEffective use of SMT solvers for Program Equivalence Checking through Invariant Sketching and Query DecompositionSATJul 12 11:00
Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri and Roberto SebastianiExperimenting on Solving Nonlinear Integer Arithmetic with Incremental LinearizationSATJul 12 11:30
Sean Weaver, Hannah Roberts and Michael SmithXORSAT Set Membership FiltersSATJul 12 12:00
Stepan Kochemazov and Oleg ZaikinALIAS: A Modular Tool for Finding Backdoors for SATSATJul 12 14:00
Alexey Ignatiev, Antonio Morgado and Joao Marques-SilvaPySAT: A Python Toolkit for Prototyping with SAT OraclesSATJul 12 14:30
Svyatoslav Korneev, Nina Narodytska, Luca Pulina, Armando Tacchella, Nikolaj Bjorner and Mooly SagivConstrained Image Generation Using Binarized Neural Networks with Decision ProceduresSATJul 12 15:00
Clemens GrabmayerModeling Terms by Graphs with Structure Constraints (Two Illustrations)TERMGRAPH
Lee Barnett and David PlaistedProgramming by Term RewritingTERMGRAPHJul 07 17:30
Nachum Dershowitz and Jean-Pierre JouannaudDrags: an algebraic framework for graph rewritingTERMGRAPHJul 07 11:00
Nneka EneA Port-graph Model for FinanceTERMGRAPHJul 07 16:30
Wolfram Kahl and Yuhang ZhaoSemantics-Preserving DPO-Based Term Graph RewritingTERMGRAPHJul 07 15:00
Mitsuhiro Okada and Yuta TakahashiOn quasi ordinal diagram systemsTERMGRAPHJul 07 12:00
Sophie Tourret and Andrew CropperSLD-Resolution Reduction of Second-Order Horn Fragments - Extended AbstractTERMGRAPHJul 07 16:00
János VargaFinding the Transitive Closure of Functional Dependencies using Strategic Port Graph RewritingTERMGRAPHJul 07 17:00
Vladimir ZamdzhievA Framework for Rewriting Families of String DiagramsTERMGRAPHJul 07 11:30
Tiantian GaoKnowledge Authoring and Question Answering via Controlled Natural LanguageICLP-DCJul 18 12:00
Van NguyenNatural Language Generation From OntologiesICLP-DCJul 18 11:30
Yi WangProbabilistic Action Language pBC+ICLP-DCJul 18 10:00
Richard TaupeSpeeding Up Lazy-Grounding Answer Set SolvingICLP-DCJul 18 15:00
Filipe Gouveia, Ines Lynce and Pedro T. MonteiroModel Revision of Logical Regulatory Networks using Logic-based ToolsICLP-DCJul 18 16:00
Emily LeblancExplaining Actual Causation via Reasoning about Actions and ChangeICLP-DCJul 18 09:30
Zhun YangTranslating P-log, LP^{MLN}, LPOD, and CR-Prolog2 into Standard Answer Set ProgramsICLP-DCJul 18 14:30
Philipp ObermeierScalable Robotic Intra-Logistics with Answer Set ProgrammingICLP-DCJul 18 14:00
Frantisek FarkaProof-relevant resolution for elaboration of programming languagesICLP-DCJul 18 09:00
Arindam MitraThe Learning-Knowledge-Reasoning Paradigm For Natural Language Understanding and Question AnsweringICLP-DCJul 18 11:00
Jamie VicaryDesigning Globular: formal proofs as geometrical objectsUITP
Tomer LibalImplementing a Proof Assistant using Focusing and Logic ProgrammingUITPJul 13 10:00
Jan Gorzny, Ezequiel Postan and Bruno Woltzenlogel PaleoPartial Regularization of First-Order Resolution ProofsUITPJul 13 11:00
Sarah Grebing, An Thuy Tien Luong and Alexander WeiglAdding Text-Based Interaction to a Direct-Manipulation Interface for Program Verification -- Lessons LearnedUITPJul 13 11:30
Rustam Zhumagambetov and Mark SterlingAutomated Theorem Proving in a Chat EnvironmentUITPJul 13 12:00
Makarius WenzelIsabelle/PIDE after 10 years of developmentUITPJul 13 14:00
Steffen Frerix and Peter KoepkeText-Orientated Formal MathematicsUITPJul 13 14:30
Florent Capelli and Stefan MengelTractability results for structured quantified CNF-formulas via knowledge compilationQBFJul 08 14:40
Holger Hoos, Tomáš Peitl, Friedrich Slivovsky and Stefan SzeiderPortfolio-Based Algorithm Selection for Circuit QBFsQBFJul 08 16:20
Martin SudaTowards the Semantics of QBF ClausesQBFJul 08 10:00
Matthias van der Hallen and Gerda JanssensA Grounder From Second-Order Logic To QBFQBFJul 08 15:00
Jan Maly and Stefan WoltranA new logic for jointly representing hard and soft constraintsPRUVJul 19 12:00
Alireza Ensan, Eugenia Ternovska and Heng LiuA Model-Theoretic View on Preferences in Declarative Specifications of Search ProblemsPRUVJul 19 16:00
Nico PotykaMeasuring Disagreement among Knowledge BasesPRUVJul 19 11:00
Cunjing Ge, Feifei Ma, Tian Liu, Jian Zhang and Xutong MaA New Probabilistic Algorithm for Approximate Model CountingPRUVJul 19 16:30
José Paredes, Maria Vanina Martinez, Gerardo Simari and Marcelo A. FalappaLeveraging Probabilistic Existential Rules for Adversarial DeduplicationPRUVJul 19 17:00
Aouatef Rouahi, Kais Ben Salah and Khaled GhediraEvidential Group Decision Making Model with Belief-Based PreferencesPRUVJul 19 11:30
Laura Giordano and Valentina GliozziReasoning about exceptions in ontologies: from the lexicographic closure to the skeptical closurePRUVJul 19 15:10
Cunjing Ge, Feifei Ma and Jian ZhangVolCE: An Efficient Tool for Solving #SMT(LA) ProblemsPRUVJul 19 17:30
Özgür AkgünAutomated Constraint Modelling with ConjureLaShJul 18 16:25
Sabine BauerDecidable Linear Tree ConstraintsLaShJul 18 17:15
Bruno Courcelle and Irène DurandMonadic Second-Order Model Checking with Fly-AutomataLaShJul 18 09:00
Johannes Fichte Solving #SAT by Parameterized Algorithms: Exploiting Small TreewidthLaShJul 18 16:50
Tomas Fiedor, Lukas Holik, Petr Janku, Ondrej Lengal and Tomas VojnarLazy Automata Techniques for WS1SLaShJul 18 10:05
Alan FrischESSENCE, A Language for Specifying Combinatorial Problems: What, Why and So What?LaShJul 18 16:00
Robert GiegerichDeclarative Dynamic Programming with Inverse Coupled Rewrite SystemsLaShJul 18 14:00
Joachim Kneis, Alexander Langer and Peter RossmanithCourcelle’s Theorem – A Game-Theoretic ApproachLaShJul 18 11:00
Eugenia TernovskaA Logic of Information FlowsLaShJul 18 15:00
Dmitriy TraytelA Derivative-Based Decision Procedure for WS1SLaShJul 18 12:05
Eugenia TernovskaA Logic of Information Flows - PaperLaSh
Sabine BauerDecidable Linear Tree Constraints - Extended AbstractLaSh
Bruno CourcelleMonadic Second-Order Model Checking with Fly-Automata - SlidesLaSh
Roberta Costabile, Alessio Fiorentino, Nicola Leone, Marco Manna, Kristian Reale and Francesco RiccaRole-Based Access Control via JASPLPOPJul 18 11:30
Marc Denecker and Jo DevriendtThe RBAC challenge in the KB-paradigmLPOP
Thom FruehwirthA Rule-Based Tool for Analysis and Generation of Graphs Applied to Mason's MarksLPOPJul 18 16:50
Thom FruehwirthSecurity Policies in Constraint Handling RulesLPOPJul 18 11:10
Daniel GallConfluence Analysis of Cognitive Models with Constraint Handling RulesLPOPJul 18 15:20
Nicola Leone, Bernardo Cuteri, Marco Manna, Kristian Reale and Francesco RiccaOn the Development of Industrial Applications with ASPLPOPJul 18 09:50
Yanhong A. Liu and Scott StollerEasier Rules and Constraints for ProgrammingLPOPJul 18 12:10
Torsten SchaubHow to upgrade ASP for true dynamic modelling and solving?LPOPJul 18 16:40
K. Tuncay TekleThe RBAC challenge in LogiQL: Solutions and LimitationsLPOP
Peter Van RoyA software system should be declarative except where it interacts with the real worldLPOPJul 18 17:00
Joost VennekensLogic-based Methods for Software Engineers and Business PeopleLPOPJul 18 12:00
David S. WarrenLPOP2018 XSB Position PaperLPOPJul 18 11:20
Neng-Fa Zhou and Håkan KjellerstrandA Picat-based XCSP Solver - from Parsing, Modeling, to SAT EncodingLPOPJul 18 15:10
Julien NarbouxGeoCoq: Formalized Foundations of GeometryThEdu
Nuno Baeta and Pedro QuaresmaRating of Geometric Automated Theorem ProversThEduJul 18 10:00
Walther NeuperLucas Interpretation from Programmers’ PerspectiveThEduJul 18 11:00
Jørgen Villadsen, Andreas Halkjær From and Anders SchlichtkrullNatural Deduction Assistant (NaDeA)ThEduJul 18 09:30
Anders Schlichtkrull, Jørgen Villadsen and Andreas Halkjær FromStudents' Proof Assistant (SPA)ThEduJul 18 09:00
Jørgen VilladsenProving in the Isabelle Proof Assistant that the Set of Real Numbers is not CountableThEduJul 18 14:30
Maximilian Doré and Krysia BrodaTowards intuitive reasoning in axiomatic geometryThEduJul 18 14:00
Natasha Fernandes, Mark Dras and Annabelle McIverProcessing text for privacy: An information flow perspectiveFM
Kim Guldstrand Larsen, Florian Lorber and Brian Nielsen20 Years of Real Real Time Model ValidationFM
Keyvan Azadbakht, Frank De Boer and Erik de VinkDeadlock Detection for Actor-based CoroutinesFMJul 15 09:00
Arthur Américo, Mario S. Alvim and Annabelle McIverAn Algebraic Approach for Reasoning About Information FlowFMJul 15 09:30
Jingyi Wang, Jun Sun, Yifan Jia, Shengchao Qin and Zhiwu XuTowards `Verifying' a Water Treatment SystemFMJul 15 10:00
Florent Avellaneda and Alexandre Petrenko FSM Inference from Long TracesFMJul 15 12:00
Davide Giacomo Cavezza, Dalal Alrajeh and Andras GyorgyA Weakness Measure for GR(1) FormulaeFMJul 15 15:00
Simon Busard and Charles PecheurProducing Explanations for Rich LogicsFMJul 15 16:00
Thomas FerrèreThe Compound Interest in Relaxing PunctualityFMJul 15 16:30
Ivan Ruchkin, Joshua Sunshine, Grant Iraci, Bradley Schmerl and David GarlanIPL: An Integration Property Language for Multi-Model Cyber-Physical SystemsFMJul 15 17:00
Raúl Pardo, Cesar Sanchez and Gerardo SchneiderTimed Epistemic Knowledge Bases for Social NetworksFMJul 15 17:30
Giovanni Bacci, Kim Guldstrand Larsen, Nicolas Markey, Patricia Bouyer-Decitre, Uli Fahrenberg and Pierre-Alain ReynierOptimal and Robust Controller Synthesis Using Energy Timed Automata with UncertaintyFMJul 16 10:00
Ian J. Hayes and Larissa MeinickeEncoding fairness in a synchronous concurrent program algebraFMJul 16 11:00
Robert Colvin and Graeme SmithA wide-spectrum language for verification of programs on weak memory modelsFMJul 16 11:30
Daniel Fava, Martin Steffen and Volker StolzOperational Semantics of a Weak Memory Model with Channel SynchronizationFMJul 16 12:00
Signe Geisler and Anne E. HaxthausenStepwise Development and Model Checking of a Distributed Interlocking System - using RAISEFMJul 16 11:00
Rongjie Yan, Di Zhu, Fan Zhang, Yiqi Lv, Junjie Yang and Kai HuangResource-aware Design for Reliable Autonomous Applications with Multiple PeriodsFMJul 16 11:30
Philipp Berger, Joost-Pieter Katoen, Erika Ábrahám, Md Tawhid Bin Waez and Thomas RambowVerifying Auto-Generated C Code from SimulinkFMJul 16 12:00
Andrea Vandin, Maurice H. Ter Beek, Axel Legay and Alberto Lluch LafuenteQFLan: A Tool for the Quantitative Analysis of Highly Reconfigurable SystemsFMJul 16 16:00
Thomas Letan, Yann Régis-Gianas, Pierre Chifflier and Guillaume HietModular Verification of Programs with Effects and Effect Handlers in CoqFMJul 16 16:30
Heiko Becker, Pavel Panchekha, Eva Darulova and Zachary TatlockCombining Tools for Optimization and Analysis of Floating-Point ComputationsFMJul 16 17:00
Laura Titolo, Mariano Moscato, Cesar Munoz, Aaron Dutle and Francois BobotA Formally Verified Floating-Point Implementation of the Compact Position Reporting AlgorithmFMJul 16 17:30
Johanna Nellen, Thomas Rambow, Md Tawhid Bin Waez, Erika Abraham and Joost-Pieter KatoenFormal Verification of Automotive Simulink Controller Models: Empirical Technical Challenges, Evaluation and RecommendationsFMJul 16 16:00
Claudio Menghi, Sergio Garcia, Patrizio Pelliccione and Jana TumovaMulti-Robot LTL Planning Under UncertaintyFMJul 16 16:30
Andrew Sogokon, Khalil Ghorbal, Yong Kiam Tan and André PlatzerVector Barrier Certificates and Comparison SystemsFMJul 16 17:00
Hana Chockler, Shibashis Guha and Orna KupfermanTimed VacuityFMJul 16 17:30
Takumi Akazaki, Shuang Liu, Yoriyuki Yamagata, Yihai Duan and Jianye HaoFalsification of Cyber-Physical Systems Using Deep Reinforcement LearningFMJul 17 09:00
Dhriti Khanna, Subodh Sharma, César Rodríguez and Rahul PurandareDynamic Symbolic Verification of MPI ProgramsFMJul 17 09:30
Sander de Putter and Anton WijsTo Compose, Or Not to Compose, That is the Question: An Analysis of Compositional State Space GenerationFMJul 17 10:00
Gavin LoweView abstraction for systems with component identitiesFMJul 17 12:00
Fuyuan Zhang, Yongwang Zhao, David Sanan, Yang Liu, Alwen Tiu, Shang-Wei Lin and Jun SunCompositional Reasoning for Shared-variable Concurrent ProgramsFMJul 17 14:00
Axel Legay, Dirk Nowotka, Danny Bøgsted Poulsen and Louis-Marie TraonouezStatistical Model Checking of LLVM CodeFMJul 17 14:30
Elvira Albert, Miguel Gomez-Zamalloa, Albert Rubio, Matteo Sammartino and Alexandra SilvaSDN-Actors: Modeling and Verification of SDN ProgramsFMJul 17 17:00
Sorawee Porncharoenwase, Tim Nelson and Shriram KrishnamurthiCompoSAT: Specification-Guided Coverage for Model FindingFMJul 17 16:00
Chuchu Fan, Zhenqi Huang and Sayan MitraApproximate Partial Order ReductionFMJul 17 16:30
Cosimo LaneveA lightweight deadlock analysis for programs with threads and reentrant locksFMJul 17 15:00
Alessandro Cimatti, Ivan Stojic and Stefano TonettaFormal Specification and Verification of Dynamic Parametrized ArchitecturesFMJul 17 17:30
Cesar Munoz, Anthony Narkawicz and Aaron DutleFrom Formal Requirements to Highly Assured Software for Unmanned Aircraft SystemsFMJul 17 09:00
Arne BoralvInterlocking Design Automation using Prover TridentFMJul 17 09:30
Joerg Brauer and Uwe SchulzeModel-Based Testing for Avionics SystemsFMJul 17 10:00
Daniel Kaestner, Laurent Mauborgne and Christian FerdinandOn Software Safety, Security, and Abstract InterpretationFMJul 17 14:00
Pavel Avgustinov, Kevin Backhouse and Man Yue MoVariant analysis with QLFMJul 17 14:30
Ernie CohenObject-Oriented Security ProofsFMJul 17 15:00
Nikolaj BjornerZ3 and SMT in Industrial R&DFMJul 17 16:00
Tewodros A. Beyene and Harald RuessEvidential and Continuous Integration of Software Verification ToolsFMJul 17 16:30
Thierry LecomteDisruptive Innovations for the Development and the Deployment of Fault-Free SoftwareFMJul 17 17:00
Gabriel EbnerFast cut-elimination using proof terms: an empirical studyCL&CJul 07 11:00
Anthony Cantor and Aaron Stump(Short Paper) Towards a Dualized Sequent Calculus with CanonicityCL&CJul 07 10:00
Graham LeighHerbrand's Theorem as Higher-Order RecursionCL&CJul 07 14:45
Federico AschieriOn Natural Deduction for Herbrand Constructive Logics III: The Strange Case of the Intuitionistic Logic of Constant DomainsCL&CJul 07 14:00
Matteo Manighetti and Andrea CondoluciAdmissible tools in the kitchen of intuitionistic logicCL&CJul 07 16:00
Sorin StratulatValidating Back-links of FOL$_{\mbox{\normalsize ID}}$ Cyclic Pre-proofsCL&CJul 07 11:45
Anupam DasSome ideas on cut-elimination for cyclic arithmetic proofsCL&CJul 07 17:30
Stéphane Demri, Etienne Lozes and Denis LugiezA Complete Proof System for Basic Symbolic Heaps with PermissionsADSLJul 13 12:00
Jens Katelaan, Dejan Jovanović and Georg WeissenbacherSloth: Separation Logic and Theories via Small ModelsADSLJul 13 16:10
Mnacho Echenim, Radu Iosif and Nicolas PeltierThe Complexity of Prenex Separation Logic with One SelectorADSLJul 13 15:20
Didier Galmiche and Daniel MeryLabelled Cyclic Proofs for Separation LogicADSLJul 13 11:30
Koji Nakazawa, Makoto Tatsuta and Daisuke KimuraCyclic Theorem Prover for Separation Logic by Magic WandADSLJul 13 11:00
James Brotherston and Max KanovichOn the Complexity of Pointer Arithmetic in Separation LogicADSLJul 13 14:50
Jason GrossTeaching Your Rooster to Crow in CCoqJul 08 17:00
Armaël GuéneauProcrastination, A proof engineering techniqueCoqJul 08 10:00
Sylvain BoulméWhat is the Foreign Function Interface of the Coq Programming Language?CoqJul 08 11:30
Reynald Affeldt, Cyril Cohen, Assia Mahboubi, Damien Rouhling and Pierre-Yves StrubClassical Analysis with CoqCoqJul 08 11:00
Olivier LaurentPreliminary Report on the Yalla LibraryCoqJul 08 12:00
Mirai Ikebuchi and Keisuke NakanoComplCoq: Rewrite Hint Construction with Completion ProceduresCoqJul 08 16:00
Lasse BlaauwbroekProof Construction by Tactic LearningCoqJul 08 17:30
Cyprien Mangin and Matthieu SozeauTowards a formalization of the guard conditionCoqJul 08 16:30
Ugo Dal LagoOn Higher-Order Probabilistic ComputationDCM
Delia KesnerQuantitative Types: from Foundations to ApplicationsDCM
Damiano MazzaPolyadic Approximations and Intersection TypesDCM
Ian MackieModels of Computation that Conserve DataDCMJul 08 10:00
Paola Giannini, Marco Servetto and Elena ZuccaA syntactic model of mutation and aliasingDCMJul 08 11:00
Adrian Francalanza, Marco Giunti and António RavaraPointing to Private NamesDCMJul 08 11:30
Joseph Razavi and Andrea SchalkA Category Theoretic Interpretation of Gandy’s Principles for MechanismsDCMJul 08 12:00
Alessandra Di PierroTowards a Formal System for Topological Quantum ComputationDCMJul 08 15:00
Nachum DershowitzGeneric Graph SemanticsDCMJul 08 16:00
Siddharth BhaskarComputability over locally finite structures from algebraLCCJul 13 11:45
Anupam Das and Isabel OitavemA recursion-theoretic characterisation of the positive polynomial-time functionsLCCJul 13 11:15
Steven Lindell and Scott WeinsteinTraversal-invariant definability and Logarithmic-space computationLCCJul 13 11:00
Pedro Lopez-Garcia, Maximiliano Klemen, Umer Liqat and Manuel V. HermenegildoA General Equational Framework for Static Profiling of Parametric Resource UsageLCCJul 13 12:00
Moritz Müller and Ján PichFeasibly constructive proofs of succinct weak circuit lower boundsLCCJul 13 11:30
Edwin PinCompleteness in the Second Level of the Polynomial Time Hierarchy through Syntactic PropertiesLCCJul 13 12:15
Martin GieseIndustrial Data AccessIJCAR
Erika AbrahamSymbolic Computation Techniques in SMT Solving: Mathematical Beauty meets Efficient HeuristicsIJCAR
Jean Marie Lagniez, Daniel Le Berre, Tiago de Lima and Valentin MontmirailAn Assumption-Based Approach for Solving The Minimal S5-Satisfiability ProblemIJCARJul 14 14:00
Yizheng Zhao and Renate A. SchmidtFAME: An Automated Tool for Semantic Forgetting in Expressive Description LogicsIJCARJul 14 16:30
Alexander Bentkamp, Jasmin Christian Blanchette, Simon Cruanes and Uwe WaldmannSuperposition for Lambda-Free Higher-Order LogicIJCARJul 16 11:30
Miika Hannula and Sebastian LinkAutomated Reasoning about Key SetsIJCARJul 17 11:30
Michael Peter Lettmann and Nicolas PeltierA Tableaux Calculus for Reducing Proof SizeIJCARJul 15 10:00
Franziska Rapp and Aart MiddeldorpFORT 2.0IJCARJul 17 15:15
Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel and Uwe WaldmannFormalizing Bachmair and Ganzinger's Ordered Resolution ProverIJCARJul 15 12:00
Alexander Steen and Christoph BenzmüllerThe Higher-Order Prover Leo-IIIIJCARJul 17 14:00
Jeremy Dawson, Nachum Dershowitz and Rajeev GoreWell-Founded UnionsIJCARJul 15 15:00
Katalin Fazekas, Fahiem Bacchus and Armin BiereImplicit Hitting Set Algorithms for Maximum Satisfiability Modulo TheoriesIJCARJul 14 11:30
Sylvain Conchon, David Declerck and Fatiha ZaidiCubicle-W: Parameterized Model Checking on Weak MemoryIJCARJul 17 14:30
Florian Lonsing and Uwe EglyQRAT+: Generalizing QRAT by a More Powerful QBF Redundancy PropertyIJCARJul 15 09:00
Guillaume Melquiond and Raphaël Rieu-HelftA Why3 framework for reflection proofs and its application to GMP's algorithmsIJCARJul 15 17:30
Marcelo Finger and Sandro PretoProbably Half True: Probabilistic Satisfiability over Lukasiewicz Infinitely-valued LogicIJCARJul 17 11:00
André PlatzerUniform Substitution for Differential Game LogicIJCARJul 15 17:00
Max Kanovich, Stepan Kuznetsov, Vivek Nigam and Andre ScedrovA Logical Framework with Commutative and Non-Commutative SubexponentialsIJCARJul 15 16:30
Peter Backeman, Aleksandar Zeljić, Christoph M. Wintersteiger and Philipp RümmerExploring Approximations for Floating-Point Arithmetic using UppSATIJCARJul 15 11:00
Manuel Bodirsky and Johannes GreinerComplexity of Combinations of Qualitative Constraint Satisfaction ProblemsIJCARJul 16 09:30
Mnacho Echenim, Nicolas Peltier and Yanis SellamiA Generic Framework for Implicate Generation Modulo TheoriesIJCARJul 14 12:00
Stefan Ciobaca and Dorel LucanuA Coinductive Approach to Proving Reachability in Logically Constrained Term Rewriting SystemsIJCARJul 14 16:00
Cunjing Ge, Feifei Ma, Tian Liu, Jian Zhang and Xutong MaA New Probabilistic Algorithm for Approximate Model CountingIJCARJul 14 15:00
Martin BrombergerA Reduction from Unbounded Linear Mixed Arithmetic Problems into Bounded ProblemsIJCARJul 15 12:00
Nao Hirokawa, Julian Nagele and Aart MiddeldorpCops and CoCoWeb: Infrastructure for Confluence ToolsIJCARJul 17 15:00
Pei Huang, Feifei Ma, Jian Zhang, Cunjing Ge and Hantao ZhangInvestigating the Existence of Large Sets of Idempotent Quasigroups via Satisfiability TestingIJCARJul 14 14:30
Jasmin Christian Blanchette, Nicolas Peltier and Simon RobillardSuperposition with Datatypes and CodatatypesIJCARJul 16 11:00
Nicholas Smallbone and Koen ClaessenEfficient encodings of first-order Horn formulas in equational logicIJCARJul 16 12:00
Evgenii Kotelnikov, Laura Kovacs and Andrei VoronkovA FOOLish Encoding of the Next State Relations of Imperative ProgramsIJCARJul 15 16:30
Dominique Larchey-WendlingConstructive Decision via Redundancy-free Proof-SearchIJCARJul 15 11:00
Nicolas Jeannerod and Ralf TreinenDeciding the First-Order Theory of an Algebra of Feature Trees with UpdatesIJCARJul 16 09:00
Jens Katelaan, Dejan Jovanović and Georg WeissenbacherA Separation Logic with Data: Small Models and AutomationIJCARJul 17 10:00
Sarah Winkler and Georg MoserMaedMax: A Maximal Ordered Completion ToolIJCARJul 17 14:45
Matteo Acclavio and Lutz StrassburgerFrom Syntactic Proofs to Combinatorial ProofsIJCARJul 15 16:00
Cláudia Nalon and Dirk PattinsonA Resolution-Based Calculus for Preferential LogicsIJCARJul 15 09:00
Benjamin Kiesl, Adrian Rebola-Pardo and Marijn HeuleExtended Resolution Simulates DRATIJCARJul 15 09:30
Bohua Zhan and Maximilian P. L. HaslbeckVerifying Asymptotic Time Complexity of Imperative Programs in IsabelleIJCARJul 15 11:30
Jochen Hoenicke and Tanja SchindlerEfficient Interpolation for the Theory of ArraysIJCARJul 14 11:00
Bartosz Piotrowski and Josef UrbanATPboost: Learning Premise Selection in Binary Setting with ATP FeedbackIJCARJul 17 14:15
Dennis Müller, Florian Rabe and Michael KohlhaseTheories as TypesIJCARJul 15 17:30
Andrew Reynolds, Arjun Viswanathan, Haniel Barbosa, Cesare Tinelli and Clark BarrettDatatypes with Shared SelectorsIJCARJul 15 11:30
Yevgeny Kazakov and Peter SkočovskýEnumerating Justifications using ResolutionIJCARJul 15 09:30
Alexey Ignatiev, Filipe Pereira, Nina Narodytska and Joao Marques-SilvaA SAT-Based Approach to Learn Explainable Decision SetsIJCARJul 15 10:00
Son Ho, Oskar Abrahamsson, Ramana Kumar, Magnus O. Myreen, Yong Kiam Tan and Michael NorrishProof-Producing Synthesis of CakeML with I/O and Local State from Monadic HOL FunctionsIJCARJul 15 17:00
Julio Cesar Lopez Hernandez and Konstantin KorovinAn abstraction-refinement framework for reasoning with large theoriesIJCARJul 17 12:00
Jacopo Urbani, Markus Krötzsch, Ceriel Jacobs, Irina Dragoste and David CarralEfficient Model Construction for Horn Logic with VLog: System DescriptionIJCARJul 14 16:45
Anupam DasFocussing, MALL and the polynomial hierarchyIJCARJul 16 10:00
Etienne Payet and Fausto SpotoChecking Array Bounds by Abstract Interpretation and Symbolic ExpressionsIJCARJul 15 16:00
Salvador LucasPresentation of the WST 2018 proceedingsWST
Eric HehnerObjective and Subjective SpecificationsWSTJul 18 12:00
Guillaume Genestier and Frédéric BlanquiTermination of Lambda-Pi modulo rewriting using the size-change principleWSTJul 19 16:00
Jera Hensel, Florian Frohn and Jürgen GieslComplexity Analysis for Bitvector ProgramsWSTJul 19 11:00
Alfons Geser, Dieter Hofbauer and Johannes WaldmannSemantic Kachinuki OrderWSTJul 18 14:00
Nachum Dershowitz and Jean-Pierre JouannaudGPO: A Path Ordering for GraphsWSTJul 18 11:30
Jose Divasón, Sebastiaan Joosten, René Thiemann and Akihisa YamadaA Perron-Frobenius Theorem for Jordan Blocks for Complexity ProvingWSTJul 19 11:30
Jonas Schöpf and Christian SternagelTTT2 with Termination Templates for TeachingWSTJul 19 15:00
Cristina David, Daniel Kroening and Peter SchrammelProcedure-Modular Termination AnalysisWSTJul 18 11:00
Salvador LucasWell-founded models in proofs of terminationWSTJul 18 15:00
Aalok Thakkar, Balaji Krishnamurthy and Piyush GuptaVerification of Rewriting-based Query OptimizersWSTJul 19 14:30
Jesús J. Doménech, Samir Genaim and John P. GallagherControl-Flow Refinement via Partial EvaluationWSTJul 19 14:00
Alicia Merayo Corcoba and Samir GenaimInference of Linear Upper-Bounds on the Expected Cost by Solving Cost RelationsWSTJul 19 12:00
Dieter HofbauerEmbracing Infinity - Termination of String Rewriting by Almost Linear Weight FunctionsWSTJul 18 14:30
Carsten Fuhs and Cynthia KopImproving Static Dependency Pairs for Higher-Order RewritingWSTJul 19 16:30
Guy Avni, Thomas A. Henzinger and Ventsislav ChonevInfinite-Duration Richman Bidding GamesSRJul 08 14:00
Nicolas Basset, Ismaël Jecker, Arno Pauly, Jean-Francois Raskin and Marie Van Den BogaardBeyond admissibility: Dominance between chains of strategiesSRJul 07 17:20
Francesco Belardinelli, Alessio Lomuscio, Aniello Murano and Sasha RubinVerification of Multi-agent Systems with Imperfect Information and Public ActionsSRJul 07 16:00
Raphaël Berthon, Bastien Maubert, Aniello Murano, Sasha Rubin and Moshe VardiStrategy Logic with Imperfect InformationSRJul 08 16:40
Antonio Di Stasio, Aniello Murano and Moshe VardiSolving Parity Games: Explicit vs SymbolicSRJul 08 14:40
Nathanaël Fijalkow, Bastien Maubert, Aniello Murano and Sasha RubinQuantifying Bounds in Strategy LogicSRJul 08 16:00
Patrick Gardy, Patricia Bouyer and Nicolas Markey Dependences in Strategy LogicSRJul 08 17:20
Neil Ghani, Jules Hedges, Philipp Zahn and Viktor WinschelCompositional Game TheorySRJul 07 14:00
Julian Gutierrez, Paul Harrenstein, Thomas Steeples and Michael WooldridgeLocal Equilibria in Logic-Based Multi-Player GamesSRJul 07 16:40
Stephane Le RouxConcurrent games and semi-random determinacySRJul 07 14:40
Henning Christiansen and Maja H. KirkebyConfluence in Constraint Handling RulesIWC
Simon ForestCritical pairs for Gray categoriesIWCJul 07 11:30
Nohra Hage and Philippe MalbosCoherence of monoids by insertionsIWCJul 07 11:00
Benjamin Dupont and Philippe MalbosCoherence modulo relationsIWCJul 07 10:00
Cyrille ChenavierThe diamond lemma for free modulesIWCJul 07 12:00
Christian Sternagel and Sarah WinklerCertified Ordered CompletionIWCJul 07 15:00
Bertram Felgenhauer, Aart Middeldorp, T. V. H. Prathamesh and Franziska RappTowards a Verified Decision Procedure for Confluence of Ground Term Rewrite Systems in Isabelle/HOLIWCJul 07 14:30
Naoki Nishida, Yuta Tsuruta and Yoshiaki KanazawaConvergence of Simultaneously and Sequentially Unraveled TRSs for Normal Conditional TRSsIWCJul 07 14:00
Kousuke Fukui and Koji NakazawaComplete Axiom System of Cluster AlgebraIWCJul 07 16:00
Manfred Schmidt-Schauss and Nils DallmeyerOptimizing Space of Parallel ProcessesWPTEJul 08 11:30
Yoshiaki Kanazawa and Naoki NishidaOn Transforming Functions Accessing Global Variables into Logically Constrained Term Rewriting SystemsWPTEJul 08 12:00
Naoki Nishida and Yuya MaedaOn Transforming Narrowing Trees into Regular Tree Grammars Generating Ranges of SubstitutionsWPTEJul 08 14:30
David SabelAutomating the Diagram Method to Prove Correctness of Program TransformationsWPTEJul 08 11:00
Sebastian Buruiana and Stefan CiobacaReducing Total Correctness to Partial Correctness by a Transformation of the Language SemanticsWPTEJul 08 14:00
Christian Herrera, Tewodros A. Beyene and Vivek NigamVerification of Ada Programs with AdaHornWPTEJul 08 15:00
Kuen-Bang HouCubical Computational Type Theory and RedPRLLFMTP
Delia KesnerA fresh view of call-by-needLFMTP
Grigore RosuWhy and How Does K work? The Logical Infrastructure Behind ItLFMTP
Carlo Angiuli, Evan Cavallo, Kuen-Bang Hou Favonia, Robert Harper and Jonathan SterlingThe RedPRL Proof AssistantLFMTP
Martin Copes, Nora Szasz and Alvaro TasistroFormalization in Constructive Type Theory of the Standardization TheoremLFMTPJul 07 14:00
Ernesto Copello, Nora Szasz and Alvaro TasistroFormalisation of Barendregt's Variable Convention for Generic Structures with BindersLFMTPJul 07 14:30
François ThiréSharing a library between proof assistants: reaching out to the HOL familyLFMTPJul 07 10:00
Rodolphe Lepigre and Christophe RaffalliAbstract Representation of Binders in OCaml using the Bindlib LibraryLFMTPJul 07 17:00
Ulysse Gérard and Dale MillerFunctional programming with λ-tree syntax: a progress reportLFMTPJul 07 17:30
Kaustuv Chaudhuri, Ulysse Gérard and Dale MillerComputation-as-deduction in Abella: work in progressLFMTPJul 07 12:00
Francesco Komauli and Alberto MomiglianoProperty-Based Testing of Abstract Machines: an Experience ReportLFMTPJul 07 12:20
David Feller, Joe Wells, Sébastien Carlier and Fairouz KamareddineWhat Does This Notation Mean Anyway? BNF-Style Notation as it is actually usedLFMTPJul 07 15:00
Somesh JhaSemantic Adversarial Deep LearningCAVJul 16 11:00
Eran YahavFrom Programs to Interpretable Deep Models and BackCAVJul 14 14:00
Byron CookFormal reasoning about the security of AWSCAV
Ilya Grishchenko, Matteo Maffei and Clara SchneidewindFoundations and Tools for the Static Analysis of Ethereum smart contractsCAV
Bernhard Kragl and Shaz QadeerLayered Concurrent ProgramsCAV
Yuki Satake and Hiroshi UnnoPropositional Dynamic Logic for Higher-Order Functional ProgramsCAVJul 14 11:00
Grigory Fedyukovich, Yueling Zhang and Aarti GuptaSyntax-Guided Termination AnalysisCAVJul 14 11:15
Hazem Torfah, Bernd Finkbeiner and Christopher HahnModel Checking Quantitative HyperpropertiesCAVJul 14 11:30
Lauren Pick, Grigory Fedyukovich and Aarti GuptaExploiting Synchrony and Symmetry in Relational VerificationCAVJul 14 11:45
Lucas Cordeiro, Pascal Kesseli, Daniel Kroening, Peter Schrammel and Marek TrtikJBMC: A Bounded Model Checking Tool for Verifying Java BytecodeCAVJul 14 12:00
Kenneth McMillanEager Abstraction for Symbolic Model CheckingCAVJul 14 12:15
Gagandeep Singh, Markus Püschel and Martin VechevFast Numerical Program Analysis with Reinforcement Learning CAVJul 14 15:00
Anna Becchi and Enea ZaffanellaA Direct Encoding for NNC PolyhedraCAVJul 14 15:15
S. Akshay, Supratik Chakraborty, Shubham Goel, Sumith Kulal and Shetal ShahWhat’s hard about Boolean Functional Synthesis?CAVJul 14 16:00
Alessandro Abate, Cristina David, Pascal Kesseli, Daniel Kroening and Elizabeth PolgreenCounterexample Guided Inductive Synthesis Modulo TheoriesCAVJul 14 16:15
Bernd Finkbeiner, Leander Tentrup, Marvin Stenger, Philip Lukert and Christopher HahnSynthesizing Reactive Systems from HyperpropertiesCAVJul 14 16:30
Daniel J. Fremont and Sanjit A. SeshiaReactive Control ImprovisationCAVJul 14 16:45
Aws Albarghouthi and Justin HsuConstraint-Based Synthesis of Coupling ProofsCAVJul 14 17:00
Chuchu Fan, Umang Mathur, Sayan Mitra and Mahesh ViswanathanController Synthesis Made Real: Reach-avoid Specifications and Linear DynamicsCAVJul 14 17:15
Suguman Bansal, Kedar Namjoshi and Yaniv Sa'ArSynthesis Of Asynchronous Reactive Programs From Temporal SpecificationsCAVJul 14 17:30
Qinheping Hu and Loris D'AntoniSyntax Guided Synthesis with Quantitative Syntactic ObjectivesCAVJul 14 17:45
Xinyu Wang, Greg Anderson, Isil Dillig and Ken McMillanLearning Abstractions for Program SynthesisCAVJul 15 10:00
George Argyros and Loris D'AntoniThe Learnability of Symbolic AutomataCAVJul 15 10:15
Hui Kong, Ezio Bartocci and Tom HenzingerReachable Set Over-approximation for Nonlinear Systems Using Piecewise Barrier TubesCAVJul 15 11:00
Goran Frehse, Mirco Giacobbe and Thomas HenzingerSpace-time InterpolantsCAVJul 15 11:15
Michael Emmi and Constantin EneaMonitoring Weak ConsistencyCAVJul 15 11:30
Yijun Feng, Joost-Pieter Katoen, Haokun Li, Bican Xia and Naijun ZhanMonitoring CTMCs By Multi-Clock Timed AutomataCAVJul 15 11:45
Frederik M. Bønneland, Peter Gjøl Jensen, Kim Guldstrand Larsen, Marco Muñiz and Jiri SrbaStart Pruning When Time Gets Urgent: Partial Order Reduction for Timed SystemsCAVJul 15 12:00
Ezio Bartocci, Roderick Bloem, Dejan Nickovic and Franz RoeckA Counting Semantics for Monitoring LTL Specifications over Finite TracesCAVJul 15 12:15
Jan Kretinsky, Tobias Meggendorfer, Salomon Sickert and Christopher ZieglerRabinizer 4: From LTL to Your Favourite Deterministic AutomatonCAVJul 15 14:00
Philipp J. Meyer, Salomon Sickert and Michael LuttenbergerStrix: Explicit Reactive Synthesis Strikes Back!CAVJul 15 14:15
Aina Niemetz, Mathias Preiner, Clifford Wolf and Armin BiereBTOR2, BtorMC and Boolector 3.0CAVJul 15 14:30
Marco Eilers and Peter MüllerNagini: A Static Verifier for PythonCAVJul 15 14:45
Michael Blondin, Javier Esparza and Stefan JaaxPeregrine: A Tool for the Analysis of Population ProtocolsCAVJul 15 15:00
Milan Ceska, Jiri Matyas, Vojtech Mrazek, Lukas Sekanina, Zdenek Vasicek and Tomas VojnarADAC: Automated Design of Approximate CircuitsCAVJul 15 15:15
Edon Kelmendi, Julia Krämer, Jan Kretinsky and Maximilian WeiningerValue Iteration for Simple Stochastic Games: Stopping Criterion and Learning AlgorithmCAVJul 15 16:00
Tim Quatmann and Joost-Pieter KatoenSound Value IterationCAVJul 15 16:15
Weichao Zhou and Wenchao LiSafety-Aware Apprenticeship LearningCAVJul 15 16:30
Qiyi Tang and Franck van BreugelDeciding Probabilistic Bisimilarity Distance One for Labelled Markov ChainsCAVJul 15 16:45
Hannah Arndt, Christina Jansen, Joost-Pieter Katoen, Christoph Matheja and Thomas NollLet this Graph be your Witness! An Attestor for Verifying Java Pointer ProgramsCAVJul 16 09:00
Mostafa Hassan, Caterina Urban, Marco Eilers and Peter MüllerMaxSMT-Based Type Inference for Python 3CAVJul 16 09:15
Andrew Gacek, John Backes, Michael Whalen, Lucas Wagner and Elaheh GhassabaniThe JKind Model CheckerCAVJul 16 09:30
Vincent Cheval, Steve Kremer and Itsaka RakotonirinaThe DEEPSEC proverCAVJul 16 09:45
Jianwen Li, Rohit Dureja, Geguang Pu, Kristin Yvonne Rozier and Moshe VardiSimpleCAR: An Efficient Bug-Finding Tool Based On Approximate ReachabilityCAVJul 16 10:00
Dmitry Blotsky, Federico Mora, Murphy Berzish, Yunhui Zheng, Ifaz Kabir and Vijay GaneshStringFuzz: A Fuzzer for String SolversCAVJul 16 10:15
Jérôme Dohrau, Alexander J Summers, Caterina Urban, Severin Münger and Peter MüllerPermission Inference for Array ProgramsCAVJul 16 12:00
Patrick Cousot, Roberto Giacobazzi and Francesco RanzatoProgram Analysis is Harder than Verification: A Computability PerspectiveCAVJul 16 12:15
Suguman Bansal, Swarat Chaudhuri and Moshe VardiAutomata vs Linear-Programming Discounted-Sum InclusionCAVJul 17 09:00
Matthew Bauer, Rohit Chadha, Mahesh Viswanathan and Prasad SistlaModel checking indistinguishability of randomized security protocolsCAVJul 17 09:15
Weikun Yang, Yakir Vizel, Pramod Subramanyan, Aarti Gupta and Sharad MalikLazy Self-Composition for Security VerificationCAVJul 17 09:30
Jun Zhang, Pengfei Gao, Fu Song and Chao WangSCInfer: Refinement-based Verification of Software Countermeasures against Side-Channel AttacksCAVJul 17 09:45
Krishnendu Chatterjee, Monika Henzinger, Veronika Loitzenbauer, Simin Oraee and Viktor TomanSymbolic Algorithms for Graphs and Markov Decision Processes with Fairness ObjectivesCAVJul 17 10:00
Tom van DijkAttracting Tangles to Solve Parity GamesCAVJul 17 10:15
Soonho Kong, Armando Solar-Lezama and Sicun GaoDelta-Decision Procedures for Exists-Forall Problems over the RealsCAVJul 17 11:00
Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark Barrett and Cesare TinelliSolving Quantified Bit-Vectors using Invertibility ConditionsCAVJul 17 11:15
Markus N. Rabe, Leander Tentrup, Cameron Rasmussen and Sanjit A. SeshiaUnderstanding and Extending Incremental Determinization for 2QBFCAVJul 17 11:30
Robert Robere, Antonina Kolokolova and Vijay GaneshThe Proof Complexity of SMT SolversCAVJul 17 11:45
Benjamin Farinier, Sebastien Bardin, Richard Bonichon and Marie-Laure PotetModel Generation for Quantified Formulas: A Taint-Based ApproachCAVJul 17 12:00
Xinhao Yuan, Junfeng Yang and Ronghui GuPartial Order Aware Concurrency SamplingCAVJul 17 14:00
Ahmed Bouajjani, Constantin Enea, Suha Orhun Mutluergil and Serdar TasiranReasoning About TSO Programs Using Reduction and AbstractionCAVJul 17 14:15
Huyen T.T. Nguyen, Cesar Rodriguez, Marcelo Sousa, Camille Coti and Laure PetrucciQuasi-Optimal Partial Order ReductionCAVJul 17 14:30
Ahmed Bouajjani, Constantin Enea, Kailiang Ji and Shaz QadeerOn the Completeness of Verifying Message Passing Programs under Bounded AsynchronyCAVJul 17 14:45
Elvira Albert, Miguel Gomez-Zamalloa, Miguel Isabel and Albert RubioConstrained Dynamic Partial Order ReductionCAVJul 17 15:00
Mark Tullsen, Lee Pike, Nathan Collins and Aaron TombFormal Verification of a Vehicle-to-Vehicle (V2V) Messaging SystemCAVJul 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 WestbrookContinuous formal verification of Amazon s2nCAVJul 17 16:15
Daniel Schemmel, Julian Büning, Oscar Soria Dustmann, Thomas Noll and Klaus WehrleSymbolic Liveness Analysis of Real-World SoftwareCAVJul 17 16:30
Byron Cook, Kareem Khazem, Daniel Kroening, Serdar Tasiran, Michael Tautschnig and Mark R. TuttleModel Checking Boot Code from AWS Data CentersCAVJul 17 16:45
Taolue Chen, Jinlong He, Fu Song, Guozhen Wang, Zhilin Wu and Jun YanAndroid Stack MachineCAVJul 17 17:00
Christoph WaltherFormally Verified Montgomery MultiplicationCAVJul 17 17:15
Eric Goubault, Sylvie Putot and Lorenz SahlmanInner and Outer Approximating Flowpipes for Delay Differential EquationsCAVJul 17 17:30
David LangworthyTLA+ in Engineering Systems – QuinceañeraTLA
Valentin SchneiderModeling Virtual Machines and Interrupts in TLA+ & PlusCalTLA
William SchultzAn Animation Module For TLA+TLA
Igor Konnov, Jure Kukovec and Thanh Hai TranBMCMT: Bounded Model Checking of TLA+ Specifications with SMTTLA
Stefan ReschApplying TLA+ in a Safety-Critical Railway ProjectTLA
Markus KuppeState Space Explosion or: How To Fight An Uphill BattleTLA
Ioannis Filippidis and Richard M. MurrayProving properties of a minimal covering algorithmTLA
Yanhong A. Liu, Scott D. Stoller, Saksham Chand and Xuetian WengInvariants in Distributed AlgorithmsTLA
Thorsten Ehlers and Dirk NowotkaTuning Parallel SAT SolversPOSJul 07 09:00
Anastasia Leventi-Peetz, Oliver Zendel, Werner Lennartz and Kai WeberCryptoMiniSat Parameter-Optimization for Solving Cryptographic InstancesPOSJul 07 09:30
Adrian Rebola Pardo and Armin BiereTwo flavors of DRATPOSJul 07 11:00
Michał Karpiński and Marek PiotrówCompetitive Sorter-based Encoding of PB-Constraints into SATPOSJul 07 11:30
Markus Iser and Carsten SinzA Problem Meta-Data Library for Research in SATPOSJul 07 16:00
Armin Biere and Marijn HeuleThe Effect of Scrambling CNFsPOSJul 07 16:30
Richard WallacePartial (Neighbourhood) Singleton Arc Consistency for Constraint Satisfaction ProblemsRCRAJul 13 14:22
Neng-Fa Zhou and Håkan KjellerstrandEncoding PB Constraints into SAT via Binary Adders and BDDs -- RevisitedRCRAJul 13 14:44
Slimane Abou-Msabah, Ahmed Riadh Baba Ali and Basma SAGERAn Enhanced Genetic Algorithm with the BLF2G Guillotine Placement Heuristic for the Orthogonal Cutting-Stock ProblemRCRAJul 13 12:06
Marco Baioletti, Alfredo Milani and Valentino SantucciAlgebraic Crossover Operators for PermutationsRCRAJul 13 11:44
Mauro VallatiOn the Configuration of SAT FormulaeRCRAJul 13 15:06
Giovanni Amendola, Carmine Dodaro, Wolfgang Faber and Francesco RiccaExternally Supported Models for Efficient Computation of Paracoherent Answer SetsRCRAJul 13 11:22
Marco Gavanelli, Maddalena Nonato, Andrea Peano and Davide BertozziLogic Programming approaches for routing fault-free and maximally-parallel Wavelength Routed Optical Networks on Chip (Application paper)RCRAJul 13 10:06
Richard WallaceReplaceability for constraint satisfaction problems: Algorithms, Inferences, and Complexity PatternsRCRAJul 13 14:00
Angelo Oddi and Riccardo RasconiGreedy Randomized Search for Scalable Compilation of Quantum CircuitsRCRAJul 13 09:44
Paul TarauShaving with Occam's Razor: Deriving Minimalist Theorem Provers for Minimal LogicRCRAJul 13 11:00
Toni Mancini, Enrico Tronci, Agostino Scialanca, Filiberto Lanciotti, Alberto Finzi, Riccardo Guarneri and Silvia Di PompeoOptimal Fault-Tolerant Placement of Relay Nodes in a Mission Critical Wireless NetworkRCRAJul 13 09:22
Toni Mancini, Federico Mari, Annalisa Massini, Igor Melatti, Ivano Salvo, Stefano Sinisi, Enrico Tronci, Rainald Ehrig, Susanna Röblitz and Brigitte LeenersComputing Personalised Treatments through In Silico Clinical Trials. A Case Study on Downregulation in Assisted Reproduction.RCRAJul 13 09:00
Paventhan VivekanandanA Homotopical Approach to CryptographyFCSJul 08 15:00
Alexandre Debant, Stephanie Delaune and Cyrille WiedlingProving physical proximity using symbolic modelsFCSJul 08 11:30
Musab A. Alturki, Max Kanovich, Tajana Ban Kirigin, Vivek Nigam, Andre Scedrov and Carolyn TalcottStatistical Model Checking of Guessing and Timing Attacks on Distance-bounding ProtocolsFCSJul 08 12:00
Alix TrieuA Study on the Preservation on Cryptographic Constant-Time Security in the CompCert CompilerFCSJul 08 14:00
Daniel Dougherty, Joshua Guttman and John RamsdellHomomorphisms and Minimality for Enrich-by-Need Security AnalysisFCSJul 08 14:30
Luca Arnaboldi and Charles MorissetLISA: Predicting the Impact of DoS Attacks on Real-World Low Power IoT SystemsFCSJul 08 10:00
Jiaming Jiang, Rada Chirkova, Jon Doyle and Arnon RosenthalAn Expressive, Flexible and Uniform Logical Formalism for Attribute-based Access ControlFCSJul 08 11:00
Charlie Jacomme and Steve KremerAn extensive formal analysis of multi-factor authentication protocolsCSFJul 09 11:00
Bruno BlanchetComposition Theorems for CryptoVerif and Application to TLS 1.3CSFJul 09 11:30
Patrick Thomas Eugster, Giorgia Azzurra Marson and Bertram PoetteringA Cryptographic Look at Multi-Party ChannelsCSFJul 09 12:00
Ilia Lebedev, Kyle Hogan and Srini DevadasSecure Boot and Remote Attestation in the Sanctum ProcessorCSF
Maxime Audinot, Sophie Pinchinat and Barbara KordyGuided design of attack trees: a system-based approachCSFJul 09 15:00
Marc Fischlin and Sogol MazaheriSelf-Guarding Cryptographic Protocols against Algorithm Substitution AttacksCSFJul 10 09:00
Cécile Baritel-Ruet, François Dupressoir, Pierre-Alain Fouque and Benjamin GrégoireFormal Security Proof of CMAC and its VariantsCSFJul 10 09:30
Marc Fischlin, Christian Janson and Sogol MazaheriBackdoored Hash Functions: Immunizing HMAC and HKDFCSFJul 10 10:00
Helene Haagh, Aleksandr Karbyshev, Sabine Oechsner, Bas Spitters and Pierre-Yves StrubComputer-aided proofs for multiparty computation with active securityCSFJul 10 11:00
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Hugo Pacheco, Vitor Pereira and Bernardo PortelaEnforcing ideal-world leakage bounds in real-world secret sharing MPC frameworksCSFJul 10 11:30
Baiyu Li and Daniele MicciancioSymbolic security of garbled circuitsCSFJul 10 12:00
Borzoo Bonakdarpour and Bernd FinkbeinerThe Complexity of Monitoring HyperpropertiesCSFJul 10 14:00
Mckenna McCall, Hengruo Zhang and Limin JiaKnowledge-based Security of Dynamic Secrets for Reactive ProgramsCSFJul 10 14:30
Andrey Chudnov and David NaumannAssuming you know: epistemic semantics of relational annotations for expressive flow policiesCSFJul 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 RosuKEVM: A Complete Formal Semantics of the Ethereum Virtual MachineCSFJul 10 16:00
Hongxu Chen, Alwen Tiu, Zhiwu Xu and Yang LiuA Permission-Dependent Type System for Secure Information Flow AnalysisCSFJul 11 09:00
Vineet Rajani and Deepak GargTypes for Information Flow Control: Labeling Granularity and Semantic ModelsCSFJul 11 09:30
Christian Müller, Helmut Seidl and Eugen ZalinescuInductive Invariants for Noninterference in Multi-agent WorkflowsCSFJul 11 10:00
Mario S. Alvim, Kostas Chatzikokolakis, Catuscia Palamidessi and Anna PaziiLocal Differential Privacy on Metric Spaces: optimizing the trade-off with utilityCSF
Samuel Yeom, Irene Giacomelli, Matt Fredrikson and Somesh JhaPrivacy Risk in Machine Learning: Analyzing the Connection to OverfittingCSFJul 11 12:00
David Basin, Sasa Radomirovic and Lara SchmidAlethea: A Provably Secure Random Sample Voting ProtocolCSFJul 11 16:00
Véronique Cortier, Constantin Cătălin Dragan, François Dupressoir and Bogdan WarinschiMachine-checked proofs for electronic voting: privacy and verifiability for BeleniosCSFJul 11 16:30
Pasquale Malacaria, Mhr Khouzani, Corina Pasareanu, Quoc-Sang Phan and Kasper LuckowSymbolic Side-Channel Analysis for Probabilistic ProgramsCSFJul 12 09:30
Gilles Barthe, Benjamin Grégoire and Vincent LaporteSecure compilation of side-channel countermeasures: the case of cryptographic “constant-time”CSFJul 12 10:00
Vincent Cheval, Veronique Cortier and Mathieu TuruaniA little more conversation, a little less action, a lot more satisfaction: Global states in ProVerif.CSFJul 12 11:00
Jannik Dreier, Lucca Hirschi, Sasa Radomirovic and Ralf SasseAutomated Unbounded Verification of Stateful Cryptographic Protocols with Exclusive ORCSFJul 12 11:30
Andreas Viktor Hess and Sebastian A. MödersheimA Typing Result for Stateful ProtocolsCSFJul 12 12:00
Sandra AlvesTermination of lambda-calculus linearization methodsLinearity/TLLA
Iliano Cervesato, Sharjeel Khan, Giselle Reis and Dragisa ZunicFormalization of Automated Trading Systems in a Concurrent Linear FrameworkLinearity/TLLAJul 08 17:20
Zeinab GalalTowards a Functional Language for Species of StructuresLinearity/TLLAJul 08 09:00
Masahito HasegawaFrom Linear Logic to Cyclic SharingLinearity/TLLAJul 07 14:55
Jiaming Jiang, Harley Eades Iii and Valeria de PaivaOn the Lambek Calculus with an Exchange ModalityLinearity/TLLAJul 07 09:20
Marie Kerjean and Yoann DabrowskiModels of Linear Logic based on the Schwartz epsilon productLinearity/TLLAJul 08 12:00
Wen Kokke, Fabrizio Montesi and Marco PeressottiTaking Linear Logic ApartLinearity/TLLAJul 07 12:00
Pierre LescanneHow to count linear and affine closed lambda terms?Linearity/TLLAJul 08 09:20
Zhaohui LuoSubstructural Calculi with Dependent TypesLinearity/TLLAJul 07 09:00
Roberto MaieliThe structure of non decomposable connectives of linear logicLinearity/TLLAJul 07 14:00
Giulio Manzonetto and Giulio GuerrieriThe Bang Calculus and the Two Girard's TranslationsLinearity/TLLAJul 07 09:55
Lê Thành Dũng Nguyễn and Thomas SeillerCoherent interaction graphs: a nondeterministic geometry of interaction for MLLLinearity/TLLAJul 08 14:55
Lê Thành Dũng Nguyễn and Thomas SeillerA semantic conjecture on second-order MLL and its complexity consequences (work in progress)Linearity/TLLAJul 08 17:00
Carlos Olarte, Valeria de Paiva, Elaine Pimentel and Giselle ReisBenchmarking Linear Logic TranslationsLinearity/TLLAJul 08 14:20
Luca Paolini, Luca Roversi and Margherita ZorziQuantum programming made easyLinearity/TLLAJul 07 17:35
Luc PellissierGeneralized generalized species of structure and resource modalitiesLinearity/TLLAJul 08 14:00
Luc Pellissier and Thomas SeillerEntropy and Complexity Lower BoundsLinearity/TLLAJul 08 09:55
Paolo PistoneProof nets, coends and the Yoneda isomorphismLinearity/TLLAJul 07 17:00
Lionel Vaux Auclair and Federico OlimpieriOn the Taylor expansion of λ-terms and the groupoid structure of their rigid approximantsLinearity/TLLAJul 07 14:20
Magnus O. MyreenThe CakeML Verified Compiler and ToolchainPAARJul 19 09:00
Ahmed Bhayat and Giles RegerSet of Support for Higher-Order ReasoningPAARJul 19 14:30
Gabriel Ebner and Matthias SchlaipferEfficient translation of sequent calculus proofs into natural deduction proofsPAARJul 19 14:00
Ullrich Hustadt, Cláudia Nalon and Clare DixonEvaluating Pre-Processing Techniques for the Separated Normal Form for Temporal LogicsPAARJul 19 15:00
Jens OttenProof Search Optimizations for Non-clausal Connection CalculiPAARJul 19 11:30
Michael Rawson and Giles RegerDynamic Strategy Priority: Empower the strong and abandon the weakPAARJul 19 10:00
Geoff Sutcliffe and Evgenii KotelnikovTFX: The TPTP Extended Typed First-order FormPAARJul 19 12:00
Jørgen Villadsen, Anders Schlichtkrull and Andreas Halkjær FromA Verified Simple Prover for First-Order LogicPAARJul 19 11:00
Karine Even-Mendoza, Sepideh Asadi, Antti Hyvärinen, Hana Chockler and Natasha SharyginaLattice-Based Refinement in Bounded Model CheckingVSTTEJul 18 12:00
Jan Steffen BeckerAnalyzing Consistency of Formal RequirementsAVOCSJul 18 16:00
Claire Dross, Guillaume Foliard, Théo Jouanny, Lionel Matias, Stuart Matthews, Jean-Marc Mota, Yannick Moy, Pascal Pignard and Romain SoulatClimbing the Software Assurance Ladder - Practical Formal Verification for Reliable SoftwareAVOCSJul 19 11:30
Rebeka Farkas, Tamás Tóth, Ákos Hajdu and András VörösBackward reachability analysis for timed automata with data variablesAVOCSJul 18 11:30
Radu Iosif and Cristina SerbanAn Entailment Checker for Separation Logic with Inductive DefinitionsAVOCSJul 18 12:00
Najes Jomaa, Paolo Torrini, David Nowak, Gilles Grimaud and Samuel HymProof-Oriented Design of a Separation Kernel with Minimal Trusted Computing BaseAVOCSJul 19 16:30
Eduard KamburjanDetecting Deadlocks in Formal System Models with Condition SynchronizationAVOCSJul 18 11:00
Christophe Limbrée and Charles PecheurA Framework for the Formal Verification of Networks of Railway Interlockings - Application to the Belgian RailwaysAVOCSJul 19 12:00
Eric Madelaine, Simon Bliutze, Xudong Qin and Min ZhangUsing SMT engine to generate Symbolic AutomataAVOCSJul 19 11:00
Jessica Petrasch, Jan-Hendrik Oepen, Sebastian Krings and Moritz GerickeWriting a Model Checker in 80 Days: Reusable Libraries and Custom ImplementationAVOCSJul 18 17:00
Nicolas Schnepf, Rémi Badonnel, Abdelkader Lahmadi and Stephan MerzRule-Based Synthesis of Chains of Security Functions for Software-Defined NetworksAVOCSJul 19 16:00
Matt Webster, Michael Breza, Clare Dixon, Michael Fisher and Julie McCannFormal Verification of Synchronisation, Gossip and Environmental Effects for Critical IoT SystemsAVOCSJul 18 16:30
Anuj Dawar and Erich GrädelPrefaceLICS
Michael Blondin, Javier Esparza, Stefan Jaax and Antonin KučeraBlack Ninjas in the Dark: Formal Analysis of Population ProtocolsLICS
Thierry CoquandInner Models of UnivalenceLICS
Peter O'HearnContinuous Reasoning: Scaling the Impact of Formal MethodsLICS
Ki Yung Ahn, Ross Horne, Shang-Wei Lin and Alwen TiuQuasi-Open Bisimilarity with Mismatch is IntuitionisticLICSJul 09 15:00
S. Akshay, Blaise Genest and Nikhil VyasDistribution-based objectives for Markov Decision ProcessesLICSJul 10 15:40
Joel Allred and Ulrich Ultes-NitscheA Simple and Optimal Complementation Algorithm for Büchi AutomataLICSJul 09 16:20
Robert AtkeyThe Syntax and Semantics of Quantitative Type TheoryLICSJul 11 12:20
Albert Atserias and Joanna OchremiakDefinable Ellipsoid Method, Sums-of-Squares Proofs, and the Isomorphism ProblemLICSJul 12 12:20
Steve Awodey, Jonas Frey and Sam SpeightImpredicative Encodings of (Higher) Inductive TypesLICSJul 10 11:00
Christel Baier, Nathalie Bertrand, Clemens Dubslaff, Daniel Gburek and Ocan SankurStochastic Shortest Paths and Weight-Bounded Properties in Markov Decision ProcessesLICSJul 10 16:00
Valentin Blot and James LairdExtensional and Intensional Semantic Universes: A Denotational Model of Dependent TypesLICSJul 11 11:20
Manuel Bodirsky, Florent Madelaine and Antoine MottetA universal-algebraic proof of the complexity dichotomy for Monotone Monadic SNPLICSJul 11 11:20
Brandon Bohrer and André PlatzerA Hybrid, Dynamic Logic for Hybrid-Dynamic Information FlowLICSJul 12 15:00
Mikolaj Bojanczyk, Laure Daviaud and Krishna Shankara NarayananRegular and First Order List FunctionsLICSJul 09 12:20
Mikołaj Bojańczyk, Martin Grohe and Michał PilipczukDefinable decompositions for graphs of bounded linear cliquewidthLICSJul 09 11:00
Mikołaj Bojańczyk and Szymon ToruńczykOn computability and tractability for infinite setsLICSJul 12 12:00
Udi Boker and Yariv ShaulianAutomaton-Based Criteria for Membership in CTLLICSJul 09 17:00
Filippo Bonchi, Fabio Gadducci, Aleks Kissinger, Pawel Sobocinski and Fabio ZanasiRewriting with FrobeniusLICSJul 12 15:00
Filippo Bonchi, Pierre Ganty, Roberto Giacobazzi and Dusko PavlovicSound up-to techniques and Complete abstract domainsLICSJul 09 17:00
Tomas Brazdil, Krishnendu Chatterjee, Antonin Kucera, Petr Novotný, Dominik Velan and Florian ZulegerEfficient Algorithms for Asymptotic Bounds on Termination Time in VASSLICSJul 12 14:40
Roberto Bruni, Hernan Melgratti and Ugo MontanariConcurrency and Probability: Removing Confusion, CompositionallyLICSJul 09 14:00
Ulrik Buchholtz, Floris van Doorn and Egbert RijkeHigher Groups in Homotopy Type TheoryLICSJul 09 12:00
Simon Castellan, Pierre Clairambault, Hugo Paquet and Glynn WinskelThe concurrent game semantics of Probabilistic PCFLICSJul 10 16:20
Yijia Chen and Jörg FlumTree depth, quantifier elimination, and quantifier rankLICSJul 10 11:40
Yijia Chen, Moritz Mueller and Keita YokoyamaA parameterized halting problem, the linear time hierarchy, and the MRDP theoremLICSJul 09 12:00
Liron Cohen, Vincent Rahli, Mark Bickford and Robert ConstableComputability Beyond Church-Turing via Choice SequencesLICSJul 11 12:00
Thierry Coquand, Simon Huber and Anders MörtbergOn Higher Inductive Types in Cubical Type TheoryLICSJul 11 10:20
Karl CraryStrong Sums in Focused LogicLICSJul 09 12:20
Raphaëlle CrubilléProbabilistic stable functions on discrete cones are power series.LICSJul 12 14:00
Daniel Danielski and Emanuel KieronskiUnary negation fragment with equivalence relations has the finite model propertyLICSJul 11 11:40
Luc Dartois, Emmanuel Filiot and Nathan LhoteLogics for Word Transductions with SynthesisLICSJul 10 14:40
Ankush Das, Jan Hoffmann and Frank PfenningWork Analysis with Resource-Aware Session TypesLICSJul 10 11:40
Vrunda Dave, Paul Gastin and Krishna SRegular Transducer Expressions for Regular Transformations over infinite wordsLICSJul 09 17:40
Laure Daviaud, Marcin Jurdzinski and Ranko LazicA pseudo-quasi-polynomial algorithm for solving mean-payoff parity gamesLICSJul 09 14:20
Nadish de SilvaLogical paradoxes in quantum computationLICSJul 12 09:20
Romain Demangeon and Nobuko YoshidaCausal Computational Complexity of Distributed ProcessesLICSJul 09 15:20
Arnaud Durand, Anselm Haak and Heribert VollmerModel-Theoretic Characterizations of Boolean and Arithmetic Circuit Classes of Small DepthLICSJul 10 11:20
Adrien Durier, Daniel Hirschkoff and Davide SangiorgiEager Functions as ProcessesLICSJul 09 14:40
Clovis Eberhart and Tom HirschowitzWhat's in a game? A theory of game modelsLICSJul 10 15:40
Javier Esparza, Jan Kretinsky and Salomon SickertOne Theorem to Rule Them All: A Unified Translation of LTL into $\omega$-AutomataLICSJul 09 16:00
Thomas Ferrère, Thomas A Henzinger and N Ege SaracA Theory of Register MonitorsLICSJul 12 14:20
Diego Figueira and M. PraveenPlaying with Repetitions in Data Words Using Energy GamesLICSJul 09 15:00
Nathanaël FijalkowThe State Complexity of Alternating AutomataLICSJul 09 16:40
Emmanuel Filiot, Raffaella Gentilini and Jean-Francois RaskinRational Synthesis Under Imperfect InformationLICSJul 09 14:40
Dror Fried, Axel Legay, Joel Ouaknine and Moshe Y VardiSequential Relational DecompositionLICSJul 09 11:40
Dan Frumin, Robbert Krebbers and Lars BirkedalReLoC: A Mechanised Relational Logic for Fine-Grained ConcurrencyLICSJul 09 14:20
Francesco GavazzoQuantitative Behavioural Reasoning for Higher-order Effectful Programs: Applicative DistancesLICSJul 12 09:00
Guillaume GeoffroyClassical realizability as a classifier for nondeterminismLICSJul 10 12:20
Neil Ghani, Jules Hedges, Viktor Winschel and Philipp ZahnCompositional game theoryLICSJul 09 15:20
Adrien GuattoA Generalized Modality for RecursionLICSJul 12 09:20
Grzegorz Głuch, Jerzy Marcinkowski and Piotr Ostropolski-NalewajaCan One Escape Red Chains? Regular Path Queries Determinacy is Undecidable.LICSJul 11 12:20
Amar Hadzihasanovic, Kang Feng Ng and Quanlong WangTwo complete axiomatisations of pure-state qubit quantum computingLICSJul 12 10:00
Michael Hahn, Andreas Krebs and Howard StraubingWreath Products of Distributive Forest AlgebrasLICSJul 10 12:00
Kuen-Bang Hou and Ulrik BuchholtzCellular Cohomology in Homotopy Type TheoryLICSJul 09 11:20
Ehud Hrushovski, Joel Ouaknine, Amaury Pouly and James WorrellPolynomial Invariants for Affine ProgramsLICSJul 10 10:00
Dominic HughesUnification nets: canonical proof net quantifiersLICSJul 10 14:40
Pawel Idziak and Jacek KrzaczkowskiSatisfiability in multi-valued circuitsLICSJul 11 12:00
Emmanuel Jeandel, Simon Perdrix and Renaud VilmartA Complete Axiomatisation of the ZX-Calculus for Clifford+T Quantum MechanicsLICSJul 12 09:40
Emmanuel Jeandel, Simon Perdrix and Renaud VilmartDiagrammatic Reasoning beyond Clifford+T Quantum MechanicsLICSJul 12 10:20
Bruce Kapron and Florian SteinbergType-two polynomial-time and restricted lookahead.LICSJul 10 15:00
Marie KerjeanA Logical Account for Linear Partial Differential EquationsLICSJul 10 14:20
Nicolai Kraus and Thorsten AltenkirchFree Higher Groups in Homotopy Type TheoryLICSJul 09 11:40
Jan Kretinsky and Tobias MeggendorferConditional Value-at-Risk for Reachability and Mean Payoff in Markov Decision ProcessesLICSJul 10 16:20
Antti Kuusisto and Carsten LutzWeighted model counting beyond two-variable logicLICSJul 11 11:00
Olivier LaurentAround Classical and Intuitionistic Linear LogicsLICSJul 10 15:00
Karoliina LehtinenA modal mu perspective on solving parity games in quasipolynomial time.LICSJul 09 14:00
Thomas LeventisProbabilistic Böhm Trees and Probabilistic SeparationLICSJul 09 17:40
Bert Lindenhovius, Michael Mislove and Vladimir ZamdzhievEnriching a Linear/Non-linear Lambda Calculus: A Programming Language for String DiagramsLICSJul 09 16:00
Radu Mardare, Prakash Panangaden, Dexter Kozen, Dana Scott, Robert Furber and Giorgio BacciBoolean-Valued Semantics for Stochastic Lambda-CalculusLICSJul 09 16:40
Radu Mardare, Prakash Panangaden, Gordon Plotkin and Giorgio BacciAn algebraic theory of Markov processesLICSJul 09 16:20
Paul-André MellièsRibbon tensorial logicLICSJul 12 15:20
Paul-André Melliès and Léo StefanescoAn Asynchronous Soundness Theorem for Concurrent Separation LogicLICSJul 10 16:00
Matteo MioRiesz Modal Logic with Threshold OperatorsLICSJul 10 14:20
Étienne MiqueyA sequent calculus with dependent types for classical arithmeticLICSJul 11 10:00
Benoit MoninAn answer to the Gamma questionLICSJul 10 10:20
Sean Moss and Tamara von GlehnDialectica models of type theoryLICSJul 11 11:00
Koko Muroya, Wai-Tak Cheung and Dan GhicaThe Geometry of Computation-Graph AbstractionLICSJul 12 10:00
Yoji Nanjo, Hiroshi Unno, Eric Koskinen and Tachio TerauchiDependent Temporal Effects and Fixpoint Logic for VerificationLICSJul 11 11:40
Matthias NiewerthMSO Queries on Trees: Enumerating Answers under Updates Using Forest AlgebrasLICSJul 10 12:20
Andreas Nuyts and Dominique DevrieseDegrees of Relatedness - A Unified Framework for Parametricity, Irrelevance, Ad Hoc Polymorphism, Intersections, Unions and Algebra in Dependent Type TheoryLICSJul 12 10:20
Michał Pilipczuk, Sebastian Siebertz and Szymon ToruńczykParameterized circuit complexity of model-checking on sparse structuresLICSJul 09 11:20
Michał Pilipczuk, Sebastian Siebertz and Szymon ToruńczykOn the number of types in sparse graphsLICSJul 10 11:00
Maciej Piróg, Tom Schrijvers, Nicolas Wu and Mauro JaskelioffSyntax and Semantics for Operations with ScopesLICSJul 12 14:40
André Platzer and Yong Kiam TanDifferential Equation Axiomatization: The Impressive Power of Differential GhostsLICSJul 12 15:20
Damien Pous and Valeria VignudelliAllegories: decidability and graph homomorphismsLICSJul 12 14:20
Thomas PowellA functional interpretation with stateLICSJul 12 09:40
Colin Riba and Pierre PradicLMSO: A Curry-Howard Approach to Church's Synthesis via Linear LogicLICSJul 10 14:00
Benjamin Sherman, Luke Sciarappa, Michael Carbin and Adam ChlipalaComputable decision-making on the reals and other spaces via partiality and nondeterminismLICSJul 12 14:00
Kristina Sojakova and Patricia JohannA General Framework for Relational ParametricityLICSJul 10 12:00
Jonathan Sterling and Robert HarperGuarded Computational Type TheoryLICSJul 10 11:20
Takeshi Tsukada, Kazuyuki Asada and Luke OngSpecies, Profunctors and Taylor Expansion Weighted by SMCC--A Unified Framework for Modelling Nondeterministic, Probabilistic and Quantum Programs--LICSJul 12 09:00
Pierre VialEvery λ-Term is Meaningful for the Infinitary Relational ModelLICSJul 09 17:20
Paul Wild, Lutz Schröder, Dirk Pattinson and Barbara KönigA van Benthem Theorem for Fuzzy Modal LogicLICSJul 10 14:00
Noam ZeilbergerA theory of linear typings as flows on 3-valent graphsLICSJul 09 11:00
Georg ZetzschePTL-separability and closures for WQOs on wordsLICSJul 09 17:20
Patrick Bahr, Bassel Mannaa and Rasmus Ejlers MøgelbergWhat makes guarded types tick?PARISJul 07 17:15
Florian Bruse, Martin Lange and Etienne LozesCollapses of Fixpoint Alternation Hierarchies in Low Type-Levels of Higher-Order Fixpoint LogicPARISJul 07 11:45
David Cerna and Michael LettmannTowards the Automatic Construction of Schematic ProofsPARISJul 07 14:45
Anupam DasOn the logical complexity of cyclic arithmeticPARISJul 08 16:45
Yue Li and Ekaterina KomendantskayaCoinductive Uniform Proofs: An Extended AbstractPARISJul 08 11:45
Rémi NolletLocal validity for circular proofs in linear logic with fixed pointsPARISJul 07 11:00
Colin Riba and Pierre PradicLMSO: A Curry-Howard Approach to Church’s Synthesis via Linear LogicPARISJul 08 11:00
Reuben Rowe and Liron CohenTransitive Closure Logic: Infinitary and Cyclic Proof SystemsPARISJul 08 16:00
Sorin StratulatUseless Explicit Induction ReasoningPARISJul 07 14:00
Joshua Blinkhorn, Olaf Beyersdorff and Luke HindeSize, Cost and Capacity: A Semantic Technique for Hard Random QBFsPC
Maria Bonet, Sam Buss, Alexey Ignatiev, Joao Marques-Silva and Antonio MorgadoOn Dual-Rail Based MaxSAT SolvingPCJul 08 17:30
Florent CapelliProof systems for #SAT based on restricted circuitsPCJul 07 17:40
Judith ClymoShort Proofs in QBF ExpansionPC
Anupam DasTowards theories for positive polynomial time and monotone proofs with extensionPCJul 08 15:00
Mareike Dressler, Adam Kurpisz and Timo de WolffOptimization over the Boolean Hypercube via Sums of Nonnegative Circuit PolynomialsPCJul 08 17:00
Emil JeřábekBounded induction without parametersPC
Manuel Kauers and Martina SeidlThe Symmetry Rule for Quantified Boolean FormulasPC
Alexander KnopBranching Program Complexity of Canonical Search Problems and Proof Complexity of FormulasPCJul 07 15:00
Antonina KolokolovaComplexity of expander-based reasoning and the power of monotone proofsPCJul 08 14:30
Barnaby Martin, Stefan Dantchev and Nicola GalesiResolution and the binary encoding of combinatorial principlesPCJul 07 17:00
Fedor Part and Iddo TzameretResolution with Counting: Different Moduli and Tree-Like Lower BoundsPCJul 07 17:20
Calin BeltaFormal Synthesis of Control Strategies for Dynamical SystemsVaVAS
Radu Calinescu and Saud YonbawiTowards a Hierarchical-Control Architecture for Distributed Autonomous Systems (Extended Abstract - Paper)VaVASJul 18 10:00
Anna Lukina, Ashish Tiwari, Scott Smolka and Radu GrosuAdaptive Neighborhood Resizing for Stochastic Reachability in Multi-Agent SystemsVaVASJul 18 11:00
Thai Son Hoang, Naoto Sato, Tomoyuki Myojin, Michael Butler, Yuichiroh Nakagawa and Hideto OgawaPolicing Functions for Machine Learning SystemsVaVASJul 18 11:30
Julian Padget, Marina De Vos and Charlie PageSocial Consequence Engines (Abstract)VaVASJul 18 12:00
Jérémie GuiochetTrust me - I am autonomousVaVAS
Isidro Durazo-Cardenas, Andrew Starr and Tetsuo TomiyamaTowards validation and verification of an autonomous railway inspection and repair systemVaVAS
Ruben Giaquinta, Ruth Hoffmann, Murray Ireland, Alice Miller and Gethin NormanProbabilistic Model Checking for Autonomous Agent Strategy Synthesis - Extended AbstractVaVASJul 18 16:00
Mohammed Al-Nuaimi, Hongyang Qu and Sandor VeresTowards a verifiable decision making framework for self-driving vehiclesVaVASJul 18 16:30
Gleifer Alves, Louise Dennis and Michael FisherFormalisation of the Rules of the Road for embedding into an Autonomous Vehicle AgentVaVASJul 18 17:00
Florian LierReproducibility in Robotics - The Big 5 IssuesVaVAS
Alvaro Miyazawa, Ana Cavalcanti, Simon Foster, Wei Li, Pedro Ribeiro, Jon Timmis and Jim WoodcockRoboTool: Modelling and Verification with RoboChartVaVASJul 19 10:00
Bruno Lacerda, David Parker and Nick HawesPolicy Generation with Probabilistic Guarantees for Long-term Autonomy of a Mobile Service RobotVaVASJul 19 11:00
Mathias Fleury, Jasmin Christian Blanchette and Peter LammichA Verified SAT Solver with Watched Literals Using Imperative HOL (Extended Abstract)IsabelleJul 13 09:30
Andreas Lochbihler and Pascal StoopLazy Algebraic Types in Isabelle/HOLIsabelleJul 13 10:00
Max W. Haslbeck and René ThiemannFormal Verification of Bounds for the LLL Basis Reduction AlgorithmIsabelleJul 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 AryalHilbert Meets Isabelle: Formalisation of the DPRM Theorem in IsabelleIsabelleJul 13 11:30
Makarius WenzelFurther Scaling of Isabelle TechnologyIsabelleJul 13 12:00
Andreas Halkjær From, Anders Schlichtkrull and Jørgen VilladsenDrawing TreesIsabelle
Andreas Halkjær From, John Bruntse Larsen, Anders Schlichtkrull and Jørgen VilladsenSubstitutionless First-Order Logic: A Formal Soundness ProofIsabelleJul 13 16:00
Christian SternagelThe remote_build ToolIsabelleJul 13 16:15
Yutaka Nagashima and Yilun HePaMpeR: A Proof Method Recommendation System for Isabelle/HOLIsabelleJul 13 16:30
Joshua Bockenek, Peter Lammich, Yakoub Nemouchi and Burkhart WolffUsing Isabelle/UTP for the Verification of Sorting Algorithms: A Case StudyIsabelleJul 13 17:00
Eric HehnerA Theory of Lazy Imperative TimingREFINEJul 18 16:30
Ian J. HayesChallenges of specifying concurrent program componentsREFINEJul 18 11:00
Mathieu Montin and Marc PantelOrdering strict partial orders to model behavioural refinementREFINEJul 18 12:00
Marwa Ben Abdelali, Lamia Labed Jilani, Wided Ghardallou and Ali MiliProgramming Without RefinementREFINEJul 18 11:30
Graeme Smith, Kirsten Winter and Robert ColvinCorrectness of Concurrent Objects under Weak Memory ModelsREFINEJul 18 10:00
Emil Sekerinski and Shucai YaoRefining Santa: An Excercise in Efficient SynchronizationREFINEJul 18 16:00
Cynthia KopAutomatic Termination Analysis Using WANDAHOR
Naoki KobayashiOn Two Kinds of Higher-Order Model Checking and Higher-Order Program VerificationHOR
Pierre VialSome applications of quantitative types inside and outside type theoryHOR
Maciej Bendkowski and Pierre LescanneCombinatorics of explicit substitutions (extended abstract)HORJul 07 10:00
Federico OlimpieriNormalization and Taylor expansion of lambda-termsHORJul 07 16:00
Connor SmithOrthogonality and sequentiality in substructural Linear HRSsHORJul 07 12:00
Flavien BreuvartRefining Properties of Filter Models: Sensibility, Approximability and ReducibilityHORJul 07 15:00
Damiano Mazza and Domenico RuoppoloThe next 700 (type-theoretical) denotational models ?HORJul 07 16:30
Davide Giacomo CavezzaHeuristic-Based GR(1) Assumptions RefinementDS-FMJul 14 11:45
Georg NührenbergFormal verification of neural networksDS-FMJul 14 14:30
Dhriti KhannaAnalysis and Verification of Message Passing based Parallel ProgramsDS-FMJul 14 14:00
Simone VuottoConsistency Checking of Functional RequirementsDS-FMJul 14 15:00
Peter Backeman, Aleksandar Zeljić, Philipp Ruemmer and Christoph M. WintersteigerThe next 10^4 UppSAT ApproximationsSMTJul 12 11:30
Mohamed Iguernlala, Sylvain Conchon and Albin CoquereauAlt-Ergo 2.2SMTJul 12 12:00
Gergely Kovásznai, Csaba Biró and Balázs ErdélyiPuli - A Problem-Specific OMT SolverSMTJul 12 15:00
Leonardo Alt and Christian ReitwiessnerSMT-based Compile-time Verification of Safety Properties for Smart ContractsSMTJul 12 16:00
Arie Gurfinkel, Sharon Shoham and Yakir VizelDiscovering Universally Quantified Solutions for Constrained Horn ClausesSMTJul 13 14:00
Andrew Reynolds, Haniel Barbosa, Aina Niemetz, Andres Noetzli, Mathias Preiner, Clark Barrett and Cesare TinelliRewrites for SMT Solvers using Syntax-Guided EnumerationSMTJul 12 17:00
Haniel Barbosa, Andrew Reynolds, Pascal Fontaine, Daniel El Ouraoui and Cesare TinelliHigher-Order SMT SolvingSMTJul 13 10:00
François Bobot, Stephane Graham-Lengrand, Bruno Marre and Guillaume BuryCentralizing Equality Reasoning in MCSATSMTJul 13 11:00
Guillaume Bury, David Delahaye and Simon CruanesSMT Solving Modulo Tableau and Rewriting TheoriesSMTJul 12 16:30
Giles Reger and Martin RienerWhat is the Point of an SMT-LIB Problem?SMTJul 13 14:30
Delia KesnerQuantitative Types: from Foundations to ApplicationsITRS
Damiano MazzaPolyadic Approximations and Intersection TypesITRS
Paweł ParysIntersection Types for Unboundedness ProblemsITRS
Federico AschieriNatural Deduction and Normalization Proofs for the Intersection Type DisciplineITRSJul 08 11:00
Giulio GuerrieriTowards a Semantic Measure of the Execution Time in Call-by-Value lambda-CalculusITRSJul 08 12:00
Olivier LaurentIntersection Subtyping with ConstructorsITRSJul 08 16:00
Simona Ronchi Della Rocca and Daniele PautassoStrong normalization of simple types through uniform intersection types.ITRSJul 08 11:30
Richard StatmanOn sets of terms with a given intersection typeITRS
Pedro Ângelo and Mário FloridoGradual Intersection TypesITRSJul 08 15:00
Thibaut BenjaminTowards a fully formalized definition of syllepsis in weak higher categoriesHDRAJul 07 15:00
Cyrille Chenavier, Christophe Cordero and Samuele GiraudoGeneralizations of the associative operad and convergent rewrite systemsHDRAJul 07 17:00
Antonin Delpeuch and Jamie VicaryNormal forms for planar connected string diagramsHDRAJul 07 17:30
Benjamin DupontTermination in linear (2,2)-categories with braidings and dualsHDRAJul 07 12:00
Amar HadzihasanovicMerge-bicategories: towards semi-strictification of higher categoriesHDRAJul 07 10:00
Nohra Hage String data structures for Chinese monoidsHDRAJul 07 16:30
Cédric Ho ThanhThe equivalence between opetopic sets and many-to-one polygraphsHDRAJul 07 11:00
Richard StatmanMinimal Bacus FP is Turing CompleteHDRAJul 07 16:00
Pedro TamaroffMinimal models for monomial algebrasHDRAJul 07 11:30
Lawrence MossImplementations of Natural LogicsARQNL
Giles RegerSome thoughts about FOL-translations in VampireARQNL
Ahmad-Saher Azizi-SultanPseudo-Propositional LogicARQNLJul 18 15:00
Tomer LibalA Simple Semi-automated Proof Assistant for First-order Modal LogicsARQNLJul 18 11:30
Daniel Mery and Didier GalmicheLabelled Connection-based Proof Search for Multiplicative Intuitionistic Linear LogicARQNLJul 18 12:00
Eugenio Orlandelli and Giovanna CorsiLabelled calculi for QMLs with non-rigid and non-denoting termsARQNLJul 18 11:00
Alexander Steen and Christoph BenzmüllerSystem Demonstration: The Higher-Order Prover Leo-IIIARQNLJul 18 16:30
Wieger Wesselink and Tim WillemseEvidence Extraction from Parameterised Boolean Equation SystemsARQNLJul 18 10:00