<> <http://www.w3.org/2000/01/rdf-schema#comment> "The repository administrator has not yet configured an RDF license."^^<http://www.w3.org/2001/XMLSchema#string> .
<> <http://xmlns.com/foaf/0.1/primaryTopic> <https://discovery.ucl.ac.uk/id/eprint/1455002> .
<https://discovery.ucl.ac.uk/id/eprint/1455002> <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <http://purl.org/ontology/bibo/Article> .
<https://discovery.ucl.ac.uk/id/eprint/1455002> <http://purl.org/dc/terms/title> "A decision procedure for satisfiability in separation logic with inductive predicates"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://discovery.ucl.ac.uk/id/eprint/1455002> <http://purl.org/ontology/bibo/abstract> "We show that the satisfiability problem for the \"symbolic heap\" fragment of separation logic with general inductively defined predicates- which includes most fragments employed in program verification - is decidable. Our decision procedure is based on the computation of a certain fixed point from the definition of an inductive predicate, called its \"base\", that exactly characterises its satisfiability. A complexity analysis of our decision procedure shows that it runs, in the worst case, in exponential time. In fact, we show that the satisfiability problem for our inductive predicates is EXPTIME- complete, and becomes NP-complete when the maximum arity over all predicates is bounded by a constant. Finally, we provide an implementation of our decision procedure, and analyse its performance both on a synthetically generated set of test formulas, and on a second test set harvested from the separation logic literature. For the large majority of these test cases, our tool reports times in the low milliseconds. Copyright © 2014 ACM."^^<http://www.w3.org/2001/XMLSchema#string> .
<https://discovery.ucl.ac.uk/id/eprint/1455002> <http://purl.org/dc/terms/date> "2014-08" .
<https://discovery.ucl.ac.uk/id/document/75030> <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <http://purl.org/ontology/bibo/Document> .
<https://discovery.ucl.ac.uk/id/org/ext-83e592c058b42423df2a2b182c5be594> <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <http://xmlns.com/foaf/0.1/Organization> .
<https://discovery.ucl.ac.uk/id/org/ext-83e592c058b42423df2a2b182c5be594> <http://xmlns.com/foaf/0.1/name> "Association for Computing Machinery (ACM)"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://discovery.ucl.ac.uk/id/eprint/1455002> <http://purl.org/dc/terms/publisher> <https://discovery.ucl.ac.uk/id/org/ext-83e592c058b42423df2a2b182c5be594> .
<https://discovery.ucl.ac.uk/id/eprint/1455002> <http://purl.org/ontology/bibo/status> <http://purl.org/ontology/bibo/status/published> .
<https://discovery.ucl.ac.uk/id/eprint/1455002> <http://purl.org/dc/terms/creator> <https://discovery.ucl.ac.uk/id/person/ext-12415a819e6288d2682da8d4ac000d08> .
<https://discovery.ucl.ac.uk/id/eprint/1455002> <http://purl.org/ontology/bibo/authorList> <https://discovery.ucl.ac.uk/id/eprint/1455002#authors> .
<https://discovery.ucl.ac.uk/id/eprint/1455002#authors> <http://www.w3.org/1999/02/22-rdf-syntax-ns#_1> <https://discovery.ucl.ac.uk/id/person/ext-12415a819e6288d2682da8d4ac000d08> .
<https://discovery.ucl.ac.uk/id/eprint/1455002> <http://purl.org/dc/terms/creator> <https://discovery.ucl.ac.uk/id/person/ext-5a7077400a5dd57a293862cc217749ed> .
<https://discovery.ucl.ac.uk/id/eprint/1455002> <http://purl.org/ontology/bibo/authorList> <https://discovery.ucl.ac.uk/id/eprint/1455002#authors> .
<https://discovery.ucl.ac.uk/id/eprint/1455002#authors> <http://www.w3.org/1999/02/22-rdf-syntax-ns#_2> <https://discovery.ucl.ac.uk/id/person/ext-5a7077400a5dd57a293862cc217749ed> .
<https://discovery.ucl.ac.uk/id/eprint/1455002> <http://purl.org/dc/terms/creator> <https://discovery.ucl.ac.uk/id/person/ext-195d250f6f83f108f082f1305388fe73> .
<https://discovery.ucl.ac.uk/id/eprint/1455002> <http://purl.org/ontology/bibo/authorList> <https://discovery.ucl.ac.uk/id/eprint/1455002#authors> .
<https://discovery.ucl.ac.uk/id/eprint/1455002#authors> <http://www.w3.org/1999/02/22-rdf-syntax-ns#_3> <https://discovery.ucl.ac.uk/id/person/ext-195d250f6f83f108f082f1305388fe73> .
<https://discovery.ucl.ac.uk/id/eprint/1455002> <http://purl.org/dc/terms/creator> <https://discovery.ucl.ac.uk/id/person/ext-1f4343bed85f99e6a171c444ff972ae0> .
<https://discovery.ucl.ac.uk/id/eprint/1455002> <http://purl.org/ontology/bibo/authorList> <https://discovery.ucl.ac.uk/id/eprint/1455002#authors> .
<https://discovery.ucl.ac.uk/id/eprint/1455002#authors> <http://www.w3.org/1999/02/22-rdf-syntax-ns#_4> <https://discovery.ucl.ac.uk/id/person/ext-1f4343bed85f99e6a171c444ff972ae0> .
<https://discovery.ucl.ac.uk/id/person/ext-5a7077400a5dd57a293862cc217749ed> <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <http://xmlns.com/foaf/0.1/Person> .
<https://discovery.ucl.ac.uk/id/person/ext-5a7077400a5dd57a293862cc217749ed> <http://xmlns.com/foaf/0.1/givenName> "C"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://discovery.ucl.ac.uk/id/person/ext-5a7077400a5dd57a293862cc217749ed> <http://xmlns.com/foaf/0.1/familyName> "Fuhs"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://discovery.ucl.ac.uk/id/person/ext-5a7077400a5dd57a293862cc217749ed> <http://xmlns.com/foaf/0.1/name> "C Fuhs"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://discovery.ucl.ac.uk/id/person/ext-195d250f6f83f108f082f1305388fe73> <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <http://xmlns.com/foaf/0.1/Person> .
<https://discovery.ucl.ac.uk/id/person/ext-195d250f6f83f108f082f1305388fe73> <http://xmlns.com/foaf/0.1/givenName> "JAN"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://discovery.ucl.ac.uk/id/person/ext-195d250f6f83f108f082f1305388fe73> <http://xmlns.com/foaf/0.1/familyName> "Pérez"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://discovery.ucl.ac.uk/id/person/ext-195d250f6f83f108f082f1305388fe73> <http://xmlns.com/foaf/0.1/name> "JAN Pérez"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://discovery.ucl.ac.uk/id/person/ext-12415a819e6288d2682da8d4ac000d08> <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <http://xmlns.com/foaf/0.1/Person> .
<https://discovery.ucl.ac.uk/id/person/ext-12415a819e6288d2682da8d4ac000d08> <http://xmlns.com/foaf/0.1/givenName> "J"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://discovery.ucl.ac.uk/id/person/ext-12415a819e6288d2682da8d4ac000d08> <http://xmlns.com/foaf/0.1/familyName> "Brotherston"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://discovery.ucl.ac.uk/id/person/ext-12415a819e6288d2682da8d4ac000d08> <http://xmlns.com/foaf/0.1/name> "J Brotherston"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://discovery.ucl.ac.uk/id/person/ext-1f4343bed85f99e6a171c444ff972ae0> <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <http://xmlns.com/foaf/0.1/Person> .
<https://discovery.ucl.ac.uk/id/person/ext-1f4343bed85f99e6a171c444ff972ae0> <http://xmlns.com/foaf/0.1/givenName> "N"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://discovery.ucl.ac.uk/id/person/ext-1f4343bed85f99e6a171c444ff972ae0> <http://xmlns.com/foaf/0.1/familyName> "Gorogiannis"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://discovery.ucl.ac.uk/id/person/ext-1f4343bed85f99e6a171c444ff972ae0> <http://xmlns.com/foaf/0.1/name> "N Gorogiannis"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://discovery.ucl.ac.uk/id/eprint/1455002> <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <http://purl.org/ontology/bibo/Article> .
<https://discovery.ucl.ac.uk/id/eprint/1455002> <http://purl.org/ontology/bibo/presentedAt> <https://discovery.ucl.ac.uk/id/event/ext-44566773c112875d6c2eed8a8338dee8> .
<https://discovery.ucl.ac.uk/id/event/ext-44566773c112875d6c2eed8a8338dee8> <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <http://purl.org/ontology/bibo/Conference> .
<https://discovery.ucl.ac.uk/id/event/ext-44566773c112875d6c2eed8a8338dee8> <http://purl.org/dc/terms/title> "23rd EACSL Annual Conference on Computer Science Logic, CSL 2014 and the 29th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2014, Vienna, Austria — July 14 - 18, 2014 "^^<http://www.w3.org/2001/XMLSchema#string> .
<https://discovery.ucl.ac.uk/id/eprint/1455002> <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <http://eprints.org/ontology/EPrint> .
<https://discovery.ucl.ac.uk/id/eprint/1455002> <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <http://eprints.org/ontology/ProceedingsSectionEPrint> .
<https://discovery.ucl.ac.uk/id/eprint/1455002> <http://purl.org/dc/terms/isPartOf> <https://discovery.ucl.ac.uk/id/repository> .
<https://discovery.ucl.ac.uk/id/eprint/1455002> <http://eprints.org/ontology/hasDocument> <https://discovery.ucl.ac.uk/id/document/75030> .
<https://discovery.ucl.ac.uk/id/document/75030> <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <http://eprints.org/ontology/Document> .
<https://discovery.ucl.ac.uk/id/document/75030> <http://www.w3.org/2000/01/rdf-schema#label> "A decision procedure for satisfiability in separation logic with inductive predicates (PDF)"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://discovery.ucl.ac.uk/id/document/75030> <http://eprints.org/ontology/hasFile> <https://discovery.ucl.ac.uk/id/eprint/1455002/2/a25-brotherston.pdf> .
<https://discovery.ucl.ac.uk/id/document/75030> <http://purl.org/dc/terms/hasPart> <https://discovery.ucl.ac.uk/id/eprint/1455002/2/a25-brotherston.pdf> .
<https://discovery.ucl.ac.uk/id/eprint/1455002/2/a25-brotherston.pdf> <http://www.w3.org/2000/01/rdf-schema#label> "a25-brotherston.pdf"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://discovery.ucl.ac.uk/id/eprint/1455002> <http://eprints.org/ontology/hasDocument> <https://discovery.ucl.ac.uk/id/document/125049> .
<https://discovery.ucl.ac.uk/id/document/125049> <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <http://eprints.org/ontology/Document> .
<https://discovery.ucl.ac.uk/id/document/125049> <http://www.w3.org/2000/01/rdf-schema#label> "A decision procedure for satisfiability in separation logic with inductive predicates (Other)"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://discovery.ucl.ac.uk/id/document/125049> <http://eprints.org/relation/isVersionOf> <https://discovery.ucl.ac.uk/id/document/75030> .
<https://discovery.ucl.ac.uk/id/document/125049> <http://eprints.org/relation/isVolatileVersionOf> <https://discovery.ucl.ac.uk/id/document/75030> .
<https://discovery.ucl.ac.uk/id/document/125049> <http://eprints.org/relation/isIndexCodesVersionOf> <https://discovery.ucl.ac.uk/id/document/75030> .
<https://discovery.ucl.ac.uk/id/document/125049> <http://eprints.org/ontology/hasFile> <https://discovery.ucl.ac.uk/id/eprint/1455002/3/indexcodes.txt> .
<https://discovery.ucl.ac.uk/id/document/125049> <http://purl.org/dc/terms/hasPart> <https://discovery.ucl.ac.uk/id/eprint/1455002/3/indexcodes.txt> .
<https://discovery.ucl.ac.uk/id/eprint/1455002/3/indexcodes.txt> <http://www.w3.org/2000/01/rdf-schema#label> "indexcodes.txt"^^<http://www.w3.org/2001/XMLSchema#string> .
<https://discovery.ucl.ac.uk/id/eprint/1455002> <http://www.w3.org/2000/01/rdf-schema#seeAlso> <https://discovery.ucl.ac.uk/id/eprint/1455002/> .
<https://discovery.ucl.ac.uk/id/eprint/1455002/> <http://purl.org/dc/elements/1.1/title> "HTML Summary of #1455002 \n\nA decision procedure for satisfiability in separation logic with inductive predicates\n\n" .
<https://discovery.ucl.ac.uk/id/eprint/1455002/> <http://purl.org/dc/elements/1.1/format> "text/html" .
<https://discovery.ucl.ac.uk/id/eprint/1455002/> <http://xmlns.com/foaf/0.1/primaryTopic> <https://discovery.ucl.ac.uk/id/eprint/1455002> .