You can subscribe to this list here.
2003 
_{Jan}

_{Feb}

_{Mar}

_{Apr}

_{May}

_{Jun}

_{Jul}

_{Aug}
(12) 
_{Sep}
(8) 
_{Oct}
(20) 
_{Nov}
(21) 
_{Dec}
(3) 

2004 
_{Jan}
(16) 
_{Feb}
(11) 
_{Mar}
(26) 
_{Apr}
(15) 
_{May}
(17) 
_{Jun}
(10) 
_{Jul}
(3) 
_{Aug}
(4) 
_{Sep}
(11) 
_{Oct}

_{Nov}
(11) 
_{Dec}
(8) 
2005 
_{Jan}
(16) 
_{Feb}
(18) 
_{Mar}
(22) 
_{Apr}
(23) 
_{May}
(17) 
_{Jun}
(22) 
_{Jul}
(10) 
_{Aug}
(9) 
_{Sep}
(13) 
_{Oct}
(26) 
_{Nov}
(26) 
_{Dec}
(31) 
2006 
_{Jan}
(29) 
_{Feb}
(35) 
_{Mar}
(20) 
_{Apr}
(23) 
_{May}
(35) 
_{Jun}
(17) 
_{Jul}
(18) 
_{Aug}
(11) 
_{Sep}
(18) 
_{Oct}
(12) 
_{Nov}
(16) 
_{Dec}
(27) 
2007 
_{Jan}
(27) 
_{Feb}
(22) 
_{Mar}
(15) 
_{Apr}
(38) 
_{May}
(26) 
_{Jun}
(24) 
_{Jul}
(8) 
_{Aug}
(20) 
_{Sep}
(21) 
_{Oct}
(23) 
_{Nov}
(20) 
_{Dec}
(24) 
2008 
_{Jan}
(16) 
_{Feb}
(19) 
_{Mar}
(24) 
_{Apr}
(54) 
_{May}
(24) 
_{Jun}
(21) 
_{Jul}
(20) 
_{Aug}
(12) 
_{Sep}
(19) 
_{Oct}
(28) 
_{Nov}
(26) 
_{Dec}
(34) 
2009 
_{Jan}
(22) 
_{Feb}
(15) 
_{Mar}
(20) 
_{Apr}
(33) 
_{May}
(27) 
_{Jun}
(30) 
_{Jul}
(23) 
_{Aug}
(13) 
_{Sep}
(21) 
_{Oct}
(19) 
_{Nov}
(29) 
_{Dec}
(22) 
2010 
_{Jan}
(36) 
_{Feb}
(30) 
_{Mar}
(58) 
_{Apr}
(38) 
_{May}
(36) 
_{Jun}
(35) 
_{Jul}
(22) 
_{Aug}
(8) 
_{Sep}
(40) 
_{Oct}
(27) 
_{Nov}
(29) 
_{Dec}
(23) 
2011 
_{Jan}
(31) 
_{Feb}
(39) 
_{Mar}
(30) 
_{Apr}
(49) 
_{May}
(38) 
_{Jun}
(27) 
_{Jul}
(11) 
_{Aug}
(13) 
_{Sep}
(20) 
_{Oct}
(28) 
_{Nov}
(23) 
_{Dec}
(18) 
2012 
_{Jan}
(36) 
_{Feb}
(39) 
_{Mar}
(61) 
_{Apr}
(71) 
_{May}
(188) 
_{Jun}
(117) 
_{Jul}
(132) 
_{Aug}
(153) 
_{Sep}
(32) 
_{Oct}
(44) 
_{Nov}
(64) 
_{Dec}
(56) 
2013 
_{Jan}
(85) 
_{Feb}
(36) 
_{Mar}
(44) 
_{Apr}
(130) 
_{May}
(47) 
_{Jun}
(33) 
_{Jul}
(34) 
_{Aug}
(25) 
_{Sep}
(20) 
_{Oct}
(49) 
_{Nov}
(20) 
_{Dec}
(39) 
2014 
_{Jan}
(38) 
_{Feb}
(61) 
_{Mar}
(83) 
_{Apr}
(56) 
_{May}
(42) 
_{Jun}
(37) 
_{Jul}
(24) 
_{Aug}
(16) 
_{Sep}
(28) 
_{Oct}
(33) 
_{Nov}
(21) 
_{Dec}
(22) 
2015 
_{Jan}
(12) 
_{Feb}
(43) 
_{Mar}
(46) 
_{Apr}
(36) 
_{May}
(57) 
_{Jun}
(29) 
_{Jul}
(19) 
_{Aug}
(21) 
_{Sep}
(17) 
_{Oct}
(20) 
_{Nov}
(77) 
_{Dec}
(30) 
2016 
_{Jan}
(20) 
_{Feb}
(39) 
_{Mar}
(53) 
_{Apr}
(32) 
_{May}
(47) 
_{Jun}
(53) 
_{Jul}
(30) 
_{Aug}
(17) 
_{Sep}
(17) 
_{Oct}
(51) 
_{Nov}

_{Dec}

S  M  T  W  T  F  S 





1

2

3

4

5

6

7

8

9

10

11

12
(1) 
13
(2) 
14
(2) 
15

16

17

18
(2) 
19
(1) 
20
(1) 
21
(1) 
22

23
(1) 
24

25

26
(4) 
27

28
(1) 
29

30
(1) 

From: <Laurent.V<igneron@lo...>  20060630 23:28:34

[We apologize if you received multiple copies of this message] XXX X X XXXXX XXXXX XXXXXX XXX X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X XXXXXXX X X X XXXXX XXXXXX XXXXXXX X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X XXXXX XXXXX X X X V E R S I O N 1 . 1 (June 30, 2006) We are happy to announce the availability of a new version of the AVISPA Tool, a pushbutton tool for the Automatic Validation of Internet Securitysensitive Protocols and Applications. The AVISPA Tool v1.1 is available at http://www.avispaproject.org The AVISPA Tool v1.1 includes several bug fixes and extends the previous versions of the AVISPA Tool with several new features (see the NEWS section below). ======== OVERVIEW ======== The AVISPA Tool is a pushbutton tool for the automated validation of Internet securitysensitive protocols and applications. It provides a modular and expressive formal language (called HLPSL) for specifying protocols and their security properties, and integrates different backends that implement a variety of stateoftheart automatic analysis techniques ranging from protocol falsification (by finding an attack on the input protocol) to abstractionbased verification methods for both finite and infinite numbers of sessions. The HLPSL is an expressive, modular, rolebased, formal language that allows for the specification of control flow patterns, datastructures, complex security properties, as well as different cryptographic primitives and their algebraic properties. These features make HLPSL well suited for specifying modern, industrialscale protocols. Moreover, the HLPSL enjoys both a declarative semantics based on a fragment of the Temporal Logic of Actions and an operational semantics based on a translation into the rewritebased formalism Intermediate Format IF. The AVISPA Tool automatically translates HLPSL specifications into equivalent IF specifications which are in turn fed to the backends. The following backends are integrated in the AVISPA Tool: * The Onthefly ModelChecker (OFMC) performs protocol falsification and bounded verification by exploring the transition system described by an IF specification in a demanddriven way. OFMC implements a number of correct and complete symbolic techniques. It supports the specification of algebraic properties of cryptographic operators, and typed and untyped protocol models. * The ConstraintLogicbased Attack Searcher (CLAtSe) applies constraint solving with some powerful simplification heuristics and redundancy elimination techniques. CLAtSe is built in a modular way and is open to extensions for handling algebraic properties of cryptographic operators. It supports typeflaw detection and handles associativity of message concatenation. * The SATbased ModelChecker (SATMC) builds a propositional formula encoding a bounded unrolling of the transition relation specified by the IF, the initial state and the set of states representing a violation of the security properties. The propositional formula is then fed to a stateoftheart SAT solver and any model found is translated back into an attack. * The TA4SP (Tree Automata based on Automatic Approximations for the Analysis of Security Protocols) backend approximates the intruder knowledge by using regular tree languages and rewriting. For secrecy properties, TA4SP can show whether a protocol is flawed (by underapproximation) or whether it is safe for any number of sessions (by overapproximation). In order to demonstrate the effectiveness of the AVISPA Tool on a large collection of practically relevant, industrial protocols, we have selected a substantial set of security problems associated with protocols that have recently been or are currently being standardized by organizations like the Internet Engineering Task Force IETF. We have then formalized in HLPSL a large subset of these protocols, and the result of this specification effort is the AVISPA Library (publicly available at the AVISPA webpage), which at present comprises 112 security problems derived from 33 protocols. Further details on the AVISPA Tool and on the AVISPA project can be found in the paper: A. Armando, D. Basin, Y. Boichut, Y. Chevalier, L. Compagna, J. Cuellar, P. Hankes Drielsma, P.C. Heam, O. Kouchnarenko, J. Mantovani, S. Moedersheim, D. von Oheimb, M. Rusinowitch, J. Santiago, M. Turuani, L. Vigano`, L. Vigneron. "The AVISPA Tool for the Automated Validation of Internet Security Protocols and Applications." In Proc. CAV'05, LNCS. Springer Verlag, 2005, Available at the URL http://www.avispaproject.org/avispacav05.ps ==== NEWS ==== * All known bugs have been fixed. * All backends have been optimised for improved performance. * The translator from HLPSL to IF has been improved, with only minor changes in the syntax:  The HLPSL type "function" being too ambiguous, it has been renamed "hash_func".  More semantic tests are done for detecting incomplete goal specifications or missing new() assignments.  The handling of sets has been simplified in the translator.  Predefined constant functions, like xor and exp, are better handled.  Warning and error messages are more precise. * OFMC, CLAtSe, and SATMC support userdefined (non temporal) security goals. * OFMC now supports reasoning modulo a userspecified algebraic theory. * CLAtse has improved in many ways:  Algebraic properties : CLAtse now supports complete analysis of cryptographic protocols modulo the xor, including all the intruder deduction rules for that operator. CLAtse also implements complete analysis modulo the exponential except for the rule g^1 = g (i.e. exponentials are tagged). Also, some improvements on the code for algebraic properties (speed, bug correction, etc.) have been added.  The protocol optimisation module now allows CLAtse to perform advanced optimisations of the protocol specification before the analysis, and may greatly reduce the analysis time. Now, CLAtse can statically decide the origin of certain messages and reduce the nondeterminism of the analysis accordingly.  User interaction (output presentation, options, etc..) improved. * The AVISPA XEmacs mode has been improved and it is now a powerful environment for writing protocol specifications and analysing them. * A new contribution has been added: hlpsldoc. It contains script files that automatically generate either a LaTeX file or a HTML file from a HLPSL specification. It has been used to generate the online AVISPA library. ======== PARTNERS ======== The following research groups have contributed to the development of the AVISPA Tool: * Artificial Intelligence Laboratory, Dipartimento di Informatica, Sistemistica e Telematica (DIST), University of Genova, Italy * Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA UMR 7503) with partners INRIA, CNRS, Universite' Henri Poincare' (UHP) Université Nancy 2 AND Laboratoire d'Informatique de l'Universite' de FrancheComte', France * Eidgenoessische Technische Hochschule Zuerich (ETHZ), Information Security Group, Department of Computer Science, Zuerich, Switzerland * Siemens Aktiengesellschaft, Munich, Germany ================ GETTING IN TOUCH ================ The home page of the AVISPA project is <http://www.avispaproject.org>;. A mailing list for general questions, bugs and bug fixes, possible extensions, and user requests on the AVISPA Tool is available. To register please send an empty message to <avispausersjoinproject.org> New releases and other important events for AVISPA will be also announced on this list.  The AVISPA Team http://www.avispaproject.org 
From: John Harrison <John.H<arrison@cl...>  20060628 19:07:41

Hi Steve,  I'd guess that it's NOT the same bug, because of the last thing I mentioned  in my first Holinfo note on this: Replacing &p and &q by p and q,  redefining p and q as real rather than naturalnumber variables, didn't  help. I think it is the same bug, because adding &p >= &0 constraints makes both work quickly: REAL_SOS `&p >= &0 /\ &q >= &1 /\ &p pow 2 = &2 * &q pow 2 ==> &p +  &1 * &q > &0`;; REAL_SOS `&p >= &0 /\ &q >= &1 /\ &p pow 2 = &2 * &q pow 2 ==> &2 * &q  &p < &p`;; It works over the naturals as well (although subtraction on N means cutoff subtraction, that doesn't matter here): SOS_RULE `q >= 1 /\ p EXP 2 = 2 * q EXP 2 ==> 2 * q  p < p`;; SOS_RULE `q >= 1 /\ p EXP 2 = 2 * q EXP 2 ==> p  q > 0`;;  I had a thought that might be helpful: Wouldn't it make things faster to  have the SOS functions first normalize their inputs using the same sort of  algorithm REAL_FIELD uses, and then continue with the sumofsquares stuff?  That would make them almost as fast as REAL_FIELD on the cases REAL_FIELD  can handle, and it will probably speed things up on the other cases, too. This is certainly the right thing to do, also from a software engineering standpoint. Actually, the same basic algebraic normalization is already done inside the SOS functions. For example, the following example works essentially by normalization without ever calling the SDP solver: REAL_SOS `(((x1 pow 2) + (x2 pow 2) + (x3 pow 2) + (x4 pow 2)) * ((y1 pow 2) + (y2 pow 2) + (y3 pow 2) + (y4 pow 2))) = ((((((x1*y1)  (x2*y2))  (x3*y3))  (x4*y4)) pow 2) + (((((x1*y2) + (x2*y1)) + (x3*y4))  (x4*y3)) pow 2) + (((((x1*y3)  (x2*y4)) + (x3*y1)) + (x4*y2)) pow 2) + (((((x1*y4) + (x2*y3))  (x3*y2)) + (x4*y1)) pow 2))`;; However, some additional preprocessing to add inequalities for injected natural numbers was left out. I'll fix this ASAP, but I'm a bit overloaded for the next few days. John. 
From: Stephen Brackin <stephen.brackin@ve...>  20060626 18:09:48

I'd guess that it's NOT the same bug, because of the last thing I mentioned in my first Holinfo note on this: Replacing &p and &q by p and q, redefining p and q as real rather than naturalnumber variables, didn't help. I had a thought that might be helpful: Wouldn't it make things faster to have the SOS functions first normalize their inputs using the same sort of algorithm REAL_FIELD uses, and then continue with the sumofsquares stuff? That would make them almost as fast as REAL_FIELD on the cases REAL_FIELD can handle, and it will probably speed things up on the other cases, too. Steve > Original Message > From: John Harrison [mailto:John.Harrison@...] > Sent: Monday, June 26, 2006 11:42 AM > To: Stephen Brackin > Cc: holinfo@... > Subject: Re: [Holinfo] Bug in REAL_SOS? > > > Hi Steve, > >  I've found what seems to be a bug in HOL Light's REAL_SOS. It didn't > prove >  >  `&q >= &1 /\ &p pow 2 = &2 * &q pow 2 ==> &p +  &1 * &q > &0` or >  `&q >= &1 /\ &p pow 2 = &2 * &q pow 2 ==> &2 * &q  &p < &p` >  >  In several minutes, although SOS_RULE proved the corresponding "for >  naturals" statements > > This seems to be another case of the bug you identified earlier: > REAL_SOS just doesn't know that injections of naturals (in this > case "&p") are always nonnegative. I'll make sure these cases work > when I fix the bug. > >  When I interrupted the REAL_SOS proof attempts, I sometimes got an error >  message such as Sys_error "/tmp/sosfsbc40.out: No such file or > directory", >  but other times not. > > This is probably because the interrupt hits the semidefinite > programming engine itself. The temporary file is created by that, > and then read in by HOL. > > John. 
From: John Harrison <John.H<arrison@cl...>  20060626 15:42:27

Hi Steve,  I've found what seems to be a bug in HOL Light's REAL_SOS. It didn't prove   `&q >= &1 /\ &p pow 2 = &2 * &q pow 2 ==> &p +  &1 * &q > &0` or  `&q >= &1 /\ &p pow 2 = &2 * &q pow 2 ==> &2 * &q  &p < &p`   In several minutes, although SOS_RULE proved the corresponding "for  naturals" statements This seems to be another case of the bug you identified earlier: REAL_SOS just doesn't know that injections of naturals (in this case "&p") are always nonnegative. I'll make sure these cases work when I fix the bug.  When I interrupted the REAL_SOS proof attempts, I sometimes got an error  message such as Sys_error "/tmp/sosfsbc40.out: No such file or directory",  but other times not. This is probably because the interrupt hits the semidefinite programming engine itself. The temporary file is created by that, and then read in by HOL. John. 
From: Malcolm.N<ewey@cs...>  20060626 09:29:44

Stephen Brackin writes: > I've found what seems to be a bug in HOL Light's REAL_SOS. It didn't prove > > > > `&q >= &1 /\ &p pow 2 = &2 * &q pow 2 ==> &p +  &1 * &q > &0` or > `&q >= &1 /\ &p pow 2 = &2 * &q pow 2 ==> &2 * &q  &p < &p` > > In several minutes, although SOS_RULE proved the corresponding "for > naturals" statements > > `q >= 1 /\ p EXP 2 = 2 * q EXP 2 ==> p  1 * q > 0` and > `q >= 1 /\ p EXP 2 = 2 * q EXP 2 ==> 2 * q  p < p` > > in seconds. Getting rid of the natural numbers altogether didn't help; > REAL_SOS also couldn't prove either of > > `q >= &1 /\ p pow 2 = &2 * q pow 2 ==> p +  &1 * q > &0` or > `q >= &1 /\ p pow 2 = &2 * q pow 2 ==> &2 * q  p < p`. > > When I interrupted the REAL_SOS proof attempts, I sometimes got an error > message such as Sys_error "/tmp/sosfsbc40.out: No such file or directory", > but other times not. > > Steve Brackin > > > > <html xmlns:o="urn:schemasmicrosoftcom:office:office" xmlns:w="urn:schemasmicrosoftcom:office:word" xmlns="http://www.w3.org/TR/REChtml40">; > > <head> > <meta httpequiv=ContentType content="text/html; charset=usascii"> > <meta name=Generator content="Microsoft Word 11 (filtered medium)"> > <style> > <! > /* Style Definitions */ > p.MsoNormal, li.MsoNormal, div.MsoNormal > {margin:0in; > marginbottom:.0001pt; > fontsize:12.0pt; > fontfamily:"Times New Roman";} > a:link, span.MsoHyperlink > {color:blue; > textdecoration:underline;} > a:visited, span.MsoHyperlinkFollowed > {color:purple; > textdecoration:underline;} > pre > {margin:0in; > marginbottom:.0001pt; > fontsize:10.0pt; > fontfamily:"Courier New";} > span.EmailStyle17 > {msostyletype:personalcompose; > fontfamily:Arial; > color:windowtext;} > @page Section1 > {size:8.5in 11.0in; > margin:1.0in 1.25in 1.0in 1.25in;} > div.Section1 > {page:Section1;} > > > </style> > > </head> > > <body lang=ENUS link=blue vlink=purple> > > <div class=Section1> > > <p class=MsoNormal><font size=2 face="Courier New"><span style='fontsize:10.0pt; > fontfamily:"Courier New"'>I’ve found what seems to be a bug in HOL Light’s > REAL_SOS. It didn’t prove<o:p></o:p></span></font></p> > > <p class=MsoNormal><font size=2 face="Courier New"><span style='fontsize:10.0pt; > fontfamily:"Courier New"'><o:p> </o:p></span></font></p> > > <pre><font size=2 face="Courier New"><span style='fontsize:10.0pt'>`&q >= &1 /\ &p pow 2 = &2 * &q pow 2 ==> &p +  &1 * &q > &0` or<o:p></o:p></span></font></pre><pre><font > size=2 face="Courier New"><span style='fontsize:10.0pt'>`&q >= &1 /\ &p pow 2 = &2 * &q pow 2 ==> &2 * &q  &p < &p`<o:p></o:p></span></font></pre><pre><font > size=2 face="Courier New"><span style='fontsize:10.0pt'><o:p> </o:p></span></font></pre><pre><font > size=2 face="Courier New"><span style='fontsize:10.0pt'>In several minutes, although SOS_RULE proved the corresponding “for naturals” statements<o:p></o:p></span></font></pre><pre><font > size=2 face="Courier New"><span style='fontsize:10.0pt'><o:p> </o:p></span></font></pre><pre><font > size=2 face="Courier New"><span style='fontsize:10.0pt'>`q >= 1 /\ p EXP 2 = 2 * q EXP 2 ==> p  1 * q > 0` and<o:p></o:p></span></font></pre><pre><font > size=2 face="Courier New"><span style='fontsize:10.0pt'>`q >= 1 /\ p EXP 2 = 2 * q EXP 2 ==> 2 * q  p < p`<o:p></o:p></span></font></pre><pre><font > size=2 face="Courier New"><span style='fontsize:10.0pt'><o:p> </o:p></span></font></pre><pre><font > size=2 face="Courier New"><span style='fontsize:10.0pt'>in seconds. Getting rid of the natural numbers altogether didn’t help; REAL_SOS also couldn’t prove either of<o:p></o:p></span></font></pre><pre><font > size=2 face="Courier New"><span style='fontsize:10.0pt'><o:p> </o:p></span></font></pre><pre><font > size=2 face="Courier New"><span style='fontsize:10.0pt'>`q >= &1 /\ p pow 2 = &2 * q pow 2 ==> p +  &1 * q > &0` or<o:p></o:p></span></font></pre><pre><font > size=2 face="Courier New"><span style='fontsize:10.0pt'>`q >= &1 /\ p pow 2 = &2 * q pow 2 ==> &2 * q  p < p`.<o:p></o:p></span></font></pre><pre><font > size=2 face="Courier New"><span style='fontsize:10.0pt'><o:p> </o:p></span></font></pre><pre><font > size=2 face="Courier New"><span style='fontsize:10.0pt'>When I interrupted the REAL_SOS proof attempts, I sometimes got an error message such as Sys_error “/tmp/sosfsbc40.out: No such file or directory”, but other times not.<o:p></o:p></span></font></pre><pre><font > size=2 face="Courier New"><span style='fontsize:10.0pt'><o:p> </o:p></span></font></pre><pre><font > size=2 face="Courier New"><span style='fontsize:10.0pt'>Steve Brackin<o:p></o:p></span></font></pre> > > <p class=MsoNormal><font size=2 face="Courier New"><span style='fontsize:10.0pt; > fontfamily:"Courier New"'><o:p> </o:p></span></font></p> > > </div> > > </body> > > </html> > Using Tomcat but need to do more? Need to support web services, security? > Get stuff done quickly with preintegrated technology to make your job easier > Download IBM WebSphere Application Server v.1.0.1 based on Apache Geronimo > http://sel.asus.falkag.net/sel?cmd=lnk&kid=120709&bid=263057&dat=121642 > _______________________________________________ > holinfo mailing list > holinfo@... > https://lists.sourceforge.net/lists/listinfo/holinfo 
From: Stephen Brackin <stephen.brackin@ve...>  20060626 07:04:49

I've found what seems to be a bug in HOL Light's REAL_SOS. It didn't prove `&q >= &1 /\ &p pow 2 = &2 * &q pow 2 ==> &p +  &1 * &q > &0` or `&q >= &1 /\ &p pow 2 = &2 * &q pow 2 ==> &2 * &q  &p < &p` In several minutes, although SOS_RULE proved the corresponding "for naturals" statements `q >= 1 /\ p EXP 2 = 2 * q EXP 2 ==> p  1 * q > 0` and `q >= 1 /\ p EXP 2 = 2 * q EXP 2 ==> 2 * q  p < p` in seconds. Getting rid of the natural numbers altogether didn't help; REAL_SOS also couldn't prove either of `q >= &1 /\ p pow 2 = &2 * q pow 2 ==> p +  &1 * q > &0` or `q >= &1 /\ p pow 2 = &2 * q pow 2 ==> &2 * q  p < p`. When I interrupted the REAL_SOS proof attempts, I sometimes got an error message such as Sys_error "/tmp/sosfsbc40.out: No such file or directory", but other times not. Steve Brackin 
From: John Harrison <John.H<arrison@cl...>  20060623 04:15:08

Hi Steve,  Have people looked into taking a symbolicalgebra program and creating a  program that does all the same sorts of things, but proves its results  correct as it goes along? There has certainly been some work in this area, but the techniques used differ widely. For example, Michael Beeson's MathXpert: http://www.cs.sjsu.edu/faculty/beeson/Papers/Englishste/Englishste.html is at first glance a conventional computer algebra system, but it does a thorough job of maintaining and enforcing sideconditions in a way that the "mainstream" systems do not. (It has other special features targeted at education). It may not produce proofs using very primitive inferences, but it doesn't "cheat". If you are looking for work within a standard theorem prover  indeed HOL Light  then see the work of Cezary Kaliszyk: http://www.cs.ru.nl/~cek/holcas/ This extends the automated facilities in HOL Light, and provides a more straightforward "computer algebra" interface.  MAXIMA would be a good starting point for such an effort because its  code is free, public, and freely available. If the  symbolicalgebra results are valid only if divisions by zero and  such don't occur, then the results proved could be appropriate  conditional statements. If the symbolicalgebra programs'  algorithms are mathematically sound, then proving their results  correct should be straightforward, just a lot of work. I like MAXIMA, and I chose it for the example in the HOL Light tutorial exactly because it's public and free. But I'm not sure that it, or any other existing computer algebra system, would be a good starting point for a verified implementation. I think it would be better to start from scratch writing in a very careful, disciplined style with verification in mind. I know of at least two attempts to create verified implementations of nontrivial "computer algebra" algorithms: * Laurent Thery and Loic Pottier have a verified implementation of Buchberger's algorithm for Groebner bases: http://wwwsop.inria.fr/croap/CFC/Gbcoq.html * Assia Mahboubi has been working towards a proven implementation of Cylindrical Algebraic Decomposition (CAD): http://wwwsop.inria.fr/marelle/Assia.Mahboubi/recheng.html However, even for implementations written carefully with verification in mind, the verifications can be highly nontrivial. So much so that when an algorithm naturally supports a "findingchecking" separation, where the correctness of a result can be checked relatively simply, I think there's a strong case for just verifying the checking process. The examples of Buchberger and CAD above present an interesting contrast from that point of view. As far as I know, CAD and other quantifier elimination procedures for the reals do not permit any specially easy way of checking the correctness of a result. To produce a proof one either has to: * Implement the algorithm in such a way that it produces a proof. As Rob Arthan mentioned, Sean McLaughlin has done this for real quantifier elimination by Hormander's algorithm in HOL Light (see subdirectory "Rqe"). This usually results in a large slowdown, and the implementation is hard. * Execute a verified implementation inside the logic. This is what Assia Mahboubi is working on for CAD. This promises greater efficiency (more so in Coq than in HOL because evaluation is highly optimized). The cost is that the correctness proof is *very* hard, probably even harder than a proofproducing implementation. By contrast, the limited real quantifier elimination for valid universal formulas done by HOL's SOS functions supports a very nice separation of finding and checking: the difficulty is in finding the right witnesses. To take the simplest case, once you've found a sumofsquares decomposition of a polynomial p(x1,...,xk): p(x1,...,xk) = s_1(x1,...,xk)^2 + ... + s_k(x1,...,xk)^2 the proof that !x1 ... xk. p(x1,...,xk) >= 0 is trivial, and nothing about how the magic polynomials s_i(x1,...,xk) are arrived at is necessary. HOL's Groebner basis procedure similarly does not need any verification of the way in which a basis is found, only the verification of some polynomial identities. If we compare this with the approach of verifying Buchberger's algorithm, we cannot easily draw *negative* conclusions. On the other hand, we are free to use a highly optimized and unverified implementation of Buchberger's algorithm, provided it keeps enough of a history trace to construct a proof afterwards.  John Harrison's MESON and family take the drudgery out of proving  logical tautologies in typical cases. Another classic findingchecking separation, by the way...  It would be very good for the formalmethods community if we had  something similar for algebraic results. Do you find HOL Light's REAL_RING and REAL_FIELD inadequate? No doubt they could be more efficient, but I find they often help a lot with basic algebraic simplifications.  Formal proofs will be a hard sell as long as we have to tell  people who need assurance that 85% of the proof effort will go  into confirming things that these people have known since high  school. True enough. To make things more concrete, do you have specific operations in MAXIMA that you would like to have proven variants of? John. 
From: John Harrison <John.H<arrison@cl...>  20060621 03:54:35

Hi Steve,  In trying to generalize earlier results, I've been trying to replace  results for the natural numbers with results for the natural numbers  embedded into the real numbers  i.e., replacing n with &n. To my surprise,  I've found that REAL_SOS knows much less about the natural numbers embedded  into the real numbers than SOS_RULE knows about the natural numbers. Yes, this is an oversight on my part.  For example, SOS_RULE can prove `!n:num. n >= 0`, `!n:num. n <= 2*n`, and  `!n m:num. ~((n < m) /\ (m < n+1))`, but REAL_SOS can't prove any of  `!n:num. &n >= &0`, `!n:num. &n <= &2 * &n`, or `!n m:num. ~((&n < &m) /\  (&m < &n + &1))`. You'll find that plain old REAL_ARITH does a bit better. This is because there is special code that includes hypotheses "&0 <= &x" for all nonnumeral "x" in the target term. The code is in "realarith.ml" in the following line of REAL_LINEAR_PROVER: let le' = le @ map (fun a > INST [rand a,n_tm] pth) aliens I will add similar code to REAL_NONLINEAR_PROVER. This still won't cope with the last goal. That gets proved because strict inequality assumptions "0 < p" over N or Z get turned into "1 <= p" before the mapping into R. I should perhaps make the pure real prover do something similar.  I thought I'd read somewhere that SOS_RULE produces its results by  embedding the natural numbers into the real numbers, applying REAL_SOS,  then translating the results back to the natural numbers. That's correct, but it's explicitly translated from N to Z using the following relativizations (see NUM_TO_INT_CONV in "int.ml"): (!n. P(&n)) <=> (!i. ~(&0 <= i) \/ P i) (?n. P(&n)) <=> (?i. &0 <= i /\ P i) so the positivity hypotheses appear without relying on the later reals procedure. John. 
From: Rob Arthan <rda@le...>  20060620 09:49:46

On Sunday 18 Jun 2006 6:23 am, Stephen Brackin wrote: > This is a question for the whole HOL community: > > > > Have people looked into taking a symbolicalgebra program and creating a > program that does all the same sorts of things, but proves its results > correct as it goes along? >... > If an algorithm is valid, then is there any reason why the times needed to > prove its results correct need be more than a constant multiple of the > times the algorithm needs to produce these results? >... May I just comment on that one point in your posting for now: The question you are asking about time complexity is a significant open question both theoretically and practically, I believe. I think the approach you have in mind is to verify an algorithm and then execute it via an execution model based on primitive inferences, (i.e., you prove:  !input. DesiredResult (input, algorithm input) once and for all, and then for a specific input, you evaluate `algorithm specific_input` via primitve inferences to give a theorem of the form:  algorithm specific_input = specific_output and so:  DesiredResult(specific_input, specific_output) In this model, I suspect that the answer is yes, theoretically. The answer is probably also yes practically provided you have a primitive inference rule that somehow lets you execute array operations in constant time. The other approach is to execute the algorithm in the metalanguage with extra instrumentation to produce a proof. In practice, the efficiency of this approach seems to me likely to depend a lot on the algorithm in question. E.g., the overhead appears to be much worse for the known decision procedures for the firstorder theory of the reals (see the paper by Sean MacLaughlin and John Harrison) than it is for decision procedures for linear arithmetic. However, these aren't the sort of algorithms you are likely to find in computer algebra systems (since their worst case timecomplexity is bad anyway). Of course, these two approaches are two ends of a continuum and efficient coding of decision procedures in HOL usually involves a mixture of the two. Regards, Rob. 
From: Ganesh <ganesh@cs...>  20060619 21:27:59

The preliminary program and registration information for TV06 is here http://www.easychair.org/FLoC06/TV.html Ganesh Gopalakrishnan (Univ of Utah) John O'Leary (Intel) 
From: Stephen Brackin <stephen.brackin@ve...>  20060618 05:24:24

This is a question for the whole HOL community: Have people looked into taking a symbolicalgebra program and creating a program that does all the same sorts of things, but proves its results correct as it goes along? MAXIMA would be a good starting point for such an effort because its code is free, public, and freely available. If the symbolicalgebra results are valid only if divisions by zero and such don't occur, then the results proved could be appropriate conditional statements. If the symbolicalgebra programs' algorithms are mathematically sound, then proving their results correct should be straightforward, just a lot of work. John Harrison has already done something similar by using MAXIMA to perform calculations, then using HOL Light to prove that the computed results have their intended properties, but this work doesn't cover all the sorts of results that MAXIMA produces and it doesn't use the mathematical validity in the algorithms producing these results. (Parts of the algorithms that represent aesthetic conventions and heuristics about what's most likely to occur in human practice can be ignored for proof purposes.) If an algorithm is valid, then is there any reason why the times needed to prove its results correct need be more than a constant multiple of the times the algorithm needs to produce these results? Do people know of any available work along these lines? Would people be interested in a community project to produce such a thing, with different people doing different parts of the problem and sharing their results? John Harrison's MESON and family take the drudgery out of proving logical tautologies in typical cases. It would be very good for the formalmethods community if we had something similar for algebraic results. Formal proofs will be a hard sell as long as we have to tell people who need assurance that 85% of the proof effort will go into confirming things that these people have known since high school. Steve Brackin 
From: Stephen Brackin <stephen.brackin@ve...>  20060618 04:08:05

Here's another HOL Light question that's mostly for John Harrison but also of general interest: In trying to generalize earlier results, I've been trying to replace results for the natural numbers with results for the natural numbers embedded into the real numbers  i.e., replacing n with &n. To my surprise, I've found that REAL_SOS knows much less about the natural numbers embedded into the real numbers than SOS_RULE knows about the natural numbers. For example, SOS_RULE can prove `!n:num. n >= 0`, `!n:num. n <= 2*n`, and `!n m:num. ~((n < m) /\ (m < n+1))`, but REAL_SOS can't prove any of `!n:num. &n >= &0`, `!n:num. &n <= &2 * &n`, or `!n m:num. ~((&n < &m) /\ (&m < &n + &1))`. I thought I'd read somewhere that SOS_RULE produces its results by embedding the natural numbers into the real numbers, applying REAL_SOS, then translating the results back to the natural numbers. I'll look at the code, but do you have any suggestions on how to get REAL_SOS to prove the same results for the natural numbers embedded into the real numbers that SOS_RULE proves for the natural numbers? Steve Brackin 
From: Stephen A. Edwards <sedwards@cs...>  20060614 20:32:00

CALL FOR PARTICIPATION The Fourth ACM/IEEE International Conference on Formal Methods and Models for CoDesign MEMOCODE'2006 July 2730, 2006 Embassy Suites, Napa Valley, California http://www.memocodeconference.com/  Advance Registration Deadline: July 5, 2006  Sponsors ACM SIGDA * IEEE Circuits and System Society IEEE Computer Society * IEEE Council on EDA Supporters Bluespec, Inc. * Nokia The IndustryUniversity Cooperative Research Program MEMOCODE traces its roots to a series of online discussions starting in 2002 on the challenges facing correct, composable and scalable design of hardware and software; and how advances in formal methods can be used to solve these tough problems; what works in practice and what does not. MEMOCODE has evolved into a forum that brings together researchers working across hardware and software domains with a natural bent towards practical formal models and methods. MEMOCODE 2006 continues this tradition to explore practical ways in handling tough problems in design and validation of hardware and software in industrial practice. This year's program is special in many ways: starting with its location in the picturesque Napa valley towards the end of the Design Automation Conference and in the company of leading research practitioners, across industry and academia in a singlesession and highly interactive setting. The program includes two panels, two tutorials, including the immensely popular fullday tutorial on SOC designs by Ran Ginosaur. If you have never attended MEMOCODE before, we invite you to view some of the archived presentations and webcasts from our San Diego meeting, the last time it was held in the US. Technical Program CoChairs James Hoe (CMU), Jens Palsberg (UCLA) ============================== Keynotes Rajeev Alur (University of Pennsylvania) Games for Formal Design and Verification of Reactive Systems Alex Aiken (Stanford University) Scalable Program Analysis Using Boolean Satisfiability Carl Seger (Intel Corp.) Integrated Design and Verification ============================== Tutorials Constance Heitmeyer (Naval Research Laboratory) Rigorous Requirements for Critical Systems: Specification, Formal Verification, and Validation with SCR (Software Cost Reduction) Ran Ginosar (Technion) Synchronization in MultipleClock SOC Designs & GALS Design ============================== Panels NanoComputing: Do we need New Formal Approaches to CoDesign? Panelists include Maya Gokhale (LANL), Alvin Lebeck (Duke), Michael Hsiao (Virginia Tech), and Sandeep Shukla (Virginia Tech) Programming Models and Languages for SOCImplemented Architectures Panelists include Arvind (MIT), Krste Asanovic (MIT), Satnam Singh (Microsoft), Kees Vissers (Xilinx), and Rajesh Gupta (UC San Diego) ============================== Program Day 1: Thursday, July 27, 2006  08:45: Welcome message: General Chair: Rajesh Gupta (UCSD) Program Chairs: James C. Hoe (CMU) and Jens Palsberg (UCLA) 09:00: Keynote: Rajeev Alur (University of Pennsylvania) Title: Games for Formal Design and Verification of Reactive Systems Chair: Sandeep Shukla (Virginia Tech) 10:00: Break 10:30: Session T1: Model Checking Analyzing Tabular Requirements Specifications Using Infinite State Model Checking Tevfik Bultan (UC Santa Barbara) Constance Heitmeyer (Naval Research Laboratory) Mixed Symbolic Representations for Model Checking Software Programs Zijiang Yang (Western Michigan University) Chao Wang (NEC Laboratories America) Aarti Gupta (NEC Laboratories America) Franjo Ivancic (NEC Laboratories America) ComponentBased Hardware/Software CoVerification Fei Xie (Portland State University) Guowu Yang (Portland State University) Xiaoyu Song (Portland State University) 12:00: Lunch 13:30: Session T2: Rulebased HW Design A Rulebased Model of Computation for SystemC: Integrating SystemC and Bluespec for CoDesign Hiren D. Patel (Virginia Tech) Sandeep K. Shukla (Virginia Tech) Elliot Mednick (Bluespec Inc.) Nikhil S. Rishiyur (Bluespec Inc.) Low Power Hardware Synthesis from TRSbased Specifications Gaurav Singh (Virginia Tech) Sandeep K. Shukla (Virginia Tech) 802.11a Transmitter: A Case Study in Microarchitectural Exploration to meet Performance Guarantees Nirav Dave (CSAIL MIT) Michael Pellauer (CSAIL MIT) Steve Gerding (CSAIL MIT) Arvind (CSAIL MIT) 15:00: Break 15:30: Session T3: HW Verification Automatic Decomposition for Sequential Equivalence Checking of System Level and RTL Descriptions Shobha Vasudevan (University of Texas at Austin) Vinod Viswanath (University of Texas at Austin) Jacob A. Abraham (University of Texas at Austin) Jiajin Tu (University of Texas at Austin) A verified hardware development using CSPB Alistair McEwan (University of Surrey) Steve Schneider (University of Surrey) 16:30: Break 17:00: Panel: NanoComputing: Do we need New Formal Approaches to CoDesign? Organizer and Chair: Sandeep Shukla (Virginia Tech) Panelists: Maya Gokhale (Los Alamos National Laboratory) Alvin Lebeck (Duke University) Michael Hsiao (Virginia Tech) Abstract: Nanotechnology is upon us with 45 nm and beyond CMOS technologies in the fabs, and with alternative computing fabrics such as Molecular, DNA guided assemblies, quantum computing, carbon nanotubes and so on. With such drastic changes in the computing fabrics, we move into unprecedented technology scaling, as well as rampant defects, and transient faults. Moreover, the billions of computing elements, we face the possibility of unthinkable amount of parallelism possibilities. The optimization factors and assumptions we made so far in hardware are no longer valid in such changed computing fabric. The parallelism heretofore unavailable being given to our disposal changes the way we design software and algorithms. The question therefore is: do we need drastic new approaches to design of hardware and software? This panel will consider this question and the experts from formal methods, reliability, spatial computing, quantum computing, codesign, language design and hardware/software design will discuss this question from individual perspectives to come up with a cogent set of questions researchers need to answer. 19:30: End of Day 1 Day 2: Friday, July 28, 2006  09:00: Keynote: Alex Aiken (Stanford University) Title: Scalable Program Analysis Using Boolean Satisfiability Chair: Jens Palsberg (UCLA) 10:00: Break 10:30: Session F1: Transactionlevel Modeling Execution Semantics and Formalisms for MultiAbstraction TLM Assertions Volkan Esen (Infineon Technologies AG) Wolfgang Ecker (Infineon Technologies AG) Thomas Steininger (Infineon Technologies AG) Michael Hull (Infineon Technologies AG) Michael Velten (Infineon Technologies AG) A Methodology for Abstracting RTL Designs into TL Descriptions Nicola Bombieri (University of Verona) Franco Fummi (University of Verona) Graziano Pravadelli (University of Verona) Using Reo for Formal Specification and Verification of System Designs Niloofar Razavi (University of Tehran) Marjan Sirjani (University of Tehran and IPM) 12:00: Lunch 13:30: Panel: Programming Models and Languages for SOCImplemented Architectures Organizer and Chair: Rajesh Gupta Panelists: Arvind (MIT) Krste Asanovic (MIT) Satnam Singh (Microsoft) Kees Vissers (Xilinx) Abstract: Microsystems implemented on chips or SOCs provide new capabilities and alternatives not easily available to architects in the past, via ISA extensions, additional datapath elements, SIMD arrays and their short vector extensions, multigrain coprocessing etc. We can, given enough design resources, build such machines. Evidence of various combinations of architectural archetypes can be seen in a flood of new machine architectures for high definition video processing, though there are significant challenges in architectural exploration. However, a central question that seems to remain unanswered, is how will the programming for such machines keep up without waiting for the god of programming to descend. 15:00: Break 15:30: Session F2: Time and Clocks Specifying and Proving Properties of Timed I/O Automata in the TIOA Toolkit Myla Archer (Naval Research Laboratory) HongPing Lim (CSAIL MIT) Nancy Lynch (CSAIL MIT) Sayan Mitra (CSAIL MIT) Shinya Umeno (CSAIL MIT) Reliable Design with Multiple Clock Domains Ed Czeck (Bluespec Inc.) Ravi Nanavati (Bluespec Inc.) Joe Stoy (Bluespec Inc.) The SystemJ Approach to SystemLevel Design Flavius Gruian (Lund University) Partha Roop (The University of Auckland) Zoran Salcic (The University of Auckland) Ivan Radojevic (The University of Auckland) 17:00: Poster Session Presentations Equivalence Checking: A RuleBased Approach Masahiro Fujita (University of Tokyo) Subash Shankar (City University of New York) Sasaki Shunsuke (University of Tokyo) Formal Methods for checking Realizability of Coalitions in 3party systems Ansuman Banerjee (IIT Kharagpur) Pallab Dasgupta (IIT Kharagpur) P.P.Chakrabarti (IIT Kharagpur) A SemanticDriven Synthesis Flow for PlatformBased Design Qi Zhu (UC Berkeley) Abhijit Davare (UC Berkeley) Alberto SangiovanniVincentelli (UC Berkeley) Assertion checking of control dominated systems with nonlinear solvers I. Ugarte (University of Cantabria) P. Sanchez (University of Cantabria) Compositional MSC/services Specifications for SystemC Implementations Frederic Doucet (UCSD) RK Shyamasundar (Tata Institute of Fundamental Research/IBM Research) Ingolf Krueger (UCSD) Rajesh Gupta (UCSD) RSHIM: Deterministic Concurrency with Recursion and Shared Variables Olivier Tardieu (Columbia University) Stephen A. Edwards (Columbia University) 17:30: Wine & Cheese Party and Poster Session 19:00: End of Day 2 Day 3: Saturday, July 29, 2006  09:00: Keynote: Carl Seger (Intel Corp.) Title: Integrated Design and Verification Chair: James C. Hoe (CMU) 10:00: Break 10:30: Session S1: Scheduling and Analysis Efficient Code Generation from Synchronous Programs Jens Brandt (University of Kaiserslautern) Klaus Schneider (University of Kaiserslautern) Eric Vecchi (University of Kaiserslautern) LatencyInsensitive Design and Central Repetitive Scheduling Robert de Simone (INRIA) JeanVivien Millo (INRIA), Julien Boucaron (INRIA) A ScenarioAware Data Flow Model for Combined LongRun Average and WorstCase Performance Analysis B.D. Theelen (Eindhoven University of Technology) M.C.W. Geilen (Eindhoven University of Technology) T. Basten (Eindhoven University of Technology) J.P.M. Voeten (Eindhoven University of Technology) S.V. Gheorghita (Eindhoven University of Technology) S. Stuijk (Eindhoven University of Technology) 11:30: End of the technical program 13:00: Tutorial (half day) Rigorous Requirements for Critical Systems: Specification, Formal Verification, and Validation with SCR (Software Cost Reduction) Presenter: Constance Heitmeyer (Naval Research Laboratory) Abstract: The Software Cost Reduction (SCR) method is a practical, industrialstrength method for constructing system and software specifications. The method has been shown to scale to large applications and to produce specifications that are both easy to understand and easy to change. Developed for use by engineers, the SCR method has been applied to a wide range of practical systems, including avionics systems, telephone networks, submarine communications, space systems, and control systems for nuclear plants. Among the organizations that have applied SCR in practice are Grumman, Lockheed, Ontario Hydro, Rockwell Aviation, and NASA. Most recently, the SCR tools were used in the certification of a securitycritical cryptographic system. 17:00: End of Day 3 Day 4: Sunday, July 30, 2006  09:00: Tutorial (full day) Synchronization in MultipleClock SOC Designs & GALS Design Presenter: Ran Ginosar (Technion) Abstract: Larger and faster SystemsonChips (SoC) employ multiple clocks, either to save on silicon area and power dissipation or to enable communications with several external clocks. Onchip Interclock domain communication is complicated: It incurs latency, requires careful design, and typically cannot be validated by either formal tools or simulations. Such communications are prone to intermittent metastability errors that are hard to identify and locate. We will describe the problems, review proven and emerging solutions, and study how to avoid common errors. We will also discuss related topics including long interconnects and GALS (Globally Asynchronous, Locally Synchronous) designs. 17:00 End of Last Day ============================== Organization General Chair Rajesh Gupta, UC San Diego Program Chairs James Hoe, CMU Jens Palsberg, UCLA Publications Elizabeth Leonard, NRL Publicity Stephen A. Edwards, Columbia University Panels Sandeep Shukla, Virginia Tech Local Arrangements Anmol Mathur, Calypto Technical Program Committee Arvind, MIT, USA Lennart Augustsson, Chalmers, Sweden Twan Basten, Eindhoven, Netherlands Gerard Berry, Esterel Tech, France Forrest Brewer, UC Santa Barbara, USA James Browne, Texas, USA Manfred Broy, TU Munich, Germany Tevfik Bultan, UC Santa Barbara, USA Rance Cleaveland, Maryland, USA Robert De Simone, INRIA, France Stephen A. Edwards, Columbia, USA Harry Foster, Jasper Design, USA Masahiro Fujita, Tokyo, Japan Franco Fummi, Verona, Italy Ganesh Gopalakrishnan, Utah, USA Rajesh Gupta, UC San Diego, USA Nicolas Halbwachs, Verimag, France Connie Heitmeyer, NRL, USA Ranjit Jhala, UC San Diego, USA Daniel Kroening, ETH Zurich, CH Shuvendu Lahiri, Microsoft, USA Elizabeth Leonard, NRL, USA Pete Manolios, Georgia Tech, USA Anmol Mathur, Calypto Design, USA John O'Leary, Intel, USA Zebo Peng, Linköping, Sweden Carl Pixley, Synopsys, USA Klaus Schneider, Kaiserslautern, DE Sandeep Shukla, Virginia Tech, USA R. K. Shyamasundar, TIFR, India JeanPierre Talpin, INRIA, France P. S. Thiagarajan, Singapore ============================== Advance Registration ends July 5, 2006. Register at http://www.memocodeconference.com/ 
From: Grumberg + Huth <floc@in...>  20060614 20:21:22

CALL FOR PAPERS: TACAS 2007 Thirteenth International Conference on Tools and Algorithms for the Construction and Analysis of Systems http://www.doc.ic.ac.uk/tacas07/ Part of ETAPS 2007, March 24  April 1, 2007, Braga, Portugal IMPORTANT DATES * 6 Oct 2006: Submission deadline (strict) for abstracts of research and tool demonstration papers * 13 Oct 2006: Submission deadline (strict) for full versions of research and tool demonstration papers * 8 Dec 2006: Notification of acceptance * 5 Jan 2007: Cameraready versions due CONFERENCE DESCRIPTION TACAS is a forum for researchers, developers and users interested in rigorously based tools and algorithms for the construction and analysis of systems. The conference serves to bridge the gaps between different communities that share common interests in, and techniques for, tool development and its algorithmic foundations. The research areas covered by such communities include but are not limited to formal methods, software and hardware verification, static analysis, programming languages, software engineering, realtime systems, communications protocols, and biological systems. The TACAS forum provides a venue for such communities at which common problems, heuristics, algorithms, data structures and methodologies can be discussed and explored. In doing so, TACAS aims to support researchers in their quest to improve the utility, reliability, flexibility and efficiency of tools and algorithms for building systems. Tool descriptions and case studies with a conceptual message, as well as theoretical papers with clear relevance for tool construction are all encouraged. The specific topics covered by the conference include, but are not limited to, the following: * Specification and verification techniques for finite and infinitestate systems * Software and hardware verification * Theoremproving and modelchecking * System construction and transformation techniques * Static and runtime analysis * Abstraction techniques for modeling and validation * Compositional and refinementbased methodologies * Testing and testcase generation * Analytical techniques for secure, realtime, hybrid, critical, biological or dependable systems * Integration of formal methods and static analysis in highlevel hardware design or software environments * Tool environments and tool architectures * SAT solvers * Applications and case studies As TACAS addresses a heterogeneous audience, potential authors are strongly encouraged to write about their ideas and findings in general and jargon independent, rather than in application and domainspecific, terms. Authors reporting on tools or case studies are strongly encouraged to indicate how their experimental results can be reproduced and confirmed independently. PROGRAMME COMMITTEE Christel Baier (U. Bonn, Germany) Armin Biere (Johannes Kepler U., Austria) Jonathan Billington (University of South Australia, Australia) Ed Brinksma (ESI and U. of Twente, The Netherlands) Rance Cleaveland (U. of Maryland & Fraunhofer USA Inc, USA) Byron Cook (tool chair) (Microsoft Research, Cambridge, UK) Dennis Dams (Bell Labs, Lucent Technologies, Murray Hill, USA) Marsha Chechik (U. Toronto, Canada) Francois Fages (INRIA Rocquencourt, France) Kathi Fisler (Worcester Polytechnic, USA) Limor Fix (Intel Research Laboratory, Pittsburgh, USA) Hubert Garavel (INRIA RhonesAlpes, France) Susanne Graf (VERIMAG, Grenoble, France) Orna Grumberg (cochair) (TECHNION, Israel Institute of Technology, Israel) John Hatcliff (Kansas State U., USA) Holger Hermanns (U. des Saarlandes, Germany) Michael Huth (cochair) (Imperial College London, UK) Daniel Jackson (Massachusetts Institute of Technology, USA) Somesh Jha (U. of Wisconsin at Madison, USA) Orna Kupferman (Hebrew U., Jerusalem, Israel) Marta Kwiatkowska (U. of Birmingham, UK) Kim Larsen (Aalborg U., Denmark) Michael Leuschel (HeinrichHeine U., Duesseldorf, Germany) Andreas Podelski (MaxPlanckInstitut fuer Informatik, Saarbruecken, Germany) Tiziana MargariaSteffen (U. Goettingen, Germany) Tom Melham (Oxford U., UK) CR Ramakrishnan (SUNY Stony Brook, USA) Jakob Rehof (Fraunhofer ISST, Germany) Natarajan Shankar (SRI, Menlo Park, USA) Bernhard Steffen (U. Dortmund, Germany) Lenore Zuck (U. of Illinois, USA). INVITED SPEAKER K. Rustan M. Leino (Microsoft Research, USA) SUBMISSION GUIDELINES Papers should be submitted using the TACAS 2007 Conference Service. As with other ETAPS conferences, TACAS accepts two types of contributions: * research papers and * tool demonstration papers. Both types of contributions will appear in the proceedings and have oral presentations during the conference. Research papers: Research papers cover one or more of the topics above, including tool development and case studies from a perspective of scientific research. Research papers are evaluated by the TACAS Program Committee. Submitted research papers must: * be in English and have a maximum of 15 pages (including figures and bibliography) * present original research which is unpublished and not submitted elsewhere (conferences or journals)  in particular, simultaneous submission of the same contribution to multiple ETAPS conferences is forbidden * use the SpringerLNCS style * be submitted electronically in Postscript or PDF form via the TACAS 2007 Conference Service (abstract no later than 6 October, 2006, and full paper no later than 13 October, 2006) Submissions deviating from these instructions may be rejected without review. Any questions regarding this policy should be directed to the Program Committee CoChairs Orna Grumberg (www.cs.technion.ac.il/users/orna/) or Michael Huth (www.doc.ic.ac.uk/~mrh/) prior to submitting. Tool demonstration papers: Tool demonstration papers present tools based on aforementioned technologies (e.g., theoremproving, modelchecking, static analysis, or other formal methods) or fall into the above application areas (e.g., system construction and transformation, testing, analysis of realtime, hybrid or biological systems, etc.). Tool demonstration papers are evaluated by the TACAS Tool Chair, Byron Cook (http://research.microsoft.com/users/bycook/default.htm) with the help of the Programme Committee. Submitted tool demonstration papers must: * be in English and have a maximum of 4 pages * have an appendix (not included in the 4 page count) that provides a detailed description of:  how the oral presentation will be conducted, e.g. illustrated by a number of snapshots  the availability of the tool, the number and types of users, other information which may illustrate the maturity and robustness of the tool  if applicable, a link to a webpage for the tool (The appendix will not be included in the proceedings, but during the evaluation of the tool demonstration papers it will be equally important as the pages submitted for publication in the proceedings.) * use the SpringerVerlag LNCS style * clearly describe the enhancements and novel features of the tool in case that one of its previous versions has already been presented at meetings or published in some form * be submitted electronically in Postscript or PDF form via the TACAS 2007 Conference Service (abstract no later than 6 October, 2006, and full paper no later than 13 October, 2006) Submissions deviating from these instructions may be rejected without review. Any questions regarding this policy should be directed to the Tool Chair Byron Cook. 
From: Paul Curzon <pc@dc...>  20060613 21:08:49

 Call for Papers  FMIS 2006 1st International Workshop on FORMAL METHODS FOR INTERACTIVE SYSTEMS Macau SAR China, 31 October 2006 http://fmis.iist.unu.edu/ ********************************************************************** IMPORTANT DATES Submission deadline: 23 July, 2006 Acceptance notification: 10 September, 2006 Final version for the preproceedings due: 12 October, 2006 Final version for the ENTCS proceedings due: 1 December, 2006 ********************************************************************** BACKGROUND AND OBJECTIVES Reducing the likelihood of human error in the use of interactive systems is increasingly important: the use of such systems is becoming widespread in applications that demand high reliability due to safety, security, financial or similar considerations. Consequently, the use of formal methods in verifying the correctness of interactive systems should also include analysis of human behaviour in interacting with the interface. The aim of this workshop is to bring together researchers in computer science and cognitive psychology, from both academia and industry, who are interested in developing formal and semiformal methodologies and tools for the evaluation and verification of interactive systems. The outcome is to establish a worldwide network of researchers interested in applying formal methods to HCI. The workshop will focus on, though will not be restricted to, * general design and verification methodologies based on cognitive psychology as well as application areas such as * mobile devices; * embedded systems; * safetycritical systems; * highreliability systems; * shared control systems; * digital libraries; * eGovernment; * pervasive systems; * augmented reality. The oneday workshop will feature a one hour presentation by a keynote speaker together with contributed papers that will undergo a peerreview process. Contributed papers may be accepted either for full presentation or short presentation. PUBLICATION Papers accepted as full paper presentations will be published by Elsevier in the series Electronic Notes in Theoretical Computer Science (ENTCS). Papers accepted as short paper presentations will be published in the participants' proceedings at the workshop only. Detailed information on the submission procedure is available below. Publication of a selection of the papers in a journal special issue is also under consideration. INVITED SPEAKER * Harold Thimbleby, University of Wales Swansea, UK SPONSORS AND ORGANISATION IFMIS 2006 will be organised jointly between the International Institute for Software Technology of the United Nations University (UNUIIST) and the EPSRC Human Error Modelling (HUM) Project of the University of London (QMUL and UCL). UNUIIST and EPSRCHUM are also sponsors of ICTAC 2006. SUBMISSION AND PUBLICATION Submissions to the workshop must not have been published or be concurrently considered for publication elsewhere. All submissions will be peerreviewed and judged on the basis of originality, contribution to the field, technical and presentation quality, and relevance to the workshop. Papers should be written in English and not exceed 16 pages in ENTCS format. Authors should utilize the ENTCS macro files that have been specially prepared for use with ENTCS. The generic ENTCS package, which contains files common for all volumes in ENTCS and includes several examples, as well as instructions, can be downloaded from http://www.entcs.org/generic.tar.gz. The entcsmacro.sty file in the ENTCS package should be be replaced by the prentcsmacro.sty file, which is specific to FMIS 2006 and can be downloaded from http://www.entcs.org/files/fmis/prentcsmacro.sty. File prentcsmacro.sty has to be renamed entcsmacro.sty. File example.tex has to be used as a template for the paper, making sure that key words are included in the frontmatter section where indicated. Authors also should not use any formatting commands that alter the ENTCS style definitions. This includes the format of Definitions, Lemmas, Theorems, etc., as well as the spacing that is defined by the ENTCS Macros. Authors must submit their papers in pdf format to the website http://confman.iist.unu.edu/FMIS2006/REGpaper/ no later than Sunday 23 July 2006. All queries should be sent to: fmis2006 AT iist.unu.edu. ORGANISERS * Antonio Cerone, UNIIIST, Macau SAR China * Paul Curzon, Queen Mary, University of London, UK PROGRAM COMMITTEE * Ann Blandford, UCL Interaction Center, UK * Ralph Back, Abo Akademi, Finland * Howard Bowman, University of Kent, UK * George Buchanan, University of Wales Swansea, UK * Antonio Cerone, UNIIIST, Macau SAR China (Cochair) * Paul Cairns, UCL Interaction Center, UK * Jose Creissac Campos, University of Minho, Portugal * Paul Curzon, Queen Mary, University of London, UK (Cochair) * Gavin Doherty, Trinity College, University of Dublin, Ireland * Michael Harrison, University of Newcastle upon Tyne, UK * C. Michael Holloway, NASA Langley Research Center, USA * Chris Johnson, University of Glasgow, UK * Alan Dix, Lancaster University, UK * Li Siu Pan, Macao Polytechnic Institute, Macau SAR China * Peter Lindsay, The University of Queensland, Australia * Philippe Palanque, University of Toulouse III, France * Fabio Paterno, CNRISTI, Italy * Rimvydas Ruksenas, Queen Mary, University of London, UK 
From: Byron Cook <bycook@mi...>  20060613 15:38:26

******** CALL FOR PARTICIPATION ************ All are invited to the 2006 Symposium on Satisfiability Solvers and Program Verification (SSPV). Seattle, August 10  11. SSPV is a FLoC event. URL: http://www.easychair.org/FLoC06/SSPV.html Sponsored by Institute for Pure and Applied Mathematics (IPAM) Organizers: Dimitris Achlioptas, Byron Cook, Moshe Vardi  We have invited the following researchers to come speak about new work in the intersection between program verification and SATsolvers. =20 Alex Aiken, Stanford=20 Title: Scalable Program Analysis Using Boolean Satisfiability Alessandro Cimatti, IRST=20 Title: Reasoning about Bit Vector programs with Decision Procedures Edmund Clarke, CMU=20 Title: Bounded and Unbounded Model Checking using SAT Carla Gomes, Cornell=20 Title: Beyond Satisfiability: Model Counting, Quantification, and Randomization Aarti Gupta, NEC=20 Title: Verifying C Programs using SATbased model checking Orna Grumberg, Technion=20 Title: Hybrid BDD and AllSAT Method for Model Checking Daniel Kroening, ETH=20 Title: SATbased methods for proving properties in Reynolds/O'Hearn Separation Logic Shuvendu Lahiri, Microsoft Research=20 Title: Efficient SATbased Techniques for Predicate Abstraction =20 Sharad Malik, Princeton=20 Title: Optimization and Relaxation in SAT Search Ken McMillan, Cadence Labs=20 Title: SAT, interpolants, and software model checking Roberto Nieuwenhuis, Technical University of Catalonia=20 Title: The new architecture and solvers in the Barcelogic tool for SAT modulo theories. Ofer Strichman, Technion =20 Title: Decision Heuristics based on an Abstraction/Refinement model 
From: Christelle Scharff <scharffc@gm...>  20060612 17:46:54

************************************************* * CALL FOR WORKSHOP PROPOSALS * ************************************************* LPAR 2006 13th International Conference on Logic for Programming Artificial Intelligence and Reasoning Phnom Penh, November 13th17th, 2006 Workshops: Sunday, November 12th, 2006 http://www.lix.polytechnique.fr/~hermann/LPAR2006/ The LPAR organizers have made arrangements to facilitate the running of preLPAR workshops on Sunday, November 12th, 2006. Meeting rooms and accommodations have been reserved at the Cambodiana Hotel (http://www.hotelcambodiana.com). Each workshop will have its own registration; it is not necessary to register to LPAR in order to attend workshops. Workshops provide an ideal platform for the presentation of preliminary work or novel ideas in a less formal way than the conference itself. They also are an opportunity to disseminate work in progress, particularly for new researchers. Workshops also provide a venue for presenting more specialized topics and opportunities for more intensive discussions, exchange of ideas, and project collaboration. The topics of the workshops can cover any areas related to logic and automated reasoning, including crossdisciplinary areas and applications. Proposals should consist of: * a title; * names, affiliations, and contact details (email, web page, phone, fax) of the workshop organizing committee together with a designated contact person as the workshop coordinator; * a brief technical description of the topics covered; * a discussion of the relevance and benefits of the workshop; * a proposed format and agenda; * a duration (which may vary from halfaday to one day); * a procedure for selecting papers and participants; and * an estimate of the number of expected attendees. Additional organizational plans may include names of potential invited speakers, proposed demo sessions and tutorials, plans for proceedings or other publications, etc. The LPAR Organizing Committee will determine the final list of accepted workshops. Important guidelines: It is suggested that prospective workshop organizers contact the workshop chair before submitting a proposal. ***** Proposals are due by Monday, July 10th, 2006.***** All proposals will be acknowledged. Organizers will be notified of acceptance or rejection by Monday, July 17th, 2006. Proposal Submission: Proposals should be submitted by email, as PDF file, to: Dr. Christelle Scharff (Workshop Chair) Email: cscharff@... Pace University Seidenberg School of Computer Science and Information Systems Department of Computer Science New York, NY 10038 Phone: +1 212 346 1016 Fax: +1 212 346 1863  Cambodia ... Land of LPAR and Pagodas  