<?xml version="1.0" encoding="UTF-8"?>
<TEI xml:space="preserve" xmlns="http://www.tei-c.org/ns/1.0" 
xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" 
xsi:schemaLocation="http://www.tei-c.org/ns/1.0 https://raw.githubusercontent.com/kermitt2/grobid/master/grobid-home/schemas/xsd/Grobid.xsd"
 xmlns:xlink="http://www.w3.org/1999/xlink">
	<teiHeader xml:lang="en">
		<fileDesc>
			<titleStmt>
				<title level="a" type="main">Invited Talk: Challenges in Bit-Vector Reasoning</title>
			</titleStmt>
			<publicationStmt>
				<publisher/>
				<availability status="unknown"><licence/></availability>
			</publicationStmt>
			<sourceDesc>
				<biblStruct>
					<analytic>
						<author role="corresp">
							<persName><forename type="first">Mathias</forename><surname>Preiner</surname></persName>
							<email>preiner@cs.stanford.edu</email>
							<affiliation key="aff0">
								<orgName type="institution">Stanford University</orgName>
							</affiliation>
						</author>
						<title level="a" type="main">Invited Talk: Challenges in Bit-Vector Reasoning</title>
					</analytic>
					<monogr>
						<idno type="ISSN">1613-0073</idno>
					</monogr>
					<idno type="MD5">75B9200EAC20793AE243818F32CF9077</idno>
				</biblStruct>
			</sourceDesc>
		</fileDesc>
		<encodingDesc>
			<appInfo>
				<application version="0.7.2" ident="GROBID" when="2025-04-23T17:21+0000">
					<desc>GROBID - A machine learning software for extracting information from scholarly documents</desc>
					<ref target="https://github.com/kermitt2/grobid"/>
				</application>
			</appInfo>
		</encodingDesc>
		<profileDesc>
			<abstract>
<div xmlns="http://www.tei-c.org/ns/1.0"><p>The theory of fixed-size bit-vectors in Satisfiability Modulo Theories is essential in bit-precise reasoning applications. The dominant state-of-the-art approach for solving bit-vector formulas is a technique called bit-blasting, an eager reduction of bit-vectors to SAT. While surprisingly efficient in practice, bit-blasting may not scale for large bit-vectors or if bit-vector arithmetic is involved. In this talk, I will highlight challenges in reasoning over bit-vectors and discuss the current state of bit-level and word-level approaches.</p></div>
			</abstract>
		</profileDesc>
	</teiHeader>
	<text xml:lang="en">
		<body/>
		<back>
			<div type="references">

				<listBibl/>
			</div>
		</back>
	</text>
</TEI>
