JML
From MaRDI portal
Cited in
(only showing first 100 items - show all)- KeY: A Formal Method for Object-Oriented Systems
- POSIX file store in Z/Eves: An experiment in the verified software repository
- Verification conditions for source-level imperative programs
- A dynamic logic for deductive verification of multi-threaded programs
- A syntax-directed Hoare logic for object-oriented programming concepts.
- Verification of object-oriented programs: a transformational approach
- Formalizing a hierarchical file system
- Verification of distributed systems with local-global predicates
- Contract-based verification of MATLAB-style matrix programs
- FeatherTrait
- Lazy behavioral subtyping
- Tools and Algorithms for the Construction and Analysis of Systems
- Automated verification of shape, size and bag properties via user-defined predicates in separation logic
- Verification of concurrent systems with VerCors
- Many-Valued Logic, Partiality, and Abstraction in Formal Specification Languages
- Featherweight Jigsaw. Replacing inheritance by composition in Java-like languages
- Modular specification and verification of object-oriented programs
- Algebraic Methodology and Software Technology
- Verification of software product lines with delta-oriented slicing
- Hoare logic for Java in Isabelle/HOL
- Programming Languages and Systems
- Specification and runtime verification of Java card programs
- CodeSurfer
- EventB2Dafny
- NAT2TEST
- Incremental reasoning with lazy behavioral subtyping for multiple inheritance
- Grail
- coreStar
- Atoment
- Java Jr
- Splint
- Houdini
- OpenJML
- JFlow
- C-Light
- Verasco
- LARVA
- MarQ
- OSMOSE
- StaRVOOrS
- Charge!
- Jessie
- Chianti
- JavaSPI
- MJ
- DeltaJ
- ASMKeY
- JBMC
- CIL
- Cibai
- DarwinSPL
- DeltaEcore
- JOANA
- SCCharts
- SCEst
- Camelot
- SPL Conqueror
- TAME
- MetaFJig
- AutoProof
- ZKPDL
- AGEDIS
- Jass
- PQL
- AO4BPEL
- UNITS
- Sather
- An assertion-based proof system for multithreaded Java
- AddressSanitizer
- ANNA
- KERNELC
- CCCC
- Abstract Certification of Global Non-interference in Rewriting Logic
- A Realizability Model for Impredicative Hoare Type Theory
- The KRAKATOA tool for certification of JAVA/JAVACARD programs annotated in JML
- Weakest pre-condition reasoning for Java programs with JML annotations
- Specification and verification challenges for sequential object-oriented programs
- Verifying traits: an incremental proof system for fine-grained reuse
- Invariant based programming: Basic approach and teaching experiences
- Fundamentals of software engineering. 6th international conference, FSEN 2015, Tehran, Iran, April 22--24, 2015. Revised selected papers
- Coalgebras and monads in the semantics of Java
- Monitoring and recovery for web service applications
- A Sound and Complete Shared-Variable Concurrency Model for Multi-threaded Java Programs
- Hoare type theory, polymorphism and separation
- An observationally complete program logic for imperative higher-order functions
- scientific article; zbMATH DE number 1693527 (Why is no real title available?)
- Modular invariants for layered object structures
- Extending Model Checking with Dynamic Analysis
- Integration of verification methods for program systems
- Theorem Proving in Higher Order Logics
- scientific article; zbMATH DE number 1670561 (Why is no real title available?)
- Programming Languages and Systems
- Stepwise Development of Simulink Models Using the Refinement Calculus Framework
- The safety-critical Java memory model formalised
- Algebraic Methodology and Software Technology
- Integrating a formal method into a software engineering process with UML and Java
- scientific article; zbMATH DE number 2090132 (Why is no real title available?)
- Formal methods for smart cards: an experience report
- Refinement checking on parametric modal transition systems
- Method redefinition-ensuring alternative behaviors
This page was built for software: JML
