AProVE
From MaRDI portal
Cited in
(only showing first 100 items - show all)- A Term Rewriting Approach to the Automated Termination Analysis of Imperative Programs
- State Space Reduction of Rewrite Theories Using Invisible Transitions
- Proving termination properties with \textsc{mu-term}
- Generalized and formalized uncurrying
- AC completion with termination tools
- On proving termination of constrained term rewrite systems by eliminating edges from dependency graphs
- Termination of Narrowing in Left-Linear Constructor Systems
- Twenty years of rewriting logic
- Operational termination of membership equational programs: the order-sorted way
- Match-bounds revisited
- scientific article; zbMATH DE number 7649967 (Why is no real title available?)
- Fast offline partial evaluation of logic programs
- Type Preservation as a Confluence Problem
- Left-linear bounded TRSs are inverse recognizability preserving
- All-Termination(T)
- Accelerated Modal Abstractions of Labelled Transition Systems
- Explaining safety failures in NetKAT
- Inferring expected runtimes of probabilistic integer programs using expected sizes
- Tuple interpretations for termination of term rewriting
- \textsc{LTL} falsification in infinite-state systems
- Time-bounded termination analysis for probabilistic programs with delays
- Deaccumulation techniques for improving provability
- Automatic discovery of fair paths in infinite-state transition systems
- Maintaining a library of formal mathematics
- Automation of Recursive Path Ordering for Infinite Labelled Rewrite Systems
- Proving operational termination of membership equational programs
- Harnessing first order termination provers using higher order dependency pairs
- Term orderings for non-reachability of (conditional) rewriting
- A Transformational Approach to Prove Outermost Termination Automatically
- Concurrent programming languages and methods for semantic analyses (extended abstract of invited talk)
- Grez
- Pattern eliminating transformations
- Proving termination of context-sensitive rewriting with MU-TERM
- Enhancing dependency pair method using strong computability in simply-typed term rewriting
- Term Rewriting and Applications
- Lazy productivity via termination
- Proving Termination of Rewrite Systems Using Bounds
- Using well-founded relations for proving operational termination
- Termination of narrowing via termination of rewriting
- Certification of Termination Proofs Using CeTA
- Complexity analysis for term rewriting by integer transition systems
- Term Rewriting and Applications
- Complexity of conditional term rewriting
- 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
- Fairness modulo theory: a new approach to LTL software model checking
- On the relative power of polynomials with real, rational, and integer coefficients in proofs of termination of rewriting
- Proving termination by dependency pairs and inductive theorem proving
- SAT modulo linear arithmetic for solving polynomial constraints
- Logic for Programming, Artificial Intelligence, and Reasoning
- Slothrop: Knuth-Bendix Completion with a Modern Termination Checker
- Goal-directed and relative dependency pairs for proving the termination of narrowing
- Formalizing soundness and completeness of unravelings
- Solving nonlinear integer arithmetic with MCSAT
- On-demand strategy annotations revisited: an improved on-demand evaluation strategy
- Proving termination and memory safety for programs with pointer arithmetic
- Polynomials over the reals in proofs of termination : from theory to practice
- Conditions for confluence of innermost terminating term rewriting systems
- Proving termination of context-sensitive rewriting by transformation
- Ranking functions for linear-constraint loops
- Verifying procedural programs via constrained rewriting induction
- Proving injectivity of functions via program inversion in term rewriting
- Towards Generic Programming with Sized Types
- Argument filterings and usable rules for simply typed dependency pairs
- Termination of cycle rewriting by transformation and matrix interpretation
- Transforming SAT into termination of rewriting
- Certifying a Termination Criterion Based on Graphs, without Graphs
- Termination Analysis with Calling Context Graphs
- Term Rewriting and Applications
- Conflict-driven conditional termination
- Derivational Complexity of Knuth-Bendix Orders Revisited
- Relative termination via dependency pairs
- KBO orientability
- Dependency Pairs for Rewriting with Built-In Numbers and Semantic Data Structures
- Mechanically proving termination using polynomial interpretations
- Termination analysis and call graph construction for higher-order functional programs
- Term Rewriting and Applications
- Elimination transformations for associative-commutative rewriting systems
- Termination graphs for Java bytecode
- On the termination of integer loops
- Non-termination analysis of logic programs with integer arithmetics
- Termination of Narrowing Using 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
- Modular termination proofs of recursive Java bytecode programs by term rewriting
- Behavioral rewrite systems and behavioral productivity
- Inferring lower bounds for runtime complexity
- Automating regression verification of pointer programs by predicate abstraction
- Justification logic and history based computation
- Proving termination in the context-sensitive dependency pair framework
- Automated Deduction – CADE-20
- Proving termination of programs automatically with AProVE
- Dependency Pairs for Rewriting with Non-free Constructors
- Reachability analysis of innermost rewriting
- COSTA
- TALP
- CLEAN
- BABEL
This page was built for software: AProVE
