Publications de l'équipe FORMES

2012

Articles dans des revues avec comité de lecture

Titre

From Diagrammatic Confluence to Modularity

Auteurs

Jean-Pierre Jouannaud; Jiaxiang Liu

Détail

Theoretical Computer Science, Elsevier, 2012, 9032

Accès au bibtex

Communications avec actes

Titre

Church-Rosser Properties of Normal Rewriting

Auteurs

Jean-Pierre Jouannaud; Jian-Qi Li

Détail

Patrick Cégielsky and Arnaud Durand. Computer Science Logic, Sep 2012, Fontainebleau, France. Dagstuhl Publishing, Computer Science Logic 2012, 16, pp. 350-365, LIPIcs

Accès au texte intégral et bibtex

Titre

Formal Verification of Netlog Protocols

Auteurs

Meixian Chen; Jean-François Monin

Détail

Tiziana Margaria and Zongyan Qiu and Hongli Yang. TASE, Jul 2012, Beijing, China. IEEE

Accès au texte intégral et bibtex

Titre

INTRODUCING EXPLICIT CAUSALITY IN OBJECT-ORIENTED HYBRID SYSTEM MODELING

Auteurs

Liu Liu; Felix Felgner; Georg Frey

Détail

9th International Conference on Modeling, Optimization & SIMulation, Jun 2012, Bordeaux, France.

Accès au texte intégral et bibtex

Titre

Thread-Modular Model Checking with Iterative Refinement

Auteurs

Wenrui Meng; Fei He; Bow-Yaw Wang; Qiang Liu

Détail

NFM 2012 - 4th International Conference on NASA Formal Methods, Apr 2012, Norfolk, Virginia, United States.

Accès au bibtex

HDR

Titre

Terminaison des systèmes de réécriture d'ordre supérieur basée sur la notion de clôture de calculabilité

Auteurs

Frédéric Blanqui

Détail

Université Paris-Diderot - Paris VII, Jul. 2012. French

Accès au texte intégral et bibtex

2011

Articles dans des revues avec comité de lecture

Titre

A Formal Definition Method of Denotational Semantics and Functions for PLC Program Language

Auteurs

Litian Xiao; Ming Gu; Jiaguang Sun

Détail

Journal of Central South University (in Chinese), Central South University, 2011

Accès au bibtex

Titre

The Denotational Semantics Definition of PLC Programs Based on Extended λ-Calculus

Auteurs

Litian Xiao; Ming Gu; Jiaguang Sun

Détail

Communications in Computer and Information Science, Springer, 2011, Advanced Research on Computer Education, Simulation and Modeling, 176(II) (40-46)

Accès au bibtex

Titre

Argument filterings and usable rules in higher-order rewrite systems

Auteurs

Sho Suzuki; Keiichirou Kusakari; Frédéric Blanqui

Détail

IPSJ Transactions on Programming, IPSJ, 2011, 4 (2), pp. 1-12

Accès au texte intégral et bibtex

Titre

Formalisation and verification of programmable logic controllers timers in Coq

Auteurs

Hai Wan; Chen Gang; Xiaoyu Song; Ming Gu

Détail

IET Software, IET, 2011

Accès au bibtex

Titre

Formal modeling and synthesis of programmable logic controllers

Auteurs

Rui Wang; Xiaoyu Song; Jianzhong Zhu; Ming Gu

Détail

Computers in Industry, Elsevier, 2011

Accès au bibtex

Titre

CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates

Auteurs

Frédéric Blanqui; Adam Koprowski

Détail

Mathematical Structures in Computer Science, Cambridge University Press, 2011, 21 (4), pp. 827-859

Accès au texte intégral et bibtex

Communications avec actes

Titre

A Framework for Verifying Data-Centric Protocols

Auteurs

Yuxin Deng; Stephane Grumbach; Jean-François Monin

Détail

Bruni, Roberto and Dingel, Juergen. DisCoTec 2011 - 6th International Federated Conferences on Formal Techniques for Distributed Systems, Jun 2011, Reykjavik, Iceland. Springer, Formal Techniques for Distributed Systems, 6722, pp. 106-120, Lecture Notes in Computer Science

Accès au texte intégral et bibtex

Titre

First steps towards the certification of an ARM simulator using Compcert

Auteurs

Xiaomu Shi; Jean-François Monin; Frederic Tuong; Frédéric Blanqui

Détail

First International Conference on Certified Programs and Proofs, Dec 2011, Hengchun, Taiwan, Province Of China. 7086, LNCS

Accès au texte intégral et bibtex

Titre

Domain-driven Probabilistic Analysis of Programmable Logic Controllers

Auteurs

Hehua Zhang; Yu Jiang; Hung William N.N.; Xiaoyu Song; Ming Gu

Détail

13th International Conference on Formal Engineering Methods(ICFEM 2011), Oct 2011, Durham, United Kingdom.

Accès au texte intégral et bibtex

Titre

Edola: A Domain Modeling and Verification Language for PLC Systems

Auteurs

Hehua Zhang; Ming Gu; Xiaoyu Song

Détail

The Sixth International Conference on Software Engineering (ICSEA 2011), Oct 2011, Barcelona, Spain.

Accès au bibtex

Titre

Proving Computational Geometry Algorithms in TLA+2

Auteurs

Hui Kong; Hehua Zhang; Xiaoyu Song; Ming Gu; Jiaguang Sun

Détail

5th IEEE International Conference on Theoretical Aspects of Software Engineering(TASE 2011), Aug 2011, Xi'an, China.

Accès au texte intégral et bibtex

Titre

Fast Instruction Set Simulation Using LLVM-based Dynamic Translation

Auteurs

Vania Joloboff ; Xinlei Zhou; Claude Helmstetter; Xiaopeng Gao

Détail

International MultiConference of Engineers and Computer Scientists 2011, Mar 2011, Hong Kong, China. Springer, Lecture Notes in Engineering and Computer Science, 2188, pp. 212-216

Accès au bibtex

Titre

A formal semantics of PLC programs in Coq

Auteurs

Sidi Ould Biha

Détail

IEEE. IEEE Computer Software and Applications, COMPSAC'11, Jul 2011, Munich, Germany.

Accès au texte intégral et bibtex

Titre

Verification of PLC Properties Based on Formal Semantics in Coq

Auteurs

Jan Olaf Blech; Sidi Ould Biha

Détail

International Conference on Software Engineering and Formal Methods, SEFM 2011, Nov 2011, Montevideo, Uruguay.

Accès au bibtex

Titre

The Verification of PLC Program Based on Interactive Theorem Proving Tool COQ

Auteurs

Litian Xiao; Ming Gu; Jiaguang Sun

Détail

4th IEEE International Conference on Computer Science and Information Technology(ICCSIT2011), Jun 2011, Chengdu, China.

Accès au bibtex

Titre

Predicate Generation for Learning-Based Quantifier-Free Loop Invariant Inference

Auteurs

Yungbum Jung; Wonchan Lee; Bow-Yaw Wang; Kwangkeun Yi

Détail

TACAS 2011 - Seventeenth International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Mar 2011, Saarbruecken, Germany. Springer, Tools and Algorithms for the Construction and Analysis of Systems, 6605, pp. 205-219, Lecture Notes in Computer Science

Accès au bibtex

Titre

CoqMTU: a higher-order type theory with a predicative hierarchy of universes parametrized by a decidable first-order theory

Auteurs

Bruno Barras; Jean-Pierre Jouannaud; Pierre-Yves Strub; Qian Wang

Détail

Twenty-Sixth Annual IEEE Symposium on "Logic in Computer Science" - LICS 2011, Jun 2011, Toronto, Canada.

Accès au texte intégral et bibtex

2010

Articles dans des revues avec comité de lecture

Titre

On the confluence of lambda-calculus with conditional rewriting

Auteurs

Frédéric Blanqui; Claude Kirchner; Colin Riba

Détail

Theoretical Computer Science, Elsevier, 2010, 411 (37), pp. 3301-3327

Accès au texte intégral et bibtex

Titre

Specifying and Verifying PLC systems with TLA+: a case study

Auteurs

Hehua Zhang; Stephan Merz; Ming Gu

Détail

Computers & Mathematics with Applications, 2010, 60 (3), pp. 695-705

Accès au bibtex

Communications avec actes

Titre

Designing a CPU model: from a pseudo-formal document to fast code

Auteurs

Frédéric Blanqui; Claude Helmstetter; Vania Joloboff; Jean-François Monin; Xiaomu Shi

Détail

3rd Workshop on: Rapid Simulation and Performance Evaluation: Methods and Tools, Jan 2011, Heraklion, Greece. 2010

Accès au texte intégral et bibtex

Titre

Automatically Inferring Quantified Loop Invariants by Algorithmic Learning from Simple Templates

Auteurs

Soonho Kong; Yungbum Jung; Cristina David; Bow-Yaw Wang; Kwangkeun Yi

Détail

Kazunori Ueda. ASIAN Symposium on Programming Languages and Systems, Nov 2010, Shanghai, China. APLAS, LNCS

Accès au bibtex

Titre

Parameterized Specification and Verification of PLC Systems in Coq

Auteurs

Hai Wan; Xiaoyu Song; Ming Gu

Détail

4th IEEE International Symposium on Theoretical Aspects of Software Engineering, Aug 2010, Taipei, Taiwan, Province Of China.

Accès au texte intégral et bibtex

Titre

Compositional Abstraction Refinement for Timed Systems

Auteurs

Fei He; Lei Zhu; William Hung; Xiaoyu Song; Ming Gu

Détail

IEEE International Symposium on Theoretical Aspects of Software Engineering, Aug 2010, Taipei, Taiwan, Province Of China.

Accès au bibtex

Titre

Specifying time-sensitive systems with TLA+

Auteurs

Hehua Zhang; Ming Gu; Xiaoyu Song

Détail

COMPSAC 2010 : 34th Annual IEEE Computer Software and Applications Conference, Jul 2010, Seoul, Korea, Republic Of. pp. 425-430

Accès au texte intégral et bibtex

Titre

On Array Theory of Bounded Elements

Auteurs

Min Zhou; Fei He; Bow-Yaw Wang; Ming Gu

Détail

CAV 2010 - 22nd International Conference on Computer Aided Verification, Jul 2010, Edinburgh, United Kingdom.

Accès au bibtex

Titre

A Computability Path Ordering for Polymorphic Terms - Short Paper

Auteurs

Jian-Qi Li

Détail

25th Annual IEEE Symposium on Logic in Computer Science (LICS 2010), Jul 2010, Edinburgh, United Kingdom.

Accès au bibtex

Titre

Proof Trick: Small Inversions

Auteurs

Jean-François Monin

Détail

Yves Bertot. Second Coq Workshop, Jul 2010, Edinburgh, United Kingdom.

Accès au texte intégral et bibtex

Titre

Coq Modulo Theory - Short Paper

Auteurs

Pierre-Yves Strub; Qian Wang

Détail

Logic In Computer Science (LICS 2010), Jul 2010, Edimbourg, United Kingdom.

Accès au texte intégral et bibtex

Titre

A Refinement-Based Validation Method for Programmable Logic Controllers

Auteurs

Hai Wan; Xiaoyu Song; Gang Chen; Ming Gu

Détail

The 10th International Conference on Quality Software, Jul 2010, Zhangjiajie, Hunan, China.

Accès au texte intégral et bibtex

Titre

Formal Modeling and Verification of Services Managements for Pervasive Computing Environment

Auteurs

Hai Wan; Zoé Drey; Zhiyang You; Liu Liu

Détail

The 7th International Conference on Service Systems and Service Management, Jun 2010, Tokyo, Japan.

Accès au texte intégral et bibtex

Titre

A Computability Path Ordering for Polymorphic Terms

Auteurs

Jean-Pierre Jouannaud; Jian-Qi Li

Détail

11th International Workshop on Termination, Jul 2010, Edinburgh, United Kingdom.

Accès au bibtex

Titre

Deriving Invariants by Algorithmic Learning, Decision Procedures, and Predicate Abstraction

Auteurs

Yungbum Jung; Soonho Kong; Bow-Yaw Wang; Kwangkeun Yi

Détail

Verification, Model Checking, and Abstract Interpretation, Jan 2010, Madrid, Spain.

Accès au bibtex

Titre

Automated Assume-Guarantee Reasoning through Implicit Learning

Auteurs

Yu-Fang Chen; Edmund Clarke; Azadeh Farzan; Ming-Hsien Tsai; Yih-Kuen Tsay; Bow-Yaw Wang

Détail

Computer Aided Verification, 2010, Edinburgh, United Kingdom.

Accès au bibtex

Titre

Coq Modulo Theory

Auteurs

Pierre-Yves Strub

Détail

Anuj Dawar and Helmut Veith. 19th EACSL Annual Conference on Computer Science Logic, Aug 2010, Brno, Czech Republic. Springer, Computer Science Logic, CSL 2010, 19th Annual Conference of the EACSL, 6247, pp. 529-543, Lecture Notes in Computer Science

Accès au texte intégral et bibtex

Titre

Infinite families of finite string rewriting systems and their confluence

Auteurs

Jean-Pierre Jouannaud; Benjamin Monate

Détail

Fermüller and Voronkov. Proc. LPAR 2010, Oct 2010, Yogyakarta, Indonesia. SPRINGER, 17th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, pp. missing

Accès au texte intégral et bibtex

Conférences invitées

Titre

Comparing Learning Algorithms in Automated Assume-Guarantee Reasoning

Auteurs

Yu-Fang Chen; Edmund Clarke; Azadeh Farzan; Fei He; Ming-Hsien Tsai; Yih-Kuen Tsay; Bow-Yaw Wang; Lei Zhu

Détail

Bernhard Steffen. International Symposium On Leveraging Applications of Formal Methods, Verification and Validation, Oct 2010, Crete, Greece. ISOLA, LNCS

Accès au bibtex

Titre

Certification of SAT Solvers in Coq

Auteurs

Jean-Pierre Jouannaud; Pierre-Yves Strub; Lianyi Zhang

Détail

Guangzhou Symposium on Satisfiability in Logic-Based Modeling, Sep 2010, Zuhai, China. Proc. Guangzhou Symposium on Satisfiability in Logic-Based Modeling

Accès au texte intégral et bibtex

Rapports

Titre

Towards Verifying Declarative Netlog Protocols with Coq

Auteurs

Yuxin Deng; Stephane Grumbach; Jean-François Monin

Détail

[Interne], 2010, pp. 20

Accès au texte intégral et bibtex

Titre

Argument filterings and usable rules in higher-order rewrite systems

Auteurs

Sho Suzuki; Keiichirou Kusakari; Frédéric Blanqui

Détail

[Research Report], 2010. IEICE-TR-SS2010-24.Vol110.N169

Accès au texte intégral et bibtex

2009

Articles dans des revues avec comité de lecture

Titre

Static Dependency Pair Method based on Strong Computability for Higher-Order Rewrite Systems

Auteurs

Keiichirou Kusakari; Yasuo Isogai; Masahiko Sakai; Frédéric Blanqui

Détail

IEICE Transactions on Information and Systems, IEICE, 2009

Accès au texte intégral et bibtex

Titre

Formal modeling and analysis of a narrow bandwidth protocol for establishing and terminating connections

Auteurs

Hai Wan; Ming Gu; Xiaoyu Song

Détail

Mathematical and Computer Modelling, Elsevier, 2009, 50 (7-8)

Accès au texte intégral et bibtex

Titre

Heuristic-Guided Abstraction Refinement

Auteurs

Fei He; Xiaoyu Song; Ming Gu; Jia-Guang Sun

Détail

Computer Journal, Oxford University Press, 2009

Accès au bibtex

Communications avec actes

Titre

SimSoC: A full system simulation software for embedded systems

Auteurs

Claude Helmstetter; Vania Joloboff; Hui Xiao

Détail

IEEE. 2009 International Workshop on Open-source Software for Scientific Computation (OSSC-2009), Sep 2009, Guiyang, China. 7 p.

Accès au texte intégral et bibtex

Titre

Data Mining Based Decomposition for Assume-Guarantee Reasoning

Auteurs

He Zhu; Fei He; William Hung; Xiaoyu Song; Ming Gu

Détail

9th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2009), Sep 2009, Austin, United States.

Accès au bibtex

Titre

Translation-based model checking for PLC programs

Auteurs

Min Zhou; Fei He; Ming Gu; Xiaoyu Song

Détail

33rd Annual IEEE International Computer Software and Applications Conference, Jul 2010, Seattle, Washington, United States. 2009

Accès au bibtex

Titre

Diagrammatic Confluence and Completion

Auteurs

Jean-Pierre Jouannaud; Vincent Van Oostrom

Détail

Wolfgang Thomas. International Conference in Automata, Languages and Programming, Jul 2009, Rhodes, Greece. Springer Berlin/Heidelberg, Automata, Languages and Programming, 2, Lecture Notes in Computer Science

Accès au bibtex

Titre

Formalization and Verification of PLC Timers in Coq

Auteurs

Hai Wan; Gang Chen; Xiaoyu Song; Ming Gu

Détail

33rd Annual IEEE International Computer Software and Applications Conference, Jul 2009, Seattle,Washington, United States.

Accès au texte intégral et bibtex

Titre

On the relation between sized-types based termination and semantic labelling

Auteurs

Frédéric Blanqui; Cody Roux

Détail

18th EACSL Annual Conference on Computer Science Logic - CSL 09, Sep 2009, Coimbra, Portugal.

Accès au texte intégral et bibtex

Titre

Formal specification and Code Generation of Programmable Logic Controllers

Auteurs

Rui Wang; Ming Gu; Xiaoyu Song; Hai Wan

Détail

IEEE International Conference on Engineering of Complex Computer System, 2009, Berlin, Germany.

Accès au bibtex

Rapports

Titre

Automated Verification of Termination Certificates

Auteurs

Frédéric Blanqui; Adam Koprowski

Détail

[Research Report], 2009, pp. 24. RR-6949

Accès au texte intégral et bibtex

Thèses

Titre

Domain-specific modeling and verification language EDOLA

Auteurs

Hehua Zhang

Détail

Tsinghua university, Dec. 2009. Chinese

Accès au texte intégral et bibtex

2008

Articles dans des revues avec comité de lecture

Titre

Modular Church-Rosser Modulo: the Full Picture

Auteurs

Jean-Pierre Jouannaud; Yoshihito Toyama

Détail

International Journal of Software and Informatics, Institute of Software of the Chinese Academy of Sciences, 2008

Accès au bibtex

Communications avec actes

Titre

Modeling and Analysis of Stage Machinery Control Systems by Timed Colored Petri Nets

Auteurs

Hehua Zhang; Ming Gu; Xiaoyu Song

Détail

SIES 2008, Jun 2008, Monpellier, France.

Accès au texte intégral et bibtex

Titre

SystemC/TLM Semantics for Heterogeneous System-on-Chip Validation

Auteurs

Florence Maraninchi; Matthieu Moy; Jérôme Cornet; Laurent Maillet-Contoz; Claude Helmstetter; Claus Traulsen

Détail

IEEE. 2008 Joint IEEE-NEWCAS and TAISA Conference, Jun 2008, Montréal, Canada. pp. unknown

Accès au texte intégral et bibtex

Titre

From formal proofs to mathematical proofs: a safe, incremental way for building in first-order decision procedures

Auteurs

Frédéric Blanqui; Jean-Pierre Jouannaud; Pierre-Yves Strub

Détail

5th IFIP International Conference on Theoretical Computer Science - TCS 2008, Sep 2008, Milan, Italy. 273, IFIP

Accès au texte intégral et bibtex

Titre

A Comparison of Two SystemC/TLM Semantics for Formal Verification

Auteurs

Claude Helmstetter; Olivier Ponsini

Détail

Formal Methods and Models for Codesign (MEMOCODE), Jun 2008, Anaheim, United States.

Accès au bibtex

Conférences invitées

Titre

The computability path ordering: the end of a quest

Auteurs

Frédéric Blanqui; Jean-Pierre Jouannaud; Albert Rubio

Détail

7th EACSL Annual Conference on Computer Science Logic - CSL'08, Sep 2008, Bertinoro, Italy. 5213, LNCS

Accès au texte intégral et bibtex