[an error occurred while processing this directive]<meta name="keywords" content="Department of Computer Science, publications, by type, Hardware Verification"></meta><meta name="description" content="Publications, by type,Hardware Verification, Department of Computer Science, Oxford"></meta><title>Department of Computer Science: Hardware Verification: 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="/research/">Research</a></li><li><a href="/research/verification/">Automated Verification</a></li><li><a href="/research/verification/activities.html">activities</a></li><li><a href="/activities/hardwareverification/">Hardware Verification</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>Hardware Verification: Publications
</h1></div><div role="toolbar" class="btn-toolbar"><div class="btn-group"><a href="/activities/publications/date/hardwareverification.html" aria-hidden="true" type="button" class="btn btn-default"><span class="glyphicon glyphicon-sort-by-attributes"></span> By date</a><a href="/activities/publications/title/hardwareverification.html" aria-hidden="true" type="button" class="btn btn-default"><span class="glyphicon glyphicon-sort-by-attributes"></span> By title</a><a href="/activities/publications/type/hardwareverification.html" aria-hidden="true" type="button" class="btn btn-oxford-blue"><span class="glyphicon glyphicon-sort-by-attributes"></span> By type</a><a href="/activities/publications/bibtex/hardwareverification.html" aria-hidden="true" type="button" class="btn btn-default"><span class="glyphicon glyphicon-file"></span> BibTex</a></div></div><h2>
      Books
      </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>
            Decision Procedures &#x2013; an Algorithmic Point of View </strong> </p>
	    <p class="publicationAuthors"> <em> Daniel Kroening and Ofer Strichman  </em> </p>
	
	<p class="publicationDetails"> Springer.
        2008.
        </p> <p
            class="publicationNote"> To appear</p>
	
        		<p class="publicationlinks"> <a
        
            		href="/publications/publication712-abstract.html">
			Details <span class="sr-only" > about <em> Decision Procedures &#x2013; an Algorithmic Point of View  </em></span> </a> |
			<a href="/publications/publication712.bib">
			BibTeX  <span class="sr-only" > data for <em> Decision Procedures &#x2013; an Algorithmic Point of View  </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>
            Word Level Predicate Abstraction and Refinement for Verifying RTL Verilog </strong> </p>
	    <p class="publicationAuthors"> <em> Himanshu Jain&#x201a; Daniel Kroening&#x201a; Natasha Sharygina and Edmund Clarke  </em> </p>
	
	<p class="publicationDetails"> 
        In <em>IEEE Transactions on Computer&#x2212;Aided Design of Integrated Circuits and Systems (TCAD)</em>.
        
            Vol. 27.
        
                Pages 366&#x2013;379.
            February,
            2008.
        </p>
	
        		<p class="publicationlinks"> <a
        
            		href="/publications/publication707-abstract.html">
			Details <span class="sr-only" > about <em> Word Level Predicate Abstraction and Refinement for Verifying RTL Verilog  </em></span> </a> |
			<a href="/publications/publication707.bib">
			BibTeX  <span class="sr-only" > data for <em> Word Level Predicate Abstraction and Refinement for Verifying RTL Verilog  </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>
            Scoot: A Tool for the Analysis of SystemC Models </strong> </p>
	    <p class="publicationAuthors"> <em> Nicolas Blanc&#x201a; Daniel Kroening and Natasha Sharygina  </em> </p>
	
	<p class="publicationDetails"> 
            In  
            <em>
            Proceedings of TACAS 2008</em>.
        Springer.
        2008.
        </p> <p
            class="publicationNote"> To appear.</p>
	
        		<p class="publicationlinks"> <a
        
            		href="/publications/publication697-abstract.html">
			Details <span class="sr-only" > about <em> Scoot: A Tool for the Analysis of SystemC Models  </em></span> </a> |
			<a href="/publications/publication697.bib">
			BibTeX  <span class="sr-only" > data for <em> Scoot: A Tool for the Analysis of SystemC Models  </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>
            Deciding Bit&#x2212;Vector Arithmetic with Abstraction </strong> </p>
	    <p class="publicationAuthors"> <em> Randal E. Bryant&#x201a; Daniel Kroening&#x201a; Joel Ouaknine&#x201a; Sanjit A. Seshia&#x201a; Ofer Strichman and Bryan Brady  </em> </p>
	
	<p class="publicationDetails"> 
            In  
            <em>
            Proceedings of TACAS 2007</em>.
        
            Vol. 4424
                of Lecture Notes in Computer Science.
        
                Pages 358&#x2013;372.
            Springer.
        2007.
        </p>
	
        		<p class="publicationlinks"> <a
        
            		href="/publications/publication715-abstract.html">
			Details <span class="sr-only" > about <em> Deciding Bit&#x2212;Vector Arithmetic with Abstraction  </em></span> </a> |
			<a href="/publications/publication715.bib">
			BibTeX  <span class="sr-only" > data for <em> Deciding Bit&#x2212;Vector Arithmetic with Abstraction  </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>
            VCEGAR: Verilog CounterExample Guided Abstraction Refinement </strong> </p>
	    <p class="publicationAuthors"> <em> Himanshu Jain&#x201a; Daniel Kroening&#x201a; Natasha Sharygina and Edmund Clarke  </em> </p>
	
	<p class="publicationDetails"> 
            In  
            <em>
            Proceedings of TACAS 2007</em>.
        
            Vol. 4424
                of Lecture Notes in Computer Science.
        
                Pages 583&#x2013;586.
            Springer.
        2007.
        </p>
	
        		<p class="publicationlinks"> <a
        
            		href="/publications/publication713-abstract.html">
			Details <span class="sr-only" > about <em> VCEGAR: Verilog CounterExample Guided Abstraction Refinement  </em></span> </a> |
			<a href="/publications/publication713.bib">
			BibTeX  <span class="sr-only" > data for <em> VCEGAR: Verilog CounterExample Guided Abstraction Refinement  </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>
            Formal Verification of SystemC by Automatic Hardware/Software Partitioning </strong> </p>
	    <p class="publicationAuthors"> <em> Daniel Kroening and Natasha Sharygina  </em> </p>
	
	<p class="publicationDetails"> 
            In  
            <em>
            Proceedings of MEMOCODE 2005</em>.
        
                Pages 101&#x2013;110.
            IEEE.
        2005.
        </p>
	
        		<p class="publicationlinks"> <a
        
            		href="/publications/publication725-abstract.html">
			Details <span class="sr-only" > about <em> Formal Verification of SystemC by Automatic Hardware/Software Partitioning  </em></span> </a> |
			<a href="/publications/publication725.bib">
			BibTeX  <span class="sr-only" > data for <em> Formal Verification of SystemC by Automatic Hardware/Software Partitioning  </em></span>   </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>
            Verification of SpecC and Verilog using Predicate Abstraction </strong> </p>
	    <p class="publicationAuthors"> <em> Himanshu Jain&#x201a; Edmund Clarke and Daniel Kroening  </em> </p>
	
	<p class="publicationDetails"> 
            In  
            <em>
            Proceedings of MEMOCODE 2004</em>.
        
                Pages 7&#x2013;16.
            IEEE.
        2004.
        </p>
	
        		<p class="publicationlinks"> <a
        
            		href="/publications/publication737-abstract.html">
			Details <span class="sr-only" > about <em> Verification of SpecC and Verilog using Predicate Abstraction  </em></span> </a> |
			<a href="/publications/publication737.bib">
			BibTeX  <span class="sr-only" > data for <em> Verification of SpecC and Verilog using Predicate Abstraction  </em></span>   </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>
            A SAT&#x2212;Based Algorithm for Reparameterization in Symbolic Simulation </strong> </p>
	    <p class="publicationAuthors"> <em> Pankaj Chauhan&#x201a; Edmund Clarke and Daniel Kroening  </em> </p>
	
	<p class="publicationDetails"> 
            In  
            <em>
            Proceedings of DAC 2004</em>.
        
                Pages 524&#x2013;529.
            ACM Press.
        2004.
        </p>
	
        		<p class="publicationlinks"> <a
        
            		href="/publications/publication738-abstract.html">
			Details <span class="sr-only" > about <em> A SAT&#x2212;Based Algorithm for Reparameterization in Symbolic Simulation  </em></span> </a> |
			<a href="/publications/publication738.bib">
			BibTeX  <span class="sr-only" > data for <em> A SAT&#x2212;Based Algorithm for Reparameterization in Symbolic Simulation  </em></span>   </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>
            Specifying and Verifying Systems with Multiple Clocks </strong> </p>
	    <p class="publicationAuthors"> <em> Edmund Clarke&#x201a; Daniel Kroening and Karen Yorav  </em> </p>
	
	<p class="publicationDetails"> 
            In  
            <em>
            Proc. of the 2003 International Conference on Computer Design (ICCD)</em>.
        
                Pages 48&#x2013;55.
            IEEE.
        October,
            2003.
        </p>
	
        		<p class="publicationlinks"> <a
        
            		href="/publications/publication742-abstract.html">
			Details <span class="sr-only" > about <em> Specifying and Verifying Systems with Multiple Clocks  </em></span> </a> |
			<a href="/publications/publication742.bib">
			BibTeX  <span class="sr-only" > data for <em> Specifying and Verifying Systems with Multiple Clocks  </em></span>   </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>
            Behavioral Consistency of C and Verilog Programs Using Bounded Model Checking </strong> </p>
	    <p class="publicationAuthors"> <em> Daniel Kroening&#x201a; Edmund Clarke and Karen Yorav  </em> </p>
	
	<p class="publicationDetails"> 
            In  
            <em>
            Proceedings of DAC 2003</em>.
        
                Pages 368&#x2013;371.
            ACM Press.
        2003.
        </p>
	
        		<p class="publicationlinks"> <a
        
            		href="/publications/publication744-abstract.html">
			Details <span class="sr-only" > about <em> Behavioral Consistency of C and Verilog Programs Using Bounded Model Checking  </em></span> </a> |
			<a href="/publications/publication744.bib">
			BibTeX  <span class="sr-only" > data for <em> Behavioral Consistency of C and Verilog Programs Using Bounded Model Checking  </em></span>   </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>
            Automated Pipeline Design </strong> </p>
	    <p class="publicationAuthors"> <em> Daniel Kroening and Wolfgang Paul  </em> </p>
	
	<p class="publicationDetails"> 
            In  
            <em>
            Proc. of 38th ACM/IEEE Design Automation Conference (DAC 2001)</em>.
        
                Pages 810&#x2013;815.
            ACM Press.
        2001.
        </p>
	
        		<p class="publicationlinks"> <a
        
            		href="/publications/publication747-abstract.html">
			Details <span class="sr-only" > about <em> Automated Pipeline Design  </em></span> </a> |
			<a href="/publications/publication747.bib">
			BibTeX  <span class="sr-only" > data for <em> Automated Pipeline Design  </em></span>   </a>
			
			
		
		</div> 
	</div> 
	
        </li></ul></div><div class="col-xs-12 col-md-3 col-md-pull-9 side-menu-col">[an error occurred while processing this directive]</div></div></div>[an error occurred while processing this directive]