[an error occurred while processing this directive]<meta name="keywords" content="Department of Computer Science, publications, by type, Pascal Kesseli"></meta><meta name="description" content="Publications, by type, Department of Computer Science, Oxford, Pascal Kesseli"></meta><title>Department of Computer Science, University of Oxford: Pascal Kesseli : 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/students.html">Students</a></li><li><a href="/people/Pascal.Kesseli"><span itemprop="name">Pascal Kesseli</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>Pascal Kesseli : Publications
</h1></div><div role="toolbar" class="btn-toolbar"><div class="btn-group"><a href="/people/publications/date/Pascal.Kesseli.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/Pascal.Kesseli.html" aria-hidden="true" type="button" class="btn btn-default"><span class="glyphicon glyphicon-sort-by-attributes"></span> By title</a><a href="/people/publications/type/Pascal.Kesseli.html" aria-hidden="true" type="button" class="btn btn-oxford-blue"><span class="glyphicon glyphicon-sort-by-attributes"></span> By type</a><a href="/people/publications/bibtex/Pascal.Kesseli.html" aria-hidden="true" type="button" class="btn btn-default"><span class="glyphicon glyphicon-file"></span> BibTex</a></div></div><p></p><h2>
      Book chapters
      </h2><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>
            Automated Formal Synthesis of Digital Controllers for State&#x2212;Space Physical Plants </strong> </p>
	    <p class="publicationAuthors"> <em> Alessandro Abate&#x201a; Iury Bessa&#x201a; Dario Cattaruzza&#x201a; Lucas Cordeiro&#x201a; Cristina David&#x201a; Pascal Kesseli&#x201a; Daniel Kroening and Elizabeth Polgreen  </em> </p>
	
	<p class="publicationDetails"> 
            In Rupak Majumdar and Viktor Kun&#x010d;ak, editors,
             
            <em>
            Computer Aided Verification: 29th International Conference&#x201a; CAV 2017&#x201a; Heidelberg&#x201a; Germany&#x201a; July 24&#x2212;28&#x201a; 2017&#x201a; Proceedings&#x201a; Part I</em>.
        
                Pages 462&#x2013;482.
            Springer International Publishing, Cham.
        2017.
        </p>
	
        		<p class="publicationlinks"> <a
        
            		href="/publications/publication11603-abstract.html">
			Details <span class="sr-only" > about <em> Automated Formal Synthesis of Digital Controllers for State&#x2212;Space Physical Plants  </em></span> </a> |
			<a href="/publications/publication11603.bib">
			BibTeX  <span class="sr-only" > data for <em> Automated Formal Synthesis of Digital Controllers for State&#x2212;Space Physical Plants  </em></span>   </a>
			
			 | <a
		href="http://dx.doi.org/10.1007/978-3-319-63387-9_23">
		DOI (10.1007/978-3-319-63387-9_23)
		</a> 
					| <a href="https://doi.org/10.1007/978-3-319-63387-9_23"> Link <span class="sr-only" > to <em> Automated Formal Synthesis of Digital Controllers for State&#x2212;Space Physical Plants  </em></span> </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>
            Assisted Coverage Closure </strong> </p>
	    <p class="publicationAuthors"> <em> Adam Nellis&#x201a; Pascal Kesseli&#x201a; Philippa Ryan Conmy&#x201a; Daniel Kroening&#x201a; Peter Schrammel and Michael Tautschnig  </em> </p>
	
	<p class="publicationDetails"> 
            In Sanjai Rayadurgam and Oksana Tkachuk, editors,
             
            <em>
            NASA Formal Methods: 8th International Symposium&#x201a; NFM 2016&#x201a; Minneapolis&#x201a; MN&#x201a; USA&#x201a; June 7&#x2212;9&#x201a; 2016&#x201a; Proceedings</em>.
        
                Pages 49&#x2013;64.
            Springer International Publishing, Cham.
        2016.
        </p>
	
        		<p class="publicationlinks"> <a
        
            		href="/publications/publication10780-abstract.html">
			Details <span class="sr-only" > about <em> Assisted Coverage Closure  </em></span> </a> |
			<a href="/publications/publication10780.bib">
			BibTeX  <span class="sr-only" > data for <em> Assisted Coverage Closure  </em></span>   </a>
			
			 | <a
		href="http://dx.doi.org/10.1007/978-3-319-40648-0_5">
		DOI (10.1007/978-3-319-40648-0_5)
		</a> 
					| <a href="http://dx.doi.org/10.1007/978-3-319-40648-0_5"> Link <span class="sr-only" > to <em> Assisted Coverage Closure  </em></span> </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>
            Danger Invariants </strong> </p>
	    <p class="publicationAuthors"> <em> Cristina David&#x201a; Pascal Kesseli&#x201a; Daniel Kroening and Matt Lewis  </em> </p>
	
	<p class="publicationDetails"> 
            In John Fitzgerald&#x201a; Constance Heitmeyer&#x201a; Stefania Gnesi and Anna Philippou, editors,
             
            <em>
            FM 2016: Formal Methods: 21st International Symposium&#x201a; Limassol&#x201a; Cyprus&#x201a; November 9&#x2212;11&#x201a; 2016&#x201a; Proceedings</em>.
        
                Pages 182&#x2013;198.
            Springer International Publishing, Cham.
        2016.
        </p>
	
        		<p class="publicationlinks"> <a
        
            		href="/publications/publication10778-abstract.html">
			Details <span class="sr-only" > about <em> Danger Invariants  </em></span> </a> |
			<a href="/publications/publication10778.bib">
			BibTeX  <span class="sr-only" > data for <em> Danger Invariants  </em></span>   </a>
			
			 | <a
		href="http://dx.doi.org/10.1007/978-3-319-48989-6_12">
		DOI (10.1007/978-3-319-48989-6_12)
		</a> 
					| <a href="http://dx.doi.org/10.1007/978-3-319-48989-6_12"> Link <span class="sr-only" > to <em> Danger Invariants  </em></span> </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>
            Learning the Language of Error </strong> </p>
	    <p class="publicationAuthors"> <em> Martin Chapman&#x201a; Hana Chockler&#x201a; Pascal Kesseli&#x201a; Daniel Kroening&#x201a; Ofer Strichman and Michael Tautschnig  </em> </p>
	
	<p class="publicationDetails"> 
            In Bernd Finkbeiner&#x201a; Geguang Pu and Lijun Zhang, editors,
             
            <em>
            Automated Technology for Verification and Analysis: 13th International Symposium&#x201a; ATVA 2015&#x201a; Shanghai&#x201a; China&#x201a; October 12&#x2212;15&#x201a; 2015&#x201a; Proceedings</em>.
        
                Pages 114&#x2013;130.
            Springer International Publishing, Cham.
        2015.
        </p>
	
        		<p class="publicationlinks"> <a
        
            		href="/publications/publication10779-abstract.html">
			Details <span class="sr-only" > about <em> Learning the Language of Error  </em></span> </a> |
			<a href="/publications/publication10779.bib">
			BibTeX  <span class="sr-only" > data for <em> Learning the Language of Error  </em></span>   </a>
			
			 | <a
		href="http://dx.doi.org/10.1007/978-3-319-24953-7_9">
		DOI (10.1007/978-3-319-24953-7_9)
		</a> 
					| <a href="http://dx.doi.org/10.1007/978-3-319-24953-7_9"> Link <span class="sr-only" > to <em> Learning the Language of Error  </em></span> </a>
  				
		
		</div> 
	</div> 
	
        </li></ul><h2>
      Journal papers
      </h2><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>
            Automated formal synthesis of provably safe digital controllers for continuous plants </strong> </p>
	    <p class="publicationAuthors"> <em> Alessandro Abate&#x201a; Iury Bessa&#x201a; Lucas Cordeiro&#x201a; Cristina David&#x201a; Pascal Kesseli&#x201a; Daniel Kroening and Elizabeth Polgreen  </em> </p>
	
	<p class="publicationDetails"> 
        In <em>Acta Informatica</em>.
        December,
            2019.
        </p>
	
        		<p class="publicationlinks"> <a
        
            		href="/publications/publication13800-abstract.html">
			Details <span class="sr-only" > about <em> Automated formal synthesis of provably safe digital controllers for continuous plants  </em></span> </a> |
			<a href="/publications/publication13800.bib">
			BibTeX  <span class="sr-only" > data for <em> Automated formal synthesis of provably safe digital controllers for continuous plants  </em></span>   </a>
			
			 | <a
		href="http://dx.doi.org/10.1007/s00236-019-00359-1">
		DOI (10.1007/s00236-019-00359-1)
		</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>
            Program Synthesis for Program Analysis </strong> </p>
	    <p class="publicationAuthors"> <em> Cristina David&#x201a; Pascal Kesseli&#x201a; Daniel Kroening and Matt Lewis  </em> </p>
	
	<p class="publicationDetails"> 
        In <em>ACM Transactions on Programming Languages and Systems</em>.
        
            Vol. 40.
        
                Pages 1&#x2212;45.
            2018.
        </p>
	
        		<p class="publicationlinks"> <a
        
            		href="/publications/publication12049-abstract.html">
			Details <span class="sr-only" > about <em> Program Synthesis for Program Analysis  </em></span> </a> |
			<a href="/publications/publication12049.bib">
			BibTeX  <span class="sr-only" > data for <em> Program Synthesis for Program Analysis  </em></span>   </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>
            Kayak: Safe Semantic Refactoring to Java Streams </strong> </p>
	    <p class="publicationAuthors"> <em> Cristina David&#x201a; Pascal Kesseli and Daniel Kroening  </em> </p>
	
	<p class="publicationDetails"> 
        In <em>CoRR</em>.
        
            Vol. abs/1712.07388.
        2017.
        </p>
	
        		<p class="publicationlinks"> <a
        
            		href="/publications/publication13798-abstract.html">
			Details <span class="sr-only" > about <em> Kayak: Safe Semantic Refactoring to Java Streams  </em></span> </a> |
			<a href="/publications/publication13798.bib">
			BibTeX  <span class="sr-only" > data for <em> Kayak: Safe Semantic Refactoring to Java Streams  </em></span>   </a>
			
			
					| <a href="http://arxiv.org/abs/1712.07388"> Link <span class="sr-only" > to <em> Kayak: Safe Semantic Refactoring to Java Streams  </em></span> </a>
  				
		
		</div> 
	</div> 
	
        </li></ul><h2>
      Conference papers
      </h2><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>
            Counterexample Guided Inductive Synthesis Modulo Theories </strong> </p>
	    <p class="publicationAuthors"> <em> Alessandro Abate&#x201a; Cristina David&#x201a; Pascal Kesseli&#x201a; Daniel Kroening and Elizabeth Polgreen  </em> </p>
	
	<p class="publicationDetails"> 
            In Hana Chockler and Georg Weissenbacher, editors,
             
            <em>
            Computer Aided Verification</em>.
        
                Pages 270&#x2013;288.
            Cham.
        2018.
        Springer International Publishing.
        </p>
	
        		<p class="publicationlinks"> <a
        
            		href="/publications/publication12086-abstract.html">
			Details <span class="sr-only" > about <em> Counterexample Guided Inductive Synthesis Modulo Theories  </em></span> </a> |
			<a href="/publications/publication12086.bib">
			BibTeX  <span class="sr-only" > data for <em> Counterexample Guided Inductive Synthesis Modulo Theories  </em></span>   </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>
            JBMC: A Bounded Model Checking Tool for Verifying Java Bytecode </strong> </p>
	    <p class="publicationAuthors"> <em> Lucas Cordeiro&#x201a; Pascal Kesseli&#x201a; Daniel Kroening&#x201a; Peter Schrammel and Marek Trtik  </em> </p>
	
	<p class="publicationDetails"> 
            In Hana Chockler and Georg Weissenbacher, editors,
             
            <em>
            Computer Aided Verification</em>.
        
                Pages 183&#x2013;190.
            Cham.
        2018.
        Springer International Publishing.
        </p>
	
        		<p class="publicationlinks"> <a
        
            		href="/publications/publication12084-abstract.html">
			Details <span class="sr-only" > about <em> JBMC: A Bounded Model Checking Tool for Verifying Java Bytecode  </em></span> </a> |
			<a href="/publications/publication12084.bib">
			BibTeX  <span class="sr-only" > data for <em> JBMC: A Bounded Model Checking Tool for Verifying Java Bytecode  </em></span>   </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>
            DSSynth: an automated digital controller synthesis tool for physical plants </strong> </p>
	    <p class="publicationAuthors"> <em> Alessandro Abate&#x201a; Iury Bessa&#x201a; Dario Cattaruzza&#x201a; Lennon Chaves&#x201a; Lucas C. Cordeiro&#x201a; Cristina David&#x201a; Pascal Kesseli&#x201a; Daniel Kroening and Elizabeth Polgreen  </em> </p>
	
	<p class="publicationDetails"> 
            In  
            <em>
            Proceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering&#x201a; ASE 2017&#x201a; Urbana&#x201a; IL&#x201a; USA&#x201a; October 30 &#x2212; November 03&#x201a; 2017</em>.
        
                Pages 919&#x2013;924.
            2017.
        </p>
	
        		<p class="publicationlinks"> <a
        
            		href="/publications/publication12092-abstract.html">
			Details <span class="sr-only" > about <em> DSSynth: an automated digital controller synthesis tool for physical plants  </em></span> </a> |
			<a href="/publications/publication12092.bib">
			BibTeX  <span class="sr-only" > data for <em> DSSynth: an automated digital controller synthesis tool for physical plants  </em></span>   </a>
			
			 | <a
		href="http://dx.doi.org/10.1109/ASE.2017.8115705">
		DOI (10.1109/ASE.2017.8115705)
		</a> 
					| <a href="https://doi.org/10.1109/ASE.2017.8115705"> Link <span class="sr-only" > to <em> DSSynth: an automated digital controller synthesis tool for physical plants  </em></span> </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>
            Sound and Automated Synthesis of Digital Stabilizing Controllers for Continuous Plants </strong> </p>
	    <p class="publicationAuthors"> <em> Alessandro Abate&#x201a; Iury Bessa&#x201a; Dario Cattaruzza&#x201a; Lucas Cordeiro&#x201a; Cristina David&#x201a; Pascal Kesseli and Daniel Kroening  </em> </p>
	
	<p class="publicationDetails"> 
            In  
            <em>
            Proceedings of the 20th International Conference on Hybrid Systems: Computation and Control</em>.
        
                Pages 197&#x2013;206.
            New York&#x201a; NY&#x201a; USA.
        2017.
        ACM.
        </p>
	
        		<p class="publicationlinks"> <a
        
            		href="/publications/publication10964-abstract.html">
			Details <span class="sr-only" > about <em> Sound and Automated Synthesis of Digital Stabilizing Controllers for Continuous Plants  </em></span> </a> |
			<a href="/publications/publication10964.bib">
			BibTeX  <span class="sr-only" > data for <em> Sound and Automated Synthesis of Digital Stabilizing Controllers for Continuous Plants  </em></span>   </a>
			
			 | <a
		href="http://dx.doi.org/10.1145/3049797.3049802">
		DOI (10.1145/3049797.3049802)
		</a> 
					| <a href="http://doi.acm.org/10.1145/3049797.3049802"> Link <span class="sr-only" > to <em> Sound and Automated Synthesis of Digital Stabilizing Controllers for Continuous Plants  </em></span> </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><a href="/people/faculty.html">Faculty</a></li><li><a href="/people/research.html">Research</a></li><li class="active"><a href="/people/students.html">Students</a></li><li><a href="/people/support.html">Professional Services</a></li></ul></li><li><a href="/aboutus/vacancies/">Vacancies</a></li><li><a href="/aboutus/cshistory.html">History</a></li><li><a href="/aboutus/contact.html">Contact Us</a></li></ul></div></div></div>[an error occurred while processing this directive]