JML
From MaRDI portal
Cited in
(only showing first 100 items - show all)- A shared-variable concurrency analysis of multi-threaded object-oriented programs
- POSIX file store in Z/Eves: An experiment in the verified software repository
- A type safe state abstraction for coordination in JAVA-like languages
- Invariant based programming: Basic approach and teaching experiences
- Integration of verification methods for program systems
- Dafny
- HasCasl
- JMLUnit
- Valigator
- WSAT
- Modula
- Virginity
- Symstra
- POOC
- jContractor
- Ada95
- ArcAngel
- JavaFAN
- LARCH
- AGVI
- SCOOP
- TASC
- ECDAR
- SPARK
- KRAKATOA
- CLOS
- PVS
- Eiffel
- ACSL
- Daikon
- GeoSteiner
- Theory and methodology of assumption/commitment based system interface specification and architectural contracts
- Valgrind
- Why3
- Spec#
- Omnibus
- JACK
- Caduceus
- Frama-C
- Alt-Ergo
- SIMPLIFY
- Class invariants as abstract interpretation of trace semantics
- An assertion-based proof system for multithreaded Java
- Formal methods for smart cards: an experience report
- How the design of JML accommodates both runtime assertion checking and formal verification
- Understanding parameters of deductive verification: an empirical investigation of KeY
- CZT
- Compositionality for quantitative specifications
- Unifying separation logic and region logic to allow interoperability
- JCML
- Coalgebras and monads in the semantics of Java
- Executing formal specifications with concurrent constraint programming
- Casper
- UniTESK
- Weakest pre-condition reasoning for Java programs with JML annotations
- The KRAKATOA tool for certification of JAVA/JAVACARD programs annotated in JML
- Source code verification of a secure payment applet
- A behavioral type system and its application in Ptolemy II
- Bogor
- BPEL2PN
- ESC/Java
- VCC
- SANTE
- Korat
- JUnit
- Pex
- Rostra
- ATGen
- A formal approach to adaptive software: continuous assurance of non-functional requirements
- Assertion-based slicing and slice graphs
- The safety-critical Java memory model formalised
- Formal verification of numerical programs: from C annotated programs to mechanical proofs
- Chalice
- VeriFast
- Boogie
- JACK
- A relational shape abstract domain
- Verifying Whiley programs with Boogie
- Motras
- Creol
- Alcoa
- Gray-box monitoring of hyperproperties with an application to privacy
- Traits: correctness-by-construction for free
- WhyML
- VeriCool
- MIO Workbench
- Smallfoot
- GENA
- ASPIER
- dSPIN
- iJulienne
- Web-TLR
- JPAX
- Spi2Java
- KeY
- KIV
- Anima
- Z/EVES
- Z
- LOOP
This page was built for software: JML
