Discussion of the HOL proof systems ()

Marco Roveri | 3 Dec 2007 22:11

Picon

Developer Positions in the Embedded System Unit of Fondazione Bruno Kessler


         [[[ Apologies for multiple copies of this message ]]]

                 Programmer Positions Available

             Design and Verification of Embedded Software

                    Embedded System Research Unit
                      Fondazione Bruno Kessler
 (formerly part of IRST - Centro per la Ricerca Scientifica e Tecnologica)
                           Trento, Italy

The Embedded System Research Unit (http://es.fbk.eu) of the Bruno
Kessler Foundation, Trento, Italy, is seeking several skilled
programmers for software development in research projects.

The successful candidates will be enrolled with a fixed length
contract, and will be subject to a trial work period.

Candidate Profile
=================

The ideal candidate should have an MS or equivalent degree in computer
science, mathematics or electronic engineering, and have excellent
software design and development skills.

The candidate should be able to work in a collaborative environment,
with a strong commitment to developing high-quality software, and
achieving assigned objectives.

(Continue reading)

Marco Roveri | 3 Dec 2007 22:11

Picon

Post-Doc Positions in the Embedded System Unit of Fondazione Bruno Kessler


         [[[ Apologies for multiple copies of this message ]]]

                   Post-Doc Positions Available

             Design and Verification of Embedded Software

                    Embedded System Research Unit
                      Fondazione Bruno Kessler
 (formerly part of IRST - Centro per la Ricerca Scientifica e Tecnologica)
                           Trento, Italy

        Deadlines: Dec. 15, 2007

The Embedded System Research Unit (http://es.fbk.eu) of the Bruno
Kessler Foundation, Trento, Italy, is seeking several candidates for
Post-Doc positions.

The activities will target algorithms, methodologies and tools for the
design and verification of Embedded Systems. The activities will mainly
focus on the following topics:

- Safety Analysis with focus on Dynamic Fault Tree Analysis
- Formal Requirements Analysis
- Verification of Hybrid Systems
- Verification of SystemC TLM models
- Optimization of Design and Installation of Aircraft Architectures

The activities will be carried out within two European Projects of the
7th framework, scheduled to start in 2008:

(Continue reading)

Marco Roveri | 3 Dec 2007 22:11

Picon

PhD Positions in the Embedded System Unit of Fondazione Bruno Kessler


         [[[ Apologies for multiple copies of this message ]]]

                 Doctoral Student Positions Available

             Design and Verification of Embedded Software

                    Embedded System Research Unit
                      Fondazione Bruno Kessler
 (formerly part of IRST - Centro per la Ricerca Scientifica e Tecnologica)
                           Trento, Italy

        Deadlines:  Dec. 15, 2007

The Embedded System Research Unit (http://es.fbk.eu) of the Bruno
Kessler Foundation, Trento, Italy, is seeking several candidates for Ph.D
positions.

The Ph.D. studies will be held at the International Doctorate School
in Information and Communication Technologies
(http://www.ict.unitn.it/) of the University of Trento, Italy.

The research activity will be carried out within the Embedded Systems
Unit of the Center for Scientific and Technological Research of the
Fondazione Bruno Kessler.

The research activity will aim at techniques, methodologies and support
tools for the design and verification of embedded systems. In
particular, possible topics will include:

(Continue reading)

PLAS2008 | 3 Dec 2007 23:34

Picon

Call for Papers: PLAS 2008

                    ACM SIGPLAN Third Workshop on
     Programming Languages and Analysis for Security (PLAS 2008)

                    Tucson, Arizona, June 8, 2008

         Sponsored by ACM SIGPLAN and co-located with PLDI'08

                 http://research.ihost.com/plas2008/

                 Submission Deadline: March 24, 2008

Call for Papers

PLAS aims to provide a forum for exploring and evaluating ideas on the
use of programming language and program analysis techniques to improve
the security of software systems. Strongly encouraged are proposals of
new, speculative ideas; evaluations of new or known techniques in
practical settings; and discussions of emerging threats and important
problems.

The scope of PLAS includes, but is not limited to:

  * Language-based techniques for security
  * Verification of security properties in software
  * Automated introduction and/or verification of security enforcement
    mechanisms
  * Program analysis techniques for discovering security vulnerabilities
  * Compiler-based security mechanisms, such as host-based intrusion
    detection and in-line reference monitors
  * Specifying and enforcing security policies for information flow

(Continue reading)

Icalp08 | 5 Dec 2007 11:18

Picon

ICALP 2008: Second Call for Papers


*** We apologize for multiple postings ****

HTML version of the CFP: http://www.ru.is/icalp08/cfp.html

___________________________________________________________________

                    CALL FOR PAPERS - ICALP'08

                 35th International Colloquium on
               Automata,  Languages and Programming

                July 6-13, 2008, Reykjavik, Iceland

                    http://www.ru.is/icalp08

___________________________________________________________________

The 35th International Colloquium on Automata, Languages and
Programming, the main conference and annual meeting of the European
Association for Theoretical Computer Science EATCS will take place
from the 6th to the 13th of July 2008 in Reykjavik, Iceland. The main
conference will take place from the 7th till the 11th of July, and
will be preceded and followed by 13 co-located events. (See
http://www.ru.is/icalp08/workshops.html for the list of events
affiliated with ICALP 2008.) In addition, the ETACS award 2008 and the
Goedel prize 2008 will be awarded at the conference.

Following the successful experience of the last three editions, ICALP
2008 will complement the established structure of the scientific

(Continue reading)

demis | 5 Dec 2007 18:58

Picon

CfPart: 3rd Int'l Workshop on Automated Specification and Verification of Web Systems (WWV'07)

             -- We apologize for multiple copies --

*******************************************************************
******************    Call for participation    *******************
*******************************************************************

             3rd International Workshop on Automated
                  Specification and Verification
                      of Web Sites (WWV'07)

          December 14, 2007, San Servolo, Venice (Italy)

                    http://wwv07.dimi.uniud.it

           EARLY REGISTRATION DEADLINE: DECEMBER 11th
*******************************************************************

WWV'07 will  be held in Venice (Italy) in the  convention centre of 
the island of San Servolo.

SCOPE

The  increased  complexity  of Web sites and the explosive growth of
Web-based applications has turned their design and construction into
a  challenging problem. Nowadays, many companies have diverted their
Web   sites   into   interactive,   completely-automated,  Web-based
applications (such  as  Amazon, on-line banking, or travel agencies)
with  a  high complexity that requires appropriate specification and
verification  techniques and tools. Systematic, formal approaches to
the  analysis  and  verification  can  address  the problems of this

(Continue reading)

paige | 6 Dec 2007 23:31

Picon

(no subject)

Apologies for any cross-posting.

---

		PRELIMINARY CALL FOR PAPERS
		Second IFIP Working Conference on
	Verified Software: Theories, Tools, and Experiments

				VSTTE 2008
		http://qpq.csl.sri.com/vsr/vstte-08
		Oct 6--10, 2008, Toronto, Canada

Program Chairs:
Jim Woodcock, University of York, jim <at> cs.york.ac.uk
Natarajan Shankar, SRI International, shankar <at> csl.sri.com

Program Committee:

Egon Borger, Supratik Chakraborty, Patrick Cousot, Jin Song Dong,
Jose Luiz Fiadeiro, Kokichi Futatsugi, Chris George, Ian Hayes,
Eric Hehner, Rajeev Joshi, Joseph Kiniry, Yassine Lakhnech,
Gary Leavens, Zhiming Liu, Peter Manolios, Tiziana Margaria,
David Naumann, Peter O'Hearn, Ernst-Rudiger Olderog, Wolfgang Paul,
Augusto Sampaio, Mark Utting, Jian Zhang

Conference Chair:
Eric Hehner, University of Toronto, hehner <at> cs.utoronto.ca

Workshop Chair: tba

(Continue reading)

Juliano Iyoda | 7 Dec 2007 01:45

Picon

ELIM_SELECT_RULE

Hello,

Does anyone know what ELIM_SELECT_RULE does?

Cheers,

Juliano

-------------------------------------------------------------------------
SF.Net email is sponsored by: 
Check out the new SourceForge.net Marketplace.
It's the best place to buy or sell services for
just about anything Open Source.
http://sourceforge.net/services/buy/index.php

Michael Norrish | 7 Dec 2007 04:06

Picon

Re: ELIM_SELECT_RULE

Juliano Iyoda wrote:
 > Hello,
 >
 > Does anyone know what ELIM_SELECT_RULE does?

I don't know what function you mean.  I just did a grep -R for it
across the HOL sources, and couldn't find any mention of it.

There is a SELECT_ELIM_TAC; is this what you mean?  This is documented at

http://hol.sourceforge.net/kananaskis-4-helpdocs/help/Docfiles/HTML/Tactic.SELECT_ELIM_TAC.html

(This documentation is accessible in ASCII form by doing

   help "SELECT_ELIM_TAC"

within HOL.  You can also find the HTML locally at

  help/HOLindex.html

Michael.

-------------------------------------------------------------------------
SF.Net email is sponsored by: 
Check out the new SourceForge.net Marketplace.
It's the best place to buy or sell services for
just about anything Open Source.
http://sourceforge.net/services/buy/index.php

Andrei Sabelfeld | 7 Dec 2007 13:45

Picon

Picon

IEEE Computer Security Foundations Symposium (CSF 2008)

[New: We are proud to announce a joint CSF/LICS invited speaker: David Basin.]

		   Call For Papers/Panels/Workshops

       21st IEEE Computer Security Foundations Symposium (CSF)
		Pittsburgh, PA, USA, June 23-25, 2008

     Sponsored by the Technical Committee on Security and Privacy
		     of the IEEE Computer Society

CSF 2008 website:  http://www.cylab.cmu.edu/CSF2008/
CSF home page:     http://www.ieee-security.org/CSFWweb/
CSF CFP:           http://www.cs.chalmers.se/~andrei/CSF08/cfp.html

The IEEE Computer Security Foundations (CSF) series brings together
researchers in computer science to examine foundational issues in
computer security. Over the past two decades, many seminal papers and
techniques have been presented first at CSF. The CiteSeer Impact page
(http://citeseer.ist.psu.edu/impact.html ) lists CSF as 38th out of
more than 1200 computer science venues, top 3.11% in impact based on
citation frequency.

This year's CSF will be colocated with the 23rd IEEE Symposium on
Logic in Computer Science (LICS). It will be held at Carnegie Mellon
University in Pittsburgh, Pennsylvania, USA.

We are proud to announce a joint CSF/LICS invited speaker: David Basin.

New theoretical results in computer security are welcome. Also welcome
are more exploratory presentations, which may examine open questions

(Continue reading)

Group

gmane.comp.mathematics.hol.

Project Web Page

Discussion of the HOL proof systems ()

Search Archive

Page

1 | 2 | 3

Articles in period: 24

December 2007

Language

Change language

Options

Current view: Threads only / Showing only 20 lines / Not hiding cited text.
Change to All messages, whole messages, or hide cited text.

Post a message
NNTP Newsgroup
Classic Gmane web interface
XML

XML

RSS Feed
List Information

About Gmane

Recent entries

LFMTP'13: Logical Frameworks and Meta-Languages (CFP) (22 May 2013)
2nd CfP: OpenMath workshop at CICM (10 July, Bath, UK), submission dea (20 May 2013)
SSTiC 2013: next registration deadline 26 May (19 May 2013)
ECSCW 2013: Doctoral Colloquium (19 May 2013)
CFP FOCLASA 2013: The 13th International Workshop on Foundations of Co (17 May 2013)
CiE 2013 in Milan, July 1 - 5: First Call for Participation (16 May 2013)
Induction in HOL4. (16 May 2013)
[fm-announcements] webcast of NFM 2013 (14 May 2013)
How to throw exception defined by user in HOL4 (14 May 2013)
RDP 2013 Call for Participation (14 May 2013)
(CFP) Certified Programs and Proofs 2013 - Second Call for Papers (10 May 2013)
*Deadline Extension* PLMMS, 9th July 2013, Bath, UK (9 May 2013)
MEMOCODE 2013 Call for Papers and Design Contest (EXTENDED DATES) (7 May 2013)
MEMOCODE Design Contest 2013 -- start May 15 (6 May 2013)
FMCAD 2013 Final Call for Papers (7 May 2013)
DIFTS'13: First Call For Papers (2 May 2013)
VeriSure Workshop Call for Papers (3 May 2013)
MCS: Formal Proofs for Mathematics and Computer Science [Call for Pape (6 May 2013)
VSTTE 2013 Call for Participation (2 May 2013)
[fm-announcements] Third Summer School on Formal Techniques (1 May 2013)
[fm-announcements] VSTTE 2013: Call for participation (1 May 2013)

Archives

41	May 2013
121	April 2013
39	March 2013
33	February 2013
77	January 2013
56	December 2012
61	November 2012
42	October 2012
31	September 2012
153	August 2012
130	July 2012
114	June 2012
186	May 2012
70	April 2012
59	March 2012
35	February 2012
34	January 2012
18	December 2011
22	November 2011
26	October 2011
19	September 2011
13	August 2011
11	July 2011
26	June 2011
37	May 2011
46	April 2011
28	March 2011
39	February 2011
29	January 2011
23	December 2010
28	November 2010
28	October 2010
37	September 2010
8	August 2010
19	July 2010
33	June 2010
35	May 2010
38	April 2010
56	March 2010
28	February 2010
36	January 2010
21	December 2009
31	November 2009
18	October 2009
20	September 2009
12	August 2009
23	July 2009
32	June 2009
27	May 2009
33	April 2009
21	March 2009
17	February 2009
23	January 2009
33	December 2008
27	November 2008
28	October 2008
19	September 2008
12	August 2008
20	July 2008
21	June 2008
25	May 2008
53	April 2008
25	March 2008
19	February 2008
16	January 2008
24	December 2007
20	November 2007
23	October 2007
16	September 2007

Design

Zawodny | Right Menu | Left Menu

Your Own Design

Paste the URL of your CSS below. Download CSS template