• Smallfoot

  • Referenced in 53 articles [sw09787]
  • oriented toward novel aspects of separation logic, namely: avoidance of frame axioms (which say what ... presence of pointers; and modular reasoning about concurrent programs...
  • cminor

  • Referenced in 19 articles [sw09739]
  • reasoning and we have designed a Separation Logic for cminor. In this paper, we give ... concurrent extensions. We detail a machine-checked proof of soundness of our Separation Logic. This ... scale machine-checked proof of a Separation Logic w.r.t. a small-step semantics. The work ... environment in which concurrent cminor programs can be verified using Separation Logic and also compiled...
  • VerCors

  • Referenced in 7 articles [sw11259]
  • software. It first discusses why verification of concurrent software is important, but also challenging. Then ... 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...
  • Caper

  • Referenced in 2 articles [sw20269]
  • verification for fine-grained concurrency. Recent program logics based on separation logic emphasise a modular...
  • Coq

  • Referenced in 1906 articles [sw00161]
  • Coq is a formal proof management system. It...
  • Dafny

  • Referenced in 74 articles [sw00183]
  • Dafny is an imperative object-based language with...
  • GAP

  • Referenced in 3221 articles [sw00320]
  • GAP is a system for computational discrete algebra...
  • Isabelle

  • Referenced in 719 articles [sw00454]
  • Isabelle is a generic proof assistant. It allows...
  • LEDA

  • Referenced in 264 articles [sw00509]
  • In the core computer science areas -- data structures...
  • Maple

  • Referenced in 5403 articles [sw00545]
  • The result of over 30 years of cutting...
  • Matlab

  • Referenced in 13702 articles [sw00558]
  • MATLAB® is a high-level language and interactive...
  • MiniSat

  • Referenced in 584 articles [sw00577]
  • An extensible SAT-solver. MiniSat is a minimalistic...
  • nauty

  • Referenced in 625 articles [sw00611]
  • graph-theoretic program NAUTY: nauty is a program...
  • Nitpick

  • Referenced in 64 articles [sw00622]
  • Nitpick is a counterexample generator for Isabelle/HOL that...
  • R

  • Referenced in 10196 articles [sw00771]
  • R is a language and environment for statistical...
  • AUTO

  • Referenced in 958 articles [sw01059]
  • AUTO is a software for continuation and bifurcation...
  • PRISM

  • Referenced in 454 articles [sw01186]
  • PRISM: Probabilistic symbolic model checker. In this paper...
  • ML

  • Referenced in 524 articles [sw01218]
  • ML (’Meta Language’) is a general-purpose functional...
  • Graphviz

  • Referenced in 93 articles [sw01283]
  • Graphviz is open source graph visualization software. Graph...
  • veriSoft

  • Referenced in 92 articles [sw01489]
  • VeriSoft automatically searches for coordination problems (deadlocks, etc...