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
• Modular Termination Proofs of Recursive Java Bytecode Programs by Term Rewriting
• Term orderings for non-reachability of (conditional) rewriting
• Pattern eliminating transformations
• Title not available (Why is that?)
• Using well-founded relations for proving operational termination
• Complexity analysis for term rewriting by integer transition systems
• 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
• Synthesizing Shortest Linear Straight-Line Programs over GF(2) Using SAT
• Title not available (Why is that?)
• Relative termination via dependency pairs
• 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
• 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
• Goal-Directed and Relative Dependency Pairs for Proving the Termination of Narrowing
• Constant runtime complexity of term rewriting is semi-decidable
• Temporal prophecy for proving temporal properties of infinite-state systems
• From LCF to Isabelle/HOL
• On the Termination of Integer Loops
• Proving Termination of Integer Term Rewriting
• Increasing interpretations
• Termination Graphs for Java Bytecode
• 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
• A Tool Proving Well-Definedness of Streams Using Termination Tools
• Type Preservation as a Confluence Problem
• All-Termination(T)
• Fast offline partial evaluation of logic programs
• Accelerated Modal Abstractions of Labelled Transition Systems
• Automation of Recursive Path Ordering for Infinite Labelled Rewrite Systems
• Behavioral Rewrite Systems and Behavioral Productivity
• Certifying a Termination Criterion Based on Graphs, without Graphs
• Termination analysis and call graph construction for higher-order functional programs
• Non-termination analysis of logic programs with integer arithmetics
• Harnessing First Order Termination Provers Using Higher Order Dependency Pairs
• Dependency Pairs for Rewriting with Non-free Constructors
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Formalizing Soundness and Completeness of Unravelings
• Termination of Cycle Rewriting by Transformation and Matrix Interpretation
• Proving Injectivity of Functions via Program Inversion in Term Rewriting
• The recursive path and polynomial ordering for first-order and higher-order terms
• Argument Filterings and Usable Rules for Simply Typed Dependency Pairs
• Parametrized verification diagrams: temporal verification of symmetric parametrized concurrent systems
• Proving Termination with (Boolean) Satisfaction
• Termination Analysis of Logic Programs Based on Dependency Graphs
• Type-based analysis of logarithmic amortised complexity
• Transforming SAT into Termination of Rewriting
• Twenty years of rewriting logic
• Match-bounds revisited
• Explaining safety failures in NetKAT
• Inferring expected runtimes of probabilistic integer programs using expected sizes
• Proving Termination in the Context-Sensitive Dependency Pair Framework
• 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
• Termination of Isabelle Functions via Termination of Rewriting
• Certification of Termination Proofs Using CeTA
• Termination of narrowing via termination of rewriting
• Term Rewriting and Applications

This page was built for software: AProVE