Bibliography

Major publications by the team in recent years

1F. Blanqui.

Definitions by rewriting in the Calculus of Constructions, in: Mathematical Structures in Computer Science, 2005, vol. 15, n^o 1, p. 37-92, Journal version of LICS'01. [ DOI : 10.1017/S0960129504004426 ]

http://hal.inria.fr/inria-00105648/en/
2F. Blanqui, C. Helmstetter, V. Joloboff, J.-F. Monin, X. Shi.

Designing a CPU model: from a pseudo-formal document to fast code, in: 3rd Workshop on: Rapid Simulation and Performance Evaluation: Methods and Tools, Grèce Heraklion, 2010, Best paper award.

http://hal.inria.fr/inria-00546228/en/
3F. Blanqui, A. Koprowski.

CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates, in: Mathematical Structures in Computer Science, 2011, vol. 21, n^o 4, p. 827-859.

http://hal.inria.fr/inria-00543157/en/
4F. Blanqui, J.-P. Jouannaud, P.-Y. Strub.

From formal proofs to mathematical proofs: a safe, incremental way for building in first-order decision procedures, in: 5th IFIP International Conference on Theoretical Computer Science - TCS 2008, Milan Italie, IFIP, 2008, vol. 273. [ DOI : 10.1007/978-0-387-09680-3_24 ]

http://hal.inria.fr/inria-00275382/en/
5B. Bérard, L. Fribourg, F. Klay, J.-F. Monin.

A compared study of two correctness proofs for the standardized algorithm of ABR conformance, in: Formal Methods in System Design, january 2003.
6B. Delsart, V. Joloboff, E. Paire.

JCOD: A Lightweight Modular Compilation Technology for Embedded Java, in: Second International Conference on Embedded Software, Lecture Notes in Computer Science, Springer-Verlag, 2002, vol. 2491, p. 197–212, ISBN 3-540-44307-X.
7F. He, X. Song, M. Gu, J. Sun.

Heuristic-Guided Abstraction Refinement, in: Computer Journal, May 2009, vol. 52, n^o 3, p. 280-287.
8J.-P. Jouannaud, A. Rubio.

Polymorphic Higher-Order Recursive Path Orderings, in: Journal of the ACM, 2007, vol. 54, n^o 1, p. 1-48.
9Y. Jung, S. Kong, B.-Y. Wang, K. Yi.

Deriving Invariants by Algorithmic Learning, Decision Procedures, and Predicate Abstraction, in: Verification, Model Checking, and Abstract Interpretation, Madrid, Spain, January 2010.

http://hal.inria.fr/inria-00517257/en/
10Y.-K. Tsay, B.-Y. Wang.

Automated Compositional Reasoning of Intuitionistically Closed Regular Properties, in: International Journal on Foundation of Computer Science, 2009, vol. 20, n^o 4, p. 747-762.

Publications of the year

Articles in International Peer-Reviewed Journal

11F. Blanqui, A. Koprowski.

CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates, in: Mathematical Structures in Computer Science, 2011, vol. 21, n^o 4, p. 827-859. [ DOI : 10.1017/S0960129511000120 ]

http://hal.inria.fr/inria-00543157/en
12S. Suzuki, K. Kusakari, F. Blanqui.

Argument filterings and usable rules in higher-order rewrite systems, in: IPSJ Transactions on Programming, March 2011, vol. 4, n^o 2, p. 1-12.

http://hal.inria.fr/inria-00555008/en
13H. Wan, C. Gang, X. Song, M. Gu.

Formalisation and verification of programmable logic controllers timers in Coq, in: IET Software, February 2011.

http://hal.inria.fr/inria-00612410/en
14R. Wang, X. Song, J. Zhu, M. Gu.

Formal modeling and synthesis of programmable logic controllers, in: Computers in Industry, January 2011.

http://hal.inria.fr/inria-00612411/en
15L. Xiao, M. Gu, J. Sun.

The Denotational Semantics Definition of PLC Programs Based on Extended $λ$ -Calculus, in: Communications in Computer and Information Science, July 2011, vol. 176(II), n^o 40-46.

http://hal.inria.fr/inria-00612409/en

Articles in National Peer-Reviewed Journal

16L. Xiao, M. Gu, J. Sun.

A Formal Definition Method of Denotational Semantics and Functions for PLC Program Language, in: Journal of Central South University (in Chinese), July 2011.

http://hal.inria.fr/inria-00612407/en

International Conferences with Proceedings

17B. Barras, J.-P. Jouannaud, P.-Y. Strub, Q. Wang.

CoqMTU: a higher-order type theory with a predicative hierarchy of universes parametrized by a decidable first-order theory, in: Twenty-Sixth Annual IEEE Symposium on "Logic in Computer Science" - LICS 2011, Toronto, Canada, 2011.

http://hal.inria.fr/inria-00583136/en
18J. O. Blech, S. Ould Biha.

Verification of PLC Properties Based on Formal Semantics in Coq, in: International Conference on Software Engineering and Formal Methods, SEFM 2011, Montevideo, Uruguay, June 2011.

http://hal.inria.fr/inria-00601907/en
19Y. Deng, S. Grumbach, J.-F. Monin.

A Framework for Verifying Data-Centric Protocols, in: DisCoTec 2011 - 6th International Federated Conferences on Formal Techniques for Distributed Systems, Reykjavik, Iceland, R. Bruni, J. Dingel (editors), Lecture Notes in Computer Science, Springer, December 2011, vol. 6722, p. 106-120. [ DOI : 10.1007/978-3-642-21461-5_7 ]

http://hal.inria.fr/hal-00647802/en
20V. Joloboff, X. Zhou, C. Helmstetter, X. Gao.

Fast Instruction Set Simulation Using LLVM-based Dynamic Translation, in: International MultiConference of Engineers and Computer Scientists 2011, Hong Kong, China, Springer, July 2011, vol. 2188, p. 212-216.

http://hal.inria.fr/hal-00646947/en
21Y. Jung, W. Lee, B.-Y. Wang, K. Yi.

Predicate Generation for Learning-Based Quantifier-Free Loop Invariant Inference, in: TACAS 2011 - Seventeenth International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Saarbruecken, Germany, Lecture Notes in Computer Science, Springer, March 2011, vol. 6605, p. 205-219. [ DOI : 10.1007/978-3-642-19835-9 ]

http://hal.inria.fr/hal-00648946/en
22H. Kong, H. Zhang, X. Song, M. Gu, J. Sun.

Proving Computational Geometry Algorithms in TLA+2, in: 5th IEEE International Conference on Theoretical Aspects of Software Engineering(TASE 2011), Xi'an, China, August 2011.

http://hal.inria.fr/inria-00612413/en
23S. Ould Biha.

A formal semantics of PLC programs in Coq, in: IEEE Computer Software and Applications, COMPSAC'11, Munich, Germany, July 2011.

http://hal.inria.fr/inria-00601906/en
24X. Shi, J.-F. Monin, F. Tuong, F. Blanqui.

First steps towards the certification of an ARM simulator using Compcert, in: First International Conference on Certified Programs and Proofs, Hengchun, Taiwan, Province Of China, December 2011.

http://hal.inria.fr/inria-00624833/en
25L. Xiao, M. Gu, J. Sun.

The Verification of PLC Program Based on Interactive Theorem Proving Tool COQ, in: 4th IEEE International Conference on Computer Science and Information Technology(ICCSIT2011), Chengdu, China, June 2011.

http://hal.inria.fr/inria-00612408/en
26H. Zhang, M. Gu, X. Song.

Edola: A Domain Modeling and Verification Language for PLC Systems, in: The Sixth International Conference on Software Engineering (ICSEA 2011), Barcelona, Spain, October 2011.

http://hal.inria.fr/inria-00612416/en
27H. Zhang, Y. Jiang, H. William N.N., X. Song, M. Gu.

Domain-driven Probabilistic Analysis of Programmable Logic Controllers, in: 13th International Conference on Formal Engineering Methods(ICFEM 2011), Durham, United Kingdom, October 2011.

http://hal.inria.fr/inria-00612414/en

References in notes

28ARM Architecture Reference Manual DDI 0100I, ARM, 2005.
29Certification Problem Format.

http://cl-informatik.uibk.ac.at/software/cpf/
30F. Ghenassia (editor)

Transaction-Level Modeling with SystemC. TLM Concepts and Applications for Embedded Systems, Springer, June 2005, ISBN 0-387-26232-6.
31Software Manual, Renesas 32-Bit RISC Microcomputer SuperHTM RISC engine Family, Renesas, 2006.
32Termination Competition.

http://termination-portal.org/wiki/Termination_Competition
33OSCI SystemC TLM 2.0.1, Open SystemC Initiative, 2009.

http://www.systemc.org/
34F. Bellard.

QEMU, A Fast And Portable Dynamic Translator, in: USENIX Annual Technical Conference, Philadelphia, PA, USA, 2005.
35F. Blanqui, C. Helmstetter, V. Joloboff, J.-F. Monin, X. Shi.

Designing a CPU model: from a pseudo-formal document to fast code, in: 3rd Workshop on: Rapid Simulation and Performance Evaluation: Methods and Tools, Grèce Heraklion, 2011.

http://hal.inria.fr/inria-00546228/en/
36A. R. Bradley, Z. Manna, H. B. Sipma.

What's decidable about arrays, in: VMCAI '06, E. A. Emerson, K. S. Namjoshi (editors), LNCS, Springer, 2006, vol. 3855, p. 427–442.
37D. Burger, T. M. Austin.

The SimpleScalar tool set, version 2.0, in: SIGARCH Comput. Archit. News, 1997, vol. 25, n^o 3, p. 13–25.

http://doi.acm.org/10.1145/268806.268810
38L. Cai, D. Gajski.

Transaction level modeling: an overview, in: CODES+ISSS '03: Proceedings of the 1st IEEE/ACM/IFIP international conference on Hardware/software codesign and system synthesis, New York, NY, USA, ACM Press, 2003, p. 19–24.

http://doi.acm.org/10.1145/944645.944651
39Y.-F. Chen, E. Clarke, A. Farzan, M.-H. Tsai, Y.-K. Tsay, B.-Y. Wang.

Automated Assume-Guarantee Reasoning through Implicit Learning, in: Computer Aided Verification, Royaume-Uni Edinburgh, 2010.

http://hal.inria.fr/inria-00496949/en/
40E. Clarke, O. Grumberg, D. A. Peled.

Model Checking, The MIT Press, Cambridge, Massachusetts, 1999.
41B. Cmelik, D. Keppel.

Shade: a fast instruction-set simulator for execution profiling, in: SIGMETRICS Perform. Eval. Rev., 1994, vol. 22, n^o 1, p. 128–137.

http://doi.acm.org/10.1145/183019.183032
42J. M. Cobleigh, G. S. Avrunin, L. A. Clarke.

Breaking Up is Hard to do: An Evaluation of Automated Assume-Guarantee Reasoning, in: ACM Trans. Software Engineering Methodology, 2008, vol. 17, n^o 2.
43J. M. Cobleigh, D. Giannakopoulou, C. S. Păsăreanu.

Learning Assumptions for Compositional Verification, in: TACAS, H. Garavel, J. Hatcliff (editors), Lecture Notes in Computer Science, Springer Verlag, 2003, vol. 2619, p. 331–346.
44 Coq Development Team.

The Coq Reference Manual, Version 8.2, INRIA Rocquencourt, France, 2008.

http://coq.inria.fr/
45J. D'Errico, W. Qin.

Constructing portable compiled instruction-set simulators: an ADL-driven approach, in: DATE '06: Proceedings of the conference on Design, automation and test in Europe, 3001 Leuven, Belgium, Belgium, European Design and Automation Association, 2006, p. 112–117.
46Y. Deng, S. Grumbach, J.-F. Monin.

Towards Verifying Declarative Netlog Protocols with Coq, 2010.

http://hal.inria.fr/inria-00506093/en/
47L. Feng, M. Kwiatkowska, D. Parker.

Compositional Verification of Probabilistic Systems using Learning, in: QEST, G. Ciardo, R. Segal (editors), IEEE CS Press, 2010.
48F. Fummi, G. Perbellini, M. Loghi, M. Poncino.

ISS-centric modular HW/SW co-simulation., in: ACM Great Lakes Symposium on VLSI, 2006, p. 31-36.
49A. Gavare.

GXemul Documentation, 2007.

http://gxemul.sourceforge.net/gxemul-stable/doc/index.html
50P. Gerin, S. Yoo, G. Nicolescu, A. A. Jerraya.

Scalable and flexible cosimulation of SoC designs with heterogeneous multi-processor target architectures, in: ASP-DAC '01: Asia South Pacific Design Automation Conference, ACM, 2001, p. 63–68.
51J. Giesl, R. Thiemann, P. Schneider-Kamp, S. Falke.

Mechanizing and Improving Dependency Pairs, in: Journal of Automated Reasoning, 2006, vol. 37, n^o 3, p. 155-203.
52J.-Y. Girard, Y. Lafont, P. Taylor.

Proofs and Types, Cambridge University Press, 1988.
53N. Hirokawa, A. Middeldorp.

Tyrolean Termination Tool: Techniques and Features, in: Information and Computation, 2007, vol. 205, n^o 4, p. 474-511.
54 IEEE.

IEEE Standard 1666 - SystemC Language Reference Manual, IEEE, 2006.
55J.-P. Jouannaud, V. Van Oostrom.

Diagrammatic Confluence and Completion, in: International Conference in Automata, Languages and Programming, Grèce Rhodes, W. Thomas (editor), Springer Berlin/Heidelberg, 2009, vol. 2.

http://hal.inria.fr/inria-00436070/en/
56Y. Jung, S. Kong, B.-Y. Wang, K. Yi.

Deriving Invariants by Algorithmic Learning, Decision Procedures, and Predicate Abstraction, in: Verification, Model Checking, and Abstract Interpretation, Espagne Madrid, 2010.

http://hal.inria.fr/inria-00517257/en/
57S. Kong, Y. Jung, C. David, B.-Y. Wang, K. Yi.

Automatically Inferring Quantified Loop Invariants by Algorithmic Learning from Simple Templates, in: ASIAN Symposium on Programming Languages and Systems, Chine Shanghai, K. Ueda (editor), 2010.

http://hal.inria.fr/inria-00515166/en/
58D. Kroening, O. Strichman.

Decision Procedures: An Algorithmic Point of View, Springer, 2008, ISBN-10: 3540741046.
59L. Lamport.

Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers, Addison-Wesley, 2002.
60X. Leroy, D. Doligez, J. Garrigue, D. Rémy, J. Vouillon.

The Objective Caml system release 3.11, Documentation and user's manual, INRIA, France, 2008.

http://caml.inria.fr/
61X. Leroy.

A formally verified compiler back-end, in: Journal of Automated Reasoning, 2009, vol. 43, n^o 4, p. 363-446.
62R. Mayr, T. Nipkow.

Higher-Order Rewrite Systems and their Confluence, in: Theoretical Computer Science, 1998, vol. 192, n^o 2, p. 3-29.
63M. Meerwein, C. Baumgartner, T. Wieja, W. Glauert.

Embedded systems verification with FGPA-enhanced in-circuit emulator, in: ISSS '00: Proceedings of the 13th international symposium on System synthesis, Washington, DC, USA, IEEE Computer Society, 2000, p. 143–148.

http://doi.acm.org/10.1145/501790.501821
64G. Nelson.

Techniques for program verification, Stanford University, Stanford, CA, USA, 1980.
65G. Nelson, D. C. Oppen.

Simplification by cooperating decision procedures, in: ACM Trans. Program. Lang. Syst., 1979, vol. 1, n^o 2, p. 245–257.
66A. Nohl, G. Braun, O. Schliebusch, R. Leupers, H. Meyr, A. Hoffmann.

A universal technique for fast and flexible instruction-set architecture simulation, in: DAC '02: Proceedings of the 39th conference on Design automation, New York, NY, USA, ACM, 2002, p. 22–27.

http://doi.acm.org/10.1145/513918.513927
67M. Poncino, J. Zhu.

DynamoSim: a trace-based dynamically compiled instruction set simulator, in: ICCAD '04: Proceedings of the 2004 IEEE/ACM International conference on Computer-aided design, Washington, DC, USA, IEEE Computer Society, 2004, p. 131–136.

http://dx.doi.org/10.1109/ICCAD.2004.1382557
68M. Reshadi, P. Mishra, N. Dutt.

Instruction set compiled simulation: a technique for fast and flexible instruction set simulation, in: DAC '03: Proceedings of the 40th conference on Design automation, New York, NY, USA, ACM, 2003, p. 758–763.

http://doi.acm.org/10.1145/775832.776026
69P. Schaumont, D. Ching, I. Verbauwhede.

An interactive codesign environment for domain-specific coprocessors, in: ACM Trans. Des. Autom. Electron. Syst., 2006, vol. 11, n^o 1, p. 70–87.

http://doi.acm.org/10.1145/1124713.1124719
70R. Sebastiani.

Lazy satisfiability modulo theories, in: Journal on Satisfiability, Boolean Modeling and Computation, 2007, vol. 3, n^o 3-4, p. 141–224.
71H. Sheini, K. Sakallah.

From propositional satisfiability to satisfiability modulo theories, in: Theory and Applications of Satisfiability Testing-SAT 2006, 2006, p. 1–9.
72P.-Y. Strub.

Type Theory and Decision Procedures, École Polytechnique, July 2008.
73P.-Y. Strub.

Coq Modulo Theory, in: 19th EACSL Annual Conference on Computer Science Logic, Tchèque, République Brno, A. Dawar, H. Veith (editors), Springer, 2010, vol. 6247, p. 529–543.

http://hal.inria.fr/inria-00497404/en/
74 Technical Committee No.65.

IEC 1131 - Programmable Controllers, International Electrotechnical Commission, 1997.
75C. Weidenbach, D. Dimova, A. Fietzke, R. Kumar, M. Suda, P. Wischnewski.

SPASS Version 3.5, in: Automated Deduction - CADE-22, 22nd International Conference on Automated Deduction, Montreal, Canada, August 2-7, 2009. Proceedings, R. A. Schmidt (editor), Lecture Notes in Computer Science, Springer Verlag, 2009, p. 140-145.
76L. de Moura, B. Dutertre, N. Shankar.

A tutorial on satisfiability modulo theories, in: CAV'07: Proceedings of the 19th international conference on Computer aided verification, Berlin, Heidelberg, Springer-Verlag, 2007, p. 20–36.
77W.-P. de Roever, F. de Boer, U. Hanneman, J. Hooman, Y. Lakhnech, M. Poel, J. Zwiers.

Concurrency Verification: Introduction to Compositional and Noncompositional Methods, Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, 2001, n^o 54.

Previous |

Home