BibSLEIGH — termination tag

termination

termination

Tag #termination

436 papers:

POPL-2020-WangFCDX #probability #proving #random #source code: Proving expected sensitivity of probabilistic programs with randomized variable-dependent termination time (PW, HF0, KC, YD, MX), p. 30.
FSCD-2019-0001K #higher-order #polymorphism: Polymorphic Higher-Order Termination (LC0, CK), p. 18.
FSCD-2019-BlanquiGH #dependence #dependent type #modulo theories #type system: Dependency Pairs Termination in Dependent Type Theory Modulo Rewriting (FB, GG, OH), p. 21.
FSCD-2019-Faggian #normalisation #probability: Probabilistic Rewriting: Normalization, Termination, and Unique Normal Forms (CF), p. 25.
FSCD-2019-GeserHW #string: Sparse Tiling Through Overlap Closures for Termination of String Rewriting (AG, DH, JW), p. 21.
OOPSLA-2019-Huang0CG #composition #probability #source code #verification: Modular verification for almost-sure termination of probabilistic programs (MH, HF0, KC, AKG), p. 29.
PEPM-2019-Asai #call-by #proving: Extracting a call-by-name partial evaluator from a proof of termination (KA), pp. 61–67.
PLDI-2019-NguyenGTH #contract #higher-order #source code: Size-change termination as a contract: dynamically and statically enforcing termination for higher-order programs (PCN, TG, STH, DVH), pp. 845–859.
CAV-2019-FrohnG #decidability #integer: Termination of Triangular Integer Loops is Decidable (FF, JG), pp. 426–444.
VMCAI-2019-FuC #nondeterminism #probability #source code: Termination of Nondeterministic Probabilistic Programs (HF0, KC), pp. 468–490.
PLDI-2018-ChenHLLTTZ #algorithm: Advanced automata-based algorithms for program termination checking (YFC, MH, OL, YL0, MHT, AT, LZ0), pp. 135–150.
POPL-2018-AgrawalC0 #approach #performance #probability #ranking #source code: Lexicographic ranking supermartingales: an efficient approach to termination of probabilistic programs (SA, KC, PN0), p. 32.
POPL-2018-LiY #algorithm #analysis #problem #quantum #source code: Algorithmic analysis of termination problems for quantum programs (YL, MY), p. 29.
POPL-2018-McIverMKK #proving: A new proof rule for almost-sure termination (AM, CM, BLK, JPK), p. 28.
SAS-2018-Zuleger #abstraction #induction #invariant #proving: Inductive Termination Proofs with Transition Invariants and Their Relationship to the Size-Change Abstraction (FZ), pp. 423–444.
CC-2018-ColinL #composition #source code: Termination checking and task decomposition for task-based intermittent programs (AC, BL), pp. 116–127.
CAV-2018-FedyukovichZG #analysis: Syntax-Guided Termination Analysis (GF, YZ, AG), pp. 124–143.
POPL-2017-ChatterjeeNZ #invariant #probability: Stochastic invariants for probabilistic termination (KC, PN0, DZ), pp. 145–160.
ESEC-FSE-2017-XieCZLLL #analysis #named: Loopster: static loop termination analysis (XX, BC0, LZ, SWL, YL0, XL), pp. 84–94.
ESOP-2017-LagoG #monad #probability #type system: Probabilistic Termination by Monadic Affine Sized Typing (UDL, CG), pp. 393–419.
CADE-2017-BrockschmidtJT0 #integer #proving #safety: Certifying Safety and Termination Proofs for Integer Transition Systems (MB, SJCJ, RT, AY0), pp. 454–471.
SEFM-2016-HenselGFS #execution #proving #source code #symbolic computation: Proving Termination of Programs with Bitvector Arithmetic by Symbolic Execution (JH, JG, FF, TS), pp. 234–252.
ICFP-2016-WatanabeST0 #automation #functional #higher-order #source code: Automatically disproving fair termination of higher-order functional programs (KW, RS, TT, NK0), pp. 243–255.
POPL-2016-ChatterjeeFNH #algorithm #analysis #probability #problem #source code: Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs (KC, HF0, PN0, RH), pp. 327–342.
SAS-2016-FrielinghausSV #analysis #interprocedural: Enforcing Termination of Interprocedural Analysis (SSF, HS, RV), pp. 447–468.
ESOP-2016-PintoDGS #composition #concurrent #verification: Modular Termination Verification for Non-blocking Concurrency (PdRP, TDY, PG, JS), pp. 176–201.
CAV-2016-ChatterjeeFG #analysis #probability #source code: Termination Analysis of Probabilistic Programs Through Positivstellensatz's (KC, HF0, AKG), pp. 3–22.
CAV-2016-ManevichDR #analysis #linear: From Shape Analysis to Termination Analysis in Linear Time (RM, BD, NR), pp. 426–446.
PODS-2015-CalauttiGP: Chase Termination for Guarded Existential Rules (MC, GG, AP), pp. 91–103.
TLCA-2015-JouannaudL: Termination of Dependently Typed Rewrite Rules (JPJ, JL), pp. 257–272.
ICGT-2015-Bruggink0NZ #graph #graph transformation #proving #using: Proving Termination of Graph Transformation Systems Using Weighted Type Graphs over Semirings (HJSB, BK, DN, HZ), pp. 52–68.
ECOOP-2015-JacobsBK #composition #verification: Modular Termination Verification (BJ, DB, RK), pp. 664–688.
PLDI-2015-LeQC #specification: Termination and non-termination specification inference (TCL, SQ, WNC), pp. 489–498.
POPL-2015-FioritiH #composition #probability: Probabilistic Termination: Soundness, Completeness, and Compositionality (LMFF, HH), pp. 489–501.
PPDP-2015-Fruhwirth #recursion: A devil’s advocate against termination of direct recursion (TWF), pp. 103–113.
ASE-2015-ChenDKSW #interprocedural #proving: Synthesising Interprocedural Bit-Precise Termination Proofs (T) (HYC, CD, DK, PS, BW), pp. 53–64.
ESOP-2015-DavidKL #source code #strict: Unrestricted Termination and Non-termination Arguments for Bit-Vector Programs (CD, DK, ML), pp. 183–204.
ESOP-2015-DavidKL15a #reasoning #safety #source code: Propositional Reasoning about Safety and Termination of Heap-Manipulating Programs (CD, DK, ML), pp. 661–684.
TACAS-2015-StroderAFHG #c #contest #memory management #named #safety #source code: AProVE: Termination and Memory Safety of C Programs — (Competition Contribution) (TS, CA, FF, JH, JG), pp. 417–419.
TACAS-2015-Urban #abstract domain #contest #named: FuncTion: An Abstract Domain Functor for Termination — (Competition Contribution) (CU), pp. 464–466.
CADE-2015-GieslMRTW #contest: Termination Competition (termCOMP 2015) (JG, FM, AR, RT, JW), pp. 105–108.
CADE-2015-IborraNVY #dependence #problem: Reducing Relative Termination to Dependency Pair Problems (JI, NN, GV, AY), pp. 163–178.
CAV-2015-DSilvaU: Conflict-Driven Conditional Termination (VD, CU), pp. 271–286.
CAV-2015-KuwaharaSU0 #abstraction #functional #higher-order #source code: Predicate Abstraction and CEGAR for Disproving Termination of Higher-Order Functional Programs (TK, RS, HU, NK), pp. 287–303.
ICALP-v2-2014-GogaczM #decidability: All-Instances Termination of Chase is Undecidable (TG, JM), pp. 293–304.
RTA-TLCA-2014-SternagelT #algebra #certification #complexity #formal method #proving: Formalizing Monotone Algebras for Certification of Termination and Complexity Proofs (CS, RT), pp. 441–455.
RTA-TLCA-2014-ZantemaKB: Termination of Cycle Rewriting (HZ, BK, HJSB), pp. 476–490.
PPDP-2014-LucasM #declarative #logic #proving #source code: Proving Operational Termination of Declarative Programs in General Logics (SL, JM), pp. 111–122.
SAS-2014-BrotherstonG #abduction #safety: Cyclic Abduction of Inductively Defined Safety and Termination Preconditions (JB, NG), pp. 68–84.
SAS-2014-UrbanM #abstract domain #proving: A Decision Tree Abstract Domain for Proving Conditional Termination (CU, AM), pp. 302–318.
SLE-J-2012-KrishnanW #analysis #attribute grammar #composition #higher-order: Monolithic and modular termination analyses for higher-order attribute grammars (LK, EVW), pp. 511–526.
DATE-2014-BishnoiEOT #power management #symmetry: Asynchronous Asymmetrical Write Termination (AAWT) for a low power STT-MRAM (RB, ME, FO, MBT), pp. 1–6.
ESOP-2014-KuwaharaTU0 #automation #functional #higher-order #source code #verification: Automatic Termination Verification for Higher-Order Functional Programs (TK, TT, HU, NK), pp. 392–411.
WRLA-2014-LucasM #order: Strong and Weak Operational Termination of Order-Sorted Rewrite Theories (SL, JM), pp. 178–194.
WRLA-2014-LucasM14a #2d #dependence #proving: 2D Dependency Pairs for Proving Operational Termination of CTRSs (SL, JM), pp. 195–212.
CAV-2014-HeizmannHP #analysis #learning #source code: Termination Analysis by Learning Terminating Programs (MH, JH, AP), pp. 797–813.
CAV-2014-KupriyanovF #concurrent #multi #source code #thread: Causal Termination of Multi-threaded Programs (AK, BF), pp. 814–830.
ICLP-J-2014-DuckHS #confluence #consistency #on the #type inference: On Termination, Confluence and Consistent CHR-based Type Inference (GJD, RH, MS), pp. 619–632.
IJCAR-2014-GieslBEFFOPSSST #automation #proving #source code: Proving Termination of Programs Automatically with AProVE (JG, MB, FE, FF, CF, CO, MP, PSK, TS, SS, RT), pp. 184–191.
IJCAR-2014-StroderGBFFHS #memory management #pointer #proving #safety #source code: Proving Termination and Memory Safety for Programs with Pointer Arithmetic (TS, JG, MB, FF, CF, JH, PSK), pp. 208–223.
VMCAI-2014-Masse #policy #ranking: Policy Iteration-Based Conditional Termination and Ranking Functions (DM), pp. 453–471.
LATA-2013-AotoI #calculus #rule-based: Termination of Rule-Based Calculi for Uniform Semi-Unification (TA, MI), pp. 56–67.
RTA-2013-BauLNW #analysis #term rewriting: Compression of Rewriting Systems for Termination Analysis (AB, ML, EN, JW), pp. 97–112.
RTA-2013-WinklerZM #automation #proving #sequence: Beyond Peano Arithmetic — Automatically Proving Termination of the Goodstein Sequence (SW, HZ, AM), pp. 335–351.
ICFP-2013-AbelP #approach #pattern matching #recursion: Wellfounded recursion with copatterns: a unified approach to termination and productivity (AA, BP), pp. 185–196.
ESEC-FSE-2013-Nori0 #proving #testing: Termination proofs from tests (AVN, RS), pp. 246–256.
PPoPP-2013-LifflanderMK #detection #fault tolerance #protocol: Adoption protocols for fanout-optimal fault-tolerant termination detection (JL, PM, LVK), pp. 13–22.
TACAS-2013-CookSZ #proving: Ramsey vs. Lexicographic Termination Proving (BC, AS, FZ), pp. 47–61.
CAV-2013-BrockschmidtCF #proving: Better Termination Proving through Cooperation (MB, BC, CF), pp. 413–429.
CAV-2013-GantyG #proving: Proving Termination Starting from the End (PG, SG), pp. 397–412.
ICLP-J-2013-GrecoMT #bottom-up #evaluation #logic programming: Logic programming with function symbols: Checking termination of bottom-up evaluation through program adornments (SG, CM, IT), pp. 737–752.
SCAM-2012-Vidal #execution #symbolic computation #verification: Closed Symbolic Execution for Verifying Program Termination (GV), pp. 34–43.
DLT-2012-KetemaS #normalisation #string: Characterizing Languages by Normalization and Termination in String Rewriting — (JK, JGS), pp. 459–464.
ICALP-v2-2012-BrazdilKNW #markov #process: Minimizing Expected Termination Time in One-Counter Markov Decision Processes (TB, AK, PN, DW), pp. 141–152.
LATA-2012-Bozzelli #abstraction #constraints: Strong Termination for Gap-Order Constraint Abstractions of Counter Systems (LB), pp. 155–168.
RTA-2012-ThiemannAN #formal method #multi #on the #order: On the Formalization of Termination Techniques based on Multiset Orderings (RT, GA, JN), pp. 339–354.
FLOPS-2012-Lobachev #parallel: Parallel Computation Skeletons with Premature Termination Property (OL), pp. 197–212.
ICFP-2012-StefanRBLMM #concurrent #data flow: Addressing covert termination and timing channels in concurrent information flow systems (DS, AR, PB, AL, JCM, DM), pp. 201–214.
PEPM-2012-AlbertAGGP #named: COSTABS: a cost and termination analyzer for ABS (EA, PA, SG, MGZ, GP), pp. 151–154.
POPL-2012-CousotC #abstract interpretation #framework: An abstract interpretation framework for termination (PC, RC), pp. 245–258.
SAS-2012-ChenFM #linear #proving: Termination Proofs for Linear Simple Loops (HYC, SF, SM), pp. 422–438.
ICSE-2012-Ghardallou #analysis #invariant #using: Using invariant relations in the termination analysis of while loops (WG), pp. 1519–1522.
SLE-2012-KrishnanW #analysis #attribute grammar #higher-order: Termination Analysis for Higher-Order Attribute Grammars (LK, EVW), pp. 44–63.
WRLA-J-2010-EscobarSM12: Folding variant narrowing and optimal variant termination (SE, RS, JM), pp. 898–928.
TACAS-2012-BozgaIK: Deciding Conditional Termination (MB, RI, FK), pp. 252–266.
TACAS-2012-PopeeaR #composition #concurrent #multi #proving #source code #thread: Compositional Termination Proofs for Multi-threaded Programs (CP, AR), pp. 237–251.
CAV-2012-BrockschmidtMOG #automation #java #proving #source code: Automated Termination Proofs for Java Programs with Cyclic Data (MB, RM, CO, JG), pp. 105–122.
CAV-2012-EsparzaGK #probability #proving #source code #using: Proving Termination of Probabilistic Programs Using Patterns (JE, AG, SK), pp. 123–138.
CAV-2012-LeeWY #algorithm #analysis #learning: Termination Analysis with Algorithmic Learning (WL, BYW, KY), pp. 88–104.
ICLP-2012-GrecoST #logic programming #on the #source code: On the Termination of Logic Programs with Function Symbols (SG, FS, IT), pp. 323–333.
IJCAR-2012-RauSS #correctness #problem #program transformation: Correctness of Program Transformations as a Termination Problem (CR, DS, MSS), pp. 462–476.
VMCAI-2012-Ben-AmramGM #integer #on the: On the Termination of Integer Loops (AMBA, SG, ANM), pp. 72–87.
VLDB-2011-GrecoST: Stratification Criteria and Rewriting Techniques for Checking Chase Termination (SG, FS, IT), pp. 1158–1168.
ICALP-v2-2011-BrazdilBEK #approximate #game studies #probability: Approximating the Termination Value of One-Counter MDPs and Stochastic Games (TB, VB, KE, AK), pp. 332–343.
FM-2011-Dunne #csp: Termination without √ in CSP (SD), pp. 278–292.
RTA-2011-BrockschmidtOG #bytecode #composition #java #proving #recursion #source code #term rewriting: Modular Termination Proofs of Recursive Java Bytecode Programs by Term Rewriting (MB, CO, JG), pp. 155–170.
RTA-2011-FalkeKS #analysis #c #compilation #source code #using: Termination Analysis of C Programs Using Compiler Intermediate Languages (SF, DK, CS), pp. 41–50.
RTA-2011-MoserS #complexity #dependence #framework #multi #proving #recursion: Termination Proofs in the Dependency Pair Framework May Induce Multiple Recursive Derivational Complexity (GM, AS), pp. 235–250.
RTA-2011-NeurauterM #matrix #proving #term rewriting: Revisiting Matrix Interpretations for Proving Termination of Term Rewriting (FN, AM), pp. 251–266.
Haskell-2011-BolingbrokeJV #combinator: Termination combinators forever (MCB, SLPJ, DV), pp. 23–34.
LOPSTR-2011-PilozziS #analysis #self #using: Improved Termination Analysis of CHR Using Self-sustainability Analysis (PP, DDS), pp. 189–204.
LOPSTR-2011-SneyersS #probability #source code: Probabilistic Termination of CHRiSM Programs (JS, DDS), pp. 221–236.
LOPSTR-2011-StroderESGF #analysis #complexity #linear #prolog #semantics: A Linear Operational Semantics for Termination and Complexity Analysis of ISO Prolog (TS, FE, PSK, JG, CF), pp. 237–252.
TACAS-2011-PodelskiR #abstraction #invariant: Transition Invariants and Transition Predicate Abstraction for Program Termination (AP, AR), pp. 3–10.
TACAS-2011-TsitovichSWK #analysis #summary: Loop Summarization and Termination Analysis (AT, NS, CMW, DK), pp. 81–95.
CADE-2011-Cook #liveness #proving #roadmap: Advances in Proving Program Termination and Liveness (BC), p. 4.
CADE-2011-WinklerM #tool support: AC Completion with Termination Tools (SW, AM), pp. 492–498.
ICLP-J-2011-CodishGBFG #analysis #constraints #integer #satisfiability #using: SAT-based termination analysis using monotonicity constraints over the integers (MC, IG, AMBA, CF, JG), pp. 503–520.
VMCAI-2011-PiskacW #automation #proving: Decision Procedures for Automating Termination Proofs (RP, TW), pp. 371–386.
VLDB-2010-SpezzanoG #approach #constraints: Chase Termination: A Constraints Rewriting Approach (FS, SG), pp. 93–104.
IFM-2010-Dimovski #composition #equivalence #nondeterminism #source code: A Compositional Method for Deciding Equivalence and Termination of Nondeterministic Programs (AD), pp. 121–135.
RTA-2010-DurandSS #bound #linear #term rewriting: Termination of linear bounded term rewriting systems (ID, GS, MS), pp. 341–356.
RTA-2010-OttoBEG #analysis #automation #bytecode #java #term rewriting: Automated Termination Analysis of Java Bytecode by Term Rewriting (CO, MB, CvE, JG), pp. 259–276.
ICGT-2010-BisztrayH: Combining Termination Criteria by Isolating Deletion (DB, RH), pp. 203–217.
LOPSTR-2010-StroderSG #analysis #dependence #logic programming #source code: Dependency Triples for Improving Termination Analysis of Logic Programs with Cut (TS, PSK, JG), pp. 184–199.
PEPM-2010-AndersonK #approximate #bound: Regular approximation and bounded domains for size-change termination (HA, SCK), pp. 53–62.
PEPM-2010-ContejeanPUCPF #approach #automation #proving: A3PAT, an approach for certified automated termination proofs (EC, AP, XU, PC, OP, JF), pp. 63–72.
SAS-2010-AliasDFG #bound #complexity #multi #ranking #source code: Multi-dimensional Rankings, Program Termination, and Complexity Bounds of Flowchart Programs (CA, AD, PF, LG), pp. 117–133.
SAS-2010-HarrisLNR: Alternation for Termination (WRH, AL, AVN, SKR), pp. 304–319.
SAS-2010-HeizmannJP #invariant: Size-Change Termination and Transition Invariants (MH, NDJ, AP), pp. 22–50.
TACAS-2010-Aderhold #analysis #automation #higher-order #recursion #source code: Automated Termination Analysis for Programs with Second-Order Recursion (MA), pp. 221–235.
WRLA-2010-EscobarSM: Folding Variant Narrowing and Optimal Variant Termination (SE, RS, JM), pp. 52–68.
WRLA-2010-GutierrezL #dependence #framework #proving: Proving Termination in the Context-Sensitive Dependency Pair Framework (RG, SL), pp. 18–34.
CAV-2010-KroeningSTW #analysis #composition #invariant: Termination Analysis with Compositional Transition Invariants (DK, NS, AT, CMW), pp. 89–103.
CSL-2010-SternagelT #dependence #proving: Signature Extensions Preserve Termination — An Alternative Proof via Dependency Pairs (CS, RT), pp. 514–528.
ICLP-J-2010-Schneider-KampGSST #analysis #automation #logic programming #source code: Automated termination analysis for logic programs with cut (PSK, JG, TS, AS, RT), pp. 365–381.
IJCAR-2010-HirokawaM #diagrams: Decreasing Diagrams and Relative Termination (NH, AM), pp. 487–501.
IJCAR-2010-WinklerM #order #tool support: Termination Tools in Ordered Completion (SW, AM), pp. 518–532.
PODS-2009-Marnette: Generalized schema-mappings: from termination to tractability (BM), pp. 13–22.
VLDB-2009-MeierSL #on the: On Chase Termination Beyond Stratification (MM, MS, GL), pp. 970–981.
CIAA-2009-IosifR #proving: Automata-Based Termination Proofs (RI, AR), pp. 165–177.
LATA-2009-Gnaedig: Termination of Priority Rewriting (IG), pp. 386–397.
RTA-2009-EndrullisVW: Local Termination (JE, RCdV, JW), pp. 270–284.
RTA-2009-FuhsGPSF #integer #proving #term rewriting: Proving Termination of Integer Term Rewriting (CF, JG, MP, PSK, SF), pp. 32–47.
RTA-2009-KorpSZM: Tyrolean Termination Tool 2 (MK, CS, HZ, AM), pp. 295–304.
RTA-2009-SchernhammerG #composition #named: VMTL — A Modular Termination Laboratory (FS, BG), pp. 285–294.
RTA-2009-Waldmann #automation: Automatic Termination (JW), pp. 1–16.
RTA-2009-Zantema: Well-Definedness of Streams by Termination (HZ), pp. 164–178.
LOPSTR-2009-IborraNV #dependence #proving: Goal-Directed and Relative Dependency Pairs for Proving the Termination of Narrowing (JI, NN, GV), pp. 52–66.
LOPSTR-2009-Schneider-KampGN #dependence #framework #logic programming #source code: The Dependency Triple Framework for Termination of Logic Programs (PSK, JG, MTN), pp. 37–51.
PPDP-2009-BiernackaB #proving: Context-based proofs of termination for typed delimited-control operators (MB, DB), pp. 289–300.
WRLA-2008-LucasM09 #equation #order #source code: Operational Termination of Membership Equational Programs: the Order-Sorted Way (SL, JM), pp. 207–225.
TACAS-2009-FogartyV #automaton: Büchi Complementation and Size-Change Termination (SF, MYV), pp. 16–30.
CADE-2009-FalkeK #analysis #approach #automation #imperative #source code #term rewriting: A Term Rewriting Approach to the Automated Termination Analysis of Imperative Programs (SF, DK), pp. 277–293.
CADE-2009-SwiderskiPGFS #analysis #dependence #induction #proving #theorem proving: Termination Analysis by Dependency Pairs and Inductive Theorem Proving (SS, MP, JG, CF, PSK), pp. 322–338.
CAV-2009-Ben-Amram #constraints #ranking: Size-Change Termination, Monotonicity Constraints and Ranking Functions (AMBA), pp. 109–123.
CSL-2009-BlanquiR #on the #semantics: On the Relation between Sized-Types Based Termination and Semantic Labelling (FB, CR), pp. 147–162.
ICLP-2009-Pilozzi #research #summary: Research Summary: Termination of CHR (PP), pp. 534–535.
ICLP-2009-PilozziS #proving: Proving Termination by Invariance Relations (PP, DDS), pp. 499–503.
ICLP-2009-PilozziS09a #automation #proving: Automating Termination Proofs for CHR (PP, DDS), pp. 504–508.
VMCAI-2009-Cook #liveness #roadmap: Advances in Program Termination and Liveness (BC), p. 4.
LATA-2008-KorpM #bound #dependence #proving #term rewriting: Match-Bounds with Dependency Pairs for Proving Termination of Rewrite Systems (MK, AM), pp. 321–332.
RTA-2008-AlpuenteEI #composition: Modular Termination of Basic Narrowing (MA, SE, JI), pp. 1–16.
RTA-2008-FuhsGMSTZ: Maximal Termination (CF, JG, AM, PSK, RT, HZ), pp. 110–125.
RTA-2008-KoprowskiW: Arctic Termination ...Below Zero (AK, JW), pp. 202–216.
RTA-2008-Toyama #lisp #proving #recursion #term rewriting: Termination Proof of S-Expression Rewriting Systems with Recursive Path Relations (YT), pp. 381–391.
FLOPS-2008-Vidal #linear: Termination of Narrowing in Left-Linear Constructor Systems (GV), pp. 113–129.
GT-VC-2007-Bruggink08 #graph transformation #proving #towards: Towards a Systematic Method for Proving Termination of Graph Transformation Systems (HJSB), pp. 23–38.
SEKE-2008-Chavarria-BaezL #approach #confluence #petri net: Analyzing Termination and Confluence in Active Rule Base via a Petri Net Approach (LCB, XL), pp. 363–366.
POPL-2008-BrotherstonBC #logic #proving: Cyclic proofs of program termination in separation logic (JB, RB, CC), pp. 101–112.
TACAS-2008-Ben-AmramC #approach #ranking #satisfiability: A SAT-Based Approach to Size Change Termination with Global Ranking Functions (AMBA, MC), pp. 218–232.
CAV-2008-CookGLRS #proving: Proving Conditional Termination (BC, SG, TLA, AR, MS), pp. 328–340.
CSL-2008-BartheGR #type system: Type-Based Termination with Sized Products (GB, BG, CR), pp. 493–507.
ICLP-2008-AlpuenteEI #dependence #using: Termination of Narrowing Using Dependency Pairs (MA, SE, JI), pp. 317–331.
ICLP-2008-PilozziS #analysis #revisited: Termination Analysis of CHR Revisited (PP, DDS), pp. 501–515.
IJCAR-2008-DuranLM #maude #named: MTT: The Maude Termination Tool (FD, SL, JM), pp. 313–319.
IJCAR-2008-SatoWKM #multi #tool support: Multi-completion with Termination Tools (HS, SW, MK, AM), pp. 306–312.
RTA-2007-GodoyHT: Termination of Rewriting with Right-Flat Rules (GG, EH, AT), pp. 200–213.
RTA-2007-KorpM #bound #proving #term rewriting #using: Proving Termination of Rewrite Systems Using Bounds (MK, AM), pp. 273–287.
RTA-2007-MarcheZ #contest: The Termination Competition (CM, HZ), pp. 303–313.
RTA-2007-ZantemaW: Termination by Quasi-periodic Interpretations (HZ, JW), pp. 404–418.
SEFM-2007-BabicHRC #proving: Proving Termination by Divergence (DB, AJH, ZR, BC), pp. 93–102.
ICFP-2007-Sereni #analysis #functional #graph #higher-order #source code: Termination analysis and call graph construction for higher-order functional programs (DS), pp. 71–84.
OOPSLA-2007-Rinard #using: Using early phase termination to eliminate load imbalances at barrier synchronization points (MCR), pp. 369–386.
LOPSTR-2007-Codish #proving: Proving Termination with (Boolean) Satisfaction (MC), pp. 1–7.
LOPSTR-2007-NguyenGSS #analysis #dependence #graph #logic programming #source code: Termination Analysis of Logic Programs Based on Dependency Graphs (MTN, JG, PSK, DDS), pp. 8–22.
PEPM-2007-Vidal #logic programming #partial evaluation #source code: Quasi-terminating logic programs for ensuring the termination of partial evaluation (GV), pp. 51–60.
PLDI-2007-CookPR #concurrent #proving #thread: Proving thread termination (BC, AP, AR), pp. 320–330.
PPDP-2007-Gnaedig #induction: Induction for positive almost sure termination (IG), pp. 167–178.
PPDP-2007-Lucas #proving #using: Practical use of polynomials over the reals in proofs of termination (SL), pp. 39–50.
CADE-2007-GieslTSS #bound #proving: Proving Termination by Bounded Increase (JG, RT, SS, PSK), pp. 443–459.
CADE-2007-Krauss: Certified Size-Change Termination (AK), pp. 460–475.
CAV-2007-Cook #automation #proving: Automatically Proving Program Termination (BC), p. 1.
SAT-2007-FuhsGMSTZ #analysis #polynomial #satisfiability: SAT Solving for Termination Analysis with Polynomial Interpretations (CF, JG, AM, PSK, RT, HZ), pp. 340–354.
RTA-2006-BournezG #proving: Proving Positive Almost Sure Termination Under Strategies (OB, FG), pp. 357–371.
RTA-2006-CodishLS #constraints #partial order: Solving Partial Order Constraints for LPO Termination (MC, VL, PJS), pp. 4–18.
RTA-2006-GieslSST #analysis #automation #haskell #programming language #term rewriting: Automated Termination Analysis for Haskell: From Term Rewriting to Programming Languages (JG, SS, PSK, RT), pp. 297–312.
RTA-2006-HofbauerW #matrix #string: Termination of String Rewriting with Matrix Interpretations (DH, JW), pp. 328–342.
RTA-2006-Koprowski06a #automation #named: TPA: Termination Proved Automatically (AK), pp. 257–266.
RTA-2006-WangS #decidability #linear: Decidability of Termination for Semi-constructor TRSs, Left-Linear Shallow TRSs and Related Systems (YW, MS), pp. 343–356.
RTA-2006-WehrmanSW #named: Slothrop: Knuth-Bendix Completion with a Modern Termination Checker (IW, AS, EMW), pp. 287–296.
FLOPS-2006-Avery #analysis #bound: Size-Change Termination and Bound Analysis (JA), pp. 192–207.
ICGT-2006-VarroVEPT #analysis #model transformation #petri net: Termination Analysis of Model Transformations by Petri Nets (DV, SVG, HE, UP, GT), pp. 260–274.
LOPSTR-2006-NguyenS #automation #named #polynomial #proving: Polytool: Proving Termination Automatically Based on Polynomial Interpretations (MTN, DDS), pp. 210–218.
LOPSTR-2006-Schneider-KampGST #analysis #automation #logic programming #source code #term rewriting: Automated Termination Analysis for Logic Programs by Term Rewriting (PSK, JG, AS, RT), pp. 177–193.
PLDI-2006-CookPR #proving: Termination proofs for systems code (BC, AP, AR), pp. 415–426.
ICSE-2006-ManoliosV #proving #static analysis #theorem proving: Integrating static analysis and general-purpose theorem proving for termination analysis (PM, DV), pp. 873–876.
ESOP-2006-CodishLSS #analysis: Size-Change Termination Analysis in k-Bits (MC, VL, PS, PJS), pp. 230–245.
TACAS-2006-LeueW #approach #graph #proving: A Region Graph Based Approach to Termination Proofs (SL, WW), pp. 318–333.
CAV-2006-BerdineCDO #automation #proving #source code: Automatic Termination Proofs for Programs with Shape-Shifting Heaps (JB, BC, DD, PWO), pp. 386–400.
CAV-2006-Braverman #integer #linear #source code: Termination of Integer Linear Programs (MB), pp. 372–385.
CAV-2006-ManoliosV #analysis #graph: Termination Analysis with Calling Context Graphs (PM, DV), pp. 401–414.
CSL-2006-Abel: Semi-continuous Sized Types and Termination (AA0), pp. 72–88.
IJCAR-2006-EndrullisWZ #matrix #proving #term rewriting: Matrix Interpretations for Proving Termination of Term Rewriting (JE, JW, HZ), pp. 574–588.
IJCAR-2006-GieslST #automation #dependence #framework #proving: Automatic Termination Proofs in the Dependency Pair Framework (JG, PSK, RT), pp. 281–286.
CIAA-J-2004-GeserHWZ05 #automaton #finite #string #term rewriting: Finding finite automata that certify termination of string rewriting systems (AG, DH, JW, HZ), pp. 471–486.
RTA-2005-BournezG #proving: Proving Positive Almost-Sure Termination (OB, FG), pp. 323–337.
RTA-2005-FernandezGR #order: Orderings for Innermost Termination (MLF, GG, AR), pp. 17–31.
RTA-2005-GeserHWZ #automaton #linear #on the #term rewriting: On Tree Automata that Certify Termination of Left-Linear Term Rewriting Systems (AG, DH, JW, HZ), pp. 353–367.
RTA-2005-Hamana #algebra #higher-order: Universal Algebra for Termination of Higher-Order Rewriting (MH), pp. 135–149.
RTA-2005-HirokawaM: Tyrolean Termination Tool (NH, AM), pp. 175–184.
RTA-2005-MoczydlowskiG #thread: Termination of Single-Threaded One-Rule Semi-Thue Systems (WM, AG), pp. 338–352.
TLCA-2005-BartheGP #polymorphism #type system: Practical Inference for Type-Based Termination in a Polymorphic Setting (GB, BG, FP), pp. 71–85.
ICFP-2005-FengS #assembly #composition #concurrent #thread #verification: Modular verification of concurrent assembly code with dynamic thread creation and termination (XF, ZS), pp. 254–267.
POPL-2005-PodelskiR #abstraction: Transition predicate abstraction and fair termination (AP, AR), pp. 132–144.
SAS-2005-BruynoogheGH #analysis #logic programming #source code: Inference of Well-Typings for Logic Programs with Application to Termination Analysis (MB, JPG, WVH), pp. 35–51.
SAS-2005-CookPR #abstraction #refinement: Abstraction Refinement for Termination (BC, AP, AR), pp. 87–101.
FASE-2005-EhrigELTVV #model transformation: Termination Criteria for Model Transformation (HE, KE, JdL, GT, DV, SVG), pp. 49–63.
CADE-2005-GodoyT #linear #term rewriting: Termination of Rewrite Systems with Shallow Right-Linear, Collapsing, and Right-Ground Rules (GG, AT), pp. 164–176.
ICLP-2005-CodishLS #constraints #testing: Testing for Termination with Monotonicity Constraints (MC, VL, PJS), pp. 326–340.
ICLP-2005-NguyenS #analysis #logic programming #polynomial #source code: Polynomial Interpretations as a Basis for Termination Analysis of Logic Programs (MTN, DDS), pp. 311–325.
VMCAI-2005-BradleyMS #polynomial #source code: Termination of Polynomial Programs (ARB, ZM, HBS), pp. 113–129.
VMCAI-2005-Cousot #abstraction #parametricity #programming #proving: Proving Program Invariance and Termination by Parametric Abstraction, Lagrangian Relaxation and Semidefinite Programming (PC), pp. 1–24.
CIAA-2004-GeserHWZ #automaton #finite #string: Finding Finite Automata That Certify Termination of String Rewriting (AG, DH, JW, HZ), pp. 134–145.
RTA-2004-Blanqui #higher-order #term rewriting #type system: A Type-Based Termination Criterion for Dependently-Typed Higher-Order Rewrite Systems (FB), pp. 24–39.
RTA-2004-GieslTSF #automation #proving: Automated Termination Proofs with AProVE (JG, RT, PSK, SF), pp. 210–220.
RTA-2004-JonesB #analysis #calculus: Termination Analysis of the Untyped lamba-Calculus (NDJ, NB), pp. 1–23.
RTA-2004-Lucas #named #proving: mu-term: A Tool for Proving Termination of Context-Sensitive Rewriting (SL), pp. 200–209.
RTA-2004-Toyama #higher-order #lisp #term rewriting: Termination of S-Expression Rewriting Systems: Lexicographic Path Ordering for Higher-Order Terms (YT), pp. 40–54.
RTA-2004-Zantema #automation #named: TORPA: Termination of Rewriting Proved Automatically (HZ), pp. 95–104.
SFM-2004-BaetenR #algebra #process: Timed Process Algebra (With a Focus on Explicit Termination and Relative-Timing) (JCMB, MAR), pp. 59–97.
LOPSTR-2004-SerebrenikM #on the #source code: On Termination of Binary CLP Programs (AS, FM), pp. 231–244.
PDCL-2004-LindenstraussSS #approach #logic programming #proving #source code: Proving Termination for Logic Programs by the Query-Mapping Pairs Approach (NL, YS, AS), pp. 453–498.
PDCL-2004-PedreschiRS #logic programming: Characterisations of Termination in Logic Programming (DP, SR, JGS), pp. 376–431.
PEPM-2004-DuranLMMU #equation #proving #source code: Proving termination of membership equational programs (FD, SL, JM, CM, XU), pp. 147–158.
FoSSaCS-2004-Lucas #proving: Polynomials for Proving Termination of Context-Sensitive Rewriting (SL), pp. 318–332.
CAV-2004-Tiwari #linear #source code: Termination of Linear Programs (AT), pp. 70–82.
CSL-2004-DawsonG #theorem: A General Theorem on Termination of Rewriting (JED, RG), pp. 100–114.
ICLP-2004-Dershowitz #abstraction: Termination by Abstraction (ND), pp. 1–18.
ICLP-2004-Smaus #logic programming #source code #using: Termination of Logic Programs Using Various Dynamic Selection Rules (JGS), pp. 43–57.
IJCAR-2004-ThiemannGS #composition #dependence #proving #using: Improved Modular Termination Proofs Using Dependency Pairs (RT, JG, PSK), pp. 75–90.
LICS-2004-Leivant #logic #proving: Proving Termination Assertions in Dynamic Logics (DL), pp. 89–98.
RTA-2003-AotoY #term rewriting: Termination of Simply Typed Term Rewriting by Translation and Labelling (TA, TY), pp. 380–394.
RTA-2003-Geser #string: Termination of String Rewriting Rules That Have One Pair of Overlaps (AG), pp. 410–423.
RTA-2003-HirokawaM: Tsukuba Termination Tool (NH, AM), pp. 311–320.
RTA-2003-ThiemannG #term rewriting: Size-Change Termination for Term Rewriting (RT, JG), pp. 264–278.
TLCA-2003-Abel: Termination and Productivity Checking with Continuous Types (AA0), pp. 1–15.
LOPSTR-2003-SerebrenikS #proving: Proving Termination with Adornments (AS, DDS), pp. 108–109.
PPDP-2003-FissoreGK #rule-based: Simplification and termination of strategies in rule-based languages (OF, IG, HK), pp. 124–135.
SAS-2003-TardieuS: Instantaneous Termination in Pure Esterel (OT, RdS), pp. 91–108.
FoSSaCS-2003-BlanchetP #encryption #protocol #verification: Verification of Cryptographic Protocols: Tagging Enforces Termination (BB, AP), pp. 136–152.
ICLP-2003-LagoonMS #analysis: Termination Analysis with Types Is More Accurate (VL, FM, PJS), pp. 254–268.
ICLP-2003-Serebrenik #analysis #logic programming #source code: Termination Analysis of Logic Programs: Extended Abstract (AS), pp. 507–508.
ICLP-2003-Smaus03a #logic programming #source code: Termination of Logic Programs for Various Dynamic Selection Rules (JGS), pp. 511–512.
DLT-2002-GieslM: Innermost Termination of Context-Sensitive Rewriting (JG, AM), pp. 231–244.
RTA-2002-Lucas #canonical: Termination of (Canonical) Context-Sensitive Rewriting (SL), pp. 296–310.
ICFP-2002-JonesG #analysis #generative: Program generation, termination, and binding-time analysis (NDJ, AJG), p. 283.
ICGT-2002-GodardMMS #algorithm #detection #distributed #graph: Termination Detection of Distributed Algorithms by Graph Relabelling Systems (EG, YM, MM, AS), pp. 106–119.
ICPR-v3-2002-Al-OhaliCS: Introducing Termination Probabilities to HMM (YAO, MC, CYS), pp. 319–322.
PPDP-2002-FissoreGK #induction #proving: System Presentation — CARIBOO: An induction based proof tool for termination with strategies (OF, IG, HK), pp. 62–73.
PPDP-2002-GramlichL #composition: Modular termination of context-sensitive rewriting (BG, SL), pp. 50–61.
PPDP-2002-JonesG #analysis #generative: Abstract and conclusions of PLI invited paper: program generation, termination, and binding-time analysis (NDJ, AJG), p. 1.
SAS-2002-BruynoogheCGV #analysis #logic programming #reuse #source code #using: Reuse of Results in Termination Analysis of Typed Logic Programs (MB, MC, SG, WV), pp. 477–492.
SAS-2002-MesnardPN #detection #logic programming #source code: Detecting Optimal Termination Conditions of Logic Programs (FM, ÉP, UN), pp. 509–526.
SAS-2002-SerebrenikS #float #logic programming #on the #source code: On Termination of Logic Programs with Floating Point Computations (AS, DDS), pp. 151–164.
GPCE-2002-JonesG #analysis #generative: Program Generation, Termination, and Binding-Time Analysis (NDJ, AJG), pp. 1–31.
GPCE-2002-Lee #analysis #polynomial: Program Termination Analysis in Polynomial Time (CSL), pp. 218–235.
WRLA-2002-FissoreGK: Outermost ground termination (OF, IG, HK), pp. 188–207.
CAV-2002-ColonS #proving: Practical Methods for Proving Program Termination (MC, HS), pp. 442–454.
VMCAI-2002-CharatonikMP #analysis #composition: Compositional Termination Analysis of Symbolic Forward Analysis (WC, SM, AP), pp. 109–125.
VMCAI-2002-GenaimCGL: Combining Norms to Prove Termination (SG, MC, JPG, VL), pp. 126–138.
RTA-2001-Hofbauer #proving: Termination Proofs by Context-Dependent Interpretations (DH), pp. 108–121.
RTA-2001-Raamsdonk #higher-order #on the: On Termination of Higher-Order Rewriting (FvR), pp. 261–275.
RTA-2001-Yamada #confluence #term rewriting: Confluence and Termination of Simply Typed Term Rewriting Systems (TY), pp. 338–352.
CIKM-2001-Couchot #analysis #composition #set: Termination Analysis of Active Rules Modular Sets (AC), pp. 326–333.
SIGIR-2001-VoKM #effectiveness #ranking: Vector-Space Ranking with Effective Early Termination (VNA, OdK, AM), pp. 35–42.
POPL-2001-LeeJB: The size-change principle for program termination (CSL, NDJ, AMBA), pp. 81–92.
PPDP-2001-BossiCR #logic programming #source code: Termination of Well-Typed Logic Programs (AB, NC, SR), pp. 73–81.
PPDP-2001-Lucas #on-demand #source code: Termination of On-Demand Rewriting and Termination of OBJ Programs (SL), pp. 82–93.
SAS-2001-MesnardN #logic programming #source code #static analysis: Applying Static Analysis Techniques for Inferring Termination Conditions of Logic Programs (FM, UN), pp. 93–110.
SAS-2001-Monniaux #analysis #probability #source code: An Abstract Analysis of the Probabilistic Termination of Programs (DM), pp. 111–126.
ESOP-2001-BossiERS #logic programming #scheduling #semantics #source code: Semantics and Termination of Simply-Moded Logic Programs with Dynamic Scheduling (AB, SE, SR, JGS), pp. 402–416.
IJCAR-2001-Jones #analysis #graph: Program Termination Analysis by Size-Change Graphs (NDJ), pp. 1–4.
IJCAR-2001-Pientka #higher-order #logic programming #reduction #source code: Termination and Reduction Checking for Higher-Order Logic Programs (BP), pp. 401–415.
IJCAR-2001-Urbain #automation #incremental #proving #term rewriting: Automated Incremental Termination Proofs for Hierarchically Defined Term Rewriting Systems (XU), pp. 485–498.
LICS-2001-Xi #dependent type #verification: Dependent Types for Program Termination Verification (HX), pp. 231–242.
RTA-2000-Blanqui #confluence #higher-order #term rewriting: Termination and Confluence of Higher-Order Rewrite Systems (FB), pp. 47–61.
RTA-2000-OhlebuschCM #analysis #logic programming #named #source code: TALP: A Tool for the Termination Analysis of Logic Programs (EO, CC, CM), pp. 270–273.
LOPSTR-2000-SerebrenikS #analysis #logic programming #source code: Non-tranformational termination analysis of logic programs, based on general term-orderings (AS, DDS).
LOPSTR-J-2000-SerebrenikS #analysis #logic programming #source code: Non-transformational Termination Analysis of Logic Programs, Based on General Term-Orderings (AS, DDS), pp. 69–85.
PPDP-2000-Gramlich #preprocessor #proving #term rewriting: Simplifying termination proofs for rewrite systems by preprocessing (BG), pp. 139–150.
SAIG-2000-SongF #approach: A New Termination Approach for Specialization (LS, YF), pp. 72–91.
SAS-2000-Mauborgne: Tree Schemata and Fair Termination (LM), pp. 302–321.
FASE-2000-HuismanJ #hoare #java #logic #verification: Java Program Verification via a Hoare Logic with Abrupt Termination (MH, BJ), pp. 284–303.
WRLA-2000-KirchnerG #normalisation #proving: Termination and normalisation under strategy Proofs in ELAN (HK, IG), pp. 93–120.
CL-2000-BraileyPN #analysis #approach #database: A Dynamic Approach to Termination Analysis for Active Database Rules (JB, AP, PN), pp. 1106–1120.
CL-2000-DebrayH #analysis #constraints #database: Constraint-Based Termination Analysis for Cyclic Active Database Rules (SKD, TJH), pp. 1121–1136.
CSL-2000-OhsakiMG #equation #semantics: Equational Termination by Semantic Labelling (HO, AM, JG), pp. 457–471.
VLDB-1999-LeeL: Unrolling Cycles to Decide Trigger Termination (SYL, TWL), pp. 483–493.
FM-v2-1999-Eschbach #algorithm #detection #specification #verification: A Termination Detection Algorithm: Specification and Verification (RE), pp. 1720–1737.
TLCA-1999-Ritter: Characterising Explicit Substitutions which Preserve Termination (ER), pp. 325–339.
FLOPS-1999-VerbaetenS #analysis #logic programming #source code #using: Termination Analysis of Tabled Logic Programs Using Mode and Type Information (SV, DDS), pp. 163–178.
PPDP-1999-KamareddineM #on the #proving #recursion: On Formalised Proofs of Termination of Recursive Functions (FK, FM), pp. 29–46.
PPDP-1999-VerbaetenSS #composition #prolog #proving: Modular Termination Proofs for Prolog with Tabling (SV, KFS, DDS), pp. 342–359.
PDP-1999-Ludwig #approach #exception #workflow: Termination handling in inter-organisational workflows-an exception management approach (HL), pp. 122–129.
ICLP-1999-Smaus #logic programming #proving #source code: Proving Termination of Input-Consuming Logic Programs (JGS), pp. 335–349.
ICLP-1999-Verbaeten #abduction #analysis #logic programming #source code: Termination Analysis for Abductive General Logic Programs (SV), pp. 365–379.
PODS-1998-BaileyDR #database #decidability #problem: Decidability and Undecidability Results for the Termination Problem of Active Database Rules (JB, GD, KR), pp. 264–273.
RTA-1998-AotoT: Termination Transformation by Tree Lifting Ordering (TA, YT), pp. 256–270.
RTA-1998-ArtsG #composition #dependence #using: Modularity of Termination Using Dependency pairs (TA, JG), pp. 226–240.
RTA-1998-MarcheU #commutative #dependence: Termination of Associative-Commutative Rewriting by Dependency Pairs (CM, XU), pp. 241–255.
RTA-1998-Xi #automation #proving #towards: Towards Automated Termination Proofs through “Freezing” (HX), pp. 271–285.
ALP-PLILP-1998-SmausHK #logic programming #source code: Termination of Logic Programs with block Declarations Running in Several Modes (JGS, PMH, AK), pp. 73–88.
LOPSTR-1998-HoarauM #compilation #constraints #logic programming #source code: Inferring and Compiling Termination for Constraint Logic Programs (SH, FM), pp. 240–254.
LOPSTR-1998-Leuschel #online: Improving Homeomorphic Embedding for Online Termination (ML), pp. 199–218.
SAS-1998-Leuschel #on the #online #power of: On the Power of Homeomorphic Embedding for Online Termination (ML), pp. 230–245.
CADE-1998-BrauburgerG #analysis #evaluation #induction: Termination Analysis by Inductive Evaluation (JB, JG), pp. 254–269.
JICSLP-1998-DecorteS #analysis: Termination Analysis: Some Practical Properties of the Norm and Level Mapping Space (SD, DDS), pp. 235–249.
ICALP-1997-Ruggieri #constraints #logic programming #source code: Termination of Constraint Logic Programs (SR), pp. 838–848.
RTA-1997-KapurS #order #proving #term rewriting: A Total, Ground path Ordering for Proving Termination of AC-Rewrite Systems (DK, GS), pp. 142–156.
RTA-1997-Zantema: Termination of Context-Sensitive Rewriting (HZ), pp. 172–186.
AdaEurope-1997-WellingsBP #ada: Task Termination in Ada 95 (AJW, AB, OP), pp. 149–160.
ALP-1997-BartheR #algebra #approach #type system: Termination of Algebraic Type Systems: The Syntactic Approach (GB, FvR), pp. 174–193.
ALP-1997-CodishT #analysis #constraints #logic programming #semantics #source code #using: A Semantic Basis for Termination Analysis of Logic Programs and Its Realization Using Symbolic Norm Constraints (MC, CT), pp. 31–45.
LOPSTR-1997-DecorteSLMS #analysis #logic programming: Termination Analysis for Tabled Logic Programming (SD, DDS, ML, BM, KFS), pp. 111–127.
LOPSTR-1997-LeuschelMS #logic programming #source code: Preserving Termination of Tabled Logic Programs While Unfolding (ML, BM, KFS), pp. 189–205.
SAS-1997-Braunburger #analysis #automation #order #polynomial #using: Automatic Termination Analysis for Partial Functions Using Polynomial Orderings (JB), pp. 330–344.
SAS-1997-PanitzS #automation #functional #higher-order #named #proving #source code #strict: TEA: Automatically Proving Termination of Programs in a Non-strict Higher-Order Functional Language (SEP, MSS), pp. 345–360.
SAS-1997-SpeirsSS #analysis: Termination Analysis for Mercury (CS, ZS, HS), pp. 160–171.
TAPSOFT-1997-ArtsG #automation #order #proving: Automatically Proving Termination Where Simplification Orderings Fail (TA, JG), pp. 261–272.
TAPSOFT-1997-GenetG #constraints #proving #using: Termination Proofs Using gpo Ordering Constraints (TG, IG), pp. 249–260.
TAPSOFT-1997-GeserMOZ: Relative Undecidability in the Termination Hierarchy of Single Rewrite Rules (AG, AM, EO, HZ), pp. 237–248.
CAV-1997-LindenstraussSS #logic programming #named #query #source code: TermiLog: A System for Checking Termination of Queries to Logic Programs (NL, YS, AS), pp. 444–447.
ICLP-1997-LindenstraussS #analysis #automation #logic programming #source code: Automatic Termination Analysis of Logic Programs (NL, YS), pp. 63–77.
ICALP-1996-Lucas: Termination of Context-Sensitive Rewriting by Rewriting (SL), pp. 122–133.
RTA-1996-ArtsG: Termination of Constructor Systems (TA, JG), pp. 63–77.
RTA-1996-Gramlich #on the #proving: On Proving Termination by Innermost Termination (BG), pp. 93–107.
RTA-1996-Rao #composition #graph grammar: Modularity of Termination in Term Graph Rewriting (MRKKR), pp. 230–244.
RTA-1996-Senizergues #on the #problem: On the Termination Problem for One-Rule Semi-Thue System (GS), pp. 302–316.
ALP-1996-OlveszkyL #order: Order-Sorted Termination: The Unsorted Way (PCÖ, OL), pp. 92–106.
LOPSTR-1996-BossiC: Replacement Can Preserve Termination (AB, NC), pp. 104–129.
SAS-1996-AndersenH #analysis #functional #higher-order #partial evaluation: Termination Analysis for Offline Partial Evaluation of a Higher Order Functional Language (PHA, CKH), pp. 67–82.
SAS-1996-BrauburgerG #analysis: Termination Analysis for Partial Functions (JB, JG), pp. 113–127.
SAS-1996-MullerGS #automation #composition #prolog #proving #source code: Automated Modular Termination Proofs for Real Prolog Programs (MM, TG, KS), pp. 220–237.
ESOP-1996-RohwedderP #higher-order #logic programming #source code: Mode and Termination Checking for Higher-Order Logic Programs (ER, FP), pp. 296–310.
CADE-1996-KolbeW #proving #reuse #theorem proving: Termination of Theorem Proving by Reuse (TK, CW), pp. 106–120.
CADE-1996-MiddeldorpOZ #self: Transforming Termination by Self-Labelling (AM, HO, HZ), pp. 373–387.
CADE-1996-Sengler #algorithm #data type: Termination of Algorithms over Non-freely Generated Data Types (CS), pp. 121–135.
ICALP-1995-DiekertG #concurrent: A Domain for Concurrent Termination: A Generalization of Mazurkiewicz Traces (VD, PG), pp. 15–26.
RTA-1995-Giesl #generative #order #polynomial #proving: Generating Polynomial Orderings for Termination Proofs (JG), pp. 426–431.
RTA-1995-Kahrs #proving #towards: Towards a Domain Theory for Termination Proofs (SK), pp. 241–255.
RTA-1995-LysneP #higher-order #term rewriting: A Termination Ordering for Higher Order Rewrite System (OL, JP), pp. 26–40.
RTA-1995-Steinbach #automation #order #proving: Automatic Termination Proofs With Transformation Orderings (JS), pp. 11–25.
RTA-1995-ZantemaG: A Complete Characterization of Termination of O^p 1^q -> 1^r O^s (HZ, AG), pp. 41–55.
TLCA-1995-Leclerc #coq #development #multi #order #proving #term rewriting: Termination Proof of Term Rewriting System with the Multiset Path Ordering. A Complete Development in the System Coq (FL), pp. 312–327.
TLCA-1995-PolS #proving #strict: Strict Functionals for Termination Proofs (JvdP, HS), pp. 350–364.
LOPSTR-1995-ArtsZ #logic programming #semantics #source code #unification #using: Termination of Logic Programs Using Semantic Unification (TA, HZ), pp. 219–233.
SAS-1995-Giesl #analysis #functional #order #source code #using: Termination Analysis for Functional Programs using Term Orderings (JG), pp. 154–171.
ICLP-1995-MartensG #deduction #flexibility: Ensuring Global Termination of Partial Deduction while Allowing Flexible Polyvariance (BM, JPG), pp. 597–611.
ILPS-1995-LauOPP #correctness #logic programming #program transformation: Correctness of Logic Program Transformations Based on Existential Termination (KKL, MO, AP, MP), pp. 480–494.
ILPS-1995-MarchioriT #logic programming #proving #source code: Proving Termination of Logic Programs with Delay Declarations (EM, FT), pp. 447–461.
ALP-1994-BossiC: Preserving Universal Termination through Unfold/Fold (AB, NC), pp. 269–286.
ALP-1994-FerreiraZ #analysis: Syntactical Analysis of Total Termination (MCFF, HZ), pp. 204–222.
ALP-1994-Gramlich #composition #confluence #on the #term rewriting: On Modularity of Termination and Confluence Properties of Conditional Rewrite Systems (BG), pp. 186–203.
LOPSTR-1994-CookG #analysis #source code: A Transformation System for Definite Programs Based on Termination Analysis (JC, JPG), pp. 51–68.
SAC-1994-GhazalO #constraints #query #source code: Termination of programs in constraint query languages (AG, AMO), pp. 266–270.
DAC-1994-GuptaP #named: OTTER: Optimal Termination of Transmission Lines Excluding Radiation (RG, LTP), pp. 640–645.
CADE-1994-BasinW #order: Termination Orderings for Rippling (DAB, TW), pp. 466–483.
CADE-1994-Martin #geometry #invariant: Termination, Geometry and Invariants (UM), pp. 432–434.
CADE-1994-MiddeldorpZ #revisited: Simple Termination Revisited (AM, HZ), pp. 451–465.
ICALP-1993-BarbaneraF #composition #confluence #term rewriting: Modularity of Termination and Confluence in Combinations of Rewrite Systems with λω (FB, MF), pp. 657–668.
RTA-1993-DershowitzH #topic: Topics in Termination (ND, CH), pp. 198–212.
RTA-1993-FerreiraZ #term rewriting: Total Termination of Term Rewriting (MCFF, HZ), pp. 213–227.
RTA-1993-MiddeldorpG: Simple Termination is Difficult (AM, BG), pp. 228–242.
RTA-1993-Plaisted #constraints #polynomial #testing: Polynomial Time Termination and Constraint Satisfaction Tests (DAP), pp. 405–420.
RTA-1993-Senizergues #decidability #problem: Some Undecidable Termination Problems for Semi-Thue Systems (GS), p. 434.
CIKM-1993-VoortS #confluence #execution: Termination and Confluence of Rule Execution (LvdV, AS), pp. 245–255.
TAPSOFT-1993-Dershowitz: Trees, Ordinals and Termination (ND), pp. 243–250.
ICLP-1993-RaoKS #haskell #proving #source code: Proving Termination of GHC Programs (MRKKR, DK, RKS), pp. 720–736.
ILPS-1993-AguzziM #logic programming #source code #term rewriting: Termination of Logic Programs via Equivalent Rewrite Systems (GA, UM), p. 634.
ILPS-1993-DecorteSF #analysis #automation: Automatic Inference of Norms: A Missing Link in Automatic Termination Analysis (SD, DDS, MF), pp. 420–436.
SIGMOD-1992-AikenWH #behaviour #confluence #database: Behavior of Database Production Rules: Termination, Confluence, and Observable Determinism (AA, JW, JMH), pp. 59–68.
ALP-1992-Gnaedig #order: Termination of Order-sorted Rewriting (IG), pp. 37–52.
ALP-1992-Gramlich #composition: Generalized Sufficient Conditions for Modular Termination of Rewriting (BG), pp. 53–68.
ALP-1992-Lescanne #term rewriting: Termination of Rewrite Systems by Elementary Interpretations (PL), pp. 21–36.
LOPSTR-1992-VerschaetseDS #analysis #automation: Automatic Termination Analysis (KV, SD, DDS), pp. 168–183.
PLILP-1992-Amtoft: Unfold/fold Transformations Preserving Termination Properties (TA), pp. 187–201.
CADE-1992-Christian: Some Termination Criteria for Narrowing and E-Narrowing (JC), pp. 582–588.
JICSLP-1992-BronsardLR #framework #logic programming #proving #source code: A Framework of Directionality for Proving Termination of Logic Programs (FB, TKL, USR), pp. 321–335.
JICSLP-1992-GrogerP #automation #logic programming #proving #recursion #source code: Handling of Mutual Recursion in Automatic Termination Proofs for Logic Programs (GG, LP), pp. 336–350.
PODS-1991-SohnG #detection #logic programming #source code #using: Termination Detection in Logic Programs using Argument Sizes (KS, AVG), pp. 216–226.
RTA-1991-DrewesL #incremental #proving: Incremental Termination Proofs and the Length of Derivations (FD, CL), pp. 49–61.
RTA-1991-Hofbauer #bound #proving #term rewriting: Time Bounded Rewrite Systems and Termination Proofs by Generalized Embedding (DH), pp. 62–73.
RTA-1991-Salomaa #confluence #decidability #monad #term rewriting: Decidability of Confluence and Termination of Monadic Term Rewriting Systems (KS), pp. 275–286.
CCPSD-1991-BossiCF #logic programming #proving #source code: Proving Termination of Logic Programs by Exploiting Term Properties (AB, NC, MF), pp. 153–180.
CSL-1991-RaoKS #logic programming #proving #source code: A Transformational Methodology for Proving Termination of Logic Programs (MRKKR, DK, RKS), pp. 213–226.
CSL-1991-Weiermann #proving #term rewriting: Proving Termination for Term Rewriting Systems (AW), pp. 419–428.
ICLP-1991-RossS #algebra #prolog #semantics: An Algebraic Semantics of Prolog Program Termination (BJR, AS), pp. 316–330.
ICLP-1991-VerschaetseS #logic programming #proving #source code #using: Deriving Termination Proofs for Logic Programs, Using Abstract Procedures (KV, DDS), pp. 301–315.
ISLP-1991-Plumer #automation #prolog #proving #source code: Automatic Termination Proofs for Prolog Programs Operating on Nonground Terms (LP), pp. 503–517.
ISLP-1991-Sagiv #logic programming #source code: A Termination Test for Logic Programs (YS), pp. 518–532.
ALP-1990-Hofbauer #multi #order #proving #recursion: Termination Proofs by Multiset Path Orderings Imply Primitive Recursive Derivation Lengths (DH), pp. 347–358.
PLILP-1990-WangS #logic programming #source code #towards: Towards a Characterization of Termination of Logic Programs (BW, RKS), pp. 204–221.
CLP-1990-Plumer90 #logic programming #proving #source code: Termination Proofs for Logic Programs Based on Predicate Inequalities (LP), pp. 634–648.
RTA-1989-HofbauerL #proving: Termination Proofs and the Length of Derivations (DH, CL), pp. 167–177.
RTA-1989-LatchS #term rewriting: A Local Termination Property for Term Rewriting Systems (DML, RS), pp. 222–233.
RTA-1989-Tison #decidability: Fair Termination is Decidable for Ground Systems (ST), pp. 462–476.
RTA-1989-ToyamaKB #linear #term rewriting: Termination for the Direct Sum of left-Linear Term Rewriting Systems -Preliminary Draft- (YT, JWK, HPB), pp. 477–491.
LICS-1989-Middeldorp #term rewriting: A Sufficient Condition for the Termination of the Direct Sum of Term Rewriting Systems (AM), pp. 396–401.
NACLP-1989-Bezem #logic programming #source code: Characterizing Termination of Logic Programs with Level Mappings (MB), pp. 69–80.
CADE-1988-Walther #algorithm #automation #bound #proving: Argument-Bounded Algorithms as a Basis for Automated Termination Proofs (CW), pp. 602–621.
CSL-1988-Plumer #automation #prolog #proving #source code: Predicate Inequalities as a Basis for Automated Termination Proofs for Prolog Programs (LP), pp. 254–271.
LICS-1988-Baudinet #approach #prolog #proving #semantics #source code: Proving Termination Properties of Prolog Programs: A Semantic Approach (MB), pp. 336–347.
LICS-1988-CartwrightD: The Topology of Program Termination (RC, AJD), pp. 296–308.
ICALP-1986-Lai #communication #detection #distributed: A Termination Detector for Static and Dynamic Distributed Systems with Asynchronous Non-first-in-first-out Communication (THL), pp. 196–205.
ICALP-1986-RosierY #complexity #concurrent #finite #on the #probability #source code: On The Complexity of Deciding Fair Termination of Probabilistic Concurrent Finite-State Programs (LER, HCY), pp. 334–343.
CADE-1986-BachmairD: Commutation, Transformation, and Termination (LB, ND), pp. 5–20.
CADE-1986-CherifaL #implementation #polynomial #term rewriting: An Actual Implementation of a Procedure That Mechanically Proves Termination of Rewriting Systems Based on Inequalities Between Polynomial Interpretations (ABC, PL), pp. 42–51.
CADE-1986-GnaedigL #commutative #proving #term rewriting: Proving Termination of Associative Commutative Rewriting Systems by Rewriting (IG, PL), pp. 52–61.
RTA-1985-Dershowitz: Termination (ND), pp. 180–224.
RTA-1985-DetlefsF #automation #proving #set: A Procedure for Automatically Proving the Termination of a Set of Rewrite Rules (DD, RF), pp. 255–270.
CAAP-1985-KapurNS #order #proving #term rewriting: A Path Ordering for Proving Termination of Term Rewriting Systems (DK, PN, GS), pp. 173–187.
POPL-1984-FrancezK: Generalized Fair Termination (NF, DK), pp. 46–53.
CADE-1984-JouannaudM #equation #set: Termination of a Set of Rules Modulo a Set of Equations (JPJ, MM), pp. 175–193.
PODS-1983-ChinR #clustering #network: Optimal Termination Prococols for Network Partitioning (FYLC, KVSR), pp. 25–35.
POPL-1982-HartSP #concurrent #probability #source code: Termination of Probabilistic Concurrent Programs (SH, MS, AP), pp. 1–6.
ICALP-1981-Dershowitz #linear #term rewriting: Termination of Linear Rewriting Systems (ND), pp. 448–458.
ICALP-1981-LehmannPS #concurrent: Impartiality, Justice and Fairness: The Ethics of Concurrent Termination (DJL, AP, JS), pp. 264–277.
ICALP-1981-Pettorossi #order #proving #recursion #term rewriting: Comparing and Putting Together Recursive Path Ordering, Simplification Orderings and Non-Ascending Property for Termination Proofs of Term Rewriting Systems (AP), pp. 432–447.
CADE-1980-Jeanrond #algebra #term rewriting: Deciding Unique Termination of Permutative Rewriting Systems: Choose Your Term Algebra Carefully (HJJ), pp. 335–355.
ICALP-1979-DershowitzM #multi #order #proving: Proving termination with Multiset Orderings (ND, ZM), pp. 188–202.
ICALP-1979-Jeanrond #axiom #commutative #theorem: A Unique Termination Theorem for a Theory with Generalised Commutative Axioms (HJJ), pp. 316–330.
ICALP-1977-BohmCD #testing #λ-calculus: Termination Tests inside λ-Calculus (CB, MC, MDC), pp. 95–110.
ICALP-1976-Bakker #nondeterminism #recursion #semantics #source code: Semantics and Termination of Nondeterministic Recursive Programs (JWdB), pp. 435–477.
ICALP-1976-Schwarz #proving #reasoning #source code: Event Based Reasoning — A System for Proving Correct Termination of Programs (JS), pp. 131–146.
ICALP-1972-HitchcockP #induction #proving: Induction Rules and Termination Proofs (PH, DMRP), pp. 225–251.