[1] Vania Joloboff, Jean-François Monin, and Xiaomu Shi. SimSoC: A Fast, Proven Faithful, Full System Virtual Prototyping Framework. In Anca Molnos and Christian Fabre, editors, Model-Implementation Fidelity in Cyber Physical System Design, pages 129--156. Springer, 2017. [ bib ]
[2] Vania Joloboff, Jean-François Monin, and Xiaomu Shi. Towards Verified Faithful Simulation. In Xuandong Li, Zhiming Liu, and Wang Yi, editors, Dependable Software Engineering: Theories, Tools, and Applications - First International Symposium, SETTA 2015, Nanjing, China, November 4-6, 2015, Proceedings, volume 9409 of Lecture Notes in Computer Science, pages 105--119. Springer, 2015. [ bib | .pdf ]
This paper presents an approach to construct a verified virtual prototyping framework of embedded software. The machine code executed on a simulated target architecture can be proven to provide the same results as the real hardware, and the proof is verified with a theorem prover. The method consists in proving each instruction of the instruction set independently, by proving that the execution of the C code simulating an instruction yields an identical result to that obtained by a formal executable model of the processor architecture. This formal model itself is obtained through an automated translation process from the architecture specifications. Each independent proof draws a number of lemmas from a generic lemma library and also uses the automation of inversion tactics in the theorem prover. The paper presents the proof of the ARM architecture version 6 Instruction Set Simulator of the SimSoC open source simulator, with all of the proofs being verified by the Coq proof assistant, using automated tactics to reduce manual proof development.

[3] Jean-François Monin and Xiaomu Shi. Handcrafted Inversions Made Operational on Operational Semantics. In S. Blazy, C. Paulin, and D. Pichardie, editors, ITP 2013, volume 7998 of LNCS, pages 338--353, Rennes, France, July 2013. Springer. [ bib | .pdf ]
When reasoning on formulas involving large-size inductively defined relations, such as the semantics of a real programming language, many steps require the inversion of a hypothesis. The built-in “inversion” tactic of Coq can then be used, but it suffers from severe controllability, maintenance and efficiency issues, which makes it unusable in practice in large applications. To circumvent this issue, we propose a proof technique based on the combination of an antidiagonal argument and the impredicative encoding of inductive data-structures. We can then encode suitable helper tactics in LTac, yielding scripts which are much shorter (as well as corresponding proof terms) and, more importantly, much more robust against changes in version changes in the background software. This is illustrated on correctness proofs of non-trivial C programs according to the operational semantics of C defined in CompCert.

[4] Meixian Chen and Jean-François Monin. Formal Verification of Netlog Protocols. In Tiziana Margaria, Zongyan Qiu, and Hongli Yang, editors, Sixth International Symposium on Theoretical Aspects of Software Engineering, TASE 2012, 4-6 July 2012, Beijing, China, pages 43--50. IEEE, 2012. [ bib | .pdf ]
Data centric languages, such as recursive rule based languages, have been proposed to program distributed applications over networks. They greatly simplify the code, while still admitting efficient distributed execution, including on sensor networks. From previous work [discotec11], we know that they also provide a promising approach to another tough issue about distributed protocols: their formal verification. Indeed, we can take advantage of their data centric orientation, which allows us to explicitly handle global structures such as the topology of the network. We illustrate here our approach on two non-trivial protocols and discuss its Coq implementation.

[5] Xiaomu Shi, Jean-François Monin, Frédéric Tuong, and Frédéric Blanqui. First Steps towards the Certification of an ARM Simulator Using Compcert. In Jean-Pierre Jouannaud and Zhong Shao, editors, Certified Proofs and Programs - First International Conference, volume 7086 of LNCS, pages 346--361, Kenting, Taiwan, December 7-9 2011. Springer. [ bib | .pdf ]
The simulation of Systems-on-Chip (SoC) is nowadays a hot topic because, beyond providing many debugging facilities, it allows the development of dedicated software before the hardware is available. Low-consumption CPUs such as ARM play a central role in SoC. However, the effectiveness of simulation depends on the faithfulness of the simulator. To this effect, we propose here to prove significant parts of such a simulator, SimSoC. Basically, on one hand, we develop a Coq formal model of the ARM architecture while on the other hand, we consider a version of the simulator including components written in Compcert-C. Then we prove that the simulation of ARM operations, according to Compcert-C formal semantics, conforms to the expected formal model of ARM. Size issues are partly dealt with using automatic generation of significant parts of the Coq model and of SimSoC from the official textual definition of ARM. However, this is still a long-term project. We report here the current stage of our efforts and discuss in particular the use of Compcert-C in this framework.

[6] Yuxin Deng, Stéphane Grumbach, and Jean-François Monin. A Framework for Verifying Data-Centric Protocols. In R. Bruni and J. Dingel, editors, FMOODS/FORTE 2011, volume 6722 of LNCS, pages 106--120, Reykjavik, Iceland, June 6-9 2011. Springer. [ bib | .pdf ]
Data centric languages, such as recursive rule based languages, have been proposed to program distributed applications over networks. They simplify greatly the code, which is orders of magnitude shorter, much more declarative, while still admitting efficient distributed execution. We show that they also provide a promising approach to the verification of distributed protocols, thanks to their data centric orientation, which allows to explicitly handle global structures, such as the topology of the network, routing tables, trees, etc, as well as their properties. We consider a framework using an original formalization in the Coq proof assistant of a distributed computation model based on message passing with either synchronous or asynchronous behavior. The declarative rules of the Netlog language for specifying distributed protocols, as well as the virtual machines for evaluating these rules, are encoded in Coq as well. We consider as a case study tree protocols, and show how this framework enables us to formally verify them in both the asynchronous and synchronous setting.

[7] Yuxin Deng, Stéphane Grumbach, and Jean-François Monin. Verifying Declarative Netlog Protocols with Coq: a First Experiment. Research Report 7511, INRIA, 2011. [ bib | .pdf ]
Declarative languages, such as recursive rule based languages, have been proposed to program distributed applications over networks. It has been shown that they simplify greatly the code, while still offering efficient distributed execution. In this report, we show that moreover they provide a promising approach to the verification of distributed protocols. We consider the Netlog language and use the Coq proof assistant. We first formalize the distributed computation model based on message passing with either synchronous or asynchronous behavior. We then see how the declarative rules of the protocols can be simply encoded in Coq and we develop the machine embedded on each node of the network which evaluates the rules. This framework enables us to formally verify distributed protocols, as shown on a concrete case study, a spanning tree construction in both the asynchronous and synchronous setting.

[8] Frédéric Blanqui, Claude Helmstetter, Vania Joloboff, Jean-François Monin, and Xiaomu Shi. Designing a CPU model: from a pseudo-formal document to fast code. In Proceedings of the 3rd Workshop on Rapid Simulation and Performance Evaluation: Methods and Tools, Heraklion, Greece, January 2011. Best Paper Award. [ bib | .pdf ]
For validating low level embedded software, engineers use simulators that take the real binary as input. Like the real hardware, these full-system simulators are organized as a set of components. The main component is the CPU simulator (ISS), because it is the usual bottleneck for the simulation speed, and its development is a long and repetitive task. Previous work showed that an ISS can be generated from an Architecture Description Language (ADL). In the work reported in this paper, we generate a CPU simulator directly from the pseudo-formal descriptions of the reference manual. For each instruction, we extract the information describing its behavior, its binary encoding, and its assembly syntax. Next, after automatically applying many optimizations on the extracted information, we generate a SystemC/TLM ISS. We also generate tests for the decoder and a formal specification in Coq. Experiments show that the generated ISS is as fast and stable as our previous hand-written ISS.

[9] F. Blanqui, C. Helmstetter, V. Joloboff, J.-F. Monin, and X. Shi. SimSoC-Cert: a Certified Simulator for Systems on Chip. Draft, September 2010. [ bib | .pdf ]
The design and debugging of Systems-on-Chip using a hardware implementation is difficult and requires heavy material. Simulation is an interesting alternative approach, which is both more flexible and less expensive. SimSoC is a fast instruction set simulator for various ARM, PowerPC, and RISC-based architectures. However, speed involves tricky short-comings and design decisions, resulting in a complex software product. This makes the accuracy of the simulator a non-trivial question: there is a strong need to strengthen the confidence that simulations results match the expected accuracy. We therefore decided to certify SimSoC, that is, to formally prove in Coq the correctness of a significant part of this software. The present paper reports our first efforts in this direction, targeting the ARMv6 architecture.

[10] Jean-François Monin. Proof Trick: Small Inversions. In Yves Bertot, editor, Second Coq Workshop, Edinburgh Royaume-Uni, July 2010. [ bib | http | .pdf | .pdf ]
We show how an inductive hypothesis can be inverted with small proof terms, using just dependent elimination with a diagonal predicate. The technique works without any auxiliary type such as True, False, eq. It can also be used to discriminate, in some sense, the constructors of an inductive type of sort Prop in Coq.

[11] Yuxin Deng, Stephane Grumbach, and Jean-François Monin. Towards Verifying Declarative Netlog Protocols with Coq. Draft, June 2010. [ bib | http | .pdf ]
Declarative languages, such as recursive rule based languages, have been proposed to program distributed applications over networks. It has been shown that they simplify greatly the code, while still offering efficient distributed execution. In this paper, we show that moreover they provide a promising approach to the verification of distributed protocols. We choose the Netlog language and use the Coq proof assistant. We first formalize the distributed computation model based on message passing with either synchronous or asynchronous behavior. We then see how the declarative rules of the protocols can be simply encoded in Coq. Finally, we develop the machine embedded on each node of the network which evaluates the rules. This framework enables us to formally verify distributed declarative protocols, as sketched on a concrete example, a breadth-first search tree construction in a distributed network.

[12] Yuxin Deng and Jean-François Monin. Verifying self-stabilizing population protocols with Coq. In Jifeng HE, Michael Hinchey, and Xirong Ma, editors, 3rd IEEE International Symposium on Theoretical Aspects of Software Engineering, Tianjin, China, July 2009. [ bib | .pdf ]
Population protocols are an elegant model recently introduced for distributed algorithms running in large and unreliable networks of tiny mobile agents. Correctness proofs of such protocols involve subtle arguments on infinite sequences of events. We propose a general formalization of self-stabilizing population protocols with the Coq proof assistant. It is used in reasoning about a concrete protocol for leader election in complete graphs. The protocol is formally proved to be correct for networks of arbitrarily large size. To this end we develop an appropriate theory of infinite sequences, including results for reasoning on abstractions. In addition, we provide a constructive correctness proof for a leader election protocol in directed rings. An advantage of using a constructive setting is that we get more informative proofs on the scenarios that converge to the desired configurations.

[13] Jean-François Monin, Cristian Ene, and Michaël Périn. Gentzen-prawitz natural deduction as a teaching tool. CoRR, abs/0907.3599, 2009. [ bib | .pdf ]
[14] Jean-François Monin. Programmation. 2008. [ bib ]
[15] Jean-François Monin and Judicaël Courant. Proving Termination Using Dependent Types: the Case of Xor-Terms. In H. Nilsson, editor, Trends in Functional Programming 7, chapter 1, pages 1--18. Intellect, Bristol, UK / Chicago, USA, April 2007. [ bib | .ps | .pdf ]
We study a normalization function in an algebra of terms quotiented by an associative, commutative and involutive operator (logical xor). This study is motivated by the formal verification of cryptographic systems, where a normalization function for xor-terms turns out to play a key role. Such a function is easy to define using general recursion. However, as it is to be used in a type theoretic proof assistant, we also need a proof termination of this function. Instead of using a clever mixture of various rewriting orderings, we follow an approach involving the power of Type Theory with dependent types. The results are to be applied in the proof of the security API described in [17].

[16] Jean-François Monin and Philippe Chavin. Coq. In H. Habrias and M. Frappier, editors, Software Specification Methods, An Overview Using a Case Study, ISTE, chapter 16. Hermès Science, April 2006. [ bib | http ]
This chapter is an attempt to provide a formal specification which is as faithful as possible to the informal one and consistent. The features of Coq are powerful enough to make the specification both very abstract and executable. We construct mathematical structures or functions whenever possible, instead of specifying them with axioms. If the axiomatic way turns out better, we look for structures satisfying the axioms we need.

[17] Judicaël Courant and Jean-François Monin. Defending the bank with a proof assistant. In WITS 2006, Vienna, March 2006. In WITS proceedings. [ bib | .ps | .pdf ]
We show how the proof-assistant Coq helped us formally verify the security of an API. As far as we know, this is the first mathematical proof of security of an API. The API we verified is a fixed version of Bond's modelization of IBM's Common Cryptographic Architecture. We explain the methodology we followed, sketch our proof and explain the points the formal verification raised.

[18] Judicaël Courant, Jean-François Monin, and Yassine Lakhnech. Proof pearl: elementary inductive and integer-based proofs about balanced words. draft, 2006. [ bib | .ps | .pdf ]
Inductive characterizations of words containing the same number of 'a' and 'b' can easily be given. However, formally proving the completeness of some of them turns out to be trickier than one may expect. We discuss and compare two Coq developments relating such balanced words to their inductive characterizations. One is based on auxiliary inductive structures and elementary arguments. The other one is based on a discrete variant of the intermediate value theorem.

[19] Judicaël Courant and Jean-François Monin. Faire garder la banque par un Coq. In Actes des dix-septièmes journées francophones des langages applicatifs, pages 25 -- 39, January 2006. [ bib | .ps | .pdf ]
Nous décrivons comment Coq nous a permis de démontrer mathématiquement et formellement la sécurité d'une interface de programmation de sécurité. À notre connaissance il s'agit de la première démonstration mathématique de sécurité d'une interface de programmation. Nous présentons brièvement notre démonstration et expliquons les difficultés rencontrées lors du processus de formalisation.

[20] Jean-François Monin. Proof pearl: From concrete to functional unparsing. In K. Slind, A. Bunker, and G. Gopalakrishnan, editors, Theorem Proving in Higher Order Logics (17th International Conference on TPHOLs 2004), volume 3223 of LNCS, pages 217--224, Park City, Utah, USA, September 2004. Springer Verlag. [ bib | .ps | .pdf ]
We provide a proof that the elegant trick of Olivier Danvy for expressing printf-like functions without dependent types is correct, where formats are encoded by functional expressions in continuation-passing style. Our proof is formalized in the Calculus of Inductive Constructions. We stress a methodological point: when one proves equalities between functions, a common temptation is to introduce a comprehension axiom and then to prove that the considered functions are extensionally equal. Rather than weakening the result (and adding an axiom), we prefer to strenghten the inductive argumentation in order to stick to the intensional equality.

[21] Jean-François Monin. Formalisation of the Join-Calculus in Type Theory, booktitle = International Worshop on Formal Methods and Security. Nankin, May 2004. [ bib ]
Towards verifying mobile code, we choose to formalize an appropriate elementary model of concurrency in type theory (more precisely: the calculus of inductive constructions, CIC, implemented in the Coq proof assistant). The chosen process calculus is the Join-Calculus (JC) of Fournet, Gonthier and Levy. The latter can be seen as a variant of the pi-calculus of Milner, Parrow and Walker, with better locality properties. We use Coq for encoding a structural operational semantics of JC based on the reflexive chemical abstract machines model. Our formalisation uses the full power of inductive constructions and dependent types available in the underlying theory of Coq, in order to capture the reflexive features of JC.

[22] B. Bérard, L. Fribourg, F. Klay, and J-F. Monin. A compared study of two correctness proofs for the standardized algorithm of ABR conformance. Formal Methods in System Design, 22:59--86, January 2003. [ bib | .ps | .pdf ]
The ABR conformance protocol is a real-time program that controls data ow rates on ATM networks. A crucial part of this protocol is the dynamical computation of the expected rate of data cells. We present here a modelling of the corresponding program with its environment, using the notion of (parametric) timed automata. A fundamental property of the service provided by the protocol to the user is expressed in this framework and proved by two di erent methods. The rst proof relies on inductive invariants, and was originally veri ed using theorem- proving assistant Coq. The second proof is based on reachability analysis, and was obtained using model-checker HyTech. We explain and compare these two proofs in the uni ed framework of timed automata.

[23] J-F. Monin. Contribution aux méthodes formelles pour le logiciel. Mémoire d'habilitation à diriger des recherches, Université de Paris Sud, April 2002. [ bib | .ps | .pdf ]
[24] J-F. Monin. Understanding Formal Methods. Springer Verlag, 2002. Foreword by G. Huet, ISBN 1-85233-247-6. [ bib ]
This book is intended to help the student or the engineer who wants an introduction to formal techniques, as well as the practitioner who wishes to broaden her or his knowledge of this subject. It mainly aims at providing a synthetic view of the logical foundations of such techniques, with an emphasis on intuitive ideas, so that it can also be considered as a practical complement to classical introductory manuals to logic, which generally focus more detail on specific subjects (e.g. first-order logic), and to books dedicated to particular formal methods.

[25] J-F. Monin. Proving the correctness of the standardized algorithm for ABR conformance. Formal Methods in System Design, 17:221--243, December 2000. [ bib | .ps | .pdf ]
Conformance control for ATM cells is based on a real-time reactive algorithm which delivers a value depending on inputs from the network. This value must always fit with a well defined theoretical value. We present here the correctness proof of the algorithm standardized for the ATM transfer capability called ABR. The proof turned out to produce a key argument during the standardization process of ABR.

[26] P. Chavin and J-F. Monin. An Abstract and constructive specification in Coq. In Marc Frappier and Henri Habrias, editors, Software Specification Methods, FACIT, chapter 13. Springer Verlag, 2000. [ bib ]
[27] J-F. Monin and F. Klay. Correctness Proof of the Standardized Algorithm for ABR Conformance. In Jeannette Wing, Jim Woodcock, and Jim Davies, editors, FM'99 -- Formal Methods, volume 1708 of LNCS, pages 662--681. Springer Verlag, 1999. [ bib | .ps | .pdf ]
Conformance control for ATM cells is based on a real-time reactive algorithm which delivers a value depending on inputs from the network. This value must always agree with a well defined theoretical value. We present here the correctness proof of the algorithm standardized for the ATM transfer capability called ABR. The proof turned out a key argument during the standardization process of ABR.

[28] J-F. Monin. Proving a real time algorithm for ATM in Coq. In E. Gimenez and C. Paulin-Mohring, editors, Types for Proofs and Programs, volume 1512 of LNCS, pages 277--293. Springer Verlag, 1998. [ bib | .ps | .pdf ]
This paper presents the techniques used for proving, in the framework of type theory, the correctness of an algorithm recently standardized at ITU-T that handles time explicitly. The structure of the proof and its formalization in Coq are described, as well as the main tools which have been developed: an abstract model of “real-time” that makes no assumption on the nature of time and a way to actually find proofs employing transitivity, using only logical definitions and an existing tactic.

[29] J-F. Monin and J. Sifakis. Application des techniques formelles au logiciel, volume 20 of Arago, chapter II, Eléments de classification des méthodes formelles. OFTA, 1997. [ bib ]
[30] J-F. Monin. Exceptions considered harmless. Science of Computer Programming, 26:179--196, 1996. [ bib | .ps | .pdf ]
Program extraction is a well known technique for developing correct functional programs from a constructive proof of their specification. This paper shows how to deal with exceptions in such a framework. We propose a modular (and impredicative) formalization in the calculus of constructions and we illustrate the technique on three examples.

[31] J-F. Monin. Extracting Programs with Exceptions in an Impredicative Type System. In B. Möller, editor, Mathematics of Program Construction, volume 947 of LNCS. Springer Verlag, 1995. [ bib | .ps | .pdf ]
This paper is about exceptions handling using classical techniques of program extraction. We propose an impredicative formalization in the calculus of constructions and we illustrate the technique on two examples. The first one, though simple, allows us to experiment various techniques. The second one is an adaptation of a bigger algorithm previously developed in Coq by J. Rouyer, namely first order unification. Only small changes were needed in order to get a more efficient program from the original one.

[32] P. Bellot, J.-P. Cottin, and J-F. Monin. Développement et validation de logiciels. Méthodes formelles. Techniques de l'Ingénieur, (12):1--12, 1995. [ bib ]
[33] G. Doumenc and J-F. Monin. The parallel abstract machine : A common execution model for FDTs. In FME'93 : Industrial-Strength Formal Methods, volume 670 of LNCS. Springer Verlag, 1993. [ bib ]
We introduce a new execution model for implementing FDTs based on the reactive approach. In this model, called the PAM, systems are divided into several reactive entities communicating by an activation mechanism. This paper introduces the PAM approach and shows how different communication mechanisms such as asynchronous fifo in ESTELLE or multiple rendez-vous in LOTOS can be implemented. It then presents the analysis of an implementation of a transport protocol (CCITT T70).

[34] F. du Castel, editor. Les télécommunications. Roger Levrault Int., 1993. contribution au chapitre informatique. [ bib ]
[35] J-F. Monin. Real-size compiler writing using Prolog with arrows. In Koichi Furukawa, editor, Proceedings of the Eighth International Conference on Logic Programming, pages 188--201, Paris, France, 1991. The MIT Press. [ bib ]
Since the seminal paper of Colmerauer (1975) on metamorphosis grammars, Prolog has been recognised as a potentially interesting language for writing compilers. However very few real size compilers have been written in Prolog until now. We describe here such an experiment, called Veda, carried out at CNET since 1984, in which an Estelle compiler-simulator for protocol checking was successfully developed. We sketch the (to our knowledge original) techniques which were introduced in Veda for enhancing performances up to a usable level, while keeping clarity, flexibility and declarativity in the programming style. One of them, based on “arrows”, has applications in a class of problems independant from compilation.

[36] J-F. Monin. A compiler written in Prolog: the Véda experience. In Deransart, Lorho, and Maluszynski, editors, Programming Languages Implementation and Logic Programming, number 348 in LNCS, Orléans, 1989. Springer Verlag. [ bib ]
[37] R. Groz, M. Litime, J-F. Monin, M. Phalippou, C. Hervé, P. Riou, P. Cousin, and J. Le Compagnon. Elements of a C.A.S.E. environment for defining and generating test suites. In Int. Work. on Prot. Test Syst, Berlin, 1989. [ bib ]
[38] J-F. Monin. Programmation en logique et compilation de protocoles : le simulateur Véda. Thèse d'université, Université de Rennes I, January 1989. [ bib ]
[39] C. Jard, J-F. Monin, and R. Groz. Development of Veda, a Prototyping Tool for Distributed Algorithms. IEEE Transactions on Software Engineering, 14(3):339--352, March 1988. [ bib ]
The development of a simulator, called Veda, is described. Veda is a software tool to help designers in protocol modeling and validation. It is oriented towards the rapid prototyping of distributed algorithms. Algorithms are described using an ISO (International Organisation for Standardization) formal description technique, called Estelle. The development of Veda and its internal structure is presented, emphasizing the use of Prolog as a software engineering tool. Typical uses of Veda are discussed.

Keywords: Parallel Programming
[40] W. Zhang and J-F. Monin. Résultats et expériences sur un environnement de simulation pour l'évaluation de performances à partir d'Estelle. In R. Castanet and O. Rafiq, editors, Colloque Francophone sur l'Ingénierie des Protocoles, Bordeaux, 1988. [ bib ]
[41] J-M. Ayache, R. Groz, C. Jard, and J-F. Monin. Des outils pour Estelle : du prototype au poste industriel. In Journées francophones pour l'informatique, January 1987. Liège. [ bib ]
[42] C. Jard, R. Groz, and J-F. Monin. Véda: a software Simulator for the Validation of Protocol Specifications. In L. Csaba, K. Tarnay, and T. Szentivanyi, editors, COMNET'85, Computer Network Usage: Recent Experiences, Budapest, 1986. North Holland. [ bib ]
[43] C. Jard, J-F. Monin, and R. Groz. Experience in implementing X250 (a CCITT subset of Estelle). In M. Diaz, editor, IFIP Workshop V on Protocol Specification Testing and Verification. North Holland, 1986. [ bib ]
[44] M. Condillac. Prolog, fondements et applications. Dunod, 1986. rédacteur de deux chapitres. [ bib ]
[45] J-F. Monin. Terminaison distribuée et groupes commutatifs. In J-P. Verjus and G. Roucairol, editors, Parallélisme, communication et synchronisation. éditions du CNRS, 1985. [ bib ]
[46] J-F. Monin. écriture d'un compilateur réel en Prolog. In S. Bourgault and M. Dincbas, editors, Séminaire sur la programmation en logique, Plestin, 1984. [ bib ]

This file was generated by bibtex2html 1.98.