<HTML>
<P> </P>
<P><SPAN style="FONT-SIZE: 12pt; FONT-FAMILY: Times New Roman">The Sixth International Workshop on Automated Verification of Infinite State Systems <BR>
(AVIS 2007) is a forum for researchers, students, and practitioners interested in the <BR>
application of formal methods and tools for the automatied verification of large <BR>
practical systems. Formal methods, in particular model checking, is increasingly <BR>
being used in industry to automatically establish the correctness of <BR>
(and to find flaws in) finite-state systems, such as descriptions of hardware <BR>
and protocols. However, model checking is limited in scope due to the state explosion <BR>
problem. Most practical system descriptions, notably that of software, are therefore not <BR>
directly amenable to finite-state verification methods since they have very large or <BR>
infinite state spaces.<BR>
For such systems, theorem proving -- a process that requires manual effort and <BR>
mathematical sophistication to use -- has so far been the only viable alternative. <BR>
More recently, we have seen the emergence of hybrid techniques that combine the <BR>
ease-of-use of model checkers with the power of theorem provers. <BR>
Tools based on these techniques afford users with full automation, and are less <BR>
sensitive to the size of the state space (which may be infinite or arbitrarily large). <BR>
There is a growing body of knowledge in this field which has a very exciting future.</SPAN></P>
<P class=MsoNormal style="MARGIN: 0in 0in 0pt"><?xml:namespace prefix = o ns = "urn:schemas-microsoft-com:office:office" /><o:p><SPAN style="FONT-SIZE: 12pt; FONT-FAMILY: Times New Roman"> </SPAN></o:p></P>
<P class=MsoNormal style="MARGIN: 0in 0in 0pt"><o:p><SPAN style="FONT-SIZE: 12pt; FONT-FAMILY: Times New Roman">The intention of this workshop is to build a forum for exchanging ideas and experiences <BR>
by bringing together theoreticians, tool builders, as well as practitioners who are <BR>
interested in this emerging area of research in formal verification. <BR>
The theme of AVIS 2007 will be “reliable software”. </SPAN></o:p></P>
<P class=MsoNormal style="MARGIN: 0in 0in 0pt"><o:p><SPAN style="FONT-SIZE: 12pt; FONT-FAMILY: Times New Roman">Software is increasingly becoming the driving force of modern civilization, <BR>
playing an increasingly important role in modern society. <BR>
Human civilization is becoming more and more dependent on software, as increasingly <BR>
capable and cheap hardware processors and communication devices are routinely being <BR>
embedded into an ever-growing list of physical systems. Software is now being used <BR>
for controlling mission-critical systems such as nuclear power plants, patient monitors, <BR>
and spacecrafts. Bugs in software systems controlling safety critical applications <BR>
can cause loss of life and property. Hence, the correctness and reliability of <BR>
software driving these systems have become issues of utmost importance.</SPAN></o:p></P>
<P class=MsoNormal style="MARGIN: 0in 0in 0pt"><o:p><SPAN style="FONT-SIZE: 12pt; FONT-FAMILY: Times New Roman"> </SPAN></o:p></P>
<P class=MsoNormal style="MARGIN: 0in 0in 0pt"><o:p><SPAN style="FONT-SIZE: 12pt; FONT-FAMILY: Times New Roman">Recently, the buzzword “verified software” has received a lot of attention. <BR>
Several workshops have been conducted (e.g., VSTTE ) and grand challenges <BR>
in constructing verified software have been laid out by eminent researchers. </SPAN></o:p></P>
<P class=MsoNormal style="MARGIN: 0in 0in 0pt"><o:p><SPAN style="FONT-SIZE: 12pt; FONT-FAMILY: Times New Roman">While constructing provably bug-free software remains the holy grail <BR>
in developing trustworthy computing systems, we believe that software reliability is <BR>
more than that. We believe that software bugs are there to stay; hence along with the <BR>
goal of producing provably correct software, software reliability research should <BR>
also focus on developing techniques that enable software systems to perform their <BR>
tasks correctly even in the presence of bugs while undergoing only <BR>
“graceful degradation”. Software systems should be able to adapt themselves <BR>
in response to changing environments. This includes automated detection of faults <BR>
at runtime, automated discovery and management of resources, automated recovery <BR>
from possible failures of components and breaches of networks, and <BR>
automated reconfiguration in response to changing requirements. </SPAN></o:p></P>
<P class=MsoNormal style="MARGIN: 0in 0in 0pt"><o:p><SPAN style="FONT-SIZE: 12pt; FONT-FAMILY: Times New Roman"> </SPAN></o:p></P>
<P class=MsoNormal style="MARGIN: 0in 0in 0pt"><o:p><SPAN style="FONT-SIZE: 12pt; FONT-FAMILY: Times New Roman">We are particularly interested in papers reporting applications of formal methods in developing provably adaptable software; <BR>
software that that comes with guarantees of continuing to run correctly even under <BR>
rapidly changing contexts. Topics of interest include but are not restricted to</SPAN></o:p></P><o:p><SPAN style="FONT-SIZE: 12pt; FONT-FAMILY: Times New Roman">
<P class=MsoNormal style="MARGIN: 0in 0in 0pt"><o:p><SPAN style="FONT-SIZE: 12pt; FONT-FAMILY: Times New Roman"> <BR>
- Verification of adaptable software systems<BR>
- Verified fault-tolerance<BR>
- Survivability<BR>
- Formal approaches to developing reliable service-oriented systems<BR>
- Software synthesis<BR>
- Reliable infrastructures<BR>
- Reliable integration of components<BR>
- Formal methods for agile software development<BR>
- Model driven approaches for creating reliable software</SPAN></o:p></P>
<P class=MsoNormal style="MARGIN: 0in 0in 0pt"><o:p><SPAN style="FONT-SIZE: 12pt; FONT-FAMILY: Times New Roman">- Program result checking<BR>
- Certified code generation from models<BR>
</SPAN></o:p></P>
<P class=MsoNormal style="MARGIN: 0in 0in 0pt"><o:p><SPAN style="FONT-SIZE: 12pt; FONT-FAMILY: Times New Roman"> <BR>
<o:p><SPAN style="FONT-SIZE: 12pt; FONT-FAMILY: Times New Roman"> </SPAN></o:p></P>
<P class=MsoNormal style="MARGIN: 0in 0in 0pt"><o:p><SPAN style="FONT-SIZE: 12pt; FONT-FAMILY: Times New Roman">Workshop Website: <A href="http://chacs.nrl.navy.mil/projects/AVIS07/index.html" target=_blank>http://chacs.nrl.navy.mil/projects/AVIS07/index.html</A></SPAN></o:p></P>
<P class=MsoNormal style="MARGIN: 0in 0in 0pt"><o:p><SPAN style="FONT-SIZE: 12pt; FONT-FAMILY: Times New Roman"></SPAN></o:p> </P>
<P class=MsoNormal style="MARGIN: 0in 0in 0pt"><o:p><SPAN style="FONT-SIZE: 12pt; FONT-FAMILY: Times New Roman">Workshop Location: Braga, Portugal</SPAN></o:p></P>
<P class=MsoNormal style="MARGIN: 0in 0in 0pt"><o:p><SPAN style="FONT-SIZE: 12pt; FONT-FAMILY: Times New Roman"> </SPAN></o:p></P>
<P class=MsoNormal style="MARGIN: 0in 0in 0pt"><o:p><SPAN style="FONT-SIZE: 12pt; FONT-FAMILY: Times New Roman">Important Dates - AVIS 2007</SPAN></o:p></P><o:p><SPAN style="FONT-SIZE: 12pt; FONT-FAMILY: Times New Roman">
<P class=MsoNormal style="MARGIN: 0in 0in 0pt"><BR>
16th January 2007 - Submission of papers (not to exceed 12 pages)<BR>
12th February 2007 - Notification of acceptance<BR>
5th March 2007 - Camera-ready copies due<BR>
31st March 2007 – Workshop</P>
<P class=MsoNormal style="MARGIN: 0in 0in 0pt"> </P>
<P class=MsoNormal style="MARGIN: 0in 0in 0pt">Accepted papers will get published in an issue of the Electronic Notes in Theoretical Computer Science (ENTCS). </P>
<P class=MsoNormal style="MARGIN: 0in 0in 0pt"> </P>
<P class=MsoNormal style="MARGIN: 0in 0in 0pt">Organizers: </P>
<P class=MsoNormal style="MARGIN: 0in 0in 0pt">Dr.Ramesh Bharadwaj<BR>
Center for High Assurance Computer Systems<BR>
Naval Research Laboratory<BR>
Washington DC 20375 USA<BR>
<A href="http://webmail.usu.edu/DEFANGED_javascript:top.opencompose('avis07@chacs.nrl.navy.mil','','','')" target=_blank>avis07@chacs.nrl.navy.mil</A><BR>
+1-202-767-7210</P>
<P class=MsoNormal style="MARGIN: 0in 0in 0pt"> </P>
<P class=MsoNormal style="MARGIN: 0in 0in 0pt">Dr. Supratik Mukhopadhyay<BR>
Department of Computer Science <BR>
Utah State University<BR>
Logan, UT, 84322, USA<BR>
+1-435-797-3267</P>
<P class=MsoNormal style="MARGIN: 0in 0in 0pt"><SPAN style="FONT-FAMILY: Arial"></SPAN></SPAN></o:p></SPAN></o:p></SPAN></o:p></P></HTML>
<BR>---- Msg sent via USU WebMail - http://webmail.usu.edu/