[Caml-list] Second Call for Papers: VSTTE 2009
Due to many requests, the submission deadline for the VSTTE workshop has been extended. * * * * VSTTE 2009 * * * *Workshop on Verified Software * *Theory Tools and Experiments * * * *(affiliated with Formal Methods Week) * * * * November 2, 2009* * Eindhoven, the Netherlands * *http://vstte09.lri.fr/ * * * *Deadline for submissions: Sep 11, 2009* * * * FM 2009 is the sixteenth in a series of symposia of the Formal Methods Europe association, and the second one that is organized as a world congress. Ten years after FM'99, the 1st World Congress, the formal methods communities from all over the world will once again have an opportunity to meet. FM 2009 will be both an opportunity to celebrate, and an opportunity to join in when enthusiastic researchers and practitioners from a diversity of backgrounds and schools come together to discuss their ideas and experiences. The workshop on Verified Software: Theories, Tools, and Experiments (VSTTE 2009) will take place on November the 2nd. The focus of this workshop will be on tools, as previous VSTTE conferences in Zurich and Toronto emphasised theories and experiments. Consisting of contributed papers and invited talks, the workshop will focus on the tools behind the development of systematic methods for specifying, building, and verifying high-quality software. This includes topics like: * Program logic * Specification and verification techniques * Tool support for specification languages * Tool for various design methodologies * Tool integration and plug-ins * Automation in formal verification * Tool comparisons and benchmark repositories * Combination of tools and techniques (e.g. formal vs. semiformal, software specification vs. engineering techniques) * Customizing tools for particular applications Papers about tool architectures, and their achievements are most welcome. The contributed papers, which should report on previously unpublished work, can reflect current and preliminary work in areas of software verification. New technical results, overviews of new developments in software verification projects, short papers accompanying tool demonstrations, as well as position papers on how to further advance the goal of verified software are all welcome. SUBMISSION PROCEDURE VSTTE proceedings will be published as a special issue of the Software Tools for Technology Transfer (STTT) journal. Submitted papers should not have been submitted elsewhere for publication. Papers should use Springer-Verlag's STTT package ftp://ftp.springer.de/pub/tex/latex/svjour/sttt/, and should not exceed 15 pages including appendices. Papers are processed through the EasyChair conference management system. IMPORTANT DATES === Submission deadline September 11, 2009, 11:59pm Samoa time (UTC-11) Notification of acceptance October 2, 2009 Final version October 16, 2009 PROGRAM COMMITTEE = * David Deharbe, Dimap UFRN, Brazil * Dino Distefano, Queen Mary University of London, UK * Jean-Christophe Filliâtre (co-chair), CNRS, France * Leo Freitas (co-chair), University of York, UK * John McDermott, Naval Research Laboratory, USA * Yannick Moy, AdaCore, France * Arnaud Venet, Kestrel Technology, USA CONTACT === Leo Freitas, l...@cs.york.ac.uk Department of Computer Science University of York, YO10 5DD York, UK Tel: (+44) (0) 1904 434753 Jean-Christophe Filliatre, jean-christophe.fillia...@lri.fr CNRS / INRIA Saclay - Ile-de-france - ProVal Parc Orsay Universite, batiment N 4, rue Jacques Monod 91893 Orsay Cedex FRANCE Tel: (+33) (0)1 74 85 42 27 FURTHER INFORMATION === Further information will be put on the workshop web-page http://vstte09.lri.fr/. ___ Caml-list mailing list. Subscription management: http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list Archives: http://caml.inria.fr Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports: http://caml.inria.fr/bin/caml-bugs
RE: [Caml-list] Windows Vista/7 specific functions
Hi Reed, Having hacked away with the Win64 port before I thought I’d have a go. The first thing I noticed is that Microsoft have finally released the x86 and x64 compilers in the same package (this was a pain if you wanted to build MSVC and MSVC64 ports as you needed two SDKs to do it...) – though I haven’t tried building the 32-bit MSVC port from this SDK yet. Here’s what I did (you’ll have to excuse my idiosyncratic way of copying binary files into the OCaml tree – these can be replaced with PATH changes if you want. I copy things around so that ocamlopt always works without needing a special build environment or vast compiler suites permanently in my PATH). The build is slightly complicated because you need to build flexdll directly. Make sure you have Cygwin base with with Devel\make and Devel\subversion added I installed the Win7 SDK to C:\Dev\WinSDK (though it still irritatingly puts the compilers in C:\Program Files (x86)\Microsoft Visual Studio 9.0\VC). I didn’t bother installing Documentation, Samples or the IA64 libraries. Add the following to your LIB environment variable: C:\Program Files (x86)\Microsoft Visual Studio 9.0\VC\lib\amd64;C:\Dev\WinSDK\lib\x64 Add the following to your INCLUDE environment variable: C:\Program Files (x86)\Microsoft Visual Studio 9.0\vc\include;C:\Dev\WinSDK\Include Set OCAMLLIB to C:\Dev\OCaml-MSVC64\lib A whole load of files now get copied to C:\Dev\OCaml-MSVC64\bin: From C:\Cygwin\bin, copy cygpath.exe and cygwin1.dll (needed by flexlink) Extract flexdll.h, default.manifest and flexlink.exe from the flexdll 0.19 x86 binaries (latest flexlink tool – doesn’t need to be x64) From C:\Program Files (x86)\Microsoft Visual Studio\9.0\VC\bin\amd64, copy: 1033\clui.dll (this needs to be in C:\Dev\OCaml-MSVC64\bin\1033) ml64.exe, cl.exe, c1.dll, c2.dll, cvtres.exe, link.exe and mspdb80.dll From C:\Dev\WinSDK\Bin\x64, copy mt.exe Or workaround that stupidity by having C:\Cygwin\bin and the other directories in your PATH Start Bash (possibly as Administrator depending on permissions set on C:\Dev) I placed the ocaml 3.11.1 tarball in C:\Dev\Src-MSVC64 Note that the sed instruction not only sets PREFIX but it also removes bufferoverflowu.lib from EXTRALIBS – apparently this is no longer needed in this version of the SDK (presumably the compiler has started to include all the required support natively or perhaps the runtime now has it). $ cd /cygdrive/c/Dev/Src-MSVC64 $ svn co svn://frisch.fr/flexdll/trunk flexdll-dev $ cd flexdll-dev $ make CHAINS=msvc flexdll_msvc.obj flexdll_initer_msvc.obj $ cp *.obj /cygdrive/c/Dev/OCaml-MSVC64/bin $ cd .. $ tar -xzf ocaml-3.11.tar.gz $ cd ocaml-3.11 $ cp config/m-nt.h config/m.h $ cp config/s-nt.h config/s.h $ sed -e '20s/=.*$/=C:\/Dev\/OCaml-MSVC64/' -e '92s/=.*/=/' config/Makefile.msvc64 config/Makefile $ make -f Makefile.nt world opt opt.opt install And you should have a fully working MSVC64 build with the Win7 SDK Compilers (and therefore be able to link against the newer libraries). If you wish, quite reasonably, to be a purist and have everything 64-bit you can now go back to flexdll-dev and say: $ sed -i -e 's/afxres.h/windows.h/' version.rc $ rc version.rc $ cvtres /nologo /machine:amd64 /out:version_res.obj version.res $ make version.ml $ ocamlopt -o flexlink.exe -ccopt -link version_res.obj version.ml coff.ml cmdline.ml create_dll.ml reloc.ml $ cp flexlink.exe /cygdrive/c/Dev/OCaml-MSVC64/bin And you’ll have flexlink.exe as a 64-bit executable as well. Best, David From: caml-list-boun...@yquem.inria.fr [mailto:caml-list-boun...@yquem.inria.fr] On Behalf Of Reed Wilson Sent: 02 September 2009 05:44 To: caml-list@yquem.inria.fr Subject: [Caml-list] Windows Vista/7 specific functions Hi all, I am going to be writing a native-code 64-bit program which takes advantage of some Windows Vista-only features (transactional NTFS), and I was wondering how to get it working in OCaml. I have made numerous interfaces to Windows XP functions, but the problem is that the NTFS transactional functions are only available through MSVS 2008 and the Vista/7 SDKs, which OCaml seems
Re: [Caml-list] batteries compilation error
Excerpts from Florent Monnier's message of Tue Sep 01 11:14:49 +0200 2009: Hi, Hi, Trying to compile batteries (version 20090405 on ocaml 3.11.1), I get this error: + ocamlfind ocamlc -c -g -I src/syntax/pa_strings -I src -I src/core -I src/main -I src/libs -I src/core/extlib_threads -I src/core/extlib -I src/core/baselib -I src/core/baselib_threads -I src/libs/common -I src/libs/camlzip -I src/libs/sexplib -I src/libs/findlib -I src/libs/compilers -I src/libs/ocamlnet -I build/optcomp -o src/syntax/pa_strings/pa_estring.cmi src/syntax/pa_strings/pa_estring.mli File src/syntax/pa_strings/pa_estring.mli, line 12, characters 0-19: Error: Unbound module Camlp4.PreCast this line 12 is only: open Camlp4.PreCast Does someone have an idea of what could cause this error ? I don't see any -I +camlp4 can you add it? -- Nicolas Pouillard http://nicolaspouillard.fr ___ Caml-list mailing list. Subscription management: http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list Archives: http://caml.inria.fr Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports: http://caml.inria.fr/bin/caml-bugs
Re: [Caml-list] Compiling OCaml under OS X 10.6
On Tue, Sep 1, 2009 at 12:32, John Whitingtonj...@coherentgraphics.co.uk wrote: Has anyone managed this? Bytecode seems fine, native not so. I haven't compiled it under 10.6, but FWIW my 64bit Godi installation of OCaml kept working just fine after the upgrade. Regards, Markus -- Markus Mottlhttp://www.ocaml.infomarkus.mo...@gmail.com ___ Caml-list mailing list. Subscription management: http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list Archives: http://caml.inria.fr Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports: http://caml.inria.fr/bin/caml-bugs
Re: [Caml-list] batteries compilation error
Trying to compile batteries (version 20090405 on ocaml 3.11.1), I get this error: + ocamlfind ocamlc -c -g -I src/syntax/pa_strings -I src -I src/core -I src/main -I src/libs -I src/core/extlib_threads -I src/core/extlib -I src/core/baselib -I src/core/baselib_threads -I src/libs/common -I src/libs/camlzip -I src/libs/sexplib -I src/libs/findlib -I src/libs/compilers -I src/libs/ocamlnet -I build/optcomp -o src/syntax/pa_strings/pa_estring.cmi src/syntax/pa_strings/pa_estring.mli File src/syntax/pa_strings/pa_estring.mli, line 12, characters 0-19: Error: Unbound module Camlp4.PreCast this line 12 is only: open Camlp4.PreCast Does someone have an idea of what could cause this error ? I don't see any -I +camlp4 can you add it? if I run the command like this on the command line it passes right but when I run again the make command it doesn't continue because ocamlbuild complains about sanity violation Anyway as it is for packaging purpose I will need to patch the Makefile, the problem is that I don't see where to add this statement in the Makefile: http://git.ocamlcore.org/cgi-bin/gitweb.cgi?p=batteries/batteries.git;a=blob;f=Makefile.in;hb=HEAD (also I've search in the debian package, and it seems they haven't patch the Makefile at all) ___ Caml-list mailing list. Subscription management: http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list Archives: http://caml.inria.fr Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports: http://caml.inria.fr/bin/caml-bugs
[Caml-list] Ocaml clone detector
Hi everyone. I think you can help me. I want to know there is a clone detector for Ocaml program. If you know any program like that, please let me know. Cheers, -- Kihong Heo kh...@ropas.snu.ac.kr Programming Research Lab. Seoul National University ___ Caml-list mailing list. Subscription management: http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list Archives: http://caml.inria.fr Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports: http://caml.inria.fr/bin/caml-bugs
Re: [Caml-list] Ocaml clone detector
Kihong Heo wrote: I want to know there is a clone detector for Ocaml program. Maybe it would help if you explained what a clone detector is. Erik -- -- Erik de Castro Lopo http://www.mega-nerd.com/ ___ Caml-list mailing list. Subscription management: http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list Archives: http://caml.inria.fr Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports: http://caml.inria.fr/bin/caml-bugs
Re: [Caml-list] Ocaml clone detector
Erik de Castro Lopo wrote: Maybe it would help if you explained what a clone detector is. A clone is software-engineering speak for duplicated code. Exactly what qualifies as 'duplicated code' and how to efficiently find such (without too many false positives nor false negatives) is still fairly active research. This is a huge issue in languages without decent abstraction features, and less so otherwise (or so it seems). Jacques ___ Caml-list mailing list. Subscription management: http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list Archives: http://caml.inria.fr Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports: http://caml.inria.fr/bin/caml-bugs
Re: [Caml-list] Compiling OCaml under OS X 10.6
On Sep 1, 2009, at 12:32 PM, John Whitington wrote: Hi Folks, Has anyone managed this? Bytecode seems fine, native not so. I've tried just ./configure and ./configure -cc gcc -m64 with the source bzip of 3.11.1 as suggested in INSTALL. Both compile fine, but give: feast:trunk john$ ocamlopt -c a.ml feast:trunk john$ ocamlopt -o a a.cmx ld: warning: in libasmrun.a, file is not of required architecture Undefined symbols: _caml_ml_set_binary_mode, referenced from: .L139 in stdlib.a(pervasives.o) .L157 in stdlib.a(pervasives.o) _camlPervasives__102 in stdlib.a(pervasives.o) _camlPervasives__102 in stdlib.a(pervasives.o) ... (several hundred more lines) This is with XCode 3.2 64-bit (from the Snow Leopard DVD), the gcc is i686-apple-darwin10-gcc-4.2.1. lipo -info libasmrun.a gives: input file /usr/local/lib/ocaml/libasmrun.a is not a fat file Non-fat file: /usr/local/lib/ocaml/libasmrun.a is architecture: x86_64 One possibly-salient error from the build: ld: warning: -read_only_relocs cannot be used with x86_64 Configure log: http://www.coherentpdf.com/configure.txt make world.opt log: http://www.coherentpdf.com/build.txt I just installed Snow Leopard in my laptop and the x86_64 ocaml appears to work fine. I noticed that in your configure log the gcc compiler is still listed at the end as 'gcc', while in mine it is 'gcc -m64'. Perhaps you need to cleanup with 'make distclean' and reconfigure before compiling the x86_64 target? Another question: Can I build a version of OCaml from these sources which isn't 64-bit so I can build code which will run on 10.5/10.4? Previous versions of gcc in Mac OS X allowed you to pass the -mmacosx- version-min=10.4 option to target the minimum API that you wanted to support. I suppose this still works with the gcc 4.2.1 included in XCode 3.2, but haven't tried it yet. Andres Cheers, -- John Whitington Coherent Graphics Ltd http://www.coherentpdf.com/ ___ Caml-list mailing list. Subscription management: http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list Archives: http://caml.inria.fr Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports: http://caml.inria.fr/bin/caml-bugs smime.p7s Description: S/MIME cryptographic signature ___ Caml-list mailing list. Subscription management: http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list Archives: http://caml.inria.fr Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports: http://caml.inria.fr/bin/caml-bugs
Re: [Caml-list] Ocaml clone detector
Jacques Carette wrote: Erik de Castro Lopo wrote: Maybe it would help if you explained what a clone detector is. A clone is software-engineering speak for duplicated code. Exactly what qualifies as 'duplicated code' and how to efficiently find such (without too many false positives nor false negatives) is still fairly active research. This is a huge issue in languages without decent abstraction features, and less so otherwise (or so it seems). Thanks for the explanation. I can think of two situations where such a clone detector may be useful; for finding similar chunks of code so that they may be refactored for software QA management and for detecting plaguarism in student programming assignments. I suspect that these two kinds of clone detectors would actually be quite different. Cheers, Erik -- -- Erik de Castro Lopo http://www.mega-nerd.com/ ___ Caml-list mailing list. Subscription management: http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list Archives: http://caml.inria.fr Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports: http://caml.inria.fr/bin/caml-bugs
Re: [Caml-list] Ocaml clone detector
As far as student plagiarism goes, we found out that for Java
programs, you can pretty much detect frauds by erasing everything from
the programs except parentheses ( ) { } and then comparing the
remaining strings for editing distance. My explanation is that
students who copy code don't want to spend much time on it. In order
to chance the parenthesis they would have to understand the structure
of the program, which they don't.
Andrej
___
Caml-list mailing list. Subscription management:
http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
Archives: http://caml.inria.fr
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs
