AProVE

swMATH7831MaRDI QIDQ19847FDOQ19847

Author name not available (Why is that?)

Official website: http://aprove.informatik.rwth-aachen.de/

Described by source

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

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

• Title not available (Why is that?)
• Fast offline partial evaluation of logic programs
• Tuple interpretations for termination of term rewriting
• \textsc{LTL} falsification in infinite-state systems
• Time-bounded termination analysis for probabilistic programs with delays
• Automatic discovery of fair paths in infinite-state transition systems
• Concurrent programming languages and methods for semantic analyses (extended abstract of invited talk)
• 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
• Complexity of conditional term rewriting
• NaTT
• 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
• Proving termination and memory safety for programs with pointer arithmetic
• On-demand strategy annotations revisited: an improved on-demand evaluation strategy
• Termination analysis and call graph construction for higher-order functional programs
• 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
• Inferring lower bounds for runtime complexity
• Automating regression verification of pointer programs by predicate abstraction
• Proving termination of programs automatically with AProVE
• Resource analysis driven by (conditional) termination proofs
• Max/Plus tree automata for termination of term rewriting
• Title not available (Why is that?)
• 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
• 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
• Certification of complexity proofs using CeTA
• Certifying confluence of quasi-decreasing strongly deterministic conditional term rewrite systems
• Certifying safety and termination proofs for integer transition systems
• iRankFinder
• ComplexityParser
• Combining model checking and data-flow analysis
• Parametrized verification diagrams: temporal verification of symmetric parametrized concurrent systems
• 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
• Modular strategic SMT solving with \textbf{SMT-RAT}
• \textsc{ComplexityParser}: an automatic tool for certifying poly-time complexity of Java programs
• A Term Rewriting Approach to the Automated Termination Analysis of Imperative Programs
• Termination of Narrowing in Left-Linear Constructor Systems
• Operational termination of membership equational programs: the order-sorted way
• Left-linear bounded TRSs are inverse recognizability preserving
• Match-bounds revisited
• Deaccumulation techniques for improving provability
• A Transformational Approach to Prove Outermost Termination Automatically
• Term Rewriting and Applications
• Proving Termination of Rewrite Systems Using Bounds
• Lazy productivity via termination
• 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
• Logic for Programming, Artificial Intelligence, and Reasoning
• Polynomials over the reals in proofs of termination : from theory to practice
• Goal-directed and relative dependency pairs for proving the termination of narrowing
• Ranking functions for linear-constraint loops
• Solving nonlinear integer arithmetic with MCSAT
• Verifying procedural programs via constrained rewriting induction
• 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
• Towards Generic Programming with Sized Types
• 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
• Proving termination in the context-sensitive dependency pair framework
• Reachability analysis of innermost rewriting
• Detecting Non-termination of Term Rewriting Systems Using an Unfolding Operator
• Automated Reasoning
• Methods for proving termination of rewriting-based programming languages by transformation
• Proving termination of nonlinear command sequences
• A Perron-Frobenius theorem for deciding matrix growth
• On Equality Predicates in Algebraic Specification Languages

This page was built for software: AProVE