
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 machinechecked proof of soundness of our Separation Logic. This ... scale machinechecked proof of a Separation Logic w.r.t. a smallstep 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 permissionbased 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 permissionbased separation logic is suitable to verify functional correctness properties...

Caper
 Referenced in 2 articles
[sw20269]
 verification for finegrained 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 objectbased 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 highlevel language and interactive...

MiniSat
 Referenced in 584 articles
[sw00577]
 An extensible SATsolver. MiniSat is a minimalistic...

nauty
 Referenced in 625 articles
[sw00611]
 graphtheoretic 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 generalpurpose 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...