EN FR
EN FR


previous Previous | up Home


Bibliography

Major publications by the team in recent years
  • 1B. 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, This research is sponsored by NSFC Program (No.91018015) and 973 Program (No.2010CB328003) of China.

    http://hal.inria.fr/inria-00583136
  • 2F. Blanqui.

    Definitions by rewriting in the Calculus of Constructions, in: Mathematical Structures in Computer Science, 2005, vol. 15, no 1, pp. 37-92. [ DOI : 10.1017/S0960129504004426 ]

    http://hal.inria.fr/inria-00105648/en/
  • 3F. 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, Best paper award.

    http://hal.inria.fr/inria-00546228/en/
  • 4F. 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, no 4, pp. 827-859.

    http://hal.inria.fr/inria-00543157/en/
  • 5F. 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/
  • 6B. 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.
  • 7B. 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, pp. 197–212, ISBN 3-540-44307-X.
  • 8F. He, X. Song, M. Gu, J. Sun.

    Heuristic-Guided Abstraction Refinement, in: Computer Journal, May 2009, vol. 52, no 3, pp. 280-287.
  • 9J.-P. Jouannaud, J.-Q. Li.

    Church-Rosser Properties of Normal Rewriting, in: Computer Science Logic, Fontainebleau, France, P. Cégielsky, A. Durand (editors), LIPIcs, Dagstuhl Publishing, September 2012, vol. 16, pp. 350-365. [ DOI : 10.4230/LIPIcs.CSL.2012.i ]

    http://hal.inria.fr/hal-00730271
  • 10J.-P. Jouannaud, J. Liu.

    From diagrammatic confluence to modularity, in: Theor. Comput. Sci., 2012, vol. 464, pp. 20-34.
  • 11J.-P. Jouannaud, A. Rubio.

    Polymorphic Higher-Order Recursive Path Orderings, in: Journal of the ACM, 2007, vol. 54, no 1, pp. 1-48.
  • 12J.-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/
  • 13X. Shi, J.-F. Monin, F. Tuong, F. Blanqui.

    First Steps towards the Certification of an ARM Simulator Using Compcert, in: Certified Proofs and Programs - First International Conference, Kenting, Taiwan, J.-P. Jouannaud, Z. Shao (editors), LNCS, Springer, December 7-9 2011, vol. 7086, pp. 346-361.
Publications of the year

Doctoral Dissertations and Habilitation Theses

International Conferences with Proceedings

  • 15J.-F. Monin, X. Shi.

    Handcrafted Inversions Made Operational on Operational Semantics, in: ITP 2013 - 4th International Conference Interactive Theorem Proving, Rennes, France, S. Blazy, C. Paulin-Mohring, D. Pichardie (editors), LNCS - Lecture Notes in Computer Science, Springer, July 2013, vol. 7998, pp. 338-353. [ DOI : 10.1007/978-3-642-39634-2_25 ]

    http://hal.inria.fr/hal-00937168
  • 16Q. Wang, B. Barras.

    Semantics of Intensional Type Theory extended with Decidable Equational Theories, in: Computer Science Logic 2013, Dagstuhl, Germany, S. R. D. Rocca (editor), Leibniz International Proceedings in Informatics (LIPIcs), Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, August 2013, vol. 23, pp. 653–667. [ DOI : 10.4230/LIPIcs.CSL.2013.653 ]

    http://hal.inria.fr/hal-00937197

Other Publications

References in notes
  • 18ARM Architecture Reference Manual DDI 0100I, ARM, 2005.
  • 19F. Ghenassia (editor)

    Transaction-Level Modeling with SystemC. TLM Concepts and Applications for Embedded Systems, Springer, June 2005, ISBN 0-387-26232-6.
  • 20Software Manual, Renesas 32-Bit RISC Microcomputer SuperHTM RISC engine Family, Renesas, 2006.
  • 21OSCI SystemC TLM 2.0.1, Open SystemC Initiative, 2009.

    http://www.systemc.org/
  • 22T. Arts, J. Giesl.

    Termination of Term Rewriting Using Dependency Pairs, in: Theoretical Computer Science, 2000, vol. 236, pp. 133-178.
  • 23F. Bellard.

    QEMU, A Fast And Portable Dynamic Translator, in: USENIX Annual Technical Conference, Philadelphia, PA, USA, 2005.
  • 24F. Blanqui.

    Terminaison des systèmes de réécriture d'ordre supérieur basée sur la notion de clôture de calculabilité, Université Paris-Diderot - Paris VII, July 2012, HDR.

    http://tel.archives-ouvertes.fr/tel-00724233
  • 25F. Blanqui, J.-P. Jouannaud, A. Rubio.

    The Computability Path Ordering: the End of a Quest, in: Proceedings of the 22nd International Conference on Computer Science Logic, Lecture Notes in Computer Science 5213, 2008, Invited paper.
  • 26A. 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, pp. 427–442.
  • 27D. Burger, T. M. Austin.

    The SimpleScalar tool set, version 2.0, in: SIGARCH Comput. Archit. News, 1997, vol. 25, no 3, pp. 13–25.

    http://doi.acm.org/10.1145/268806.268810
  • 28L. 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, pp. 19–24.

    http://doi.acm.org/10.1145/944645.944651
  • 29Y.-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/
  • 30E. Clarke, O. Grumberg, D. A. Peled.

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

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

    http://doi.acm.org/10.1145/183019.183032
  • 32J. 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, no 2.
  • 33J. 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, pp. 331–346.
  • 34J. 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, pp. 112–117.
  • 35L. Feng, M. Kwiatkowska, D. Parker.

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

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

    GXemul Documentation, 2007.

    http://gxemul.sourceforge.net/gxemul-stable/doc/index.html
  • 38P. 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, pp. 63–68.
  • 39IEEE.

    IEEE Standard 1666 - SystemC Language Reference Manual, IEEE, 2006.
  • 40Y. 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/
  • 41S. 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/
  • 42D. Kroening, O. Strichman.

    Decision Procedures: An Algorithmic Point of View, Springer, 2008, ISBN-10: 3540741046.
  • 43M. 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, pp. 143–148.

    http://doi.acm.org/10.1145/501790.501821
  • 44G. Nelson.

    Techniques for program verification, Stanford University, Stanford, CA, USA, 1980.
  • 45A. 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, pp. 22–27.

    http://doi.acm.org/10.1145/513918.513927
  • 46M. 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, pp. 131–136.

    http://dx.doi.org/10.1109/ICCAD.2004.1382557
  • 47M. 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, pp. 758–763.

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

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

    http://doi.acm.org/10.1145/1124713.1124719
  • 49R. Sebastiani.

    Lazy satisfiability modulo theories, in: Journal on Satisfiability, Boolean Modeling and Computation, 2007, vol. 3, no 3-4, pp. 141–224.
  • 50H. Sheini, K. Sakallah.

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

    Type Theory and Decision Procedures, École Polytechnique, July 2008.
  • 52Coq. D. Team.

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

    http://coq.inria.fr/
  • 53L. 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, pp. 20–36.
  • 54W.-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, no 54.
  • 55V. van Oostrom.

    Confluence by Decreasing Diagrams, in: RTA, A. Voronkov (editor), Lecture Notes in Computer Science, Springer, 2008, vol. 5117, pp. 306-320.


previous Previous | up Home