Zobrazeno 1 - 4
of 4
pro vyhledávání: '"Mickaël Laurent"'
Publikováno v:
ACM SIGAda Ada Letters. 42:40-44
This paper describes several new features of the open-source model checker Kind 2. Its input language and model checking engines have been extended to allow users to model and reason about systems with machine integers. In addition, Kind 2 can now pr
Publikováno v:
Proceedings of the ACM on Programming Languages
Proceedings of the ACM on Programming Languages, ACM, 2022, 49th ACM SIGPLAN Symposium on Principles of Programming Languages, 6 (POPL), pp.75. ⟨10.1145/3498674⟩
Proceedings of the ACM on Programming Languages, 2022, 49th ACM SIGPLAN Symposium on Principles of Programming Languages, 6 (POPL), pp.75. ⟨10.1145/3498674⟩
Proceedings of the ACM on Programming Languages, ACM, 2022, 49th ACM SIGPLAN Symposium on Principles of Programming Languages, 6 (POPL), pp.75. ⟨10.1145/3498674⟩
Proceedings of the ACM on Programming Languages, 2022, 49th ACM SIGPLAN Symposium on Principles of Programming Languages, 6 (POPL), pp.75. ⟨10.1145/3498674⟩
We extend classic union and intersection type systems with a type-case construction and show that the combination of the union elimination rule of the former and the typing rules for type-cases of our extension encompasses occurrence typing . To appl
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::9d6d0123aac00b349d32fabd39fb9442
https://hal.archives-ouvertes.fr/hal-03426711/file/main.pdf
https://hal.archives-ouvertes.fr/hal-03426711/file/main.pdf
Publikováno v:
Formal Methods for Industrial Critical Systems ISBN: 9783030852474
FMICS
FMICS
We introduce two new major features of the open-source model checker Kind 2 which provide traceability information between specification and design elements such as assumptions, guarantees, or other behavioral constraints in synchronous reactive syst
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::f16ce180a6e7e213ceda5b90f6e7e824
https://doi.org/10.1007/978-3-030-85248-1_14
https://doi.org/10.1007/978-3-030-85248-1_14
Publikováno v:
Science of Computer Programming
Science of Computer Programming, 2022, 217 (102781), ⟨10.1016/j.scico.2022.102781⟩
Science of Computer Programming, 2022, 217 (102781), ⟨10.1016/j.scico.2022.102781⟩
International audience; We revisit occurrence typing, a technique to refine the type of variables occurring in type-cases and, thus, capturesome programming patterns used in untyped languages. Although occurrence typing was tied from its inceptionto