Travelled to:1 × Brazil
1 × Canada
1 × France
1 × Ireland
1 × Serbia
1 × The Netherlands
2 × Belgium
2 × Denmark
2 × Japan
2 × Poland
2 × Portugal
3 × Austria
3 × Spain
4 × Italy
5 × United Kingdom
6 × USA
7 × Germany
Collaborated with:P.Schneider-Kamp R.Thiemann T.Arts C.Fuhs A.Middeldorp T.Ströder F.Emmes D.Kapur ∅ M.Brockschmidt F.Frohn J.Brauburger C.Otto J.Hensel S.Swiderski S.Falke M.T.Nguyen M.Hark H.Zantema A.Serebrenik J.Waldmann C.Aschermann M.Codish T.Enger L.Noschinski H.Zankl H.Ohsaki P.Giesl M.Plücker R.Musiol C.v.Essen D.D.Schreye B.L.Kaminski J.Katoen F.Mesnard A.Rubio Y.Fekete I.Gonopolskiy A.M.Ben-Amram M.Parting M.Naaf S.Swiderski
Talks about:termin (35) program (18) analysi (15) rewrit (14) term (10) depend (9) prove (8) logic (7) proof (6) autom (6)
Person: Jürgen Giesl
DBLP: Giesl:J=uuml=rgen
Facilitated 2 volumes:
Ed
EdContributed to:
20152015
201520142014
20122012
2012
2012
20122011
201120112011201020102010200920092009200820072007
20072006200620062004200420032003
2002200120012000
20001999199919991998199819971996
199619951995
1997201620192019
2020Wrote 54 papers:
- CADE-2015-GieslMRTW #contest #termination
- Termination Competition (termCOMP 2015) (JG, FM, AR, RT, JW), pp. 105–108.
- RTA-2015-FrohnGHAS #bound #complexity #runtime
- Inferring Lower Bounds for Runtime Complexity (FF, JG, JH, CA, TS), pp. 334–349.
- TACAS-2015-StroderAFHG #c #contest #memory management #named #safety #source code #termination
- AProVE: Termination and Memory Safety of C Programs — (Competition Contribution) (TS, CA, FF, JH, JG), pp. 417–419.
- IJCAR-2014-GieslBEFFOPSSST #automation #proving #source code #termination
- 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 #termination
- Proving Termination and Memory Safety for Programs with Pointer Arithmetic (TS, JG, MB, FF, CF, JH, PSK), pp. 208–223.
- TACAS-2014-BrockschmidtEFFG #analysis #complexity #integer #runtime #source code
- Alternating Runtime and Size Complexity Analysis of Integer Programs (MB, FE, SF, CF, JG), pp. 140–155.
- CAV-2012-BrockschmidtMOG #automation #java #proving #source code #termination
- Automated Termination Proofs for Java Programs with Cyclic Data (MB, RM, CO, JG), pp. 105–122.
- IJCAR-2012-EmmesEG #automation #proving
- Proving Non-looping Non-termination Automatically (FE, TE, JG), pp. 225–240.
- LOPSTR-2012-GieslSSEF #evaluation #graph #logic programming #source code #symbolic computation #term rewriting
- Symbolic Evaluation Graphs and Term Rewriting — A General Methodology for Analyzing Logic Programs (JG, TS, PSK, FE, CF), p. 1.
- PPDP-2012-GieslSSEF #evaluation #graph #logic programming #source code #symbolic computation #term rewriting
- Symbolic evaluation graphs and term rewriting: a general methodology for analyzing logic programs (JG, TS, PSK, FE, CF), pp. 1–12.
- SMT-2012-CodishFFGW #constraints
- Exotic Semi-Ring Constraints (MC, YF, CF, JG, JW), pp. 88–97.
- CADE-2011-NoschinskiEG #analysis #complexity #dependence #framework #term rewriting
- A Dependency Pair Framework for Innermost Complexity Analysis of Term Rewrite Systems (LN, FE, JG), pp. 422–438.
- ICLP-J-2011-CodishGBFG #analysis #constraints #integer #satisfiability #termination #using
- SAT-based termination analysis using monotonicity constraints over the integers (MC, IG, AMBA, CF, JG), pp. 503–520.
- LOPSTR-2011-StroderESGF #analysis #complexity #linear #prolog #semantics #termination
- A Linear Operational Semantics for Termination and Complexity Analysis of ISO Prolog (TS, FE, PSK, JG, CF), pp. 237–252.
- RTA-2011-BrockschmidtOG #bytecode #composition #java #proving #recursion #source code #term rewriting #termination
- Modular Termination Proofs of Recursive Java Bytecode Programs by Term Rewriting (MB, CO, JG), pp. 155–170.
- ICLP-J-2010-Schneider-KampGSST #analysis #automation #logic programming #source code #termination
- Automated termination analysis for logic programs with cut (PSK, JG, TS, AS, RT), pp. 365–381.
- LOPSTR-2010-StroderSG #analysis #dependence #logic programming #source code #termination
- Dependency Triples for Improving Termination Analysis of Logic Programs with Cut (TS, PSK, JG), pp. 184–199.
- RTA-2010-OttoBEG #analysis #automation #bytecode #java #term rewriting #termination
- Automated Termination Analysis of Java Bytecode by Term Rewriting (CO, MB, CvE, JG), pp. 259–276.
- CADE-2009-SwiderskiPGFS #analysis #dependence #induction #proving #termination #theorem proving
- Termination Analysis by Dependency Pairs and Inductive Theorem Proving (SS, MP, JG, CF, PSK), pp. 322–338.
- LOPSTR-2009-Schneider-KampGN #dependence #framework #logic programming #source code #termination
- The Dependency Triple Framework for Termination of Logic Programs (PSK, JG, MTN), pp. 37–51.
- RTA-2009-FuhsGPSF #integer #proving #term rewriting #termination
- Proving Termination of Integer Term Rewriting (CF, JG, MP, PSK, SF), pp. 32–47.
- RTA-2008-FuhsGMSTZ #termination
- Maximal Termination (CF, JG, AM, PSK, RT, HZ), pp. 110–125.
- RTA-2008-ThiemannGS
- Deciding Innermost Loops (RT, JG, PSK), pp. 366–380.
- CADE-2007-GieslTSS #bound #proving #termination
- Proving Termination by Bounded Increase (JG, RT, SS, PSK), pp. 443–459.
- LOPSTR-2007-NguyenGSS #analysis #dependence #graph #logic programming #source code #termination
- Termination Analysis of Logic Programs Based on Dependency Graphs (MTN, JG, PSK, DDS), pp. 8–22.
- SAT-2007-FuhsGMSTZ #analysis #polynomial #satisfiability #termination
- SAT Solving for Termination Analysis with Polynomial Interpretations (CF, JG, AM, PSK, RT, HZ), pp. 340–354.
- IJCAR-2006-GieslST #automation #dependence #framework #proving #termination
- Automatic Termination Proofs in the Dependency Pair Framework (JG, PSK, RT), pp. 281–286.
- LOPSTR-2006-Schneider-KampGST #analysis #automation #logic programming #source code #term rewriting #termination
- Automated Termination Analysis for Logic Programs by Term Rewriting (PSK, JG, AS, RT), pp. 177–193.
- RTA-2006-GieslSST #analysis #automation #haskell #programming language #term rewriting #termination
- Automated Termination Analysis for Haskell: From Term Rewriting to Programming Languages (JG, SS, PSK, RT), pp. 297–312.
- IJCAR-2004-ThiemannGS #composition #dependence #proving #termination #using
- Improved Modular Termination Proofs Using Dependency Pairs (RT, JG, PSK), pp. 75–90.
- RTA-2004-GieslTSF #automation #proving #termination
- Automated Termination Proofs with AProVE (JG, RT, PSK, SF), pp. 210–220.
- CADE-2003-GieslK #equation #induction
- Deciding Inductive Validity of Equations (JG, DK), pp. 17–31.
- RTA-2003-GieslZ #liveness
- Liveness in Rewriting (JG, HZ), pp. 321–336.
- RTA-2003-ThiemannG #term rewriting #termination
- Size-Change Termination for Term Rewriting (RT, JG), pp. 264–278.
- DLT-2002-GieslM #termination
- Innermost Termination of Context-Sensitive Rewriting (JG, AM), pp. 231–244.
- IJCAR-2001-GieslK #decidability #induction #theorem
- Decidable Classes of Inductive Theorems (JG, DK), pp. 469–484.
- RTA-2001-GieslK #dependence #equation
- Dependency Pairs for Equational Rewriting (JG, DK), pp. 93–108.
- CADE-2000-GieslM
- Eliminating Dummy Elimination (JG, AM), pp. 309–323.
- CSL-2000-OhsakiMG #equation #semantics #termination
- Equational Termination by Semantic Labelling (HO, AM, JG), pp. 457–471.
- CSL-1999-ArtsG #erlang #process #verification
- Applying Rewriting Techniques to the Verification of Erlang Processes (TA, JG), pp. 96–110.
- LOPSTR-1999-Giesl #verification
- Context-Moving Transformations for Function Verification (JG), pp. 293–312.
- RTA-1999-GieslM #term rewriting
- Transforming Context-Sensitive Rewrite Systems (JG, AM), pp. 271–287.
- CADE-1998-BrauburgerG #analysis #evaluation #induction #termination
- Termination Analysis by Inductive Evaluation (JB, JG), pp. 254–269.
- RTA-1998-ArtsG #composition #dependence #termination #using
- Modularity of Termination Using Dependency pairs (TA, JG), pp. 226–240.
- RTA-1997-ArtsG #automation #normalisation #proving
- Proving Innermost Normalisation Automatically (TA, JG), pp. 157–171.
- RTA-1996-ArtsG #termination
- Termination of Constructor Systems (TA, JG), pp. 63–77.
- SAS-1996-BrauburgerG #analysis #termination
- Termination Analysis for Partial Functions (JB, JG), pp. 113–127.
- RTA-1995-Giesl #generative #order #polynomial #proving #termination
- Generating Polynomial Orderings for Termination Proofs (JG), pp. 426–431.
- SAS-1995-Giesl #analysis #functional #order #source code #termination #using
- Termination Analysis for Functional Programs using Term Orderings (JG), pp. 154–171.
- TAPSOFT-1997-ArtsG #automation #order #proving #termination
- Automatically Proving Termination Where Simplification Orderings Fail (TA, JG), pp. 261–272.
- IJCAR-2016-FrohnNHBG #bound #integer #runtime #source code
- Lower Runtime Bounds for Integer Programs (FF, MN, JH, MB, JG), pp. 550–567.
- CADE-2019-GieslGH #constant #probability #source code
- Computing Expected Runtimes for Constant Probability Programs (JG, PG, MH), pp. 269–286.
- CAV-2019-FrohnG #decidability #integer #termination
- Termination of Triangular Integer Loops is Decidable (FF, JG), pp. 426–444.
- POPL-2020-HarkKGK #bound #induction #probability #verification
- Aiming low is harder: induction for lower bounds in probabilistic program verification (MH, BLK, JG, JPK), p. 28.