[Hol-info] Problem loading HolSmtLib

Hi Fellows Visiting the HOL world after a long time. Installed HOL under Linux (RHEL 3 and also on Mac OSX-Intel), looks like a clean installation. Most basic libraries load and work well (including HolSatLib) except for HolSmtLib.  When I load the HolSmtLib at the HOL prompt, I get the

Re: [Hol-info] Problem loading HolSmtLib

From: Tom Ridge t...@leicester.ac.uk To: Ashish Darbari ash...@darbari.org Cc: hol-info@lists.sourceforge.net hol-info@lists.sourceforge.net Sent: Tuesday, 10 January 2012, 16:44 Subject: Re: [Hol-info] Problem loading HolSmtLib Are you using mosml? I have no information

[Hol-info] Formal Verification Opportunity at Imagination Technologies UK

All If it is of interest for budding formal verification engineers, my group is looking for a Graduate Engineer to work in the area of formal hardware verification at our UK office. Please get in touch with me if you're interested and for details of the opening see: Vacancy Detail - Imagination

[Hol-info] New positions in formal verification at Imagination Technologies

hunting and building formal proofs is something that you enjoy, then please contact me at ashish.darb...@imgtec.com.  Ashish Darbari,  DPhil (Oxon), FBCS, FIETE, SMACM, SMIEEERoyal Academy of Engineering Visiting ProfessorVisiting Professor University of SouthamptonPrincipal Hardware Design

Re: [Hol-info] HOL 4 Kananaskis 11 Installation Problem

Hi Michael This is what I see when I run Holmake from within the tools/set_mtime directory [adarbari@localhost HOL]$ Holmake --poly_not_hol --no_sigobj --qof bash: Holmake: command not found... I do see Holmakefile executable in that directory. Ashish -- *Dr Ashish Darbari, FBCS

Re: [Hol-info] HOL 4 Kananaskis 11 Installation Problem

ipt Build failed in directory /home/adarbari/HOL/tools/set_mtime (exited with code 1) -- *Dr Ashish Darbari, FBCS, FIETE, DPhil (Oxon)Founder & CEO+44 207 096 0465ashish.darb...@axiomise.com <ashish.darb...@axiomise.com>Axiomise Ltd. Company No: 1101612871-75 Shelton StreetWC2H 9JQ

[Hol-info] HOL 4 Kananaskis 11 Installation Problem

I'm running into this problem on Cent OS 7. No issues reported with Poly ML installation (installation from sources). When running either smart-configure or tweaking by hand the configure.sml file I get Static Errors. Any idea how to fix this? Ashish [adarbari@localhost hol-kananaskis-11]$

Re: [Hol-info] HOL 4 Kananaskis 11 Installation Problem

Ashish Darbari, FBCS, FIETE, DPhil (Oxon)Founder & CEO+44 207 096 0465ashish.darb...@axiomise.com <ashish.darb...@axiomise.com>Axiomise Ltd. Company No: 1101612871-75 Shelton StreetWC2H 9JQ* *London, UK* On 23 May 2018 at 11:44, Chun Tian <binghe.l...@gmail.com> wrote: >

[Hol-info] Training: Getting Started with Formal Verification

with formal for hardware verification then this course is ideal. Price: £350 for students, £475 for professionals Where: Reading, UK When: 24 Jan 2019 More information: www.axiomise.com/formal_training Ashish -- *Dr Ashish Darbari, FBCS, FIETE, DPhil (Oxon)Founder & CEO+44 207

[Hol-info] Unique on-demand course in applied formal methods

-- *Dr Ashish Darbari, FBCS, FIETE, DPhil (Oxon)Founder & ceoashish.darb...@axiomise.com Axiomise Ltd. Company No: 1101612871-75 Shelton StreetWC2H 9JQ* *London, UK* ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge