package lstar-rocq

  1. Overview
  2. Docs
Formally-verified automata learning in Rocq

Install 

dune-project
 Dependency

github.com Readme Changelog Edit opam file Versions (3)

Authors

  1. C
    Charles Averill <charlesaverill20@gmail.com>

Maintainers

  1. C
    Charles Averill <charlesaverill20@gmail.com>

Sources

lstar-rocq-2.0.tbz
sha256=c0e054fc161cd19cbe5926074527d11be7d05f2ba2a642f4f17ec9451740d9d9
sha512=9ea8383a8632fc12a6e3993d91a8f696ea3daf704628037250c8af7e315112a9557608348332f194122b62711ed2a554c5500abe57b49e174ebf4d9974786dac

doc/CHANGES.html

v2.0

Breaking changes. Both L* and KV signatures have changed, requiring passing fuel in via the Teacher module rather than upon calling the learner loop. This arises from new guarantees about termination and minimality for both algorithms.

v1.0

Initial release