Automated Deduction - CADE 29 29th International Conference on Automated Deduction, Rome, Italy, July 1-4, 2023, Proceedings /

Table of Contents: “…Certified Core-Guided MaxSAT Solving -- Superposition with Delayed Unification -- On Incremental Pre-processing for SMT -- Verified Given Clause Procedures -- QSMA: A New Algorithm for Quantified Satisfiability Modulo Theory and Assignment -- Uniform Substitution for Dynamic Logic with Communicating Hybrid Programs -- An Isabelle/HOL Formalization of the SCL(FOL) Calculus -- SCL(FOL) Can Simulate Non-Redundant Superposition Clause Learning -- Formal Reasoning about Influence in Natural Sciences Experiments -- A Theory of Cartesian Arrays (with Applications in Quantum Circuit Verification) -- SAT-Based Subsumption Resolution -- A more Pragmatic CDCL for IsaSAT and targetting LLVM (Short Paper) -- Proving Non-Termination by Acceleration Driven Clause Learning (Short Paper) -- COOL 2 - A Generic Reasoner for Modal Fixpoint Logics (System Description) -- Choose your Colour: Tree Interpolation for Quantified Formulas in SMT -- Proving Termination of C Programs with Lists -- Reasoning about Regular Properties: A Comparative Study -- Program Synthesis in Saturation -- A Uniform Formalisation of Three-Valued Logics in Bisequent Calculus -- Proving Almost-Sure Innermost Termination of Probabilistic Term Rewriting Using Dependency Pairs -- Verification of NP-hardness Reduction Functions for Exact Lattice Problems -- Buy One Get 14 Free: Evaluating Local Reductions for Modal Logic -- Left-Linear Completion with AC Axioms -- On P -interpolation in local theory extensions and applications to the study of interpolation in the description logics EL, EL+ -- Theorem Proving in Dependently-Typed Higher-Order Logic -- Towards Fast Nominal Anti-Unification of Letrec-Expressions -- Confluence Criteria for Logically Constrained Rewrite Systems -- Towards a Verified Tableau Prover for a Quantifier-Free Fragment of Set Theory -- An Experimental Pipeline for Automated Reasoning in Natural Language (Short paper) -- Combining Combination Properties: An Analysis of Stable-infiniteness, Convexity, and Politeness -- Decidability of difference logic over the reals with uninterpreted unary predicates -- Incremental Rewriting Modulo SMT -- Iscalc: an Interactive Symbolic Computation Framework (System Description).…”
Link to Metadata

Automated Reasoning with Analytic Tableaux and Related Methods 32nd International Conference, TABLEAUX 2023, Prague, Czech Republic, September 18-21, 2023, Proceedings /

Table of Contents: “…Range-Restricted and Horn Interpolation through Clausal Tableaux -- Non-Classical Logics in Satisfiability Modulo Theories -- DefTab: A Tableaux System for Sceptical Consequence in Default Modal Logics -- Non-distributive description logic -- A new calculus for intuitionistic Strong L\"ob logic: strong termination and cut-elimination, formalized -- Some Analytic Systems of Rules -- A cut-free, sound and complete Russellian theory of definite descriptions -- Towards Proof-Theoretic Formulation of the General Theory of Term-Forming Operators -- Lemmas: Generation, Selection, Application -- Machine-Learned Premise Selection for Lean -- gym-saturation: Gymnasium environments for saturation provers (System description) -- A linear perspective on cut-elimination for non-wellfounded sequent calculi with least and greatest fixed points -- Ill-founded Proof Systems For Intuitionistic Linear-time Temporal Logic -- Proof Systems for the Modal $\mu$-Calculus Obtained by Determinizing Automata -- Extensions of K5: Proof Theory and Uniform Lyndon Interpolation -- On intuitionistic diamonds (and lack thereof) -- NP Complexity for Combinations of Non-Normal Modal Logics -- Resolution-based Calculi for Non-Normal Modal Logics -- Canonicity of Proofs in Constructive Modal Logic -- Proof-theoretic Semantics for Intuitionistic Multiplicative Linear Logic -- The MaxSAT problem in the real-valued MV-algebra -- The Logic of Separation Logic: Models and Proofs -- Testing the Satisfiability of Formulas in Separation Logic with Permissions -- Nested Sequents for Quantified Modal Logics -- A Naive Prover for First-Order Logic: A Minimal Example of Analytic Completeness.…”
Link to Metadata

Foundations of Software Science and Computation Structures 24th International Conference, FOSSACS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Sof...

Table of Contents: “…Constructing a universe for the setoid model -- Nominal Equational Problems -- Finding Cut-Offs in Leaderless Rendez-Vous Protocols is Easy -- Fixpoint Theory - Upside Down -- "Most of"' leads to undecidability: Failure of adding frequencies to LTL -- Combining Semilattices and Semimodules -- One-way Resynchronizability of Word Transducers -- Fair Refinement for Asynchronous Session Types -- Running Time Analysis of Broadcast Consensus Protocols -- Leafy automata for higher-order concurrency -- Factorization in Call-by-Name and Call-by-Value Calculi via Linear Logic -- Generalized Bounded Linear Logic and its Categorical Semantics -- Focused Proof-search in the Logic of Bunched Implications -- Interpolation and Amalgamation for Arrays with MaxDi -- Adjoint Reactive GUI Programming -- On the Expressiveness of Büchi Arithmetic -- Parametricity for Primitive Nested Types -- The Spirit of Node Replication -- Nondeterministic and co-Nondeterministic Implies Deterministic, for Data Languages -- CertifyingInexpressibility -- A General Semantic Construction of Dependent Re nement Type Systems, Categorically -- Simple Stochastic Games with Almost-Sure Energy-Parity Objectives are in NP and coNP -- Nondeterministic Syntactic Complexity -- A String Diagrammatic Axiomatisation of Finite-State Automata -- Work-sensitive Dynamic Complexity of Formal Languages -- Learning Pomset Automata -- The Structure of Sum-Over-Paths, its Consequences, and Completeness for Clifford -- A Quantified Coalgebraic van Benthem Theorem.…”
Link to Metadata

Tools and Algorithms for the Construction and Analysis of Systems 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice o...

Table of Contents: “…SAT and SMT -- Decomposing Farkas Interpolants -- Parallel SAT Simplification on GPU Architectures -- Encoding Redundancy for Satisfaction-Driven Clause Learning -- WAPS: Weighted and Projected Sampling -- Building Better Bit-Blasting for Floating-Point Problems -- The Axiom Profiler: Understanding and Debugging SMT Quantifier Instantiations -- On the Empirical Time Complexity of Scale-Free 3-SAT at the Phase Transition -- Modular and Efficient Divide-and-Conquer SAT Solver on Top of the Painless Framework -- SAT Solving and Theorem Proving -- Quantitative Verification of Masked Arithmetic Programs against Side-Channel Attacks -- Incremental Analysis of Evolving Alloy Models -- Extending a Brainiac Prover to Lambda-Free Higher-Order Logic -- Verification and Analysis LCV: A Verification Tool for Linear Controller Software -- Semantic Fault Localization and Suspiciousness Ranking -- Computing Coupled Similarity -- Reachability Analysis for Termination and Confluence of Rewriting -- Model Checking -- VoxLogicA: a Spatial Model Checker for Declarative Image Analysis -- On Reachability in Parameterized Phaser Programs -- Abstract Dependency Graphs and Their Application to Model Checking -- Tool Demo -- nonreach - A Tool for Nonreachability Analysis -- The Quantitative Verification Benchmark Set -- ILAng: A Modeling Platform for SoC Verification using Instruction-Level Abstractions -- MetAcsl: Specification and Verification of High-Level Properties -- ROLL 1.0: !…”
Link to Metadata

Computer Aided Verification 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part II /

Table of Contents: “…Logics, Decision Procedures, and Solvers -- Satisfiability Checking for Mission-Time LTL -- High-Level Abstractions for Simplifying Extended String Constraints in SMT -- Alternating Automata Modulo First Order Theories -- Q3B: An Efficient BDD-based SMT Solver for Quantified Bit-Vectors -- CVC4SY: Smart and Fast Term Enumeration for Syntax-Guided Synthesis -- Incremental Determinization for Quantifier Elimination and Functional Synthesis -- Numerical Programs -- Loop Summarization with Rational Vector Addition Systems -- Invertibility Conditions for Floating-Point Formulas -- Numerically-Robust Inductive Proof Rules for Continuous Dynamical Systems -- Icing: Supporting Fast-math Style Optimizations in a Verified Compiler -- Sound Approximation of Programs with Elementary Functions -- Verification -- Formal verification of quantum algorithms using quantum Hoare logic -- SecCSL: Security Concurrent Separation Logic -- Reachability Analysis for AWS-based Networks -- Distributed Systems and Networks -- Verification of Threshold-Based Distributed Algorithms by Decomposition to Decidable Logics -- Gradual Consistency Checking -- Checking Robustness Against Snapshot Isolation -- Efficient verification of network fault tolerance via counterexampleguided refinement -- On the Complexity of Checking Consistency for Replicated Data Types -- Communication-closed asynchronous protocols -- Verification and Invariants -- Interpolating Strong Induction -- Verifying Asynchronous Event-Driven Programs Using Partial Abstract Transformers -- Inferring Inductive Invariants from Phase Structures -- Termination of Triangular Integer Loops is Decidable -- AliveInLean: A Verified LLVM Peephole Optimization Verifier -- Concurrency -- Automated Parameterized Verification of CRDTs -- What's wrong with on-the-y partial order reduction -- Integrating Formal Schedulability Analysis into a Verifed OS Kernel -- Rely-guarantee Reasoning about Concurrent Memory Management in Zephyr RTOS -- Violat: Generating Tests of Observational Refinement for Concurrent Objects. .…”
Link to Metadata

Computer Aided Verification 33rd International Conference, CAV 2021, Virtual Event, July 20-23, 2021, Proceedings, Part II /

Table of Contents: “…Complexity and Termination -- Learning Probabilistic Termination Proofs -- Ghost Signals: Verifying Termination of Busy Waiting -- Reflections on Termination of Linear Loops -- Decision Tree Learning in CEGIS-Based Termination Analysis -- ATLAS: Automated Amortised Complexity Analysis of Self-Adjusting Data Structures -- Decision Procedures and Solvers -- Theory Exploration Powered by Deductive Synthesis -- CoqQFBV: A Scalable Certified SMT Quantifier-Free Bit-Vector Solver -- Porous Invariants -- JavaSMT 3: Interacting with SMT Solvers in Java -- Efficient SMT-based Analysis of Failure Propagation -- ToolX : Better Delta Debugging for the SMT-LIBv2 Language and Friends -- Learning Union of Integer Hypercubes with Queries (with applications to monadic decomposition) -- Interpolation and Model Checking for Nonlinear Arithmetic -- An SMT Solver for Regular Expressions and Linear Arithmetic over String Length -- Counting Minimal Unsatisfiable Subsets -- Sound Verification Procedures for Temporal Properties of Infinite-State Systems -- Hardware and Model Checking -- Progress in Certifying Hardware Model Checking Results -- Model-Checking Structured Context-Free Languages -- Model Checking ! …”
Link to Metadata