• Smallfoot

  • Referenced in 51 articles [sw09787]
  • Smallfoot: Modular automatic assertion checking with separation logic. Separation logic is a program logic ... tool for checking certain lightweight separation logic specifications. The assertions describe the shapes of data ... oriented toward novel aspects of separation logic, namely: avoidance of frame axioms (which say what...
  • Datalog

  • Referenced in 271 articles [sw20023]
  • beginning of logic programming, but it became prominent as a separate area around 1977 when...
  • VeriFast

  • Referenced in 48 articles [sw07705]
  • program verifier. This note describes a separation-logic-based approach for the specification and verification ... abstract representation of memory as a separation logic assertion. Folding or unfolding abstract predicate assertions...
  • HIP

  • Referenced in 20 articles [sw09786]
  • heap manipulating programs. HIP is a separation logic based automated verification system for a simple ... will construct a set of separation logic proof obligations in the form of formula implications ... which are sent to the SLEEK separation logic prover. SLEEK is a fully automatic prover ... separation logic with frame inferring capability...
  • cminor

  • Referenced in 19 articles [sw09739]
  • Separation Logic for Small-Step cminor. cminor is a mid-level imperative programming language; there ... reasoning and we have designed a Separation Logic for cminor. In this paper, we give ... checked proof of soundness of our Separation Logic. This is the first large-scale machine ... checked proof of a Separation Logic w.r.t. a small-step semantics. The work presented...
  • jStar

  • Referenced in 30 articles [sw11261]
  • symbolic execution and abstraction using separation logic. The proposed technology has been implemented...
  • Slide

  • Referenced in 15 articles [sw28542]
  • SLIDE - Separation Logic with Inductive Definitions. Automata-based entailment checking for Separation Logic with Inductive ... prototype tool for checking entailment in Separation Logic with user-provided inductive definitions of recursive...
  • URDME

  • Referenced in 20 articles [sw10400]
  • construction. The core simulation routines are logically separated from the model building interface and written...
  • Predator

  • Referenced in 16 articles [sw07396]
  • were originally inspired by works on separation logic with higher-order list predicates, but they...
  • Cyclist

  • Referenced in 14 articles [sw18519]
  • algorithms have been integrated, focusing on Separation Logic with inductively defined predicates. For information...
  • Charge!

  • Referenced in 8 articles [sw22731]
  • Charge! A framework for higher-order separation logic in Coq. We present a comprehensive ... shallow embedding of a higher-order separation logic for a subset of Java ... abstraction similar to pen-and-paper separation-logic proof outlines. In particular, the tactics allow...
  • Find

  • Referenced in 78 articles [sw21614]
  • intrusion of logical errors. The proof of termination is treated as a separate exercise. Finally...
  • Curry

  • Referenced in 40 articles [sw08981]
  • combine the currently separated research efforts of the functional and logic programming communities...
  • SOLA-VOF

  • Referenced in 39 articles [sw24125]
  • used for calculations involving two fluids separated by a sharp interface. In either case ... program. Its logical parts are isolated in separate subroutines, and numerous special features have been...
  • Separation Logic

  • Referenced in 6 articles [sw28549]
  • Separation Logic Framework for Imperative HOL. We provide a framework for separation-logic based correctness...
  • MONA

  • Referenced in 113 articles [sw06170]
  • reductions, DAGification, guided tree automata, three-valued logic, eager minimization, BDD-based automata representations ... quantify their respective effects by experimenting with separate versions of the MONA tool that...
  • VerCors

  • Referenced in 5 articles [sw11259]
  • VerCors project we use permission-based separation logic to reason about multithreaded Java programs ... discuss in particular how we use the logic to use different implementations of synchronisers ... Concretely, we illustrate how permission-based separation logic is suitable to verify functional correctness properties...
  • Mercury

  • Referenced in 64 articles [sw08333]
  • delivers efficiency far in excess of existing logic programming systems, and close to conventional programming ... large-scale program development, allowing modularity, separate compilation, and numerous optimization/time trade-offs...
  • 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...