• GRASShopper

  • Referenced in 5 articles [sw23304]
  • properties. The logic supports mixing of separation logic and first-order logic assertions, yielding expressive...
  • VeriStar

  • Referenced in 3 articles [sw09393]
  • prover for a decidable subset of separation logic. Together with VeriSmall, a proved-sound Smallfoot ... tightly integrated collection of machine-verified program logics and compilers giving foundational correctness guarantees.par VeriStar ... entailment holds in a proved-sound separation logic for C minor ... easily be ported to other separation logics...
  • THOR

  • Referenced in 5 articles [sw15079]
  • Oriented Reasoning), a tool based on separation logic that is capable of reasoning automatically about...
  • Crowfoot

  • Referenced in 5 articles [sw07706]
  • Crowfoot’s assertion language, based on separation logic, features nested Hoare triples which describe...
  • coreStar

  • Referenced in 3 articles [sw18520]
  • coreStar: The Core of jStar. Separation logic is a promising approach to program verification. However ... provide basic support for developing separation logic tools. This paper shows how a language...
  • SDSAT

  • Referenced in 2 articles [sw00842]
  • Existing Separation Logic (a.k.a. Difference Logic, DL) solvers can be broadly classified as eager ... merits. We propose a novel Separation Logic Solver SDSAT that combines the strengths of both ... uniform adequate ranges for variables appearing in separation predicates. This phase is similar to previous ... smaller ranges for variables. Furthermore, the Separation Logic formula is not transformed into an equi...
  • Auto2_Imperative_HOL

  • Referenced in 2 articles [sw32246]
  • based on Imperative HOL and its separation logic framework. A major goal of this work ... functional programs and for working with separation logic...
  • PARLOG

  • Referenced in 39 articles [sw23764]
  • read as a sentence of predicate logic. It differs from PROLOG in incorporating parallel modes ... reasons of efficient implementation, it distinguishes and separates and- parallel and or-parallel evaluation. PARLOG ... introduction to PARLOG. It assumes familiarity with logic programming...
  • Hop

  • Referenced in 5 articles [sw22620]
  • charge of executing the logic of an application while the second one is in charge ... executing the graphical user interface. Hop separates the logic and the graphical user interface...
  • TSAT++

  • Referenced in 3 articles [sw21350]
  • presented, showing that TSAT++, instantiated for separation logic, is competitive with, or faster than, state...
  • Caper

  • Referenced in 2 articles [sw20269]
  • concurrency. Recent program logics based on separation logic emphasise a modular approach to proving functional...
  • Mechanized Semantic Library

  • Referenced in 5 articles [sw13123]
  • developing semantic models of program logics and type systems: separation algebras, permission share models, indirection ... clean axiomatization of step indexing), and modal logics. The library has a special emphasis...
  • DTRE

  • Referenced in 3 articles [sw22672]
  • Theories and interpretations provide a clean, logically based separation between types and their implementations; thus...
  • VST-Floyd

  • Referenced in 1 article [sw28118]
  • Floyd: a separation logic tool to verify correctness of C programs. The Verified Software Toolchain ... shallowly embedded higher-order separation Hoare logic which is proved sound in Coq with respect...
  • spock

  • Referenced in 5 articles [sw30413]
  • emerging logic-programming paradigm that strictly separates the description of a problem from its solving ... their programs. Unlike in other areas of logic programming, applying tracing techniques for debugging logic...
  • RLgraph

  • Referenced in 2 articles [sw31155]
  • communication patterns. We argue for the separation of logical component composition, backend graph definition...
  • CoALP

  • Referenced in 17 articles [sw16105]
  • derivations and parallelism, as execution of such logic programs can have both recursive and corecursive ... abstractly. The programming developments have often occurred separately and have usually been implementation-led. Here ... implementation of a new dialect, CoALP, of logic programming, characterised by guarded lazy corecursion...
  • DRAGO

  • Referenced in 3 articles [sw15032]
  • internally executed in each separate ontology. Using Distributed Description Logics as a formal framework...
  • CLAIRE

  • Referenced in 33 articles [sw02583]
  • imperative (functional) language. Although these paradigms are separately well known and are available under various ... inference compiler transforms a set of logical rules into a set of functions (demons that...
  • WALi-NWA

  • Referenced in 0 articles [sw33481]
  • portions of WALi are mostly logically separate from the rest of WALi, it does...