Analyzing program termination and complexity automatically with \textsf{AProVE} (Q2362493): Difference between revisions

@@ Property / describes a project that uses @@
+SMT-LIB
@@ Property / describes a project that uses: SMT-LIB / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+CeTA
@@ Property / describes a project that uses: CeTA / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Sat4j
@@ Property / describes a project that uses: Sat4j / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+SMTInterpol
@@ Property / describes a project that uses: SMTInterpol / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+KITTeL
@@ Property / describes a project that uses: KITTeL / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+MiniSat
@@ Property / describes a project that uses: MiniSat / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Coq
@@ Property / describes a project that uses: Coq / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Isabelle/HOL
@@ Property / describes a project that uses: Isabelle/HOL / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Sugar
@@ Property / describes a project that uses: Sugar / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+CoLoR
@@ Property / describes a project that uses: CoLoR / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Yices
@@ Property / describes a project that uses: Yices / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+z3
@@ Property / describes a project that uses: z3 / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+LLVM
@@ Property / describes a project that uses: LLVM / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+CiME
@@ Property / describes a project that uses: CiME / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1007/s10817-016-9388-y
+Normal rank
@@ Property / OpenAlex ID @@
+W2533836568
@@ Property / OpenAlex ID: W2533836568 / rank @@
+Normal rank
@@ Property / cites work @@
+Multi-dimensional Rankings, Program Termination, and Complexity Bounds of Flowchart Programs
+Normal rank
@@ Property / cites work @@
+Removing redundant arguments automatically
@@ Property / cites work: Removing redundant arguments automatically / rank @@
+Normal rank
@@ Property / cites work @@
+Analyzing innermost runtime complexity of term rewriting by dependency pairs
+Normal rank
@@ Property / cites work @@
+Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
+Normal rank
@@ Property / cites work @@
+CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates
+Normal rank
@@ Property / cites work @@
+Computer Aided Verification
@@ Property / cites work: Computer Aided Verification / rank @@
+Normal rank
@@ Property / cites work @@
+<tt>Polytool</tt>: Polynomial interpretations as a basis for termination analysis of logic programs
+Normal rank
@@ Property / cites work @@
+Modular Termination Proofs of Recursive Java Bytecode Programs by Term Rewriting
+Normal rank
@@ Property / cites work @@
+Matrix interpretations for proving termination of term rewriting
+Normal rank
@@ Property / cites work @@
+Proving termination by dependency pairs and inductive theorem proving
+Normal rank
@@ Property / cites work @@
+SAT solving for termination proofs with recursive path orders and dependency pairs
+Normal rank
@@ Property / cites work @@
+Q5389068
@@ Property / cites work: Q5389068 / rank @@
+Normal rank
@@ Property / cites work @@
+Ramsey vs. Lexicographic Termination Proving
@@ Property / cites work: Ramsey vs. Lexicographic Termination Proving / rank @@
+Normal rank
@@ Property / cites work @@
+Theory and Applications of Satisfiability Testing
@@ Property / cites work: Theory and Applications of Satisfiability Testing / rank @@
+Normal rank
@@ Property / cites work @@
+Proving Non-looping Non-termination Automatically
@@ Property / cites work: Proving Non-looping Non-termination Automatically / rank @@
+Normal rank
@@ Property / cites work @@
+Termination Analysis of C Programs Using Compiler Intermediate Languages
+Normal rank
@@ Property / cites work @@
+Inferring Lower Bounds for Runtime Complexity
@@ Property / cites work: Inferring Lower Bounds for Runtime Complexity / rank @@
+Normal rank
@@ Property / cites work @@
+Lower Runtime Bounds for Integer Programs
@@ Property / cites work: Lower Runtime Bounds for Integer Programs / rank @@
+Normal rank
@@ Property / cites work @@
+SAT Solving for Termination Analysis with Polynomial Interpretations
+Normal rank
@@ Property / cites work @@
+Maximal Termination
@@ Property / cites work: Maximal Termination / rank @@
+Normal rank
@@ Property / cites work @@
+Search Techniques for Rational Polynomial Orders
@@ Property / cites work: Search Techniques for Rational Polynomial Orders / rank @@
+Normal rank
@@ Property / cites work @@
+Proving Termination of Integer Term Rewriting
@@ Property / cites work: Proving Termination of Integer Term Rewriting / rank @@
+Normal rank
@@ Property / cites work @@
+Frontiers of Combining Systems
@@ Property / cites work: Frontiers of Combining Systems / rank @@
+Normal rank
@@ Property / cites work @@
+Mechanizing and improving dependency pairs
@@ Property / cites work: Mechanizing and improving dependency pairs / rank @@
+Normal rank
@@ Property / cites work @@
+Proving Termination by Bounded Increase
@@ Property / cites work: Proving Termination by Bounded Increase / rank @@
+Normal rank
@@ Property / cites work @@
+Proving Termination of Programs Automatically with AProVE
+Normal rank
@@ Property / cites work @@
+Proving Termination of Programs with Bitvector Arithmetic by Symbolic Execution
+Normal rank
@@ Property / cites work @@
+Q3077191
@@ Property / cites work: Q3077191 / rank @@
+Normal rank
@@ Property / cites work @@
+Lazy Abstraction with Interpolants
@@ Property / cites work: Lazy Abstraction with Interpolants / rank @@
+Normal rank
@@ Property / cites work @@
+Isabelle/HOL. A proof assistant for higher-order logic
+Normal rank
@@ Property / cites work @@
+Automated Termination Analysis of Java Bytecode by Term Rewriting
+Normal rank
@@ Property / cites work @@
+Verification, Model Checking, and Abstract Interpretation
+Normal rank
@@ Property / cites work @@
+Dependency Triples for Improving Termination Analysis of Logic Programs with Cut
+Normal rank
@@ Property / cites work @@
+Proving Termination and Memory Safety for Programs with Pointer Arithmetic
+Normal rank
@@ Property / cites work @@
+Compiling finite linear CSP into SAT
@@ Property / cites work: Compiling finite linear CSP into SAT / rank @@
+Normal rank
@@ Property / cites work @@
+Certification of Termination Proofs Using CeTA
@@ Property / cites work: Certification of Termination Proofs Using CeTA / rank @@
+Normal rank
@@ Property / cites work @@
+KBO orientability
@@ Property / cites work: KBO orientability / rank @@
+Normal rank
@@ links / mardi / name / links / mardi / name @@
+Publication:2362493