• Smallfoot

• Referenced in 52 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 283 articles [sw20023]
• beginning of logic programming, but it became prominent as a separate area around 1977 when...

• VeriFast

• Referenced in 57 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 27 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 32 articles [sw11261]
• symbolic execution and abstraction using separation logic. The proposed technology has been implemented...

• Slide

• Referenced in 19 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 25 articles [sw10400]
• construction. The core simulation routines are logically separated from the model building interface and written...

• Cyclist

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

• Predator

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

• Charge!

• Referenced in 9 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 85 articles [sw21614]
• intrusion of logical errors. The proof of termination is treated as a separate exercise. Finally...

• Curry

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

• SOLA-VOF

• Referenced in 43 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 7 articles [sw28549]
• Separation Logic Framework for Imperative HOL. We provide a framework for separation-logic based correctness...

• MONA

• Referenced in 127 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 6 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...

• Viper

• Referenced in 8 articles [sw15038]
• verification techniques based on first-order logic specifications has benefitted greatly from verification infrastructures such ... suited to verification techniques based on separation logic and other permission logics, because they...

• GRASShopper

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

• Mercury

• Referenced in 68 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...