[an error occurred while processing this directive]<meta name="keywords" content="Department of Computer Science, publications, by title, Christoph Haase"></meta><meta name="description" content="Publications, by title, Department of Computer Science, Oxford, Christoph Haase"></meta><title>Department of Computer Science, University of Oxford: Christoph Haase : Publications
</title><style type="text/css">
			  .btn-toolbar::after, .btn-toolbar::before
			  {
			    content: " ";
			    display: table;
			  }

			
			.btn-toolbar
			{
			    margin-bottom: 2em;
			}

			  .btn-toolbar::after, .btn-group::after
			  {
			    clear: both;
			  }


			.btn-toolbar .btn, .btn-toolbar .btn-group
			  {
			    float: left;
			}
			
			.btn-group
			  {
			    display: inline-block;
			    position: relative;
			    vertical-align: middle;
			}

			  .btn-group > .btn:first-child:not(:last-child)
			  {
			    border-bottom-right-radius: 0;
			    border-top-right-radius: 0;
			}
			
			.btn-group > .btn:first-child
			  {
			    margin-left: 0;
			}

			.btn-group > .btn
			  {
			    float: left;
			    position: relative;
			}

			  .btn-group > .btn:not(:first-child):not(:last-child)
			  {
			    border-radius: 0;
			}
			
			  .btn-group > .btn:last-child:not(:first-child)
			  {
			    border-bottom-left-radius: 0;
			    border-top-left-radius: 0;
			}
			
			.btn-group .btn + .btn, .btn-group .btn + .btn-group, .btn-group .btn-group + .btn, .btn-group .btn-group + .btn-group
			  {
			    margin-left: -2px;
			}
			</style>[an error occurred while processing this directive]<div class="content-width"><ol class="breadcrumb text-uppercase"><li><a href="/">Home</a></li><li><a href="/aboutus/">About Us</a></li><li><a href="/people/">People</a></li><li><a href="/people/faculty.html">Faculty</a></li><li><a href="/people/Christoph.Haase"><span itemprop="name">Christoph Haase</span></a></li><li class="active">Publications</li></ol></div><!-- MOBILE NAVIGATION --><div class="content-width space-below mobile-menu-placeholder visible-xs visible-sm"></div><!-- COLUMNS --><div class="container-fluid content-width"><div class="row"><div class="col-xs-12 col-md-9 col-md-push-3" id="maincontent"><!-- CONTENT (Column 2) --><div class="page-title"><h1>Christoph Haase : Publications
</h1></div><div role="toolbar" class="btn-toolbar"><div class="btn-group"><a href="/people/publications/date/Christoph.Haase.html" aria-hidden="true" type="button" class="btn btn-default"><span class="glyphicon glyphicon-sort-by-attributes"></span> By date</a><a href="/people/publications/title/Christoph.Haase.html" aria-hidden="true" type="button" class="btn btn-oxford-blue"><span class="glyphicon glyphicon-sort-by-attributes"></span> By title</a><a href="/people/publications/type/Christoph.Haase.html" aria-hidden="true" type="button" class="btn btn-default"><span class="glyphicon glyphicon-sort-by-attributes"></span> By type</a><a href="/people/publications/bibtex/Christoph.Haase.html" aria-hidden="true" type="button" class="btn btn-default"><span class="glyphicon glyphicon-file"></span> BibTex</a></div></div><p></p><ul class="list-unbulleted list-unbulleted-spaced"><li>
	
	<div class="row">
		
			<div class="col-xs-1 text-right">
				[1] 
			</div>

		
        
		<div
			class="col-xs-11"
		>
			
	
	<p class="publicationTitle"> <strong>
            A Polynomial&#x2212;Time Algorithm for Reachability in Branching VASS in Dimension One </strong> </p>
	    <p class="publicationAuthors"> <em> Stefan G&#xf6;ller&#x201a; Christoph Haase&#x201a; Ranko Lazic and Patrick Totzke  </em> </p>
	
	<p class="publicationDetails"> 
            In  
            <em>
            Automata&#x201a; Languages&#x201a; and Programming&#x201a; ICALP</em>.
        
            Vol. 55
                of LIPIcs.
        
                Pages 105:1&#x2013;105:13.
            Schloss Dagstuhl &#x2212; Leibniz&#x2212;Zentrum fuer Informatik.
        2016.
        </p>
	
        		<p class="publicationlinks"> <a
        
            		href="/publications/publication14466-abstract.html">
			Details <span class="sr-only" > about <em> A Polynomial&#x2212;Time Algorithm for Reachability in Branching VASS in Dimension One  </em></span> </a> |
			<a href="/publications/publication14466.bib">
			BibTeX  <span class="sr-only" > data for <em> A Polynomial&#x2212;Time Algorithm for Reachability in Branching VASS in Dimension One  </em></span>   </a>
			
			 | <a
		href="http://dx.doi.org/10.4230/LIPIcs.ICALP.2016.105">
		DOI (10.4230/LIPIcs.ICALP.2016.105)
		</a> 
		
		</div> 
	</div> 
	
        </li><li>
	
	<div class="row">
		
			<div class="col-xs-1 text-right">
				[2] 
			</div>

		
        
		<div
			class="col-xs-11"
		>
			
	
	<p class="publicationTitle"> <strong>
            A survival guide to Presburger arithmetic </strong> </p>
	    <p class="publicationAuthors"> <em> Christoph Haase  </em> </p>
	
	<p class="publicationDetails"> 
        In <em>SIGLOG News</em>.
        
            Vol. 5.
        
            No. 3.
        
                Pages 67&#x2013;82.
            2018.
        </p>
	
        		<p class="publicationlinks"> <a
        
            		href="/publications/publication14455-abstract.html">
			Details <span class="sr-only" > about <em> A survival guide to Presburger arithmetic  </em></span> </a> |
			<a href="/publications/publication14455.bib">
			BibTeX  <span class="sr-only" > data for <em> A survival guide to Presburger arithmetic  </em></span>   </a>
			
			 | <a
		href="http://dx.doi.org/10.1145/3242953.3242964">
		DOI (10.1145/3242953.3242964)
		</a> 
		
		</div> 
	</div> 
	
        </li><li>
	
	<div class="row">
		
			<div class="col-xs-1 text-right">
				[3] 
			</div>

		
        
		<div
			class="col-xs-11"
		>
			
	
	<p class="publicationTitle"> <strong>
            Affine Extensions of Integer Vector Addition Systems with States </strong> </p>
	    <p class="publicationAuthors"> <em> Michael Blondin&#x201a; Christoph Haase and Filip Mazowiecki  </em> </p>
	
	<p class="publicationDetails"> 
            In  
            <em>
            Concurrency Theory&#x201a; CONCUR</em>.
        
            Vol. 118
                of LIPIcs.
        
                Pages 14:1&#x2013;14:17.
            Schloss Dagstuhl &#x2212; Leibniz&#x2212;Zentrum fuer Informatik.
        2018.
        </p>
	
        		<p class="publicationlinks"> <a
        
            		href="/publications/publication14464-abstract.html">
			Details <span class="sr-only" > about <em> Affine Extensions of Integer Vector Addition Systems with States  </em></span> </a> |
			<a href="/publications/publication14464.bib">
			BibTeX  <span class="sr-only" > data for <em> Affine Extensions of Integer Vector Addition Systems with States  </em></span>   </a>
			
			 | <a
		href="http://dx.doi.org/10.4230/LIPIcs.CONCUR.2018.14">
		DOI (10.4230/LIPIcs.CONCUR.2018.14)
		</a> 
		
		</div> 
	</div> 
	
        </li><li>
	
	<div class="row">
		
			<div class="col-xs-1 text-right">
				[4] 
			</div>

		
        
		<div
			class="col-xs-11"
		>
			
	
	<p class="publicationTitle"> <strong>
            Approaching Arithmetic Theories with Finite&#x2212;State Automata </strong> </p>
	    <p class="publicationAuthors"> <em> Christoph Haase  </em> </p>
	
	<p class="publicationDetails"> 
            In  
            <em>
            Language and Automata Theory and Applications&#x201a; LATA</em>.
        
            Vol. 12038
                of Lect. Notes Comp. Sci..
        
                Pages 1&#x2013;11.
            Springer.
        2020.
        </p>
	
        		<p class="publicationlinks"> <a
        
            		href="/publications/publication14480-abstract.html">
			Details <span class="sr-only" > about <em> Approaching Arithmetic Theories with Finite&#x2212;State Automata  </em></span> </a> |
			<a href="/publications/publication14480.bib">
			BibTeX  <span class="sr-only" > data for <em> Approaching Arithmetic Theories with Finite&#x2212;State Automata  </em></span>   </a>
			
			 | <a
		href="http://dx.doi.org/10.1007/978-3-030-40608-0_3">
		DOI (10.1007/978-3-030-40608-0_3)
		</a> 
		
		</div> 
	</div> 
	
        </li><li>
	
	<div class="row">
		
			<div class="col-xs-1 text-right">
				[5] 
			</div>

		
        
		<div
			class="col-xs-11"
		>
			
	
	<p class="publicationTitle"> <strong>
            Approaching the Coverability Problem Continuously </strong> </p>
	    <p class="publicationAuthors"> <em> Michael Blondin&#x201a; Alain Finkel&#x201a; Christoph Haase and Serge Haddad  </em> </p>
	
	<p class="publicationDetails"> 
            In  
            <em>
            Tools and Algorithms for the Construction and Analysis of Systems&#x201a; TACAS</em>.
        
            Vol. 9636
                of Lect. Notes Comp. Sci..
        
                Pages 480&#x2013;496.
            Springer.
        2016.
        </p>
	
        		<p class="publicationlinks"> <a
        
            		href="/publications/publication14461-abstract.html">
			Details <span class="sr-only" > about <em> Approaching the Coverability Problem Continuously  </em></span> </a> |
			<a href="/publications/publication14461.bib">
			BibTeX  <span class="sr-only" > data for <em> Approaching the Coverability Problem Continuously  </em></span>   </a>
			
			 | <a
		href="http://dx.doi.org/10.1007/978-3-662-49674-9\_28">
		DOI (10.1007/978-3-662-49674-9\_28)
		</a> 
		
		</div> 
	</div> 
	
        </li><li>
	
	<div class="row">
		
			<div class="col-xs-1 text-right">
				[6] 
			</div>

		
        
		<div
			class="col-xs-11"
		>
			
	
	<p class="publicationTitle"> <strong>
            Branching&#x2212;Time Model Checking of Parametric One&#x2212;Counter Automata </strong> </p>
	    <p class="publicationAuthors"> <em> Stefan G&#xf6;ller&#x201a; Christoph Haase&#x201a; Jo&#xeb;l Ouaknine and James Worrell  </em> </p>
	
	<p class="publicationDetails"> 
            In  
            <em>
            Foundations of Software Science and Computational Structures&#x201a; FOSSACS</em>.
        
            Vol. 7213
                of Lect. Notes Comp. Sci..
        
                Pages 406&#x2013;420.
            Springer.
        2012.
        </p>
	
        		<p class="publicationlinks"> <a
        
            		href="/publications/publication14470-abstract.html">
			Details <span class="sr-only" > about <em> Branching&#x2212;Time Model Checking of Parametric One&#x2212;Counter Automata  </em></span> </a> |
			<a href="/publications/publication14470.bib">
			BibTeX  <span class="sr-only" > data for <em> Branching&#x2212;Time Model Checking of Parametric One&#x2212;Counter Automata  </em></span>   </a>
			
			 | <a
		href="http://dx.doi.org/10.1007/978-3-642-28729-9\_27">
		DOI (10.1007/978-3-642-28729-9\_27)
		</a> 
		
		</div> 
	</div> 
	
        </li><li>
	
	<div class="row">
		
			<div class="col-xs-1 text-right">
				[7] 
			</div>

		
        
		<div
			class="col-xs-11"
		>
			
	
	<p class="publicationTitle"> <strong>
            Complexity of Subsumption in the <span style="font-family: serif"><span style="font-family: cursive; text-transform: uppercase; font-style: italic">EL</span></span> Family of Description Logics: Acyclic and Cyclic TBoxes </strong> </p>
	    <p class="publicationAuthors"> <em> Christoph Haase and Carsten Lutz  </em> </p>
	
	<p class="publicationDetails"> 
            In  
            <em>
            European Conference on Artificial Intelligence&#x201a; ECAI</em>.
        
            Vol. 178
                of Frontiers in Artificial Intelligence and Applications.
        
                Pages 25&#x2013;29.
            IOS Press.
        2008.
        </p>
	
        		<p class="publicationlinks"> <a
        
            		href="/publications/publication14463-abstract.html">
			Details <span class="sr-only" > about <em> Complexity of Subsumption in the <span style="font-family: serif"><span style="font-family: cursive; text-transform: uppercase; font-style: italic">EL</span></span> Family of Description Logics: Acyclic and Cyclic TBoxes  </em></span> </a> |
			<a href="/publications/publication14463.bib">
			BibTeX  <span class="sr-only" > data for <em> Complexity of Subsumption in the <span style="font-family: serif"><span style="font-family: cursive; text-transform: uppercase; font-style: italic">EL</span></span> Family of Description Logics: Acyclic and Cyclic TBoxes  </em></span>   </a>
			
			 | <a
		href="http://dx.doi.org/10.3233/978-1-58603-891-5-25">
		DOI (10.3233/978-1-58603-891-5-25)
		</a> 
		
		</div> 
	</div> 
	
        </li><li>
	
	<div class="row">
		
			<div class="col-xs-1 text-right">
				[8] 
			</div>

		
        
		<div
			class="col-xs-11"
		>
			
	
	<p class="publicationTitle"> <strong>
            Computing quantiles in Markov chains with multi&#x2212;dimensional costs </strong> </p>
	    <p class="publicationAuthors"> <em> Christoph Haase&#x201a; Stefan Kiefer and Markus Lohrey  </em> </p>
	
	<p class="publicationDetails"> 
            In  
            <em>
            Logic in Computer Science&#x201a; LICS</em>.
        IEEE.
        2017.
        </p>
	
        		<p class="publicationlinks"> <a
        
            		href="/publications/publication14452-abstract.html">
			Details <span class="sr-only" > about <em> Computing quantiles in Markov chains with multi&#x2212;dimensional costs  </em></span> </a> |
			<a href="/publications/publication14452.bib">
			BibTeX  <span class="sr-only" > data for <em> Computing quantiles in Markov chains with multi&#x2212;dimensional costs  </em></span>   </a>
			
			 | <a
		href="http://dx.doi.org/10.1109/LICS.2017.8005090">
		DOI (10.1109/LICS.2017.8005090)
		</a> 
		
		</div> 
	</div> 
	
        </li><li>
	
	<div class="row">
		
			<div class="col-xs-1 text-right">
				[9] 
			</div>

		
        
		<div
			class="col-xs-11"
		>
			
	
	<p class="publicationTitle"> <strong>
            Context&#x2212;free commutative grammars with integer counters and resets </strong> </p>
	    <p class="publicationAuthors"> <em> Dmitry Chistikov&#x201a; Christoph Haase and Simon Halfon  </em> </p>
	
	<p class="publicationDetails"> 
        In <em>Theor. Comput. Sci.</em>.
        
            Vol. 735.
        
                Pages 147&#x2013;161.
            2018.
        </p>
	
        		<p class="publicationlinks"> <a
        
            		href="/publications/publication14474-abstract.html">
			Details <span class="sr-only" > about <em> Context&#x2212;free commutative grammars with integer counters and resets  </em></span> </a> |
			<a href="/publications/publication14474.bib">
			BibTeX  <span class="sr-only" > data for <em> Context&#x2212;free commutative grammars with integer counters and resets  </em></span>   </a>
			
			 | <a
		href="http://dx.doi.org/10.1016/j.tcs.2016.06.017">
		DOI (10.1016/j.tcs.2016.06.017)
		</a> 
		
		</div> 
	</div> 
	
        </li><li>
	
	<div class="row">
		
			<div class="col-xs-1 text-right">
				[10] 
			</div>

		
        
		<div
			class="col-xs-11"
		>
			
	
	<p class="publicationTitle"> <strong>
            Counting Problems for Parikh Images </strong> </p>
	    <p class="publicationAuthors"> <em> Christoph Haase&#x201a; Stefan Kiefer and Markus Lohrey  </em> </p>
	
	<p class="publicationDetails"> 
            In  
            <em>
            Mathematical Foundations of Computer Science&#x201a; MFCS</em>.
        
            Vol. 83
                of LIPIcs.
        
                Pages 12:1&#x2013;12:13.
            Schloss Dagstuhl &#x2212; Leibniz&#x2212;Zentrum fuer Informatik.
        2017.
        </p>
	
        		<p class="publicationlinks"> <a
        
            		href="/publications/publication14465-abstract.html">
			Details <span class="sr-only" > about <em> Counting Problems for Parikh Images  </em></span> </a> |
			<a href="/publications/publication14465.bib">
			BibTeX  <span class="sr-only" > data for <em> Counting Problems for Parikh Images  </em></span>   </a>
			
			 | <a
		href="http://dx.doi.org/10.4230/LIPIcs.MFCS.2017.12">
		DOI (10.4230/LIPIcs.MFCS.2017.12)
		</a> 
		
		</div> 
	</div> 
	
        </li><li>
	
	<div class="row">
		
			<div class="col-xs-1 text-right">
				[11] 
			</div>

		
        
		<div
			class="col-xs-11"
		>
			
	
	<p class="publicationTitle"> <strong>
            Directed Reachability for Infinite&#x2212;State Systems </strong> </p>
	    <p class="publicationAuthors"> <em> Michael Blondin&#x201a; Christoph Haase and Philip Offtermatt  </em> </p>
	
	<p class="publicationDetails"> 
            In  
            <em>
            Tools and Algorithms for the Construction and Analysis of Systems&#x201a; TACAS</em>.
        Springer.
        2021.
        </p> <p
            class="publicationNote"> To appear</p>
	
        		<p class="publicationlinks"> <a
        
            		href="/publications/publication14482-abstract.html">
			Details <span class="sr-only" > about <em> Directed Reachability for Infinite&#x2212;State Systems  </em></span> </a> |
			<a href="/publications/publication14482.bib">
			BibTeX  <span class="sr-only" > data for <em> Directed Reachability for Infinite&#x2212;State Systems  </em></span>   </a>
			
			
		
		</div> 
	</div> 
	
        </li><li>
	
	<div class="row">
		
			<div class="col-xs-1 text-right">
				[12] 
			</div>

		
        
		<div
			class="col-xs-11"
		>
			
	
	<p class="publicationTitle"> <strong>
            Foundations for Decision Problems in Separation Logic with General Inductive Predicates </strong> </p>
	    <p class="publicationAuthors"> <em> Timos Antonopoulos&#x201a; Nikos Gorogiannis&#x201a; Christoph Haase&#x201a; Max I. Kanovich and Jo&#xeb;l Ouaknine  </em> </p>
	
	<p class="publicationDetails"> 
            In  
            <em>
            Foundations of Software Science and Computation Structures&#x201a; FOSSACS</em>.
        
            Vol. 8412
                of Lect. Notes Comp. Sci..
        
                Pages 411&#x2013;425.
            Springer.
        2014.
        </p>
	
        		<p class="publicationlinks"> <a
        
            		href="/publications/publication14458-abstract.html">
			Details <span class="sr-only" > about <em> Foundations for Decision Problems in Separation Logic with General Inductive Predicates  </em></span> </a> |
			<a href="/publications/publication14458.bib">
			BibTeX  <span class="sr-only" > data for <em> Foundations for Decision Problems in Separation Logic with General Inductive Predicates  </em></span>   </a>
			
			 | <a
		href="http://dx.doi.org/10.1007/978-3-642-54830-7\_27">
		DOI (10.1007/978-3-642-54830-7\_27)
		</a> 
		
		</div> 
	</div> 
	
        </li><li>
	
	<div class="row">
		
			<div class="col-xs-1 text-right">
				[13] 
			</div>

		
        
		<div
			class="col-xs-11"
		>
			
	
	<p class="publicationTitle"> <strong>
            Ideal Downward Refinement in the <span style="font-family: serif"><span style="font-family: cursive; text-transform: uppercase; font-style: italic">EL</span></span> Description Logic </strong> </p>
	    <p class="publicationAuthors"> <em> Jens Lehmann and Christoph Haase  </em> </p>
	
	<p class="publicationDetails"> 
            In  
            <em>
            Inductive Logic Programming&#x201a; ILP</em>.
        
            Vol. 5989
                of Lect. Notes Comp. Sci..
        
                Pages 73&#x2013;87.
            Springer.
        2009.
        </p>
	
        		<p class="publicationlinks"> <a
        
            		href="/publications/publication14473-abstract.html">
			Details <span class="sr-only" > about <em> Ideal Downward Refinement in the <span style="font-family: serif"><span style="font-family: cursive; text-transform: uppercase; font-style: italic">EL</span></span> Description Logic  </em></span> </a> |
			<a href="/publications/publication14473.bib">
			BibTeX  <span class="sr-only" > data for <em> Ideal Downward Refinement in the <span style="font-family: serif"><span style="font-family: cursive; text-transform: uppercase; font-style: italic">EL</span></span> Description Logic  </em></span>   </a>
			
			 | <a
		href="http://dx.doi.org/10.1007/978-3-642-13840-9\_8">
		DOI (10.1007/978-3-642-13840-9\_8)
		</a> 
					| <a href="https://doi.org/10.1007/978-3-642-13840-9\_8"> Link <span class="sr-only" > to <em> Ideal Downward Refinement in the <span style="font-family: serif"><span style="font-family: cursive; text-transform: uppercase; font-style: italic">EL</span></span> Description Logic  </em></span> </a>
  				
		
		</div> 
	</div> 
	
        </li><li>
	
	<div class="row">
		
			<div class="col-xs-1 text-right">
				[14] 
			</div>

		
        
		<div
			class="col-xs-11"
		>
			
	
	<p class="publicationTitle"> <strong>
            Integer Vector Addition Systems with States </strong> </p>
	    <p class="publicationAuthors"> <em> Christoph Haase and Simon Halfon  </em> </p>
	
	<p class="publicationDetails"> 
            In  
            <em>
            Reachability Problems&#x201a; RP</em>.
        
            Vol. 8762
                of Lect. Notes Comp. Sci..
        
                Pages 112&#x2013;124.
            Springer.
        2014.
        </p>
	
        		<p class="publicationlinks"> <a
        
            		href="/publications/publication14467-abstract.html">
			Details <span class="sr-only" > about <em> Integer Vector Addition Systems with States  </em></span> </a> |
			<a href="/publications/publication14467.bib">
			BibTeX  <span class="sr-only" > data for <em> Integer Vector Addition Systems with States  </em></span>   </a>
			
			 | <a
		href="http://dx.doi.org/10.1007/978-3-319-11439-2\_9">
		DOI (10.1007/978-3-319-11439-2\_9)
		</a> 
		
		</div> 
	</div> 
	
        </li><li>
	
	<div class="row">
		
			<div class="col-xs-1 text-right">
				[15] 
			</div>

		
        
		<div
			class="col-xs-11"
		>
			
	
	<p class="publicationTitle"> <strong>
            Logics for continuous reachability in Petri nets and vector addition systems with states </strong> </p>
	    <p class="publicationAuthors"> <em> Michael Blondin and Christoph Haase  </em> </p>
	
	<p class="publicationDetails"> 
            In  
            <em>
            Logic in Computer Science&#x201a; LICS</em>.
        IEEE.
        2017.
        </p>
	
        		<p class="publicationlinks"> <a
        
            		href="/publications/publication14462-abstract.html">
			Details <span class="sr-only" > about <em> Logics for continuous reachability in Petri nets and vector addition systems with states  </em></span> </a> |
			<a href="/publications/publication14462.bib">
			BibTeX  <span class="sr-only" > data for <em> Logics for continuous reachability in Petri nets and vector addition systems with states  </em></span>   </a>
			
			 | <a
		href="http://dx.doi.org/10.1109/LICS.2017.8005068">
		DOI (10.1109/LICS.2017.8005068)
		</a> 
		
		</div> 
	</div> 
	
        </li><li>
	
	<div class="row">
		
			<div class="col-xs-1 text-right">
				[16] 
			</div>

		
        
		<div
			class="col-xs-11"
		>
			
	
	<p class="publicationTitle"> <strong>
            Model Checking Succinct and Parametric One&#x2212;Counter Automata </strong> </p>
	    <p class="publicationAuthors"> <em> Stefan G&#xf6;ller&#x201a; Christoph Haase&#x201a; Jo&#xeb;l Ouaknine and James Worrell  </em> </p>
	
	<p class="publicationDetails"> 
            In  
            <em>
            Automata&#x201a; Languages and Programming&#x201a; ICALP</em>.
        
            Vol. 6199
                of Lect. Notes Comp. Sci..
        
                Pages 575&#x2013;586.
            Springer.
        2010.
        </p>
	
        		<p class="publicationlinks"> <a
        
            		href="/publications/publication14454-abstract.html">
			Details <span class="sr-only" > about <em> Model Checking Succinct and Parametric One&#x2212;Counter Automata  </em></span> </a> |
			<a href="/publications/publication14454.bib">
			BibTeX  <span class="sr-only" > data for <em> Model Checking Succinct and Parametric One&#x2212;Counter Automata  </em></span>   </a>
			
			 | <a
		href="http://dx.doi.org/10.1007/978-3-642-14162-1\_48">
		DOI (10.1007/978-3-642-14162-1\_48)
		</a> 
		
		</div> 
	</div> 
	
        </li><li>
	
	<div class="row">
		
			<div class="col-xs-1 text-right">
				[17] 
			</div>

		
        
		<div
			class="col-xs-11"
		>
			
	
	<p class="publicationTitle"> <strong>
            On Process&#x2212;Algebraic Extensions of Metric Temporal Logic </strong> </p>
	    <p class="publicationAuthors"> <em> Christoph Haase&#x201a; Jo&#xeb;l Ouaknine and James Worrell  </em> </p>
	
	<p class="publicationDetails"> 
            In  
            <em>
            Reflections on the Work of C. A. R. Hoare.</em>.
        
                Pages 283&#x2013;300.
            Springer.
        2010.
        </p>
	
        		<p class="publicationlinks"> <a
        
            		href="/publications/publication14477-abstract.html">
			Details <span class="sr-only" > about <em> On Process&#x2212;Algebraic Extensions of Metric Temporal Logic  </em></span> </a> |
			<a href="/publications/publication14477.bib">
			BibTeX  <span class="sr-only" > data for <em> On Process&#x2212;Algebraic Extensions of Metric Temporal Logic  </em></span>   </a>
			
			 | <a
		href="http://dx.doi.org/10.1007/978-1-84882-912-1\_13">
		DOI (10.1007/978-1-84882-912-1\_13)
		</a> 
		
		</div> 
	</div> 
	
        </li><li>
	
	<div class="row">
		
			<div class="col-xs-1 text-right">
				[18] 
			</div>

		
        
		<div
			class="col-xs-11"
		>
			
	
	<p class="publicationTitle"> <strong>
            On the Complexity of Quantified Integer Programming </strong> </p>
	    <p class="publicationAuthors"> <em> Dmitry Chistikov and Christoph Haase  </em> </p>
	
	<p class="publicationDetails"> 
            In  
            <em>
            Automata&#x201a; Languages&#x201a; and Programming&#x201a; ICALP</em>.
        
            Vol. 80
                of LIPIcs.
        
                Pages 94:1&#x2013;94:13.
            Schloss Dagstuhl &#x2212; Leibniz&#x2212;Zentrum fuer Informatik.
        2017.
        </p>
	
        		<p class="publicationlinks"> <a
        
            		href="/publications/publication14448-abstract.html">
			Details <span class="sr-only" > about <em> On the Complexity of Quantified Integer Programming  </em></span> </a> |
			<a href="/publications/publication14448.bib">
			BibTeX  <span class="sr-only" > data for <em> On the Complexity of Quantified Integer Programming  </em></span>   </a>
			
			 | <a
		href="http://dx.doi.org/10.4230/LIPIcs.ICALP.2017.94">
		DOI (10.4230/LIPIcs.ICALP.2017.94)
		</a> 
		
		</div> 
	</div> 
	
        </li><li>
	
	<div class="row">
		
			<div class="col-xs-1 text-right">
				[19] 
			</div>

		
        
		<div
			class="col-xs-11"
		>
			
	
	<p class="publicationTitle"> <strong>
            On the Existential Theories of B&#xfc;chi Arithmetic and Linear <span style="font-family: serif">p</span>&#x2212;adic Fields </strong> </p>
	    <p class="publicationAuthors"> <em> Florent Gu&#xe9;pin&#x201a; Christoph Haase and James Worrell  </em> </p>
	
	<p class="publicationDetails"> 
            In  
            <em>
            Logic in Computer Science&#x201a; LICS</em>.
        IEEE.
        2019.
        </p>
	
        		<p class="publicationlinks"> <a
        
            		href="/publications/publication14479-abstract.html">
			Details <span class="sr-only" > about <em> On the Existential Theories of B&#xfc;chi Arithmetic and Linear <span style="font-family: serif">p</span>&#x2212;adic Fields  </em></span> </a> |
			<a href="/publications/publication14479.bib">
			BibTeX  <span class="sr-only" > data for <em> On the Existential Theories of B&#xfc;chi Arithmetic and Linear <span style="font-family: serif">p</span>&#x2212;adic Fields  </em></span>   </a>
			
			 | <a
		href="http://dx.doi.org/10.1109/LICS.2019.8785681">
		DOI (10.1109/LICS.2019.8785681)
		</a> 
		
		</div> 
	</div> 
	
        </li><li>
	
	<div class="row">
		
			<div class="col-xs-1 text-right">
				[20] 
			</div>

		
        
		<div
			class="col-xs-11"
		>
			
	
	<p class="publicationTitle"> <strong>
            On the Expressiveness of B&#xfc;chi Arithmetic </strong> </p>
	    <p class="publicationAuthors"> <em> Christoph Haase and Jakub R&#xf3;&#x017c;ycki  </em> </p>
	
	<p class="publicationDetails"> 
            In  
            <em>
            Foundations of Software Science and Computation Structures&#x201a; FOSSACS</em>.
        Springer.
        2021.
        </p> <p
            class="publicationNote"> To appear</p>
	
        		<p class="publicationlinks"> <a
        
            		href="/publications/publication14481-abstract.html">
			Details <span class="sr-only" > about <em> On the Expressiveness of B&#xfc;chi Arithmetic  </em></span> </a> |
			<a href="/publications/publication14481.bib">
			BibTeX  <span class="sr-only" > data for <em> On the Expressiveness of B&#xfc;chi Arithmetic  </em></span>   </a>
			
			
		
		</div> 
	</div> 
	
        </li><li>
	
	<div class="row">
		
			<div class="col-xs-1 text-right">
				[21] 
			</div>

		
        
		<div
			class="col-xs-11"
		>
			
	
	<p class="publicationTitle"> <strong>
            On the Relationship between Reachability Problems in Timed and Counter Automata </strong> </p>
	    <p class="publicationAuthors"> <em> Christoph Haase&#x201a; Jo&#xeb;l Ouaknine and James Worrell  </em> </p>
	
	<p class="publicationDetails"> 
            In  
            <em>
            Reachability Problems&#x201a; RP</em>.
        
            Vol. 7550
                of Lect. Notes Comp. Sci..
        
                Pages 54&#x2013;65.
            Springer.
        2012.
        </p>
	
        		<p class="publicationlinks"> <a
        
            		href="/publications/publication14471-abstract.html">
			Details <span class="sr-only" > about <em> On the Relationship between Reachability Problems in Timed and Counter Automata  </em></span> </a> |
			<a href="/publications/publication14471.bib">
			BibTeX  <span class="sr-only" > data for <em> On the Relationship between Reachability Problems in Timed and Counter Automata  </em></span>   </a>
			
			 | <a
		href="http://dx.doi.org/10.1007/978-3-642-33512-9\_6">
		DOI (10.1007/978-3-642-33512-9\_6)
		</a> 
		
		</div> 
	</div> 
	
        </li><li>
	
	<div class="row">
		
			<div class="col-xs-1 text-right">
				[22] 
			</div>

		
        
		<div
			class="col-xs-11"
		>
			
	
	<p class="publicationTitle"> <strong>
            On the Size of Finite Rational Matrix Semigroups </strong> </p>
	    <p class="publicationAuthors"> <em> Georgina Bumpus&#x201a; Christoph Haase&#x201a; Stefan Kiefer&#x201a; Paul&#x2212;Ioan Stoienescu and Jonathan Tanner  </em> </p>
	
	<p class="publicationDetails"> 
            In  
            <em>
            Automata&#x201a; Languages&#x201a; and Programming&#x201a; ICALP</em>.
        
            Vol. 168
                of LIPIcs.
        
                Pages 115:1&#x2013;115:13.
            Schloss Dagstuhl &#x2212; Leibniz&#x2212;Zentrum fuer Informatik.
        2020.
        </p>
	
        		<p class="publicationlinks"> <a
        
            		href="/publications/publication14445-abstract.html">
			Details <span class="sr-only" > about <em> On the Size of Finite Rational Matrix Semigroups  </em></span> </a> |
			<a href="/publications/publication14445.bib">
			BibTeX  <span class="sr-only" > data for <em> On the Size of Finite Rational Matrix Semigroups  </em></span>   </a>
			
			 | <a
		href="http://dx.doi.org/10.4230/LIPIcs.ICALP.2020.115">
		DOI (10.4230/LIPIcs.ICALP.2020.115)
		</a> 
		
		</div> 
	</div> 
	
        </li><li>
	
	<div class="row">
		
			<div class="col-xs-1 text-right">
				[23] 
			</div>

		
        
		<div
			class="col-xs-11"
		>
			
	
	<p class="publicationTitle"> <strong>
            On the power of ordering in linear arithmetic theories </strong> </p>
	    <p class="publicationAuthors"> <em> Dmitry Chistikov and Christoph Haase  </em> </p>
	
	<p class="publicationDetails"> 
            In  
            <em>
            Automata&#x201a; Languages&#x201a; and Programming&#x201a; ICALP</em>.
        
            Vol. 168
                of LIPIcs.
        
                Pages 119:1&#x2013;119:15.
            Schloss Dagstuhl &#x2212; Leibniz&#x2212;Zentrum fuer Informatik.
        2020.
        </p>
	
        		<p class="publicationlinks"> <a
        
            		href="/publications/publication14446-abstract.html">
			Details <span class="sr-only" > about <em> On the power of ordering in linear arithmetic theories  </em></span> </a> |
			<a href="/publications/publication14446.bib">
			BibTeX  <span class="sr-only" > data for <em> On the power of ordering in linear arithmetic theories  </em></span>   </a>
			
			 | <a
		href="http://dx.doi.org/10.4230/LIPIcs.ICALP.2020.119">
		DOI (10.4230/LIPIcs.ICALP.2020.119)
		</a> 
		
		</div> 
	</div> 
	
        </li><li>
	
	<div class="row">
		
			<div class="col-xs-1 text-right">
				[24] 
			</div>

		
        
		<div
			class="col-xs-11"
		>
			
	
	<p class="publicationTitle"> <strong>
            Presburger arithmetic with stars&#x201a; rational subsets of graph groups&#x201a; and nested zero tests </strong> </p>
	    <p class="publicationAuthors"> <em> Christoph Haase and Georg Zetzsche  </em> </p>
	
	<p class="publicationDetails"> 
            In  
            <em>
            Logic in Computer Science&#x201a; LICS</em>.
        IEEE.
        2019.
        </p>
	
        		<p class="publicationlinks"> <a
        
            		href="/publications/publication14478-abstract.html">
			Details <span class="sr-only" > about <em> Presburger arithmetic with stars&#x201a; rational subsets of graph groups&#x201a; and nested zero tests  </em></span> </a> |
			<a href="/publications/publication14478.bib">
			BibTeX  <span class="sr-only" > data for <em> Presburger arithmetic with stars&#x201a; rational subsets of graph groups&#x201a; and nested zero tests  </em></span>   </a>
			
			 | <a
		href="http://dx.doi.org/10.1109/LICS.2019.8785850">
		DOI (10.1109/LICS.2019.8785850)
		</a> 
		
		</div> 
	</div> 
	
        </li><li>
	
	<div class="row">
		
			<div class="col-xs-1 text-right">
				[25] 
			</div>

		
        
		<div
			class="col-xs-11"
		>
			
	
	<p class="publicationTitle"> <strong>
            Reachability in Register Machines with Polynomial Updates </strong> </p>
	    <p class="publicationAuthors"> <em> Alain Finkel&#x201a; Stefan G&#xf6;ller and Christoph Haase  </em> </p>
	
	<p class="publicationDetails"> 
            In  
            <em>
            Mathematical Foundations of Computer Science&#x201a; MFCS</em>.
        
            Vol. 8087
                of Lect. Notes Comp. Sci..
        
                Pages 409&#x2013;420.
            Springer.
        2013.
        </p>
	
        		<p class="publicationlinks"> <a
        
            		href="/publications/publication14469-abstract.html">
			Details <span class="sr-only" > about <em> Reachability in Register Machines with Polynomial Updates  </em></span> </a> |
			<a href="/publications/publication14469.bib">
			BibTeX  <span class="sr-only" > data for <em> Reachability in Register Machines with Polynomial Updates  </em></span>   </a>
			
			 | <a
		href="http://dx.doi.org/10.1007/978-3-642-40313-2\_37">
		DOI (10.1007/978-3-642-40313-2\_37)
		</a> 
		
		</div> 
	</div> 
	
        </li><li>
	
	<div class="row">
		
			<div class="col-xs-1 text-right">
				[26] 
			</div>

		
        
		<div
			class="col-xs-11"
		>
			
	
	<p class="publicationTitle"> <strong>
            Reachability in Succinct and Parametric One&#x2212;Counter Automata </strong> </p>
	    <p class="publicationAuthors"> <em> Christoph Haase&#x201a; Stephan Kreutzer&#x201a; Jo&#xeb;l Ouaknine and James Worrell  </em> </p>
	
	<p class="publicationDetails"> 
            In  
            <em>
            Concurrency Theory&#x201a; CONCUR</em>.
        
            Vol. 5710
                of Lect. Notes Comp. Sci..
        
                Pages 369&#x2013;383.
            Springer.
        2009.
        </p>
	
        		<p class="publicationlinks"> <a
        
            		href="/publications/publication14450-abstract.html">
			Details <span class="sr-only" > about <em> Reachability in Succinct and Parametric One&#x2212;Counter Automata  </em></span> </a> |
			<a href="/publications/publication14450.bib">
			BibTeX  <span class="sr-only" > data for <em> Reachability in Succinct and Parametric One&#x2212;Counter Automata  </em></span>   </a>
			
			 | <a
		href="http://dx.doi.org/10.1007/978-3-642-04081-8\_25">
		DOI (10.1007/978-3-642-04081-8\_25)
		</a> 
		
		</div> 
	</div> 
	
        </li><li>
	
	<div class="row">
		
			<div class="col-xs-1 text-right">
				[27] 
			</div>

		
        
		<div
			class="col-xs-11"
		>
			
	
	<p class="publicationTitle"> <strong>
            Reachability in Two&#x2212;Dimensional Vector Addition Systems with States Is PSPACE&#x2212;Complete </strong> </p>
	    <p class="publicationAuthors"> <em> Michael Blondin&#x201a; Alain Finkel&#x201a; Stefan G&#xf6;ller&#x201a; Christoph Haase and Pierre McKenzie  </em> </p>
	
	<p class="publicationDetails"> 
            In  
            <em>
            Logic in Computer Science&#x201a; LICS</em>.
        
                Pages 32&#x2013;43.
            IEEE.
        2015.
        </p>
	
        		<p class="publicationlinks"> <a
        
            		href="/publications/publication14456-abstract.html">
			Details <span class="sr-only" > about <em> Reachability in Two&#x2212;Dimensional Vector Addition Systems with States Is PSPACE&#x2212;Complete  </em></span> </a> |
			<a href="/publications/publication14456.bib">
			BibTeX  <span class="sr-only" > data for <em> Reachability in Two&#x2212;Dimensional Vector Addition Systems with States Is PSPACE&#x2212;Complete  </em></span>   </a>
			
			 | <a
		href="http://dx.doi.org/10.1109/LICS.2015.14">
		DOI (10.1109/LICS.2015.14)
		</a> 
		
		</div> 
	</div> 
	
        </li><li>
	
	<div class="row">
		
			<div class="col-xs-1 text-right">
				[28] 
			</div>

		
        
		<div
			class="col-xs-11"
		>
			
	
	<p class="publicationTitle"> <strong>
            Relating Reachability Problems in Timed and Counter Automata </strong> </p>
	    <p class="publicationAuthors"> <em> Christoph Haase&#x201a; Jo&#xeb;l Ouaknine and James Worrell  </em> </p>
	
	<p class="publicationDetails"> 
        In <em>Fundam. Inform.</em>.
        
            Vol. 143.
        
            No. 3&#x2212;4.
        
                Pages 317&#x2013;338.
            2016.
        </p>
	
        		<p class="publicationlinks"> <a
        
            		href="/publications/publication14475-abstract.html">
			Details <span class="sr-only" > about <em> Relating Reachability Problems in Timed and Counter Automata  </em></span> </a> |
			<a href="/publications/publication14475.bib">
			BibTeX  <span class="sr-only" > data for <em> Relating Reachability Problems in Timed and Counter Automata  </em></span>   </a>
			
			 | <a
		href="http://dx.doi.org/10.3233/FI-2016-1316">
		DOI (10.3233/FI-2016-1316)
		</a> 
		
		</div> 
	</div> 
	
        </li><li>
	
	<div class="row">
		
			<div class="col-xs-1 text-right">
				[29] 
			</div>

		
        
		<div
			class="col-xs-11"
		>
			
	
	<p class="publicationTitle"> <strong>
            SeLoger: A Tool for Graph&#x2212;Based Reasoning in Separation Logic </strong> </p>
	    <p class="publicationAuthors"> <em> Christoph Haase&#x201a; Samin Ishtiaq&#x201a; Jo&#xeb;l Ouaknine and Matthew J. Parkinson  </em> </p>
	
	<p class="publicationDetails"> 
            In  
            <em>
            Computer Aided Verification&#x201a; CAV</em>.
        
            Vol. 8044
                of Lect. Notes Comp. Sci..
        
                Pages 790&#x2013;795.
            Springer.
        2013.
        </p>
	
        		<p class="publicationlinks"> <a
        
            		href="/publications/publication14457-abstract.html">
			Details <span class="sr-only" > about <em> SeLoger: A Tool for Graph&#x2212;Based Reasoning in Separation Logic  </em></span> </a> |
			<a href="/publications/publication14457.bib">
			BibTeX  <span class="sr-only" > data for <em> SeLoger: A Tool for Graph&#x2212;Based Reasoning in Separation Logic  </em></span>   </a>
			
			 | <a
		href="http://dx.doi.org/10.1007/978-3-642-39799-8\_55">
		DOI (10.1007/978-3-642-39799-8\_55)
		</a> 
		
		</div> 
	</div> 
	
        </li><li>
	
	<div class="row">
		
			<div class="col-xs-1 text-right">
				[30] 
			</div>

		
        
		<div
			class="col-xs-11"
		>
			
	
	<p class="publicationTitle"> <strong>
            Subclasses of Presburger arithmetic and the weak EXP hierarchy </strong> </p>
	    <p class="publicationAuthors"> <em> Christoph Haase  </em> </p>
	
	<p class="publicationDetails"> 
            In  
            <em>
            Computer Science Logic and Logic in Computer Science&#x201a; CSL&#x2212;LICS</em>.
        
                Pages 47:1&#x2013;47:10.
            ACM.
        2014.
        </p>
	
        		<p class="publicationlinks"> <a
        
            		href="/publications/publication14447-abstract.html">
			Details <span class="sr-only" > about <em> Subclasses of Presburger arithmetic and the weak EXP hierarchy  </em></span> </a> |
			<a href="/publications/publication14447.bib">
			BibTeX  <span class="sr-only" > data for <em> Subclasses of Presburger arithmetic and the weak EXP hierarchy  </em></span>   </a>
			
			 | <a
		href="http://dx.doi.org/10.1145/2603088.2603092">
		DOI (10.1145/2603088.2603092)
		</a> 
		
		</div> 
	</div> 
	
        </li><li>
	
	<div class="row">
		
			<div class="col-xs-1 text-right">
				[31] 
			</div>

		
        
		<div
			class="col-xs-11"
		>
			
	
	<p class="publicationTitle"> <strong>
            The Logical View on Continuous Petri Nets </strong> </p>
	    <p class="publicationAuthors"> <em> Michael Blondin&#x201a; Alain Finkel&#x201a; Christoph Haase and Serge Haddad  </em> </p>
	
	<p class="publicationDetails"> 
        In <em>ACM Trans. Comput. Log.</em>.
        
            Vol. 18.
        
            No. 3.
        
                Pages 24:1&#x2013;24:28.
            2017.
        </p>
	
        		<p class="publicationlinks"> <a
        
            		href="/publications/publication14459-abstract.html">
			Details <span class="sr-only" > about <em> The Logical View on Continuous Petri Nets  </em></span> </a> |
			<a href="/publications/publication14459.bib">
			BibTeX  <span class="sr-only" > data for <em> The Logical View on Continuous Petri Nets  </em></span>   </a>
			
			 | <a
		href="http://dx.doi.org/10.1145/3105908">
		DOI (10.1145/3105908)
		</a> 
		
		</div> 
	</div> 
	
        </li><li>
	
	<div class="row">
		
			<div class="col-xs-1 text-right">
				[32] 
			</div>

		
        
		<div
			class="col-xs-11"
		>
			
	
	<p class="publicationTitle"> <strong>
            The Odds of Staying on Budget </strong> </p>
	    <p class="publicationAuthors"> <em> Christoph Haase and Stefan Kiefer  </em> </p>
	
	<p class="publicationDetails"> 
            In  
            <em>
            Automata&#x201a; Languages&#x201a; and Programming&#x201a; ICALP</em>.
        
            Vol. 9135
                of Lect. Notes Comp. Sci..
        
                Pages 234&#x2013;246.
            Springer.
        2015.
        </p>
	
        		<p class="publicationlinks"> <a
        
            		href="/publications/publication14451-abstract.html">
			Details <span class="sr-only" > about <em> The Odds of Staying on Budget  </em></span> </a> |
			<a href="/publications/publication14451.bib">
			BibTeX  <span class="sr-only" > data for <em> The Odds of Staying on Budget  </em></span>   </a>
			
			 | <a
		href="http://dx.doi.org/10.1007/978-3-662-47666-6\_19">
		DOI (10.1007/978-3-662-47666-6\_19)
		</a> 
		
		</div> 
	</div> 
	
        </li><li>
	
	<div class="row">
		
			<div class="col-xs-1 text-right">
				[33] 
			</div>

		
        
		<div
			class="col-xs-11"
		>
			
	
	<p class="publicationTitle"> <strong>
            The Power of Priority Channel Systems </strong> </p>
	    <p class="publicationAuthors"> <em> Christoph Haase&#x201a; Sylvain Schmitz and Philippe Schnoebelen  </em> </p>
	
	<p class="publicationDetails"> 
        In <em>Log. Methods Comput. Sci.</em>.
        
            Vol. 10.
        
            No. 4.
        2014.
        </p>
	
        		<p class="publicationlinks"> <a
        
            		href="/publications/publication14476-abstract.html">
			Details <span class="sr-only" > about <em> The Power of Priority Channel Systems  </em></span> </a> |
			<a href="/publications/publication14476.bib">
			BibTeX  <span class="sr-only" > data for <em> The Power of Priority Channel Systems  </em></span>   </a>
			
			 | <a
		href="http://dx.doi.org/10.2168/LMCS-10(4:4)2014">
		DOI (10.2168/LMCS-10(4:4)2014)
		</a> 
		
		</div> 
	</div> 
	
        </li><li>
	
	<div class="row">
		
			<div class="col-xs-1 text-right">
				[34] 
			</div>

		
        
		<div
			class="col-xs-11"
		>
			
	
	<p class="publicationTitle"> <strong>
            The Power of Priority Channel Systems </strong> </p>
	    <p class="publicationAuthors"> <em> Christoph Haase&#x201a; Sylvain Schmitz and Philippe Schnoebelen  </em> </p>
	
	<p class="publicationDetails"> 
            In  
            <em>
            Concurrency Theory&#x201a; CONCUR</em>.
        
            Vol. 8052
                of Lect. Notes Comp. Sci..
        
                Pages 319&#x2013;333.
            Springer.
        2013.
        </p>
	
        		<p class="publicationlinks"> <a
        
            		href="/publications/publication14468-abstract.html">
			Details <span class="sr-only" > about <em> The Power of Priority Channel Systems  </em></span> </a> |
			<a href="/publications/publication14468.bib">
			BibTeX  <span class="sr-only" > data for <em> The Power of Priority Channel Systems  </em></span>   </a>
			
			 | <a
		href="http://dx.doi.org/10.1007/978-3-642-40184-8\_23">
		DOI (10.1007/978-3-642-40184-8\_23)
		</a> 
		
		</div> 
	</div> 
	
        </li><li>
	
	<div class="row">
		
			<div class="col-xs-1 text-right">
				[35] 
			</div>

		
        
		<div
			class="col-xs-11"
		>
			
	
	<p class="publicationTitle"> <strong>
            The Taming of the Semi&#x2212;Linear Set </strong> </p>
	    <p class="publicationAuthors"> <em> Dmitry Chistikov and Christoph Haase  </em> </p>
	
	<p class="publicationDetails"> 
            In  
            <em>
            Automata&#x201a; Languages&#x201a; and Programming&#x201a; ICALP</em>.
        
            Vol. 55
                of LIPIcs.
        
                Pages 128:1&#x2013;128:13.
            Schloss Dagstuhl &#x2212; Leibniz&#x2212;Zentrum fuer Informatik.
        2016.
        </p>
	
        		<p class="publicationlinks"> <a
        
            		href="/publications/publication14449-abstract.html">
			Details <span class="sr-only" > about <em> The Taming of the Semi&#x2212;Linear Set  </em></span> </a> |
			<a href="/publications/publication14449.bib">
			BibTeX  <span class="sr-only" > data for <em> The Taming of the Semi&#x2212;Linear Set  </em></span>   </a>
			
			 | <a
		href="http://dx.doi.org/10.4230/LIPIcs.ICALP.2016.128">
		DOI (10.4230/LIPIcs.ICALP.2016.128)
		</a> 
		
		</div> 
	</div> 
	
        </li><li>
	
	<div class="row">
		
			<div class="col-xs-1 text-right">
				[36] 
			</div>

		
        
		<div
			class="col-xs-11"
		>
			
	
	<p class="publicationTitle"> <strong>
            The complexity of the <span style="font-family: serif">K</span>th largest subset problem and related problems </strong> </p>
	    <p class="publicationAuthors"> <em> Christoph Haase and Stefan Kiefer  </em> </p>
	
	<p class="publicationDetails"> 
        In <em>Inf. Process. Lett.</em>.
        
            Vol. 116.
        
            No. 2.
        
                Pages 111&#x2013;115.
            2016.
        </p>
	
        		<p class="publicationlinks"> <a
        
            		href="/publications/publication14460-abstract.html">
			Details <span class="sr-only" > about <em> The complexity of the <span style="font-family: serif">K</span>th largest subset problem and related problems  </em></span> </a> |
			<a href="/publications/publication14460.bib">
			BibTeX  <span class="sr-only" > data for <em> The complexity of the <span style="font-family: serif">K</span>th largest subset problem and related problems  </em></span>   </a>
			
			 | <a
		href="http://dx.doi.org/10.1016/j.ipl.2015.09.015">
		DOI (10.1016/j.ipl.2015.09.015)
		</a> 
		
		</div> 
	</div> 
	
        </li><li>
	
	<div class="row">
		
			<div class="col-xs-1 text-right">
				[37] 
			</div>

		
        
		<div
			class="col-xs-11"
		>
			
	
	<p class="publicationTitle"> <strong>
            Tightening the Complexity of Equivalence Problems for Commutative Grammars </strong> </p>
	    <p class="publicationAuthors"> <em> Christoph Haase and Piotr Hofman  </em> </p>
	
	<p class="publicationDetails"> 
            In  
            <em>
            Symposium on Theoretical Aspects of Computer Science&#x201a; STACS</em>.
        
            Vol. 47
                of LIPIcs.
        
                Pages 41:1&#x2013;41:14.
            Schloss Dagstuhl &#x2212; Leibniz&#x2212;Zentrum fuer Informatik.
        2016.
        </p>
	
        		<p class="publicationlinks"> <a
        
            		href="/publications/publication14453-abstract.html">
			Details <span class="sr-only" > about <em> Tightening the Complexity of Equivalence Problems for Commutative Grammars  </em></span> </a> |
			<a href="/publications/publication14453.bib">
			BibTeX  <span class="sr-only" > data for <em> Tightening the Complexity of Equivalence Problems for Commutative Grammars  </em></span>   </a>
			
			 | <a
		href="http://dx.doi.org/10.4230/LIPIcs.STACS.2016.41">
		DOI (10.4230/LIPIcs.STACS.2016.41)
		</a> 
		
		</div> 
	</div> 
	
        </li><li>
	
	<div class="row">
		
			<div class="col-xs-1 text-right">
				[38] 
			</div>

		
        
		<div
			class="col-xs-11"
		>
			
	
	<p class="publicationTitle"> <strong>
            Tractable Reasoning in a Fragment of Separation Logic </strong> </p>
	    <p class="publicationAuthors"> <em> Byron Cook&#x201a; Christoph Haase&#x201a; Jo&#xeb;l Ouaknine&#x201a; Matthew J. Parkinson and James Worrell  </em> </p>
	
	<p class="publicationDetails"> 
            In  
            <em>
            Concurrency Theory&#x201a; CONCUR</em>.
        
            Vol. 6901
                of Lect. Notes Comp. Sci..
        
                Pages 235&#x2013;249.
            Springer.
        2011.
        </p>
	
        		<p class="publicationlinks"> <a
        
            		href="/publications/publication14472-abstract.html">
			Details <span class="sr-only" > about <em> Tractable Reasoning in a Fragment of Separation Logic  </em></span> </a> |
			<a href="/publications/publication14472.bib">
			BibTeX  <span class="sr-only" > data for <em> Tractable Reasoning in a Fragment of Separation Logic  </em></span>   </a>
			
			 | <a
		href="http://dx.doi.org/10.1007/978-3-642-23217-6\_16">
		DOI (10.1007/978-3-642-23217-6\_16)
		</a> 
		
		</div> 
	</div> 
	
        </li></ul></div><div class="col-xs-12 col-md-3 col-md-pull-9 side-menu-col"><h2 class="side-menu-title text-uppercase"><a href="#">About Us</a></h2><ul class="side-menu"><li class="active mobile-menu-source"><a href="/people/">People</a><ul><li class="active"><a href="/people/faculty.html">Faculty</a></li><li><a href="/people/research.html">Research</a></li><li><a href="/people/students.html">Students</a></li><li><a href="/people/support.html">Professional Services</a></li><li><a href="/people/visitingprofessors.html">Visiting Professors</a></li><li><a href="/people/emeritusfaculty.html">Emeritus Faculty</a></li></ul></li><li><a href="/aboutus/vacancies/">Vacancies</a></li><li><a href="/aboutus/women-cs-oxford/index.html">Women in the department</a></li><li><a href="/aboutus/equality-diversity-inclusion/index.html">Equality, diversity and inclusion</a></li><li><a href="https://www.alumniweb.ox.ac.uk/cs/make-a-donation">Support Us</a></li><li><a href="/aboutus/cshistory.html">Our History</a></li><li><a href="/aboutus/contact.html">Contact Us</a></li></ul></div></div></div>[an error occurred while processing this directive]