René Thiemann and Akihisa YamadaEfficient Formalization of Simplification OrdersWST
Cynthia Kop and Deivid ValeTuple Interpretations and Applications to Higher-Order Runtime ComplexityWSTAug 11 09:00
Liye Guo and Cynthia KopA transitive HORPO for curried systemsWSTAug 11 09:30
Alfons Geser, Dieter Hofbauer and Johannes WaldmannApproximating Relative Match-BoundsWSTAug 11 10:00
Nao Hirokawa and Aart MiddeldorpHydra Battles and AC TerminationWSTAug 11 12:00
Florian Frohn and Carsten FuhsA Calculus for Modular Non-Termination Proofs by Loop AccelerationWSTAug 11 14:00
Marcel Hark, Florian Frohn and Jürgen GieslDeciding Termination of Uniform Loops with Polynomial Parameterized ComplexityWSTAug 11 14:30
Jürgen Giesl, Nils Lommen, Marcel Hark and Fabian MeyerImproved Automatic Complexity Analysis of Integer ProgramsWSTAug 11 15:00
Nils Lommen, Fabian Meyer, Marcel Hark and Jürgen GieslAutomatic Complexity Analysis of (Probabilistic) Integer Programs via KoATWSTAug 12 11:00
Christina Kohl and René ThiemannCeTA – A certifier for termCOMP 2022WSTAug 12 14:00
Johannes WaldmannCertified MatchboxWSTAug 12 14:20
Elvira Albert, Pablo Gordillo, Alejandro Hernández-Cerezo, Clara Rodríguez-Núñez and Albert RubioUsing Automated Reasoning Techniques for Enhancing the Efficiency and Security of (Ethereum) Smart ContractsIJCARAug 10 14:00
Gilles DowekFrom the Universality of Mathematical Truth to the Interoperability of Proof SystemsIJCARAug 08 09:00
Haniel Barbosa, Andrew Reynolds, Gereon Kremer, Hanna Lachnitt, Aina Niemetz, Andres Noetzli, Alex Ozdemir, Mathias Preiner, Arjun Viswanathan, Scott Viteri, Yoni Zohar, Cesare Tinelli and Clark BarrettFlexible Proof Production in an Industrial-Strength SMT SolverIJCARAug 10 12:00
Paolo Felli, Marco Montali and Sarah WinklerCTL* Model Checking for Data-Aware Dynamic Systems with ArithmeticIJCARAug 10 09:00
Mauro Ferrari and Camillo FiorentiniSAT-based Proof Search in Intermediate Propositional LogicsIJCARAug 08 16:00
Hannes Ihalainen, Jeremias Berg and Matti JärvisaloClause Redundancy and Preprocessing in Maximum SatisfiabilityIJCARAug 08 16:40
Gereon Kremer, Andrew Reynolds, Clark Barrett and Cesare TinelliCooperating Techniques for Solving Nonlinear Arithmetic in the cvc5 SMT Solver (System Description)IJCARAug 08 10:00
Joseph Reeves, Marijn Heule and Randal BryantPreprocessing of Propagation Redundant ClausesIJCARAug 08 16:20
Ying Sheng, Andres Noetzli, Andrew Reynolds, Yoni Zohar, David Dill, Wolfgang Grieskamp, Junkil Park, Shaz Qadeer, Clark Barrett and Cesare TinelliReasoning About Vectors using an SMT Theory of SequencesIJCARAug 10 11:40
Martin Bromberger, Lorenz Leutgeb and Christoph WeidenbachAn Efficient Subsumption Test Pipeline for BS(LRA) ClausesIJCARAug 08 12:00
André Duarte and Konstantin KorovinGround Joinability and Connectedness in the Superposition CalculusIJCARAug 08 11:20
Fajar Haifani, Patrick Koopmann, Sophie Tourret and Christoph WeidenbachConnection-Minimal Abduction in EL via Translation to FOLIJCARAug 10 11:00
Fajar Haifani and Christoph WeidenbachSemantic RelevanceIJCARAug 09 14:35
Hendrik Leidinger and Christoph WeidenbachSCL(EQ): SCL for First-Order Logic with EqualityIJCARAug 08 11:00
Akihisa YamadaTerm Ordering for Non-Reachability of (Conditional) RewritingIJCARAug 08 11:40
Christian Alrabbaa, Franz Baader, Stefan Borgwardt, Raimund Dachselt, Patrick Koopmann and Julián MéndezEvonne: Interactive Proof Visualization for Description Logics (System Description)IJCARAug 08 14:55
Claudia Cauli, Magdalena Ortiz and Nir PitermanActions over Core-Closed Knowledge BasesIJCARAug 08 14:00
Tanel Tammet, Dirk Draheim and Priit JärvGK: Implementing Full First Order Default Logic for Commonsense Reasoning (System Description)IJCARAug 08 14:20
Hui Yang, Yue Ma and Nicole BidoitHypergraph-Based Inference Rules for Computing EL+-Ontology JustificationsIJCARAug 08 15:10
Michael Bernreiter, Anela Lolic, Jan Maly and Stefan WoltranSequent Calculi for Choice LogicsIJCARAug 09 09:00
Chad Brown and Cezary KaliszykLash 1.0 (System Description)IJCARAug 09 09:20
Julie Cailler, Johann Rosain, David Delahaye, Simon Robillard and Hinde BouzianeGoéland: A Concurrent Tableau-Based Theorem Prover (System Description)IJCARAug 09 09:35
Štěpán Holub, Martin Raška and Štěpán StarostaBinary Codes that do Not Preserve PrimitivityIJCARAug 09 10:10
Takuya Matsuzaki and Tomohiro FujitaFormula Simplification via Invariance Detection by Algebraically Indexed TypesIJCARAug 08 17:00
Michał Sochański, Dorota Leszczyńska-Jasion, Szymon Chlebowski, Agata Tomczyk and Marcin JukiewiczSynthetic Tableaux: Minimal Tableau Search HeuristicsIJCARAug 09 09:50
Marta Bilkova, Sabine Frittella and Daniil KozhemiachenkoParaconsistent Gödel Modal LogicIJCARAug 10 16:20
Eben Blaisdell, Max Kanovich, Stepan Kuznetsov, Elaine Pimentel and Andre ScedrovNon-associative, Non-commutative Multi-Modal Linear LogicIJCARAug 10 16:00
Ori Lahav and Yoni ZoharEffective Semantics for the Modal Logics K and KT via Non-deterministic MatricesIJCARAug 10 16:40
Cláudia Nalon, Ullrich Hustadt, Fabio Papacchini and Clare DixonLocal Reductions for the Modal CubeIJCARAug 08 14:35
Anupam Das and Marianna GirlandoCyclic Proofs, Hypersequents, and Transitive Closure LogicIJCARAug 09 11:40
Francisco Durán, Steven Eker, Santiago Escobar, Narciso Marti-Oliet, Jose Meseguer, Ruben Rubio and Carolyn TalcottEquational Unification and Matching, and Symbolic Reachability Analysis in Maude 3.2 (System Description)IJCARAug 09 14:55
Andrzej IndrzejczakLe\'sniewski's Ontology -- Proof-Theoretic CharacterizationIJCARAug 09 11:20
Chaitanya Mangla, Sean Holden and Paulson LarryBayesian Ranking for Strategy Scheduling in Automated Theorem ProversIJCARAug 09 14:00
Temur Kutsia and Cleo PauA Framework for Approximate Generalization in Quantitative TheoriesIJCARAug 09 15:10
Jelle Piepenbrock, Tom Heskes, Mikolas Janota and Josef UrbanGuiding an Automated Theorem Prover with Neural RewritingIJCARAug 10 15:00
Andrei PopescuRensets and Renaming-Based Recursion for Syntax with BindingsIJCARAug 09 12:00
Vitor Rodrigues Greati and Joao MarcosFinite Two-Dimensional Proof Systems for Non-finitely Axiomatizable LogicsIJCARAug 09 11:00
Martin SudaVampire Getting Noisy: Will Random Bits Help Conquer Chaos? (System Description)IJCARAug 09 14:20
S. Akshay, Supratik Chakraborty and Debtanu PalOn Eventual Non-negativity and Positivity for the Weighted Sum of Powers of MatricesIJCARAug 10 09:35
Marius Bozga, Lucas Bueri and Radu IosifDecision Problems in a Logic for Reasoning about Reconfigurable Distributed SystemsIJCARAug 10 11:20
Florian Frohn and Jürgen GieslProving Non-Termination and Lower Runtime Bounds with LoAT (System Description)IJCARAug 10 09:55
James Gallicchio, Yong Kiam Tan, Stefan Mitsch and André PlatzerImplicit Definitions with Differential Equations for KeYmaera X (System Description)IJCARAug 10 09:20
Nils Lommen, Fabian Meyer and Jürgen GieslAutomatic Complexity Analysis of Integer Programs via Triangular Weakly Non-Linear LoopsIJCARAug 10 10:10
Jianglin Lan, Yang Zheng and Alessio LomuscioTight Neural Network Verification via Semidefinite Relaxations and Linear ReformulationsFoMLASJul 31 11:00
Youcheng Sun, Muhammad Usman, Divya Gopinath and Corina PăsăreanuVPN: Verification of Poisoning in Neural NetworksFoMLASAug 01 09:30
Ravi Mangal and Corina PasareanuA Cascade of Checkers for Run-time Certification of Local RobustnessFoMLASJul 31 11:30
Haoze Wu, Clark Barrett, Mahmood Sharif, Nina Narodytska and Gagandeep SinghScalable Verification of GNN-based Job SchedulersFoMLASAug 01 09:00
João Batista Pereira Matos Júnior, Lucas C. Cordeiro, Edoardo Manino, Xidan Song and Iury BessaCEG4N: Counter-Example Guided Neural Network Quantization RefinementFoMLASJul 31 16:00
Natan Levy and Guy KatzRoMA: a Method for Neural Network Robustness Measurement and AssessmentFoMLASJul 31 12:00
Guy Amir, Guy Katz, Michael Schapira and Tom ZelaznyVerification-Aided Deep Ensemble SelectionFoMLASAug 01 10:00
Matan Ostrovsky, Clark Barrett and Guy KatzAn Abstraction-Refinement Approach to Verifying Convolutional Neural NetworksFoMLASJul 31 09:30
Idan Refaeli and Guy KatzMinimal Multi-Layer Modifications of Deep Neural NetworksFoMLASAug 01 16:00
Matthew Daggitt, Wen Kokke, Robert Atkey, Luca Arnaboldi and Ekaterina KomendantskayaVehicle: A High-Level Language for Embedding Logical Specifications in Neural NetworksFoMLASAug 01 11:30
Omri Isac, Clark Barrett, Min Zhang and Guy KatzNeural Network Verification with Proof ProductionFoMLASAug 01 14:00
Marco Casadio, Ekaterina Komendantskaya, Verena Rieser, Matthew Daggitt, Daniel Kienitz, Luca Arnaboldi and Wen KokkeWhy Robust Natural Language Understanding is a ChallengeFoMLASJul 31 09:00
Natalia Ślusarz, Ekaterina Komendantskaya, Matthew Daggitt and Robert StewartDifferentiable Logics for Neural Network Training and VerificationFoMLASAug 01 12:00
Remi Desmartin, Grant Passmore and Ekaterina KomendantskayaNeural Networks in Imandra: Matrix Representation as a Verification ChoiceFoMLASJul 31 10:00
Klas Leino, Aymeric Fromherz, Ravi Mangal, Matt Fredrikson, Bryan Parno and Corina PasareanuSelf-Correcting Neural Networks For Safe ClassificationFoMLASAug 01 16:30
Saddek Bensalem, Chih-Hong Cheng, Xiaowei Huang, Panagiotis Katsaros, Adam Molin, Dejan Nickovic and Doron PeledFormal Specification for Learning-Enabled Autonomous SystemsFoMLASAug 01 11:00
Ichiro HasuoGoal-Aware RSS for Complex Scenarios via Program LogicFoMLASJul 31 16:30
Azza GaysinProof complexity of CSPPCJul 31 14:30
Emre Yolcu and Marijn HeuleExponential separations using guarded extension variablesPCAug 01 17:00
Hunter MonroeAverage-Case Hardness of Proving Tautologies and TheoremsPCAug 01 14:00
Dmitry Itsykson and Artur RiazanovProof complexity of natural formulas via communication argumentsPCJul 31 15:00
Nikita GaevoySimulations between proof systemsPCAug 01 14:30
Benjamin Böhm, Tomáš Peitl and Olaf BeyersdorffQCDCL with Cube Learning or Pure Literal Elimination – What is best?PCAug 01 10:00
Ilario Bonacina, Nicola Galesi and Massimo LauriaOn vanishing sums of roots of unity in polynomial calculus and sum-of-squares (an extended abstract)PCAug 01 16:00
Tomáš Peitl and Stefan SzeiderAre Hitting Formulas Hard for Resolution?PCAug 01 15:00
Anthony Widjaja LinData Path Queries over Embedded Graph DatabasesVardiFestJul 31 09:50
Shufang ZhuLTLf Synthesis as AND-OR Graph Search: Knowledge Compilation at WorkVardiFestJul 31 10:00
Mikhail SoutchanskiTowards Combination of Logic and Calculus for Near-Optimal Planning in Relational Hybrid SystemsVardiFestJul 31 10:10
Jianwen LiSAT-based Reasoning Techniques for LTL over Finite and Infinite TracesVardiFestJul 31 10:20
Aniello MuranoFormal Aspects of Strategic Reasoning in MASVardiFestJul 31 11:00
Alan Khoja, Martin Kölbl, Stefan Leue and Rüdiger WilhelmiChecking Legal Contracts - On a Not So Usual Application of Mechanized LogicVardiFestJul 31 11:10
Nir PitermanModelling with Reconfigurable Communication InterfacesVardiFestJul 31 11:20
Giuseppe PerelliOn the Extraordinary Effectiveness of Logic in Strategic ReasoningVardiFestJul 31 11:35
Munyque Mittelmann, Bastien Maubert, Aniello Murano and Laurent PerrusselAutomated Synthesis of MechanismsVardiFestJul 31 11:45
Natasha AlechinaSynthesis of plans for teams of manufacturing robotsVardiFestJul 31 11:55
Joe HalpernThat's All I know: On the Effectiveness of Logic in Game TheoryVardiFestJul 31 12:10
Thomas HenzingerBetween Determinism and NondeterminismVardiFestJul 31 12:20
Sandeep Shukla A Short Talk Proposal for the VardiFest "On the Not So Unusual Effectiveness of Logic" VardiFestJul 31 12:30
Suguman BansalAutomata-Based Quantitative ReasoningVardiFestJul 31 14:50
Antonio Di StasioLTLf Synthesis Under Environment SpecificationsVardiFestJul 31 15:00
Lucas Martinelli TabajaraBoolean Synthesis via Decision DiagramsVardiFestJul 31 15:10
Benjamin Bordais, Damien Busatto-Gaston, Shibashis Guha and Jean-Francois RaskinStrategy synthesis for Global Window PCTLVardiFestJul 31 15:20
Hector GeffnerLogic and Languages for Representation LearningVardiFestJul 31 16:00
Irun Cohen and Assaf MarronNatural AutoencodingVardiFestJul 31 16:10
Luis LambFrom Logic to Neurosymbolic AIVardiFestJul 31 16:20
Stefania Costantini, Andrea Formisano and Valentina PitoniAn Epistemic Logic for modelling Cooperative AgentsVardiFestJul 31 16:30
Martin Charles GolumbicOn the Effectiveness of Logic in Algorithmic Graph TheoryVardiFestJul 31 16:45
David HarelComputability and Complexity over Finite Unordered Structures; e.g., Graphs (1979-1982)VardiFestJul 31 16:55
Alessandro Cimatti, Luca Geatti, Nicola Gigante, Angelo Montanari and Stefano TonettaThe Safety Fragment of LTLVardiFestAug 01 09:50
Ashutosh Trivedi, Fabio Somenzi and Mateo PerezAn Automata-Theoretic Approach to Model-Free Reinforcement LearningVardiFestAug 01 10:00
Fabio MogaveroStrategy Logic: Origin, Results, and Open QuestionsVardiFestAug 01 10:10
Maurizio LenzeriniRewriting of Regular Path Queries: The first paper of the four ItaliansVardiFestAug 01 10:20
Diego CalvaneseRewriting, Answering, and Losslessness: A Clarification by the “Four Italians”VardiFestAug 01 11:00
Ichiro HasuoBisimulation Games Played in Fibered CategoriesVardiFestAug 01 11:10
Andrea FerraraCapturing abscondingsVardiFestAug 01 11:20
Samson AbramskyFrom Kochen-Specker to Feder-VardiVardiFestAug 01 11:35
Georg GottlobData Complexity and Expressive Power of Ontological Reasoning FormalismsVardiFestAug 01 11:45
Amit BhatiaLogic-driven approaches for smart, safe and energy-efficient aviationVardiFestAug 01 11:55
Yong LiDivide-and-Conquer Determinization for B\"uchi AutomataVardiFestAug 01 12:10
Ben Greenman, Sam Saarinen, Tim Nelson and Shriram KrishnamurthiLittle Tricky Logic: Misconceptions in the Understanding of LTLVardiFestAug 01 12:20
Vijay Ganesh, Dhananjay Ashok, Christopher Srinivasa and Vineel NagisettyA Solver + Gradient Descent Training Algorithm for Deep Neural NetworkVardiFest
Joel OuaknineAlgorithms, Complexity, Verification: From Cook and Karp to Vardi; or, a Brief Glimpse of the Skolem LandscapeVardiFestAug 01 14:25
Leonid LibkinApproximations of Certain Answers in First-Order LogicVardiFestAug 01 14:35
Eugenia TernovskaTowards Algebraic Techniques for Descriptive ComplexityVardiFestAug 01 14:45
Victor VianuFixpoint Logics, Relational Machines, and Computational ComplexityVardiFestAug 01 15:00
Marijn HeuleUnderstandable Proofs of UnsatisfiabilityVardiFestAug 01 16:00
Eli Singerman, Gila Kamhi, Ranan Fraer and Avner LandverMoshe Vardi and Intel Corporation: Long and Fruitful CollaborationVardiFestAug 01 15:20
Yoram MosesA Toast for Moshe at the FLoC VardiFestVardiFestAug 01 15:30
Supratik ChakrabortyTo Count or Not to Count: A Personal PerspectiveVardiFestAug 01 15:10
Mahesh ViswanathanVerifying Accuracy Claims of Differential Privacy AlgorithmsVardiFestAug 01 16:45
Sharad MalikBridging Practice and Theory in SAT: Moshe Vardi the CatalystVardiFestAug 01 16:55
Giuseppe De GiacomoLTLf? It's Easy! Precisely!VardiFest
Kuldeep S. Meel12 Years and Counting: Samples from My Undergraduate Research ProjecVardiFest
Sasha RubinTrace-view vs Strategy-view of the Environment in Reactive SynthesisVardiFest
Andrea Balogh and Barry O'SullivanSymmetry breaking and Knowledge CompilationCPAug 01 15:00
Nicolas Beldiceanu, Jovial Cheukam Ngouonou, Rémi Douence, Ramiz Gindullin and Claude-Guy QuimperExtended Abstract: Acquiring Maps of Interrelated Conjectures on Sharp BoundsCPAug 01 17:26
Auguste Burlats and Gilles PesantExploiting Model Entropy to Make Branching Decisions in Constraint ProgrammingCPAug 01 14:20
Vianney Coppé, Xavier Gillard and Pierre SchausSolving the Constrained Single-Row Facility Layout Problem with Decision Diagrams (Extended Abstract)CPAug 01 12:21
Christopher Coulombe and Claude-Guy QuimperExtended Abstract: Constraint Acquisition Based on Solution CountingCPAug 01 17:23
Marco Dalla, Andrea Visentin and Barry O'SullivanAutomated SAT Problem Feature Extraction using 1 Convolutional AutoencodersCPAug 01 11:55
Augustin Delecluse, Pierre Schaus and Pascal Van HentenryckExtended Abstract: Sequence Variables for Routing ProblemsCPAug 01 10:23
Sharmi Dev Gupta, Begum Genc and Barry O'SullivanFinding Counterfactual Explanations through Constraint RelaxationsCPAug 01 14:40
Alexander Ek, Andreas Schutt, Peter J. Stuckey and Guido TackExplaining Propagation for Gini and Spread with Variable Mean (Extended Abstract)CPAug 01 17:20
Thibault Falque, Christophe Lecoutre, Bertrand Mazure and Hugues WattezAggressive Bound Descent for Constraint OptimizationCPAug 01 14:00
Thibault Falque and Romain WallonOn PB Encodings for Constraint ProblemsCPAug 01 16:40
Ramiz Gindullin, Nicolas Beldiceanu and Jovial Cheukam NgouonouA Boolean Formula Seeker in the Context of Acquiring Maps of Interrelated Conjectures on Sharp BoundsCPAug 01 17:00
Priyanka Golia, Subhajit Roy and Kuldeep S. MeelBoolean Functional Synthesis and its ApplicationsCPAug 01 16:20
Daphné Lafleur, Sarath Chandar and Gilles PesantCombining Reinforcement Learning and Constraint Programming for Sequence-Generation Tasks with Hard Constraints - Extended AbstractCPAug 01 10:26
Jimmy H. M. Lee and Allen Z. ZhongExploiting Functional Constraints in Automatic Dominance Breaking for Constraint Optimization (Extended Abstract)CPAug 01 15:23
Jheisson López, Laura Climent and Alejandro ArbelaezLarge Neighborhood Search for Robust Solutions for Constraint Satisfaction Problems with Ordered DomainsCPAug 01 15:26
Xiao Peng, Olivier Simonin and Christine SolnonSolving the Non-Crossing MAPF for non point-sized robotsCPAug 01 10:00
Louis Popovic, Alain Côté, Mohamed Gaha, Franklin Nguewouo and Quentin CappartExtended Abstract for : Scheduling the Equipment Maintenance of an Electric Power Transmission Network using Constraint ProgrammingCPAug 01 10:20
Siddharth Prasad, Maria-Florina Balcan, Tuomas Sandholm and Ellen VitercikImproved Sample Complexity Bounds for Branch-and-CutCPAug 01 15:20
Isaac Rudich, Quentin Cappart and Louis-Martin RousseauPeel-and-Bound: Generating Stronger Relaxed Bounds with Multivalued Decision DiagramsCPAug 01 12:18
Rodothea Myrsini Tsoupidi, Roberto Castañeda Lozano, Elena Troubitsyna and Panagiotis PapadimitratosOptimized Code Generation against Power Side ChannelsCPAug 01 16:00
Felix Ulrich-Oltean, Peter Nightingale and James WalkerSelecting SAT Encodings for Pseudo-Boolean and Linear Integer ConstraintsCPAug 01 12:15
Ruiwei Wang and Roland YapCNF Encodings of Binary Constraint Trees (Extended Abstract)CPAug 01 12:24
Neha RungtaA Billion SMT Queries a DayCAV
Arie GurfinkelProgram Verification with Constrained Horn Clauses (Invited Paper)CAV
Jialu Bao, Nitesh Trivedi, Drashti Pathak, Justin Hsu and Subhajit RoyData-Driven Invariant Learning for Probabilistic ProgramsCAVAug 07 09:00
Krishnendu Chatterjee, Amir Kafshdar Goharshady, Tobias Meggendorfer and Đorđe ŽikelićSound and Complete Certificates for Quantitative Termination Analysis of Probabilistic ProgramsCAVAug 07 09:20
Mingshuai Chen, Joost-Pieter Katoen, Lutz Klinkenberg and Tobias WinklerDoes a Program Yield the Right Distribution? Verifying Probabilistic Programs via Generating FunctionsCAVAug 07 09:40
Sebastian Junges and Matthijs T. J. SpaanAbstraction-Refinement for Hierarchical Probabilistic ModelsCAVAug 07 10:00
Marc Fischer, Christian Sprecher, Dimitar I. Dimitrov, Gagandeep Singh and Martin VechevShared Certificates for Neural Network VerificationCAVAug 07 14:00
Brandon Paulsen and Chao WangExample Guided Synthesis of Linear Approximations for Neural Network VerificationCAVAug 07 14:20
Long H. Pham and Jun SunVerifying Neural Networks Against Backdoor AttacksCAVAug 07 14:40
Peng Jin, Jiaxu Tian, Dapeng Zhi, Xuejun Wen and Min ZhangTrainify: A CEGAR-Driven Training and Verification Framework for Safe Deep Reinforcement LearningCAVAug 07 15:00
Marco Casadio, Ekaterina Komendantskaya, Matthew L. Daggitt, Wen Kokke, Guy Katz, Guy Amir and Idan RefaeliNeural Network Robustness as a Verification Property: A Principled Case StudyCAVAug 07 15:20
Mayuko Kori, Natsuki Urabe, Shin-ya Katsumata, Kohei Suenaga and Ichiro HasuoThe Lattice-Theoretic Essence of Property Directed Reachability AnalysisCAVAug 07 16:00
Yucheng Ji, Hongfei Fu, Bin Fang and Haibo ChenAffine Loop Invariant Generation via Matrix AlgebraCAVAug 07 16:20
Ahmed Bouajjani, Wael-Amine Boutglay and Peter HabermehlData-driven Numerical Invariant Synthesis with Automatic Generation of AttributesCAVAug 07 16:40
Prantik Chatterjee, Jaydeepsinh Meda, Akash Lal and Subhajit RoyProof-guided Underapproximation Widening for Bounded Model CheckingCAVAug 07 17:00
Leonardo Alt, Martin Blicha, Antti Hyvärinen and Natasha SharyginaSolCMC: Solidity Compiler’s Model CheckerCAVAug 07 17:20
Raven Beutner and Bernd FinkbeinerSoftware Verification of Hyperproperties Beyond k-SafetyCAVAug 08 09:00
Priyanka Golia, Brendan Juba and Kuldeep S. MeelA Scalable Shannon Entropy EstimatorCAVAug 08 09:20
Yuxin Fan, Fu Song, Taolue Chen, Liangfeng Zhang and Wanwei LiuPoS4MPC: Automated Security Policy Synthesis for Secure Multi-Party ComputationCAVAug 08 09:40
Norine Coenen, Raimund Dachselt, Bernd Finkbeiner, Hadar Frenkel, Christopher Hahn, Tom Horak, Niklas Metzger and Julian SiberExplaining Hyperproperty ViolationsCAVAug 08 10:00
Elvira Albert, Marta Bellés-Muñoz, Miguel Isabel, Clara Rodríguez-Núñez and Albert RubioDistilling Constraints in Zero-Knowledge ProtocolsCAVAug 08 10:20
Ryotaro Banno, Kotaro Matsuoka, Naoki Matsumoto, Song Bian, Masaki Waga and Kohei SuenagaOblivious Online Monitoring for Safety LTL Specification via Fully Homomorphic EncryptionCAVAug 08 14:00
Anna Becchi and Alessandro CimattiAbstraction Modulo Stability for Reverse EngineeringCAVAug 08 14:20
Stanley Bak, Sergiy Bogomolov, Brandon Hencey, Niklas Kochdumper, Ethan Lew and Kostiantyn PotomkinReachability of Koopman Linearized Systems Using Random Fourier Feature Observables and Polynomial Zonotope RefinementCAVAug 08 14:40
Eric Goubault and Sylvie PutotRINO: Robust INner and Outer Approximated Reachability of Neural Networks Controlled SystemsCAVAug 08 15:00
Geunyeol Yu, Jia Lee and Kyungmin BaeSTLmc: Robust STL Model Checking of Hybrid Systems using SMTCAVAug 08 15:10
Elizabeth Polgreen, Kevin Cheang, Pranav Gaddamadugu, Adwait Godbole, Kevin Laeufer, Shaokai Lin, Yatin A. Manerkar, Federico Mora and Sanjit A. SeshiaUCLID5: Multi-Modal Formal Modeling, Verification, and SynthesisCAVAug 08 15:20
Chaitanya Agarwal, Shibashis Guha, Jan Křetínský and Pazhamalai MuruganandhamPAC Statistical Model Checking of Mean Payoff in Discrete- and Continuous-Time MDPCAVAug 08 16:00
Thom Badings, Nils Jansen, Sebastian Junges, Marielle Stoelinga and Matthias VolkSampling-Based Verification of CTMCs with Uncertain RatesCAVAug 08 16:20
Pablo Castro, Pedro R. D'Argenio, Luciano Putruele and Ramiro DemasiPlaying Against Fair Adversaries in Stochastic Games with Total RewardsCAVAug 08 16:40
Lorenz Leutgeb, Georg Moser and Florian ZulegerAutomated Expected Amortised Cost Analysis of Probabilistic Data StructuresCAVAug 08 17:00
Aina Niemetz, Mathias Preiner and Clark BarrettMurxla: A Modular and Highly Extensible API Fuzzer for SMT SolversCAVAug 08 17:20
Kyveli Doveri, Pierre Ganty and Nicolas MazzocchiFORQ-based Language Inclusion Formal TestingCAVAug 09 11:00
Thibault Dardinier, Gaurav Parthasarathy, Noé Weeks, Peter Müller and Alexander J. SummersSound Automation of Magic WandsCAVAug 09 11:20
Yong Li, Andrea Turrini, Weizhi Feng, Moshe Vardi and Lijun ZhangDivide-and-Conquer Determinization of Büchi Automata based on SCC DecompositionCAVAug 09 11:40
Alexandre Duret-Lutz, Etienne Renault, Maximilien Colange, Florian Renkin, Alexandre Gbaguidi Aisse, Philipp Schlehuber-Caissier, Thomas Medioni, Antoine Martin, Jérôme Dubois, Clément Gillard and Henrich LaukoFrom Spot 2.0 to Spot 2.10: What's New?CAVAug 09 12:00
Vojtěch Havlena, Ondrej Lengal and Barbora ŠmahlíkováComplementing Büchi Automata with RankerCAVAug 09 12:10
Andres Noetzli, Andrew Reynolds, Haniel Barbosa, Clark Barrett and Cesare TinelliEven Faster Conflicts and Lazier Reductions for String SolversCAVAug 09 14:00
Shaowei Cai, Bohan Li and Xindi ZhangLocal Search For SMT on Linear Integer ArithmeticCAVAug 09 14:20
Marco Faella and Gennaro ParlatoReasoning about Data Trees using CHCsCAVAug 09 14:40
Joshua M. Cohen, Qinshi Wang and Andrew W. AppelVerified Erasure Correction in Coq with MathComp and VSTCAVAug 09 15:00
Shenghao Yuan, Frédéric Besson, Jean-Pierre Talpin, Samuel Hym, Koen Zandberg and Emmanuel BaccelliEnd-to-end Mechanised Proof of an eBPF Virtual Machine for MicrocontrollersCAVAug 09 15:20
Joonwon Choi, Adam Chlipala and ArvindHemiola: A DSL and Verification Tools to Guide Design and Proof of Hierarchical Cache-Coherence ProtocolsCAVAug 09 15:40
Kishor Jothimurugan, Suguman Bansal, Osbert Bastani and Rajeev AlurSpecification-Guided Learning of Nash Equilibria with High Social WelfareCAVAug 10 14:00
Jingbo Wang, Yannan Li and Chao WangSynthesizing Fair Decision Trees via Iterative Constraint SolvingCAVAug 10 14:20
Seongwon Bang, Seunghyeon Nam, Inwhan Chun, Ho Young Jhoo and Juneyoung LeeSMT-based Translation Validation for Machine Learning CompilerCAVAug 10 14:40
Ji Guan, Wang Fang and Mingsheng YingVerifying Fairness in Quantum Machine LearningCAVAug 10 15:00
Timo P. Gros, Holger Hermanns, Joerg Hoffmann, Michaela Klauck, Maximilian Alexander Köhl and Verena WolfMoGym: Using Formal Models for Training and Verifying Decision-making AgentsCAVAug 10 15:20
Mateus De Oliveira OliveiraSynthesis and Analysis of Petri Nets from Causal SpecificationsCAVAug 10 16:00
Michael Blondin, Filip Mazowiecki and Philip OfftermattVerifying generalised and structural soundness of workflow nets via relaxationsCAVAug 10 16:20
Andreas Katis, Anastasia Mavridou, Dimitra Giannakopoulou, Thomas Pressburger and Johann SchumannCapture, Analyze, Diagnose: Realizability Checking of Requirements in FRETCAVAug 10 16:40
Bernd Finkbeiner, Niklas Metzger and Yoram MosesInformation Flow Guided SynthesisCAVAug 10 16:50
Andreas Gittis, Eric Vin and Daniel FremontRandomized Synthesis for Diversity and Cost Constraints with Control ImprovisationCAVAug 10 17:10
Daniel Waszkiewicz and Konstanty Junosza-SzaniawskiTowards an Efficient CNF Encoding of Block CiphersPOSAug 01 09:00
Thomas Bartel, Tomas Balyo and Markus IserDinosat: A SAT Solver with Native DNF SupportPOSAug 01 11:00
Hidetomo Nabeshima, Tsubasa Fukiage, Yuto Obitsu, Xiao-Nan Lu and Katsumi InoueDPS: A Framework for Deterministic Parallel SAT SolversPOSAug 01 11:30
Mathias Fleury and Armin BiereScalable Proof Producing Multi-Threaded SAT Solving with Gimsatul through Sharing instead of Copying ClausesPOSAug 01 12:00
Randal Bryant and Mate SoosCombining CDCL, Gauss-Jordan Elimination, and Proof GenerationPOSAug 01 14:30
Isaac Grosof, Naifeng Zhang and Marijn HeuleTowards the shortest DRAT proof of the Pigeonhole PrinciplePOSAug 01 15:00
Tim Holzenkamp, Kevin Kuryshev, Thomas Oltmann, Lucas Wäldele, Johann Zuber, Tobias Heuer and Markus IserSATViz: Real-Time Visualization of Clausal ProofsPOSAug 01 16:00
Faiq Miftakhul Falakh and Sebastian RudolphAGM Revision in Description Logics Under Fixed-Domain SemanticsDLAug 08 11:00
Tim Lyon and Jonas KargeUniform and Modular Sequent Systems for Description LogicsDLAug 09 10:15
Philippe Balbiani, Cigdem Gencer and Martin DiéguezAdvanced languages of terms for ontologiesDLAug 08 15:05
Ludovic Brieulle, Chan Le Duc and Pascal VaillantCategory-based Semantics for the Description Logic ALC and ReasoningDLAug 10 12:15
Birte Glimm, Yevgeny Kazakov and Michael WeltConcept Abduction for Description LogicsDLAug 09 14:00
Jing Xiong, Guohui Xiao, Tahir Emre Kalayci, Marco Montali, Zhenzhen Gu and Diego CalvaneseExtraction of Object-Centric Event Logs through Virtual Knowledge GraphsDLAug 10 11:50
Zuzana Hlávková, Martin Homola, Patrick Koopmann and Júlia PukancováAn API for DL Abduction SolversDLAug 09 15:15
Martin Homola, Júlia Pukancová, Iveta Balintová and Janka BoborováHybrid MHS-MXP ABox Abduction Solver: First Emprical ResultsDLAug 08 12:15
Jean Christoph Jung, Andrea Mazzullo and Frank WolterMore on Interpolants and Explicit Definitions for Description Logics with Nominals and/or Role InclusionsDLAug 09 09:00
Satyadharma Tirtarasa and Anni-Yasmin TurhanA new dimension to generalization: computing temporal EL concepts from positive examples (Extended Abstract)DLAug 08 16:50
Guendalina Righetti, Daniele Porello and Roberto ConfalonieriEvaluating the Interpretability of Threshold OperatorsDLAug 09 15:30
Marie Fortin, Boris Konev, Vladislav Ryzhikov, Yury Savateev, Frank Wolter and Michael ZakharyaschevReverse Engineering of Temporal Queries with and without LTL Ontologies: First StepsDLAug 07 10:05
Maurice Funk, Jean Christoph Jung and Carsten LutzActively Learning ELIQs in the Presence of DL-Lite-Horn OntologiesDLAug 08 16:25
Lucía Gómez Álvarez, Sebastian Rudolph and Hannes StrassModelling Multiple Perspectives by Standpoint-Enhanced DLsDLAug 07 16:50
Bartosz Bednarczyk and Mateusz UrbańczykComonadic Semantics for Description Logics GamesDLAug 08 14:50
Christian Alrabbaa, Stefan Borgwardt, Tom Friese, Patrick Koopmann, Julián Méndez and Alexej PopovičOn the Eve of True Explainability for OWL Ontologies: Description Logic Proofs with Evee and EvonneDLAug 09 14:25
Bernardo Alkmim, Edward Haeusler and Cláudia NalonA Labelled Natural Deduction System for an Intuitionistic Description Logic with NominalsDLAug 09 15:45
Christian Alrabbaa, Stefan Borgwardt, Patrick Koopmann and Alisa KovtunovaFinding Good Proofs for Answers to Conjunctive Queries Mediated by Lightweight OntologiesDLAug 07 09:40
Stefan Borgwardt, Jörg Hoffmann, Alisa Kovtunova, Markus Krötzsch, Bernhard Nebel and Marcel SteinmetzExpressivity of Planning with Horn Description Logic Ontologies (Extended Abstract)DLAug 09 12:00
Federica Di Stefano, Magdalena Ortiz and Mantas SimkusPointwise Circumscription in Description LogicsDLAug 08 11:50
Alex Borgida, Enrico Franconi, David Toman and Grant WeddellAccessing Document Data Sources using Referring Expression TypesDLAug 10 11:25
Loris Bozzato, Thomas Eiter and Rafael KieselReasoning on Multi-Relational Contextual Hierarchies via Answer Set Programming with Algebraic MeasuresDLAug 07 15:00
Moritz Illich and Birte GlimmComputing Concept Referring Expressions with Standard OWL ReasonersDLAug 10 11:00
Birte Glimm and Yevgeny KazakovSAT-Based Axiom Pinpointing RevisitedDLAug 09 14:50
Mostafa Sakr and Renate A. SchmidtFine-Grained Forgetting for the Description Logic ALCDLAug 09 09:50
Zhenzhen Gu, Davide Lanti, Alessandro Mosca, Guohui Xiao, Jing Xiong and Diego CalvaneseOntology-based Data Federation (Extended Abstract)DLAug 08 14:25
Meghyn Bienvenu, Quentin Manière and Michaël ThomazoComplexity Landscape for Counting Queries (Extended abstract)DLAug 07 09:15
Franz Baader, Patrick Koopmann, Friedrich Michel, Anni-Yasmin Turhan and Benjamin ZarriessEfficient TBox Reasoning with Value Restrictions using the FL0wer Reasoner (Extended Abstract)DLAug 08 16:00
Meghyn Bienvenu and Camille BourgauxQuerying Inconsistent Prioritized Data with ORBITS: Algorithms, Implementation, and Experiments (Extended Abstract)DLAug 08 14:00
Haoruo Zhao, Bijan Parsia and Uli SattlerNext Steps for ReAD: Modules for Classification OptimisationDLAug 10 10:00
Fajar Haifani, Patrick Koopmann, Sophie Tourret and Christoph WeidenbachConnection-minimal Abduction in EL via translation to FOL (Extended Abstract)DLAug 08 10:00
Laura Giordano, Alberto Martelli and Daniele Theseider DupreReasoning about actions with EL ontologies in a temporal action theory (Extended Abstract)DLAug 08 17:15
Franz Baader, Patrick Koopmann, Francesco Kriegel and Adrian NuradiansyahOptimal ABox Repair w.r.t. Static EL TBoxes: from Quantified ABoxes back to ABoxes (Extended Abstract)DLAug 09 09:25
Mikkel Milo, Eske Hoy Nielsen, Danil Annenkov and Bas SpittersFinding smart contract vulnerabilities with ConCert's property-based testing frameworkFMBCAug 11 11:00
Martin Ceresa and Cesar SanchezMulti: a Formal Playground for Smart Multi-contract interactionFMBCAug 11 16:00
Andre Knispel, James Chapman, Orestis Melkonian and Polina VinogradovaHuman and machine-readable models of state machines for the Cardano ledgerFMBCAug 11 15:00
Polina Vinogradova, Manuel Chakravarty, Orestis Melkonian, Michael Peyton Jones, James Chapman, Tudor Ferariu and Jacco KrijnenDesigning EUTxO smart contracts as communicating state machines: the case of simulating accountsFMBCAug 11 12:00
Polina Vinogradova, Orestis Melkonian, Andre Knispel and James ChapmanDeterminism of ledger updatesFMBCAug 11 14:45
Ignacio Ballesteros, Clara Benac, Luis Eduardo Bueso, Lars-Åke Fredlund, Ángel Herranz and Julio MariñoAutomatic generation of attacker contracts in SolidityFMBCAug 11 11:30
Chad Brown, Cezary Kaliszyk, Josef Urban and Thibault GauthierProofgold: Blockchain for Formal MethodsFMBCAug 11 14:00
Aurélien Saue, Arvid Jakobsson and Kristina SojakovaFAT CAT: Formal Acceptance Testing of Contracts for Administering TokensFMBCAug 11 12:15
Cezara Dragoi, Constantin Enea, Srinidhi Nagendra and Mandayam SrivasA Domain Specific Language for Testing Consensus ImplementationsFMBCAug 11 14:30
Lea Salome Brugger, Laura Kovács, Anja Petković Komel, Sophie Rain and Michael RawsonAutomating Security Analysis of Off-Chain ProtocolsFMBCAug 11 16:30