Prototypes

CiME and Alt-Ergo

• CiME 3 is a rewriting toolbox that provides Coq certificates for termination, local confluence and convergence, and equality proofs (standard rewriting).
  Termination proofs may be obtained using various criteria:
  • Manna-Ness,
  • Dependency pairs:
    • plain/marks,
    • graphs refinements with or without extended sub-term criterion,
  as well as various orderings:
  • Polynomial interpretations,
  • (extended) 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.
  CiME 3 supports CPF v2 for the aformentioned techniques.
  Output are in Coq scripts only regarding proofs of confluence and of equality.

  Try Online

  Download

  CiME 3 "release" is here! new syntax for heuristics and ordering parameters, certified proofs of local confluence and convergence, certified proofs of equality (example)...

  Binary executables of the tool are available under CeCill-C licence
  (don't hesitate to ask for a binary dedicated to your architecture).
  

  • Release CiME 3 binaries for i686 64 bits linux: [static](Bugfix 2011/05/26) [dynamic] (Bugfix 2011/04/01)
  • Ocaml Sources [tarball] (Bugfix 2011/03/08)
    
    
  • Coccinelle 8.3 version [tar.gz]
  • Coccinelle 8.2 version [tar.gz]
    
    
  • Short manual [html]

  Legacy

  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. No confluence. Obsolete syntax.
  • CiME 3 binaries for i686 64 bits linux: [static] [dynamic] updated (07/13/10)
  • CiME 3 binaries for i686 32 bits linux: [static] [dynamic] updated (07/13/10)
  • CiME 3 binaries for intel mac OS X: [dynamic] updated (07/13/10)
  • Relevant Coccinelle 8.2 version: [tar.gz] (21/01/11)
  
  
  • 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.
  • 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.3 [tar.gz]
  • For Coq 8.2 [tar.gz] updated (21/01/11)
    
    
  • 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, Pons, Urbain. Automated Certified Proofs with CiME 3. In M. Schmidt-Schauss, ed., 22nd International Conference on Rewriting Techniques and Applications (RTA11), Novi Sad, Serbia, 2011, to appear.
• 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), volume 5901 of Lecture Notes in Computer Science, pages 283--295, Špindleruv Mlýn, Czech Republic, Jan. 2010.
• 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, Courtieu, Forest, Pons, Urbain. Automated Certified Proofs with CiME 3.
  Technical Report 2044, Cédric, 2011
  [pdf]
• 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]