<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE rdf:RDF[
	<!ENTITY rdf 'http://www.w3.org/1999/02/22-rdf-syntax-ns#'>
	<!ENTITY rdfs 'http://www.w3.org/2000/01/rdf-schema#'>
	<!ENTITY owl 'http://www.w3.org/2002/07/owl#'>
	<!ENTITY swivt 'http://semantic-mediawiki.org/swivt/1.0#'>
	<!ENTITY wiki 'http://murray.cds.caltech.edu/Special:URIResolver/'>
	<!ENTITY category 'http://murray.cds.caltech.edu/Special:URIResolver/Category-3A'>
	<!ENTITY property 'http://murray.cds.caltech.edu/Special:URIResolver/Property-3A'>
	<!ENTITY wikiurl 'https://murray.cds.caltech.edu/'>
]>

<rdf:RDF
	xmlns:rdf="&rdf;"
	xmlns:rdfs="&rdfs;"
	xmlns:owl ="&owl;"
	xmlns:swivt="&swivt;"
	xmlns:wiki="&wiki;"
	xmlns:category="&category;"
	xmlns:property="&property;">

	<owl:Ontology rdf:about="https://murray.cds.caltech.edu/Special:ExportRDF/Fast_Automatic_Verification_of_Large-2DScale_Systems_with_Lookup_Tables">
		<swivt:creationDate rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2026-04-15T05:25:48+00:00</swivt:creationDate>
		<owl:imports rdf:resource="http://semantic-mediawiki.org/swivt/1.0"/>
	</owl:Ontology>
	<swivt:Subject rdf:about="http://murray.cds.caltech.edu/Special:URIResolver/Fast_Automatic_Verification_of_Large-2DScale_Systems_with_Lookup_Tables">
		<rdf:type rdf:resource="http://murray.cds.caltech.edu/Special:URIResolver/Category-3APapers"/>
		<rdfs:label>Fast Automatic Verification of Large-Scale Systems with Lookup Tables</rdfs:label>
		<rdfs:isDefinedBy rdf:resource="https://murray.cds.caltech.edu/Special:ExportRDF/Fast_Automatic_Verification_of_Large-2DScale_Systems_with_Lookup_Tables"/>
		<swivt:page rdf:resource="https://murray.cds.caltech.edu/Fast_Automatic_Verification_of_Large-2DScale_Systems_with_Lookup_Tables"/>
		<swivt:wikiNamespace rdf:datatype="http://www.w3.org/2001/XMLSchema#integer">0</swivt:wikiNamespace>
		<swivt:wikiPageContentLanguage rdf:datatype="http://www.w3.org/2001/XMLSchema#string">en</swivt:wikiPageContentLanguage>
		<property:Abstract rdf:datatype="http://www.w3.org/2001/XMLSchema#string">Modern safety-critical systems are difficult to formally verify, largely due to their large scale. In particular, the widespread use of lookup tables in embedded systems across diverse industries, such as aeronautics and automotive systems, create a critical obstacle to the scala- bility of formal verification. This paper presents a novel approach for the formal verification of large-scale systems with lookup tables. We use a learning-based technique to automatically learn abstractions of the lookup tables and use the abstractions to then prove the desired property. If the verification fails, we propose a falsification heuristic to search for a violation of the specification. In contrast with previous work on lookup table verification, our technique is completely automatic, making it ideal for deployment in a production environment. To our knowledge, our approach is the only technique that can automatically verify large-scale systems lookup with tables.

We illustrate the effectiveness of our technique on a benchmark which cannot be handled by the commer- cial tool SLDV, and we demonstrate the performance improvement provided by our technique.</property:Abstract>
		<property:Authors rdf:datatype="http://www.w3.org/2001/XMLSchema#string">Nikos Arichega</property:Authors>
		<property:Authors rdf:datatype="http://www.w3.org/2001/XMLSchema#string">Sumanth Dathathri</property:Authors>
		<property:Authors rdf:datatype="http://www.w3.org/2001/XMLSchema#string">Shashank Vernekar</property:Authors>
		<property:Authors rdf:datatype="http://www.w3.org/2001/XMLSchema#string">Sicun Gao</property:Authors>
		<property:Authors rdf:datatype="http://www.w3.org/2001/XMLSchema#string">Shin’Ichi Shiraishi</property:Authors>
		<property:Authors rdf:datatype="http://www.w3.org/2001/XMLSchema#string">Richard M. Murray</property:Authors>
		<property:ID rdf:datatype="http://www.w3.org/2001/XMLSchema#string">2016h</property:ID>
		<property:Source rdf:datatype="http://www.w3.org/2001/XMLSchema#string">Submitted, 2017 ACM International Conference on Hybrid Systems: Computation and Control (HSCC)</property:Source>
		<property:Tag rdf:datatype="http://www.w3.org/2001/XMLSchema#string">ari+17-hscc</property:Tag>
		<property:Title rdf:resource="&wiki;Fast_Automatic_Verification_of_Large-2DScale_Systems_with_Lookup_Tables"/>
		<property:Type rdf:datatype="http://www.w3.org/2001/XMLSchema#string">Conference paper</property:Type>
		<swivt:wikiPageModificationDate rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2017-01-13T03:35:09Z</swivt:wikiPageModificationDate>
		<property:Modification_date-23aux rdf:datatype="http://www.w3.org/2001/XMLSchema#double">2457766.6494097</property:Modification_date-23aux>
		<swivt:wikiPageSortKey rdf:datatype="http://www.w3.org/2001/XMLSchema#string">Fast Automatic Verification of Large-Scale Systems with Lookup Tables</swivt:wikiPageSortKey>
		<property:URL rdf:resource="http://www.cds.caltech.edu/~murray/preprints/ari+17-hscc_s.pdf"/>
	</swivt:Subject>
	<owl:ObjectProperty rdf:about="http://murray.cds.caltech.edu/Special:URIResolver/Property-3ATitle">
		<rdfs:label>Title</rdfs:label>
		<rdfs:isDefinedBy rdf:resource="https://murray.cds.caltech.edu/Special:ExportRDF/Property-3ATitle"/>
		<swivt:page rdf:resource="https://murray.cds.caltech.edu/Property-3ATitle"/>
		<swivt:wikiNamespace rdf:datatype="http://www.w3.org/2001/XMLSchema#integer">102</swivt:wikiNamespace>
		<swivt:wikiPageContentLanguage rdf:datatype="http://www.w3.org/2001/XMLSchema#string">en</swivt:wikiPageContentLanguage>
		<swivt:wikiPageSortKey rdf:datatype="http://www.w3.org/2001/XMLSchema#string">Title</swivt:wikiPageSortKey>
		<swivt:type rdf:resource="http://semantic-mediawiki.org/swivt/1.0#_wpg"/>
	</owl:ObjectProperty>
	<owl:DatatypeProperty rdf:about="http://semantic-mediawiki.org/swivt/1.0#creationDate" />
	<owl:Class rdf:about="http://murray.cds.caltech.edu/Special:URIResolver/Category-3APapers" />
	<owl:ObjectProperty rdf:about="http://semantic-mediawiki.org/swivt/1.0#page" />
	<owl:DatatypeProperty rdf:about="http://semantic-mediawiki.org/swivt/1.0#wikiNamespace" />
	<owl:DatatypeProperty rdf:about="http://semantic-mediawiki.org/swivt/1.0#wikiPageContentLanguage" />
	<owl:DatatypeProperty rdf:about="http://murray.cds.caltech.edu/Special:URIResolver/Property-3AAbstract" />
	<owl:DatatypeProperty rdf:about="http://murray.cds.caltech.edu/Special:URIResolver/Property-3AAuthors" />
	<owl:DatatypeProperty rdf:about="http://murray.cds.caltech.edu/Special:URIResolver/Property-3AID" />
	<owl:DatatypeProperty rdf:about="http://murray.cds.caltech.edu/Special:URIResolver/Property-3ASource" />
	<owl:DatatypeProperty rdf:about="http://murray.cds.caltech.edu/Special:URIResolver/Property-3ATag" />
	<owl:DatatypeProperty rdf:about="http://murray.cds.caltech.edu/Special:URIResolver/Property-3AType" />
	<owl:DatatypeProperty rdf:about="http://semantic-mediawiki.org/swivt/1.0#wikiPageModificationDate" />
	<owl:DatatypeProperty rdf:about="http://murray.cds.caltech.edu/Special:URIResolver/Property-3AModification_date-23aux" />
	<owl:DatatypeProperty rdf:about="http://semantic-mediawiki.org/swivt/1.0#wikiPageSortKey" />
	<owl:ObjectProperty rdf:about="http://murray.cds.caltech.edu/Special:URIResolver/Property-3AURL" />
	<owl:ObjectProperty rdf:about="http://semantic-mediawiki.org/swivt/1.0#type" />
	<!-- Created by Semantic MediaWiki, https://www.semantic-mediawiki.org/ -->
</rdf:RDF>