Modular verification of programs with effects and effects handlers

Autor: Thomas Letan, Pierre Chifflier, Guillaume Hiet, Yann Régis-Gianas

Publikováno v: Formal Aspects of Computing
Formal Aspects of Computing, Springer Verlag, 2020, ⟨10.1007/s00165-020-00523-2⟩
Formal Aspects of Computing, 2020, ⟨10.1007/s00165-020-00523-2⟩

Modern computing systems have grown in complexity, and even though system components are generally carefully designed and even verified by different groups of people, thecompositionof these components is often regarded with less attention. Inconsiste

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::b264ca4e934c763c499602cdbbc52edd
https://hal.archives-ouvertes.fr/hal-03107526

Analysing installation scenarios of Debian packages

Autor: Mihaela Sighireanu, Nicolas Jeannerod, Claude Marché, Ralf Treinen, Yann Régis-Gianas, Benedikt Becker

Publikováno v: Tools and Algorithms for the Construction and Analysis of Systems ISBN: 9783030452360
TACAS (2)
Tools and Algorithms for the Construction and Analysis of Systems
TACAS 2020-26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems
TACAS 2020-26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Apr 2020, The conference took place on-line, because it couldn't be held in Dublin, Ireland. pp.235-253, ⟨10.1007/978-3-030-45237-7_14⟩

The Debian distribution includes more than 28 thousand maintainer scripts, almost all of them are written in Posix shell. These scripts are executed with root privileges at installation, update, and removal of a package, which make them critical for

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::83781a0aa95ff8ec80f03f0f0b2d4b88
https://doi.org/10.1007/978-3-030-45237-7_14

Morbig: A Static parser for POSIX shell

Autor: Ralf Treinen, Nicolas Jeannerod, Yann Régis-Gianas

Publikováno v: Journal of Computer Languages. 57:100944

The POSIX shell language defies conventional wisdom of compiler construction on several levels: The shell language was not designed for static parsing, but with an intertwining of syntactic analysis and execution by expansion in mind. Token recogniti

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::bcc4e99eef6741abc5514b3a456a63b7
https://doi.org/10.1016/j.cola.2020.100944

Modular Verification of Programs with Effects and Effect Handlers in Coq

Autor: Thomas Letan, Yann Régis-Gianas, Pierre Chifflier, Guillaume Hiet

Publikováno v: FM 2018-22nd International Symposium on Formal Methods
FM 2018-22nd International Symposium on Formal Methods, Jul 2018, Oxford, United Kingdom. pp.338-354, ⟨10.1007/978-3-319-95582-7_20⟩
Formal Methods ISBN: 9783319955810
FM

International audience; Modern computing systems have grown in complexity, and the attack surface has increased accordingly. Even though system components are generally carefully designed and even verified by different groups of people, the compositi

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::7df59d78375118733e8b73e32abe6961
https://hal.inria.fr/hal-01799712

Mtac2: Typed tactics for backward reasoning in Coq

Autor: Yann Régis-Gianas, Derek Dreyer, Robbert Krebbers, Beta Ziliani, Jan-Oliver Kaiser

Publikováno v: Proceedings of the ACM on Programming Languages, 2(ICFP)
Proceedings of the ACM on Programming Languages
Proceedings of the ACM on Programming Languages, ACM, 2018, 2 (ICFP), pp.1-31. ⟨10.1145/3236773⟩
Proceedings of the ACM on Programming Languages, 2018, 2 (ICFP), pp.1-31. ⟨10.1145/3236773⟩

Coq supports a range of built-in tactics, which are engineered primarily to support backward reasoning . Starting from a desired goal, the Coq programmer can use these tactics to manipulate the proof state interactively, applying axioms or lemmas to

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::f04fcf8e3d307d4d94952473d2a99a8d
http://resolver.tudelft.nl/uuid:76e4c827-24ae-45c5-a57f-f902a6011fd8