AProVE
From MaRDI portal
Software:19847
No author found.
Related Items (only showing first 100 items - show all)
\textsc{ComplexityParser}: an automatic tool for certifying poly-time complexity of Java programs ⋮ Relative termination via dependency pairs ⋮ Automatically proving termination and memory safety for programs with pointer arithmetic ⋮ A Tool Proving Well-Definedness of Streams Using Termination Tools ⋮ On the Termination of Integer Loops ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Harnessing First Order Termination Provers Using Higher Order Dependency Pairs ⋮ Generalized and Formalized Uncurrying ⋮ SMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT Solving ⋮ Combining Model Checking and Data-Flow Analysis ⋮ Knuth-Bendix completion of theories of commuting group endomorphisms ⋮ KBO orientability ⋮ Automatic discovery of fair paths in infinite-state transition systems ⋮ Termination of string rewriting proved automatically ⋮ Certification of Termination Proofs Using CeTA ⋮ Mechanically proving termination using polynomial interpretations ⋮ Termination and complexity analysis for programs with bitvector arithmetic by symbolic execution ⋮ Automating regression verification of pointer programs by predicate abstraction ⋮ Proving termination of context-sensitive rewriting by transformation ⋮ Proving Termination of Programs Automatically with AProVE ⋮ Proving Termination and Memory Safety for Programs with Pointer Arithmetic ⋮ SAT solving for termination proofs with recursive path orders and dependency pairs ⋮ Dependency pairs for proving termination properties of conditional term rewriting systems ⋮ Multi-completion with termination tools ⋮ Lower bounds for runtime complexity of term rewriting ⋮ Termination of Cycle Rewriting by Transformation and Matrix Interpretation ⋮ Certifying confluence of quasi-decreasing strongly deterministic conditional term rewrite systems ⋮ Certifying safety and termination proofs for integer transition systems ⋮ Tyrolean termination tool: techniques and features ⋮ On tree automata that certify termination of left-linear term rewriting systems ⋮ Elimination transformations for associative-commutative rewriting systems ⋮ Mechanizing and improving dependency pairs ⋮ Parametrized verification diagrams: temporal verification of symmetric parametrized concurrent systems ⋮ Deaccumulation techniques for improving provability ⋮ Transforming derivational complexity of term rewriting to runtime complexity ⋮ Modular strategic SMT solving with \textbf{SMT-RAT} ⋮ Twenty years of rewriting logic ⋮ Complexity analysis for term rewriting by integer transition systems ⋮ Sufficient completeness verification for conditional and constrained TRS ⋮ Solving Nonlinear Integer Arithmetic with MCSAT ⋮ Formalizing Soundness and Completeness of Unravelings ⋮ Conflict-driven conditional termination ⋮ Fairness modulo theory: a new approach to LTL software model checking ⋮ Relational program reasoning using compiler IR ⋮ Proving termination by dependency pairs and inductive theorem proving ⋮ SAT modulo linear arithmetic for solving polynomial constraints ⋮ Dependency Pairs for Rewriting with Built-In Numbers and Semantic Data Structures ⋮ Fast offline partial evaluation of logic programs ⋮ Termination of Innermost Context-Sensitive Rewriting Using Dependency Pairs ⋮ On Equality Predicates in Algebraic Specification Languages ⋮ Checking Conservativity of Overloaded Definitions in Higher-Order Logic ⋮ Slothrop: Knuth-Bendix Completion with a Modern Termination Checker ⋮ Automated Termination Analysis for Haskell: From Term Rewriting to Programming Languages ⋮ Unnamed Item ⋮ Time-bounded termination analysis for probabilistic programs with delays ⋮ Type-based termination of generic programs ⋮ Termination of just/fair computations in term rewriting ⋮ Maintaining a library of formal mathematics ⋮ Proving termination of nonlinear command sequences ⋮ Matrix interpretations for proving termination of term rewriting ⋮ Certifying a Termination Criterion Based on Graphs, without Graphs ⋮ The 2D dependency pair framework for conditional rewrite systems. II: Advanced processors and implementation techniques ⋮ Enhancing dependency pair method using strong computability in simply-typed term rewriting ⋮ Loop detection in term rewriting using the eliminating unfoldings ⋮ Adding constants to string rewriting ⋮ A Perron-Frobenius theorem for deciding matrix growth ⋮ Rewrite rules for \(\mathrm{CTL}^\ast\) ⋮ Termination of narrowing via termination of rewriting ⋮ Lazy productivity via termination ⋮ Characterizing and proving operational termination of deterministic conditional term rewriting systems ⋮ Proving operational termination of membership equational programs ⋮ Unnamed Item ⋮ On the relative power of polynomials with real, rational, and integer coefficients in proofs of termination of rewriting ⋮ Context-sensitive dependency pairs ⋮ Termination Graphs for Java Bytecode ⋮ From LCF to Isabelle/HOL ⋮ Proving Termination Properties with mu-term ⋮ Constant runtime complexity of term rewriting is semi-decidable ⋮ Explaining safety failures in NetKAT ⋮ Inferring expected runtimes of probabilistic integer programs using expected sizes ⋮ Methods for Proving Termination of Rewriting-based Programming Languages by Transformation ⋮ Using well-founded relations for proving operational termination ⋮ Non-termination analysis of logic programs with integer arithmetics ⋮ Termination of Isabelle Functions via Termination of Rewriting ⋮ Temporal prophecy for proving temporal properties of infinite-state systems ⋮ Derivational complexity and context-sensitive Rewriting ⋮ Conditions for confluence of innermost terminating term rewriting systems ⋮ Match-bounds revisited ⋮ Increasing interpretations ⋮ On-demand strategy annotations revisited: an improved on-demand evaluation strategy ⋮ The size-change principle and dependency pairs for termination of term rewriting ⋮ Modular and incremental automated termination proofs ⋮ Tuple interpretations for termination of term rewriting ⋮ Term orderings for non-reachability of (conditional) rewriting ⋮ \textsc{LTL} falsification in infinite-state systems ⋮ Improving the Context-sensitive Dependency Graph ⋮ Proving Termination of Context-Sensitive Rewriting with MU-TERM ⋮ Termination of Lazy Rewriting Revisited ⋮ Pattern eliminating transformations
This page was built for software: AProVE
