• Matlab

  • Referenced in 8412 articles [sw00558]
  • traditional programming languages, such as C/C++ or Java™. You can use MATLAB for a range...
  • CPLEX

  • Referenced in 2153 articles [sw04082]
  • ILOG® CPLEX® offers C, C++, Java, .NET, and Python libraries that solve linear programming...
  • Coq

  • Referenced in 1388 articles [sw00161]
  • CompCert compiler certification project or Java Card EAL7 certification in industrial context), the formalization...
  • Python

  • Referenced in 558 articles [sw14460]
  • possible in languages such as C++ or Java. The language provides constructs intended to enable...
  • JML

  • Referenced in 179 articles [sw04597]
  • Java Modeling Language (JML) is a behavioral interface specification language that can be used ... specify the behavior of Java modules. It combines the design by contract approach of Eiffel...
  • Bandera

  • Referenced in 131 articles [sw07663]
  • model-check properties of concurrent Java software. The Bandera Tool Set is an integrated collection ... designed to facilitate experimentation with model-checking Java source code. Bandera takes as input Java ... values of variables and internal states of Java lock objects. par In this tutorial paper ... simple concurrent Java program to illustrate the functionality of the main components of Bandera...
  • Java PathFinder

  • Referenced in 112 articles [sw07658]
  • Model checking JAVA programs using JAVA PathFinder. The paper describes a translator called JAVA PATHFINDER ... which translates from JAVA to PROMELA, the modeling language of the SPIN model checker ... translates a given JAVA program into a PROMELA model, which then can be model checked ... using SPIN. The JAVA program may contain assertions, which are translated into similar assertions...
  • AspectJ

  • Referenced in 122 articles [sw04426]
  • aspect-oriented extension to the Java. AspectJ TM is a simple and practical aspect-oriented ... extension to Java TM . With just a few new constructs, AspectJ provides support for modular ... crosscutting implementation, comprising pointcuts, advice, and ordinary Java member declarations. AspectJ code is compiled into ... standard Java bytecode. Simple extensions to existing Java development environments make it possible to browse...
  • ESC/Java

  • Referenced in 131 articles [sw07217]
  • Extended Static Checker for Java version 2 (ESC/Java2) is a programming tool that attempts ... common run-time errors in JML-annotated Java programs by static analysis of the program...
  • Featherweight Java

  • Referenced in 78 articles [sw16204]
  • Featherweight Java: A minimal core calculus for Java and GJ. Several recent studies have introduced ... lightweight versions of Java: reduced languages in which complex features like threads and reflection ... assignment) to obtain a small calculus, Featherweight Java, for which rigorous proofs are not only ... possible but easy. Featherweight Java bears a similar relation to Java as the lambda-calculus...
  • CEC 05

  • Referenced in 147 articles [sw18811]
  • algorithms. The codes in Matlab, C and Java for them could be found...
  • KRAKATOA

  • Referenced in 78 articles [sw03159]
  • basic structure of an environment for proving JAVA programs annotated with JML specifications. Our method ... translator of our own, which reads the JAVA files and produces specifications ... representation of the JAVA semantics of the JAVA program into WHY’s input language...
  • KNITRO

  • Referenced in 134 articles [sw00490]
  • offers interfaces to C, C++, Fortran, Java, AMPL, AIMMS, GAMS, MPL, Mathematica, MATLAB Microsoft Excel...
  • SIMPLIFY

  • Referenced in 129 articles [sw04976]
  • Modula-3, and another checker for Java. The aim of ESC is to increase software...
  • MatrixMarket

  • Referenced in 116 articles [sw04020]
  • download and include in your applications, Java applets which will generate matrices in your...
  • Sat4j

  • Referenced in 60 articles [sw07283]
  • release 2.2 system description. Sat4j is a java library for solving boolean satisfaction and optimization ... Minimally Unsatisfiable Subset (MUS) problems. Being in Java, the promise ... solve those problems (a SAT solver in Java is about 3.25 times slower than ... featured, robust, user friendly, and to follow Java design guidelines and code conventions (checked using...
  • TAPENADE

  • Referenced in 99 articles [sw06598]
  • TAPENADE can be utilized as a server (JAVA servlet), which runs at INRIA Sophia-Antipolis...
  • Why3

  • Referenced in 93 articles [sw04438]
  • intermediate language for the verification of C, Java, or Ada programs. Why3 is a complete...
  • Eiffel

  • Referenced in 90 articles [sw03522]
  • Eiffel later found their way into Java, C#, and other languages. New language design ideas...