• JTLV

  • Referenced in 8 articles [sw08859]
  • Integrated Developer Environment for algorithmic verification applications. Jtlv may be viewed ... much enhanced Tlv [18], with Java rather than Tlv-basic as the scripting language. JTLV ... facilitates a rich, common, and abstract verification developer environment that is implemented as an Eclipse...
  • jMocha

  • Referenced in 4 articles [sw24777]
  • model checking, and the model checker jMocha (Java MOdel-CHecking Algorithm) is based on this ... interactive software environment for specification, simulation and verification, and is intended as a vehicle ... development of new verification algorithms and approaches. It is written in Java and uses native ... message sequence chart fashion; (3) requirements verification both by symbolic and enumerative model checking...
  • Joogie

  • Referenced in 4 articles [sw13771]
  • Joogie: From java through jimple to boogie. Recently, software verification is being used to prove ... assistance to the compiler optimization. Compared to verification of correctness properties, the translation from source ... this paper, we present a translation of Java into logic that is suitable for proving...
  • Uppaal2k

  • Referenced in 43 articles [sw01595]
  • integrated tool environment for modeling, simulation and verification of real-time systems, developed jointly ... client/server application implemented in Java and C++, and is currently available for Linux, SunOS ... Uppaal2k. A model-checker for automatic verification of safety and bonded-liveness properties by reachability...
  • Jass

  • Referenced in 11 articles [sw32265]
  • compiler that translates annotated into pure Java programs in which compliance with the specification ... Contract features known from classical program verification (e.g. pre- and postconditions, invariants), Jass additionally supports...
  • VerCors

  • Referenced in 7 articles [sw11259]
  • concurrent software. It first discusses why verification of concurrent software is important, but also challenging ... based separation logic to reason about multithreaded Java programs. We discuss in particular ... different implementations of synchronisers in verification, and how we reason about class invariance properties...
  • JVer

  • Referenced in 1 article [sw25426]
  • describe JVer, a tool for verifying Java bytecode programs annotated with pre and post conditions ... except that: (1) it produces verification conditions for Java bytecode, not Java source ... aliasing and heap modification; (3) it produces verification conditions directly using symbolic simulation, without...
  • JACK

  • Referenced in 7 articles [sw07878]
  • inspect the generated proof obligations in a Java syntax, and to trace them back ... support for annotation generation, and for interactive verification. The whole platform works both for source...
  • MOPBox

  • Referenced in 1 article [sw33222]
  • library-based approach to runtime verification. MOPBox is a Java library for defining and evaluating...
  • Codecharts

  • Referenced in 2 articles [sw09151]
  • design verification}, a process of proving or refuting that a Java program (i.e. its native ... well as a fully-automated design verification tool. We conclude with empirical results which suggest...
  • GraVy

  • Referenced in 2 articles [sw34340]
  • propose a gradual verification approach, GraVy. For a given piece of Java code, GraVy partitions...
  • CoMA

  • Referenced in 4 articles [sw06745]
  • technique we propose makes use of Java annotations, which link the concrete implementation ... reuse of specifications for other purposes (formal verification, simulation, model-based testing...
  • Java-MaC

  • Referenced in 11 articles [sw20000]
  • Monitoring and Checking (MaC) architecture for Java programs. The MaC architecture provides assurance that ... time. MaC bridges the gap between formal verification, which ensures the correctness of a design ... architecture and a prototype implementation Java...
  • KeY-C

  • Referenced in 5 articles [sw00486]
  • present KeY-C, a tool for deductive verification of C programs. KeY-C allows ... version of KeY that supports Java Card. In this paper we give a glimpse...
  • JBMC

  • Referenced in 2 articles [sw25908]
  • Java programs. It checks runtime exceptions and user-definded assertions. The verification is performed...
  • BicolanoMT

  • Referenced in 3 articles [sw28593]
  • sequential bytecode supported by the CLDC (Java for mobile phones) platform. We use a special ... developed to be suited for program verification and static analysis...
  • ESC4

  • Referenced in 2 articles [sw07219]
  • Java modeling language Extended Static Checking (ESC) is a fully automated formal verification technique. Verification...
  • Snugglebug

  • Referenced in 7 articles [sw13707]
  • foundation for bug-finding, specification inference, verification, and test generation. This paper addresses demand-driven ... techniques were critical for successfully analyzing large Java applications...
  • AGVI

  • Referenced in 4 articles [sw02287]
  • implemented a toolkit AGVI, Automatic Generation, Verification, and Implementation of Security Protocols. With AGVI ... protocols and implement the protocols in Java. Our experiments have successfully generated new and even...
  • DynaMate

  • Referenced in 2 articles [sw14286]
  • inferring loop invariants for automatic full functional verification. DYNAMATE is a tool that automatically infers ... loop invariants and uses them to prove Java programs correct with respect to a given...