AProVE

swMATH7831MaRDI QIDQ19847FDOQ19847

Author name not available (Why is that?)

Described by source

• Analyzing program termination and complexity automatically with \textsf{AProVE}

Cited In (only showing first 100 items - show all)

• Termination of Narrowing in Left-Linear Constructor Systems
• Title not available (Why is that?)
• Tuple interpretations for termination of term rewriting
• \textsc{LTL} falsification in infinite-state systems
• Time-bounded termination analysis for probabilistic programs with delays
• Combining Model Checking and Data-Flow Analysis
• Automatic discovery of fair paths in infinite-state transition systems
• Resource Analysis driven by (Conditional) Termination Proofs
• Inferring Lower Bounds for Runtime Complexity
• Term orderings for non-reachability of (conditional) rewriting
• Pattern eliminating transformations
• Using well-founded relations for proving operational termination
• Complexity analysis for term rewriting by integer transition systems
• Goal-directed and relative dependency pairs for proving the termination of narrowing
• On the relative power of polynomials with real, rational, and integer coefficients in proofs of termination of rewriting
• Fairness modulo theory: a new approach to LTL software model checking
• On-demand strategy annotations revisited: an improved on-demand evaluation strategy
• Towards Generic Programming with Sized Types
• Title not available (Why is that?)
• Relative termination via dependency pairs
• Termination graphs for Java bytecode
• On the termination of integer loops
• Modular termination proofs of recursive Java bytecode programs by term rewriting
• Termination and complexity analysis for programs with bitvector arithmetic by symbolic execution
• SAT solving for termination proofs with recursive path orders and dependency pairs
• Automating regression verification of pointer programs by predicate abstraction
• Detecting Non-termination of Term Rewriting Systems Using an Unfolding Operator
• Max/Plus tree automata for termination of term rewriting
• Transforming derivational complexity of term rewriting to runtime complexity
• Checking Conservativity of Overloaded Definitions in Higher-Order Logic
• Automatic Termination Verification for Higher-Order Functional Programs
• The 2D dependency pair framework for conditional rewrite systems. II: Advanced processors and implementation techniques
• Proving Termination and Memory Safety for Programs with Pointer Arithmetic
• Automatically proving termination and memory safety for programs with pointer arithmetic
• Constant runtime complexity of term rewriting is semi-decidable
• Temporal prophecy for proving temporal properties of infinite-state systems
• From LCF to Isabelle/HOL
• Proving Termination of Integer Term Rewriting
• Increasing interpretations
• Synthesizing shortest linear straight-line programs over \(\mathrm{GF}(2)\) using SAT
• Type-based termination of generic programs
• Certifying confluence of quasi-decreasing strongly deterministic conditional term rewrite systems
• Certifying safety and termination proofs for integer transition systems
• Concurrent Programming Languages and Methods for Semantic Analyses (Extended Abstract of Invited Talk)
• Proving Termination of Programs Automatically with AProVE
• Termination of Innermost Context-Sensitive Rewriting Using Dependency Pairs
• Lower bounds for runtime complexity of term rewriting
• Termination of Context-Sensitive Rewriting with Built-In Numbers and Collection Data Structures
• Relational program reasoning using compiler IR
• Derivational complexity and context-sensitive Rewriting
• Title not available (Why is that?)
• Modular strategic SMT solving with \textbf{SMT-RAT}
• \textsc{ComplexityParser}: an automatic tool for certifying poly-time complexity of Java programs
• Loop detection in term rewriting using the eliminating unfoldings
• Adding constants to string rewriting
• A Term Rewriting Approach to the Automated Termination Analysis of Imperative Programs
• Left-linear bounded TRSs are inverse recognizability preserving
• Twenty years of rewriting logic
• Match-bounds revisited
• Explaining safety failures in NetKAT
• Inferring expected runtimes of probabilistic integer programs using expected sizes
• Deaccumulation techniques for improving provability
• Maintaining a library of formal mathematics
• Title not available (Why is that?)
• A Transformational Approach to Prove Outermost Termination Automatically
• Proving operational termination of membership equational programs
• Proving termination of context-sensitive rewriting with MU-TERM
• Term Rewriting and Applications
• Proving Termination of Rewrite Systems Using Bounds
• Enhancing dependency pair method using strong computability in simply-typed term rewriting
• Lazy productivity via termination
• Certification of Termination Proofs Using CeTA
• Termination of narrowing via termination of rewriting
• Term Rewriting and Applications
• Beyond Dependency Graphs
• Solving Non-linear Polynomial Arithmetic via SAT Modulo Linear Arithmetic
• Termination Analysis by Dependency Pairs and Inductive Theorem Proving
• Frontiers of Combining Systems
• SMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT Solving
• Logic for Programming, Artificial Intelligence, and Reasoning
• Polynomials over the reals in proofs of termination : from theory to practice
• Slothrop: Knuth-Bendix Completion with a Modern Termination Checker
• Conditions for confluence of innermost terminating term rewriting systems
• Proving termination by dependency pairs and inductive theorem proving
• SAT modulo linear arithmetic for solving polynomial constraints
• Proving termination of context-sensitive rewriting by transformation
• Termination Analysis with Calling Context Graphs
• Term Rewriting and Applications
• Derivational Complexity of Knuth-Bendix Orders Revisited
• Term Rewriting and Applications
• Dependency Pairs for Rewriting with Built-In Numbers and Semantic Data Structures
• Conflict-driven conditional termination
• KBO orientability
• Mechanically proving termination using polynomial interpretations
• Termination of Narrowing Using Dependency Pairs
• Elimination transformations for associative-commutative rewriting systems
• Automated Deduction – CADE-20
• Justification logic and history based computation
• Proving termination in the context-sensitive dependency pair framework
• Automated Reasoning

This page was built for software: AProVE