• Spec#

  • Referenced in 120 articles [sw04598]
  • language, the Spec# compiler, and the Boogie static program verifier. The language includes constructs ... compiler emits run-time checks to enforce these specifications, and the verifier can check...
  • MAC

  • Referenced in 1 article [sw32897]
  • verified static information-flow control library. The programming language Haskell plays a unique, privileged role ... control (IFC) research: it is able to enforce information security via libraries. Many state ... work, we focus on MAC, a statically-enforced IFC library for Haskell. In MAC, like...
  • session-ocaml

  • Referenced in 1 article [sw32937]
  • slots’ manipulated with lenses, which can statically enforce session linearity and delegations. We show applications...
  • Kilim

  • Referenced in 7 articles [sw20229]
  • demonstrate a static analysis built around isolation type qualifiers to enforce these constraints. Kilim comfortably...
  • SAFECode

  • Referenced in 4 articles [sw13323]
  • SAFECode: Enforcing Alias Analysis for Weakly Typed Languages. Static analysis of programs in weakly typed...
  • HLIO

  • Referenced in 3 articles [sw22611]
  • HLIO: mixing static and dynamic typing for information-flow control in Haskell. Information-Flow Control ... typically enforced via type systems and static analyses or via dynamic execution monitors...
  • Contract

  • Referenced in 3 articles [sw13677]
  • both documented and enforced. Contracts are more expressive than static types. If a contract...
  • PLURAL

  • Referenced in 2 articles [sw13787]
  • paper describes Plural, a tool to automatically enforce typestate-based protocols using permissions in Java ... annotations on methods and method parameters. A static flow analysis tracks permissions in code that...
  • Sage

  • Referenced in 3 articles [sw30073]
  • Sage programming language, which is designed to enforce precise interface specifications in a flexible manner ... checking for this expressive language is not statically decidable, Sage uses hybrid type checking, which...
  • Aletheia

  • Referenced in 1 article [sw34338]
  • general technique to refine the output of static security checkers. The key idea ... negligible factor (x 1.006). Other policies are enforced with a similarly high level of efficacy...
  • MorphDroid

  • Referenced in 1 article [sw34337]
  • solutions have been proposed to verify or enforce privacy policies. A key limitation of existing ... this paper, we present MorphDroid, a novel static analysis algorithm that verifies mobile applications against...
  • ANSYS

  • Referenced in 655 articles [sw00044]
  • ANSYS offers a comprehensive software suite that spans...
  • Gmsh

  • Referenced in 576 articles [sw00366]
  • Gmsh is a 3D finite element grid generator...
  • HSL

  • Referenced in 269 articles [sw00418]
  • HSL (formerly the Harwell Subroutine Library) is a...
  • FreeFem++

  • Referenced in 1037 articles [sw01436]
  • FreeFem++ is an implementation of a language dedicated...
  • BLAS

  • Referenced in 483 articles [sw03216]
  • Low-level utilities common to many mathematical software...
  • SPIN

  • Referenced in 709 articles [sw03455]
  • Spin is a popular open-source software tool...
  • PETSc

  • Referenced in 1148 articles [sw04012]
  • The Portable, Extensible Toolkit for Scientific Computation (PETSc...
  • Gurobi

  • Referenced in 501 articles [sw04105]
  • GUROBI OPTIMIZER: State of the Art Mathematical Programming...