[ The Types Forum (announcements only), 
     http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]


The Sixth International Workshop on Automated Verification of Infinite State Systems
(AVIS 2007) is a forum for researchers, students, and practitioners interested in the
application of formal methods and tools for the automatied verification of large
practical systems. Formal methods, in particular model checking, is increasingly
being used in industry to automatically establish the correctness of
(and to find flaws in) finite-state systems, such as descriptions of hardware
and protocols. However, model checking is limited in scope due to the state explosion
problem. Most practical system descriptions, notably that of software, are therefore not
directly amenable to finite-state verification methods since they have very large or
infinite state spaces.
For such systems, theorem proving -- a process that requires manual effort and
mathematical sophistication to use -- has so far been the only viable alternative.
More recently, we have seen the emergence of hybrid techniques that combine the
ease-of-use of model checkers with the power of theorem provers.
Tools based on these techniques afford users with full automation, and are less
sensitive to the size of the state space (which may be infinite or arbitrarily large).
There is a growing body of knowledge in this field which has a very exciting future.


The intention of this workshop is to build a forum for exchanging ideas and experiences
by bringing together theoreticians, tool builders, as well as practitioners who are
interested in this emerging area of research in formal verification. 
The theme of AVIS 2007  will be  “reliable software”.

Software is increasingly becoming the driving force  of modern civilization,
playing an increasingly important  role in modern society.  
Human civilization is   becoming more and more dependent on software, as increasingly
capable and cheap hardware processors and communication devices are routinely being
embedded into an ever-growing list of physical systems.  Software is now being used
for controlling mission-critical systems such as nuclear power plants, patient monitors,
and spacecrafts.  Bugs in software systems controlling safety critical applications
can cause loss of life and property.  Hence, the correctness and reliability of 
software driving these systems have become issues of utmost importance.


Recently, the buzzword “verified software” has received a lot of attention.
Several workshops have been conducted (e.g., VSTTE ) and grand challenges
in constructing verified software have been laid out by eminent  researchers.

While constructing  provably bug-free  software remains the holy grail
in developing trustworthy computing systems, we believe that  software reliability is
more than that. We believe that software bugs are there to stay;  hence along with the
goal of producing provably correct software, software reliability research should
also focus on developing techniques that enable software systems to perform their
tasks correctly even in the presence of bugs while undergoing only
“graceful degradation”. Software systems should be able to adapt themselves
in response to changing environments. This includes automated detection of faults
at runtime, automated  discovery and management of resources, automated recovery
from possible failures of  components  and breaches of networks, and
automated reconfiguration in response to changing requirements.  


We are particularly interested in  papers reporting  applications of formal methods in developing provably adaptable software;
software that that comes with guarantees of continuing  to run correctly even under
rapidly changing contexts. Topics of interest include but are not restricted to

- Verification of adaptable software systems
- Verified fault-tolerance
- Survivability
- Formal approaches to developing reliable service-oriented systems
- Software synthesis
- Reliable infrastructures
- Reliable integration of components
- Formal methods for  agile software development
- Model driven approaches for creating reliable software

- Program result checking
- Certified code generation from models


Workshop Website: http://chacs.nrl.navy.mil/projects/AVIS07/index.html


Workshop Location: Braga, Portugal


Important Dates - AVIS 2007

16th January 2007 - Submission of papers (not to exceed 12 pages)
12th February 2007 - Notification of acceptance
5th March 2007 - Camera-ready copies due
31st March 2007 – Workshop


Accepted papers will get  published in an issue of the Electronic Notes in Theoretical Computer Science (ENTCS).



Dr.Ramesh Bharadwaj
Center for High Assurance Computer Systems
Naval Research Laboratory
Washington DC 20375 USA


Dr. Supratik Mukhopadhyay
Department of Computer Science
Utah State University
Logan, UT, 84322, USA

---- Msg sent via USU WebMail - http://webmail.usu.edu/

Reply via email to