|
[*]
|
Cláudio Belo Lourenço, Denis Cousineau, Florian Faissole, Claude
Marché, David Mentré, and Hiroaki Inoue.
Automated verification of temporal properties of Ladder programs.
In Formal Methods for Industrial Critical Systems, volume 12863
of Lecture Notes in Computer Science, pages 21--38, 2021.
[ bib |
DOI |
full text on HAL ]
|
|
[*]
|
Benedikt Becker, Cláudio Belo Lourenço, and Claude Marché.
Explaining counterexamples with giant-step assertion checking.
In José Creissac Campos and Andrei Paskevich, editors, 6th
Workshop on Formal Integrated Development Environments (F-IDE 2021),
Electronic Proceedings in Theoretical Computer Science, May 2021.
[ bib |
DOI |
full text on HAL ]
|
|
[*]
|
Diego Diverio, Cláudio Belo Lourenço, and Claude Marché.
“You-Know-Why”: an early-stage prototype of a key server
developed using Why3.
In VerifyThis Long-term Challenge 2020: Proceedings of the
Online-Event, pages 4--7, Dublin, Ireland, April 2020. Karlsruhe Institute
of Technology.
[ bib |
DOI |
full text on HAL ]
|
|
[*]
|
Sylvain Dailler, David Hauzar, Claude Marché, and Yannick Moy.
Instrumenting a weakest precondition calculus for counterexample
generation.
Journal of Logical and Algebraic Methods in Programming,
99:97--113, 2018.
[ bib |
DOI |
full text on HAL ]
|
|
[*]
|
Sylvain Dailler, Claude Marché, and Yannick Moy.
Lightweight interactive proving inside an automatic program verifier.
In Proceedings of the Fourth Workshop on Formal Integrated
Development Environment, F-IDE, Oxford, UK, July 14, 2018, 2018.
[ bib |
full text on HAL ]
|
|
[*]
|
Clément Fumex, Claude Marché, and Yannick Moy.
Automating the verification of floating-point programs.
In Andrei Paskevich and Thomas Wies, editors, Verified Software:
Theories, Tools, and Experiments. Revised Selected Papers Presented at the
9th International Conference VSTTE, number 10712 in Lecture Notes in
Computer Science, Heidelberg, Germany, December 2017. Springer.
[ bib |
full text on HAL ]
|
|
[*]
|
Clément Fumex, Claire Dross, Jens Gerlach, and Claude Marché.
Specification and proof of high-level functional properties of
bit-level programs.
In Sanjai Rayadurgam and Oksana Tkachuk, editors, 8th NASA
Formal Methods Symposium, volume 9690 of Lecture Notes in Computer
Science, pages 291--306, Minneapolis, MN, USA, June 2016. Springer.
[ bib |
full text on HAL ]
|
|
[*]
|
François Bobot, Jean-Christophe Filliâtre, Claude Marché, and Andrei
Paskevich.
Let's verify this with Why3.
International Journal on Software Tools for Technology Transfer
(STTT), 17(6):709--727, 2015.
See also http://toccata.lri.fr/gallery/fm2012comp.en.html.
[ bib |
DOI |
full text on HAL ]
|