
GRASShopper
 Referenced in 5 articles
[sw23304]
 properties. The logic supports mixing of separation logic and firstorder logic assertions, yielding expressive...

VeriStar
 Referenced in 3 articles
[sw09393]
 prover for a decidable subset of separation logic. Together with VeriSmall, a provedsound Smallfoot ... tightly integrated collection of machineverified program logics and compilers giving foundational correctness guarantees.par VeriStar ... entailment holds in a provedsound 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 orparallel 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...

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

spock
 Referenced in 5 articles
[sw30413]
 emerging logicprogramming 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 implementationled. 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...

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