BibSLEIGH
BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
EDIT!
CC-BY
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
termination
Google termination

Tag #termination

436 papers:

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

Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.