Skip to content
Snippets Groups Projects
  1. Apr 11, 2014
  2. Apr 09, 2014
  3. Apr 08, 2014
  4. Apr 07, 2014
  5. Mar 25, 2014
  6. Mar 21, 2014
  7. Mar 20, 2014
  8. Mar 17, 2014
  9. Mar 14, 2014
  10. Mar 13, 2014
  11. Mar 11, 2014
  12. Mar 05, 2014
  13. Mar 04, 2014
  14. Mar 03, 2014
  15. Feb 28, 2014
    • Etienne Kneuss's avatar
      Implement the Leon library. Support classes and methods. · 027c0d4c
      Etienne Kneuss authored
      - Implement the Leon Library in Leon-land rather than Scala-land.
        import leon.Utils._ becomes import leon.lang._
        import leon.Annotations._ becomes import leon.annontation._
      
        For now, the library defines generic Options and Lists.
        The library is automatically imported from the ./leon script, unless
        the --library=no option is passed.
      
      - Support parsing of multiple files and modules.
      
      - Introduce new annontations:
          @ignore: remove definition from Leon
          @verified: do not consider for verification unless explicitly
              specified
      027c0d4c
    • Etienne Kneuss's avatar
      EnumeratingSolver / PortfolioSolver · aab7b7f3
      Etienne Kneuss authored
      Use a datagen-based solver to find simple counter-examples. Note that
      this solver returns Unknown most of the time, so it is best to combine
      it with a full-fledged solver.
      
      PortfolioSolver allows us to combine solvers and have them run in
      parallel. The first result (!= Unknown) is used. Solvers can be selected
      for verification using the --solvers option.
      aab7b7f3
  16. Feb 24, 2014
  17. Feb 20, 2014
  18. Feb 18, 2014
Loading