Prototypes

CiME Alt-Ergo

• CiME 3 is a rewriting toolbox that provides Coq certificates for termination proofs (standard rewriting) obtained using various criteria:
  • Dependency pairs:
    • plain/marks,
    • graphs refinements with or without sub-term criterion,
  as well as various orderings:
  • Polynomial interpretations,
  • Matrix interpretations,
  • Full RPO with status, with AFS refinements.
  
  CiME 3 may be used alone (searching for proofs and producing certificates) or in conjunction with your own prover via xml input/output and translation to .v files.
  Note that in addition to its own xml format, CiME 3 now supports CPF v2 for the aformentioned techniques.

  Download

  Binary executables of the tool are available under CeCill-C licence
  (don't hesitate to ask for a binary dedicated to your architecture).
  These versions can discover and certify termination proofs of more than 620 problems of the TRS section (1391 problems) of the TPDB.
  Require minisat 2.0.
  • latest CiME 3 binaries for i686 64 bits linux: [static] [dynamic] updated (07/13/10)
  • latest CiME 3 binaries for i686 32 bits linux: [static] [dynamic] updated (07/13/10)
  • latest CiME 3 binaries for intel mac OS X: [dynamic] updated (07/13/10)
  • Relevant Coccinelle 8.2 version: [tar.gz] (07/13/10)
  
  
  • Short tutorial
  • example of preamble [cim3] (requires minisat2)
  • preamble for using sub-term only [cim3]
  • short howto for sub-term.
  • some benchs with sub-term.

  Previous versions

  • CiME 3 binaries for i686 32 bits linux: [static] [dynamic] (16/10/09)
    
  • CiME 3 binaries for i686 64 bits linux: [static] [dynamic] (16/10/09)
  • CiME 3 binaries for mac OS X: [dynamic] (16/10/09)
    
  • Relevant Coccinelle 8.2 version: [tar.gz] (16/10/09)

  Mailing list

  For any requests, information, announcement, you may subscribe to the cime-club mailing list.
  
  
• Alt-Ergo is a theorem prover aiming at program verification with full automation. It contains:
  • Congruence Closure parameterized by an equational theory;
  • Fourier-Motzkin procedure;
  • SAT-solver.

Libraries

• Coccinelle (Terms, Rewriting, RPO, etc.)
  
  • For Coq 8.2 [tar.gz] updated (12/11/09)
    
    
  • Legacy Coccinelle Trunk 11444 version: [tar.gz]
  • For Coq trunk 9816 [tgz]
  • For Coq 8.1 [tgz]
• Ordinals
  
  • Description (French): [html]
  • Archive: [tgz]

Publications

• Contejean, Courtieu, Forest, Paskevich, Pons and Urbain. A3PAT, an approach for certified automated termination proofs. In Proc. of the 2010 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM10), ACM, pp 63--72, Madrid, Spain, jan. 2010.
• Courtieu, Gbedo, Pons. Improved matrix interpretations. In J. van Leeuwen et al., ed., 36th International Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM 2010), LNCS, Špindleruv Mlýn, Czech Republic, Jan. 2010. To appear.
• Courtieu, Gbedo, Pons. Matrix Interpretations Revisited. In A. Geser ed., 10th International Workshop on Termination (WST 09), 2009.
• Courtieu, Forest, Urbain. Certifying a Termination Criterion Based on Graphs, without Graphs. In C. Munoz and O. Ait Mohamed ed., 21st International Conference on Theorem Proving in Higher Order Logics (TPHOLs 08), volume 5170 of Lecture Notes in Computer Science, pages 183--198, Montréal, Canada, Aug. 2008.
• Bertot, Komendantskaya. Inductive and Coinductive Components of Corecursive Functions in Coq. In 9th International Workshop on Coalgebraic Methods in Computer Science (CMCS 08), volume 203 of Electronic Notes in Computer Science, pages 25--47, Apr. 2008.
• Bobot, Conchon, Contejean, Lescuyer. Implementing Polymorphism in SMT solvers. In C. Barrett and L. de Moura ed., 6th International Workshop on Satisfiability Modulo (SMT 08), 2008.
• Conchon, Contejean, Kanig, Lescuyer. CC(X): Semantical Combination of Congruence Closure with Solvable Theories. Proceedings of SMT 07, Electronic Notes on Theoretical Computer Science 192(2):51--69, 2008.
• Contejean, Courtieu, Forest, Pons, Urbain. Certification of automated termination proofs. In B. Konev and F. Wolter ed., 6th International Symposium on Frontiers of Combining Systems (FroCos 07), volume 4720 of Lecture Notes in Artificial Intelligence, pages 148--162, Liverpool, UK, Sep. 2007.
• Conchon, Contejean, Kanig, Lescuyer. Lightweight Integration of the Ergo Theorem Prover inside a Proof Assistant. In J. Rushby and N. Shankar ed., Automated Formal Methods (AFM 07), Atlanta, USA, 2007.
• Conchon, Contejean, Kanig. CC(X): Efficiently Combining Equality and Solvable Theories without Canonizers. In S. Krstic and A. Oliveras ed., 5th International Workshop on Satisfiability Modulo (SMT 2007), Berlin, Germany, Jul. 2007.
• Contejean. Modelling permutations in COQ for Coccinelle. In H. Comon-Lundth, C. Kirchner and H. Kirchner ed., Rewriting, Computation and Proof, Paris, France, 2007.
• Castéran. Utilisation en Coq de l'opérateur de description.
  Actes des Journées francophones des langages applicatifs (JFLA), January 2007.
  [pdf] (in French.)
• Contejean, Forest, Urbain. Deep-Embedded Unification.
  Technical Report 1547, Cédric, 2008
• Conchon, Contejean. Rule Based Incremental Congruence Closure with Commutative Symbols.
  Research Report LRI/PCRI.
  [pdf]