Tuesday 6 November 2007, Atlanta, Georgia, USA

In association with the 22nd IEEE/ACM International Conference on Automated Software Engineering (ASE 2007)

Workshop Description   Workshop Committee   Workshop Program   Abstracts   Proceedings   Workshop Location   Contacts

This was the second in the Automated Formal Methods (AFM) workshop series, which began with AFM06. AFM functions both as a user's meeting for the SRI tools PVS, SAL (with HybridSAL), and Yices, and as a general workshop for those interested in state of the art automation for formal methods.

Workshop Description

AFM is particularly interested in the use (rather than the construction) of highly automated tools for formal methods and the tight or loose integration of different methods into tool chains that strive to provide end-to-end automation for all aspects of software development. Users of all levels of expertise are invited to report on their experiences.

Workshop Program

The full program included nine contributed papers (listed below) selected by the international program committee, brief descriptions of new developments in the SRI tool suite, and short presentations (five minutes, five slides) on ongoing work from the user community.

Schedule

Abstracts

Leonardo de Moura, Microsoft Research
SMT @ Microsoft

Abstract: Decision procedures for checking satisfiability of logical formulas are crucial for many verification applications. Of particular recent interest are solvers for Satisfiability Modulo Theories (SMT). The success of SMT is largely due to the supported background theories: uninterpreted functions; real or integer arithmetic; and theories of program or hardware structures such as bit-vectors and arrays.

SMT solvers are used in several projects at Microsoft, the main applications are: program verification, test case generation, whitebox fuzz testing, predicate abstraction, and internet worm prevention. In this talk, we will describe these projects, their requirements, and how they influenced the design and implementation of SMT solvers.

Thomas Weigert

Verify the requirements for large telecommunications systems

Abstract: The most expensive failures of computer-based systems are due to unanticipated interactions between system components. In telecommunications systems, this problem has long been known as the "feature interaction problem" and a series of conferences is dedicated to developing solutions to this costly source of errors. With the advent of more sophisticated user interactions, this problem has spread to web services, email systems, user interfaces for consumer devices, and many more.

While a number of research approaches to solving the feature interaction problem have been presented, these have not significantly impacted industrial system development. We believe, this is due to that the mathematical representations chosen to model system behavior have pushed solutions towards formalisms that are inaccessible to the majority of engineers and also towards implementations that are not able to cope with the enormous state spaces induced by todayls computer systems.

We have implemented a verification system based on an alternative mathematical model of behavior (Letichevsky's theory of agents and environments) and have been able to express popular engineering notations such as UML sequence diagrams within this framework in a manner that allows efficient reasoning over such specifications. Our tool has been successfully deployed to prove the correctness of large, industrial-scale system specifications and which has been able to detect serious defects in each of these specifications. Detecting such defects before implementation promises a dramatic reduction in the cost of quality of large software-based systems.

Workshop Proceedings

Workshop Committee

Workshop Location

Workshop Organizers