meta.yml

---
fullname: JMLCoq
shortname: jmlcoq
organization: coq-community
community: true
action: true
nix: true
coqdoc: false
dune: false

synopsis: >-
  Coq definition of the JML specification language
  and a verified runtime assertion checker for JML

description: |-
  A Coq formalization of the syntax and semantics of the
  Java-targeted JML specification language, along with a
  verified runtime assertion checker for JML.

publications:
- pub_url: https://www.research-collection.ethz.ch/handle/20.500.11850/44276
  pub_title: A formal definition of JML in Coq and its application to runtime assertion checking
  pub_doi: 10.3929/ethz-a-006680049
- pub_url: https://www.research-collection.ethz.ch/handle/20.500.11850/68882
  pub_title: A Formalization of JML in the Coq Proof System
  pub_doi: 10.3929/ethz-a-006903145

authors:
- name: Hermann Lehner
  initial: true
- name: David Pichardie
  initial: true
- name: Andreas Kägi
  initial: true

maintainers:
- name: Karl Palmskog
  nickname: palmskog

opam-file-maintainer: palmskog@gmail.com

opam-file-version: dev

license:
  fullname: MIT License
  identifier: MIT

supported_coq_versions:
  text: 8.10 or later
  opam: '{>= "8.10"}'

tested_coq_nix_versions:
- coq_version: 'master'

tested_coq_opam_versions:
- version: dev
- version: '8.19'
- version: '8.18'
- version: '8.17'
- version: '8.16'
- version: '8.15'
- version: '8.14'
- version: '8.13'
- version: '8.12'
- version: '8.11'
- version: '8.10'

namespace: JML

keywords:
- name: JML
- name: Java Modeling Language
- name: runtime verification

categories:
- name: Computer Science/Decision Procedures and Certified Algorithms/Correctness proofs of algorithms

documentation: |-
  ## Documentation

  More information about the formalization can be found on the
  [project website](http://jmlcoq.info).
---