• Why3

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

  • Referenced in 30 articles [sw09906]
  • overview of the runtime verification tool Java PathExplorer. We present an overview of the Java ... PathExplorer runtime verification tool, in short referred to as JPAX. JPAX can monitor the execution ... Java program and check that it conforms with a set of user provided properties formulated ... specialized analysis, such as the temporal logic verification, the deadlock analysis and the data race...
  • jStar

  • Referenced in 32 articles [sw11261]
  • jStar: Towards practical verification for Java. In this paper we introduce a novel methodology ... Java programs which builds on recent theoretical developments in program verification: it combines the idea...
  • WhyML

  • Referenced in 28 articles [sw09709]
  • intermediate language for the verification of C, Java, or Ada programs. We demonstrate the benefits ... WhyML on non-trivial examples of program verification...
  • Java+ITP

  • Referenced in 8 articles [sw32259]
  • Java+ITP: A verification tool based on Hoare logic and algebraic semantics. Java ... verification of properties of a sequential imperative subset of the Java language. It is based ... reasoning in a Hoare logic for this Java fragment that we propose and prove correct ... translated into semantically equivalent first-order verification conditions (VCs) which are then sent to Maude...
  • OpenJML

  • Referenced in 6 articles [sw19841]
  • OpenJML: Software verification for Java 7 using JML, OpenJDK, and Eclipse. OpenJML is a tool ... checking code and specifications of Java programs. We describe our experience building the tool ... many advances in specification-based software verification. The implementation demonstrates the value of integrating specification ... software specification and verification and for small-scale studies on existing Java programs...
  • Cibai

  • Referenced in 4 articles [sw26821]
  • static analyzer for modular analysis and verification of Java classes. We introduce Cibai a generic ... interpretation for the modular analysis and verification of Java classes. We present the abstract semantics...
  • KeY

  • Referenced in 64 articles [sw09969]
  • integrate design, implementation, formal specification, and formal verification of object-oriented software as seamlessly ... first-order Dynamic Logic for Java with a user-friendly graphical interface. The project...
  • VeriCool

  • Referenced in 10 articles [sw09749]
  • approach to the automatic verification of concurrent Java-like programs. The cornerstone of the approach...
  • LARVA

  • Referenced in 7 articles [sw21408]
  • runtime monitoring of Java programs. The use of runtime verification, as a lightweight approach ... LARVA, for the runtime verification of real-time properties of Java programs. Properties...
  • LOOP

  • Referenced in 29 articles [sw10292]
  • specification language tailored to Java) classes into their semantics in higher order logic. It serves ... theorem prover in which the actual verification of the desired properties takes place. Also...
  • jContractor

  • Referenced in 10 articles [sw01488]
  • allowed to use unconstrained Java expressions, in addition to runtime verification they can perform additional...
  • AnBx

  • Referenced in 3 articles [sw27775]
  • AnBx Compiler and Java Code Generator: Security Protocols Specification, Verification and Implementation - Alice ... compiler for verification (requires the OFMC model-checker); Java code generator from AnBx ... Java; New AnBx-IDE available here (Eclipse plugin supporting the AnBx/AnB language and verification tools...
  • ProMoVer

  • Referenced in 4 articles [sw06738]
  • tool for fully automated procedure-modular verification of Java programs equipped with method-local ... natural instantiation of the modular verification paradigm, where correctness of global properties is relativized...
  • Rebeca

  • Referenced in 9 articles [sw09422]
  • Rebeca are used to introduce compositional verification, abstraction, symmetry and partial order reduction techniques ... object-based computational model, Java-like syntax, and set of verification tools make Rebeca...
  • JCML

  • Referenced in 2 articles [sw06406]
  • specification language for the runtime verification of Java card programs Java Card is a version ... improve the safety of Java Card applets concentrates on static verification methods. This work presents ... runtime verification approach based on design by contract to improve the safety of Java Card ... Java modelling language) and its implementation: a compiler that generates runtime verification code. We also...
  • JNuke

  • Referenced in 3 articles [sw28382]
  • framework for verification and model checking of Java programs. It is a novel combination...
  • Jahob

  • Referenced in 10 articles [sw12385]
  • verification system for programs written in a subset of Java. Using Jahob, developers can statically...
  • JKelloy

  • Referenced in 2 articles [sw09964]
  • structures. Several tools support Alloy specifications for Java programs. However, they can only check ... presents JKelloy, a tool for deductive verification of Java programs with Alloy specifications. It includes ... Java states, and two sets of calculus rules that (1) generate verification conditions in relational...
  • Omnibus

  • Referenced in 3 articles [sw04600]
  • supporting tool for integrating different assertion-based verification techniques. Omnibus is a new system ... superficially similar to Java but removes aspects that particularly complicate verification. Integrated support is provided ... verification. The language is supported by a prototype IDE with a type checker, Java code...