AProVE
From MaRDI portal
Cited in
(only showing first 100 items - show all)- Match-bounds revisited
- Increasing interpretations
- On-demand strategy annotations revisited: an improved on-demand evaluation strategy
- COSTA
- iRankFinder
- ComplexityParser
- TALP
- CLEAN
- BABEL
- Haskell
- Termination and complexity analysis for programs with bitvector arithmetic by symbolic execution
- Automating regression verification of pointer programs by predicate abstraction
- Yices
- CEGAR
- Complexity analysis for term rewriting by integer transition systems
- Conflict-driven conditional termination
- Fairness modulo theory: a new approach to LTL software model checking
- Relational program reasoning using compiler IR
- OBJ3
- Constant runtime complexity of term rewriting is semi-decidable
- CafeOBJ
- Maude
- Timbuk
- CeTA
- TERMINATOR
- GiNaCRA
- Twenty years of rewriting logic
- Cseq
- SMTInterpol
- Ultimate Automizer
- ACL2s
- Tyrolean
- PMaude
- Explaining safety failures in NetKAT
- Inferring expected runtimes of probabilistic integer programs using expected sizes
- Temporal prophecy for proving temporal properties of infinite-state systems
- Derivational complexity and context-sensitive Rewriting
- Tuple interpretations for termination of term rewriting
- Term orderings for non-reachability of (conditional) rewriting
- \textsc{LTL} falsification in infinite-state systems
- Pattern eliminating transformations
- \textsc{ComplexityParser}: an automatic tool for certifying poly-time complexity of Java programs
- LLBMC
- Automatic discovery of fair paths in infinite-state transition systems
- MathSAT5
- ABC
- Sugar
- CSI
- MTT
- CoLoR
- ITP
- SCC
- Tom
- Transforming derivational complexity of term rewriting to runtime complexity
- DPPD
- HERMIT
- CiME
- MU-TERM
- mkbTT
- Slothrop
- CARIBOO
- VMTL
- Jambox
- Saigawa
- InvX
- IsaFoR
- TPDB
- TPA
- Matchbox
- Tsukuba
- TORPA
- SPIKE
- Time-bounded termination analysis for probabilistic programs with delays
- Maintaining a library of formal mathematics
- The 2D dependency pair framework for conditional rewrite systems. II: Advanced processors and implementation techniques
- A Perron-Frobenius theorem for deciding matrix growth
- Proving operational termination of membership equational programs
- From LCF to Isabelle/HOL
- Using well-founded relations for proving operational termination
- Conditions for confluence of innermost terminating term rewriting systems
- Relative termination via dependency pairs
- Automatically proving termination and memory safety for programs with pointer arithmetic
- SAT solving for termination proofs with recursive path orders and dependency pairs
- Lower bounds for runtime complexity of term rewriting
- Certifying confluence of quasi-decreasing strongly deterministic conditional term rewrite systems
- Certifying safety and termination proofs for integer transition systems
- Parametrized verification diagrams: temporal verification of symmetric parametrized concurrent systems
- Modular strategic SMT solving with \textbf{SMT-RAT}
- Fast offline partial evaluation of logic programs
- Enhancing dependency pair method using strong computability in simply-typed term rewriting
- CoCasl
- SMT-RAT
- CArL
- SymDiff
- On the relative power of polynomials with real, rational, and integer coefficients in proofs of termination of rewriting
- Conditional Confluence
- C-SHORe
- Lazy-CSeq
- The size-change principle and dependency pairs for termination of term rewriting
- Modular and incremental automated termination proofs
This page was built for software: AProVE
