- Referenced in 53 articles
- oriented toward novel aspects of separation logic, namely: avoidance of frame axioms (which say what ... presence of pointers; and modular reasoning about concurrent programs...
- Referenced in 19 articles
- 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...
- Referenced in 7 articles
- 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...
- Referenced in 2 articles
- verification for fine-grained concurrency. Recent program logics based on separation logic emphasise a modular...
- Referenced in 1906 articles
- Coq is a formal proof management system. It...
- Referenced in 74 articles
- Dafny is an imperative object-based language with...
- Referenced in 3221 articles
- GAP is a system for computational discrete algebra...
- Referenced in 719 articles
- Isabelle is a generic proof assistant. It allows...
- Referenced in 264 articles
- In the core computer science areas -- data structures...
- Referenced in 5403 articles
- The result of over 30 years of cutting...
- Referenced in 13702 articles
- MATLAB® is a high-level language and interactive...
- Referenced in 584 articles
- An extensible SAT-solver. MiniSat is a minimalistic...
- Referenced in 625 articles
- graph-theoretic program NAUTY: nauty is a program...
- Referenced in 64 articles
- Nitpick is a counterexample generator for Isabelle/HOL that...
- Referenced in 10196 articles
- R is a language and environment for statistical...
- Referenced in 958 articles
- AUTO is a software for continuation and bifurcation...
- Referenced in 454 articles
- PRISM: Probabilistic symbolic model checker. In this paper...
- Referenced in 524 articles
- ML (’Meta Language’) is a general-purpose functional...
- Referenced in 93 articles
- Graphviz is open source graph visualization software. Graph...
- Referenced in 92 articles
- VeriSoft automatically searches for coordination problems (deadlocks, etc...