Duality in specification languages: a lattice-theoretical approach, Acta Informatica, vol.27, issue.7, pp.583-625, 1990. ,
Relational Logic with Framing and Hypotheses, Foundations of Software Technology and Theoretical Computer Science (Leibniz International Proceedings in Informatics), vol.65, p.16, 2016. ,
Relational Verification Using Product Programs, International Conference on Formal Methods, vol.6664, pp.200-214, 2011. ,
Proving Pointer Programs in Hoare Logic, Mathematics of Program Construction, pp.102-126, 2000. ,
Hoare Logic and Games, 2018. ,
Méthodes et outils pour la spécification et la preuve de propriétés difficiles de programmes séquentiels, 2018. ,
Variations on the McCarthy's 91 Function, 2018. ,
Schorr-Waite Algorithm proved using a Ghost Monitor, 2018. ,
Deductive Verification via Ghost Debugging, 2018. ,
URL : https://hal.archives-ouvertes.fr/hal-01907894
Guarded commands, nondeterminacy and formal derivation of programs, Commun. ACM, vol.18, pp.453-457, 1975. ,
The Spirit of Ghost Code, Formal Methods in System Design, vol.48, pp.152-174, 2016. ,
Relational Program Reasoning Using Compiler IR, Journal of Automated Reasoning, vol.60, pp.337-363, 2018. ,
The Essence of Higher-Order Concurrent Separation Logic, 26th European Symposium on Programming Languages and Systems, vol.10201, pp.696-723, 2017. ,
URL : https://hal.archives-ouvertes.fr/hal-01633133
Dafny: An Automatic Program Verifier for Functional Correctness, LPAR-16, vol.6355, pp.348-370, 2010. ,
Synthesis of Strategies Using the Hoare Logic of Angelic and Demonic Nondeterminism, Logical Methods in Computer Science, vol.12, p.3, 2016. ,
Properties of programs and partial function logic, vol.5, pp.79-98, 1970. ,
Time Credits and Time Receipts in Iris, European Symposium on Programming (LNCS), Luís Caires, vol.11423, pp.3-29, 2019. ,
Hoare Logic for Realistically Modelled Machine Code, Tools and Algorithms for the Construction and Analysis of Systems, pp.568-582, 2007. ,
An efficient machine-independent procedure for garbage collection in various list structures, Commun. ACM, vol.10, pp.501-506, 1967. ,
A Higher-Order Logic for Concurrent Termination-Preserving Refinement, European Symposium on Programming (Lecture Notes in Computer Science), Hongseok Yang, vol.10201, pp.909-936, 2017. ,
, Local Reasoning about While-Loops. VS-Theory Workshop, 3rd Int. Conf. on Verified Software: Theories, Tools and Experiments, 2010.
Dynamic Logic for an Intermediate Language Verification, Interaction and Refinement, Ph.D. Dissertation. Karlsruhe Institute of Technology, pp.90-411691, 2013. ,
Relational Separation Logic, Theoretical Computer Science, vol.375, pp.308-334, 2007. ,